From 9d786af51784fe2987029fad88923ef126b847c8 Mon Sep 17 00:00:00 2001
From: mondokm <milanmondok1998@gmail.com>
Date: Tue, 20 Feb 2024 10:12:29 +0100
Subject: [PATCH] Fixed a bug that caused unintended creation of terminal nodes

---
 .../expression/MddExpressionTemplate.java     | 33 ++++++++++---------
 1 file changed, 18 insertions(+), 15 deletions(-)

diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/symbolic/symbolicnode/expression/MddExpressionTemplate.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/symbolic/symbolicnode/expression/MddExpressionTemplate.java
index c502de0431..98226f69cb 100644
--- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/symbolic/symbolicnode/expression/MddExpressionTemplate.java
+++ b/subprojects/common/analysis/src/main/java/hu/bme/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);
 
     }