Enable default values for unbounded domains

ftsrg · Feb 20, 2024 · a3b3071 · a3b3071
1 parent b09d67f
commit a3b3071
Showing 1 changed file with 10 additions and 10 deletions.
diff --git a/.../mit/theta/analysis/algorithm/symbolic/symbolicnode/expression/MddExpressionTemplate.java b/.../mit/theta/analysis/algorithm/symbolic/symbolicnode/expression/MddExpressionTemplate.java
@@ -68,16 +68,16 @@ public RecursiveIntObjMapView<? extends MddNode> toCanonicalRepresentation(MddVa
         }
 
         // Check if default
-//        if (!ExprUtils.getConstants(canonizedExpr).contains(decl)) {
-//            final MddNode childNode;
-//            if (mddVariable.getLower().isPresent()) {
-//                childNode = mddVariable.getLower().get().checkInNode(new MddExpressionTemplate(canonizedExpr, o -> (Decl) o, solverPool));
-//            } else {
-//                final MddGraph<Expr> mddGraph = (MddGraph<Expr>) mddVariable.getMddGraph();
-//                childNode = mddGraph.getNodeFor(canonizedExpr);
-//            }
-//            return MddExpressionRepresentation.ofDefault(canonizedExpr, decl, mddVariable, solverPool, childNode);
-//        }
+        if (mddVariable.getDomainSize() == 0 && !ExprUtils.getConstants(canonizedExpr).contains(decl)) {
+            final MddNode childNode;
+            if (mddVariable.getLower().isPresent()) {
+                childNode = mddVariable.getLower().get().checkInNode(new MddExpressionTemplate(canonizedExpr, o -> (Decl) o, solverPool));
+            } else {
+                final MddGraph<Expr> mddGraph = (MddGraph<Expr>) mddVariable.getMddGraph();
+                childNode = mddGraph.getNodeFor(canonizedExpr);
+            }
+            return MddExpressionRepresentation.ofDefault(canonizedExpr, decl, mddVariable, solverPool, childNode);
+        }
 
         return MddExpressionRepresentation.of(canonizedExpr, decl, mddVariable, solverPool);