Fixed a bug that caused unintended creation of terminal nodes

ftsrg · Feb 20, 2024 · 9d786af · 9d786af
1 parent 105f3ea
commit 9d786af
Showing 1 changed file with 18 additions and 15 deletions.
diff --git a/.../mit/theta/analysis/algorithm/symbolic/symbolicnode/expression/MddExpressionTemplate.java b/.../mit/theta/analysis/algorithm/symbolic/symbolicnode/expression/MddExpressionTemplate.java
@@ -51,30 +51,33 @@ public RecursiveIntObjMapView<? extends MddNode> toCanonicalRepresentation(MddVa
 
         final Expr<BoolType> canonizedExpr = ExprUtils.canonize(ExprUtils.simplify(expr));
 
-        // TODO: we might not need this
-        // Check if terminal 1
-        if (ExprUtils.getConstants(canonizedExpr).isEmpty()) {
-            if (canonizedExpr instanceof FalseExpr) {
-                return mddVariable.getMddGraph().getTerminalZeroNode();
-            } /*else {
-                final MddGraph<Expr> mddGraph = (MddGraph<Expr>) mddVariable.getMddGraph();
-                return mddGraph.getNodeFor(canonizedExpr);
-            }*/
+//        // TODO: we might not need this
+//        // Check if terminal 1
+//        if (ExprUtils.getConstants(canonizedExpr).isEmpty()) {
+//            if (canonizedExpr instanceof FalseExpr) {
+//                return mddVariable.getMddGraph().getTerminalZeroNode();
+//            } /*else {
+//                final MddGraph<Expr> mddGraph = (MddGraph<Expr>) mddVariable.getMddGraph();
+//                return mddGraph.getNodeFor(canonizedExpr);
+//            }*/
+//        }
+
+        // Check if terminal 0
+        if (canonizedExpr instanceof FalseExpr || !isSat(canonizedExpr, solverPool)) {
+            return mddVariable.getMddGraph().getTerminalZeroNode();
         }
 
-        // Check if default
+        // Check if default or terminal 1
         if (!ExprUtils.getConstants(canonizedExpr).contains(decl)) {
             if (mddVariable.getLower().isPresent()) {
                 final MddNode childNode = mddVariable.getLower().get().checkInNode(new MddExpressionTemplate(canonizedExpr, o -> (Decl) o, solverPool));
                 return MddExpressionRepresentation.ofDefault(canonizedExpr, decl, mddVariable, solverPool, childNode);
+            } else {
+                final MddGraph<Expr> mddGraph = (MddGraph<Expr>) mddVariable.getMddGraph();
+                return mddGraph.getNodeFor(canonizedExpr);
             }
         }
 
-        // Check if terminal 0
-        if (!isSat(canonizedExpr, solverPool)) {
-            return mddVariable.getMddGraph().getTerminalZeroNode();
-        }
-
         return MddExpressionRepresentation.of(canonizedExpr, decl, mddVariable, solverPool);
 
     }