From ef9dfaa6577571cd600314d8c23fcd794d5fedfa Mon Sep 17 00:00:00 2001 From: mondokm Date: Wed, 21 Feb 2024 10:02:06 +0100 Subject: [PATCH] Fixed a bug that could result in unsat terminal nodes --- .../expression/MddExpressionRepresentation.java | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/symbolic/symbolicnode/expression/MddExpressionRepresentation.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/symbolic/symbolicnode/expression/MddExpressionRepresentation.java index 366a946cb3..7caa2b98fe 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/symbolic/symbolicnode/expression/MddExpressionRepresentation.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/symbolic/symbolicnode/expression/MddExpressionRepresentation.java @@ -115,7 +115,20 @@ public MddNode get(int key) { } else { final Expr canonizedExpr = ExprUtils.canonize(ExprUtils.simplify(simplifiedExpr)); MddGraph mddGraph = (MddGraph) mddVariable.getMddGraph(); - childNode = canonizedExpr instanceof FalseExpr ? mddGraph.getTerminalZeroNode() : mddGraph.getNodeFor(canonizedExpr); + + if (canonizedExpr instanceof FalseExpr) { + childNode = mddGraph.getTerminalZeroNode(); + } else { + var solver = solverPool.requestSolver(); + try (var wpp = new WithPushPop(solver)) { + solver.add(canonizedExpr); + if (solver.check().isSat()) { + childNode = mddGraph.getNodeFor(canonizedExpr); + } else { + childNode = mddGraph.getTerminalZeroNode(); + } + } + } } if (!childNode.equals(mddVariable.getMddGraph().getTerminalZeroNode()))