MDD look-ahead optimizations

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddChecker.kt

@@ -1,5 +1,5 @@
 /*
- *  Copyright 2025 Budapest University of Technology and Economics
+ *  Copyright 2025-2026 Budapest University of Technology and Economics
  *
  *  Licensed under the Apache License, Version 2.0 (the "License");
  *  you may not use this file except in compliance with the License.
@@ -30,6 +30,7 @@ import hu.bme.mit.theta.analysis.algorithm.mdd.ansd.AbstractNextStateDescriptor
 import hu.bme.mit.theta.analysis.algorithm.mdd.ansd.impl.*
 import hu.bme.mit.theta.analysis.algorithm.mdd.expressionnode.ExprLatticeDefinition
 import hu.bme.mit.theta.analysis.algorithm.mdd.expressionnode.MddExplicitRepresentationExtractor
+import hu.bme.mit.theta.analysis.algorithm.mdd.expressionnode.MddExpressionRepresentation
 import hu.bme.mit.theta.analysis.algorithm.mdd.expressionnode.MddExpressionTemplate
 import hu.bme.mit.theta.analysis.algorithm.mdd.fixedpoint.*
 import hu.bme.mit.theta.analysis.expl.ExplState
@@ -59,6 +60,8 @@ constructor(
   private val iterationStrategy: IterationStrategy = IterationStrategy.GSAT,
   private val traceTimeout: Long = 10,
   private val variableOrdering: List<VarDecl<*>> = monolithicExpr.orderVars(),
+  private val mddToExprStrategy: MddExpressionRepresentation.MddToExprStrategy =
+    MddExpressionRepresentation.MddToExprStrategy.VARIABLE_LEVEL,
 ) : SafetyChecker<MddProof, Trace<ExplState, ExprAction>, UnitPrec> {
 
   enum class IterationStrategy {
@@ -70,6 +73,8 @@ constructor(
   override fun check(prec: UnitPrec?): SafetyResult<MddProof, Trace<ExplState, ExprAction>> {
     val totalTime = Stopwatch.createStarted()
 
+    MddExpressionRepresentation.setMddToExprStrategy(mddToExprStrategy)
+
     val mddGraph = JavaMddFactory.getDefault().createMddGraph(ExprLatticeDefinition.forExpr())
 
     val stateOrder = JavaMddFactory.getDefault().createMddVariableOrder(mddGraph)

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddSinglePathExtractor.kt

@@ -1,5 +1,5 @@
 /*
- *  Copyright 2025 Budapest University of Technology and Economics
+ *  Copyright 2025-2026 Budapest University of Technology and Economics
  *
  *  Licensed under the Apache License, Version 2.0 (the "License");
  *  you may not use this file except in compliance with the License.
@@ -36,7 +36,7 @@ object MddSinglePathExtractor {
       } else {
         val cursor = node.cursor()
         cursor.moveNext()
-        templateBuilder.set(cursor.key(), transform(cursor.value()).node)
+        templateBuilder.set(cursor.key(), transform(cursor.value() as MddHandle).node)
       }
 
       return node.variableHandle.checkInNode(

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

@@ -1,5 +1,5 @@
 /*
- *  Copyright 2025 Budapest University of Technology and Economics
+ *  Copyright 2025-2026 Budapest University of Technology and Economics
  *
  *  Licensed under the Apache License, Version 2.0 (the "License");
  *  you may not use this file except in compliance with the License.
@@ -73,7 +73,7 @@ private static void collect(
                                     node.getVariableHandle().getVariable().orElseThrow(),
                                     cursor.key()));
 
-                    collect(cursor.value(), assignments, valuations);
+                    collect((MddHandle) cursor.value(), assignments, valuations);
 
                     assignments.pop();
                 }

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

@@ -1,5 +1,5 @@
 /*
- *  Copyright 2025 Budapest University of Technology and Economics
+ *  Copyright 2025-2026 Budapest University of Technology and Economics
  *
  *  Licensed under the Apache License, Version 2.0 (the "License");
  *  you may not use this file except in compliance with the License.
@@ -16,7 +16,7 @@
 package hu.bme.mit.theta.analysis.algorithm.mdd.ansd;
 
 import hu.bme.mit.delta.collections.IntSetView;
-import hu.bme.mit.delta.java.mdd.MddNode;
+import hu.bme.mit.delta.collections.RecursiveIntObjMapView;
 
 /**
  * Represents a sub-state space of the system under analysis. Instances of this type have some sort
@@ -67,5 +67,5 @@ default <T> T getTraceInfo(Class<T> typeToken) {
      */
     public StateSpaceInfo getLocalStateSpace(Object someLowerComponent);
 
