diff --git a/lib/hu.bme.mit.delta-0.0.1-all.jar b/lib/hu.bme.mit.delta-0.0.1-all.jar index b2de26a43e..96e8fd8bc0 100644 Binary files a/lib/hu.bme.mit.delta-0.0.1-all.jar and b/lib/hu.bme.mit.delta-0.0.1-all.jar differ diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddChecker.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddChecker.kt index 82f905abe2..2642e87bdf 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddChecker.kt +++ b/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> = monolithicExpr.orderVars(), + private val mddToExprStrategy: MddExpressionRepresentation.MddToExprStrategy = + MddExpressionRepresentation.MddToExprStrategy.VARIABLE_LEVEL, ) : SafetyChecker, UnitPrec> { enum class IterationStrategy { @@ -70,6 +73,8 @@ constructor( override fun check(prec: UnitPrec?): SafetyResult> { val totalTime = Stopwatch.createStarted() + MddExpressionRepresentation.setMddToExprStrategy(mddToExprStrategy) + val mddGraph = JavaMddFactory.getDefault().createMddGraph(ExprLatticeDefinition.forExpr()) val stateOrder = JavaMddFactory.getDefault().createMddVariableOrder(mddGraph) diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddSinglePathExtractor.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddSinglePathExtractor.kt index e175a12072..67102d2155 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddSinglePathExtractor.kt +++ b/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( diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddValuationCollector.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddValuationCollector.java index eda24b18bc..f02ff6d546 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddValuationCollector.java +++ b/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(); } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/ansd/StateSpaceInfo.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/ansd/StateSpaceInfo.java index 326e62ab41..2d0ca3fe3b 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/ansd/StateSpaceInfo.java +++ b/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 getTraceInfo(Class typeToken) { */ public StateSpaceInfo getLocalStateSpace(Object someLowerComponent); - public MddNode toStructuralRepresentation(); + public RecursiveIntObjMapView toStructuralRepresentation(); } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/ansd/impl/MddNodeNextStateDescriptor.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/ansd/impl/MddNodeNextStateDescriptor.java index 6599029c95..bb7686ebe1 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/ansd/impl/MddNodeNextStateDescriptor.java +++ b/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 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 getDiagonal(StateSpaceInfo loc @Override public IntObjMapView> 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)) { diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/expressionnode/MddExpressionRepresentation.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/expressionnode/MddExpressionRepresentation.java index e2db6cce55..2c2ec4a781 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/expressionnode/MddExpressionRepresentation.java +++ b/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,8 +16,7 @@ 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; @@ -25,9 +24,11 @@ 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 toExpr(MddHandle handle) { + return True(); + } + }, + NODE_LEVEL { + @Override + public Expr toExpr(MddHandle handle) { + return MddToExprUtilKt.toExprNodeLevel(handle); + } + }, + VARIABLE_LEVEL { + @Override + public Expr toExpr(MddHandle handle) { + return MddToExprUtilKt.toApproximationExprVariableLevel(handle); + } + }, + VECTOR_LEVEL { + @Override + public Expr toExpr(MddHandle handle) { + return MddToExprUtilKt.toExprVectorLevel(handle); + } + }; + + public abstract Expr toExpr(MddHandle handle); + } + + public static void setMddToExprStrategy(MddToExprStrategy strategy) { + mddToExprStrategy = strategy; + } private MddExpressionRepresentation( final Expr expr, @@ -200,54 +234,12 @@ public RecursiveIntObjCursor cursor() { @Override public RecursiveIntObjCursor cursor(RecursiveIntObjMapView constraint) { - Preconditions.checkArgument(constraint instanceof MddNode); - final MddNode mddNodeConstraint = (MddNode) constraint; - final List> 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 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>(); 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(); diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/fixedpoint/MddStateSpaceInfo.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/fixedpoint/MddStateSpaceInfo.java index 882d37dd42..ac93dfc278 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/fixedpoint/MddStateSpaceInfo.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/fixedpoint/MddStateSpaceInfo.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. @@ -15,36 +15,16 @@ */ package hu.bme.mit.theta.analysis.algorithm.mdd.fixedpoint; -import static hu.bme.mit.theta.core.type.booltype.BoolExprs.True; - -import com.google.common.base.Preconditions; -import com.koloboke.collect.map.ObjIntMap; -import com.koloboke.collect.map.hash.HashObjIntMaps; -import com.koloboke.collect.set.ObjSet; -import com.koloboke.collect.set.hash.HashObjSets; -import hu.bme.mit.delta.Pair; -import hu.bme.mit.delta.collections.IntObjMapView; import hu.bme.mit.delta.collections.IntSetView; -import hu.bme.mit.delta.collections.IntStatistics; -import hu.bme.mit.delta.collections.impl.IntObjMapViews; -import hu.bme.mit.delta.java.mdd.*; -import hu.bme.mit.delta.java.mdd.impl.MddStructuralTemplate; +import hu.bme.mit.delta.collections.RecursiveIntObjMapView; +import hu.bme.mit.delta.java.mdd.MddNode; +import hu.bme.mit.delta.java.mdd.MddVariable; import hu.bme.mit.theta.analysis.algorithm.mdd.ansd.StateSpaceInfo; -import hu.bme.mit.theta.common.container.Containers; -import hu.bme.mit.theta.core.type.Expr; -import hu.bme.mit.theta.core.type.booltype.BoolType; -import java.util.Objects; -import java.util.Optional; -import java.util.Set; public final class MddStateSpaceInfo implements StateSpaceInfo { private final MddVariable variable; private final MddNode mddNode; - private static BinaryOperationCache cache = - new BinaryOperationCache<>(); - private MddNode structuralRepresentation = null; - public MddStateSpaceInfo(final MddVariable variable, final MddNode mddNode) { this.variable = variable; this.mddNode = mddNode; @@ -110,116 +90,9 @@ public StateSpaceInfo getLocalStateSpace(final Object someLowerComponent) { } @Override - public MddNode toStructuralRepresentation() { - if (structuralRepresentation == null) { - var cached = cache.getOrNull(variable, mddNode); - if (cached != null) { - structuralRepresentation = cached; - return structuralRepresentation; - } - final BoundsCollector boundsCollector = new BoundsCollector(mddNode, variable); - structuralRepresentation = representBounds(variable, boundsCollector); - cache.addToCache(variable, mddNode, structuralRepresentation); - } - return structuralRepresentation; - } - - private MddNode representBounds(MddVariable variable, BoundsCollector boundsCollector) { - final MddNode continuation; - if (variable.getLower().isPresent()) { - continuation = representBounds(variable.getLower().get(), boundsCollector); - } else { - final MddGraph> mddGraph = - (MddGraph>) variable.getMddGraph(); - continuation = mddGraph.getNodeFor(True()); - } - final var bounds = boundsCollector.getBoundsFor(variable); - final IntObjMapView template; - if (bounds.isPresent()) { - if (Objects.equals(bounds.get().first, bounds.get().second)) { - template = IntObjMapView.singleton(bounds.get().first, continuation); - } else { - // TODO: canonization of trimmed intobjmapviews could be improved - template = - new IntObjMapViews.Trimmed<>( - IntObjMapView.empty(continuation), - IntSetView.range(bounds.get().first, bounds.get().second + 1)); - } - } else { - template = IntObjMapView.empty(continuation); - } - - return variable.checkInNode(MddStructuralTemplate.of(template)); - } - - // private MddNode collapseEdges(MddNode parent) { - // - // IntSetView setView = IntSetView.empty(); - // for (var c = parent.cursor(); c.moveNext(); ) { - // setView = setView.union(c.value().keySet()); - // } - // - // } - - private static class BoundsCollector { - - private final ObjIntMap lowerBounds; - private final ObjIntMap upperBounds; - private final ObjSet hasDefaultValue; - - public BoundsCollector(MddNode rootNode, MddVariable variable) { - Preconditions.checkNotNull(rootNode); - this.lowerBounds = HashObjIntMaps.newUpdatableMap(); - this.upperBounds = HashObjIntMaps.newUpdatableMap(); - this.hasDefaultValue = HashObjSets.newUpdatableSet(); - - final Set traversed = Containers.createSet(); - traverse(rootNode, variable, traversed); - } - - private void traverse( - final MddNode node, final MddVariable variable, final Set traversed) { - if (traversed.contains(node) || node.isTerminal()) { - return; - } else { - traversed.add(node); - } - Preconditions.checkNotNull(variable); - - for (var c = node.cursor(); c.moveNext(); ) {} // TODO delete later - - final var nodeInterpreter = variable.getNodeInterpreter(node); - if (nodeInterpreter.defaultValue() != null) { - final MddNode defaultValue = nodeInterpreter.defaultValue(); - traverse(defaultValue, variable.getLower().orElse(null), traversed); - hasDefaultValue.add(variable); - } else { - final IntStatistics statistics = nodeInterpreter.statistics(); - lowerBounds.put( - variable, - Math.min( - lowerBounds.getOrDefault(variable, Integer.MAX_VALUE), - statistics.lowestValue())); - upperBounds.put( - variable, - Math.max( - upperBounds.getOrDefault(variable, Integer.MIN_VALUE), - statistics.highestValue())); - - for (var cur = nodeInterpreter.cursor(); cur.moveNext(); ) { - if (cur.value() != null) { - traverse(cur.value(), variable.getLower().orElse(null), traversed); - } - } - } - } - - public Optional> getBoundsFor(MddVariable variable) { - if (hasDefaultValue.contains(variable)) return Optional.empty(); - if (!lowerBounds.containsKey(variable) || !upperBounds.containsKey(variable)) - return Optional.empty(); - return Optional.of( - new Pair<>(lowerBounds.getInt(variable), upperBounds.getInt(variable))); - } + public RecursiveIntObjMapView toStructuralRepresentation() { + var varHandle = variable.getDefaultSetSignatureHandle(); + var mddHandle = varHandle.getHandleFor(mddNode); + return mddHandle; } } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/mddtoexpr/MddToExpr.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/mddtoexpr/MddToExpr.java new file mode 100644 index 0000000000..a62bd9667f --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/mddtoexpr/MddToExpr.java @@ -0,0 +1,25 @@ +/* + * Copyright 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. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.analysis.algorithm.mdd.mddtoexpr; + +import hu.bme.mit.delta.java.mdd.MddHandle; +import hu.bme.mit.theta.core.type.Expr; +import hu.bme.mit.theta.core.type.booltype.BoolType; + +public interface MddToExpr { + + Expr toExpr(MddHandle node); +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/mddtoexpr/MddToExprNodeLevel.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/mddtoexpr/MddToExprNodeLevel.kt new file mode 100644 index 0000000000..d92b8d9775 --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/mddtoexpr/MddToExprNodeLevel.kt @@ -0,0 +1,141 @@ +/* + * 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. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.analysis.algorithm.mdd.mddtoexpr + +import hu.bme.mit.delta.java.mdd.BinaryOperationCache +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.expressionnode.LitExprConverter +import hu.bme.mit.theta.core.decl.Decl +import hu.bme.mit.theta.core.decl.Decls +import hu.bme.mit.theta.core.type.Expr +import hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Eq +import hu.bme.mit.theta.core.type.booltype.BoolExprs.True +import hu.bme.mit.theta.core.type.booltype.BoolType +import hu.bme.mit.theta.core.type.booltype.SmartBoolExprs.* + +object MddToExprNodeLevel : MddToExpr { + + val auxvarCache: BinaryOperationCache> = + BinaryOperationCache() + val constraintCache: BinaryOperationCache> = + BinaryOperationCache() + val expressionCache: BinaryOperationCache> = + BinaryOperationCache() + + override fun toExpr(root: MddHandle): Expr = + toExpr(root.node, root.variableHandle.variable.orElseThrow()) + + fun toExpr(root: MddNode, variable: MddVariable): Expr { + // Return cached expression if present + expressionCache.getOrNull(root, variable)?.let { + return it + } + + // Traverse the MDD and collect unique (node, variable) pairs + val visited = mutableSetOf>() + val stack = ArrayDeque>() + stack.add(Pair(root, variable)) + + while (stack.isNotEmpty()) { + val (node, varNode) = stack.removeLast() + val pair = Pair(node, varNode) + if (visited.contains(pair)) continue + visited.add(pair) + + // Ensure constraint (and auxiliary var) exists for this node-variable pair + getConstraintForNode(node, varNode) + + // If non-terminal, push children (including default) with the next variable + if (!node.isTerminal && varNode.lower.isPresent) { + val nextVar = varNode.lower.orElseThrow() + val defaultNode = node.defaultValue() + if (defaultNode != null) { + stack.add(Pair(defaultNode, nextVar)) + } else { + val cursor = node.cursor() + while (cursor.moveNext()) { + stack.add(Pair(cursor.value(), nextVar)) + } + } + } + } + val constraints = visited.map { (n, v) -> constraintCache.getOrNull(n, v)!! } + + val rootRepresentative = getRepresentativeForNode(root, variable) + val result: Expr = And(rootRepresentative, And(constraints)) + + expressionCache.addToCache(root, variable, result) + return result + } + + fun getRepresentativeForNode(node: MddNode, variable: MddVariable?): Expr { + if (node.isTerminal) return True() + else { + auxvarCache.getOrNull(node, variable)?.let { + return it.ref + } + + val varDecl = Decls.Var("mddnode_${auxvarCache.cacheSize}", BoolType.getInstance()) + val constDecl = varDecl.getConstDecl(0) + auxvarCache.addToCache(node, variable, constDecl) + return constDecl.ref + } + } + + fun getConstraintForNode(node: MddNode, variable: MddVariable): Expr { + // Return existing constraint if already created + constraintCache.getOrNull(node, variable)?.let { + return it + } + + val representative = getRepresentativeForNode(node, variable) + + val definition: Expr = + if (node.isTerminal) { + // Terminal definition + return representative + } else { + if (node.defaultValue() == null) { + val x = variable.getTraceInfo(Decl::class.java)!! + + val disjuncts = mutableListOf>() + + val cursor = node.cursor() + while (cursor.moveNext()) { + + val childRepresentative = + getRepresentativeForNode(cursor.value(), variable.lower.orElse(null)) + + val value = cursor.key() + disjuncts += + And(Eq(x.ref, LitExprConverter.toLitExpr(value, x.type)), childRepresentative) + } + + Eq(representative, Or(disjuncts)) + } else { + Eq( + representative, + getRepresentativeForNode(node.defaultValue(), variable.lower.orElseThrow()), + ) + } + } + + constraintCache.addToCache(node, variable, definition) + return definition + } +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/mddtoexpr/MddToExprUtil.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/mddtoexpr/MddToExprUtil.kt new file mode 100644 index 0000000000..602b34a4f2 --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/mddtoexpr/MddToExprUtil.kt @@ -0,0 +1,27 @@ +/* + * Copyright 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. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.analysis.algorithm.mdd.mddtoexpr + +import hu.bme.mit.delta.java.mdd.MddHandle +import hu.bme.mit.theta.core.type.Expr +import hu.bme.mit.theta.core.type.booltype.BoolType + +fun MddHandle.toExprNodeLevel(): Expr = MddToExprNodeLevel.toExpr(this) + +fun MddHandle.toExprVectorLevel(): Expr = MddToExprVectorLevel().toExpr(this) + +fun MddHandle.toApproximationExprVariableLevel(): Expr = + MddToExprVariableLevel().toExpr(this) diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/mddtoexpr/MddToExprVariableLevel.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/mddtoexpr/MddToExprVariableLevel.java new file mode 100644 index 0000000000..2d46c39906 --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/mddtoexpr/MddToExprVariableLevel.java @@ -0,0 +1,162 @@ +/* + * Copyright 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. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.analysis.algorithm.mdd.mddtoexpr; + +import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.*; +import static hu.bme.mit.theta.core.type.booltype.SmartBoolExprs.And; + +import com.google.common.base.Preconditions; +import com.koloboke.collect.map.ObjObjMap; +import com.koloboke.collect.map.hash.HashObjObjMaps; +import hu.bme.mit.delta.collections.IntStatistics; +import hu.bme.mit.delta.java.mdd.BinaryOperationCache; +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.expressionnode.LitExprConverter; +import hu.bme.mit.theta.core.decl.Decl; +import hu.bme.mit.theta.core.type.Expr; +import hu.bme.mit.theta.core.type.abstracttype.Ordered; +import hu.bme.mit.theta.core.type.booltype.BoolType; +import java.util.ArrayList; +import java.util.List; + +public class MddToExprVariableLevel implements MddToExpr { + + @Override + public Expr toExpr(MddHandle mddHandle) { + return getExpr( + mddHandle.getNode(), mddHandle.getVariableHandle().getVariable().orElseThrow()); + } + + public static Expr getExpr(MddNode mddNode, MddVariable variable) { + final var bounds = BoundsCollector.traverse(mddNode, variable); + final var exprs = new ArrayList>(); + for (var entry : bounds.entrySet()) { + final var decl = entry.getKey().getTraceInfo(Decl.class); + final var boundsForVar = entry.getValue(); + if (!boundsForVar.hasDefault + && decl.getType().getDomainSize().isInfinite() + && decl.getType() instanceof Ordered) { + if (boundsForVar.lower == boundsForVar.upper) { + exprs.add( + Eq( + decl.getRef(), + LitExprConverter.toLitExpr( + boundsForVar.lower, decl.getType()))); + } else { + exprs.add( + And( + Geq( + decl.getRef(), + LitExprConverter.toLitExpr( + boundsForVar.lower, decl.getType())), + Leq( + decl.getRef(), + LitExprConverter.toLitExpr( + boundsForVar.upper, decl.getType())))); + } + } + } + return And(exprs); + } + + private static class BoundsCollector { + + static class Bounds { + int lower; + int upper; + boolean hasDefault; + + Bounds(int lower, int upper, boolean hasDefault) { + this.lower = lower; + this.upper = upper; + this.hasDefault = hasDefault; + } + } + + private static BinaryOperationCache< + MddNode, MddVariable, ObjObjMap> + cache = new BinaryOperationCache<>(); + + public static ObjObjMap traverse( + final MddNode node, final MddVariable variable) { + final var cached = cache.getOrNull(node, variable); + if (cached != null) { + return cached; + } + if (node.isTerminal()) { + return HashObjObjMaps.newUpdatableMap(); + } + + Preconditions.checkNotNull(variable); + + for (var c = node.cursor(); c.moveNext(); ) {} // TODO delete later + + final ObjObjMap returnValue = + HashObjObjMaps.newUpdatableMap(); + final var currentBounds = + new BoundsCollector.Bounds(Integer.MAX_VALUE, Integer.MIN_VALUE, false); + + final List> childBounds = + new ArrayList<>(); + + final var nodeInterpreter = variable.getNodeInterpreter(node); + if (nodeInterpreter.defaultValue() != null) { + final MddNode defaultValue = nodeInterpreter.defaultValue(); + childBounds.add(traverse(defaultValue, variable.getLower().orElse(null))); + currentBounds.hasDefault = true; + } else { + final IntStatistics statistics = nodeInterpreter.statistics(); + currentBounds.lower = statistics.lowestValue(); + currentBounds.upper = statistics.highestValue(); + + for (var cur = nodeInterpreter.cursor(); cur.moveNext(); ) { + if (cur.value() != null) { + childBounds.add(traverse(cur.value(), variable.getLower().orElse(null))); + } + } + } + + returnValue.put(variable, currentBounds); + for (final var childBoundMap : childBounds) { + for (final var entry : childBoundMap.entrySet()) { + final MddVariable var = entry.getKey(); + final BoundsCollector.Bounds childBoundsForVar = entry.getValue(); + + final BoundsCollector.Bounds existingBounds = + returnValue.getOrDefault(var, null); + if (existingBounds == null) { + returnValue.put( + var, + new BoundsCollector.Bounds( + childBoundsForVar.lower, + childBoundsForVar.upper, + childBoundsForVar.hasDefault)); + } else { + existingBounds.lower = + Math.min(existingBounds.lower, childBoundsForVar.lower); + existingBounds.upper = + Math.max(existingBounds.upper, childBoundsForVar.upper); + existingBounds.hasDefault |= childBoundsForVar.hasDefault; + } + } + } + cache.addToCache(node, variable, returnValue); + return returnValue; + } + } +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/mddtoexpr/MddToExprVectorLevel.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/mddtoexpr/MddToExprVectorLevel.kt new file mode 100644 index 0000000000..4b7907fc40 --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/mddtoexpr/MddToExprVectorLevel.kt @@ -0,0 +1,28 @@ +/* + * Copyright 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. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.analysis.algorithm.mdd.mddtoexpr + +import hu.bme.mit.delta.java.mdd.MddHandle +import hu.bme.mit.theta.analysis.algorithm.mdd.MddValuationCollector +import hu.bme.mit.theta.core.type.Expr +import hu.bme.mit.theta.core.type.booltype.BoolType +import hu.bme.mit.theta.core.type.booltype.SmartBoolExprs.Or + +class MddToExprVectorLevel : MddToExpr { + + override fun toExpr(node: MddHandle): Expr = + Or(MddValuationCollector.collect(node).map { it.toExpr() }) +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/varordering/ForceVarOrdering.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/varordering/ForceVarOrdering.kt index 59bcf7d50b..1dbdc16f94 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/varordering/ForceVarOrdering.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/varordering/ForceVarOrdering.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. @@ -81,8 +81,8 @@ private fun eventSpans(vars: List, events: List>) = when (it.isEmpty()) { true -> 0 else -> { - val firstVar = it.filter { decl -> decl in vars }.minOf { vars.indexOf(it) } - val lastVar = it.filter { decl -> decl in vars }.maxOf { vars.indexOf(it) } + val firstVar = it.filter { decl -> decl in vars }.minOfOrNull { vars.indexOf(it) } ?: 0 + val lastVar = it.filter { decl -> decl in vars }.maxOfOrNull { vars.indexOf(it) } ?: 0 lastVar - firstVar } } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/MddHandleVisualizer.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/MddHandleVisualizer.java index 4f39b64b2d..d7badd0128 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/MddHandleVisualizer.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/MddHandleVisualizer.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. @@ -139,10 +139,10 @@ private void traverse(final Graph graph, final MddHandle node, final Set X = Decls.Var("x", IntType.getInstance()); - private static final VarDecl Y = Decls.Var("y", IntType.getInstance()); - - private static final VarDecl A = Decls.Var("a", BoolType.getInstance()); - private static final VarDecl B = Decls.Var("b", BoolType.getInstance()); - - private static final EnumType colorType = EnumType.of("color", List.of("red", "green", "blue")); - private static final VarDecl C = Decls.Var("c", colorType); - private static final LitExpr RED = colorType.litFromShortName("red"); - private static final LitExpr GREEN = colorType.litFromShortName("green"); - private static final LitExpr BLUE = colorType.litFromShortName("blue"); - - @Parameterized.Parameter(value = 0) - public List> varOrder; - - @Parameterized.Parameter(value = 1) - public Expr constraintExpr; - - @Parameterized.Parameter(value = 2) - public Expr transExpr; - - @Parameterized.Parameter(value = 3) - public Integer topLevelCursorExpectedSize; - - @Parameterized.Parameters(name = "{index}: {0}, {1}, {2}, {3}") - public static Collection data() { - return Arrays.asList( - new Object[][] { - { - List.of(X, Y), - BoolExprs.And( - Eq(X.getRef(), Int(0)), Eq(Y.getRef(), Int(0))), // x = 0, y = 0 - BoolExprs.And( - Eq(Prime(X.getRef()), X.getRef()), - Eq(Prime(Y.getRef()), Y.getRef())), // x'=x, y'=y - 1 - }, - { - List.of(X, Y), - BoolExprs.And( - Eq(X.getRef(), Int(0)), Eq(Y.getRef(), Int(0))), // x = 0, y = 0 - BoolExprs.And( - Eq(Prime(X.getRef()), Add(X.getRef(), Int(1))), - Eq(Prime(Y.getRef()), Y.getRef())), // x'=x + 1, y'=y - 1 - }, - { - List.of(X, Y), - Or( - BoolExprs.And(Eq(X.getRef(), Int(0)), Eq(Y.getRef(), Int(0))), - BoolExprs.And( - Eq(X.getRef(), Int(1)), - Eq(Y.getRef(), Int(1)))), // x = 0, y = 0 or x = 1, y = 1 - BoolExprs.And( - Eq(Prime(X.getRef()), X.getRef()), - Eq(Prime(Y.getRef()), Y.getRef())), // x'=x, y'=y - 2 - }, - { - List.of(X, Y), - BoolExprs.And( - Eq(X.getRef(), Int(0)), Eq(Y.getRef(), Int(0))), // x = 0, y = 0 - BoolExprs.And( - Eq(Prime(X.getRef()), Y.getRef()), - Eq(Prime(Y.getRef()), Y.getRef())), // x'=y, y'=y - 1 - }, - { - List.of(X, Y), - BoolExprs.And( - Eq(X.getRef(), Int(0)), Eq(Y.getRef(), Int(0))), // x = 0, y = 0 - BoolExprs.And( - Eq(Prime(X.getRef()), Add(Y.getRef(), Int(1))), - Eq(Prime(Y.getRef()), Y.getRef())), // x'=y + 1, y'=y - 1 - }, - }); - } - - @Test - public void test() throws Exception { - - try (final SolverPool solverPool = new SolverPool(Z3LegacySolverFactory.getInstance())) { - final MddGraph mddGraph = - JavaMddFactory.getDefault().createMddGraph(ExprLatticeDefinition.forExpr()); - - final MddVariableOrder stateOrder = - JavaMddFactory.getDefault().createMddVariableOrder(mddGraph); - final MddVariableOrder transOrder = - JavaMddFactory.getDefault().createMddVariableOrder(mddGraph); - - varOrder.forEach( - v -> { - final var domainSize = - Math.max(v.getType().getDomainSize().getFiniteSize().intValue(), 0); - stateOrder.createOnTop( - MddVariableDescriptor.create(v.getConstDecl(0), domainSize)); - transOrder.createOnTop( - MddVariableDescriptor.create(v.getConstDecl(1), domainSize)); - transOrder.createOnTop( - MddVariableDescriptor.create(v.getConstDecl(0), domainSize)); - }); - - final var stateSig = stateOrder.getDefaultSetSignature(); - final var transSig = transOrder.getDefaultSetSignature(); - - final var constraintUnfolded = PathUtils.unfold(constraintExpr, 0); - final var transUnfolded = PathUtils.unfold(transExpr, 0); - - final MddHandle constraintHandle = - stateSig.getTopVariableHandle() - .checkInNode( - MddExpressionTemplate.of( - constraintUnfolded, o -> (Decl) o, solverPool)); - final MddHandle transHandle = - transSig.getTopVariableHandle() - .checkInNode( - MddExpressionTemplate.of( - transUnfolded, o -> (Decl) o, solverPool)); - - final var stateSpaceInfo = - new MddStateSpaceInfo( - stateSig.getTopVariableHandle().getVariable().orElseThrow(), - constraintHandle.getNode()); - final var structuralRepresentation = stateSpaceInfo.toStructuralRepresentation(); - // final var structuralHandle = - // stateSig.getTopVariableHandle().getHandleFor(structuralRepresentation); - - Integer size = 0; - for (var cursor = transHandle.cursor(structuralRepresentation); cursor.moveNext(); ) { - size++; - } - - assertEquals(topLevelCursorExpectedSize, size); - } - } -} diff --git a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddConstrainedCursorTest.java.bak b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddConstrainedCursorTest.java.bak new file mode 100644 index 0000000000..ef2aea4034 --- /dev/null +++ b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddConstrainedCursorTest.java.bak @@ -0,0 +1,191 @@ +///* +// * Copyright 2025 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. +// * You may obtain a copy of the License at +// * +// * http://www.apache.org/licenses/LICENSE-2.0 +// * +// * Unless required by applicable law or agreed to in writing, software +// * distributed under the License is distributed on an "AS IS" BASIS, +// * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// * See the License for the specific language governing permissions and +// * limitations under the License. +// */ +//package hu.bme.mit.theta.analysis.algorithm.mdd; +// +//import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Add; +//import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Eq; +//import static hu.bme.mit.theta.core.type.anytype.Exprs.Prime; +//import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Or; +//import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int; +//import static org.junit.Assert.assertEquals; +// +//import hu.bme.mit.delta.java.mdd.JavaMddFactory; +//import hu.bme.mit.delta.java.mdd.MddGraph; +//import hu.bme.mit.delta.java.mdd.MddHandle; +//import hu.bme.mit.delta.java.mdd.MddVariableOrder; +//import hu.bme.mit.delta.mdd.MddVariableDescriptor; +//import hu.bme.mit.theta.analysis.algorithm.mdd.expressionnode.ExprLatticeDefinition; +//import hu.bme.mit.theta.analysis.algorithm.mdd.expressionnode.MddExpressionTemplate; +//import hu.bme.mit.theta.analysis.algorithm.mdd.fixedpoint.MddStateSpaceInfo; +//import hu.bme.mit.theta.core.decl.Decl; +//import hu.bme.mit.theta.core.decl.Decls; +//import hu.bme.mit.theta.core.decl.VarDecl; +//import hu.bme.mit.theta.core.type.Expr; +//import hu.bme.mit.theta.core.type.LitExpr; +//import hu.bme.mit.theta.core.type.booltype.BoolExprs; +//import hu.bme.mit.theta.core.type.booltype.BoolType; +//import hu.bme.mit.theta.core.type.enumtype.EnumType; +//import hu.bme.mit.theta.core.type.inttype.IntType; +//import hu.bme.mit.theta.core.utils.PathUtils; +//import hu.bme.mit.theta.solver.SolverPool; +//import hu.bme.mit.theta.solver.z3legacy.Z3LegacySolverFactory; +//import java.util.Arrays; +//import java.util.Collection; +//import java.util.List; +//import org.junit.Test; +//import org.junit.runner.RunWith; +//import org.junit.runners.Parameterized; +// +//@RunWith(value = Parameterized.class) +//public class MddConstrainedCursorTest { +// +// private static final VarDecl X = Decls.Var("x", IntType.getInstance()); +// private static final VarDecl Y = Decls.Var("y", IntType.getInstance()); +// +// private static final VarDecl A = Decls.Var("a", BoolType.getInstance()); +// private static final VarDecl B = Decls.Var("b", BoolType.getInstance()); +// +// private static final EnumType colorType = EnumType.of("color", List.of("red", "green", "blue")); +// private static final VarDecl C = Decls.Var("c", colorType); +// private static final LitExpr RED = colorType.litFromShortName("red"); +// private static final LitExpr GREEN = colorType.litFromShortName("green"); +// private static final LitExpr BLUE = colorType.litFromShortName("blue"); +// +// @Parameterized.Parameter(value = 0) +// public List> varOrder; +// +// @Parameterized.Parameter(value = 1) +// public Expr constraintExpr; +// +// @Parameterized.Parameter(value = 2) +// public Expr transExpr; +// +// @Parameterized.Parameter(value = 3) +// public Integer topLevelCursorExpectedSize; +// +// @Parameterized.Parameters(name = "{index}: {0}, {1}, {2}, {3}") +// public static Collection data() { +// return Arrays.asList( +// new Object[][] { +// { +// List.of(X, Y), +// BoolExprs.And( +// Eq(X.getRef(), Int(0)), Eq(Y.getRef(), Int(0))), // x = 0, y = 0 +// BoolExprs.And( +// Eq(Prime(X.getRef()), X.getRef()), +// Eq(Prime(Y.getRef()), Y.getRef())), // x'=x, y'=y +// 1 +// }, +// { +// List.of(X, Y), +// BoolExprs.And( +// Eq(X.getRef(), Int(0)), Eq(Y.getRef(), Int(0))), // x = 0, y = 0 +// BoolExprs.And( +// Eq(Prime(X.getRef()), Add(X.getRef(), Int(1))), +// Eq(Prime(Y.getRef()), Y.getRef())), // x'=x + 1, y'=y +// 1 +// }, +// { +// List.of(X, Y), +// Or( +// BoolExprs.And(Eq(X.getRef(), Int(0)), Eq(Y.getRef(), Int(0))), +// BoolExprs.And( +// Eq(X.getRef(), Int(1)), +// Eq(Y.getRef(), Int(1)))), // x = 0, y = 0 or x = 1, y = 1 +// BoolExprs.And( +// Eq(Prime(X.getRef()), X.getRef()), +// Eq(Prime(Y.getRef()), Y.getRef())), // x'=x, y'=y +// 2 +// }, +// { +// List.of(X, Y), +// BoolExprs.And( +// Eq(X.getRef(), Int(0)), Eq(Y.getRef(), Int(0))), // x = 0, y = 0 +// BoolExprs.And( +// Eq(Prime(X.getRef()), Y.getRef()), +// Eq(Prime(Y.getRef()), Y.getRef())), // x'=y, y'=y +// 1 +// }, +// { +// List.of(X, Y), +// BoolExprs.And( +// Eq(X.getRef(), Int(0)), Eq(Y.getRef(), Int(0))), // x = 0, y = 0 +// BoolExprs.And( +// Eq(Prime(X.getRef()), Add(Y.getRef(), Int(1))), +// Eq(Prime(Y.getRef()), Y.getRef())), // x'=y + 1, y'=y +// 1 +// }, +// }); +// } +// +// @Test +// public void test() throws Exception { +// +// try (final SolverPool solverPool = new SolverPool(Z3LegacySolverFactory.getInstance())) { +// final MddGraph mddGraph = +// JavaMddFactory.getDefault().createMddGraph(ExprLatticeDefinition.forExpr()); +// +// final MddVariableOrder stateOrder = +// JavaMddFactory.getDefault().createMddVariableOrder(mddGraph); +// final MddVariableOrder transOrder = +// JavaMddFactory.getDefault().createMddVariableOrder(mddGraph); +// +// varOrder.forEach( +// v -> { +// final var domainSize = +// Math.max(v.getType().getDomainSize().getFiniteSize().intValue(), 0); +// stateOrder.createOnTop( +// MddVariableDescriptor.create(v.getConstDecl(0), domainSize)); +// transOrder.createOnTop( +// MddVariableDescriptor.create(v.getConstDecl(1), domainSize)); +// transOrder.createOnTop( +// MddVariableDescriptor.create(v.getConstDecl(0), domainSize)); +// }); +// +// final var stateSig = stateOrder.getDefaultSetSignature(); +// final var transSig = transOrder.getDefaultSetSignature(); +// +// final var constraintUnfolded = PathUtils.unfold(constraintExpr, 0); +// final var transUnfolded = PathUtils.unfold(transExpr, 0); +// +// final MddHandle constraintHandle = +// stateSig.getTopVariableHandle() +// .checkInNode( +// MddExpressionTemplate.of( +// constraintUnfolded, o -> (Decl) o, solverPool)); +// final MddHandle transHandle = +// transSig.getTopVariableHandle() +// .checkInNode( +// MddExpressionTemplate.of( +// transUnfolded, o -> (Decl) o, solverPool)); +// +// final var stateSpaceInfo = +// new MddStateSpaceInfo( +// stateSig.getTopVariableHandle().getVariable().orElseThrow(), +// constraintHandle.getNode()); +// final var structuralRepresentation = stateSpaceInfo.toStructuralRepresentation(); +// // final var structuralHandle = +// // stateSig.getTopVariableHandle().getHandleFor(structuralRepresentation); +// +// Integer size = 0; +// for (var cursor = transHandle.cursor(structuralRepresentation); cursor.moveNext(); ) { +// size++; +// } +// +// assertEquals(topLevelCursorExpectedSize, size); +// } +// } +//} diff --git a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddStateSpaceInfoTest.java b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddStateSpaceInfoTest.java deleted file mode 100644 index 692847f652..0000000000 --- a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddStateSpaceInfoTest.java +++ /dev/null @@ -1,166 +0,0 @@ -/* - * Copyright 2025 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. - * You may obtain a copy of the License at - * - * http://www.apache.org/licenses/LICENSE-2.0 - * - * Unless required by applicable law or agreed to in writing, software - * distributed under the License is distributed on an "AS IS" BASIS, - * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. - * See the License for the specific language governing permissions and - * limitations under the License. - */ -package hu.bme.mit.theta.analysis.algorithm.mdd; - -import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Eq; -import static hu.bme.mit.theta.core.type.booltype.BoolExprs.*; -import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int; -import static org.junit.Assert.assertEquals; - -import hu.bme.mit.delta.java.mdd.JavaMddFactory; -import hu.bme.mit.delta.java.mdd.MddGraph; -import hu.bme.mit.delta.java.mdd.MddHandle; -import hu.bme.mit.delta.java.mdd.MddVariableOrder; -import hu.bme.mit.delta.mdd.MddInterpreter; -import hu.bme.mit.delta.mdd.MddVariableDescriptor; -import hu.bme.mit.theta.analysis.algorithm.mdd.expressionnode.ExprLatticeDefinition; -import hu.bme.mit.theta.analysis.algorithm.mdd.expressionnode.MddExpressionTemplate; -import hu.bme.mit.theta.analysis.algorithm.mdd.fixedpoint.MddStateSpaceInfo; -import hu.bme.mit.theta.core.decl.Decl; -import hu.bme.mit.theta.core.decl.Decls; -import hu.bme.mit.theta.core.decl.VarDecl; -import hu.bme.mit.theta.core.type.Expr; -import hu.bme.mit.theta.core.type.LitExpr; -import hu.bme.mit.theta.core.type.booltype.BoolType; -import hu.bme.mit.theta.core.type.enumtype.EnumType; -import hu.bme.mit.theta.core.type.inttype.IntType; -import hu.bme.mit.theta.core.utils.PathUtils; -import hu.bme.mit.theta.solver.SolverPool; -import hu.bme.mit.theta.solver.z3legacy.Z3LegacySolverFactory; -import java.util.Arrays; -import java.util.Collection; -import java.util.List; -import org.junit.Test; -import org.junit.runner.RunWith; -import org.junit.runners.Parameterized; - -@RunWith(value = Parameterized.class) -public class MddStateSpaceInfoTest { - - private static final VarDecl X = Decls.Var("x", IntType.getInstance()); - private static final VarDecl Y = Decls.Var("y", IntType.getInstance()); - - private static final VarDecl A = Decls.Var("a", BoolType.getInstance()); - private static final VarDecl B = Decls.Var("b", BoolType.getInstance()); - - private static final EnumType colorType = EnumType.of("color", List.of("red", "green", "blue")); - private static final VarDecl C = Decls.Var("c", colorType); - private static final LitExpr RED = colorType.litFromShortName("red"); - private static final LitExpr GREEN = colorType.litFromShortName("green"); - private static final LitExpr BLUE = colorType.litFromShortName("blue"); - - @Parameterized.Parameter(value = 0) - public List> varOrder; - - @Parameterized.Parameter(value = 1) - public Expr stateSpaceExpr; - - @Parameterized.Parameter(value = 2) - public Long expectedSize; - - @Parameterized.Parameters(name = "{index}: {0}, {1}, {2}") - public static Collection data() { - return Arrays.asList( - new Object[][] { - { - List.of(X, Y), - And(Eq(X.getRef(), Int(0)), Eq(Y.getRef(), Int(0))), // x = 0, y = 0 - 1L - }, - { - List.of(A, B), - Eq(A.getRef(), False()), // a = 0 - 2L - }, - { - List.of(A, B), - Eq(B.getRef(), False()), // y = 0 - 2L - }, - { - List.of(A, B), - True(), // true - 4L - }, - { - List.of(X, Y), - Or( - And(Eq(X.getRef(), Int(0)), Eq(Y.getRef(), Int(0))), - And( - Eq(X.getRef(), Int(1)), - Eq(Y.getRef(), Int(1)))), // x = 0, y = 0 or x = 1, y = 1 - 4L - }, - { - List.of(X, Y), - Or( - And(Eq(X.getRef(), Int(0)), Eq(Y.getRef(), Int(0))), - And(Eq(X.getRef(), Int(1)), Eq(Y.getRef(), Int(1))), - And( - Eq(X.getRef(), Int(2)), - Eq( - Y.getRef(), - Int(2)))), // x = 0, y = 0 or x = 1, y = 1 or x - // = 2, y = 3 - 9L - }, - {List.of(A, C), And(A.getRef(), Eq(C.getRef(), RED)), 1L}, - {List.of(A, C), A.getRef(), 3L}, - {List.of(A, C), True(), 6L}, - {List.of(C, A), True(), 6L}, - }); - } - - @Test - public void test() throws Exception { - - try (final SolverPool solverPool = new SolverPool(Z3LegacySolverFactory.getInstance())) { - final MddGraph mddGraph = - JavaMddFactory.getDefault().createMddGraph(ExprLatticeDefinition.forExpr()); - - final MddVariableOrder variableOrder = - JavaMddFactory.getDefault().createMddVariableOrder(mddGraph); - varOrder.forEach( - v -> { - final var domainSize = - Math.max(v.getType().getDomainSize().getFiniteSize().intValue(), 0); - variableOrder.createOnTop( - MddVariableDescriptor.create(v.getConstDecl(0), domainSize)); - }); - final var signature = variableOrder.getDefaultSetSignature(); - - final var stateUnfolded = PathUtils.unfold(stateSpaceExpr, 0); - final MddHandle stateHandle = - signature - .getTopVariableHandle() - .checkInNode( - MddExpressionTemplate.of( - stateUnfolded, o -> (Decl) o, solverPool)); - - final var stateSpaceInfo = - new MddStateSpaceInfo( - signature.getTopVariableHandle().getVariable().orElseThrow(), - stateHandle.getNode()); - final var structuralRepresentation = stateSpaceInfo.toStructuralRepresentation(); - final var structuralHandle = - signature.getTopVariableHandle().getHandleFor(structuralRepresentation); - - final Long resultSize = MddInterpreter.calculateNonzeroCount(structuralHandle); - - assertEquals(expectedSize, resultSize); - } - } -} diff --git a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddStateSpaceInfoTest.java.bak b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddStateSpaceInfoTest.java.bak new file mode 100644 index 0000000000..01b5c1682e --- /dev/null +++ b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddStateSpaceInfoTest.java.bak @@ -0,0 +1,192 @@ +///* +// * 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. +// * You may obtain a copy of the License at +// * +// * http://www.apache.org/licenses/LICENSE-2.0 +// * +// * Unless required by applicable law or agreed to in writing, software +// * distributed under the License is distributed on an "AS IS" BASIS, +// * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// * See the License for the specific language governing permissions and +// * limitations under the License. +// */ +//package hu.bme.mit.theta.analysis.algorithm.mdd; +// +//import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Eq; +//import static hu.bme.mit.theta.core.type.booltype.BoolExprs.*; +//import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int; +//import static org.junit.Assert.assertEquals; +// +//import hu.bme.mit.delta.collections.IntObjMapView; +//import hu.bme.mit.delta.collections.IntStatistics; +//import hu.bme.mit.delta.collections.RecursiveIntObjMapView; +//import hu.bme.mit.delta.java.mdd.JavaMddFactory; +//import hu.bme.mit.delta.java.mdd.MddGraph; +//import hu.bme.mit.delta.java.mdd.MddHandle; +//import hu.bme.mit.delta.java.mdd.MddVariableOrder; +//import hu.bme.mit.delta.mdd.MddVariableDescriptor; +//import hu.bme.mit.theta.analysis.algorithm.mdd.expressionnode.ExprLatticeDefinition; +//import hu.bme.mit.theta.analysis.algorithm.mdd.expressionnode.MddExpressionTemplate; +//import hu.bme.mit.theta.analysis.algorithm.mdd.fixedpoint.MddStateSpaceInfo; +//import hu.bme.mit.theta.core.decl.Decl; +//import hu.bme.mit.theta.core.decl.Decls; +//import hu.bme.mit.theta.core.decl.VarDecl; +//import hu.bme.mit.theta.core.type.Expr; +//import hu.bme.mit.theta.core.type.LitExpr; +//import hu.bme.mit.theta.core.type.booltype.BoolType; +//import hu.bme.mit.theta.core.type.enumtype.EnumType; +//import hu.bme.mit.theta.core.type.inttype.IntType; +//import hu.bme.mit.theta.core.utils.PathUtils; +//import hu.bme.mit.theta.solver.SolverPool; +//import hu.bme.mit.theta.solver.z3legacy.Z3LegacySolverFactory; +//import java.util.Arrays; +//import java.util.Collection; +//import java.util.List; +//import org.junit.Test; +//import org.junit.runner.RunWith; +//import org.junit.runners.Parameterized; +// +//@RunWith(value = Parameterized.class) +//public class MddStateSpaceInfoTest { +// +// private static final VarDecl X = Decls.Var("x", IntType.getInstance()); +// private static final VarDecl Y = Decls.Var("y", IntType.getInstance()); +// +// private static final VarDecl A = Decls.Var("a", BoolType.getInstance()); +// private static final VarDecl B = Decls.Var("b", BoolType.getInstance()); +// +// private static final EnumType colorType = EnumType.of("color", List.of("red", "green", "blue")); +// private static final VarDecl C = Decls.Var("c", colorType); +// private static final LitExpr RED = colorType.litFromShortName("red"); +// private static final LitExpr GREEN = colorType.litFromShortName("green"); +// private static final LitExpr BLUE = colorType.litFromShortName("blue"); +// +// @Parameterized.Parameter(value = 0) +// public List> varOrder; +// +// @Parameterized.Parameter(value = 1) +// public Expr stateSpaceExpr; +// +// @Parameterized.Parameter(value = 2) +// public Long expectedSize; +// +// @Parameterized.Parameters(name = "{index}: {0}, {1}, {2}") +// public static Collection data() { +// return Arrays.asList( +// new Object[][] { +// { +// List.of(X, Y), +// And(Eq(X.getRef(), Int(0)), Eq(Y.getRef(), Int(0))), // x = 0, y = 0 +// 1L +// }, +// { +// List.of(A, B), +// Eq(A.getRef(), False()), // a = 0 +// 2L +// }, +// { +// List.of(A, B), +// Eq(B.getRef(), False()), // y = 0 +// 2L +// }, +// { +// List.of(A, B), +// True(), // true +// 4L +// }, +// { +// List.of(X, Y), +// Or( +// And(Eq(X.getRef(), Int(0)), Eq(Y.getRef(), Int(0))), +// And( +// Eq(X.getRef(), Int(1)), +// Eq(Y.getRef(), Int(1)))), // x = 0, y = 0 or x = 1, y = 1 +// 4L +// }, +// { +// List.of(X, Y), +// Or( +// And(Eq(X.getRef(), Int(0)), Eq(Y.getRef(), Int(0))), +// And(Eq(X.getRef(), Int(1)), Eq(Y.getRef(), Int(1))), +// And( +// Eq(X.getRef(), Int(2)), +// Eq( +// Y.getRef(), +// Int(2)))), // x = 0, y = 0 or x = 1, y = 1 or x +// // = 2, y = 3 +// 9L +// }, +// {List.of(A, C), And(A.getRef(), Eq(C.getRef(), RED)), 1L}, +// {List.of(A, C), A.getRef(), 3L}, +// {List.of(A, C), True(), 6L}, +// {List.of(C, A), True(), 6L}, +// }); +// } +// +// @Test +// public void test() throws Exception { +// +// try (final SolverPool solverPool = new SolverPool(Z3LegacySolverFactory.getInstance())) { +// final MddGraph mddGraph = +// JavaMddFactory.getDefault().createMddGraph(ExprLatticeDefinition.forExpr()); +// +// final MddVariableOrder variableOrder = +// JavaMddFactory.getDefault().createMddVariableOrder(mddGraph); +// varOrder.forEach( +// v -> { +// final var domainSize = +// Math.max(v.getType().getDomainSize().getFiniteSize().intValue(), 0); +// variableOrder.createOnTop( +// MddVariableDescriptor.create(v.getConstDecl(0), domainSize)); +// }); +// final var signature = variableOrder.getDefaultSetSignature(); +// +// final var stateUnfolded = PathUtils.unfold(stateSpaceExpr, 0); +// final MddHandle stateHandle = +// signature +// .getTopVariableHandle() +// .checkInNode( +// MddExpressionTemplate.of( +// stateUnfolded, o -> (Decl) o, solverPool)); +// +// final var stateSpaceInfo = +// new MddStateSpaceInfo( +// signature.getTopVariableHandle().getVariable().orElseThrow(), +// stateHandle.getNode()); +// final var structuralRepresentation = stateSpaceInfo.toStructuralRepresentation(); +// +// final Long resultSize = calculateSize(structuralRepresentation); +// +// assertEquals(expectedSize, resultSize); +// } +// } +// +// private static Long calculateSize(RecursiveIntObjMapView mapView) { +// if (mapView.equals(IntObjMapView.empty())) { +// return 1L; +// } else { +// mapView.defaultValue(); +// if (mapView.defaultValue() != null) { +// return null; +// } else { +// Long ret = 0L; +// IntStatistics statistics = mapView.statistics(); +// int lowestValue = statistics.lowestValue(); +// int highestValue = statistics.highestValue(); +// +// for (int i = lowestValue; i < highestValue + 1; ++i) { +// Long res = calculateSize((RecursiveIntObjMapView) mapView.get(i)); +// if (res == null) { +// return null; +// } +// +// ret += res; +// } +// return ret; +// } +// } +// } +//} diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/ExprSimplifier.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/ExprSimplifier.java index 41ce2504d0..d14784b234 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/ExprSimplifier.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/ExprSimplifier.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. @@ -261,6 +261,12 @@ private Expr simplifyGenericIte( final Expr then = simplify(expr.getThen(), val); final Expr elze = simplify(expr.getElse(), val); + if (then instanceof TrueExpr && elze instanceof FalseExpr) { + return (Expr) cond; + } else if (then instanceof FalseExpr && elze instanceof TrueExpr) { + return (Expr) Not(cond); + } + return expr.with(cond, then, elze); } diff --git a/subprojects/frontends/petrinet-xsts/src/test/java/hu.bme.mit.theta.frontend.petrinet.xsts/PnmlSymbolicGSATTest.java b/subprojects/frontends/petrinet-xsts/src/test/java/hu.bme.mit.theta.frontend.petrinet.xsts/PnmlSymbolicGSATTest.java index 602bfcff39..6982e34001 100644 --- a/subprojects/frontends/petrinet-xsts/src/test/java/hu.bme.mit.theta.frontend.petrinet.xsts/PnmlSymbolicGSATTest.java +++ b/subprojects/frontends/petrinet-xsts/src/test/java/hu.bme.mit.theta.frontend.petrinet.xsts/PnmlSymbolicGSATTest.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. diff --git a/subprojects/solver/solver-z3-legacy/src/main/java/hu/bme/mit/theta/solver/z3legacy/Z3LegacySolverFactory.java b/subprojects/solver/solver-z3-legacy/src/main/java/hu/bme/mit/theta/solver/z3legacy/Z3LegacySolverFactory.java index 091e79615e..b9947cb84e 100644 --- a/subprojects/solver/solver-z3-legacy/src/main/java/hu/bme/mit/theta/solver/z3legacy/Z3LegacySolverFactory.java +++ b/subprojects/solver/solver-z3-legacy/src/main/java/hu/bme/mit/theta/solver/z3legacy/Z3LegacySolverFactory.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. @@ -57,9 +57,11 @@ public Solver createSolver() { final com.microsoft.z3legacy.Solver z3Solver = z3Context.mkSimpleSolver(); final Z3SymbolTable symbolTable = new Z3SymbolTable(); + final Z3TypeSymbolTable typeSymbolTable = new Z3TypeSymbolTable(); final Z3TransformationManager transformationManager = - new Z3TransformationManager(symbolTable, z3Context); - final Z3TermTransformer termTransformer = new Z3TermTransformer(symbolTable); + new Z3TransformationManager(symbolTable, typeSymbolTable, z3Context); + final Z3TermTransformer termTransformer = + new Z3TermTransformer(symbolTable, typeSymbolTable); return new Z3Solver( symbolTable, transformationManager, termTransformer, z3Context, z3Solver); @@ -71,9 +73,11 @@ public UCSolver createUCSolver() { final com.microsoft.z3legacy.Solver z3Solver = z3Context.mkSimpleSolver(); final Z3SymbolTable symbolTable = new Z3SymbolTable(); + final Z3TypeSymbolTable typeSymbolTable = new Z3TypeSymbolTable(); final Z3TransformationManager transformationManager = - new Z3TransformationManager(symbolTable, z3Context); - final Z3TermTransformer termTransformer = new Z3TermTransformer(symbolTable); + new Z3TransformationManager(symbolTable, typeSymbolTable, z3Context); + final Z3TermTransformer termTransformer = + new Z3TermTransformer(symbolTable, typeSymbolTable); return new Z3Solver( symbolTable, transformationManager, termTransformer, z3Context, z3Solver); @@ -85,9 +89,11 @@ public ItpSolver createItpSolver() { final com.microsoft.z3legacy.Solver z3Solver = z3Context.mkSimpleSolver(); final Z3SymbolTable symbolTable = new Z3SymbolTable(); + final Z3TypeSymbolTable typeSymbolTable = new Z3TypeSymbolTable(); final Z3TransformationManager transformationManager = - new Z3TransformationManager(symbolTable, z3Context); - final Z3TermTransformer termTransformer = new Z3TermTransformer(symbolTable); + new Z3TransformationManager(symbolTable, typeSymbolTable, z3Context); + final Z3TermTransformer termTransformer = + new Z3TermTransformer(symbolTable, typeSymbolTable); return new Z3ItpSolver( symbolTable, transformationManager, termTransformer, z3Context, z3Solver); diff --git a/subprojects/solver/solver-z3-legacy/src/main/java/hu/bme/mit/theta/solver/z3legacy/Z3TermTransformer.java b/subprojects/solver/solver-z3-legacy/src/main/java/hu/bme/mit/theta/solver/z3legacy/Z3TermTransformer.java index 3a2eb54f0c..cec6422883 100644 --- a/subprojects/solver/solver-z3-legacy/src/main/java/hu/bme/mit/theta/solver/z3legacy/Z3TermTransformer.java +++ b/subprojects/solver/solver-z3-legacy/src/main/java/hu/bme/mit/theta/solver/z3legacy/Z3TermTransformer.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. @@ -32,7 +32,6 @@ import com.google.common.collect.ImmutableList; import com.microsoft.z3legacy.*; import com.microsoft.z3legacy.enumerations.Z3_decl_kind; -import com.microsoft.z3legacy.enumerations.Z3_sort_kind; import hu.bme.mit.theta.common.TernaryOperator; import hu.bme.mit.theta.common.TriFunction; import hu.bme.mit.theta.common.Tuple2; @@ -110,13 +109,16 @@ final class Z3TermTransformer { private static final String PARAM_NAME_FORMAT = "_p%d"; private final Z3SymbolTable symbolTable; + private final Z3TypeSymbolTable typeSymbolTable; private final Map< Tuple2, TriFunction>, Expr>> environment; - public Z3TermTransformer(final Z3SymbolTable symbolTable) { + public Z3TermTransformer( + final Z3SymbolTable symbolTable, final Z3TypeSymbolTable typeSymbolTable) { this.symbolTable = symbolTable; + this.typeSymbolTable = typeSymbolTable; environment = Containers.createMap(); @@ -427,6 +429,10 @@ private Expr transform( return transformArrLit(term, model, vars); } else if (term.isApp()) { + if (term.getFuncDecl().getDeclKind().equals(Z3_decl_kind.Z3_OP_DT_CONSTRUCTOR)) { + final EnumType enumType = (EnumType) transformSort(term.getSort()); + return transformEnumLit(term, enumType); + } return transformApp(term, model, vars); } else if (term.isQuantifier()) { @@ -747,6 +753,8 @@ private Type transformSort(final com.microsoft.z3legacy.Sort sort) { return ArrayType.of( transformSort(((com.microsoft.z3legacy.ArraySort) sort).getDomain()), transformSort(((com.microsoft.z3legacy.ArraySort) sort).getRange())); + } else if (sort instanceof com.microsoft.z3legacy.DatatypeSort) { + return typeSymbolTable.getType(sort.getName().toString()); } else { throw new AssertionError("Unsupported sort: " + sort); } @@ -855,25 +863,6 @@ private Expr transformUnsupported( (term, model, vars) -> { final com.microsoft.z3legacy.Expr[] args = term.getArgs(); checkArgument(args.length == 2, "Number of arguments must be two"); - if (args[0].getSort().getSortKind().equals(Z3_sort_kind.Z3_DATATYPE_SORT)) { - // binary operator is on enum types - // if either arg is a literal, we need special handling to get its type - // (references' decl kind is Z3_OP_UNINTERPRETED, literals' decl kind is - // Z3_OP_DT_CONSTRUCTOR) - int litIndex = -1; - for (int i = 0; i < 2; i++) { - if (args[i].getFuncDecl() - .getDeclKind() - .equals(Z3_decl_kind.Z3_OP_DT_CONSTRUCTOR)) litIndex = i; - } - if (litIndex > -1) { - int refIndex = Math.abs(litIndex - 1); - final Expr refOp = transform(args[refIndex], model, vars); - final Expr litExpr = - transformEnumLit(args[litIndex], (EnumType) refOp.getType()); - return function.apply(refOp, litExpr); - } - } final Expr op1 = transform(args[0], model, vars); final Expr op2 = transform(args[1], model, vars); return function.apply(op1, op2); @@ -915,6 +904,31 @@ private Expr transformUnsupported( (term, model, vars) -> { final com.microsoft.z3legacy.Expr[] args = term.getArgs(); checkArgument(args.length == 3, "Number of arguments must be three"); + // if + // (args[0].getSort().getSortKind().equals(Z3_sort_kind.Z3_DATATYPE_SORT)) { + // // ternary operator is on enum types + // // if either arg is a literal, we need special + // handling to get its type + // // (references' decl kind is Z3_OP_UNINTERPRETED, + // literals' decl kind is + // // Z3_OP_DT_CONSTRUCTOR) + // int litIndex = -1; + // for (int i = 0; i < 3; i++) { + // if (args[i].getFuncDecl() + // .getDeclKind() + // .equals(Z3_decl_kind.Z3_OP_DT_CONSTRUCTOR)) + // litIndex = i; + // } + // if (litIndex > -1) { + // int refIndex = Math.abs(litIndex - 1); + // final Expr refOp = transform(args[refIndex], + // model, vars); + //// final Expr litExpr = + //// transformEnumLit(args[litIndex], (EnumType) + // refOp.getType()); + //// return function.apply(refOp, litExpr); + // } + // } final Expr op1 = transform(args[0], model, vars); final Expr op2 = transform(args[1], model, vars); final Expr op3 = transform(args[2], model, vars); diff --git a/subprojects/solver/solver-z3-legacy/src/main/java/hu/bme/mit/theta/solver/z3legacy/Z3TransformationManager.java b/subprojects/solver/solver-z3-legacy/src/main/java/hu/bme/mit/theta/solver/z3legacy/Z3TransformationManager.java index c1fb3e4547..f9ba00bf48 100644 --- a/subprojects/solver/solver-z3-legacy/src/main/java/hu/bme/mit/theta/solver/z3legacy/Z3TransformationManager.java +++ b/subprojects/solver/solver-z3-legacy/src/main/java/hu/bme/mit/theta/solver/z3legacy/Z3TransformationManager.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. @@ -26,8 +26,11 @@ final class Z3TransformationManager { private final Z3DeclTransformer declTransformer; private final Z3ExprTransformer exprTransformer; - public Z3TransformationManager(final Z3SymbolTable symbolTable, final Context context) { - this.typeTransformer = new Z3TypeTransformer(this, context); + public Z3TransformationManager( + final Z3SymbolTable symbolTable, + final Z3TypeSymbolTable typeSymbolTable, + final Context context) { + this.typeTransformer = new Z3TypeTransformer(this, typeSymbolTable, context); this.declTransformer = new Z3DeclTransformer(this, symbolTable, context); this.exprTransformer = new Z3ExprTransformer(this, context); } diff --git a/subprojects/solver/solver-z3-legacy/src/main/java/hu/bme/mit/theta/solver/z3legacy/Z3TypeSymbolTable.java b/subprojects/solver/solver-z3-legacy/src/main/java/hu/bme/mit/theta/solver/z3legacy/Z3TypeSymbolTable.java new file mode 100644 index 0000000000..c3fd3e1a25 --- /dev/null +++ b/subprojects/solver/solver-z3-legacy/src/main/java/hu/bme/mit/theta/solver/z3legacy/Z3TypeSymbolTable.java @@ -0,0 +1,61 @@ +/* + * 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. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.solver.z3legacy; + +import static com.google.common.base.Preconditions.*; + +import com.google.common.collect.BiMap; +import com.google.common.collect.HashBiMap; +import com.google.common.collect.Maps; +import hu.bme.mit.theta.core.type.Type; + +final class Z3TypeSymbolTable { + + private final BiMap constToSymbol; + + public Z3TypeSymbolTable() { + constToSymbol = Maps.synchronizedBiMap(HashBiMap.create()); + } + + public boolean definesType(final Type type) { + return constToSymbol.containsKey(type); + } + + public boolean definesSymbol(final String symbol) { + return constToSymbol.inverse().containsKey(symbol); + } + + public String getSymbol(final Type type) { + checkArgument(definesType(type), "Type %s not found in symbol table", type); + return constToSymbol.get(type); + } + + public Type getType(final String symbol) { + checkArgument(definesSymbol(symbol), "Symbol %s not found in symbol table", symbol); + return constToSymbol.inverse().get(symbol); + } + + public void put(final Type type, final String symbol) { + checkNotNull(type); + checkNotNull(symbol); + checkState(!constToSymbol.containsKey(type), "Type %s not found.", type); + constToSymbol.put(type, symbol); + } + + public void clear() { + constToSymbol.clear(); + } +} diff --git a/subprojects/solver/solver-z3-legacy/src/main/java/hu/bme/mit/theta/solver/z3legacy/Z3TypeTransformer.java b/subprojects/solver/solver-z3-legacy/src/main/java/hu/bme/mit/theta/solver/z3legacy/Z3TypeTransformer.java index 4d3653ba70..0374f51d57 100644 --- a/subprojects/solver/solver-z3-legacy/src/main/java/hu/bme/mit/theta/solver/z3legacy/Z3TypeTransformer.java +++ b/subprojects/solver/solver-z3-legacy/src/main/java/hu/bme/mit/theta/solver/z3legacy/Z3TypeTransformer.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. @@ -34,6 +34,7 @@ final class Z3TypeTransformer { private final Z3TransformationManager transformer; private final Context context; + private final Z3TypeSymbolTable symbolTable; private final com.microsoft.z3legacy.BoolSort boolSort; private final com.microsoft.z3legacy.IntSort intSort; @@ -42,9 +43,13 @@ final class Z3TypeTransformer { private final Set fpSorts; private final Map enumSorts; - Z3TypeTransformer(final Z3TransformationManager transformer, final Context context) { + Z3TypeTransformer( + final Z3TransformationManager transformer, + final Z3TypeSymbolTable symbolTable, + final Context context) { this.context = context; this.transformer = transformer; + this.symbolTable = symbolTable; boolSort = context.mkBoolSort(); intSort = context.mkIntSort(); @@ -108,10 +113,13 @@ public void reset() { } private EnumSort createEnumSort(EnumType enumType) { - return context.mkEnumSort( - enumType.getName(), - enumType.getValues().stream() - .map(lit -> EnumType.makeLongName(enumType, lit)) - .toArray(String[]::new)); + var sort = + context.mkEnumSort( + enumType.getName(), + enumType.getValues().stream() + .map(lit -> EnumType.makeLongName(enumType, lit)) + .toArray(String[]::new)); + symbolTable.put(enumType, sort.getName().toString()); + return sort; } } diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToMddChecker.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToMddChecker.kt index e63d9ca699..f22ec97758 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToMddChecker.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToMddChecker.kt @@ -51,32 +51,15 @@ fun getMddChecker( val refinementSolverFactory: SolverFactory = getSolver(mddConfig.solver, mddConfig.validateSolver) - val stmts = - xcfa.procedures - .flatMap { it.edges.flatMap { xcfaEdge -> xcfaEdge.getFlatLabels().map { it.toStmt() } } } - .toSet() val solverPool = SolverPool(refinementSolverFactory) - val iterationStrategy = mddConfig.iterationStrategy val baseChecker = { monolithicExpr: MonolithicExpr -> MddChecker( monolithicExpr, solverPool, logger, - iterationStrategy, - // variableOrdering = - // orderVarsFromRandomStartingPoints( - // monolithicExpr.vars, - // stmts - // .map { - // object : Event> { - // override fun getAffectedVars(): List> = - // StmtUtils.getWrittenVars(it).toList() - // } - // } - // .toList(), - // 20, - // ), + iterationStrategy = mddConfig.iterationStrategy, + mddToExprStrategy = mddConfig.mddToExprStrategy ) } val passes = mutableListOf>() diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/XcfaConfig.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/XcfaConfig.kt index 65772fac39..20c9090cdf 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/XcfaConfig.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/XcfaConfig.kt @@ -19,6 +19,7 @@ import com.beust.jcommander.Parameter import hu.bme.mit.theta.analysis.algorithm.loopchecker.abstraction.LoopCheckerSearchStrategy import hu.bme.mit.theta.analysis.algorithm.loopchecker.refinement.ASGTraceCheckerStrategy import hu.bme.mit.theta.analysis.algorithm.mdd.MddChecker.IterationStrategy +import hu.bme.mit.theta.analysis.algorithm.mdd.expressionnode.MddExpressionRepresentation import hu.bme.mit.theta.analysis.expr.refinement.PruneStrategy import hu.bme.mit.theta.common.logging.Logger import hu.bme.mit.theta.frontend.ParseContext @@ -547,6 +548,11 @@ data class MddConfig( description = "Iteration strategy for the MDD checker", ) var iterationStrategy: IterationStrategy = IterationStrategy.GSAT, + @Parameter( + names = ["--mdd-to-expr-strategy"], + description = "MDD to expression conversion strategy", + ) + var mddToExprStrategy: MddExpressionRepresentation.MddToExprStrategy = MddExpressionRepresentation.MddToExprStrategy.VARIABLE_LEVEL, @Parameter(names = ["--reversed"], description = "Create a reversed monolithic expression") var reversed: Boolean = false, @Parameter(names = ["--cegar"], description = "Wrap the check in a predicate-based CEGAR loop") diff --git a/subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/XstsMddStructuralSymbolicComparisonTest.java b/subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/XstsMddStructuralSymbolicComparisonTest.java index b7d53ecedb..74a23f275d 100644 --- a/subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/XstsMddStructuralSymbolicComparisonTest.java +++ b/subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/XstsMddStructuralSymbolicComparisonTest.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. @@ -156,7 +156,7 @@ private static Long calculateNonzeroCount( MddHandle node, int level, Map cache, - RecursiveIntObjCursor cursor) { + RecursiveIntObjCursor cursor) { Long cached = (Long) cache.getOrDefault(node, null); if (cached != null) { return cached; @@ -171,7 +171,9 @@ private static Long calculateNonzeroCount( while (cursor.moveNext()) { try (var valueCursor = cursor.valueCursor()) { - Long res = calculateNonzeroCount(cursor.value(), level - 1, cache, valueCursor); + Long res = + calculateNonzeroCount( + (MddHandle) cursor.value(), level - 1, cache, valueCursor); if (res == null) { return null; } diff --git a/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliMdd.kt b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliMdd.kt index 3338f3820d..520f0dec44 100644 --- a/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliMdd.kt +++ b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliMdd.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. @@ -24,6 +24,7 @@ import hu.bme.mit.theta.analysis.algorithm.InvariantProof import hu.bme.mit.theta.analysis.algorithm.SafetyResult import hu.bme.mit.theta.analysis.algorithm.mdd.MddAnalysisStatistics import hu.bme.mit.theta.analysis.algorithm.mdd.MddChecker +import hu.bme.mit.theta.analysis.algorithm.mdd.expressionnode.MddExpressionRepresentation import hu.bme.mit.theta.common.logging.Logger import hu.bme.mit.theta.solver.SolverManager import hu.bme.mit.theta.solver.SolverPool @@ -44,6 +45,11 @@ class XstsCliMdd : .enum() .default(MddChecker.IterationStrategy.GSAT) + private val mddToExprStrategy: MddExpressionRepresentation.MddToExprStrategy by + option(help = "The MDD to expression conversion strategy") + .enum() + .default(MddExpressionRepresentation.MddToExprStrategy.VARIABLE_LEVEL) + private fun printResult( status: SafetyResult, XstsAction>>, xsts: XSTS, @@ -85,7 +91,13 @@ class XstsCliMdd : SolverPool(solverFactory).use { solverPool -> val checker = createChecker(xsts, solverFactory) { - MddChecker(it, solverPool, logger, iterationStrategy) + MddChecker( + it, + solverPool, + logger, + iterationStrategy, + mddToExprStrategy = mddToExprStrategy, + ) } checker.check(null) }