diff --git a/build.gradle.kts b/build.gradle.kts index 4cb03e1d2d..314c263e42 100644 --- a/build.gradle.kts +++ b/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")) } diff --git a/buildSrc/src/main/kotlin/Deps.kt b/buildSrc/src/main/kotlin/Deps.kt index 6618e45452..1ee4c32127 100644 --- a/buildSrc/src/main/kotlin/Deps.kt +++ b/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}" diff --git a/lib/javasmt.jar b/lib/javasmt.jar index 5f806c43c0..d245f5fbdf 100644 Binary files a/lib/javasmt.jar and b/lib/javasmt.jar differ diff --git a/subprojects/common/analysis/build.gradle.kts b/subprojects/common/analysis/build.gradle.kts index 36fe0aaf99..7b2aa21c05 100644 --- a/subprojects/common/analysis/build.gradle.kts +++ b/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")) diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/ExprTraceProofChecker.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/ExprTraceProofChecker.java new file mode 100644 index 0000000000..c391462aa8 --- /dev/null +++ b/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 { + + private final Solver solver; + private final Expr init; + private final Expr target; + + private ExprTraceProofChecker( + final Expr init, final Expr target, final Solver solver) { + this.solver = checkNotNull(solver); + this.init = checkNotNull(init); + this.target = checkNotNull(target); + } + + public static ExprTraceProofChecker create( + final Expr init, final Expr target, final Solver solver) { + return new ExprTraceProofChecker(init, target, solver); + } + + @Override + public ExprTraceStatus check( + final Trace trace) { + checkNotNull(trace); + final int stateCount = trace.getStates().size(); + + final List 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 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 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(); + } +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/ptr/VarRefToPtrPrec.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/ptr/VarRefToPtrPrec.kt new file mode 100644 index 0000000000..af06f55937 --- /dev/null +++ b/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

