bugfix in DNNF Compiler

booleworks · Nov 22, 2024 · 8b7745b · 8b7745b
1 parent 6093cd7
commit 8b7745b
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/core/src/main/java/com/booleworks/logicng/knowledgecompilation/dnnf/DnnfCompiler.java b/core/src/main/java/com/booleworks/logicng/knowledgecompilation/dnnf/DnnfCompiler.java
@@ -300,11 +300,11 @@ protected LngResult<Formula> conjoin(final Formula implied, final DTreeNode tree
             return LngResult.of(f.falsum());
         }
         final LngResult<Formula> left = cnfAux(tree.left(), currentShannons, handler);
-        if (left.getResult() == null || left.getResult() == f.falsum()) {
+        if (!left.isSuccess() || left.getResult() == f.falsum()) {
             return left;
         }
         final LngResult<Formula> right = cnfAux(tree.right(), currentShannons, handler);
-        if (right.getResult() == null || right.getResult() == f.falsum()) {
+        if (!right.isSuccess() || right.getResult() == f.falsum()) {
             return right;
         }
         return LngResult.of(f.and(implied, left.getResult(), right.getResult()));
@@ -319,7 +319,7 @@ protected LngResult<Formula> cnfAux(final DTree tree, final int currentShannons,
                 return LngResult.of(cache.get(key));
             } else {
                 final LngResult<Formula> dnnf = cnf2Ddnnf(tree, handler);
-                if (dnnf.getResult() != null && dnnf.getResult() != f.falsum()) {
+                if (dnnf.isSuccess() && dnnf.getResult() != f.falsum()) {
                     cache.put((BitSet) key.clone(), dnnf.getResult());
                 }
                 return dnnf;