From 71ba6b048aada6b97789c9e1cec1f93cd47504f3 Mon Sep 17 00:00:00 2001 From: mondokm Date: Tue, 20 Feb 2024 11:56:56 +0100 Subject: [PATCH] Temporarily disabled defaultvalue, because it is not handled in saturation --- .../expression/MddExpressionTemplate.java | 21 ++++++++++--------- 1 file changed, 11 insertions(+), 10 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 98226f69cb..14adc106e8 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 @@ -67,16 +67,17 @@ public RecursiveIntObjMapView toCanonicalRepresentation(MddVa return mddVariable.getMddGraph().getTerminalZeroNode(); } - // 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 mddGraph = (MddGraph) mddVariable.getMddGraph(); - return mddGraph.getNodeFor(canonizedExpr); - } - } + // 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 mddGraph = (MddGraph) mddVariable.getMddGraph(); +// childNode = mddGraph.getNodeFor(canonizedExpr); +// } +// return MddExpressionRepresentation.ofDefault(canonizedExpr, decl, mddVariable, solverPool, childNode); +// } return MddExpressionRepresentation.of(canonizedExpr, decl, mddVariable, solverPool);