(private val innerRefToPrec: RefutationToPrec) : + RefutationToPrec, VarsRefutation> { + + override fun toPrec(refutation: VarsRefutation, index: Int): PtrPrec

{ + return PtrPrec(innerRefToPrec.toPrec(refutation, index)) + } + + override fun join(prec1: PtrPrec

, prec2: PtrPrec

): PtrPrec

{ + 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() + } +} diff --git a/subprojects/solver/solver-javasmt/build.gradle.kts b/subprojects/solver/solver-javasmt/build.gradle.kts index 3840f712d3..494da73b5c 100644 --- a/subprojects/solver/solver-javasmt/build.gradle.kts +++ b/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"))) } diff --git a/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTExprTransformer.java b/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTExprTransformer.java index 2fb06b2417..1299678d86 100644 --- a/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTExprTransformer.java +++ b/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 Formula transformArrayLit( final ArrayLitExpr expr) { - final TE elseElem = (TE) toTerm(expr.getElseElem()); - final FormulaType elemType = - (FormulaType) transformer.toSort(expr.getType().getElemType()); - final FormulaType indexType = - (FormulaType) transformer.toSort(expr.getType().getIndexType()); - var arr = arrayFormulaManager.makeArray(elseElem, indexType, elemType); - for (Tuple2, ? 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 elemType = + // (FormulaType) transformer.toSort(expr.getType().getElemType()); + // final FormulaType indexType = + // (FormulaType) transformer.toSort(expr.getType().getIndexType()); + // var arr = arrayFormulaManager.makeArray(elseElem, indexType, elemType); + // for (Tuple2, ? 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 Formula transformArrayLit( private Formula transformArrayInit( final ArrayInitExpr expr) { - final TE elseElem = (TE) toTerm(expr.getElseElem()); - final FormulaType elemType = - (FormulaType) transformer.toSort(expr.getType().getElemType()); - final FormulaType indexType = - (FormulaType) transformer.toSort(expr.getType().getIndexType()); - var arr = arrayFormulaManager.makeArray(elseElem, indexType, elemType); - for (Tuple2, ? 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 elemType = + // (FormulaType) transformer.toSort(expr.getType().getElemType()); + // final FormulaType indexType = + // (FormulaType) transformer.toSort(expr.getType().getIndexType()); + // var arr = arrayFormulaManager.makeArray(elseElem, indexType, elemType); + // for (Tuple2, ? 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) { diff --git a/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTHornSolver.java b/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTHornSolver.java new file mode 100644 index 0000000000..ffc78249dd --- /dev/null +++ b/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTHornSolver.java @@ -0,0 +1,110 @@ +/* + * 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.solver.javasmt; + +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Bool; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.False; +import static hu.bme.mit.theta.core.utils.TypeUtils.cast; + +import hu.bme.mit.theta.core.type.Expr; +import hu.bme.mit.theta.core.type.booltype.BoolType; +import hu.bme.mit.theta.solver.*; +import java.util.*; +import org.sosy_lab.java_smt.api.*; + +final class JavaSMTHornSolver extends JavaSMTSolver implements HornSolver { + + public JavaSMTHornSolver( + final JavaSMTSymbolTable symbolTable, + final JavaSMTTransformationManager transformationManager, + final JavaSMTTermTransformer termTransformer, + final SolverContext context, + final BasicProverEnvironment solver) { + super(symbolTable, transformationManager, termTransformer, context, solver); + } + + //// + + @Override + public void track(final Expr assertion) { + throw new UnsupportedOperationException("Cannot \"track\" in Horn solver"); + } + + @Override + public Collection> getUnsatCore() { + throw new UnsupportedOperationException("Cannot get unsat core in Horn solver"); + } + + private Expr toExpr(Formula f) { + if (f.toString().matches("query!([0-9]+)")) { // z3 query![0-9]+ + return False(); + } + final var e = termTransformer.toExpr(f); + return cast(e, Bool()); + } + + @Override + public ProofNode getProof() { + try { + var proof = solver.getProof(); + + var builder = new ProofNode.Builder(toExpr(proof.getFormula())); + final var rootBuilder = builder; + + proof_transformer: + while (true) { + switch (proof.getRule().toString()) { + case "ASSERTED": + { + builder.addChild(new ProofNode.Builder(toExpr(proof.getFormula()))); + break proof_transformer; + } + case "HYPER_RESOLVE": + { + final var childBuilder = + new ProofNode.Builder(toExpr(proof.getFormula())); + builder.addChild(childBuilder); + if (proof.getChildren().size() > 1) { + proof = proof.getChildren().get(1); + builder = childBuilder; + break; + } else { + break proof_transformer; + } + } + case "MODUS_PONENS": + { + final var childBuilder = + new ProofNode.Builder(toExpr(proof.getFormula())); + builder.addChild(childBuilder); + proof = proof.getChildren().get(0); + builder = childBuilder; + break; + } + default: + throw new UnsupportedOperationException( + "Unsupported proof rule: " + proof.getRule()); + } + } + + ProofNode ret = rootBuilder.build(); + return ret; + + } catch (SolverException | InterruptedException e) { + throw new RuntimeException(e); + } + } +} diff --git a/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolver.java b/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolver.java index 032aeb7e51..57e06a72c2 100644 --- a/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolver.java +++ b/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolver.java @@ -17,6 +17,9 @@ import static com.google.common.base.Preconditions.checkNotNull; import static com.google.common.base.Preconditions.checkState; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Bool; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.False; +import static hu.bme.mit.theta.core.utils.TypeUtils.cast; import com.google.common.collect.ImmutableList; import com.google.common.collect.ImmutableMap; @@ -33,10 +36,7 @@ import hu.bme.mit.theta.core.type.bvtype.BvType; import hu.bme.mit.theta.core.type.enumtype.EnumType; import hu.bme.mit.theta.core.type.functype.FuncType; -import hu.bme.mit.theta.solver.Solver; -import hu.bme.mit.theta.solver.SolverStatus; -import hu.bme.mit.theta.solver.Stack; -import hu.bme.mit.theta.solver.UCSolver; +import hu.bme.mit.theta.solver.*; import hu.bme.mit.theta.solver.impl.StackImpl; import java.util.Collection; import java.util.Collections; @@ -52,14 +52,14 @@ import org.sosy_lab.java_smt.api.SolverContext; import org.sosy_lab.java_smt.api.SolverException; -final class JavaSMTSolver implements UCSolver, Solver { +class JavaSMTSolver implements UCSolver, Solver { - private final JavaSMTSymbolTable symbolTable; - private final JavaSMTTransformationManager transformationManager; - private final JavaSMTTermTransformer termTransformer; + protected final JavaSMTSymbolTable symbolTable; + protected final JavaSMTTransformationManager transformationManager; + protected final JavaSMTTermTransformer termTransformer; - private final SolverContext context; - private final BasicProverEnvironment solver; + protected final SolverContext context; + protected final BasicProverEnvironment solver; private final Stack> assertions; @@ -235,6 +235,34 @@ public ImmutableMap getStatistics() { return solver.getStatistics(); } + private Expr toExpr(Formula f) { + if (f.toString().matches("query!([0-9]+)")) { // z3 query![0-9]+ + return False(); + } + final var e = termTransformer.toExpr(f); + return cast(e, Bool()); + } + + @Override + public ProofNode getProof() { + try { + var proof = solver.getProof(); + + return toProof(proof).build(); + + } catch (SolverException | InterruptedException e) { + throw new RuntimeException(e); + } + } + + private ProofNode.Builder toProof(org.sosy_lab.java_smt.api.proofs.ProofNode proof) { + var builder = new ProofNode.Builder(toExpr(proof.getFormula())); + for (org.sosy_lab.java_smt.api.proofs.ProofNode child : proof.getChildren()) { + builder.addChild(toProof(child)); + } + return builder; + } + //// private final class JavaSMTModel extends Valuation { diff --git a/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolverFactory.java b/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolverFactory.java index 3828196142..ea1b5ddc52 100644 --- a/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolverFactory.java +++ b/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolverFactory.java @@ -15,10 +15,7 @@ */ package hu.bme.mit.theta.solver.javasmt; -import hu.bme.mit.theta.solver.ItpSolver; -import hu.bme.mit.theta.solver.Solver; -import hu.bme.mit.theta.solver.SolverFactory; -import hu.bme.mit.theta.solver.UCSolver; +import hu.bme.mit.theta.solver.*; import java.util.List; import java.util.Map; import java.util.stream.Stream; @@ -108,6 +105,11 @@ public static JavaSMTSolverFactory create(Solvers solver, String[] args) { @Override public Solver createSolver() { try { + Configuration config = + Configuration.builder() + .copyFrom(this.config) + .setOption("solver.z3.requireProofs", "true") + .build(); final SolverContext context = SolverContextFactory.createSolverContext( config, logger, shutdownManager.getNotifier(), solver); @@ -200,4 +202,32 @@ public ItpSolver createItpSolver() { throw new JavaSMTSolverException(e); } } + + @Override + public HornSolver createHornSolver() { + try { + Configuration config = + Configuration.builder() + .copyFrom(this.config) + .setOption("solver.z3.requireProofs", "true") + .build(); + final SolverContext context = + SolverContextFactory.createSolverContext( + config, logger, shutdownManager.getNotifier(), solver); + final JavaSMTSymbolTable symbolTable = new JavaSMTSymbolTable(); + final JavaSMTTransformationManager transformationManager = + new JavaSMTTransformationManager(symbolTable, context); + final JavaSMTTermTransformer termTransformer = + new JavaSMTTermTransformer(symbolTable, context); + + final ProverEnvironment prover = + context.newProverEnvironment( + ProverOptions.GENERATE_MODELS, ProverOptions.GENERATE_PROOFS); + + return new JavaSMTHornSolver( + symbolTable, transformationManager, termTransformer, context, prover); + } catch (InvalidConfigurationException e) { + throw new JavaSMTSolverException(e); + } + } } diff --git a/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolverManager.java b/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolverManager.java index dc2ab6e5dc..ed8f552cfc 100644 --- a/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolverManager.java +++ b/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolverManager.java @@ -18,12 +18,7 @@ import static com.google.common.base.Preconditions.checkArgument; import static com.google.common.base.Preconditions.checkState; -import hu.bme.mit.theta.solver.ItpSolver; -import hu.bme.mit.theta.solver.Solver; -import hu.bme.mit.theta.solver.SolverBase; -import hu.bme.mit.theta.solver.SolverFactory; -import hu.bme.mit.theta.solver.SolverManager; -import hu.bme.mit.theta.solver.UCSolver; +import hu.bme.mit.theta.solver.*; import java.util.HashSet; import java.util.Set; import java.util.regex.Pattern; @@ -98,5 +93,13 @@ public ItpSolver createItpSolver() { instantiatedSolvers.add(solver); return solver; } + + @Override + public HornSolver createHornSolver() { + checkState(!closed, "Solver manager was closed"); + final var solver = solverFactory.createHornSolver(); + instantiatedSolvers.add(solver); + return solver; + } } } diff --git a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericSmtLibHornSolver.java b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericSmtLibHornSolver.java index 96a23ab363..4b7dfe95c2 100644 --- a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericSmtLibHornSolver.java +++ b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericSmtLibHornSolver.java @@ -15,28 +15,19 @@ */ package hu.bme.mit.theta.solver.smtlib.impl.generic; -import static com.google.common.base.Preconditions.checkState; import static hu.bme.mit.theta.core.decl.Decls.Const; import static hu.bme.mit.theta.core.type.arraytype.ArrayExprs.Array; import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Bool; -import static hu.bme.mit.theta.core.type.booltype.BoolExprs.False; import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int; import static hu.bme.mit.theta.core.type.rattype.RatExprs.Rat; -import static hu.bme.mit.theta.core.utils.ExprUtils.extractFuncAndArgs; -import static hu.bme.mit.theta.core.utils.TypeUtils.cast; +import static hu.bme.mit.theta.solver.HornUtils.proofFromExpr; import com.google.common.collect.Lists; -import com.microsoft.z3.Z3Exception; -import hu.bme.mit.theta.core.type.Expr; import hu.bme.mit.theta.core.type.Type; -import hu.bme.mit.theta.core.type.anytype.RefExpr; -import hu.bme.mit.theta.core.type.booltype.BoolType; import hu.bme.mit.theta.core.type.bvtype.BvExprs; -import hu.bme.mit.theta.core.type.functype.FuncAppExpr; import hu.bme.mit.theta.core.type.functype.FuncType; import hu.bme.mit.theta.solver.HornSolver; import hu.bme.mit.theta.solver.ProofNode; -import hu.bme.mit.theta.solver.ProofNode.Builder; import hu.bme.mit.theta.solver.smtlib.dsl.gen.SMTLIBv2Parser.SortContext; import hu.bme.mit.theta.solver.smtlib.solver.SmtLibEnumStrategy; import hu.bme.mit.theta.solver.smtlib.solver.SmtLibSolver; @@ -117,61 +108,4 @@ public ProofNode getProof() { throw new AssertionError(); } } - - private ProofNode proofFromExpr(Expr proof) { - checkState(proof instanceof FuncAppExpr, "Proof must be a function application."); - int id = 0; - final Map, Integer> lookup = new LinkedHashMap<>(); - - final var args = extractFuncAndArgs((FuncAppExpr) proof).get2(); - - Deque> proofStack = new LinkedList<>(); - proofStack.push(args.get(0)); - lookup.put(args.get(0), id++); - - Expr root = cast(False(), Bool()); - final var rootBuilder = new ProofNode.Builder(root); - - Map visited = new LinkedHashMap<>(); - visited.put(lookup.get(args.get(0)), rootBuilder); - - while (!proofStack.isEmpty()) { - final var proofNodeExpr = proofStack.pop(); - if (!visited.containsKey(lookup.getOrDefault(proofNodeExpr, -1))) { - throw new Z3Exception("Node should exist in the graph nodes"); - } - final var proofNode = visited.get(lookup.get(proofNodeExpr)); - - if (proofNodeExpr instanceof FuncAppExpr funcAppExpr) { - final var nameAndArgs = extractFuncAndArgs(funcAppExpr); - if (nameAndArgs.get1() instanceof RefExpr refName - && refName.getDecl().getName().startsWith("hyper-res")) { - if (!nameAndArgs.get2().isEmpty()) { - for (int i = 1; i < nameAndArgs.get2().size() - 1; ++i) { - final var child = nameAndArgs.get2().get(i); - if (!visited.containsKey(lookup.getOrDefault(child, -1))) { - if (!lookup.containsKey(child)) { - lookup.put(child, id++); - } - visited.put( - lookup.get(child), new Builder(extractProofExpr(child))); - proofStack.push(child); - } - proofNode.addChild(visited.get(lookup.get(child))); - } - } - } - } - } - return rootBuilder.build(); - } - - private Expr extractProofExpr(Expr expr) { - checkState(expr instanceof FuncAppExpr, "Proof should be function application."); - final var nameAndArgs = extractFuncAndArgs((FuncAppExpr) expr); - final var args = nameAndArgs.get2(); - final var lastArg = args.get(args.size() - 1); - checkState(lastArg instanceof FuncAppExpr, "Proof should be function application."); - return (Expr) lastArg; - } } diff --git a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/SmtLibSolver.java b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/SmtLibSolver.java index d4fba45d1f..1b3decda93 100644 --- a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/SmtLibSolver.java +++ b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/SmtLibSolver.java @@ -16,29 +16,31 @@ package hu.bme.mit.theta.solver.smtlib.solver; import static com.google.common.base.Preconditions.checkState; - +import static hu.bme.mit.theta.core.decl.Decls.Const; +import static hu.bme.mit.theta.core.type.arraytype.ArrayExprs.Array; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Bool; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int; +import static hu.bme.mit.theta.core.type.rattype.RatExprs.Rat; +import static hu.bme.mit.theta.solver.HornUtils.proofFromExpr; + +import com.google.common.collect.Lists; import hu.bme.mit.theta.core.decl.ConstDecl; import hu.bme.mit.theta.core.model.Valuation; import hu.bme.mit.theta.core.type.Expr; import hu.bme.mit.theta.core.type.Type; import hu.bme.mit.theta.core.type.booltype.BoolType; +import hu.bme.mit.theta.core.type.bvtype.BvExprs; import hu.bme.mit.theta.core.type.enumtype.EnumType; +import hu.bme.mit.theta.core.type.functype.FuncType; import hu.bme.mit.theta.core.utils.ExprUtils; -import hu.bme.mit.theta.solver.Solver; -import hu.bme.mit.theta.solver.SolverStatus; -import hu.bme.mit.theta.solver.Stack; -import hu.bme.mit.theta.solver.UCSolver; -import hu.bme.mit.theta.solver.UnknownSolverStatusException; +import hu.bme.mit.theta.solver.*; import hu.bme.mit.theta.solver.impl.StackImpl; import hu.bme.mit.theta.solver.smtlib.dsl.gen.SMTLIBv2Lexer; import hu.bme.mit.theta.solver.smtlib.dsl.gen.SMTLIBv2Parser; import hu.bme.mit.theta.solver.smtlib.solver.binary.SmtLibSolverBinary; +import hu.bme.mit.theta.solver.smtlib.solver.model.SmtLibModel; import hu.bme.mit.theta.solver.smtlib.solver.model.SmtLibValuation; -import hu.bme.mit.theta.solver.smtlib.solver.parser.CheckSatResponse; -import hu.bme.mit.theta.solver.smtlib.solver.parser.GeneralResponse; -import hu.bme.mit.theta.solver.smtlib.solver.parser.GetModelResponse; -import hu.bme.mit.theta.solver.smtlib.solver.parser.GetUnsatCoreResponse; -import hu.bme.mit.theta.solver.smtlib.solver.parser.ThrowExceptionErrorListener; +import hu.bme.mit.theta.solver.smtlib.solver.parser.*; import hu.bme.mit.theta.solver.smtlib.solver.transformer.SmtLibSymbolTable; import hu.bme.mit.theta.solver.smtlib.solver.transformer.SmtLibTermTransformer; import hu.bme.mit.theta.solver.smtlib.solver.transformer.SmtLibTransformationManager; @@ -193,6 +195,55 @@ public void track(Expr assertion) { clearState(); } + private static Type transformSort(final SMTLIBv2Parser.SortContext ctx) { + final String name = ctx.identifier().symbol().getText(); + return switch (name) { + case "Int" -> Int(); + case "Bool" -> Bool(); + case "Real" -> Rat(); + case "BitVec" -> { + assert ctx.identifier().index().size() == 1; + yield BvExprs.BvType(Integer.parseInt(ctx.identifier().index().get(0).getText())); + } + case "Array" -> { + assert ctx.sort().size() == 2; + yield Array(transformSort(ctx.sort().get(0)), transformSort(ctx.sort().get(1))); + } + default -> throw new UnsupportedOperationException(); + }; + } + + @Override + public ProofNode getProof() { + + solverBinary.issueCommand("(get-proof)"); + var response = solverBinary.readResponse(); + final var res = parseResponse(response); + if (res.isError()) { + throw new SmtLibSolverException(res.getReason()); + } else if (res.isSpecific()) { + final GetProofResponse getModelResponse = res.asSpecific().asGetProofResponse(); + getModelResponse + .getFunDeclarations() + .forEach( + (name, def) -> { + var type = transformSort(def.get2()); + for (SMTLIBv2Parser.SortContext s : Lists.reverse(def.get1())) { + type = FuncType.of(transformSort(s), type); + } + symbolTable.put(Const(name, type), name, def.get3()); + }); + final var proof = + termTransformer.toExpr( + getModelResponse.getProof(), + Bool(), + new SmtLibModel(Collections.emptyMap())); + return proofFromExpr(proof); + } else { + throw new AssertionError(); + } + } + @Override public SolverStatus check() { solverBinary.issueCommand("(check-sat)"); diff --git a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/utils/SmtLibTermLogger.kt b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/utils/SmtLibTermLogger.kt new file mode 100644 index 0000000000..f731431728 --- /dev/null +++ b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/utils/SmtLibTermLogger.kt @@ -0,0 +1,101 @@ +/* + * 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.solver.smtlib.utils + +import hu.bme.mit.theta.solver.* +import hu.bme.mit.theta.solver.logger.TermLogger +import hu.bme.mit.theta.solver.smtlib.impl.generic.GenericSmtLibHornSolver +import hu.bme.mit.theta.solver.smtlib.impl.generic.GenericSmtLibSymbolTable +import hu.bme.mit.theta.solver.smtlib.impl.generic.GenericSmtLibTermTransformer +import hu.bme.mit.theta.solver.smtlib.impl.generic.GenericSmtLibTransformationManager +import hu.bme.mit.theta.solver.smtlib.impl.mathsat.MathSATSmtLibItpSolver +import hu.bme.mit.theta.solver.smtlib.solver.SmtLibItpSolver +import hu.bme.mit.theta.solver.smtlib.solver.SmtLibSolver +import hu.bme.mit.theta.solver.smtlib.solver.binary.SmtLibSolverBinary +import java.io.File + +class SmtLibTermLogger(val filePrefix: String) : TermLogger { + + private val solver: () -> SmtLibSolver + private val ucSolver: () -> SmtLibSolver + private val itpSolver: () -> SmtLibItpSolver<*> + private val hornSolver: () -> GenericSmtLibHornSolver + private lateinit var cachedSolver: SmtLibSolver + private lateinit var cachedUcSolver: SmtLibSolver + private lateinit var cachedItpSolver: SmtLibItpSolver<*> + private lateinit var cachedHornSolver: GenericSmtLibHornSolver + + private val loggerBinary: SmtLibSolverBinary + + private var idx = 0 + private var activeFile: File + + init { + activeFile = File("$filePrefix${idx++}.smt2") + activeFile.delete() + + val symbolTable = GenericSmtLibSymbolTable() + val transformationManager = GenericSmtLibTransformationManager(symbolTable) + val termTransformer = GenericSmtLibTermTransformer(symbolTable) + loggerBinary = LoggerBinary() + solver = { + SmtLibSolver(symbolTable, transformationManager, termTransformer, loggerBinary, false) + } + ucSolver = { + SmtLibSolver(symbolTable, transformationManager, termTransformer, loggerBinary, false) + } + itpSolver = { + MathSATSmtLibItpSolver(symbolTable, transformationManager, termTransformer, loggerBinary) + } + hornSolver = { + GenericSmtLibHornSolver(symbolTable, transformationManager, termTransformer, loggerBinary) + } + } + + private inner class LoggerBinary : SmtLibSolverBinary { + + override fun issueCommand(command: String) { + activeFile.appendText(command) + activeFile.appendText(System.lineSeparator()) + } + + override fun readResponse(): String { + return "success" + } + + override fun close() {} + } + + override fun getSolver(): Solver = + if (this::cachedSolver.isInitialized) cachedSolver else solver().also { cachedSolver = it } + + override fun getUCSolver(): UCSolver = + if (this::cachedUcSolver.isInitialized) cachedUcSolver + else ucSolver().also { cachedUcSolver = it } + + override fun getHornSolver(): HornSolver = + if (this::cachedHornSolver.isInitialized) cachedHornSolver + else hornSolver().also { cachedHornSolver = it } + + override fun getItpSolver(): ItpSolver = + if (this::cachedItpSolver.isInitialized) cachedItpSolver + else itpSolver().also { cachedItpSolver = it } + + override fun endCurrentFile() { + activeFile = File("$filePrefix${idx++}.smt2") + activeFile.delete() + } +} diff --git a/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3HornSolver.java b/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3HornSolver.java index 874f39980d..cdf7776799 100644 --- a/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3HornSolver.java +++ b/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3HornSolver.java @@ -50,6 +50,11 @@ public Z3HornSolver( Context z3Context, Solver z3Solver) { super(symbolTable, transformationManager, termTransformer, z3Context, z3Solver); + final var params = z3Context.mkParams(); + params.add("fp.xform.slice", true); + params.add("fp.xform.inline_linear", false); + params.add("fp.xform.inline_eager", false); + z3Solver.setParameters(params); } //// diff --git a/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/HornUtils.java b/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/HornUtils.java new file mode 100644 index 0000000000..b6721159e1 --- /dev/null +++ b/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/HornUtils.java @@ -0,0 +1,93 @@ +/* + * 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.solver; + +import static com.google.common.base.Preconditions.checkState; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Bool; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.False; +import static hu.bme.mit.theta.core.utils.ExprUtils.extractFuncAndArgs; +import static hu.bme.mit.theta.core.utils.TypeUtils.cast; + +import com.microsoft.z3.Z3Exception; +import hu.bme.mit.theta.core.type.Expr; +import hu.bme.mit.theta.core.type.anytype.RefExpr; +import hu.bme.mit.theta.core.type.booltype.BoolType; +import hu.bme.mit.theta.core.type.functype.FuncAppExpr; +import java.util.Deque; +import java.util.LinkedHashMap; +import java.util.LinkedList; +import java.util.Map; + +public class HornUtils { + + public static ProofNode proofFromExpr(Expr proof) { + checkState(proof instanceof FuncAppExpr, "Proof must be a function application."); + int id = 0; + final Map, Integer> lookup = new LinkedHashMap<>(); + + final var args = extractFuncAndArgs((FuncAppExpr) proof).get2(); + + Deque> proofStack = new LinkedList<>(); + proofStack.push(args.get(0)); + lookup.put(args.get(0), id++); + + Expr root = cast(False(), Bool()); + final var rootBuilder = new ProofNode.Builder(root); + + Map visited = new LinkedHashMap<>(); + visited.put(lookup.get(args.get(0)), rootBuilder); + + while (!proofStack.isEmpty()) { + final var proofNodeExpr = proofStack.pop(); + if (!visited.containsKey(lookup.getOrDefault(proofNodeExpr, -1))) { + throw new Z3Exception("Node should exist in the graph nodes"); + } + final var proofNode = visited.get(lookup.get(proofNodeExpr)); + + if (proofNodeExpr instanceof FuncAppExpr funcAppExpr) { + final var nameAndArgs = extractFuncAndArgs(funcAppExpr); + if (nameAndArgs.get1() instanceof RefExpr refName + && refName.getDecl().getName().startsWith("hyper-res")) { + if (!nameAndArgs.get2().isEmpty()) { + for (int i = 1; i < nameAndArgs.get2().size() - 1; ++i) { + final var child = nameAndArgs.get2().get(i); + if (!visited.containsKey(lookup.getOrDefault(child, -1))) { + if (!lookup.containsKey(child)) { + lookup.put(child, id++); + } + visited.put( + lookup.get(child), + new ProofNode.Builder(extractProofExpr(child))); + proofStack.push(child); + } + proofNode.addChild(visited.get(lookup.get(child))); + } + } + } + } + } + return rootBuilder.build(); + } + + public static Expr extractProofExpr(Expr expr) { + checkState(expr instanceof FuncAppExpr, "Proof should be function application."); + final var nameAndArgs = extractFuncAndArgs((FuncAppExpr) expr); + final var args = nameAndArgs.get2(); + final var lastArg = args.get(args.size() - 1); + checkState(lastArg instanceof FuncAppExpr, "Proof should be function application."); + return (Expr) lastArg; + } +} diff --git a/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/Solver.java b/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/Solver.java index 8f97d1d21e..31cd605faf 100644 --- a/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/Solver.java +++ b/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/Solver.java @@ -46,4 +46,8 @@ default void add(final Iterable> assertions) { add(assertion); } } + + default ProofNode getProof() { + throw new UnsupportedOperationException("Cannot get proof"); + } } diff --git a/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/logger/SolverLoggerWrapper.java b/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/logger/SolverLoggerWrapper.java new file mode 100644 index 0000000000..cff3786def --- /dev/null +++ b/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/logger/SolverLoggerWrapper.java @@ -0,0 +1,341 @@ +/* + * 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.solver.logger; + +import hu.bme.mit.theta.core.Relation; +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.solver.*; +import java.util.Collection; +import java.util.List; +import java.util.Set; + +/** Records solver calls. Use whenToSave to direct when to persist the calls to file. */ +public final class SolverLoggerWrapper implements Solver, UCSolver, ItpSolver, HornSolver { + private final SolverBase solverBase; + private final TermLogger termLogger; + private final Set whenToSave; + + public SolverLoggerWrapper( + SolverBase solverBase, TermLogger termLogger, Set whenToSave) { + this.solverBase = solverBase; + this.termLogger = termLogger; + this.whenToSave = whenToSave; + } + + public enum SaveStrategy { + ON_ADD, + ON_POP, + ON_CHECK, /* check, get unsat core, interpolate, etc */ + ON_RESET, + } + + private void save(SaveStrategy saveStrategy) { + if (saveStrategy != null && whenToSave.contains(saveStrategy)) { + termLogger.endCurrentFile(); + } + } + + // Solver + @Override + public void add(Expr assertion) { + if (solverBase instanceof Solver solver) { + termLogger.getSolver().add(assertion); + save(SaveStrategy.ON_ADD); + solver.add(assertion); + } + } + + @Override + public void add(Iterable> assertions) { + if (solverBase instanceof Solver solver) { + termLogger.getSolver().add(assertions); + save(SaveStrategy.ON_ADD); + solver.add(assertions); + } + } + + // UCSolver + + @Override + public void track(Expr assertion) { + if (solverBase instanceof UCSolver ucSolver) { + termLogger.getUCSolver().track(assertion); + save(SaveStrategy.ON_ADD); + ucSolver.track(assertion); + } + } + + @Override + public void track(Iterable> assertions) { + if (solverBase instanceof UCSolver ucSolver) { + termLogger.getUCSolver().track(assertions); + save(SaveStrategy.ON_ADD); + ucSolver.track(assertions); + } + } + + @Override + public Collection> getUnsatCore() { + if (solverBase instanceof UCSolver ucSolver) { + try { + termLogger.getUCSolver().getUnsatCore(); + } catch (Throwable ignored) { + + } + save(SaveStrategy.ON_CHECK); + return ucSolver.getUnsatCore(); + } + return null; + } + + // ItpSolver + + @Override + public ItpPattern createBinPattern(ItpMarker markerA, ItpMarker markerB) { + if (solverBase instanceof ItpSolver itpSolver) { + try { + termLogger.getItpSolver().createBinPattern(markerA, markerB); + } catch (Throwable ignored) { + + } + return itpSolver.createBinPattern(markerA, markerB); + } + return null; + } + + @Override + public ItpPattern createSeqPattern(List markers) { + if (solverBase instanceof ItpSolver itpSolver) { + try { + termLogger.getItpSolver().createSeqPattern(markers); + } catch (Throwable ignored) { + + } + return itpSolver.createSeqPattern(markers); + } + return null; + } + + @Override + public ItpPattern createTreePattern(ItpMarkerTree root) { + if (solverBase instanceof ItpSolver itpSolver) { + try { + termLogger.getItpSolver().createTreePattern(root); + } catch (Throwable ignored) { + + } + return itpSolver.createTreePattern(root); + } + return null; + } + + @Override + public ItpMarker createMarker() { + if (solverBase instanceof ItpSolver itpSolver) { + try { + termLogger.getItpSolver().createMarker(); + } catch (Throwable ignored) { + + } + return itpSolver.createMarker(); + } + return null; + } + + @Override + public void add(ItpMarker marker, Expr assertion) { + if (solverBase instanceof ItpSolver itpSolver) { + termLogger.getItpSolver().add(marker, assertion); + save(SaveStrategy.ON_ADD); + itpSolver.add(marker, assertion); + } + } + + @Override + public void add(ItpMarker marker, Iterable> assertions) { + if (solverBase instanceof ItpSolver itpSolver) { + termLogger.getItpSolver().add(marker, assertions); + save(SaveStrategy.ON_ADD); + itpSolver.add(marker, assertions); + } + } + + @Override + public Interpolant getInterpolant(ItpPattern pattern) { + if (solverBase instanceof ItpSolver itpSolver) { + try { + termLogger.getItpSolver().getInterpolant(pattern); + } catch (Throwable ignored) { + + } + save(SaveStrategy.ON_CHECK); + return itpSolver.getInterpolant(pattern); + } + return null; + } + + @Override + public Collection getMarkers() { + if (solverBase instanceof ItpSolver itpSolver) { + try { + termLogger.getItpSolver().getMarkers(); + } catch (Throwable ignored) { + + } + return itpSolver.getMarkers(); + } + return null; + } + + // HornSolver + + @Override + public void add(Relation relation) { + if (solverBase instanceof HornSolver hornSolver) { + termLogger.getHornSolver().add(relation); + save(SaveStrategy.ON_ADD); + hornSolver.add(relation); + } + } + + @Override + public void add(Collection relations) { + if (solverBase instanceof HornSolver hornSolver) { + termLogger.getHornSolver().add(relations); + save(SaveStrategy.ON_ADD); + hornSolver.add(relations); + } + } + + @Override + public ProofNode getProof() { + if (solverBase instanceof HornSolver hornSolver) { + try { + termLogger.getHornSolver().getProof(); + } catch (Throwable ignored) { + + } + save(SaveStrategy.ON_CHECK); + return hornSolver.getProof(); + } else if (solverBase instanceof Solver solver) { + try { + termLogger.getSolver().getProof(); + } catch (Throwable ignored) { + + } + save(SaveStrategy.ON_CHECK); + return solver.getProof(); + } + return null; + } + + // SolverBase + + @Override + public SolverStatus check() { + try { + if (solverBase instanceof HornSolver) { + termLogger.getHornSolver().check(); + } else if (solverBase instanceof Solver) { + termLogger.getSolver().check(); + } else if (solverBase instanceof UCSolver) { + termLogger.getUCSolver().check(); + } else if (solverBase instanceof ItpSolver) { + termLogger.getItpSolver().check(); + } + } catch (Throwable ignored) { + + } + save(SaveStrategy.ON_CHECK); + return solverBase.check(); + } + + @Override + public void push() { + try { + if (solverBase instanceof HornSolver) { + termLogger.getHornSolver().push(); + } else if (solverBase instanceof Solver) { + termLogger.getSolver().push(); + } else if (solverBase instanceof UCSolver) { + termLogger.getUCSolver().push(); + } else if (solverBase instanceof ItpSolver) { + termLogger.getItpSolver().push(); + } + } catch (Throwable ignored) { + + } + solverBase.push(); + } + + @Override + public void pop(int n) { + try { + if (solverBase instanceof HornSolver) { + termLogger.getHornSolver().pop(n); + } else if (solverBase instanceof Solver) { + termLogger.getSolver().pop(n); + } else if (solverBase instanceof UCSolver) { + termLogger.getUCSolver().pop(n); + } else if (solverBase instanceof ItpSolver) { + termLogger.getItpSolver().pop(n); + } + } catch (Throwable ignored) { + + } + save(SaveStrategy.ON_POP); + solverBase.pop(n); + } + + @Override + public void reset() { + try { + if (solverBase instanceof HornSolver) { + termLogger.getHornSolver().reset(); + } else if (solverBase instanceof Solver) { + termLogger.getSolver().reset(); + } else if (solverBase instanceof UCSolver) { + termLogger.getUCSolver().reset(); + } else if (solverBase instanceof ItpSolver) { + termLogger.getItpSolver().reset(); + } + } catch (Throwable ignored) { + + } + save(SaveStrategy.ON_RESET); + solverBase.reset(); + } + + @Override + public SolverStatus getStatus() { + return solverBase.getStatus(); + } + + @Override + public Valuation getModel() { + return solverBase.getModel(); + } + + @Override + public Collection> getAssertions() { + return solverBase.getAssertions(); + } + + @Override + public void close() throws Exception {} +} diff --git a/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/logger/SolverLoggerWrapperFactory.java b/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/logger/SolverLoggerWrapperFactory.java new file mode 100644 index 0000000000..88c4e5cfae --- /dev/null +++ b/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/logger/SolverLoggerWrapperFactory.java @@ -0,0 +1,91 @@ +/* + * 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.solver.logger; + +import hu.bme.mit.theta.solver.*; +import java.util.Set; + +public final class SolverLoggerWrapperFactory implements SolverFactory { + + private final String solverName; + private final TermLogger termLogger; + private final Set whenToSave; + + public SolverLoggerWrapperFactory( + String solverName, + TermLogger termLogger, + Set whenToSave) { + this.solverName = solverName; + this.termLogger = termLogger; + this.whenToSave = whenToSave; + } + + @Override + public Solver createSolver() { + try { + return new SolverLoggerWrapper( + SolverManager.resolveSolverFactory(solverName).createSolver(), + termLogger, + whenToSave); + + } catch (Exception e) { + e.printStackTrace(); + throw new UnsupportedOperationException("Logging solver could not be created"); + } + } + + @Override + public UCSolver createUCSolver() { + try { + return new SolverLoggerWrapper( + SolverManager.resolveSolverFactory(solverName).createUCSolver(), + termLogger, + whenToSave); + + } catch (Exception e) { + e.printStackTrace(); + throw new UnsupportedOperationException("Logging solver could not be created"); + } + } + + @Override + public ItpSolver createItpSolver() { + try { + return new SolverLoggerWrapper( + SolverManager.resolveSolverFactory(solverName).createItpSolver(), + termLogger, + whenToSave); + + } catch (Exception e) { + e.printStackTrace(); + throw new UnsupportedOperationException("Logging solver could not be created"); + } + } + + @Override + public HornSolver createHornSolver() { + try { + return new SolverLoggerWrapper( + SolverManager.resolveSolverFactory(solverName).createHornSolver(), + termLogger, + whenToSave); + + } catch (Exception e) { + e.printStackTrace(); + throw new UnsupportedOperationException("Logging solver could not be created"); + } + } +} diff --git a/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/logger/TermLogger.java b/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/logger/TermLogger.java new file mode 100644 index 0000000000..7ab8d00017 --- /dev/null +++ b/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/logger/TermLogger.java @@ -0,0 +1,30 @@ +/* + * 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.solver.logger; + +import hu.bme.mit.theta.solver.*; + +public interface TermLogger { + Solver getSolver(); + + UCSolver getUCSolver(); + + HornSolver getHornSolver(); + + ItpSolver getItpSolver(); + + void endCurrentFile(); +} diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToCegarChecker.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToCegarChecker.kt index 37bd0904c8..8079566b80 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToCegarChecker.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToCegarChecker.kt @@ -39,6 +39,7 @@ import hu.bme.mit.theta.solver.SolverFactory import hu.bme.mit.theta.xcfa.analysis.* import hu.bme.mit.theta.xcfa.analysis.por.XcfaDporLts import hu.bme.mit.theta.xcfa.cli.params.* +import hu.bme.mit.theta.xcfa.cli.params.Refinement.* import hu.bme.mit.theta.xcfa.cli.utils.getSolver import hu.bme.mit.theta.xcfa.dereferences import hu.bme.mit.theta.xcfa.model.XCFA @@ -112,13 +113,22 @@ fun getCegarChecker( cegarConfig.refinerConfig.refinement.refiner(refinementSolverFactory, cegarConfig.cexMonitor) as ExprTraceChecker val precRefiner: PrecRefiner = - cegarConfig.abstractorConfig.domain.itpPrecRefiner( - cegarConfig.refinerConfig.exprSplitter.exprSplitter - ) as PrecRefiner + when (cegarConfig.refinerConfig.refinement) { + UNSAT_CORE, + PROOF -> + cegarConfig.abstractorConfig.domain.varPrecRefiner( + cegarConfig.refinerConfig.exprSplitter.exprSplitter + ) + else -> + cegarConfig.abstractorConfig.domain.itpPrecRefiner( + cegarConfig.refinerConfig.exprSplitter.exprSplitter + ) + } + as PrecRefiner val atomicNodePruner: NodePruner = cegarConfig.abstractorConfig.domain.nodePruner as NodePruner val refiner: ArgRefiner = - if (cegarConfig.refinerConfig.refinement == Refinement.MULTI_SEQ) + if (cegarConfig.refinerConfig.refinement == MULTI_SEQ) if (cegarConfig.porLevel == POR.AASPOR) MultiExprTraceRefiner.create( ref, diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/ParamValues.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/ParamValues.kt index a945a0c05b..2879861ba0 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/ParamValues.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/ParamValues.kt @@ -28,15 +28,13 @@ import hu.bme.mit.theta.analysis.algorithm.cegar.abstractor.StopCriterions import hu.bme.mit.theta.analysis.expl.ExplPrec import hu.bme.mit.theta.analysis.expl.ExplState import hu.bme.mit.theta.analysis.expl.ItpRefToExplPrec +import hu.bme.mit.theta.analysis.expl.VarsRefToExplPrec import hu.bme.mit.theta.analysis.expr.ExprAction import hu.bme.mit.theta.analysis.expr.ExprState import hu.bme.mit.theta.analysis.expr.refinement.* import hu.bme.mit.theta.analysis.pred.* import hu.bme.mit.theta.analysis.pred.ExprSplitters.ExprSplitter -import hu.bme.mit.theta.analysis.ptr.ItpRefToPtrPrec -import hu.bme.mit.theta.analysis.ptr.PtrPrec -import hu.bme.mit.theta.analysis.ptr.PtrState -import hu.bme.mit.theta.analysis.ptr.getPtrPartialOrd +import hu.bme.mit.theta.analysis.ptr.* import hu.bme.mit.theta.analysis.waitlist.Waitlist import hu.bme.mit.theta.common.logging.Logger import hu.bme.mit.theta.core.decl.VarDecl @@ -126,6 +124,16 @@ enum class Domain( out Prec, out Refutation, >, + val varPrecRefiner: + (exprSplitter: ExprSplitter) -> PrecRefiner< + out ExprState, + out ExprAction, + out Prec, + out Refutation, + >? = + { + null + }, val initPrec: (XCFA, InitPrec) -> XcfaPrec>, val partialOrd: (Solver) -> PartialOrd>, val nodePruner: NodePruner, @@ -148,6 +156,11 @@ enum class Domain( ItpRefToPtrPrec(ItpRefToExplPrec()) ) }, + varPrecRefiner = { + XcfaPrecRefiner, ExplPrec, VarsRefutation>( + VarRefToPtrPrec(VarsRefToExplPrec()) + ) + }, initPrec = { x, ip -> ip.explPrec(x) }, partialOrd = { PartialOrd { s1, s2 -> s1.isLeq(s2) }.getPtrPartialOrd() }, nodePruner = AtomicNodePruner>, XcfaAction>(), @@ -275,6 +288,12 @@ enum class Refinement( }, stopCriterion = StopCriterions.firstCex(), ), + PROOF( + refiner = { s, _ -> + ExprTraceProofChecker.create(BoolExprs.True(), BoolExprs.True(), s.createSolver()) + }, + stopCriterion = StopCriterions.firstCex(), + ), UCB( refiner = { s, _ -> ExprTraceUCBChecker.create(BoolExprs.True(), BoolExprs.True(), s.createUCSolver()) diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/SolverRegistration.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/SolverRegistration.kt index d455f425c3..df832393c6 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/SolverRegistration.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/SolverRegistration.kt @@ -19,14 +19,25 @@ import hu.bme.mit.theta.common.logging.Logger import hu.bme.mit.theta.solver.SolverFactory import hu.bme.mit.theta.solver.SolverManager import hu.bme.mit.theta.solver.javasmt.JavaSMTSolverManager +import hu.bme.mit.theta.solver.logger.SolverLoggerWrapper +import hu.bme.mit.theta.solver.logger.SolverLoggerWrapperFactory import hu.bme.mit.theta.solver.smtlib.SmtLibSolverManager +import hu.bme.mit.theta.solver.smtlib.utils.SmtLibTermLogger import hu.bme.mit.theta.solver.validator.SolverValidatorWrapperFactory import hu.bme.mit.theta.solver.z3legacy.Z3SolverManager import java.nio.file.Path -fun getSolver(name: String, validate: Boolean): SolverFactory = +var idx = 0 + +fun getSolver(name: String, validate: Boolean, log: Boolean = true): SolverFactory = if (validate) { SolverValidatorWrapperFactory.create(name) + } else if (log) { + SolverLoggerWrapperFactory( + name, + SmtLibTermLogger("smtlib_${idx++}_"), + setOf(SolverLoggerWrapper.SaveStrategy.ON_RESET), + ) } else { SolverManager.resolveSolverFactory(name) } diff --git a/subprojects/xcfa/xcfa2chc/src/main/java/hu/bme/mit/theta/xcfa2chc/Xcfa2Chc.kt b/subprojects/xcfa/xcfa2chc/src/main/java/hu/bme/mit/theta/xcfa2chc/Xcfa2Chc.kt index 26c52f6553..458291b0b8 100644 --- a/subprojects/xcfa/xcfa2chc/src/main/java/hu/bme/mit/theta/xcfa2chc/Xcfa2Chc.kt +++ b/subprojects/xcfa/xcfa2chc/src/main/java/hu/bme/mit/theta/xcfa2chc/Xcfa2Chc.kt @@ -67,9 +67,9 @@ fun XcfaProcedure.toCHC( } val types = vars.map { it.type }.toTypedArray() - val oldParams = vars.associateWith { Param("|" + it.name + "|", it.type) } + val oldParams = vars.associateWith { Param(it.name, it.type) } val oldParamList = vars.map { oldParams[it]!!.ref }.toTypedArray() - val newParams = vars.associateWith { Param("|" + it.name + "_new|", it.type) } + val newParams = vars.associateWith { Param(it.name + "_new", it.type) } val ufs = locs.associateWith { Relation(it.name, *types) }