Merge pull request #389 from ftsrg/satfix

Fix issue with simple saturation and improve identity detection

Author: mondokm

build.gradle.kts

@@ -29,7 +29,7 @@ buildscript {
 
 allprojects {
     group = "hu.bme.mit.theta"
-    version = "6.19.0"
+    version = "6.19.1"
 
 
     apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts"))

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/ansd/impl/OnTheFlyReachabilityNextStateDescriptor.java

@@ -93,7 +93,7 @@ public IntObjMapView<AbstractNextStateDescriptor> getDiagonal(StateSpaceInfo loc
                 : new IntObjMapViews.Transforming<>(
                         wrapped.getDiagonal(localStateSpace),
                         (descriptor, key) -> {
-                            if (key == null) return AbstractNextStateDescriptor.terminalEmpty();
+                            if (key == null) return descriptor;
                             return OnTheFlyReachabilityNextStateDescriptor.of(
                                     descriptor, target.get(key), killSwitch);
                         });

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/expressionnode/MddExpressionRepresentation.java

@@ -613,14 +613,16 @@ private void cacheModel(Valuation valuation) {
                     }
                 }
 
-                if (childNode.isTerminal()) break;
+                if (childNode.isTerminal()) return;
 
                 // Preconditions.checkArgument(childNode.getRepresentation() instanceof
                 // MddExpressionRepresentation);
                 // TODO assert
                 var nextRepr = childNode.getRepresentation();
                 while (nextRepr instanceof IdentityRepresentation identity) {
-                    nextRepr = identity.getContinuation().getRepresentation();
+                    var cont = identity.getContinuation();
+                    if (cont.isTerminal()) return;
+                    nextRepr = cont.getRepresentation();
                 }
                 representation = (MddExpressionRepresentation) nextRepr;
             }

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/expressionnode/MddExpressionTemplate.java

@@ -126,9 +126,7 @@ public RecursiveIntObjMapView<? extends MddNode> toCanonicalRepresentation(
 
         if (transExpr
                 && decl instanceof IndexedConstDecl<?> constDecl
-                && constDecl.getIndex() == 0
-                && mddVariable.getLower().isPresent()
-                && mddVariable.getLower().get().getLower().isPresent()) {
+                && constDecl.getIndex() == 0) {
             final Substitution sub =
                     BasicSubstitution.builder()
                             .put(
@@ -138,18 +136,25 @@ public RecursiveIntObjMapView<? extends MddNode> toCanonicalRepresentation(
             final Expr<BoolType> identityContinuationExpr =
                     ExprUtils.simplify(sub.apply(canonizedExpr));
             if (!ExprUtils.getConstants(identityContinuationExpr).contains(decl)) {
-                final var cont =
-                        mddVariable
-                                .getLower()
-                                .get()
-                                .getLower()
-                                .get()
-                                .checkInNode(
-                                        new MddExpressionTemplate(
-                                                identityContinuationExpr,
-                                                extractDecl,
-                                                solverPool,
-                                                transExpr));
+                final MddNode cont;
+                if (mddVariable.getLower().isPresent()
+                        && mddVariable.getLower().get().getLower().isPresent()) {
+                    cont =
+                            mddVariable
+                                    .getLower()
+                                    .get()
+                                    .getLower()
+                                    .get()
+                                    .checkInNode(
+                                            new MddExpressionTemplate(
+                                                    identityContinuationExpr,
+                                                    extractDecl,
+                                                    solverPool,
+                                                    transExpr));
+                } else {
+                    final MddGraph<Expr> mddGraph = (MddGraph<Expr>) mddVariable.getMddGraph();
+                    cont = mddGraph.getNodeFor(identityContinuationExpr);
+                }
                 return new IdentityRepresentation(cont);
             }
         }