diff --git a/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java b/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java index 88f3008b0e..91cb67ff7d 100644 --- a/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java +++ b/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java @@ -16,6 +16,7 @@ import java.util.Optional; import org.checkerframework.checker.nullness.qual.Nullable; import org.sosy_lab.java_smt.api.SolverContext.ProverOptions; +import org.sosy_lab.java_smt.api.proofs.Proof; /** * Super interface for {@link ProverEnvironment} and {@link InterpolatingProverEnvironment} that @@ -160,6 +161,13 @@ default ImmutableMap getStatistics() { return ImmutableMap.of(); } + /** + * Get proof of unsatisfiability of the conjuction of the current satck of all formulas. This + * method should be called only immediately after an {@link #isUnsat()} call that returned + * true. + */ + Proof getProof() throws SolverException, InterruptedException; + /** * Closes the prover environment. The object should be discarded, and should not be used after * closing. The first call of this method will close the prover instance, further calls are diff --git a/src/org/sosy_lab/java_smt/api/SolverContext.java b/src/org/sosy_lab/java_smt/api/SolverContext.java index 3fbd476c77..574dd6b2be 100644 --- a/src/org/sosy_lab/java_smt/api/SolverContext.java +++ b/src/org/sosy_lab/java_smt/api/SolverContext.java @@ -52,6 +52,9 @@ enum ProverOptions { */ GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS, + /** Whether the solver should generate proofs for unsatisfiable formulas. */ + GENERATE_PROOFS, + /** Whether the solver should enable support for formulae build in SL theory. */ ENABLE_SEPARATION_LOGIC } diff --git a/src/org/sosy_lab/java_smt/api/proofs/Proof.java b/src/org/sosy_lab/java_smt/api/proofs/Proof.java new file mode 100644 index 0000000000..0df15c7c57 --- /dev/null +++ b/src/org/sosy_lab/java_smt/api/proofs/Proof.java @@ -0,0 +1,26 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2026 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.api.proofs; + +/** + * This class provides a proof of unsatisifabilty for a given query. It allows the retrieval of the + * root proof node in the proof DAG. + */ +public interface Proof { + + /** + * Returns the root proof node of the DAG from this proof. + * + * @return an object of type {@link ProofNode} the root proof node. + * @see ProofNode + */ + ProofNode getProofRoot(); +} diff --git a/src/org/sosy_lab/java_smt/api/proofs/ProofNode.java b/src/org/sosy_lab/java_smt/api/proofs/ProofNode.java new file mode 100644 index 0000000000..331c49035a --- /dev/null +++ b/src/org/sosy_lab/java_smt/api/proofs/ProofNode.java @@ -0,0 +1,43 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2026 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.api.proofs; + +import com.google.common.collect.ImmutableSet; +import java.util.Optional; +import org.sosy_lab.java_smt.api.Formula; + +/** A proof node in the proof DAG of a proof. */ +public interface ProofNode { + + /** Get the children of the proof node. */ + ImmutableSet getChildren(); + + /** + * Check if the proof node is a leaf. + * + * @return True if the proof node is a leaf, false otherwise. + */ + boolean isLeaf(); + + /** + * Get the formula of the proof node. + * + * @return The formula of the proof node. + */ + Optional getFormula(); + + /** + * Get the rule of the proof node. + * + * @return The rule of the proof node. + */ + ProofRule getRule(); +} diff --git a/src/org/sosy_lab/java_smt/api/proofs/ProofRule.java b/src/org/sosy_lab/java_smt/api/proofs/ProofRule.java new file mode 100644 index 0000000000..5d50d69538 --- /dev/null +++ b/src/org/sosy_lab/java_smt/api/proofs/ProofRule.java @@ -0,0 +1,31 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2026 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.api.proofs; + +/** + * A proof rule from a given proof format. E.g.: + * + *

CVC5 currently uses many rules in its calculus for proving unsatisfiability. Through its API + * one can retrieve a rule in form of an enum. See: ... + * Note: Other solvers may return just a String, the name of the rule applied. + * + *

We can look at RESOLUTION: Given two nodes viewed as clauses C_1 and C_2, as well as the pivot + * which is a literal occurring in C_1 and C_2 (positively and negatively or the other way around) + * and its polarity, it produces C which "is a clause resulting from collecting all the literals in + * C_1, minus the first occurrence of the pivot or its negation, and C_2, minus the first occurrence + * of the pivot or its negation, according to the policy above". See the link given earlier. + */ +public interface ProofRule { + + /** Get the name of the proof rule. */ + String getName(); +} diff --git a/src/org/sosy_lab/java_smt/api/proofs/package-info.java b/src/org/sosy_lab/java_smt/api/proofs/package-info.java new file mode 100644 index 0000000000..96e316567b --- /dev/null +++ b/src/org/sosy_lab/java_smt/api/proofs/package-info.java @@ -0,0 +1,14 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2026 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ +/** + * This package is meant to provide abstract classes and interfaces that are inherited and used all + * over to process proofs from the solvers. + */ +package org.sosy_lab.java_smt.api.proofs; diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractProof.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractProof.java new file mode 100644 index 0000000000..7a346722ea --- /dev/null +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProof.java @@ -0,0 +1,28 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2026 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.basicimpl; + +import java.util.Objects; +import org.sosy_lab.java_smt.api.proofs.Proof; +import org.sosy_lab.java_smt.api.proofs.ProofNode; + +public abstract class AbstractProof implements Proof { + private final ProofNode root; + + public AbstractProof(ProofNode pRoot) { + root = Objects.requireNonNull(pRoot); + } + + @Override + public ProofNode getProofRoot() { + return root; + } +} diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractProofNode.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractProofNode.java new file mode 100644 index 0000000000..1c69e4f5a0 --- /dev/null +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProofNode.java @@ -0,0 +1,132 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2026 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.basicimpl; + +import com.google.common.collect.ImmutableSet; +import java.util.LinkedHashSet; +import java.util.Optional; +import java.util.Set; +import org.checkerframework.checker.nullness.qual.Nullable; +import org.sosy_lab.java_smt.api.Formula; +import org.sosy_lab.java_smt.api.proofs.ProofNode; +import org.sosy_lab.java_smt.api.proofs.ProofRule; + +/** + * A proof DAG of a proof. + * + * @author Gabriel Carpio + */ +public abstract class AbstractProofNode implements ProofNode { + + private ImmutableSet children = ImmutableSet.of(); + private ProofRule rule; + protected Optional formula = Optional.empty(); + + protected AbstractProofNode(ProofRule pRule, @Nullable Formula pFormula) { + this.rule = pRule; + this.formula = Optional.ofNullable(pFormula); + } + + @Override + public Optional getFormula() { + return this.formula; + } + + @Override + public ImmutableSet getChildren() { + return this.children; + } + + protected void addChild(ProofNode pChild) { + Set tempChildren = new LinkedHashSet<>(this.children); + tempChildren.add(pChild); + this.children = ImmutableSet.copyOf(tempChildren); + } + + @Override + public ProofRule getRule() { + return rule; + } + + @Override + public boolean isLeaf() { + return getChildren().isEmpty(); + } + + /** + * This method gibes the proof back as a formatted string. It is meant to have a readable proof + * for debugging purposes. + */ + public String proofAsString() { + return proofAsString(0); + } + + protected String proofAsString(int pIndentLevel) { + StringBuilder sb = new StringBuilder(); + String indent = " ".repeat(pIndentLevel); + + String sFormula = getFormula().map(Object::toString).orElse("null"); + + sb.append(indent).append("Formula: ").append(sFormula).append("\n"); + sb.append(indent).append("Rule: ").append(getRule().getName()).append("\n"); + sb.append(indent) + .append("No. Children: ") + .append(this.isLeaf() ? 0 : getChildren().size()) + .append("\n"); + sb.append(indent).append("leaf: ").append(isLeaf()).append("\n"); + + int i = 0; + if (!isLeaf()) { + for (ProofNode child : getChildren()) { + sb.append(indent).append("Child ").append(++i).append(":\n"); + sb.append(((AbstractProofNode) child).proofAsString(pIndentLevel + 1)); + } + } + + return sb.toString(); + } + + protected abstract static class ProofFrame { + final T proof; + int numArgs = 0; + boolean visited; + + protected ProofFrame(T pProof) { + this.proof = pProof; + this.visited = false; + } + + /** Get the proof object. */ + public T getProof() { + return proof; + } + + /** Get the number of arguments the proof object has. */ + public int getNumArgs() { + return numArgs; + } + + /** Check if the frame has been visited. */ + public boolean isVisited() { + return visited; + } + + /** Set the frame as visited. */ + public void setAsVisited() { + this.visited = true; + } + + /** Set the number of arguments the proof object has. */ + public void setNumArgs(int pNumArgs) { + this.numArgs = pNumArgs; + } + } +} diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java index 76523447d1..476a01996c 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java @@ -32,6 +32,7 @@ import org.sosy_lab.java_smt.api.OptimizationProverEnvironment.OptStatus; import org.sosy_lab.java_smt.api.SolverContext.ProverOptions; import org.sosy_lab.java_smt.api.SolverException; +import org.sosy_lab.java_smt.api.proofs.Proof; public abstract class AbstractProver implements BasicProverEnvironment { @@ -40,6 +41,7 @@ public abstract class AbstractProver implements BasicProverEnvironment { protected final boolean generateAllSat; protected final boolean generateUnsatCores; private final boolean generateUnsatCoresOverAssumptions; + protected final boolean generateProofs; protected final boolean enableSL; // flags for status @@ -64,6 +66,7 @@ protected AbstractProver(Set pOptions) { generateUnsatCores = pOptions.contains(ProverOptions.GENERATE_UNSAT_CORE); generateUnsatCoresOverAssumptions = pOptions.contains(ProverOptions.GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS); + generateProofs = pOptions.contains(ProverOptions.GENERATE_PROOFS); enableSL = pOptions.contains(ProverOptions.ENABLE_SEPARATION_LOGIC); assertedFormulas.add(LinkedHashMultimap.create()); @@ -97,6 +100,13 @@ protected final void checkGenerateUnsatCoresOverAssumptions() { Preconditions.checkState(!wasLastSatCheckSatisfiable); } + protected final void checkGenerateProofs() { + Preconditions.checkState(generateProofs, TEMPLATE, ProverOptions.GENERATE_PROOFS); + Preconditions.checkState(!closed); + Preconditions.checkState(!changedSinceLastSatQuery); + Preconditions.checkState(!wasLastSatCheckSatisfiable); + } + protected final void checkGenerateInterpolants() { Preconditions.checkState(!closed); Preconditions.checkState( @@ -276,4 +286,10 @@ public void close() { closeAllEvaluators(); closed = true; } + + @Override + public Proof getProof() throws InterruptedException, SolverException { + throw new UnsupportedOperationException( + "ProofNode generation is not available for the current solver."); + } } diff --git a/src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/BasicProverWithAssumptionsWrapper.java b/src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/BasicProverWithAssumptionsWrapper.java index 596f30f4eb..789a1ef79b 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/BasicProverWithAssumptionsWrapper.java +++ b/src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/BasicProverWithAssumptionsWrapper.java @@ -18,6 +18,7 @@ import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.Model; import org.sosy_lab.java_smt.api.SolverException; +import org.sosy_lab.java_smt.api.proofs.Proof; public class BasicProverWithAssumptionsWrapper> implements BasicProverEnvironment { @@ -128,4 +129,9 @@ public R allSat(AllSatCallback pCallback, List pImportant clearAssumptions(); return delegate.allSat(pCallback, pImportant); } + + @Override + public Proof getProof() throws SolverException, InterruptedException { + return delegate.getProof(); + } } diff --git a/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingBasicProverEnvironment.java b/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingBasicProverEnvironment.java index c548d30384..d8ad071624 100644 --- a/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingBasicProverEnvironment.java +++ b/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingBasicProverEnvironment.java @@ -18,6 +18,7 @@ import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.Model; import org.sosy_lab.java_smt.api.SolverException; +import org.sosy_lab.java_smt.api.proofs.Proof; class DebuggingBasicProverEnvironment implements BasicProverEnvironment { private final BasicProverEnvironment delegate; @@ -93,6 +94,11 @@ public Optional> unsatCoreOverAssumptions( return delegate.unsatCoreOverAssumptions(assumptions); } + @Override + public Proof getProof() throws SolverException, InterruptedException { + return delegate.getProof(); + } + @Override public void close() { debugging.assertThreadLocal(); diff --git a/src/org/sosy_lab/java_smt/delegate/logging/LoggingBasicProverEnvironment.java b/src/org/sosy_lab/java_smt/delegate/logging/LoggingBasicProverEnvironment.java index 2f194c6125..c20916c683 100644 --- a/src/org/sosy_lab/java_smt/delegate/logging/LoggingBasicProverEnvironment.java +++ b/src/org/sosy_lab/java_smt/delegate/logging/LoggingBasicProverEnvironment.java @@ -24,6 +24,7 @@ import org.sosy_lab.java_smt.api.Model; import org.sosy_lab.java_smt.api.Model.ValueAssignment; import org.sosy_lab.java_smt.api.SolverException; +import org.sosy_lab.java_smt.api.proofs.Proof; /** Wraps a basic prover environment with a logging object. */ class LoggingBasicProverEnvironment implements BasicProverEnvironment { @@ -120,6 +121,12 @@ public ImmutableMap getStatistics() { return wrapped.getStatistics(); } + @Override + public Proof getProof() throws SolverException, InterruptedException { + Proof p = wrapped.getProof(); + return p; + } + @Override public void close() { wrapped.close(); diff --git a/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsBasicProverEnvironment.java b/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsBasicProverEnvironment.java index 49106d6324..d0c6bef146 100644 --- a/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsBasicProverEnvironment.java +++ b/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsBasicProverEnvironment.java @@ -18,6 +18,7 @@ import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.Model; import org.sosy_lab.java_smt.api.SolverException; +import org.sosy_lab.java_smt.api.proofs.Proof; import org.sosy_lab.java_smt.delegate.statistics.TimerPool.TimerWrapper; class StatisticsBasicProverEnvironment implements BasicProverEnvironment { @@ -99,6 +100,11 @@ public Optional> unsatCoreOverAssumptions( return delegate.unsatCoreOverAssumptions(pAssumptions); } + @Override + public Proof getProof() throws SolverException, InterruptedException { + return delegate.getProof(); + } + @Override public void close() { delegate.close(); diff --git a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBasicProverEnvironment.java b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBasicProverEnvironment.java index f0401c6db2..09d5894c60 100644 --- a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBasicProverEnvironment.java +++ b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBasicProverEnvironment.java @@ -20,6 +20,7 @@ import org.sosy_lab.java_smt.api.Model; import org.sosy_lab.java_smt.api.SolverContext; import org.sosy_lab.java_smt.api.SolverException; +import org.sosy_lab.java_smt.api.proofs.Proof; class SynchronizedBasicProverEnvironment implements BasicProverEnvironment { @@ -104,6 +105,11 @@ public ImmutableMap getStatistics() { } } + @Override + public Proof getProof() throws SolverException, InterruptedException { + return delegate.getProof(); + } + @Override public void close() { synchronized (sync) { diff --git a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBasicProverEnvironmentWithContext.java b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBasicProverEnvironmentWithContext.java index 43922ccc25..353e6dbbf5 100644 --- a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBasicProverEnvironmentWithContext.java +++ b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBasicProverEnvironmentWithContext.java @@ -22,6 +22,7 @@ import org.sosy_lab.java_smt.api.Model; import org.sosy_lab.java_smt.api.SolverContext; import org.sosy_lab.java_smt.api.SolverException; +import org.sosy_lab.java_smt.api.proofs.Proof; class SynchronizedBasicProverEnvironmentWithContext implements BasicProverEnvironment { @@ -121,6 +122,11 @@ public ImmutableMap getStatistics() { } } + @Override + public Proof getProof() throws SolverException, InterruptedException { + return delegate.getProof(); + } + @Override public void close() { synchronized (sync) { diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java index bee81d9746..6a033847d5 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java @@ -10,6 +10,7 @@ import static com.google.common.base.Preconditions.checkNotNull; import static com.google.common.base.Preconditions.checkState; +import static org.sosy_lab.java_smt.solvers.cvc5.CVC5ProofNode.generateProofImpl; import com.google.common.collect.Collections2; import com.google.common.collect.HashMultimap; @@ -43,6 +44,7 @@ import org.sosy_lab.java_smt.api.FormulaManager; import org.sosy_lab.java_smt.api.SolverContext.ProverOptions; import org.sosy_lab.java_smt.api.SolverException; +import org.sosy_lab.java_smt.api.proofs.Proof; import org.sosy_lab.java_smt.basicimpl.AbstractProverWithAllSat; abstract class CVC5AbstractProver extends AbstractProverWithAllSat { @@ -97,6 +99,7 @@ protected Solver getNewSolver() { newSolver.setOption("produce-assertions", "true"); newSolver.setOption("dump-models", "true"); + newSolver.setOption("produce-proofs", generateProofs ? "true" : "false"); // Set Strings option to enable all String features (such as lessOrEquals) newSolver.setOption("strings-exp", "true"); @@ -317,6 +320,23 @@ public Optional> unsatCoreOverAssumptions( throw new UnsupportedOperationException(ASSUMPTION_SOLVING_NOT_SUPPORTED); } + @Override + public Proof getProof() throws SolverException, InterruptedException { + checkGenerateProofs(); + checkState(!closed); + checkState(isUnsat()); + + io.github.cvc5.Proof[] proofs = solver.getProof(); + checkState(proofs != null && proofs.length != 0, "No proof available"); + + // CVC5ProofProcessor pp = new CVC5ProofProcessor(creator); + try { + return new CVC5Proof(generateProofImpl(proofs[0], creator)); + } catch (CVC5ApiException e) { + throw new SolverException("There was a problem generating proof", e); + } + } + @Override public void close() { if (!closed) { diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Proof.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Proof.java new file mode 100644 index 0000000000..a6a0e46653 --- /dev/null +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Proof.java @@ -0,0 +1,21 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2026 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.solvers.cvc5; + +import org.sosy_lab.java_smt.api.proofs.Proof; +import org.sosy_lab.java_smt.api.proofs.ProofNode; +import org.sosy_lab.java_smt.basicimpl.AbstractProof; + +class CVC5Proof extends AbstractProof implements Proof { + CVC5Proof(ProofNode pRoot) { + super(pRoot); + } +} diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5ProofNode.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5ProofNode.java new file mode 100644 index 0000000000..276b262c00 --- /dev/null +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5ProofNode.java @@ -0,0 +1,98 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2026 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.solvers.cvc5; + +import com.google.common.collect.ImmutableMap; +import io.github.cvc5.CVC5ApiException; +import io.github.cvc5.Term; +import java.util.ArrayDeque; +import java.util.Deque; +import java.util.LinkedHashMap; +import java.util.Map; +import org.sosy_lab.java_smt.api.Formula; +import org.sosy_lab.java_smt.api.proofs.ProofNode; +import org.sosy_lab.java_smt.api.proofs.ProofRule; +import org.sosy_lab.java_smt.basicimpl.AbstractProofNode; + +/** A proof of unsatisfiability returned by CVC5 transformed to the general proof API. */ +public final class CVC5ProofNode extends AbstractProofNode { + + static CVC5ProofNode generateProofImpl( + io.github.cvc5.Proof pProof, CVC5FormulaCreator pFormulaCreator) throws CVC5ApiException { + + Deque stack = new ArrayDeque<>(); + Map tempComputed; + + ImmutableMap computed = ImmutableMap.of(); + + stack.push(new CVC5Frame(pProof)); + + while (!stack.isEmpty()) { + CVC5Frame frame = stack.peek(); + + if (!frame.isVisited()) { + + frame.setNumArgs(frame.getProof().getChildren().length); + frame.setAsVisited(); + + for (int i = frame.getNumArgs() - 1; i >= 0; i--) { + io.github.cvc5.Proof child = frame.getProof().getChildren()[i]; + if (!computed.containsKey(child)) { + stack.push(new CVC5Frame(child)); + } + } + } else { + stack.pop(); + int numChildren = frame.getNumArgs(); + + CVC5ProofRule proofRule = + Enum.valueOf(CVC5ProofRule.class, frame.getProof().getRule().toString()); + + // Generate formula + Term term = frame.getProof().getResult(); + Formula pFormula = pFormulaCreator.encapsulate(pFormulaCreator.getFormulaType(term), term); + CVC5ProofNode pn = new CVC5ProofNode(proofRule, pFormula); + for (int i = 0; i < numChildren; i++) { + io.github.cvc5.Proof child = frame.getProof().getChildren()[i]; + + if (computed.containsKey(child)) { + pn.addChild(computed.get(child)); + } + } + tempComputed = new LinkedHashMap<>(computed); + tempComputed.put(frame.getProof(), pn); + computed = ImmutableMap.copyOf(tempComputed); + } + } + return computed.get(pProof); + } + + private static class CVC5Frame extends ProofFrame { + CVC5Frame(io.github.cvc5.Proof proof) { + super(proof); + } + } + + private CVC5ProofNode(ProofRule pProofRule, Formula pFormula) { + + super(pProofRule, pFormula); + } + + @Override + protected void addChild(ProofNode pChild) { + super.addChild(pChild); + } + + @Override + public String proofAsString() { + return super.proofAsString(); + } +} diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5ProofRule.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5ProofRule.java new file mode 100644 index 0000000000..b4107eec03 --- /dev/null +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5ProofRule.java @@ -0,0 +1,184 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2026 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.solvers.cvc5; + +import org.sosy_lab.java_smt.api.proofs.ProofRule; + +// TODO: Properly include the formulas for the proof rules. +enum CVC5ProofRule implements ProofRule { + ASSUME("assume"), + SCOPE("scope"), + SUBS("subs"), + MACRO_REWRITE("macro_rewrite"), + EVALUATE("evaluate"), + DISTINCT_VALUES("distinct_values"), + ACI_NORM("aci_norm"), + ABSORB("absorb"), + MACRO_SR_EQ_INTRO("macro_sr_eq_intro"), + MACRO_SR_PRED_INTRO("macro_sr_pred_intro"), + MACRO_SR_PRED_ELIM("macro_sr_pred_elim"), + MACRO_SR_PRED_TRANSFORM("macro_sr_pred_transform"), + ENCODE_EQ_INTRO("encode_eq_intro"), + DSL_REWRITE("dsl_rewrite"), + THEORY_REWRITE("theory_rewrite"), + ITE_EQ("ite_eq"), + TRUST("trust"), + TRUST_THEORY_REWRITE("trust_theory_rewrite"), + SAT_REFUTATION("sat_refutation"), + DRAT_REFUTATION("drat_refutation"), + SAT_EXTERNAL_PROVE("sat_external_prove"), + RESOLUTION("resolution"), + CHAIN_M_RESOLUTION("chain_m_resolution"), + CHAIN_RESOLUTION("chain_resolution"), + FACTORING("factoring"), + REORDERING("reordering"), + MACRO_RESOLUTION("macro_resolution"), + MACRO_RESOLUTION_TRUST("macro_resolution_trust"), + SPLIT("split"), + EQ_RESOLVE("eq_resolve"), + MODUS_PONENS("modus_ponens"), + NOT_NOT_ELIM("not_not_elim"), + CONTRA("contra"), + AND_ELIM("and_elim"), + AND_INTRO("and_intro"), + NOT_OR_ELIM("not_or_elim"), + IMPLIES_ELIM("implies_elim"), + NOT_IMPLIES_ELIM1("not_implies_elim1"), + NOT_IMPLIES_ELIM2("not_implies_elim2"), + EQUIV_ELIM1("equiv_elim1"), + EQUIV_ELIM2("equiv_elim2"), + NOT_EQUIV_ELIM1("not_equiv_elim1"), + NOT_EQUIV_ELIM2("not_equiv_elim2"), + XOR_ELIM1("xor_elim1"), + XOR_ELIM2("xor_elim2"), + NOT_XOR_ELIM1("not_xor_elim1"), + NOT_XOR_ELIM2("not_xor_elim2"), + ITE_ELIM1("ite_elim1"), + ITE_ELIM2("ite_elim2"), + NOT_ITE_ELIM1("not_ite_elim1"), + NOT_ITE_ELIM2("not_ite_elim2"), + NOT_AND("not_and"), + CNF_AND_POS("cnf_and_pos"), + CNF_AND_NEG("cnf_and_neg"), + CNF_OR_POS("cnf_or_pos"), + CNF_OR_NEG("cnf_or_neg"), + CNF_IMPLIES_POS("cnf_implies_pos"), + CNF_IMPLIES_NEG1("cnf_implies_neg1"), + CNF_IMPLIES_NEG2("cnf_implies_neg2"), + CNF_EQUIV_POS1("cnf_equiv_pos1"), + CNF_EQUIV_POS2("cnf_equiv_pos2"), + CNF_EQUIV_NEG1("cnf_equiv_neg1"), + CNF_EQUIV_NEG2("cnf_equiv_neg2"), + CNF_XOR_POS1("cnf_xor_pos1"), + CNF_XOR_POS2("cnf_xor_pos2"), + CNF_XOR_NEG1("cnf_xor_neg1"), + CNF_XOR_NEG2("cnf_xor_neg2"), + CNF_ITE_POS1("cnf_ite_pos1"), + CNF_ITE_POS2("cnf_ite_pos2"), + CNF_ITE_POS3("cnf_ite_pos3"), + CNF_ITE_NEG1("cnf_ite_neg1"), + CNF_ITE_NEG2("cnf_ite_neg2"), + CNF_ITE_NEG3("cnf_ite_neg3"), + REFL("refl"), + SYMM("symm"), + TRANS("trans"), + CONG("cong"), + NARY_CONG("nary_cong"), + TRUE_INTRO("true_intro"), + TRUE_ELIM("true_elim"), + FALSE_INTRO("false_intro"), + FALSE_ELIM("false_elim"), + HO_APP_ENCODE("ho_app_encode"), + HO_CONG("ho_cong"), + ARRAYS_READ_OVER_WRITE("arrays_read_over_write"), + ARRAYS_READ_OVER_WRITE_CONTRA("arrays_read_over_write_contra"), + ARRAYS_READ_OVER_WRITE_1("arrays_read_over_write_1"), + ARRAYS_EXT("arrays_ext"), + MACRO_BV_BITBLAST("macro_bv_bitblast"), + BV_BITBLAST_STEP("bv_bitblast_step"), + BV_EAGER_ATOM("bv_eager_atom"), + BV_POLY_NORM("bv_poly_norm"), + BV_POLY_NORM_EQ("bv_poly_norm_eq"), + DT_SPLIT("dt_split"), + SKOLEM_INTRO("skolem_intro"), + SKOLEMIZE("skolemize"), + INSTANTIATE("instantiate"), + ALPHA_EQUIV("alpha_equiv"), + QUANT_VAR_REORDERING("quant_var_reordering"), + SETS_SINGLETON_INJ("sets_singleton_inj"), + SETS_EXT("sets_ext"), + SETS_FILTER_UP("sets_filter_up"), + SETS_FILTER_DOWN("sets_filter_down"), + CONCAT_EQ("concat_eq"), + CONCAT_UNIFY("concat_unify"), + CONCAT_SPLIT("concat_split"), + CONCAT_CSPLIT("concat_csplit"), + CONCAT_LPROP("concat_lprop"), + CONCAT_CPROP("concat_cprop"), + STRING_DECOMPOSE("string_decompose"), + STRING_LENGTH_POS("string_length_pos"), + STRING_LENGTH_NON_EMPTY("string_length_non_empty"), + STRING_REDUCTION("string_reduction"), + STRING_EAGER_REDUCTION("string_eager_reduction"), + RE_INTER("re_inter"), + RE_CONCAT("re_concat"), + RE_UNFOLD_POS("re_unfold_pos"), + RE_UNFOLD_NEG("re_unfold_neg"), + RE_UNFOLD_NEG_CONCAT_FIXED("re_unfold_neg_concat_fixed"), + STRING_CODE_INJ("string_code_inj"), + STRING_SEQ_UNIT_INJ("string_seq_unit_inj"), + STRING_EXT("string_ext"), + MACRO_STRING_INFERENCE("macro_string_inference"), + MACRO_ARITH_SCALE_SUM_UB("macro_arith_scale_sum_ub"), + ARITH_MULT_ABS_COMPARISON("arith_mult_abs_comparison"), + ARITH_SUM_UB("arith_sum_ub"), + INT_TIGHT_UB("int_tight_ub"), + INT_TIGHT_LB("int_tight_lb"), + ARITH_TRICHOTOMY("arith_trichotomy"), + ARITH_REDUCTION("arith_reduction"), + ARITH_POLY_NORM("arith_poly_norm"), + ARITH_POLY_NORM_REL("arith_poly_norm_rel"), + ARITH_MULT_SIGN("arith_mult_sign"), + ARITH_MULT_POS("arith_mult_pos"), + ARITH_MULT_NEG("arith_mult_neg"), + ARITH_MULT_TANGENT("arith_mult_tangent"), + ARITH_TRANS_PI("arith_trans_pi"), + ARITH_TRANS_EXP_NEG("arith_trans_exp_neg"), + ARITH_TRANS_EXP_POSITIVITY("arith_trans_exp_positivity"), + ARITH_TRANS_EXP_SUPER_LIN("arith_trans_exp_super_lin"), + ARITH_TRANS_EXP_ZERO("arith_trans_exp_zero"), + ARITH_TRANS_EXP_APPROX_ABOVE_NEG("arith_trans_exp_approx_above_neg"), + ARITH_TRANS_EXP_APPROX_ABOVE_POS("arith_trans_exp_approx_above_pos"), + ARITH_TRANS_EXP_APPROX_BELOW("arith_trans_exp_approx_below"), + ARITH_TRANS_SINE_BOUNDS("arith_trans_sine_bounds"), + ARITH_TRANS_SINE_SHIFT("arith_trans_sine_shift"), + ARITH_TRANS_SINE_SYMMETRY("arith_trans_sine_symmetry"), + ARITH_TRANS_SINE_TANGENT_ZERO("arith_trans_sine_tangent_zero"), + ARITH_TRANS_SINE_TANGENT_PI("arith_trans_sine_tangent_pi"), + ARITH_TRANS_SINE_APPROX_ABOVE_NEG("arith_trans_sine_approx_above_neg"), + ARITH_TRANS_SINE_APPROX_ABOVE_POS("arith_trans_sine_approx_above_pos"), + ARITH_TRANS_SINE_APPROX_BELOW_NEG("arith_trans_sine_approx_below_neg"), + ARITH_TRANS_SINE_APPROX_BELOW_POS("arith_trans_sine_approx_below_pos"), + LFSC_RULE("lfsc_rule"), + ALETHE_RULE("alethe_rule"), + UNKNOWN("unknown"); + + private final String name; + + CVC5ProofRule(String pName) { + name = pName; + } + + @Override + public String getName() { + return name; + } +} diff --git a/src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java b/src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java index 4364dfae74..cf2ba05ae7 100644 --- a/src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java +++ b/src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java @@ -16,20 +16,34 @@ import static org.sosy_lab.java_smt.SolverContextFactory.Solvers.MATHSAT5; import static org.sosy_lab.java_smt.SolverContextFactory.Solvers.OPENSMT; import static org.sosy_lab.java_smt.SolverContextFactory.Solvers.PRINCESS; +import static org.sosy_lab.java_smt.api.FormulaType.IntegerType; import static org.sosy_lab.java_smt.api.SolverContext.ProverOptions.GENERATE_UNSAT_CORE; import static org.sosy_lab.java_smt.api.SolverContext.ProverOptions.GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS; import static org.sosy_lab.java_smt.test.ProverEnvironmentSubject.assertThat; import com.google.common.collect.ImmutableList; +import java.util.ArrayDeque; +import java.util.Deque; import java.util.List; import java.util.Optional; import org.junit.Test; +import org.sosy_lab.java_smt.api.ArrayFormula; import org.sosy_lab.java_smt.api.BasicProverEnvironment; +import org.sosy_lab.java_smt.api.BitvectorFormula; import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.Formula; +import org.sosy_lab.java_smt.api.FormulaType; +import org.sosy_lab.java_smt.api.FormulaType.ArrayFormulaType; +import org.sosy_lab.java_smt.api.FunctionDeclaration; import org.sosy_lab.java_smt.api.Model; +import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula; +import org.sosy_lab.java_smt.api.NumeralFormula.RationalFormula; import org.sosy_lab.java_smt.api.ProverEnvironment; +import org.sosy_lab.java_smt.api.RationalFormulaManager; import org.sosy_lab.java_smt.api.SolverContext.ProverOptions; import org.sosy_lab.java_smt.api.SolverException; +import org.sosy_lab.java_smt.api.proofs.ProofNode; +import org.sosy_lab.java_smt.api.proofs.ProofRule; public class ProverEnvironmentTest extends SolverBasedTest0.ParameterizedSolverBasedTest0 { @@ -189,4 +203,348 @@ private void checkSimpleQuery(ProverEnvironment pProver) pProver.pop(); } } + + @Test + public void testGetSimpleBooleanProof() throws InterruptedException, SolverException { + assume().that(solverToUse()).isEqualTo(CVC5); + requireProofGeneration(); // Ensures proofs are supported + BooleanFormula q1 = bmgr.makeVariable("q1"); + BooleanFormula q2 = bmgr.makeVariable("q2"); + + try (ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_PROOFS)) { + prover.addConstraint(bmgr.or(bmgr.not(q1), q2)); + prover.addConstraint(q1); + prover.addConstraint(bmgr.not(q2)); + + assertThat(prover.isUnsat()).isTrue(); + + // Test getProof() + ProofNode proofNode = prover.getProof().getProofRoot(); + verifyProofObjectValidity(proofNode); + } + } + + @Test + public void testGetComplexRationalNumeralAndUFProof() + throws InterruptedException, SolverException { + assume().that(solverToUse()).isEqualTo(CVC5); + requireProofGeneration(); // Ensures proofs are supported + requireRationals(); + + // "(declare-fun x1 () Real)" + + // "(declare-fun x2 () Real)" + + // "(declare-fun x3 () Real)" + + // "(declare-fun y1 () Real)" + + // "(declare-fun y2 () Real)" + + // "(declare-fun y3 () Real)" + + // "(declare-fun b () Real)" + + // "(declare-fun f (Real) Real)" + + // "(declare-fun g (Real) Real)" + + // "(declare-fun a () Bool)" + + // "(declare-fun c () Bool)" + + // "(assert (and a (= (+ (f y1) y2) y3) (<= y1 x1)))" + + // "(assert (and (= x2 (g b)) (= y2 (g b)) (<= x1 y1) (< x3 y3)))" + + // "(assert (= a (= (+ (f x1) x2) x3)))" + + // "(assert (and (or a c) (not c)))"; + RationalFormula x1 = mgr.makeVariable(FormulaType.RationalType, "x1"); + RationalFormula x2 = mgr.makeVariable(FormulaType.RationalType, "x2"); + RationalFormula x3 = mgr.makeVariable(FormulaType.RationalType, "x3"); + RationalFormula y1 = mgr.makeVariable(FormulaType.RationalType, "y1"); + RationalFormula y2 = mgr.makeVariable(FormulaType.RationalType, "y2"); + RationalFormula y3 = mgr.makeVariable(FormulaType.RationalType, "y3"); + RationalFormula b = mgr.makeVariable(FormulaType.RationalType, "b"); + FunctionDeclaration f = + mgr.getUFManager().declareUF("f", FormulaType.RationalType, FormulaType.RationalType); + FunctionDeclaration g = + mgr.getUFManager().declareUF("g", FormulaType.RationalType, FormulaType.RationalType); + BooleanFormula a = bmgr.makeVariable("a"); + BooleanFormula c = bmgr.makeVariable("c"); + + RationalFormulaManager rfmgr = mgr.getRationalFormulaManager(); + + try (ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_PROOFS)) { + // "(assert (and a (= (+ (f y1) y2) y3) (<= y1 x1)))" + prover.addConstraint( + bmgr.and( + a, + rfmgr.equal(rfmgr.add(mgr.makeApplication(f, y1), y2), y3), + rfmgr.lessOrEquals(y1, x1))); + // "(assert (and (= x2 (g b)) (= y2 (g b)) (<= x1 y1) (< x3 y3)))" + prover.addConstraint( + bmgr.and( + rfmgr.equal(x2, mgr.makeApplication(g, b)), + rfmgr.equal(y2, mgr.makeApplication(g, b)), + rfmgr.lessOrEquals(x1, y1), + rfmgr.lessThan(x3, y3))); + // "(assert (= a (= (+ (f x1) x2) x3)))" + prover.addConstraint( + bmgr.equivalence(a, rfmgr.equal(rfmgr.add(mgr.makeApplication(f, x1), x2), x3))); + // "(assert (and (or a c) (not c)))" + prover.addConstraint(bmgr.and(bmgr.or(a, c), bmgr.not(c))); + assertThat(prover.isUnsat()).isTrue(); + + // Retrieve and verify proofNode + ProofNode proofNode = prover.getProof().getProofRoot(); + verifyProofObjectValidity(proofNode); + } + } + + @Test + public void proofOfTrueTest() throws InterruptedException, SolverException { + assume().that(solverToUse()).isEqualTo(CVC5); + requireProofGeneration(); + + BooleanFormula tru = bmgr.makeTrue(); + + try (ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_PROOFS)) { + prover.addConstraint(tru); + assertThat(prover.isUnsat()).isFalse(); + + @SuppressWarnings("unused") + ProofNode proofNode = prover.getProof().getProofRoot(); + throw new AssertionError("Expected IllegalStateException was not thrown"); + + } catch (IllegalStateException e) { + // this should be thrown as getProof was called when last evaluation + // was SAT + } + } + + @Test + public void proofOfFalseTest() throws InterruptedException, SolverException { + requireProofGeneration(); + assume().that(solverToUse()).isEqualTo(CVC5); + + BooleanFormula bottom = bmgr.makeFalse(); + + try (ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_PROOFS)) { + prover.addConstraint(bottom); + assertThat(prover.isUnsat()).isTrue(); + + ProofNode proofNode = prover.getProof().getProofRoot(); + assertThat(proofNode).isNotNull(); + } + } + + @Test + public void testGetSimpleIntegerProof() throws InterruptedException, SolverException { + assume().that(solverToUse()).isEqualTo(CVC5); + requireProofGeneration(); // Ensures proofs are supported + requireIntegers(); + + IntegerFormula x1 = imgr.makeVariable("x1"); + IntegerFormula two = imgr.makeNumber("2"); + IntegerFormula cero = imgr.makeNumber("0"); + + try (ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_PROOFS)) { + prover.addConstraint(imgr.equal(x1, two)); + prover.addConstraint(imgr.lessThan(x1, cero)); + assertThat(prover.isUnsat()).isTrue(); + + // Test getProof() + ProofNode proofNode = prover.getProof().getProofRoot(); + verifyProofObjectValidity(proofNode); + } + } + + @Test + public void getProofAfterGetProofAndAddingAssertionsTest() + throws InterruptedException, SolverException { + assume().that(solverToUse()).isEqualTo(CVC5); + requireProofGeneration(); // Ensures proofs are supported + BooleanFormula q1 = bmgr.makeVariable("q1"); + BooleanFormula q2 = bmgr.makeVariable("q2"); + IntegerFormula x1 = imgr.makeVariable("x1"); + IntegerFormula two = imgr.makeNumber("2"); + IntegerFormula cero = imgr.makeNumber("0"); + + try (ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_PROOFS)) { + prover.addConstraint(bmgr.or(bmgr.not(q1), q2)); + prover.addConstraint(q1); + prover.addConstraint(bmgr.not(q2)); + + assertThat(prover.isUnsat()).isTrue(); + + // Test getProof() + ProofNode proofNode = prover.getProof().getProofRoot(); + verifyProofObjectValidity(proofNode); + + // assert integer formulas and test again + prover.addConstraint(imgr.equal(x1, two)); + prover.addConstraint(imgr.lessThan(x1, cero)); + + assertThat(prover.isUnsat()).isTrue(); + + // Test getProof() + ProofNode secondProofNode = prover.getProof().getProofRoot(); + verifyProofObjectValidity(secondProofNode); + + assertThat(proofNode).isNotEqualTo(secondProofNode); + } + } + + @Test + public void getProofAfterGetProofClearingStackAndAddingDifferentAssertionsTest() + throws InterruptedException, SolverException { + assume().that(solverToUse()).isEqualTo(CVC5); + requireProofGeneration(); // Ensures proofs are supported + requireIntegers(); + + BooleanFormula q1 = bmgr.makeVariable("q1"); + BooleanFormula q2 = bmgr.makeVariable("q2"); + IntegerFormula x1 = imgr.makeVariable("x1"); + IntegerFormula two = imgr.makeNumber("2"); + IntegerFormula cero = imgr.makeNumber("0"); + + try (ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_PROOFS)) { + + prover.push(bmgr.or(bmgr.not(q1), q2)); + prover.push(q1); + prover.push(bmgr.not(q2)); + + assertThat(prover.isUnsat()).isTrue(); + + // Test getProof() + ProofNode proofNode = prover.getProof().getProofRoot(); + verifyProofObjectValidity(proofNode); + + prover.pop(); + prover.pop(); + prover.pop(); + + // assert integer formulas and test again + prover.push(imgr.equal(x1, two)); + prover.push(imgr.lessThan(x1, cero)); + + assertThat(prover.isUnsat()).isTrue(); + + // Test getProof() + ProofNode secondProofNode = prover.getProof().getProofRoot(); + verifyProofObjectValidity(secondProofNode); + + assertThat(proofNode).isNotEqualTo(secondProofNode); + } + } + + @Test + public void getProofWithoutProofProductionEnabledTest() + throws InterruptedException, SolverException { + requireProofGeneration(); + + BooleanFormula bottom = bmgr.makeFalse(); + + try (ProverEnvironment prover = context.newProverEnvironment()) { + prover.addConstraint(bottom); + assertThat(prover.isUnsat()).isTrue(); + + @SuppressWarnings("unused") + ProofNode proofNode = prover.getProof().getProofRoot(); + throw new AssertionError("Expected IllegalStateException was not thrown"); + + } catch (IllegalStateException e) { + assertThat(e.getMessage()).isEqualTo("Please set the prover option GENERATE_PROOFS."); + } + } + + // This test is based on the bvIsZeroAfterShiftLeft() test in BitvectorFormulaManagerTest + @Test + public void getBitVectorProofTest() throws InterruptedException, SolverException { + assume().that(solverToUse()).isEqualTo(CVC5); + requireProofGeneration(); + requireBitvectors(); + + BitvectorFormula one = bvmgr.makeBitvector(32, 1); + + // unsigned char + BitvectorFormula a = bvmgr.makeVariable(8, "char_a"); + BitvectorFormula b = bvmgr.makeVariable(8, "char_b"); + BitvectorFormula rightOp = bvmgr.makeBitvector(32, 7); + + // 'cast' a to unsigned int + a = bvmgr.extend(a, 32 - 8, false); + b = bvmgr.extend(b, 32 - 8, false); + a = bvmgr.or(a, one); + b = bvmgr.or(b, one); + a = bvmgr.extract(a, 7, 0); + b = bvmgr.extract(b, 7, 0); + a = bvmgr.extend(a, 32 - 8, false); + b = bvmgr.extend(b, 32 - 8, false); + + a = bvmgr.shiftLeft(a, rightOp); + b = bvmgr.shiftLeft(b, rightOp); + a = bvmgr.extract(a, 7, 0); + b = bvmgr.extract(b, 7, 0); + BooleanFormula f = bmgr.not(bvmgr.equal(a, b)); + + try (ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_PROOFS)) { + prover.addConstraint(f); + assertThat(prover.isUnsat()).isTrue(); + + // Test getProof() + ProofNode proofNode = prover.getProof().getProofRoot(); + verifyProofObjectValidity(proofNode); + } + } + + // This test is based on the testIntIndexIntValue() test in ArrayFormulaManagerTest + @Test + public void getArrayProofTest() throws InterruptedException, SolverException { + assume().that(solverToUse()).isEqualTo(CVC5); + requireProofGeneration(); + requireIntegers(); + requireArrays(); + + // (arr2 = store(arr1, 4, 2)) & !(select(arr2, 4) = 2) + ArrayFormulaType type = + FormulaType.getArrayType(IntegerType, IntegerType); + IntegerFormula num2 = imgr.makeNumber(2); + IntegerFormula num4 = imgr.makeNumber(4); + ArrayFormula arr1 = amgr.makeArray("arr1", type); + ArrayFormula arr2 = amgr.makeArray("arr2", type); + BooleanFormula query = + bmgr.and( + amgr.equivalence(arr2, amgr.store(arr1, num4, num2)), + bmgr.not(imgr.equal(num2, amgr.select(arr2, num4)))); + + try (ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_PROOFS)) { + prover.addConstraint(query); + assertThat(prover.isUnsat()).isTrue(); + + // Test getProof() + ProofNode proofNode = prover.getProof().getProofRoot(); + verifyProofObjectValidity(proofNode); + } + } + + /** + * Helper function that tests that every proof has valid information stored (proof rules, + * formulas, successors). + * + *

In this case a formula must be present, because only CVC5 is implemented. However, the + * implementation of solvers which not always expose a formula is a work in progress. + * + * @param pRoot the root of the proof DAG to be tested. + */ + private void verifyProofObjectValidity(ProofNode pRoot) { + assertThat(pRoot).isNotNull(); + + Deque stack = new ArrayDeque<>(); + stack.push(pRoot); + + while (!stack.isEmpty()) { + ProofNode proofNode = stack.pop(); + ProofRule rule = proofNode.getRule(); + Optional formula = proofNode.getFormula(); + + assertThat(rule).isNotNull(); + assertThat(rule).isInstanceOf(ProofRule.class); + assertThat(proofNode.getChildren()).isNotNull(); + assertThat(formula.isPresent()).isTrue(); + + for (ProofNode child : proofNode.getChildren()) { + assertThat(child).isNotNull(); + stack.push(child); + } + } + } } diff --git a/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java b/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java index e28c6823c2..c8fd67a6e0 100644 --- a/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java +++ b/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java @@ -423,6 +423,24 @@ protected void requireUserPropagators() { .isEqualTo(Solvers.Z3); } + protected void requireProofGeneration() { + assume() + .withMessage( + "Current version of solver %s does not support proof generation", solverToUse()) + .that(solverToUse()) + .isNoneOf( + Solvers.BOOLECTOR, + Solvers.BITWUZLA, + Solvers.YICES2, + Solvers.CVC4, + Solvers.PRINCESS, + Solvers.MATHSAT5, + Solvers.Z3_WITH_INTERPOLATION, + Solvers.Z3, + Solvers.OPENSMT, + Solvers.SMTINTERPOL); + } + /** * Use this for checking assertions about BooleanFormulas with Truth: * assertThatFormula(formula).is...().