-    public MddNode toStructuralRepresentation();
+    public RecursiveIntObjMapView<?> toStructuralRepresentation();
 }

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

@@ -1,5 +1,5 @@
 /*
- *  Copyright 2025 Budapest University of Technology and Economics
+ *  Copyright 2025-2026 Budapest University of Technology and Economics
  *
  *  Licensed under the Apache License, Version 2.0 (the "License");
  *  you may not use this file except in compliance with the License.
@@ -19,6 +19,7 @@
 import hu.bme.mit.delta.collections.IntObjCursor;
 import hu.bme.mit.delta.collections.IntObjMapView;
 import hu.bme.mit.delta.collections.RecursiveIntObjCursor;
+import hu.bme.mit.delta.collections.RecursiveIntObjMapView;
 import hu.bme.mit.delta.collections.impl.IntObjMapViews;
 import hu.bme.mit.delta.java.mdd.MddHandle;
 import hu.bme.mit.delta.java.mdd.MddNode;
@@ -88,7 +89,7 @@ public boolean evaluate() {
 
     @Override
     public IntObjMapView<AbstractNextStateDescriptor> getDiagonal(StateSpaceInfo localStateSpace) {
-        final MddNode constraint = localStateSpace.toStructuralRepresentation();
+        final RecursiveIntObjMapView<?> constraint = localStateSpace.toStructuralRepresentation();
         return new ConstrainedIntObjMapView<>(
                 new IntObjMapViews.Transforming<>(
                         node,
@@ -109,7 +110,7 @@ public IntObjMapView<AbstractNextStateDescriptor> getDiagonal(StateSpaceInfo loc
     @Override
     public IntObjMapView<IntObjMapView<AbstractNextStateDescriptor>> getOffDiagonal(
             StateSpaceInfo localStateSpace) {
-        final MddNode constraint = localStateSpace.toStructuralRepresentation();
+        final RecursiveIntObjMapView<?> constraint = localStateSpace.toStructuralRepresentation();
         return new IntObjMapViews.Transforming<>(
                 node,
                 outerNode ->
@@ -187,7 +188,6 @@ public boolean moveTo(int key) {
         @Override
         public AbstractNextStateDescriptor.Cursor valueCursor(
                 int from, StateSpaceInfo localStateSpace) {
-            final MddNode constraint = localStateSpace.toStructuralRepresentation();
             // TODO the valueCursor call of the wrapped cursor has to propagate the constraint
             var fromCursor = wrapped.valueCursor();
             if (fromCursor.moveTo(from)) {

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

@@ -1,5 +1,5 @@
 /*
- *  Copyright 2025 Budapest University of Technology and Economics
+ *  Copyright 2025-2026 Budapest University of Technology and Economics
  *
  *  Licensed under the Apache License, Version 2.0 (the "License");
  *  you may not use this file except in compliance with the License.
@@ -16,18 +16,19 @@
 package hu.bme.mit.theta.analysis.algorithm.mdd.expressionnode;
 
 import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.*;
-import static hu.bme.mit.theta.core.type.booltype.BoolExprs.False;
-import static hu.bme.mit.theta.core.type.booltype.BoolExprs.True;
+import static hu.bme.mit.theta.core.type.booltype.BoolExprs.*;
 import static hu.bme.mit.theta.core.type.booltype.SmartBoolExprs.And;
 
 import com.google.common.base.Preconditions;
 import com.koloboke.collect.map.hash.HashIntObjMap;
 import com.koloboke.collect.map.hash.HashIntObjMaps;
 import hu.bme.mit.delta.collections.*;
 import hu.bme.mit.delta.java.mdd.MddGraph;
+import hu.bme.mit.delta.java.mdd.MddHandle;
 import hu.bme.mit.delta.java.mdd.MddNode;
 import hu.bme.mit.delta.java.mdd.MddVariable;
 import hu.bme.mit.theta.analysis.algorithm.mdd.identitynode.IdentityRepresentation;
+import hu.bme.mit.theta.analysis.algorithm.mdd.mddtoexpr.MddToExprUtilKt;
 import hu.bme.mit.theta.common.GrowingIntArray;
 import hu.bme.mit.theta.common.exception.NotSolvableException;
 import hu.bme.mit.theta.core.decl.Decl;
@@ -36,7 +37,6 @@
 import hu.bme.mit.theta.core.model.Valuation;
 import hu.bme.mit.theta.core.type.Expr;
 import hu.bme.mit.theta.core.type.LitExpr;
-import hu.bme.mit.theta.core.type.abstracttype.Ordered;
 import hu.bme.mit.theta.core.type.booltype.BoolType;
 import hu.bme.mit.theta.core.type.booltype.FalseExpr;
 import hu.bme.mit.theta.core.utils.ExprUtils;
@@ -58,6 +58,40 @@ public class MddExpressionRepresentation implements RecursiveIntObjMapView<MddNo
 
     private final SolverPool solverPool;
     private final boolean transExpr;
+    private static MddToExprStrategy mddToExprStrategy = MddToExprStrategy.VARIABLE_LEVEL;
+
+    public enum MddToExprStrategy {
+        NONE {
+            @Override
+            public Expr<BoolType> toExpr(MddHandle handle) {
+                return True();
+            }
+        },
+        NODE_LEVEL {
+            @Override
+            public Expr<BoolType> toExpr(MddHandle handle) {
+                return MddToExprUtilKt.toExprNodeLevel(handle);
+            }
+        },
+        VARIABLE_LEVEL {
+            @Override
+            public Expr<BoolType> toExpr(MddHandle handle) {
+                return MddToExprUtilKt.toApproximationExprVariableLevel(handle);
+            }
+        },
+        VECTOR_LEVEL {
+            @Override
+            public Expr<BoolType> toExpr(MddHandle handle) {
+                return MddToExprUtilKt.toExprVectorLevel(handle);
+            }
+        };
+
+        public abstract Expr<BoolType> toExpr(MddHandle handle);
+    }
+
+    public static void setMddToExprStrategy(MddToExprStrategy strategy) {
+        mddToExprStrategy = strategy;
+    }
 
     private MddExpressionRepresentation(
             final Expr<BoolType> expr,
@@ -200,54 +234,12 @@ public RecursiveIntObjCursor<? extends MddNode> cursor() {
 
     @Override
     public RecursiveIntObjCursor<? extends MddNode> cursor(RecursiveIntObjMapView<?> constraint) {
-        Preconditions.checkArgument(constraint instanceof MddNode);
-        final MddNode mddNodeConstraint = (MddNode) constraint;
-        final List<Expr<BoolType>> exprs = new ArrayList<>();
-
-        if (mddVariable.getLower().isPresent() && !mddNodeConstraint.isTerminal()) {
-            MddVariable variable = mddVariable.getLower().get();
-            MddNode mddNode =
-                    mddNodeConstraint.defaultValue() == null
-                            ? mddNodeConstraint.get(mddNodeConstraint.statistics().lowestValue())
-                            : mddNodeConstraint.defaultValue();
-            while (true) {
+        Preconditions.checkArgument(constraint instanceof MddHandle);
+        final MddHandle mddHandle = (MddHandle) constraint;
 
-                // This is needed because the constraint node might contain level-skips: if the
-                // domain is bounded, then default values are detected
-                if (mddNode.isTerminal()) break;
-
-                final IntStatistics statistics = mddNode.statistics();
-                final Decl<?> decl = variable.getTraceInfo(Decl.class);
-                final LitExpr<?> lowerBound =
-                        LitExprConverter.toLitExpr(statistics.lowestValue(), decl.getType());
-                final LitExpr<?> upperBound =
-                        LitExprConverter.toLitExpr(statistics.highestValue(), decl.getType());
-                if (decl.getType().getDomainSize().isInfinite()
-                        && decl.getType() instanceof Ordered) { // TODO delete
-                    if (lowerBound.equals(upperBound)) {
-                        exprs.add(Eq(decl.getRef(), lowerBound));
-                    } else {
-                        exprs.add(
-                                And(
-                                        Geq(decl.getRef(), lowerBound),
-                                        Leq(decl.getRef(), upperBound)));
-                    }
-                }
+        final var constraintExpr = mddToExprStrategy.toExpr(mddHandle);
 
-                if (variable.getLower().isEmpty()
-                        || variable.getLower().get().getLower().isEmpty()) {
-                    break;
-                } else {
-                    variable = variable.getLower().get().getLower().get();
-                    mddNode =
-                            mddNode.get(
-                                    statistics.lowestValue()); // TODO we assume here that all edges
-                    // point to the same node
-                }
-            }
-        }
-        //        System.out.println(exprs);
-        return new Cursor(null, Traverser.create(this, And(exprs), solverPool));
+        return new Cursor(null, Traverser.create(this, constraintExpr, solverPool));
     }
 
     @Override
@@ -315,9 +307,9 @@ public ExplicitRepresentation() {
         public void cacheNode(int key, MddNode node) {
             Preconditions.checkState(!complete);
             Preconditions.checkState(defaultValue == null);
-            if (this.cache.size() > 1000) {
-                throw new NotSolvableException();
-            }
+//            if (this.cache.size() > 1000) {
+//                throw new NotSolvableException();
+//            }
             this.cache.put(key, node);
             this.edgeOrdering.add(key);
         }
@@ -352,6 +344,7 @@ private static class Traverser implements Closeable {
 
         private MddExpressionRepresentation currentRepresentation;
         private final Expr<BoolType> constraint;
+        private boolean constraintApplied;
 
         private final SolverPool solverPool;
         private Solver solver;
@@ -366,6 +359,7 @@ private Traverser(
             this.stack = new Stack<>();
             this.constraint = constraint;
             this.currentRepresentation = rootRepresentation;
+            this.constraintApplied = false;
         }
 
         public static Traverser create(
@@ -406,7 +400,7 @@ else if (!currentRepresentation.explicitRepresentation.isComplete()) {
                                 assignment, currentRepresentation.decl.getType());
                 try (WithPushPop wpp = new WithPushPop(solver)) {
                     solver.add(currentRepresentation.expr);
-                    solver.add(constraint);
+                    //                    solver.add(constraint);
                     solver.add(Eq(currentRepresentation.decl.getRef(), litExpr));
                     solver.check();
                     status = solver.getStatus();
@@ -436,7 +430,10 @@ public QueryResult queryEdge() {
                 try (var wpp = new WithPushPop(solver)) {
 
                     solver.add(currentRepresentation.expr);
-                    solver.add(constraint);
+                    if (currentRepresentation.explicitRepresentation.getCacheView().size() >= 0) {
+                        solver.add(constraint);
+                        constraintApplied = true;
+                    }
                     final var negatedAssignments = new ArrayList<Expr<BoolType>>();
                     for (var cur =
                                     currentRepresentation
@@ -507,7 +504,7 @@ public QueryResult queryEdge() {
                     cacheModel(modelToCache);
                     return QueryResult.singleEdge(LitExprConverter.toInt(literal));
                 } else {
-                    if (!Objects.equals(constraint, True())) {
+                    if (constraintApplied && !Objects.equals(constraint, True())) {
                         return QueryResult.constrainedFailed();
                     } else {
                         currentRepresentation.explicitRepresentation.setComplete();