Add DNF/CNF absorption by default

cjdrake · Mar 1, 2015 · 2643466 · 2643466
1 parent d8092f1
commit 2643466
Showing 1 changed file with 4 additions and 12 deletions.
diff --git a/extension/boolexpr/flatten.c b/extension/boolexpr/flatten.c
@@ -208,18 +208,14 @@ _to_dnf(struct BoolExpr *nnf)
         CHECK_NULL(temp, _op_transform(nnf, _to_dnf));
         CHECK_NULL_1(nf1, _simplify(temp), temp);
         BoolExpr_DecRef(temp);
-
-        /* a ; a | b | c ; a & b & c ; a & b | c & d */
-        if (IS_ATOM(nf1) || _is_clause(nf1) || IS_OR(nf1))
-            return nf1;
-
-        /* (a | b) & (c | d) */
         CHECK_NULL_1(nf2, _absorb(nf1), nf1);
         BoolExpr_DecRef(nf1);
 
+        /* a ; a | b | c ; a & b & c ; a & b | c & d */
         if (IS_ATOM(nf2) || _is_clause(nf2) || IS_OR(nf2))
             return nf2;
 
+        /* (a | b) & (c | d) */
         CHECK_NULL_1(temp, _distribute(OP_AND, nf2), nf2);
         BoolExpr_DecRef(nf2);
         CHECK_NULL_1(dnf, _absorb(temp), temp);
@@ -245,18 +241,14 @@ _to_cnf(struct BoolExpr *nnf)
         CHECK_NULL(temp, _op_transform(nnf, _to_cnf));
         CHECK_NULL_1(nf1, _simplify(temp), temp);
         BoolExpr_DecRef(temp);
-
-        /* a ; a | b | c ; a & b & c ; (a | b) & (c | d) */
-        if (IS_ATOM(nf1) || _is_clause(nf1) || IS_AND(nf1))
-            return nf1;
-
-        /* a & b | c & d */
         CHECK_NULL_1(nf2, _absorb(nf1), nf1);
         BoolExpr_DecRef(nf1);
 
+        /* a ; a | b | c ; a & b & c ; (a | b) & (c | d) */
         if (IS_ATOM(nf2) || _is_clause(nf2) || IS_AND(nf2))
             return nf2;
 
+        /* a & b | c & d */
         CHECK_NULL_1(temp, _distribute(OP_OR, nf2), nf2);
         BoolExpr_DecRef(nf2);
         CHECK_NULL_1(cnf, _absorb(temp), temp);