JavaSMT proofs

build.gradle.kts

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

buildSrc/src/main/kotlin/Deps.kt

@@ -30,7 +30,7 @@ object Deps {
 
     val cvc5 = "lib/cvc5.jar"
 
-    val javasmt = "org.sosy-lab:java-smt:${Versions.javasmt}"
+    //val javasmt = "org.sosy-lab:java-smt:${Versions.javasmt}"
     val javasmtLocal = "lib/javasmt.jar"
     val sosylabCommon = "org.sosy-lab:common:${Versions.sosylab}"
 

subprojects/common/analysis/build.gradle.kts

@@ -23,7 +23,7 @@ dependencies {
     implementation(project(":theta-common"))
     implementation(project(":theta-core"))
     implementation(project(":theta-solver"))
-    implementation(Deps.javasmt)
+    implementation(Deps.sosylabCommon)
     implementation(project(":theta-solver-javasmt"))
     implementation(project(":theta-solver-z3-legacy"))
     implementation(project(":theta-graph-solver"))

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/ExprTraceProofChecker.java

@@ -0,0 +1,127 @@
+/*
+ *  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.expr.refinement;
+
+import static com.google.common.base.Preconditions.checkNotNull;
+import static hu.bme.mit.theta.core.type.booltype.BoolExprs.False;
+
+import com.google.common.collect.ImmutableList;
+import hu.bme.mit.theta.analysis.Trace;
+import hu.bme.mit.theta.analysis.expr.ExprAction;
+import hu.bme.mit.theta.analysis.expr.ExprState;
+import hu.bme.mit.theta.core.model.Valuation;
+import hu.bme.mit.theta.core.type.Expr;
+import hu.bme.mit.theta.core.type.booltype.BoolType;
+import hu.bme.mit.theta.core.utils.ExprUtils;
+import hu.bme.mit.theta.core.utils.IndexedVars;
+import hu.bme.mit.theta.core.utils.PathUtils;
+import hu.bme.mit.theta.core.utils.indexings.VarIndexing;
+import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory;
+import hu.bme.mit.theta.solver.ProofNode;
+import hu.bme.mit.theta.solver.Solver;
+import hu.bme.mit.theta.solver.utils.WithPushPop;
+import java.util.ArrayList;
+import java.util.List;
+import java.util.Set;
+import java.util.stream.Collectors;
+
+/** An ExprTraceChecker that generates an unsat core by checking the trace at once. */
+public final class ExprTraceProofChecker implements ExprTraceChecker<VarsRefutation> {
+
+    private final Solver solver;
+    private final Expr<BoolType> init;
+    private final Expr<BoolType> target;
+
+    private ExprTraceProofChecker(
+            final Expr<BoolType> init, final Expr<BoolType> target, final Solver solver) {
+        this.solver = checkNotNull(solver);
+        this.init = checkNotNull(init);
+        this.target = checkNotNull(target);
+    }
+
+    public static ExprTraceProofChecker create(
+            final Expr<BoolType> init, final Expr<BoolType> target, final Solver solver) {
+        return new ExprTraceProofChecker(init, target, solver);
+    }
+
+    @Override
+    public ExprTraceStatus<VarsRefutation> check(
+            final Trace<? extends ExprState, ? extends ExprAction> trace) {
+        checkNotNull(trace);
+        final int stateCount = trace.getStates().size();
+
+        final List<VarIndexing> indexings = new ArrayList<>(stateCount);
+        indexings.add(VarIndexingFactory.indexing(0));
+
+        try (WithPushPop wpp = new WithPushPop(solver)) {
+            solver.add(ExprUtils.getConjuncts(PathUtils.unfold(init, indexings.get(0))));
+            solver.add(
+                    ExprUtils.getConjuncts(
+                            PathUtils.unfold(trace.getState(0).toExpr(), indexings.get(0))));
+            assert solver.check().isSat() : "Initial state of the trace is not feasible";
+            boolean concretizable = true;
+
+            for (int i = 1; i < stateCount; ++i) {
+                indexings.add(indexings.get(i - 1).add(trace.getAction(i - 1).nextIndexing()));
+                solver.add(
+                        ExprUtils.getConjuncts(
+                                PathUtils.unfold(trace.getState(i).toExpr(), indexings.get(i))));
+                solver.add(
+                        ExprUtils.getConjuncts(
+                                PathUtils.unfold(
+                                        trace.getAction(i - 1).toExpr(), indexings.get(i - 1))));
+
+                if (!solver.check().isSat()) {
+                    concretizable = false;
+                    break;
+                }
+            }
+
+            if (concretizable) {
+                solver.add(
+                        ExprUtils.getConjuncts(
+                                PathUtils.unfold(target, indexings.get(stateCount - 1))));
+                concretizable = solver.check().isSat();
+            }
+
+            if (concretizable) {
+                final Valuation model = solver.getModel();
+                final ImmutableList.Builder<Valuation> builder = ImmutableList.builder();
+                for (final VarIndexing indexing : indexings) {
+                    builder.add(PathUtils.extractValuation(model, indexing));
+                }
+                return ExprTraceStatus.feasible(Trace.of(builder.build(), trace.getActions()));
+            } else {
+                Set<ProofNode> proofLevel = Set.of(solver.getProof());
+                while (proofLevel.stream()
+                        .allMatch(proofNode -> proofNode.expr().equals(False()))) {
+                    proofLevel =
+                            proofLevel.stream()
+                                    .flatMap(proofNode -> proofNode.children().stream())
+                                    .collect(Collectors.toSet());
+                }
+                final var reasons = proofLevel.stream().map(ProofNode::expr).toList();
+                final IndexedVars indexedVars = ExprUtils.getVarsIndexed(reasons);
+                return ExprTraceStatus.infeasible(VarsRefutation.create(indexedVars));
+            }
+        }
+    }
+
+    @Override
+    public String toString() {
+        return getClass().getSimpleName();
+    }
+}

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/ptr/VarRefToPtrPrec.kt

@@ -0,0 +1,41 @@
+/*
+ *  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.ptr
+
+import com.google.common.base.Preconditions
+import hu.bme.mit.theta.analysis.Prec
+import hu.bme.mit.theta.analysis.expr.refinement.RefutationToPrec
+import hu.bme.mit.theta.analysis.expr.refinement.VarsRefutation
+import hu.bme.mit.theta.common.Utils
+
+/** Transformer from interpolant refutation to pointer precision. */
+class VarRefToPtrPrec<P : Prec>(private val innerRefToPrec: RefutationToPrec<P, VarsRefutation>) :
+  RefutationToPrec<PtrPrec<P>, VarsRefutation> {
+
+  override fun toPrec(refutation: VarsRefutation, index: Int): PtrPrec<P> {
+    return PtrPrec(innerRefToPrec.toPrec(refutation, index))
+  }
+
+  override fun join(prec1: PtrPrec<P>, prec2: PtrPrec<P>): PtrPrec<P> {
+    Preconditions.checkNotNull(prec1)
+    Preconditions.checkNotNull(prec2)
+    return PtrPrec(innerRefToPrec.join(prec1.innerPrec, prec2.innerPrec))
+  }
+
+  override fun toString(): String {
+    return Utils.lispStringBuilder(javaClass.simpleName).aligned().add(innerRefToPrec).toString()
+  }
+}

subprojects/solver/solver-javasmt/build.gradle.kts

@@ -22,7 +22,7 @@ dependencies {
     implementation(project(":theta-core"))
     implementation(project(":theta-solver"))
     implementation(files(rootDir.resolve(Deps.javasmtLocal)))
-    implementation(Deps.javasmt)
+    implementation(Deps.sosylabCommon)
     implementation(files(rootDir.resolve(Deps.cvc5)))
     testImplementation(testFixtures(project(":theta-core")))
 }

subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTExprTransformer.java

@@ -29,7 +29,6 @@
 import hu.bme.mit.theta.core.decl.ParamDecl;
 import hu.bme.mit.theta.core.dsl.DeclSymbol;
 import hu.bme.mit.theta.core.type.Expr;
-import hu.bme.mit.theta.core.type.LitExpr;
 import hu.bme.mit.theta.core.type.Type;
 import hu.bme.mit.theta.core.type.anytype.Dereference;
 import hu.bme.mit.theta.core.type.anytype.IteExpr;
@@ -795,21 +794,21 @@ private Formula transformBvSMod(final BvSModExpr expr) {
         final BitvectorFormula leftOpTerm = (BitvectorFormula) toTerm(expr.getLeftOp());
         final BitvectorFormula rightOpTerm = (BitvectorFormula) toTerm(expr.getRightOp());
 
-        return bitvectorFormulaManager.smod(leftOpTerm, rightOpTerm);
+        return bitvectorFormulaManager.smodulo(leftOpTerm, rightOpTerm);
     }
 
     private Formula transformBvURem(final BvURemExpr expr) {
         final BitvectorFormula leftOpTerm = (BitvectorFormula) toTerm(expr.getLeftOp());
         final BitvectorFormula rightOpTerm = (BitvectorFormula) toTerm(expr.getRightOp());
 
-        return bitvectorFormulaManager.rem(leftOpTerm, rightOpTerm, false);
+        return bitvectorFormulaManager.remainder(leftOpTerm, rightOpTerm, false);
     }
 
     private Formula transformBvSRem(final BvSRemExpr expr) {
         final BitvectorFormula leftOpTerm = (BitvectorFormula) toTerm(expr.getLeftOp());
         final BitvectorFormula rightOpTerm = (BitvectorFormula) toTerm(expr.getRightOp());
 
-        return bitvectorFormulaManager.rem(leftOpTerm, rightOpTerm, true);
+        return bitvectorFormulaManager.remainder(leftOpTerm, rightOpTerm, true);
     }
 
     private Formula transformBvAnd(final BvAndExpr expr) {
@@ -1112,7 +1111,7 @@ private Formula transformFpFromBv(final FpFromBvExpr expr) {
         final BitvectorFormula val = (BitvectorFormula) toTerm(expr.getOp());
         final FloatingPointType fpSort =
                 FloatingPointType.getFloatingPointType(
-                        expr.getFpType().getExponent(), expr.getFpType().getSignificand() - 1);
+                        expr.getFpType().getExponent(), expr.getFpType().getSignificand());
         return floatingPointFormulaManager.castFrom(val, expr.isSigned(), fpSort);
     }
 
@@ -1170,18 +1169,20 @@ private Formula transformArrayNeq(final ArrayNeqExpr<?, ?> expr) {
 
     private <TI extends Formula, TE extends Formula> Formula transformArrayLit(
             final ArrayLitExpr<?, ?> expr) {
-        final TE elseElem = (TE) toTerm(expr.getElseElem());
-        final FormulaType<TE> elemType =
-                (FormulaType<TE>) transformer.toSort(expr.getType().getElemType());
-        final FormulaType<TI> indexType =
-                (FormulaType<TI>) transformer.toSort(expr.getType().getIndexType());
-        var arr = arrayFormulaManager.makeArray(elseElem, indexType, elemType);
-        for (Tuple2<? extends LitExpr<?>, ? extends LitExpr<?>> element : expr.getElements()) {
-            final TI index = (TI) toTerm(element.get1());
-            final TE elem = (TE) toTerm(element.get2());
-            arr = arrayFormulaManager.store(arr, index, elem);
-        }
-        return arr;
+        throw new UnsupportedOperationException();
+        //        final TE elseElem = (TE) toTerm(expr.getElseElem());
+        //        final FormulaType<TE> elemType =
+        //                (FormulaType<TE>) transformer.toSort(expr.getType().getElemType());
+        //        final FormulaType<TI> indexType =
+        //                (FormulaType<TI>) transformer.toSort(expr.getType().getIndexType());
+        //        var arr = arrayFormulaManager.makeArray(elseElem, indexType, elemType);
+        //        for (Tuple2<? extends LitExpr<?>, ? extends LitExpr<?>> element :
+        // expr.getElements()) {
+        //            final TI index = (TI) toTerm(element.get1());
+        //            final TE elem = (TE) toTerm(element.get2());
+        //            arr = arrayFormulaManager.store(arr, index, elem);
+        //        }
+        //        return arr;
     }
 
     /*
@@ -1190,18 +1191,19 @@ private <TI extends Formula, TE extends Formula> Formula transformArrayLit(
 
     private <TI extends Formula, TE extends Formula> Formula transformArrayInit(
             final ArrayInitExpr<?, ?> expr) {
-        final TE elseElem = (TE) toTerm(expr.getElseElem());
-        final FormulaType<TE> elemType =
-                (FormulaType<TE>) transformer.toSort(expr.getType().getElemType());
-        final FormulaType<TI> indexType =
-                (FormulaType<TI>) transformer.toSort(expr.getType().getIndexType());
-        var arr = arrayFormulaManager.makeArray(elseElem, indexType, elemType);
-        for (Tuple2<? extends Expr<?>, ? extends Expr<?>> element : expr.getElements()) {
-            final TI index = (TI) toTerm(element.get1());
-            final TE elem = (TE) toTerm(element.get2());
-            arr = arrayFormulaManager.store(arr, index, elem);
-        }
-        return arr;
+        throw new UnsupportedOperationException();
+        //        final TE elseElem = (TE) toTerm(expr.getElseElem());
+        //        final FormulaType<TE> elemType =
+        //                (FormulaType<TE>) transformer.toSort(expr.getType().getElemType());
+        //        final FormulaType<TI> indexType =
+        //                (FormulaType<TI>) transformer.toSort(expr.getType().getIndexType());
+        //        var arr = arrayFormulaManager.makeArray(elseElem, indexType, elemType);
+        //        for (Tuple2<? extends Expr<?>, ? extends Expr<?>> element : expr.getElements()) {
+        //            final TI index = (TI) toTerm(element.get1());
+        //            final TE elem = (TE) toTerm(element.get2());
+        //            arr = arrayFormulaManager.store(arr, index, elem);
+        //        }
+        //        return arr;
     }
 
     private Formula transformFuncApp(final FuncAppExpr<?, ?> expr) {