fix for issue #4

logic-ng · Aug 12, 2016 · 3870b4f · 3870b4f
1 parent 72fcf2c
commit 3870b4f
Show file tree

Hide file tree

Showing 2 changed files with 20 additions and 3 deletions.
diff --git a/src/main/java/org/logicng/transformations/cnf/CNFFactorization.java b/src/main/java/org/logicng/transformations/cnf/CNFFactorization.java
@@ -100,9 +100,10 @@ public Formula apply(final Formula formula, boolean cache) {
       case AND:
         nops = new LinkedHashSet<>();
         for (final Formula op : formula) {
+          final Formula apply = this.apply(op, cache);
           if (!this.proceed)
             return null;
-          nops.add(this.apply(op, cache));
+          nops.add(apply);
         }
         cached = formula.factory().and(nops);
         break;
@@ -133,8 +134,12 @@ private Formula distribute(final Formula f1, final Formula f2) {
       final FormulaFactory f = f1.factory();
       if (f1.type() == AND || f2.type() == AND) {
         final LinkedHashSet<Formula> nops = new LinkedHashSet<>();
-        for (final Formula op : f1.type() == AND ? f1 : f2)
-          nops.add(this.distribute(op, f1.type() == AND ? f2 : f1));
+        for (final Formula op : f1.type() == AND ? f1 : f2) {
+          final Formula distribute = this.distribute(op, f1.type() == AND ? f2 : f1);
+          if (!this.proceed)
+            return null;
+          nops.add(distribute);
+        }
         return f.and(nops);
       }
       final Formula clause = f.or(f1, f2);

diff --git a/src/test/java/org/logicng/transformations/cnf/CNFEncoderTest.java b/src/test/java/org/logicng/transformations/cnf/CNFEncoderTest.java
@@ -154,4 +154,16 @@ public void testAdvancedEncoder() throws ParserException {
     Assert.assertEquals(p.parse("(z1 | z2) & z3 & z4 & (~@RESERVED_CNF_2 | z1) & (~@RESERVED_CNF_2 | z5) & (~@RESERVED_CNF_2 | ~z6) & (~@RESERVED_CNF_2 | ~z7) & (@RESERVED_CNF_2 | ~z1 | ~z5 | z6 | z7) & (@RESERVED_CNF_2 | z8 | z9)"), encoder3.encode(phi3));
   }
 
+  @Test
+  public void testBug() throws ParserException {
+    final FormulaFactory f = new FormulaFactory();
+    final PropositionalParser parser = new PropositionalParser(f);
+    final Formula f1 = parser.parse("(x10 & x9 & x3 & x12 | x10 & x9 & x8 | x9 & x8 & x12) & ~x5 & ~x7 & x1 | (x10 & x9 & x3 & x12 | x10 & x9 & x8 | x9 & x8 & x12) & ~(x11 & x3) & ~(x11 & x8) & ~x5 & ~x7 & x0");
+    final Formula f2 = parser.parse("x1 & x3 & x4");
+    final Formula f3 = parser.parse("(x10 & x9 & x3 & x12 | x10 & x9 & x8 | x9 & x8 & x12) & ~(x11 & x3) & ~(x11 & x8 & x12) & ~x5 & ~x7 & x1 | (x10 & x9 & x3 & x12 | x10 & x9 & x8 | x9 & x8 & x12) & ~(x11 & x3) & ~(x11 & x8) & ~x5 & ~x7 & x0 | x3 & x4 & ~x5 & ~x7 & x1 | x3 & x4 & ~x5 & ~x7 & x0 | x2 & x6 & ~x5 & ~x7 & x0");
+    final Formula f4 = parser.parse("(x1 & x3 & x4 | x0 & (x2 & x6 | x3 & x4) | x9 & (x1 & x10 & x8 & ~x12 & x3 | (x1 | x0) & (x12 & (x10 & x3 | x8) | x10 & x8) & ~x11)) & ~x5 & ~x7");
+    Assert.assertNotEquals(null, f.not(f.equivalence(f1, f2)).cnf());
+    Assert.assertNotEquals(null, f.not(f.equivalence(f3, f4)).cnf());
+  }
+
 }