From d7f226a7647db0162c0c2ac71d6cdbb7610de3e7 Mon Sep 17 00:00:00 2001 From: Gabriel Carpio Date: Sat, 20 Dec 2025 09:05:25 +0100 Subject: [PATCH 01/44] Added interfaces for handling general proofs of unsatisfiability: `Proof`, `ProofRule`. --- .../sosy_lab/java_smt/api/proofs/Proof.java | 37 +++++++++++++++++++ .../java_smt/api/proofs/ProofRule.java | 23 ++++++++++++ 2 files changed, 60 insertions(+) create mode 100644 src/org/sosy_lab/java_smt/api/proofs/Proof.java create mode 100644 src/org/sosy_lab/java_smt/api/proofs/ProofRule.java 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..11beab6aa5 --- /dev/null +++ b/src/org/sosy_lab/java_smt/api/proofs/Proof.java @@ -0,0 +1,37 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2024 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.api.proofs; + +import java.util.Optional; +import java.util.Set; +import org.sosy_lab.java_smt.api.Formula; + +/** + * A proof node in the proof DAG of a proof. + * + * @author Gabriel Carpio + */ +public interface Proof { + + /** Get the children of the proof node. */ + Set getChildren(); + + boolean isLeaf(); + + /** + * Get the formula of the proof node. + * + * @return The formula of the proof node. + */ + Optional getFormula(); + + 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..0199864eb5 --- /dev/null +++ b/src/org/sosy_lab/java_smt/api/proofs/ProofRule.java @@ -0,0 +1,23 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2024 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.api.proofs; + +/** A proof rule from a given proof format. */ +public interface ProofRule { + + /** Get the name of the proof rule. */ + String getName(); + + /** Get the formula of the proof rule. */ + default String getFormula() { + return "no formula available"; + } +} From 9647cd57f03a042bb73ee3df11632a838375f5bf Mon Sep 17 00:00:00 2001 From: Gabriel Carpio Date: Sat, 20 Dec 2025 09:06:06 +0100 Subject: [PATCH 02/44] Added abstract class implementing the proof interface `AbstractProof`. --- .../java_smt/basicimpl/AbstractProof.java | 110 ++++++++++++++++++ 1 file changed, 110 insertions(+) create mode 100644 src/org/sosy_lab/java_smt/basicimpl/AbstractProof.java 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..849d2af692 --- /dev/null +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProof.java @@ -0,0 +1,110 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2024 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.basicimpl; + +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.Proof; +import org.sosy_lab.java_smt.api.proofs.ProofRule; + +/** + * A proof DAG of a proof. + * + * @author Gabriel Carpio + */ +public abstract class AbstractProof implements Proof { + + // protected abstract class Transformation { + // protected Transformation( + // FormulaCreator formulaCreator, T proof) {} + + // protected abstract Proof generateProof(); + // } + + private final Set children = new LinkedHashSet<>(); + private ProofRule rule; + protected Optional formula = Optional.empty(); + + protected AbstractProof(ProofRule rule, @Nullable Formula formula) { + this.rule = rule; + this.formula = Optional.ofNullable(formula); + } + + // TODO: Use Optional instead of nullable + @Override + public Optional getFormula() { + return this.formula; + } + + @Override + public Set getChildren() { + return this.children; + } + + protected void addChild(Proof child) { + this.children.add(child); + } + + @Override + public ProofRule getRule() { + return rule; + } + + @Override + public boolean isLeaf() { + return getChildren().isEmpty(); + } + + // void setRule(ProofRule rule) { + // this.rule = rule; + // } + + public void setFormula(@Nullable Formula pFormula) { + formula = Optional.ofNullable(pFormula); + } + + public void setRule(ProofRule pRule) { + rule = pRule; + } + + // use this for debugging + public String proofAsString() { + return proofAsString(0); + } + + protected String proofAsString(int indentLevel) { + StringBuilder sb = new StringBuilder(); + String indent = " ".repeat(indentLevel); + + 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 (Proof child : getChildren()) { + sb.append(indent).append("Child ").append(++i).append(":\n"); + sb.append(((AbstractProof) child).proofAsString(indentLevel + 1)); + } + } + + return sb.toString(); + } +} From 570eb5c7aa2bd6c78f619a44bb9bb86830de99f3 Mon Sep 17 00:00:00 2001 From: Gabriel Carpio Date: Sat, 20 Dec 2025 09:11:06 +0100 Subject: [PATCH 03/44] Added the implementation of method `getProof` for retrieving `Proof` objects in `BasicProverEnvironment` and multiple classes that implement said interface: `BasicProverEnvironmentWithAssumptionsWrapper`, `DebuggingBasicProverEnvironment`, `LoggingBasicProverEnvironment`, `StatisticsBasicProverEnvironment`, `SynchronizedBasicProverEnvironment`, `SynchronizedBasicProverEnvironmentWithContext`. --- src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java | 7 +++++++ .../BasicProverWithAssumptionsWrapper.java | 6 ++++++ .../debugging/DebuggingBasicProverEnvironment.java | 6 ++++++ .../delegate/logging/LoggingBasicProverEnvironment.java | 7 +++++++ .../statistics/StatisticsBasicProverEnvironment.java | 6 ++++++ .../synchronize/SynchronizedBasicProverEnvironment.java | 6 ++++++ .../SynchronizedBasicProverEnvironmentWithContext.java | 6 ++++++ 7 files changed, 44 insertions(+) diff --git a/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java b/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java index 88f3008b0e..00d9d9989f 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,12 @@ default ImmutableMap getStatistics() { return ImmutableMap.of(); } + /** + * Get proof of unsatisfiability of the conjuction of the current satck of all formulas. Should + * only be called after {@link #isUnsat()} 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/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) { From 0fd007030a9146003f5d7336a8849211c5644921 Mon Sep 17 00:00:00 2001 From: Gabriel Carpio Date: Sat, 20 Dec 2025 09:13:55 +0100 Subject: [PATCH 04/44] Added the implementation of method `getProof` for retrieving `Proof` objects in abstract class `AbstractProver` as well as flag `generateProofs` and method `checkGenerateProofs`. --- .../java_smt/basicimpl/AbstractProver.java | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java index f3d83cb22b..1f9559b3b1 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java @@ -29,6 +29,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 { @@ -37,6 +38,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 @@ -61,6 +63,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()); @@ -94,6 +97,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 checkEnableSeparationLogic() { Preconditions.checkState(!closed); Preconditions.checkState(enableSL, TEMPLATE, ProverOptions.ENABLE_SEPARATION_LOGIC); @@ -245,4 +255,10 @@ public void close() { closeAllEvaluators(); closed = true; } + + @Override + public Proof getProof() throws InterruptedException, SolverException { + throw new UnsupportedOperationException( + "Proof generation is not available for the current solver."); + } } From 6272b50e9b31192406c833d04d080110c12e3614 Mon Sep 17 00:00:00 2001 From: Gabriel Carpio Date: Sat, 20 Dec 2025 09:17:25 +0100 Subject: [PATCH 05/44] Added the abstract class `ProofFrame` for transformation of native proof objects from the solvers into `Proof` objects. --- .../java_smt/api/proofs/ProofFrame.java | 53 +++++++++++++++++++ 1 file changed, 53 insertions(+) create mode 100644 src/org/sosy_lab/java_smt/api/proofs/ProofFrame.java diff --git a/src/org/sosy_lab/java_smt/api/proofs/ProofFrame.java b/src/org/sosy_lab/java_smt/api/proofs/ProofFrame.java new file mode 100644 index 0000000000..71677e7ef4 --- /dev/null +++ b/src/org/sosy_lab/java_smt/api/proofs/ProofFrame.java @@ -0,0 +1,53 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2024 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.api.proofs; + +/** + * Stores proof related information and gets stored in a stack when processing proofs. Each frame + * contains a proof object and the number of arguments it has. + * + * @param The type of the proof object. + */ +public abstract class ProofFrame { + final T proof; + int numArgs = 0; + boolean visited; + + protected ProofFrame(T proof) { + this.proof = proof; + 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(boolean isVisited) { + this.visited = isVisited; + } + + /** Set the number of arguments the proof object has. */ + public void setNumArgs(int numArgs) { + this.numArgs = numArgs; + } +} From 0f8c032dbc0d303b16ba34b03f03dba687cd4b02 Mon Sep 17 00:00:00 2001 From: Gabriel Carpio Date: Sat, 20 Dec 2025 09:18:28 +0100 Subject: [PATCH 06/44] Added `GENERATE_PROOFS` to `ProverOptions` in `SolverContext`. --- src/org/sosy_lab/java_smt/api/SolverContext.java | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/org/sosy_lab/java_smt/api/SolverContext.java b/src/org/sosy_lab/java_smt/api/SolverContext.java index 3fbd476c77..100eb55494 100644 --- a/src/org/sosy_lab/java_smt/api/SolverContext.java +++ b/src/org/sosy_lab/java_smt/api/SolverContext.java @@ -52,6 +52,14 @@ enum ProverOptions { */ GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS, + /** + * Whether the solver should generate proofs for unsatisfiable formulas. For Z3, this parameter + * is context(not solver)-based, so for setting it, the extra option in the {@link + * org.sosy_lab.common.configuration.Configuration} instance: "requireProofs" should be set to + * "true". + */ + GENERATE_PROOFS, + /** Whether the solver should enable support for formulae build in SL theory. */ ENABLE_SEPARATION_LOGIC } From b9dc8508902f4fcdde2b30da7133439caae8d256 Mon Sep 17 00:00:00 2001 From: Gabriel Carpio Date: Sat, 20 Dec 2025 09:22:36 +0100 Subject: [PATCH 07/44] Implemented method `getProof` in `CVC5AbstractProver` for retrieving common `Proof`s from the solver. --- .../solvers/cvc5/CVC5AbstractProver.java | 22 +++++++++++++++++++ 1 file changed, 22 insertions(+) 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..c800e48812 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.CVC5Proof.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,25 @@ 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(); + if (proofs == null || proofs.length == 0) { + throw new IllegalStateException("No proof available"); + } + + // CVC5ProofProcessor pp = new CVC5ProofProcessor(creator); + try { + return generateProofImpl(proofs[0], creator); + } catch (CVC5ApiException e) { + throw new SolverException("There was a problem generating proof", e); + } + } + @Override public void close() { if (!closed) { From d3e69b11adb4580cb973d76c55bd9acf3cceaf51 Mon Sep 17 00:00:00 2001 From: Gabriel Carpio Date: Sat, 20 Dec 2025 09:26:46 +0100 Subject: [PATCH 08/44] Added enum `CVC5ProofRule` for the different proof rules used by CVC5. --- .../java_smt/solvers/cvc5/CVC5ProofRule.java | 190 ++++++++++++++++++ 1 file changed, 190 insertions(+) create mode 100644 src/org/sosy_lab/java_smt/solvers/cvc5/CVC5ProofRule.java 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..b73ded009d --- /dev/null +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5ProofRule.java @@ -0,0 +1,190 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2024 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_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; + private final String formula; + + CVC5ProofRule(String pName, String pFormula) { + name = pName; + formula = pFormula; + } + + @Override + public String getName() { + return name; + } + + @Override + public String getFormula() { + return formula; + } +} From 1b79e82697c085ea078fa65f67ec56b14e118e4a Mon Sep 17 00:00:00 2001 From: Gabriel Carpio Date: Sat, 20 Dec 2025 09:28:50 +0100 Subject: [PATCH 09/44] Added class `CV5Proof` which extends `AbstractProof`. `generateProofImpl` handles transformation from the solver's native proof into the common `Proof`. --- .../java_smt/solvers/cvc5/CVC5Proof.java | 109 ++++++++++++++++++ 1 file changed, 109 insertions(+) create mode 100644 src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Proof.java 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..5fd2f2e197 --- /dev/null +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Proof.java @@ -0,0 +1,109 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2024 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.solvers.cvc5; + +import io.github.cvc5.CVC5ApiException; +import io.github.cvc5.Term; +import java.util.ArrayDeque; +import java.util.Deque; +import java.util.HashMap; +import java.util.Map; +import org.sosy_lab.java_smt.api.Formula; +import org.sosy_lab.java_smt.api.proofs.Proof; +import org.sosy_lab.java_smt.api.proofs.ProofFrame; +import org.sosy_lab.java_smt.api.proofs.ProofRule; + +public class CVC5Proof extends org.sosy_lab.java_smt.basicimpl.AbstractProof { + + static CVC5Proof generateProofImpl(io.github.cvc5.Proof pProof, CVC5FormulaCreator formulaCreator) + throws CVC5ApiException { + + // boolean skippedScope = false; + + Deque stack = new ArrayDeque<>(); + + Map computed = new HashMap<>(); + + stack.push(new CVC5Frame(pProof)); + + while (!stack.isEmpty()) { + CVC5Frame frame = stack.peek(); + + if (!frame.isVisited()) { + + frame.setNumArgs(frame.getProof().getChildren().length); + frame.setAsVisited(true); + + 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(); + + // if (frame.getProof().getRule().getValue() == 1 && !skippedScope) { + // Skip processing the frame if its rule is "SCOPE" + // This rule seems to just help the processing by CVC5 + // pProof = changeRoot(frame.getProof()); + // skippedScope = true; + // continue; + // } + + CVC5ProofRule proofRule = + Enum.valueOf(CVC5ProofRule.class, frame.getProof().getRule().toString()); + // ProofRule.fromName( + // CVC5ProofRule.class, frame.getProof().getRule().toString().toLowerCase()); + + // Generate formula + Term term = frame.getProof().getResult(); + Formula pFormula = formulaCreator.encapsulate(formulaCreator.getFormulaType(term), term); + CVC5Proof pn = new CVC5Proof(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)); + } + } + computed.put(frame.getProof(), pn); + } + } + return computed.get(pProof); + } + + private static class CVC5Frame extends ProofFrame { + CVC5Frame(io.github.cvc5.Proof proof) { + super(proof); + } + } + + public CVC5Proof(ProofRule pProofRule, Formula formula) { + + super(pProofRule, formula); + } + + @Override + protected void addChild(Proof pProof) { + super.addChild(pProof); + } + + // private static Proof changeRoot(Proof root) { + // return root.getArguments()[0]; + // } + + @Override + public String proofAsString() { + return super.proofAsString(); + } +} From 9f2ac63bef0209dcb24c747546f886cc8a21c698 Mon Sep 17 00:00:00 2001 From: Gabriel Carpio Date: Sat, 20 Dec 2025 09:32:30 +0100 Subject: [PATCH 10/44] Added method `requireProofGeneration` to `SolverBasedTest0`. --- src/org/sosy_lab/java_smt/test/SolverBasedTest0.java | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java b/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java index 901452e8d7..481e955e6f 100644 --- a/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java +++ b/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java @@ -406,6 +406,15 @@ 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, Solvers.OPENSMT, Solvers.SMTINTERPOL); + } + /** * Use this for checking assertions about BooleanFormulas with Truth: * assertThatFormula(formula).is...(). From dcc728a8ca567ce12d3d70a6b6d026e37dd7d13a Mon Sep 17 00:00:00 2001 From: Gabriel Carpio Date: Sat, 20 Dec 2025 10:05:26 +0100 Subject: [PATCH 11/44] In `ProverEnvironmentTest` added multiple methods for testing retrieving common `Proof`s from solvers. Conditions include: different theories, trivial proofs, simple proofs, not enabling proof production, etc. --- .../java_smt/test/ProverEnvironmentTest.java | 497 ++++++++++++++++++ 1 file changed, 497 insertions(+) diff --git a/src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java b/src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java index 4364dfae74..66b2365507 100644 --- a/src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java +++ b/src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java @@ -10,26 +10,52 @@ import static com.google.common.truth.Truth.assertThat; import static com.google.common.truth.TruthJUnit.assume; +import static org.junit.Assert.assertNotEquals; import static org.junit.Assert.assertThrows; +import static org.junit.Assert.assertTrue; import static org.sosy_lab.java_smt.SolverContextFactory.Solvers.CVC4; import static org.sosy_lab.java_smt.SolverContextFactory.Solvers.CVC5; 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.SolverContextFactory.Solvers.SMTINTERPOL; +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.Proof; +import org.sosy_lab.java_smt.api.proofs.ProofRule; +import org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaSolverContext; +import org.sosy_lab.java_smt.solvers.boolector.BoolectorSolverContext; +import org.sosy_lab.java_smt.solvers.cvc4.CVC4SolverContext; +import org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5SolverContext; +import org.sosy_lab.java_smt.solvers.opensmt.OpenSmtSolverContext; +import org.sosy_lab.java_smt.solvers.princess.PrincessSolverContext; +import org.sosy_lab.java_smt.solvers.smtinterpol.SmtInterpolSolverContext; +import org.sosy_lab.java_smt.solvers.yices2.Yices2SolverContext; +import org.sosy_lab.java_smt.solvers.z3.Z3SolverContext; public class ProverEnvironmentTest extends SolverBasedTest0.ParameterizedSolverBasedTest0 { @@ -189,4 +215,475 @@ private void checkSimpleQuery(ProverEnvironment pProver) pProver.pop(); } } + + @Test + public void testGetSimpleBooleanProof() throws InterruptedException, SolverException { + 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() + Proof proof = prover.getProof(); + checkProof(proof); + + } catch (UnsupportedOperationException e) { + assertThat(e) + .hasMessageThat() + .isEqualTo("Proof generation is not available for the current solver."); + Class contextClass = context.getClass(); + boolean isExpected = + contextClass.equals(CVC4SolverContext.class) + || contextClass.equals(OpenSmtSolverContext.class) + || contextClass.equals(BoolectorSolverContext.class) + || contextClass.equals(BitwuzlaSolverContext.class) + || contextClass.equals(Yices2SolverContext.class) + || contextClass.equals(PrincessSolverContext.class) + || contextClass.equals(Mathsat5SolverContext.class) + || contextClass.equals(Z3SolverContext.class) + || contextClass.equals(SmtInterpolSolverContext.class); + assertThat(isExpected).isTrue(); + } + } + + @Test + public void testGetComplexRationalNumeralAndUFProof() + throws InterruptedException, SolverException { + 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))); + assertTrue(prover.isUnsat()); + + // Retrieve and verify proof + Proof proof = prover.getProof(); + checkProof(proof); + + } catch (UnsupportedOperationException e) { + assertThat(e) + .hasMessageThat() + .isEqualTo("Proof generation is not available for the current solver."); + Class contextClass = context.getClass(); + boolean isExpected = + contextClass.equals(CVC4SolverContext.class) + || contextClass.equals(OpenSmtSolverContext.class) + || contextClass.equals(BoolectorSolverContext.class) + || contextClass.equals(BitwuzlaSolverContext.class) + || contextClass.equals(Yices2SolverContext.class) + || contextClass.equals(PrincessSolverContext.class) + || contextClass.equals(Mathsat5SolverContext.class) + || contextClass.equals(Z3SolverContext.class) + || contextClass.equals(SmtInterpolSolverContext.class); + assertThat(isExpected).isTrue(); + } + } + + @Test + public void proofOfTrueTest() throws InterruptedException, SolverException { + requireProofGeneration(); + + BooleanFormula tru = bmgr.makeTrue(); + + try (ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_PROOFS)) { + prover.addConstraint(tru); + assertThat(prover.isUnsat()).isFalse(); + + Proof proof = prover.getProof(); + assertThat(proof).isNotNull(); + + } catch (UnsupportedOperationException e) { + assertThat(e) + .hasMessageThat() + .isEqualTo("Proof generation is not available for the current solver."); + Class contextClass = context.getClass(); + boolean isExpected = + contextClass.equals(CVC4SolverContext.class) + || contextClass.equals(BoolectorSolverContext.class) + || contextClass.equals(BitwuzlaSolverContext.class) + || contextClass.equals(Yices2SolverContext.class) + || contextClass.equals(PrincessSolverContext.class) + || contextClass.equals(Mathsat5SolverContext.class) + || contextClass.equals(Z3SolverContext.class) + || contextClass.equals(SmtInterpolSolverContext.class); + assertThat(isExpected).isTrue(); + } catch (IllegalStateException ie) { + // this should be thrown as getProof was called when last evaluation was SAT + } + } + + @Test + public void proofOfFalseTest() throws InterruptedException, SolverException { + requireProofGeneration(); + // assume().that(solverToUse()).isNotEqualTo(MATHSAT5); + + BooleanFormula bottom = bmgr.makeFalse(); + + try (ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_PROOFS)) { + prover.addConstraint(bottom); + assertThat(prover.isUnsat()).isTrue(); + + Proof proof = prover.getProof(); + assertThat(proof).isNotNull(); + + } catch (UnsupportedOperationException e) { + if (solverToUse().equals(MATHSAT5)) { + assertThat(e).hasMessageThat().isEqualTo("No proof available."); + + } else { + assertThat(e) + .hasMessageThat() + .isEqualTo("Proof generation is not available for the current solver."); + } + Class contextClass = context.getClass(); + boolean isExpected = + contextClass.equals(CVC4SolverContext.class) + || contextClass.equals(OpenSmtSolverContext.class) + || contextClass.equals(BoolectorSolverContext.class) + || contextClass.equals(BitwuzlaSolverContext.class) + || contextClass.equals(Yices2SolverContext.class) + || contextClass.equals(PrincessSolverContext.class) + || contextClass.equals(Mathsat5SolverContext.class) + || contextClass.equals(Z3SolverContext.class) + || contextClass.equals(SmtInterpolSolverContext.class); + assertThat(isExpected).isTrue(); + } catch (IllegalStateException ie) { + // this should be thrown as getProof was called when last evaluation was SAT + } + } + + @Test + public void testGetSimpleIntegerProof() throws InterruptedException, SolverException { + 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() + Proof proof = prover.getProof(); + checkProof(proof); + + } catch (UnsupportedOperationException e) { + assertThat(e) + .hasMessageThat() + .isEqualTo("Proof generation is not available for the current solver."); + Class contextClass = context.getClass(); + boolean isExpected = + contextClass.equals(CVC4SolverContext.class) + || contextClass.equals(OpenSmtSolverContext.class) + || contextClass.equals(BoolectorSolverContext.class) + || contextClass.equals(BitwuzlaSolverContext.class) + || contextClass.equals(Yices2SolverContext.class) + || contextClass.equals(PrincessSolverContext.class) + || contextClass.equals(Mathsat5SolverContext.class) + || contextClass.equals(Z3SolverContext.class) + || contextClass.equals(SmtInterpolSolverContext.class); + assertThat(isExpected).isTrue(); + } + } + + @Test + public void getProofAfterGetProofAndAddingAssertionsTest() + throws InterruptedException, SolverException { + 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() + Proof proof = prover.getProof(); + checkProof(proof); + + // assert integer formulas and test again + prover.addConstraint(imgr.equal(x1, two)); + prover.addConstraint(imgr.lessThan(x1, cero)); + + assertThat(prover.isUnsat()).isTrue(); + + // Test getProof() + Proof secondProof = prover.getProof(); + checkProof(secondProof); + + assertNotEquals(proof, secondProof); + + } catch (UnsupportedOperationException e) { + assertThat(e) + .hasMessageThat() + .isEqualTo("Proof generation is not available for the current solver."); + Class contextClass = context.getClass(); + boolean isExpected = + contextClass.equals(CVC4SolverContext.class) + || contextClass.equals(OpenSmtSolverContext.class) + || contextClass.equals(BoolectorSolverContext.class) + || contextClass.equals(BitwuzlaSolverContext.class) + || contextClass.equals(Yices2SolverContext.class) + || contextClass.equals(PrincessSolverContext.class) + || contextClass.equals(Mathsat5SolverContext.class) + || contextClass.equals(Z3SolverContext.class) + || contextClass.equals(SmtInterpolSolverContext.class); + assertThat(isExpected).isTrue(); + } + } + + // TODO: MathSAT5 produces a proof with a CLAUSE_HYP rule without children, investigate why this + // coudl be and how to process + @Test + public void getProofAfterGetProofClearingStackAndAddingDifferentAssertionsTest() + throws InterruptedException, SolverException { + 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() + Proof proof = prover.getProof(); + checkProof(proof); + + 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() + Proof secondProof = prover.getProof(); + checkProof(secondProof); + + assertNotEquals(proof, secondProof); + + } catch (UnsupportedOperationException e) { + assertThat(e) + .hasMessageThat() + .isEqualTo("Proof generation is not available for the current solver."); + Class contextClass = context.getClass(); + boolean isExpected = + contextClass.equals(CVC4SolverContext.class) + || contextClass.equals(OpenSmtSolverContext.class) + || contextClass.equals(BoolectorSolverContext.class) + || contextClass.equals(BitwuzlaSolverContext.class) + || contextClass.equals(Yices2SolverContext.class) + || contextClass.equals(PrincessSolverContext.class) + || contextClass.equals(Mathsat5SolverContext.class) + || contextClass.equals(Z3SolverContext.class) + || contextClass.equals(SmtInterpolSolverContext.class); + assertThat(isExpected).isTrue(); + } + } + + @Test + public void getProofWithoutProofProductionEnabledTest() + throws InterruptedException, SolverException { + requireProofGeneration(); + + BooleanFormula bottom = bmgr.makeFalse(); + + try (ProverEnvironment prover = context.newProverEnvironment()) { + prover.addConstraint(bottom); + assertThat(prover.isUnsat()).isTrue(); + + Proof proof = prover.getProof(); + + // Z3 always has proof generation on + //if (solverToUse().equals(Z3)) { + // assertThat(proof.getFormula()).isNotNull(); + //} + + } catch (UnsupportedOperationException e) { + assertThat(e) + .hasMessageThat() + .isEqualTo("Proof generation is not available for the current solver."); + } catch (IllegalStateException e) { + assertThat(e).hasMessageThat().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 { + 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() + Proof proof = prover.getProof(); + checkProof(proof); + } + } + + // This test is based on the testIntIndexIntValue() test in ArrayFormulaManagerTest + @Test + public void getArrayProofTest() throws InterruptedException, SolverException { + 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() + Proof proof = prover.getProof(); + checkProof(proof); + } + } + + // Traverses a proof and asserts that certain values are not null, instances, etc. + private void checkProof(Proof root) { + assertThat(root).isNotNull(); + + Deque stack = new ArrayDeque<>(); + stack.push(root); + + while (!stack.isEmpty()) { + Proof proof = stack.pop(); + ProofRule rule = proof.getRule(); + Optional formula = proof.getFormula(); + + assertThat(rule).isNotNull(); + assertThat(rule).isInstanceOf(ProofRule.class); + assertThat(proof.getChildren()).isNotNull(); + if (solverToUse().equals(SMTINTERPOL)) { + + } else if (solverToUse().equals(PRINCESS)) { + assertThat(formula.isEmpty()).isTrue(); + } else if (solverToUse().equals(MATHSAT5) || solverToUse().equals(OPENSMT)) { + // do nothing, optional proof may not provide a formula + } else { + assertThat(formula.isPresent()).isTrue(); + } + + //if (solverToUse().equals(PRINCESS) && rule instanceof PrincessProofRule) { + // checkPrincessSpecificFields((PrincessProofRule) rule); + //} + + for (Proof child : proof.getChildren()) { + assertThat(child).isNotNull(); + stack.push(child); + } + } + } } From f8494378b2262a3cd89d6b744a47a8a6675e120c Mon Sep 17 00:00:00 2001 From: Gabriel Carpio Date: Sat, 10 Jan 2026 16:41:27 +0100 Subject: [PATCH 12/44] In `ProverEnvironmentTest` fixed "MissingFail" and "UnusedVariable" warnings. --- .../java_smt/test/ProverEnvironmentTest.java | 165 ++---------------- 1 file changed, 19 insertions(+), 146 deletions(-) diff --git a/src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java b/src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java index 66b2365507..0b318f758d 100644 --- a/src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java +++ b/src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java @@ -13,6 +13,7 @@ import static org.junit.Assert.assertNotEquals; import static org.junit.Assert.assertThrows; import static org.junit.Assert.assertTrue; +import static org.junit.Assert.fail; import static org.sosy_lab.java_smt.SolverContextFactory.Solvers.CVC4; import static org.sosy_lab.java_smt.SolverContextFactory.Solvers.CVC5; import static org.sosy_lab.java_smt.SolverContextFactory.Solvers.MATHSAT5; @@ -47,15 +48,6 @@ import org.sosy_lab.java_smt.api.SolverException; import org.sosy_lab.java_smt.api.proofs.Proof; import org.sosy_lab.java_smt.api.proofs.ProofRule; -import org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaSolverContext; -import org.sosy_lab.java_smt.solvers.boolector.BoolectorSolverContext; -import org.sosy_lab.java_smt.solvers.cvc4.CVC4SolverContext; -import org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5SolverContext; -import org.sosy_lab.java_smt.solvers.opensmt.OpenSmtSolverContext; -import org.sosy_lab.java_smt.solvers.princess.PrincessSolverContext; -import org.sosy_lab.java_smt.solvers.smtinterpol.SmtInterpolSolverContext; -import org.sosy_lab.java_smt.solvers.yices2.Yices2SolverContext; -import org.sosy_lab.java_smt.solvers.z3.Z3SolverContext; public class ProverEnvironmentTest extends SolverBasedTest0.ParameterizedSolverBasedTest0 { @@ -218,6 +210,7 @@ private void checkSimpleQuery(ProverEnvironment pProver) @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"); @@ -232,29 +225,13 @@ public void testGetSimpleBooleanProof() throws InterruptedException, SolverExcep // Test getProof() Proof proof = prover.getProof(); checkProof(proof); - - } catch (UnsupportedOperationException e) { - assertThat(e) - .hasMessageThat() - .isEqualTo("Proof generation is not available for the current solver."); - Class contextClass = context.getClass(); - boolean isExpected = - contextClass.equals(CVC4SolverContext.class) - || contextClass.equals(OpenSmtSolverContext.class) - || contextClass.equals(BoolectorSolverContext.class) - || contextClass.equals(BitwuzlaSolverContext.class) - || contextClass.equals(Yices2SolverContext.class) - || contextClass.equals(PrincessSolverContext.class) - || contextClass.equals(Mathsat5SolverContext.class) - || contextClass.equals(Z3SolverContext.class) - || contextClass.equals(SmtInterpolSolverContext.class); - assertThat(isExpected).isTrue(); } } @Test public void testGetComplexRationalNumeralAndUFProof() throws InterruptedException, SolverException { + assume().that(solverToUse()).isEqualTo(CVC5); requireProofGeneration(); // Ensures proofs are supported requireRationals(); @@ -313,28 +290,12 @@ public void testGetComplexRationalNumeralAndUFProof() // Retrieve and verify proof Proof proof = prover.getProof(); checkProof(proof); - - } catch (UnsupportedOperationException e) { - assertThat(e) - .hasMessageThat() - .isEqualTo("Proof generation is not available for the current solver."); - Class contextClass = context.getClass(); - boolean isExpected = - contextClass.equals(CVC4SolverContext.class) - || contextClass.equals(OpenSmtSolverContext.class) - || contextClass.equals(BoolectorSolverContext.class) - || contextClass.equals(BitwuzlaSolverContext.class) - || contextClass.equals(Yices2SolverContext.class) - || contextClass.equals(PrincessSolverContext.class) - || contextClass.equals(Mathsat5SolverContext.class) - || contextClass.equals(Z3SolverContext.class) - || contextClass.equals(SmtInterpolSolverContext.class); - assertThat(isExpected).isTrue(); } } @Test public void proofOfTrueTest() throws InterruptedException, SolverException { + assume().that(solverToUse()).isEqualTo(CVC5); requireProofGeneration(); BooleanFormula tru = bmgr.makeTrue(); @@ -344,32 +305,19 @@ public void proofOfTrueTest() throws InterruptedException, SolverException { assertThat(prover.isUnsat()).isFalse(); Proof proof = prover.getProof(); + fail("Expected IllegalStateException was not thrown"); assertThat(proof).isNotNull(); - } catch (UnsupportedOperationException e) { - assertThat(e) - .hasMessageThat() - .isEqualTo("Proof generation is not available for the current solver."); - Class contextClass = context.getClass(); - boolean isExpected = - contextClass.equals(CVC4SolverContext.class) - || contextClass.equals(BoolectorSolverContext.class) - || contextClass.equals(BitwuzlaSolverContext.class) - || contextClass.equals(Yices2SolverContext.class) - || contextClass.equals(PrincessSolverContext.class) - || contextClass.equals(Mathsat5SolverContext.class) - || contextClass.equals(Z3SolverContext.class) - || contextClass.equals(SmtInterpolSolverContext.class); - assertThat(isExpected).isTrue(); } catch (IllegalStateException ie) { - // this should be thrown as getProof was called when last evaluation was SAT + // this should be thrown as getProof was called when last evaluation + // was SAT } } @Test public void proofOfFalseTest() throws InterruptedException, SolverException { requireProofGeneration(); - // assume().that(solverToUse()).isNotEqualTo(MATHSAT5); + assume().that(solverToUse()).isEqualTo(CVC5); BooleanFormula bottom = bmgr.makeFalse(); @@ -379,35 +327,12 @@ public void proofOfFalseTest() throws InterruptedException, SolverException { Proof proof = prover.getProof(); assertThat(proof).isNotNull(); - - } catch (UnsupportedOperationException e) { - if (solverToUse().equals(MATHSAT5)) { - assertThat(e).hasMessageThat().isEqualTo("No proof available."); - - } else { - assertThat(e) - .hasMessageThat() - .isEqualTo("Proof generation is not available for the current solver."); - } - Class contextClass = context.getClass(); - boolean isExpected = - contextClass.equals(CVC4SolverContext.class) - || contextClass.equals(OpenSmtSolverContext.class) - || contextClass.equals(BoolectorSolverContext.class) - || contextClass.equals(BitwuzlaSolverContext.class) - || contextClass.equals(Yices2SolverContext.class) - || contextClass.equals(PrincessSolverContext.class) - || contextClass.equals(Mathsat5SolverContext.class) - || contextClass.equals(Z3SolverContext.class) - || contextClass.equals(SmtInterpolSolverContext.class); - assertThat(isExpected).isTrue(); - } catch (IllegalStateException ie) { - // this should be thrown as getProof was called when last evaluation was SAT } } @Test public void testGetSimpleIntegerProof() throws InterruptedException, SolverException { + assume().that(solverToUse()).isEqualTo(CVC5); requireProofGeneration(); // Ensures proofs are supported requireIntegers(); @@ -423,29 +348,13 @@ public void testGetSimpleIntegerProof() throws InterruptedException, SolverExcep // Test getProof() Proof proof = prover.getProof(); checkProof(proof); - - } catch (UnsupportedOperationException e) { - assertThat(e) - .hasMessageThat() - .isEqualTo("Proof generation is not available for the current solver."); - Class contextClass = context.getClass(); - boolean isExpected = - contextClass.equals(CVC4SolverContext.class) - || contextClass.equals(OpenSmtSolverContext.class) - || contextClass.equals(BoolectorSolverContext.class) - || contextClass.equals(BitwuzlaSolverContext.class) - || contextClass.equals(Yices2SolverContext.class) - || contextClass.equals(PrincessSolverContext.class) - || contextClass.equals(Mathsat5SolverContext.class) - || contextClass.equals(Z3SolverContext.class) - || contextClass.equals(SmtInterpolSolverContext.class); - assertThat(isExpected).isTrue(); } } @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"); @@ -475,23 +384,6 @@ public void getProofAfterGetProofAndAddingAssertionsTest() checkProof(secondProof); assertNotEquals(proof, secondProof); - - } catch (UnsupportedOperationException e) { - assertThat(e) - .hasMessageThat() - .isEqualTo("Proof generation is not available for the current solver."); - Class contextClass = context.getClass(); - boolean isExpected = - contextClass.equals(CVC4SolverContext.class) - || contextClass.equals(OpenSmtSolverContext.class) - || contextClass.equals(BoolectorSolverContext.class) - || contextClass.equals(BitwuzlaSolverContext.class) - || contextClass.equals(Yices2SolverContext.class) - || contextClass.equals(PrincessSolverContext.class) - || contextClass.equals(Mathsat5SolverContext.class) - || contextClass.equals(Z3SolverContext.class) - || contextClass.equals(SmtInterpolSolverContext.class); - assertThat(isExpected).isTrue(); } } @@ -500,6 +392,7 @@ public void getProofAfterGetProofAndAddingAssertionsTest() @Test public void getProofAfterGetProofClearingStackAndAddingDifferentAssertionsTest() throws InterruptedException, SolverException { + assume().that(solverToUse()).isEqualTo(CVC5); requireProofGeneration(); // Ensures proofs are supported requireIntegers(); @@ -536,23 +429,6 @@ public void getProofAfterGetProofClearingStackAndAddingDifferentAssertionsTest() checkProof(secondProof); assertNotEquals(proof, secondProof); - - } catch (UnsupportedOperationException e) { - assertThat(e) - .hasMessageThat() - .isEqualTo("Proof generation is not available for the current solver."); - Class contextClass = context.getClass(); - boolean isExpected = - contextClass.equals(CVC4SolverContext.class) - || contextClass.equals(OpenSmtSolverContext.class) - || contextClass.equals(BoolectorSolverContext.class) - || contextClass.equals(BitwuzlaSolverContext.class) - || contextClass.equals(Yices2SolverContext.class) - || contextClass.equals(PrincessSolverContext.class) - || contextClass.equals(Mathsat5SolverContext.class) - || contextClass.equals(Z3SolverContext.class) - || contextClass.equals(SmtInterpolSolverContext.class); - assertThat(isExpected).isTrue(); } } @@ -567,25 +443,21 @@ public void getProofWithoutProofProductionEnabledTest() prover.addConstraint(bottom); assertThat(prover.isUnsat()).isTrue(); + @SuppressWarnings("unused") Proof proof = prover.getProof(); + fail("Expected IllegalStateException was not thrown"); // Z3 always has proof generation on - //if (solverToUse().equals(Z3)) { + // if (solverToUse().equals(Z3)) { // assertThat(proof.getFormula()).isNotNull(); - //} - - } catch (UnsupportedOperationException e) { - assertThat(e) - .hasMessageThat() - .isEqualTo("Proof generation is not available for the current solver."); - } catch (IllegalStateException e) { - assertThat(e).hasMessageThat().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(); @@ -625,6 +497,7 @@ public void getBitVectorProofTest() throws InterruptedException, SolverException // 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(); @@ -676,9 +549,9 @@ private void checkProof(Proof root) { assertThat(formula.isPresent()).isTrue(); } - //if (solverToUse().equals(PRINCESS) && rule instanceof PrincessProofRule) { + // if (solverToUse().equals(PRINCESS) && rule instanceof PrincessProofRule) { // checkPrincessSpecificFields((PrincessProofRule) rule); - //} + // } for (Proof child : proof.getChildren()) { assertThat(child).isNotNull(); From 7abe58117ac7e59662d8a80c44b2fd0df1024bf1 Mon Sep 17 00:00:00 2001 From: Gabriel Carpio Date: Sat, 10 Jan 2026 18:38:04 +0100 Subject: [PATCH 13/44] Added file `package-info.java` to package `proofs`. --- .../sosy_lab/java_smt/api/proofs/package-info.java | 14 ++++++++++++++ 1 file changed, 14 insertions(+) create mode 100644 src/org/sosy_lab/java_smt/api/proofs/package-info.java 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..1d2d7f8a4b --- /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: 2024 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; From f1fa31abeaf70671080768ea75a5b43c9e8fff67 Mon Sep 17 00:00:00 2001 From: Gabriel Carpio Date: Sat, 10 Jan 2026 18:39:01 +0100 Subject: [PATCH 14/44] Added missing documentation in interface `Proof`. --- src/org/sosy_lab/java_smt/api/proofs/Proof.java | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/src/org/sosy_lab/java_smt/api/proofs/Proof.java b/src/org/sosy_lab/java_smt/api/proofs/Proof.java index 11beab6aa5..13ba501d39 100644 --- a/src/org/sosy_lab/java_smt/api/proofs/Proof.java +++ b/src/org/sosy_lab/java_smt/api/proofs/Proof.java @@ -16,14 +16,17 @@ /** * A proof node in the proof DAG of a proof. - * - * @author Gabriel Carpio */ public interface Proof { /** Get the children of the proof node. */ Set getChildren(); + /** + * Check if the proof node is a leaf. + * + * @return True if the proof node is a leaf, false otherwise. + */ boolean isLeaf(); /** @@ -33,5 +36,10 @@ public interface Proof { */ Optional getFormula(); + /** + * Get the rule of the proof node. + * + * @return The rule of the proof node. + */ ProofRule getRule(); } From f5e33763879f7c767f86bdc2af42b9f9febf942b Mon Sep 17 00:00:00 2001 From: Gabriel Carpio Date: Sat, 10 Jan 2026 18:39:48 +0100 Subject: [PATCH 15/44] Fixed multiple checkstyle warnings. --- .../java_smt/test/ProverEnvironmentTest.java | 21 +++++++++---------- 1 file changed, 10 insertions(+), 11 deletions(-) diff --git a/src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java b/src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java index 0b318f758d..079d35d677 100644 --- a/src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java +++ b/src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java @@ -10,10 +10,7 @@ import static com.google.common.truth.Truth.assertThat; import static com.google.common.truth.TruthJUnit.assume; -import static org.junit.Assert.assertNotEquals; import static org.junit.Assert.assertThrows; -import static org.junit.Assert.assertTrue; -import static org.junit.Assert.fail; import static org.sosy_lab.java_smt.SolverContextFactory.Solvers.CVC4; import static org.sosy_lab.java_smt.SolverContextFactory.Solvers.CVC5; import static org.sosy_lab.java_smt.SolverContextFactory.Solvers.MATHSAT5; @@ -285,7 +282,7 @@ public void testGetComplexRationalNumeralAndUFProof() 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))); - assertTrue(prover.isUnsat()); + assertThat(prover.isUnsat()).isTrue(); // Retrieve and verify proof Proof proof = prover.getProof(); @@ -305,10 +302,10 @@ public void proofOfTrueTest() throws InterruptedException, SolverException { assertThat(prover.isUnsat()).isFalse(); Proof proof = prover.getProof(); - fail("Expected IllegalStateException was not thrown"); - assertThat(proof).isNotNull(); + throw new AssertionError("Expected IllegalStateException was not thrown"); + // assertThat(proof).isNotNull(); // unreachable - } catch (IllegalStateException ie) { + } catch (IllegalStateException e) { // this should be thrown as getProof was called when last evaluation // was SAT } @@ -383,7 +380,7 @@ public void getProofAfterGetProofAndAddingAssertionsTest() Proof secondProof = prover.getProof(); checkProof(secondProof); - assertNotEquals(proof, secondProof); + assertThat(proof).isNotEqualTo(secondProof); } } @@ -428,7 +425,7 @@ public void getProofAfterGetProofClearingStackAndAddingDifferentAssertionsTest() Proof secondProof = prover.getProof(); checkProof(secondProof); - assertNotEquals(proof, secondProof); + assertThat(proof).isNotEqualTo(secondProof); } } @@ -445,12 +442,14 @@ public void getProofWithoutProofProductionEnabledTest() @SuppressWarnings("unused") Proof proof = prover.getProof(); - fail("Expected IllegalStateException was not thrown"); + throw new AssertionError("Expected IllegalStateException was not thrown"); // Z3 always has proof generation on // if (solverToUse().equals(Z3)) { // assertThat(proof.getFormula()).isNotNull(); // } + } catch (IllegalStateException e) { + assertThat(e.getMessage()).isEqualTo("Please set the prover option GENERATE_PROOFS."); } } @@ -540,7 +539,7 @@ private void checkProof(Proof root) { assertThat(rule).isInstanceOf(ProofRule.class); assertThat(proof.getChildren()).isNotNull(); if (solverToUse().equals(SMTINTERPOL)) { - +// do nothing } else if (solverToUse().equals(PRINCESS)) { assertThat(formula.isEmpty()).isTrue(); } else if (solverToUse().equals(MATHSAT5) || solverToUse().equals(OPENSMT)) { From 27847d82ff7e4311ce230f448fc82af6c33c641a Mon Sep 17 00:00:00 2001 From: Gabriel Carpio Date: Sat, 10 Jan 2026 18:50:08 +0100 Subject: [PATCH 16/44] Formatting changes --- src/org/sosy_lab/java_smt/api/proofs/Proof.java | 4 +--- src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java | 2 +- 2 files changed, 2 insertions(+), 4 deletions(-) diff --git a/src/org/sosy_lab/java_smt/api/proofs/Proof.java b/src/org/sosy_lab/java_smt/api/proofs/Proof.java index 13ba501d39..2cecc501f0 100644 --- a/src/org/sosy_lab/java_smt/api/proofs/Proof.java +++ b/src/org/sosy_lab/java_smt/api/proofs/Proof.java @@ -14,9 +14,7 @@ import java.util.Set; import org.sosy_lab.java_smt.api.Formula; -/** - * A proof node in the proof DAG of a proof. - */ +/** A proof node in the proof DAG of a proof. */ public interface Proof { /** Get the children of the proof node. */ diff --git a/src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java b/src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java index 079d35d677..928415557e 100644 --- a/src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java +++ b/src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java @@ -539,7 +539,7 @@ private void checkProof(Proof root) { assertThat(rule).isInstanceOf(ProofRule.class); assertThat(proof.getChildren()).isNotNull(); if (solverToUse().equals(SMTINTERPOL)) { -// do nothing + // do nothing } else if (solverToUse().equals(PRINCESS)) { assertThat(formula.isEmpty()).isTrue(); } else if (solverToUse().equals(MATHSAT5) || solverToUse().equals(OPENSMT)) { From 8213c7afae9a814328a2e317dd176147fee0fcc1 Mon Sep 17 00:00:00 2001 From: Gabriel Carpio Date: Sat, 10 Jan 2026 18:50:46 +0100 Subject: [PATCH 17/44] Added `CVC5ProofRule` `CHAIN_M_RESOLUTION`. --- src/org/sosy_lab/java_smt/solvers/cvc5/CVC5ProofRule.java | 1 + 1 file changed, 1 insertion(+) diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5ProofRule.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5ProofRule.java index b73ded009d..7bf2c8d3f7 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5ProofRule.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5ProofRule.java @@ -36,6 +36,7 @@ enum CVC5ProofRule implements ProofRule { 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", ""), From 6a133f60c00830ec428509429f1a3ef9c11568d8 Mon Sep 17 00:00:00 2001 From: Gabriel Carpio Date: Sat, 10 Jan 2026 19:09:59 +0100 Subject: [PATCH 18/44] Implemented refaster suggestion. --- .../sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) 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 c800e48812..d70a1e6792 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java @@ -327,9 +327,7 @@ public Proof getProof() throws SolverException, InterruptedException { checkState(isUnsat()); io.github.cvc5.Proof[] proofs = solver.getProof(); - if (proofs == null || proofs.length == 0) { - throw new IllegalStateException("No proof available"); - } + checkState(proofs != null && proofs.length != 0, "No proof available"); // CVC5ProofProcessor pp = new CVC5ProofProcessor(creator); try { From 72c969762867e242e07ad542c7ed68c17d1f4c11 Mon Sep 17 00:00:00 2001 From: Gabriel Carpio Date: Sat, 10 Jan 2026 19:10:31 +0100 Subject: [PATCH 19/44] Fixed "unused" warning in `ProverEnvironmentTest`. --- src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java b/src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java index 928415557e..dd12b544bd 100644 --- a/src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java +++ b/src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java @@ -301,9 +301,9 @@ public void proofOfTrueTest() throws InterruptedException, SolverException { prover.addConstraint(tru); assertThat(prover.isUnsat()).isFalse(); + @SuppressWarnings("unused") Proof proof = prover.getProof(); throw new AssertionError("Expected IllegalStateException was not thrown"); - // assertThat(proof).isNotNull(); // unreachable } catch (IllegalStateException e) { // this should be thrown as getProof was called when last evaluation From 50a9b16edd6aca82ed0479992873e3c85efe5dc5 Mon Sep 17 00:00:00 2001 From: gcarpio21 Date: Fri, 16 Jan 2026 14:02:43 +0000 Subject: [PATCH 20/44] Removed unnecessary method from the `ProofRule` interface. --- .../java_smt/api/proofs/ProofRule.java | 5 - .../java_smt/solvers/cvc5/CVC5ProofRule.java | 320 +++++++++--------- 2 files changed, 157 insertions(+), 168 deletions(-) diff --git a/src/org/sosy_lab/java_smt/api/proofs/ProofRule.java b/src/org/sosy_lab/java_smt/api/proofs/ProofRule.java index 0199864eb5..eca73f0677 100644 --- a/src/org/sosy_lab/java_smt/api/proofs/ProofRule.java +++ b/src/org/sosy_lab/java_smt/api/proofs/ProofRule.java @@ -15,9 +15,4 @@ public interface ProofRule { /** Get the name of the proof rule. */ String getName(); - - /** Get the formula of the proof rule. */ - default String getFormula() { - return "no formula available"; - } } diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5ProofRule.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5ProofRule.java index 7bf2c8d3f7..b3d357db00 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5ProofRule.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5ProofRule.java @@ -14,169 +14,167 @@ // 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", ""); + 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; - private final String formula; - CVC5ProofRule(String pName, String pFormula) { + CVC5ProofRule(String pName){ name = pName; - formula = pFormula; } @Override @@ -184,8 +182,4 @@ public String getName() { return name; } - @Override - public String getFormula() { - return formula; - } } From ed64164dca14ee3c3b9cdeaec42af96e22c7a44c Mon Sep 17 00:00:00 2001 From: gcarpio21 Date: Tue, 20 Jan 2026 14:42:10 +0000 Subject: [PATCH 21/44] Proofs: Changed `children` in `AbstractProof` to type `ImmutableSet`. Deleted out-commented code. Deleted resolved TODO. --- .../java_smt/basicimpl/AbstractProof.java | 18 +++--------------- 1 file changed, 3 insertions(+), 15 deletions(-) diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractProof.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractProof.java index 849d2af692..a975121660 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProof.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProof.java @@ -3,14 +3,14 @@ * an API wrapper for a collection of SMT solvers: * https://github.com/sosy-lab/java-smt * - * SPDX-FileCopyrightText: 2024 Dirk Beyer + * SPDX-FileCopyrightText: 2026 Dirk Beyer * * SPDX-License-Identifier: Apache-2.0 */ package org.sosy_lab.java_smt.basicimpl; -import java.util.LinkedHashSet; +import com.google.common.collect.ImmutableSet; import java.util.Optional; import java.util.Set; import org.checkerframework.checker.nullness.qual.Nullable; @@ -25,14 +25,7 @@ */ public abstract class AbstractProof implements Proof { - // protected abstract class Transformation { - // protected Transformation( - // FormulaCreator formulaCreator, T proof) {} - - // protected abstract Proof generateProof(); - // } - - private final Set children = new LinkedHashSet<>(); + private final Set children = ImmutableSet.of(); private ProofRule rule; protected Optional formula = Optional.empty(); @@ -41,7 +34,6 @@ protected AbstractProof(ProofRule rule, @Nullable Formula formula) { this.formula = Optional.ofNullable(formula); } - // TODO: Use Optional instead of nullable @Override public Optional getFormula() { return this.formula; @@ -66,10 +58,6 @@ public boolean isLeaf() { return getChildren().isEmpty(); } - // void setRule(ProofRule rule) { - // this.rule = rule; - // } - public void setFormula(@Nullable Formula pFormula) { formula = Optional.ofNullable(pFormula); } From f037077fef22a10d915fbd656d48f94652e3d3e4 Mon Sep 17 00:00:00 2001 From: gcarpio21 Date: Tue, 20 Jan 2026 14:47:02 +0000 Subject: [PATCH 22/44] Proofs: Fixed year in copyright header. --- src/org/sosy_lab/java_smt/api/proofs/Proof.java | 2 +- src/org/sosy_lab/java_smt/api/proofs/ProofFrame.java | 2 +- src/org/sosy_lab/java_smt/api/proofs/ProofRule.java | 2 +- src/org/sosy_lab/java_smt/api/proofs/package-info.java | 2 +- src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Proof.java | 2 +- src/org/sosy_lab/java_smt/solvers/cvc5/CVC5ProofRule.java | 5 ++--- 6 files changed, 7 insertions(+), 8 deletions(-) diff --git a/src/org/sosy_lab/java_smt/api/proofs/Proof.java b/src/org/sosy_lab/java_smt/api/proofs/Proof.java index 2cecc501f0..e30b8e69a3 100644 --- a/src/org/sosy_lab/java_smt/api/proofs/Proof.java +++ b/src/org/sosy_lab/java_smt/api/proofs/Proof.java @@ -3,7 +3,7 @@ * an API wrapper for a collection of SMT solvers: * https://github.com/sosy-lab/java-smt * - * SPDX-FileCopyrightText: 2024 Dirk Beyer + * SPDX-FileCopyrightText: 2026 Dirk Beyer * * SPDX-License-Identifier: Apache-2.0 */ diff --git a/src/org/sosy_lab/java_smt/api/proofs/ProofFrame.java b/src/org/sosy_lab/java_smt/api/proofs/ProofFrame.java index 71677e7ef4..9f7e64d954 100644 --- a/src/org/sosy_lab/java_smt/api/proofs/ProofFrame.java +++ b/src/org/sosy_lab/java_smt/api/proofs/ProofFrame.java @@ -3,7 +3,7 @@ * an API wrapper for a collection of SMT solvers: * https://github.com/sosy-lab/java-smt * - * SPDX-FileCopyrightText: 2024 Dirk Beyer + * SPDX-FileCopyrightText: 2026 Dirk Beyer * * SPDX-License-Identifier: Apache-2.0 */ diff --git a/src/org/sosy_lab/java_smt/api/proofs/ProofRule.java b/src/org/sosy_lab/java_smt/api/proofs/ProofRule.java index eca73f0677..fa2499af8f 100644 --- a/src/org/sosy_lab/java_smt/api/proofs/ProofRule.java +++ b/src/org/sosy_lab/java_smt/api/proofs/ProofRule.java @@ -3,7 +3,7 @@ * an API wrapper for a collection of SMT solvers: * https://github.com/sosy-lab/java-smt * - * SPDX-FileCopyrightText: 2024 Dirk Beyer + * SPDX-FileCopyrightText: 2026 Dirk Beyer * * SPDX-License-Identifier: Apache-2.0 */ 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 index 1d2d7f8a4b..96e316567b 100644 --- a/src/org/sosy_lab/java_smt/api/proofs/package-info.java +++ b/src/org/sosy_lab/java_smt/api/proofs/package-info.java @@ -3,7 +3,7 @@ * an API wrapper for a collection of SMT solvers: * https://github.com/sosy-lab/java-smt * - * SPDX-FileCopyrightText: 2024 Dirk Beyer + * SPDX-FileCopyrightText: 2026 Dirk Beyer * * SPDX-License-Identifier: Apache-2.0 */ diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Proof.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Proof.java index 5fd2f2e197..58da05cb79 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Proof.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Proof.java @@ -3,7 +3,7 @@ * an API wrapper for a collection of SMT solvers: * https://github.com/sosy-lab/java-smt * - * SPDX-FileCopyrightText: 2024 Dirk Beyer + * SPDX-FileCopyrightText: 2026 Dirk Beyer * * SPDX-License-Identifier: Apache-2.0 */ diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5ProofRule.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5ProofRule.java index b3d357db00..b4107eec03 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5ProofRule.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5ProofRule.java @@ -3,7 +3,7 @@ * an API wrapper for a collection of SMT solvers: * https://github.com/sosy-lab/java-smt * - * SPDX-FileCopyrightText: 2024 Dirk Beyer + * SPDX-FileCopyrightText: 2026 Dirk Beyer * * SPDX-License-Identifier: Apache-2.0 */ @@ -173,7 +173,7 @@ enum CVC5ProofRule implements ProofRule { private final String name; - CVC5ProofRule(String pName){ + CVC5ProofRule(String pName) { name = pName; } @@ -181,5 +181,4 @@ enum CVC5ProofRule implements ProofRule { public String getName() { return name; } - } From 77d77a8f90fa08da49d87db7a12538d71df44b18 Mon Sep 17 00:00:00 2001 From: gcarpio21 Date: Tue, 20 Jan 2026 14:47:58 +0000 Subject: [PATCH 23/44] Fixed formatting --- .../sosy_lab/java_smt/basicimpl/AbstractProver.java | 4 ++-- src/org/sosy_lab/java_smt/test/SolverBasedTest0.java | 12 ++++++++++-- 2 files changed, 12 insertions(+), 4 deletions(-) diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java index a0328110d6..4da6a6d5c4 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java @@ -104,9 +104,9 @@ protected final void checkGenerateProofs() { Preconditions.checkState(generateProofs, TEMPLATE, ProverOptions.GENERATE_PROOFS); Preconditions.checkState(!closed); Preconditions.checkState(!changedSinceLastSatQuery); - Preconditions.checkState(!wasLastSatCheckSatisfiable); + Preconditions.checkState(!wasLastSatCheckSatisfiable); } - + protected final void checkGenerateInterpolants() { Preconditions.checkState(!closed); Preconditions.checkState( diff --git a/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java b/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java index 167221e266..d90fbbdc36 100644 --- a/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java +++ b/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java @@ -432,8 +432,16 @@ protected void requireProofGeneration() { .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, Solvers.OPENSMT, Solvers.SMTINTERPOL); + .isNoneOf( + Solvers.BOOLECTOR, + Solvers.BITWUZLA, + Solvers.YICES2, + Solvers.CVC4, + Solvers.PRINCESS, + Solvers.MATHSAT5, + Solvers.Z3, + Solvers.OPENSMT, + Solvers.SMTINTERPOL); } /** From c2cdbae81157f0a478208e20c8d26c8d7dcc9959 Mon Sep 17 00:00:00 2001 From: gcarpio21 Date: Tue, 20 Jan 2026 14:51:11 +0000 Subject: [PATCH 24/44] Proofs: fixed documentation for proof retrieval code. --- src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java | 5 +++-- src/org/sosy_lab/java_smt/api/SolverContext.java | 7 +------ 2 files changed, 4 insertions(+), 8 deletions(-) diff --git a/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java b/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java index 00d9d9989f..91cb67ff7d 100644 --- a/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java +++ b/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java @@ -162,8 +162,9 @@ default ImmutableMap getStatistics() { } /** - * Get proof of unsatisfiability of the conjuction of the current satck of all formulas. Should - * only be called after {@link #isUnsat()} returned true. + * 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; diff --git a/src/org/sosy_lab/java_smt/api/SolverContext.java b/src/org/sosy_lab/java_smt/api/SolverContext.java index 100eb55494..574dd6b2be 100644 --- a/src/org/sosy_lab/java_smt/api/SolverContext.java +++ b/src/org/sosy_lab/java_smt/api/SolverContext.java @@ -52,12 +52,7 @@ enum ProverOptions { */ GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS, - /** - * Whether the solver should generate proofs for unsatisfiable formulas. For Z3, this parameter - * is context(not solver)-based, so for setting it, the extra option in the {@link - * org.sosy_lab.common.configuration.Configuration} instance: "requireProofs" should be set to - * "true". - */ + /** Whether the solver should generate proofs for unsatisfiable formulas. */ GENERATE_PROOFS, /** Whether the solver should enable support for formulae build in SL theory. */ From ab4e4851dd3ba37c3a4026935caa17cdf4f12024 Mon Sep 17 00:00:00 2001 From: gcarpio21 Date: Tue, 20 Jan 2026 15:30:09 +0000 Subject: [PATCH 25/44] Proofs: added `Z3_WITH_INTERPOLATION` to the solvers to exclude during testing. --- src/org/sosy_lab/java_smt/test/SolverBasedTest0.java | 1 + 1 file changed, 1 insertion(+) diff --git a/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java b/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java index d90fbbdc36..a929a248a8 100644 --- a/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java +++ b/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java @@ -439,6 +439,7 @@ protected void requireProofGeneration() { Solvers.CVC4, Solvers.PRINCESS, Solvers.MATHSAT5, + Solvers.Z3_WITH_INTERPOLATION, Solvers.Z3, Solvers.OPENSMT, Solvers.SMTINTERPOL); From d1a18f96ad9afa5012bb6439a44f3e9c4279135e Mon Sep 17 00:00:00 2001 From: gcarpio21 Date: Tue, 20 Jan 2026 15:30:51 +0000 Subject: [PATCH 26/44] Revert "Proofs: Changed `children` in `AbstractProof` to type `ImmutableSet`. Deleted out-commented code. Deleted resolved TODO." This reverts commit ed64164dca14ee3c3b9cdeaec42af96e22c7a44c. --- .../java_smt/basicimpl/AbstractProof.java | 18 +++++++++++++++--- 1 file changed, 15 insertions(+), 3 deletions(-) diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractProof.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractProof.java index a975121660..849d2af692 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProof.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProof.java @@ -3,14 +3,14 @@ * an API wrapper for a collection of SMT solvers: * https://github.com/sosy-lab/java-smt * - * SPDX-FileCopyrightText: 2026 Dirk Beyer + * SPDX-FileCopyrightText: 2024 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; @@ -25,7 +25,14 @@ */ public abstract class AbstractProof implements Proof { - private final Set children = ImmutableSet.of(); + // protected abstract class Transformation { + // protected Transformation( + // FormulaCreator formulaCreator, T proof) {} + + // protected abstract Proof generateProof(); + // } + + private final Set children = new LinkedHashSet<>(); private ProofRule rule; protected Optional formula = Optional.empty(); @@ -34,6 +41,7 @@ protected AbstractProof(ProofRule rule, @Nullable Formula formula) { this.formula = Optional.ofNullable(formula); } + // TODO: Use Optional instead of nullable @Override public Optional getFormula() { return this.formula; @@ -58,6 +66,10 @@ public boolean isLeaf() { return getChildren().isEmpty(); } + // void setRule(ProofRule rule) { + // this.rule = rule; + // } + public void setFormula(@Nullable Formula pFormula) { formula = Optional.ofNullable(pFormula); } From 98daf50a401e80b25b0fa316cce8b50840248a49 Mon Sep 17 00:00:00 2001 From: gcarpio21 Date: Tue, 20 Jan 2026 15:32:07 +0000 Subject: [PATCH 27/44] Proofs: Fixed header year, deleted unneeded comments. --- .../sosy_lab/java_smt/basicimpl/AbstractProof.java | 14 +------------- 1 file changed, 1 insertion(+), 13 deletions(-) diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractProof.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractProof.java index 849d2af692..45b0a3fb81 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProof.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProof.java @@ -3,7 +3,7 @@ * an API wrapper for a collection of SMT solvers: * https://github.com/sosy-lab/java-smt * - * SPDX-FileCopyrightText: 2024 Dirk Beyer + * SPDX-FileCopyrightText: 2026 Dirk Beyer * * SPDX-License-Identifier: Apache-2.0 */ @@ -25,13 +25,6 @@ */ public abstract class AbstractProof implements Proof { - // protected abstract class Transformation { - // protected Transformation( - // FormulaCreator formulaCreator, T proof) {} - - // protected abstract Proof generateProof(); - // } - private final Set children = new LinkedHashSet<>(); private ProofRule rule; protected Optional formula = Optional.empty(); @@ -41,7 +34,6 @@ protected AbstractProof(ProofRule rule, @Nullable Formula formula) { this.formula = Optional.ofNullable(formula); } - // TODO: Use Optional instead of nullable @Override public Optional getFormula() { return this.formula; @@ -66,10 +58,6 @@ public boolean isLeaf() { return getChildren().isEmpty(); } - // void setRule(ProofRule rule) { - // this.rule = rule; - // } - public void setFormula(@Nullable Formula pFormula) { formula = Optional.ofNullable(pFormula); } From 71fbd4be32d97d8e36765731d4a4d3b1484ef34b Mon Sep 17 00:00:00 2001 From: gcarpio21 Date: Wed, 21 Jan 2026 13:38:38 +0000 Subject: [PATCH 28/44] Proofs: Field `children` of `AbstractProof` now is an `ImmutableSet`. --- src/org/sosy_lab/java_smt/basicimpl/AbstractProof.java | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractProof.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractProof.java index 45b0a3fb81..894e588c87 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProof.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProof.java @@ -10,6 +10,7 @@ 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; @@ -25,7 +26,7 @@ */ public abstract class AbstractProof implements Proof { - private final Set children = new LinkedHashSet<>(); + private Set children = ImmutableSet.of(); private ProofRule rule; protected Optional formula = Optional.empty(); @@ -45,7 +46,9 @@ public Set getChildren() { } protected void addChild(Proof child) { - this.children.add(child); + Set tempChildren = new LinkedHashSet<>(this.children); + tempChildren.add(child); + this.children = ImmutableSet.copyOf(tempChildren); } @Override From 0cdc9b0d444bf50fcac735fc9809c8e4876c2fe7 Mon Sep 17 00:00:00 2001 From: gcarpio21 Date: Thu, 22 Jan 2026 08:49:44 +0000 Subject: [PATCH 29/44] Proofs: Moved `ProofFrame` inside `AbstractProof`. Changed return type of `getChildren` to `ImmutableSet`. --- .../java_smt/api/proofs/ProofFrame.java | 53 ------------------- .../java_smt/basicimpl/AbstractProof.java | 40 +++++++++++++- 2 files changed, 38 insertions(+), 55 deletions(-) delete mode 100644 src/org/sosy_lab/java_smt/api/proofs/ProofFrame.java diff --git a/src/org/sosy_lab/java_smt/api/proofs/ProofFrame.java b/src/org/sosy_lab/java_smt/api/proofs/ProofFrame.java deleted file mode 100644 index 9f7e64d954..0000000000 --- a/src/org/sosy_lab/java_smt/api/proofs/ProofFrame.java +++ /dev/null @@ -1,53 +0,0 @@ -/* - * 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; - -/** - * Stores proof related information and gets stored in a stack when processing proofs. Each frame - * contains a proof object and the number of arguments it has. - * - * @param The type of the proof object. - */ -public abstract class ProofFrame { - final T proof; - int numArgs = 0; - boolean visited; - - protected ProofFrame(T proof) { - this.proof = proof; - 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(boolean isVisited) { - this.visited = isVisited; - } - - /** Set the number of arguments the proof object has. */ - public void setNumArgs(int numArgs) { - this.numArgs = numArgs; - } -} diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractProof.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractProof.java index 894e588c87..052a603d90 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProof.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProof.java @@ -26,7 +26,7 @@ */ public abstract class AbstractProof implements Proof { - private Set children = ImmutableSet.of(); + private ImmutableSet children = ImmutableSet.of(); private ProofRule rule; protected Optional formula = Optional.empty(); @@ -41,7 +41,7 @@ public Optional getFormula() { } @Override - public Set getChildren() { + public ImmutableSet getChildren() { return this.children; } @@ -98,4 +98,40 @@ protected String proofAsString(int indentLevel) { return sb.toString(); } + + protected abstract static class ProofFrame { + final T proof; + int numArgs = 0; + boolean visited; + + protected ProofFrame(T proof) { + this.proof = proof; + 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(boolean isVisited) { + this.visited = isVisited; + } + + /** Set the number of arguments the proof object has. */ + public void setNumArgs(int numArgs) { + this.numArgs = numArgs; + } + } } From 230924ac478d7fd8a44edaae7ad4f1a1524cdba6 Mon Sep 17 00:00:00 2001 From: gcarpio21 Date: Thu, 22 Jan 2026 08:50:32 +0000 Subject: [PATCH 30/44] Proofs: changed modifier of `CVC5Proof` constructor to private. --- src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Proof.java | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Proof.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Proof.java index 58da05cb79..1b36083303 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Proof.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Proof.java @@ -18,7 +18,6 @@ import java.util.Map; import org.sosy_lab.java_smt.api.Formula; import org.sosy_lab.java_smt.api.proofs.Proof; -import org.sosy_lab.java_smt.api.proofs.ProofFrame; import org.sosy_lab.java_smt.api.proofs.ProofRule; public class CVC5Proof extends org.sosy_lab.java_smt.basicimpl.AbstractProof { @@ -88,7 +87,7 @@ private static class CVC5Frame extends ProofFrame { } } - public CVC5Proof(ProofRule pProofRule, Formula formula) { + private CVC5Proof(ProofRule pProofRule, Formula formula) { super(pProofRule, formula); } From 47922a94c1fb12cca90c789aff0e4c7922ee238c Mon Sep 17 00:00:00 2001 From: gcarpio21 Date: Thu, 22 Jan 2026 08:53:38 +0000 Subject: [PATCH 31/44] Proofs: return type of `getChildren` from the general proof API changed to `ImmutableSet`. --- src/org/sosy_lab/java_smt/api/proofs/Proof.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/org/sosy_lab/java_smt/api/proofs/Proof.java b/src/org/sosy_lab/java_smt/api/proofs/Proof.java index e30b8e69a3..263cac8035 100644 --- a/src/org/sosy_lab/java_smt/api/proofs/Proof.java +++ b/src/org/sosy_lab/java_smt/api/proofs/Proof.java @@ -10,15 +10,15 @@ package org.sosy_lab.java_smt.api.proofs; +import com.google.common.collect.ImmutableSet; import java.util.Optional; -import java.util.Set; import org.sosy_lab.java_smt.api.Formula; /** A proof node in the proof DAG of a proof. */ public interface Proof { /** Get the children of the proof node. */ - Set getChildren(); + ImmutableSet getChildren(); /** * Check if the proof node is a leaf. From 7f94d1b557595a3f58dd7b62358a7be1cf76eee1 Mon Sep 17 00:00:00 2001 From: gcarpio21 Date: Thu, 22 Jan 2026 10:21:51 +0000 Subject: [PATCH 32/44] Proofs: renamed parameters, changed signatures and types in `AbstractProof` to comply with the Style & Coding Guide. --- .../java_smt/basicimpl/AbstractProof.java | 40 ++++++++----------- 1 file changed, 17 insertions(+), 23 deletions(-) diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractProof.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractProof.java index 052a603d90..83fc041667 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProof.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProof.java @@ -30,9 +30,9 @@ public abstract class AbstractProof implements Proof { private ProofRule rule; protected Optional formula = Optional.empty(); - protected AbstractProof(ProofRule rule, @Nullable Formula formula) { - this.rule = rule; - this.formula = Optional.ofNullable(formula); + protected AbstractProof(ProofRule pRule, @Nullable Formula pFormula) { + this.rule = pRule; + this.formula = Optional.ofNullable(pFormula); } @Override @@ -45,9 +45,9 @@ public ImmutableSet getChildren() { return this.children; } - protected void addChild(Proof child) { + protected void addChild(Proof pChild) { Set tempChildren = new LinkedHashSet<>(this.children); - tempChildren.add(child); + tempChildren.add(pChild); this.children = ImmutableSet.copyOf(tempChildren); } @@ -61,22 +61,16 @@ public boolean isLeaf() { return getChildren().isEmpty(); } - public void setFormula(@Nullable Formula pFormula) { - formula = Optional.ofNullable(pFormula); - } - - public void setRule(ProofRule pRule) { - rule = pRule; - } - - // use this for debugging + /** 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 indentLevel) { + protected String proofAsString(int pIndentLevel) { StringBuilder sb = new StringBuilder(); - String indent = " ".repeat(indentLevel); + String indent = " ".repeat(pIndentLevel); String sFormula = getFormula().map(Object::toString).orElse("null"); @@ -92,7 +86,7 @@ protected String proofAsString(int indentLevel) { if (!isLeaf()) { for (Proof child : getChildren()) { sb.append(indent).append("Child ").append(++i).append(":\n"); - sb.append(((AbstractProof) child).proofAsString(indentLevel + 1)); + sb.append(((AbstractProof) child).proofAsString(pIndentLevel + 1)); } } @@ -104,8 +98,8 @@ protected abstract static class ProofFrame { int numArgs = 0; boolean visited; - protected ProofFrame(T proof) { - this.proof = proof; + protected ProofFrame(T pProof) { + this.proof = pProof; this.visited = false; } @@ -125,13 +119,13 @@ public boolean isVisited() { } /** Set the frame as visited. */ - public void setAsVisited(boolean isVisited) { - this.visited = isVisited; + public void setAsVisited() { + this.visited = true; } /** Set the number of arguments the proof object has. */ - public void setNumArgs(int numArgs) { - this.numArgs = numArgs; + public void setNumArgs(int pNumArgs) { + this.numArgs = pNumArgs; } } } From 127a0af674f25a2821685bb10e328960c712d6fb Mon Sep 17 00:00:00 2001 From: gcarpio21 Date: Thu, 22 Jan 2026 12:42:40 +0000 Subject: [PATCH 33/44] Proofs: renamed parameters and changed types in `CVC5Proof` to comply with the Style & Coding Guide. --- .../java_smt/basicimpl/AbstractProof.java | 5 ++- .../java_smt/solvers/cvc5/CVC5Proof.java | 43 +++++++------------ 2 files changed, 19 insertions(+), 29 deletions(-) diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractProof.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractProof.java index 83fc041667..dfefd73078 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProof.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProof.java @@ -61,8 +61,9 @@ 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. + /** + * 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); diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Proof.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Proof.java index 1b36083303..4f5c5c9a2d 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Proof.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Proof.java @@ -10,26 +10,27 @@ 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.HashMap; +import java.util.LinkedHashMap; import java.util.Map; import org.sosy_lab.java_smt.api.Formula; import org.sosy_lab.java_smt.api.proofs.Proof; import org.sosy_lab.java_smt.api.proofs.ProofRule; +/** A proof of unsatisfiability returned by CVC5 transformed to the general proof API. */ public class CVC5Proof extends org.sosy_lab.java_smt.basicimpl.AbstractProof { - static CVC5Proof generateProofImpl(io.github.cvc5.Proof pProof, CVC5FormulaCreator formulaCreator) - throws CVC5ApiException { - - // boolean skippedScope = false; + static CVC5Proof generateProofImpl( + io.github.cvc5.Proof pProof, CVC5FormulaCreator pFormulaCreator) throws CVC5ApiException { Deque stack = new ArrayDeque<>(); + Map tempComputed; - Map computed = new HashMap<>(); + ImmutableMap computed = ImmutableMap.of(); stack.push(new CVC5Frame(pProof)); @@ -39,7 +40,7 @@ static CVC5Proof generateProofImpl(io.github.cvc5.Proof pProof, CVC5FormulaCreat if (!frame.isVisited()) { frame.setNumArgs(frame.getProof().getChildren().length); - frame.setAsVisited(true); + frame.setAsVisited(); for (int i = frame.getNumArgs() - 1; i >= 0; i--) { io.github.cvc5.Proof child = frame.getProof().getChildren()[i]; @@ -51,22 +52,12 @@ static CVC5Proof generateProofImpl(io.github.cvc5.Proof pProof, CVC5FormulaCreat stack.pop(); int numChildren = frame.getNumArgs(); - // if (frame.getProof().getRule().getValue() == 1 && !skippedScope) { - // Skip processing the frame if its rule is "SCOPE" - // This rule seems to just help the processing by CVC5 - // pProof = changeRoot(frame.getProof()); - // skippedScope = true; - // continue; - // } - CVC5ProofRule proofRule = Enum.valueOf(CVC5ProofRule.class, frame.getProof().getRule().toString()); - // ProofRule.fromName( - // CVC5ProofRule.class, frame.getProof().getRule().toString().toLowerCase()); // Generate formula Term term = frame.getProof().getResult(); - Formula pFormula = formulaCreator.encapsulate(formulaCreator.getFormulaType(term), term); + Formula pFormula = pFormulaCreator.encapsulate(pFormulaCreator.getFormulaType(term), term); CVC5Proof pn = new CVC5Proof(proofRule, pFormula); for (int i = 0; i < numChildren; i++) { io.github.cvc5.Proof child = frame.getProof().getChildren()[i]; @@ -75,7 +66,9 @@ static CVC5Proof generateProofImpl(io.github.cvc5.Proof pProof, CVC5FormulaCreat pn.addChild(computed.get(child)); } } - computed.put(frame.getProof(), pn); + tempComputed = new LinkedHashMap<>(computed); + tempComputed.put(frame.getProof(), pn); + computed = ImmutableMap.copyOf(tempComputed); } } return computed.get(pProof); @@ -87,20 +80,16 @@ private static class CVC5Frame extends ProofFrame { } } - private CVC5Proof(ProofRule pProofRule, Formula formula) { + private CVC5Proof(ProofRule pProofRule, Formula pFormula) { - super(pProofRule, formula); + super(pProofRule, pFormula); } @Override - protected void addChild(Proof pProof) { - super.addChild(pProof); + protected void addChild(Proof pChild) { + super.addChild(pChild); } - // private static Proof changeRoot(Proof root) { - // return root.getArguments()[0]; - // } - @Override public String proofAsString() { return super.proofAsString(); From e969884780673692e582127fb891d7189656d9d1 Mon Sep 17 00:00:00 2001 From: gcarpio21 Date: Thu, 22 Jan 2026 12:52:21 +0000 Subject: [PATCH 34/44] Proofs: renamed parameters in `ProverEnvironmentTest` to comply with the Style & Coding Guide, deleted unnecessary comments. --- .../java_smt/test/ProverEnvironmentTest.java | 26 +++---------------- 1 file changed, 4 insertions(+), 22 deletions(-) diff --git a/src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java b/src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java index dd12b544bd..e4d8aad2f3 100644 --- a/src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java +++ b/src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java @@ -384,8 +384,6 @@ public void getProofAfterGetProofAndAddingAssertionsTest() } } - // TODO: MathSAT5 produces a proof with a CLAUSE_HYP rule without children, investigate why this - // coudl be and how to process @Test public void getProofAfterGetProofClearingStackAndAddingDifferentAssertionsTest() throws InterruptedException, SolverException { @@ -444,10 +442,6 @@ public void getProofWithoutProofProductionEnabledTest() Proof proof = prover.getProof(); throw new AssertionError("Expected IllegalStateException was not thrown"); - // Z3 always has proof generation on - // if (solverToUse().equals(Z3)) { - // assertThat(proof.getFormula()).isNotNull(); - // } } catch (IllegalStateException e) { assertThat(e.getMessage()).isEqualTo("Please set the prover option GENERATE_PROOFS."); } @@ -524,11 +518,11 @@ public void getArrayProofTest() throws InterruptedException, SolverException { } // Traverses a proof and asserts that certain values are not null, instances, etc. - private void checkProof(Proof root) { - assertThat(root).isNotNull(); + private void checkProof(Proof pRoot) { + assertThat(pRoot).isNotNull(); Deque stack = new ArrayDeque<>(); - stack.push(root); + stack.push(pRoot); while (!stack.isEmpty()) { Proof proof = stack.pop(); @@ -538,19 +532,7 @@ private void checkProof(Proof root) { assertThat(rule).isNotNull(); assertThat(rule).isInstanceOf(ProofRule.class); assertThat(proof.getChildren()).isNotNull(); - if (solverToUse().equals(SMTINTERPOL)) { - // do nothing - } else if (solverToUse().equals(PRINCESS)) { - assertThat(formula.isEmpty()).isTrue(); - } else if (solverToUse().equals(MATHSAT5) || solverToUse().equals(OPENSMT)) { - // do nothing, optional proof may not provide a formula - } else { - assertThat(formula.isPresent()).isTrue(); - } - - // if (solverToUse().equals(PRINCESS) && rule instanceof PrincessProofRule) { - // checkPrincessSpecificFields((PrincessProofRule) rule); - // } + assertThat(formula.isPresent()).isTrue(); for (Proof child : proof.getChildren()) { assertThat(child).isNotNull(); From 1e01011e70c68d8596a966a0291ec771f61c1871 Mon Sep 17 00:00:00 2001 From: gcarpio21 Date: Mon, 26 Jan 2026 12:41:24 +0000 Subject: [PATCH 35/44] Proofs: made `CVC5` `final`. --- src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Proof.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Proof.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Proof.java index 4f5c5c9a2d..0613028947 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Proof.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Proof.java @@ -22,7 +22,7 @@ import org.sosy_lab.java_smt.api.proofs.ProofRule; /** A proof of unsatisfiability returned by CVC5 transformed to the general proof API. */ -public class CVC5Proof extends org.sosy_lab.java_smt.basicimpl.AbstractProof { +public final class CVC5Proof extends org.sosy_lab.java_smt.basicimpl.AbstractProof { static CVC5Proof generateProofImpl( io.github.cvc5.Proof pProof, CVC5FormulaCreator pFormulaCreator) throws CVC5ApiException { From c59874b39603bcb7f9d22c7cef60fc96978aeaa9 Mon Sep 17 00:00:00 2001 From: gcarpio21 Date: Mon, 26 Jan 2026 12:41:47 +0000 Subject: [PATCH 36/44] Proofs: removed unused import in `ProverEnvironmentTest`. --- src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java | 1 - 1 file changed, 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java b/src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java index e4d8aad2f3..c1427f6d01 100644 --- a/src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java +++ b/src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java @@ -16,7 +16,6 @@ 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.SolverContextFactory.Solvers.SMTINTERPOL; 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; From f750ce1a116809701e3d2efbdd1af038b26de591 Mon Sep 17 00:00:00 2001 From: gcarpio21 Date: Wed, 28 Jan 2026 13:39:36 +0000 Subject: [PATCH 37/44] Proofs: renamed helper function for testing in `ProverEnvironmentTest`. --- .../java_smt/test/ProverEnvironmentTest.java | 20 +++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java b/src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java index c1427f6d01..68955c4193 100644 --- a/src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java +++ b/src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java @@ -220,7 +220,7 @@ public void testGetSimpleBooleanProof() throws InterruptedException, SolverExcep // Test getProof() Proof proof = prover.getProof(); - checkProof(proof); + verifyProofObjectValidity(proof); } } @@ -285,7 +285,7 @@ public void testGetComplexRationalNumeralAndUFProof() // Retrieve and verify proof Proof proof = prover.getProof(); - checkProof(proof); + verifyProofObjectValidity(proof); } } @@ -343,7 +343,7 @@ public void testGetSimpleIntegerProof() throws InterruptedException, SolverExcep // Test getProof() Proof proof = prover.getProof(); - checkProof(proof); + verifyProofObjectValidity(proof); } } @@ -367,7 +367,7 @@ public void getProofAfterGetProofAndAddingAssertionsTest() // Test getProof() Proof proof = prover.getProof(); - checkProof(proof); + verifyProofObjectValidity(proof); // assert integer formulas and test again prover.addConstraint(imgr.equal(x1, two)); @@ -377,7 +377,7 @@ public void getProofAfterGetProofAndAddingAssertionsTest() // Test getProof() Proof secondProof = prover.getProof(); - checkProof(secondProof); + verifyProofObjectValidity(secondProof); assertThat(proof).isNotEqualTo(secondProof); } @@ -406,7 +406,7 @@ public void getProofAfterGetProofClearingStackAndAddingDifferentAssertionsTest() // Test getProof() Proof proof = prover.getProof(); - checkProof(proof); + verifyProofObjectValidity(proof); prover.pop(); prover.pop(); @@ -420,7 +420,7 @@ public void getProofAfterGetProofClearingStackAndAddingDifferentAssertionsTest() // Test getProof() Proof secondProof = prover.getProof(); - checkProof(secondProof); + verifyProofObjectValidity(secondProof); assertThat(proof).isNotEqualTo(secondProof); } @@ -482,7 +482,7 @@ public void getBitVectorProofTest() throws InterruptedException, SolverException // Test getProof() Proof proof = prover.getProof(); - checkProof(proof); + verifyProofObjectValidity(proof); } } @@ -512,12 +512,12 @@ public void getArrayProofTest() throws InterruptedException, SolverException { // Test getProof() Proof proof = prover.getProof(); - checkProof(proof); + verifyProofObjectValidity(proof); } } // Traverses a proof and asserts that certain values are not null, instances, etc. - private void checkProof(Proof pRoot) { + private void verifyProofObjectValidity(Proof pRoot) { assertThat(pRoot).isNotNull(); Deque stack = new ArrayDeque<>(); From be6ae14fb395bc0190cc348ef2f2bfd81eeac6e8 Mon Sep 17 00:00:00 2001 From: gcarpio21 Date: Wed, 28 Jan 2026 13:40:09 +0000 Subject: [PATCH 38/44] Proofs: added more documentation to the `ProofRule` interface. --- .../sosy_lab/java_smt/api/proofs/ProofRule.java | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/api/proofs/ProofRule.java b/src/org/sosy_lab/java_smt/api/proofs/ProofRule.java index fa2499af8f..5d50d69538 100644 --- a/src/org/sosy_lab/java_smt/api/proofs/ProofRule.java +++ b/src/org/sosy_lab/java_smt/api/proofs/ProofRule.java @@ -10,7 +10,20 @@ package org.sosy_lab.java_smt.api.proofs; -/** A proof rule from a given proof format. */ +/** + * 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. */ From 58cf62c2bbe338d01174fa3b2e034cf20a2ba5fc Mon Sep 17 00:00:00 2001 From: gcarpio21 Date: Wed, 28 Jan 2026 14:51:04 +0000 Subject: [PATCH 39/44] Proofs: added more documentation in `ProverEnvironmentTest`. --- .../sosy_lab/java_smt/test/ProverEnvironmentTest.java | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java b/src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java index 68955c4193..0fb3e9000e 100644 --- a/src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java +++ b/src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java @@ -516,7 +516,15 @@ public void getArrayProofTest() throws InterruptedException, SolverException { } } - // Traverses a proof and asserts that certain values are not null, instances, etc. + /** + * 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(Proof pRoot) { assertThat(pRoot).isNotNull(); From 3fcf9f0b51007b1f304b08ef8f343f87fc15bdfe Mon Sep 17 00:00:00 2001 From: gcarpio21 Date: Fri, 30 Jan 2026 10:51:26 +0000 Subject: [PATCH 40/44] Proofs: Renamed `Proof` into `ProofNode`. --- .../java_smt/api/BasicProverEnvironment.java | 4 +- .../sosy_lab/java_smt/api/proofs/Proof.java | 29 +--- .../java_smt/api/proofs/ProofNode.java | 43 ++++++ .../java_smt/basicimpl/AbstractProofNode.java | 132 ++++++++++++++++++ .../java_smt/basicimpl/AbstractProver.java | 6 +- .../BasicProverWithAssumptionsWrapper.java | 4 +- .../DebuggingBasicProverEnvironment.java | 4 +- .../LoggingBasicProverEnvironment.java | 6 +- .../StatisticsBasicProverEnvironment.java | 4 +- .../SynchronizedBasicProverEnvironment.java | 4 +- ...izedBasicProverEnvironmentWithContext.java | 4 +- .../solvers/cvc5/CVC5AbstractProver.java | 6 +- .../{CVC5Proof.java => CVC5ProofNode.java} | 17 +-- .../java_smt/test/ProverEnvironmentTest.java | 66 ++++----- 14 files changed, 241 insertions(+), 88 deletions(-) create mode 100644 src/org/sosy_lab/java_smt/api/proofs/ProofNode.java create mode 100644 src/org/sosy_lab/java_smt/basicimpl/AbstractProofNode.java rename src/org/sosy_lab/java_smt/solvers/cvc5/{CVC5Proof.java => CVC5ProofNode.java} (82%) diff --git a/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java b/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java index 91cb67ff7d..70e30d3b23 100644 --- a/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java +++ b/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java @@ -16,7 +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; +import org.sosy_lab.java_smt.api.proofs.ProofNode; /** * Super interface for {@link ProverEnvironment} and {@link InterpolatingProverEnvironment} that @@ -166,7 +166,7 @@ default ImmutableMap getStatistics() { * method should be called only immediately after an {@link #isUnsat()} call that returned * true. */ - Proof getProof() throws SolverException, InterruptedException; + ProofNode getProof() throws SolverException, InterruptedException; /** * Closes the prover environment. The object should be discarded, and should not be used after diff --git a/src/org/sosy_lab/java_smt/api/proofs/Proof.java b/src/org/sosy_lab/java_smt/api/proofs/Proof.java index 263cac8035..944cd6af70 100644 --- a/src/org/sosy_lab/java_smt/api/proofs/Proof.java +++ b/src/org/sosy_lab/java_smt/api/proofs/Proof.java @@ -3,7 +3,7 @@ * an API wrapper for a collection of SMT solvers: * https://github.com/sosy-lab/java-smt * - * SPDX-FileCopyrightText: 2026 Dirk Beyer + * SPDX-FileCopyrightText: 2024 Dirk Beyer * * SPDX-License-Identifier: Apache-2.0 */ @@ -11,33 +11,10 @@ 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 Proof { - /** Get the children of the proof node. */ - ImmutableSet getChildren(); + public ImmutableSet getProofNodes(); - /** - * 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(); + public 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/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 4da6a6d5c4..41405c1454 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java @@ -32,7 +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; +import org.sosy_lab.java_smt.api.proofs.ProofNode; public abstract class AbstractProver implements BasicProverEnvironment { @@ -288,8 +288,8 @@ public void close() { } @Override - public Proof getProof() throws InterruptedException, SolverException { + public ProofNode getProof() throws InterruptedException, SolverException { throw new UnsupportedOperationException( - "Proof generation is not available for the current solver."); + "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 789a1ef79b..3925452d05 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/BasicProverWithAssumptionsWrapper.java +++ b/src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/BasicProverWithAssumptionsWrapper.java @@ -18,7 +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.api.proofs.ProofNode; public class BasicProverWithAssumptionsWrapper> implements BasicProverEnvironment { @@ -131,7 +131,7 @@ public R allSat(AllSatCallback pCallback, List pImportant } @Override - public Proof getProof() throws SolverException, InterruptedException { + public ProofNode 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 d8ad071624..e4ae1227bd 100644 --- a/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingBasicProverEnvironment.java +++ b/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingBasicProverEnvironment.java @@ -18,7 +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.api.proofs.ProofNode; class DebuggingBasicProverEnvironment implements BasicProverEnvironment { private final BasicProverEnvironment delegate; @@ -95,7 +95,7 @@ public Optional> unsatCoreOverAssumptions( } @Override - public Proof getProof() throws SolverException, InterruptedException { + public ProofNode getProof() throws SolverException, InterruptedException { return delegate.getProof(); } 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 c20916c683..a43902991d 100644 --- a/src/org/sosy_lab/java_smt/delegate/logging/LoggingBasicProverEnvironment.java +++ b/src/org/sosy_lab/java_smt/delegate/logging/LoggingBasicProverEnvironment.java @@ -24,7 +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; +import org.sosy_lab.java_smt.api.proofs.ProofNode; /** Wraps a basic prover environment with a logging object. */ class LoggingBasicProverEnvironment implements BasicProverEnvironment { @@ -122,8 +122,8 @@ public ImmutableMap getStatistics() { } @Override - public Proof getProof() throws SolverException, InterruptedException { - Proof p = wrapped.getProof(); + public ProofNode getProof() throws SolverException, InterruptedException { + ProofNode p = wrapped.getProof(); return p; } 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 d0c6bef146..70b6ccf74d 100644 --- a/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsBasicProverEnvironment.java +++ b/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsBasicProverEnvironment.java @@ -18,7 +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.api.proofs.ProofNode; import org.sosy_lab.java_smt.delegate.statistics.TimerPool.TimerWrapper; class StatisticsBasicProverEnvironment implements BasicProverEnvironment { @@ -101,7 +101,7 @@ public Optional> unsatCoreOverAssumptions( } @Override - public Proof getProof() throws SolverException, InterruptedException { + public ProofNode getProof() throws SolverException, InterruptedException { return delegate.getProof(); } 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 09d5894c60..b258c71b36 100644 --- a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBasicProverEnvironment.java +++ b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBasicProverEnvironment.java @@ -20,7 +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; +import org.sosy_lab.java_smt.api.proofs.ProofNode; class SynchronizedBasicProverEnvironment implements BasicProverEnvironment { @@ -106,7 +106,7 @@ public ImmutableMap getStatistics() { } @Override - public Proof getProof() throws SolverException, InterruptedException { + public ProofNode getProof() throws SolverException, InterruptedException { return delegate.getProof(); } 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 353e6dbbf5..364e37af49 100644 --- a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBasicProverEnvironmentWithContext.java +++ b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBasicProverEnvironmentWithContext.java @@ -22,7 +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; +import org.sosy_lab.java_smt.api.proofs.ProofNode; class SynchronizedBasicProverEnvironmentWithContext implements BasicProverEnvironment { @@ -123,7 +123,7 @@ public ImmutableMap getStatistics() { } @Override - public Proof getProof() throws SolverException, InterruptedException { + public ProofNode getProof() throws SolverException, InterruptedException { return delegate.getProof(); } 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 d70a1e6792..101cf6fb00 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java @@ -10,7 +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.CVC5Proof.generateProofImpl; +import static org.sosy_lab.java_smt.solvers.cvc5.CVC5ProofNode.generateProofImpl; import com.google.common.collect.Collections2; import com.google.common.collect.HashMultimap; @@ -44,7 +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.api.proofs.ProofNode; import org.sosy_lab.java_smt.basicimpl.AbstractProverWithAllSat; abstract class CVC5AbstractProver extends AbstractProverWithAllSat { @@ -321,7 +321,7 @@ public Optional> unsatCoreOverAssumptions( } @Override - public Proof getProof() throws SolverException, InterruptedException { + public ProofNode getProof() throws SolverException, InterruptedException { checkGenerateProofs(); checkState(!closed); checkState(isUnsat()); diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Proof.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5ProofNode.java similarity index 82% rename from src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Proof.java rename to src/org/sosy_lab/java_smt/solvers/cvc5/CVC5ProofNode.java index 0613028947..276b262c00 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Proof.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5ProofNode.java @@ -18,19 +18,20 @@ import java.util.LinkedHashMap; import java.util.Map; import org.sosy_lab.java_smt.api.Formula; -import org.sosy_lab.java_smt.api.proofs.Proof; +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 CVC5Proof extends org.sosy_lab.java_smt.basicimpl.AbstractProof { +public final class CVC5ProofNode extends AbstractProofNode { - static CVC5Proof generateProofImpl( + static CVC5ProofNode generateProofImpl( io.github.cvc5.Proof pProof, CVC5FormulaCreator pFormulaCreator) throws CVC5ApiException { Deque stack = new ArrayDeque<>(); - Map tempComputed; + Map tempComputed; - ImmutableMap computed = ImmutableMap.of(); + ImmutableMap computed = ImmutableMap.of(); stack.push(new CVC5Frame(pProof)); @@ -58,7 +59,7 @@ static CVC5Proof generateProofImpl( // Generate formula Term term = frame.getProof().getResult(); Formula pFormula = pFormulaCreator.encapsulate(pFormulaCreator.getFormulaType(term), term); - CVC5Proof pn = new CVC5Proof(proofRule, pFormula); + CVC5ProofNode pn = new CVC5ProofNode(proofRule, pFormula); for (int i = 0; i < numChildren; i++) { io.github.cvc5.Proof child = frame.getProof().getChildren()[i]; @@ -80,13 +81,13 @@ private static class CVC5Frame extends ProofFrame { } } - private CVC5Proof(ProofRule pProofRule, Formula pFormula) { + private CVC5ProofNode(ProofRule pProofRule, Formula pFormula) { super(pProofRule, pFormula); } @Override - protected void addChild(Proof pChild) { + protected void addChild(ProofNode pChild) { super.addChild(pChild); } diff --git a/src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java b/src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java index 0fb3e9000e..d5a8497ee5 100644 --- a/src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java +++ b/src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java @@ -42,7 +42,7 @@ 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.Proof; +import org.sosy_lab.java_smt.api.proofs.ProofNode; import org.sosy_lab.java_smt.api.proofs.ProofRule; public class ProverEnvironmentTest extends SolverBasedTest0.ParameterizedSolverBasedTest0 { @@ -219,8 +219,8 @@ public void testGetSimpleBooleanProof() throws InterruptedException, SolverExcep assertThat(prover.isUnsat()).isTrue(); // Test getProof() - Proof proof = prover.getProof(); - verifyProofObjectValidity(proof); + ProofNode proofNode = prover.getProof(); + verifyProofObjectValidity(proofNode); } } @@ -283,9 +283,9 @@ public void testGetComplexRationalNumeralAndUFProof() prover.addConstraint(bmgr.and(bmgr.or(a, c), bmgr.not(c))); assertThat(prover.isUnsat()).isTrue(); - // Retrieve and verify proof - Proof proof = prover.getProof(); - verifyProofObjectValidity(proof); + // Retrieve and verify proofNode + ProofNode proofNode = prover.getProof(); + verifyProofObjectValidity(proofNode); } } @@ -301,7 +301,7 @@ public void proofOfTrueTest() throws InterruptedException, SolverException { assertThat(prover.isUnsat()).isFalse(); @SuppressWarnings("unused") - Proof proof = prover.getProof(); + ProofNode proofNode = prover.getProof(); throw new AssertionError("Expected IllegalStateException was not thrown"); } catch (IllegalStateException e) { @@ -321,8 +321,8 @@ public void proofOfFalseTest() throws InterruptedException, SolverException { prover.addConstraint(bottom); assertThat(prover.isUnsat()).isTrue(); - Proof proof = prover.getProof(); - assertThat(proof).isNotNull(); + ProofNode proofNode = prover.getProof(); + assertThat(proofNode).isNotNull(); } } @@ -342,8 +342,8 @@ public void testGetSimpleIntegerProof() throws InterruptedException, SolverExcep assertThat(prover.isUnsat()).isTrue(); // Test getProof() - Proof proof = prover.getProof(); - verifyProofObjectValidity(proof); + ProofNode proofNode = prover.getProof(); + verifyProofObjectValidity(proofNode); } } @@ -366,8 +366,8 @@ public void getProofAfterGetProofAndAddingAssertionsTest() assertThat(prover.isUnsat()).isTrue(); // Test getProof() - Proof proof = prover.getProof(); - verifyProofObjectValidity(proof); + ProofNode proofNode = prover.getProof(); + verifyProofObjectValidity(proofNode); // assert integer formulas and test again prover.addConstraint(imgr.equal(x1, two)); @@ -376,10 +376,10 @@ public void getProofAfterGetProofAndAddingAssertionsTest() assertThat(prover.isUnsat()).isTrue(); // Test getProof() - Proof secondProof = prover.getProof(); - verifyProofObjectValidity(secondProof); + ProofNode secondProofNode = prover.getProof(); + verifyProofObjectValidity(secondProofNode); - assertThat(proof).isNotEqualTo(secondProof); + assertThat(proofNode).isNotEqualTo(secondProofNode); } } @@ -405,8 +405,8 @@ public void getProofAfterGetProofClearingStackAndAddingDifferentAssertionsTest() assertThat(prover.isUnsat()).isTrue(); // Test getProof() - Proof proof = prover.getProof(); - verifyProofObjectValidity(proof); + ProofNode proofNode = prover.getProof(); + verifyProofObjectValidity(proofNode); prover.pop(); prover.pop(); @@ -419,10 +419,10 @@ public void getProofAfterGetProofClearingStackAndAddingDifferentAssertionsTest() assertThat(prover.isUnsat()).isTrue(); // Test getProof() - Proof secondProof = prover.getProof(); - verifyProofObjectValidity(secondProof); + ProofNode secondProofNode = prover.getProof(); + verifyProofObjectValidity(secondProofNode); - assertThat(proof).isNotEqualTo(secondProof); + assertThat(proofNode).isNotEqualTo(secondProofNode); } } @@ -438,7 +438,7 @@ public void getProofWithoutProofProductionEnabledTest() assertThat(prover.isUnsat()).isTrue(); @SuppressWarnings("unused") - Proof proof = prover.getProof(); + ProofNode proofNode = prover.getProof(); throw new AssertionError("Expected IllegalStateException was not thrown"); } catch (IllegalStateException e) { @@ -481,8 +481,8 @@ public void getBitVectorProofTest() throws InterruptedException, SolverException assertThat(prover.isUnsat()).isTrue(); // Test getProof() - Proof proof = prover.getProof(); - verifyProofObjectValidity(proof); + ProofNode proofNode = prover.getProof(); + verifyProofObjectValidity(proofNode); } } @@ -511,8 +511,8 @@ public void getArrayProofTest() throws InterruptedException, SolverException { assertThat(prover.isUnsat()).isTrue(); // Test getProof() - Proof proof = prover.getProof(); - verifyProofObjectValidity(proof); + ProofNode proofNode = prover.getProof(); + verifyProofObjectValidity(proofNode); } } @@ -525,23 +525,23 @@ public void getArrayProofTest() throws InterruptedException, SolverException { * * @param pRoot the root of the proof DAG to be tested. */ - private void verifyProofObjectValidity(Proof pRoot) { + private void verifyProofObjectValidity(ProofNode pRoot) { assertThat(pRoot).isNotNull(); - Deque stack = new ArrayDeque<>(); + Deque stack = new ArrayDeque<>(); stack.push(pRoot); while (!stack.isEmpty()) { - Proof proof = stack.pop(); - ProofRule rule = proof.getRule(); - Optional formula = proof.getFormula(); + ProofNode proofNode = stack.pop(); + ProofRule rule = proofNode.getRule(); + Optional formula = proofNode.getFormula(); assertThat(rule).isNotNull(); assertThat(rule).isInstanceOf(ProofRule.class); - assertThat(proof.getChildren()).isNotNull(); + assertThat(proofNode.getChildren()).isNotNull(); assertThat(formula.isPresent()).isTrue(); - for (Proof child : proof.getChildren()) { + for (ProofNode child : proofNode.getChildren()) { assertThat(child).isNotNull(); stack.push(child); } From 4329cbf95b29e89fd15c9200dbe3173d800a2ef3 Mon Sep 17 00:00:00 2001 From: gcarpio21 Date: Fri, 30 Jan 2026 10:52:08 +0000 Subject: [PATCH 41/44] Proofs: Added `AbstractProof`. --- .../java_smt/basicimpl/AbstractProof.java | 124 +----------------- 1 file changed, 6 insertions(+), 118 deletions(-) diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractProof.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractProof.java index dfefd73078..fbe51fdc6c 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProof.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProof.java @@ -3,130 +3,18 @@ * an API wrapper for a collection of SMT solvers: * https://github.com/sosy-lab/java-smt * - * SPDX-FileCopyrightText: 2026 Dirk Beyer + * SPDX-FileCopyrightText: 2024 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.Proof; -import org.sosy_lab.java_smt.api.proofs.ProofRule; +import org.sosy_lab.java_smt.api.proofs.ProofNode; -/** - * A proof DAG of a proof. - * - * @author Gabriel Carpio - */ -public abstract class AbstractProof implements Proof { - - private ImmutableSet children = ImmutableSet.of(); - private ProofRule rule; - protected Optional formula = Optional.empty(); - - protected AbstractProof(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(Proof 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 (Proof child : getChildren()) { - sb.append(indent).append("Child ").append(++i).append(":\n"); - sb.append(((AbstractProof) 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; - } +public class AbstractProof { + // public final ProofNode root; + // public final ImmutableSet proofNodes; - /** Set the number of arguments the proof object has. */ - public void setNumArgs(int pNumArgs) { - this.numArgs = pNumArgs; - } - } + public AbstractProof(ProofNode pRoot) {} } From f6489e887b4f8ec8145999f52b475e2cd925a610 Mon Sep 17 00:00:00 2001 From: gcarpio21 Date: Fri, 30 Jan 2026 12:00:42 +0000 Subject: [PATCH 42/44] Proofs: `AbstractProof` implements `Proof`. `getProof` in `BasicProverEnvironment` now returns an object of type `Proof`. Tests modified accordingly. --- .../java_smt/api/BasicProverEnvironment.java | 4 ++-- .../sosy_lab/java_smt/api/proofs/Proof.java | 14 +++++++---- .../java_smt/basicimpl/AbstractProof.java | 15 ++++++++---- .../java_smt/basicimpl/AbstractProver.java | 4 ++-- .../BasicProverWithAssumptionsWrapper.java | 4 ++-- .../DebuggingBasicProverEnvironment.java | 4 ++-- .../LoggingBasicProverEnvironment.java | 6 ++--- .../StatisticsBasicProverEnvironment.java | 4 ++-- .../SynchronizedBasicProverEnvironment.java | 4 ++-- ...izedBasicProverEnvironmentWithContext.java | 4 ++-- .../solvers/cvc5/CVC5AbstractProver.java | 6 ++--- .../java_smt/solvers/cvc5/CVC5Proof.java | 21 ++++++++++++++++ .../java_smt/test/ProverEnvironmentTest.java | 24 +++++++++---------- 13 files changed, 74 insertions(+), 40 deletions(-) create mode 100644 src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Proof.java diff --git a/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java b/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java index 70e30d3b23..91cb67ff7d 100644 --- a/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java +++ b/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java @@ -16,7 +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.ProofNode; +import org.sosy_lab.java_smt.api.proofs.Proof; /** * Super interface for {@link ProverEnvironment} and {@link InterpolatingProverEnvironment} that @@ -166,7 +166,7 @@ default ImmutableMap getStatistics() { * method should be called only immediately after an {@link #isUnsat()} call that returned * true. */ - ProofNode getProof() throws SolverException, InterruptedException; + Proof getProof() throws SolverException, InterruptedException; /** * Closes the prover environment. The object should be discarded, and should not be used after diff --git a/src/org/sosy_lab/java_smt/api/proofs/Proof.java b/src/org/sosy_lab/java_smt/api/proofs/Proof.java index 944cd6af70..56f872b225 100644 --- a/src/org/sosy_lab/java_smt/api/proofs/Proof.java +++ b/src/org/sosy_lab/java_smt/api/proofs/Proof.java @@ -10,11 +10,17 @@ package org.sosy_lab.java_smt.api.proofs; -import com.google.common.collect.ImmutableSet; - +/** + * 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 { - public ImmutableSet getProofNodes(); - + /** + * Returns the root proof node of the DAG from this proof. + * + * @return an object of type {@link ProofNode} the root proof node. + * @see ProofNode + */ public ProofNode getProofRoot(); } diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractProof.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractProof.java index fbe51fdc6c..db15e58aad 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProof.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProof.java @@ -10,11 +10,18 @@ package org.sosy_lab.java_smt.basicimpl; +import org.sosy_lab.java_smt.api.proofs.Proof; import org.sosy_lab.java_smt.api.proofs.ProofNode; -public class AbstractProof { - // public final ProofNode root; - // public final ImmutableSet proofNodes; +public class AbstractProof implements Proof { + public final ProofNode root; - public AbstractProof(ProofNode pRoot) {} + public AbstractProof(ProofNode pRoot) { + root = pRoot; + } + + @Override + public ProofNode getProofRoot() { + return root; + } } diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java index 41405c1454..476a01996c 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java @@ -32,7 +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.ProofNode; +import org.sosy_lab.java_smt.api.proofs.Proof; public abstract class AbstractProver implements BasicProverEnvironment { @@ -288,7 +288,7 @@ public void close() { } @Override - public ProofNode getProof() throws InterruptedException, SolverException { + 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 3925452d05..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,7 +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.ProofNode; +import org.sosy_lab.java_smt.api.proofs.Proof; public class BasicProverWithAssumptionsWrapper> implements BasicProverEnvironment { @@ -131,7 +131,7 @@ public R allSat(AllSatCallback pCallback, List pImportant } @Override - public ProofNode getProof() throws SolverException, InterruptedException { + 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 e4ae1227bd..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,7 +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.ProofNode; +import org.sosy_lab.java_smt.api.proofs.Proof; class DebuggingBasicProverEnvironment implements BasicProverEnvironment { private final BasicProverEnvironment delegate; @@ -95,7 +95,7 @@ public Optional> unsatCoreOverAssumptions( } @Override - public ProofNode getProof() throws SolverException, InterruptedException { + public Proof getProof() throws SolverException, InterruptedException { return delegate.getProof(); } 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 a43902991d..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,7 +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.ProofNode; +import org.sosy_lab.java_smt.api.proofs.Proof; /** Wraps a basic prover environment with a logging object. */ class LoggingBasicProverEnvironment implements BasicProverEnvironment { @@ -122,8 +122,8 @@ public ImmutableMap getStatistics() { } @Override - public ProofNode getProof() throws SolverException, InterruptedException { - ProofNode p = wrapped.getProof(); + public Proof getProof() throws SolverException, InterruptedException { + Proof p = wrapped.getProof(); return p; } 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 70b6ccf74d..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,7 +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.ProofNode; +import org.sosy_lab.java_smt.api.proofs.Proof; import org.sosy_lab.java_smt.delegate.statistics.TimerPool.TimerWrapper; class StatisticsBasicProverEnvironment implements BasicProverEnvironment { @@ -101,7 +101,7 @@ public Optional> unsatCoreOverAssumptions( } @Override - public ProofNode getProof() throws SolverException, InterruptedException { + public Proof getProof() throws SolverException, InterruptedException { return delegate.getProof(); } 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 b258c71b36..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,7 +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.ProofNode; +import org.sosy_lab.java_smt.api.proofs.Proof; class SynchronizedBasicProverEnvironment implements BasicProverEnvironment { @@ -106,7 +106,7 @@ public ImmutableMap getStatistics() { } @Override - public ProofNode getProof() throws SolverException, InterruptedException { + public Proof getProof() throws SolverException, InterruptedException { return delegate.getProof(); } 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 364e37af49..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,7 +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.ProofNode; +import org.sosy_lab.java_smt.api.proofs.Proof; class SynchronizedBasicProverEnvironmentWithContext implements BasicProverEnvironment { @@ -123,7 +123,7 @@ public ImmutableMap getStatistics() { } @Override - public ProofNode getProof() throws SolverException, InterruptedException { + public Proof getProof() throws SolverException, InterruptedException { return delegate.getProof(); } 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 101cf6fb00..6a033847d5 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java @@ -44,7 +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.ProofNode; +import org.sosy_lab.java_smt.api.proofs.Proof; import org.sosy_lab.java_smt.basicimpl.AbstractProverWithAllSat; abstract class CVC5AbstractProver extends AbstractProverWithAllSat { @@ -321,7 +321,7 @@ public Optional> unsatCoreOverAssumptions( } @Override - public ProofNode getProof() throws SolverException, InterruptedException { + public Proof getProof() throws SolverException, InterruptedException { checkGenerateProofs(); checkState(!closed); checkState(isUnsat()); @@ -331,7 +331,7 @@ public ProofNode getProof() throws SolverException, InterruptedException { // CVC5ProofProcessor pp = new CVC5ProofProcessor(creator); try { - return generateProofImpl(proofs[0], creator); + return new CVC5Proof(generateProofImpl(proofs[0], creator)); } catch (CVC5ApiException e) { throw new SolverException("There was a problem generating proof", e); } 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..c4134a29d4 --- /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: 2024 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/test/ProverEnvironmentTest.java b/src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java index d5a8497ee5..cf2ba05ae7 100644 --- a/src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java +++ b/src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java @@ -219,7 +219,7 @@ public void testGetSimpleBooleanProof() throws InterruptedException, SolverExcep assertThat(prover.isUnsat()).isTrue(); // Test getProof() - ProofNode proofNode = prover.getProof(); + ProofNode proofNode = prover.getProof().getProofRoot(); verifyProofObjectValidity(proofNode); } } @@ -284,7 +284,7 @@ public void testGetComplexRationalNumeralAndUFProof() assertThat(prover.isUnsat()).isTrue(); // Retrieve and verify proofNode - ProofNode proofNode = prover.getProof(); + ProofNode proofNode = prover.getProof().getProofRoot(); verifyProofObjectValidity(proofNode); } } @@ -301,7 +301,7 @@ public void proofOfTrueTest() throws InterruptedException, SolverException { assertThat(prover.isUnsat()).isFalse(); @SuppressWarnings("unused") - ProofNode proofNode = prover.getProof(); + ProofNode proofNode = prover.getProof().getProofRoot(); throw new AssertionError("Expected IllegalStateException was not thrown"); } catch (IllegalStateException e) { @@ -321,7 +321,7 @@ public void proofOfFalseTest() throws InterruptedException, SolverException { prover.addConstraint(bottom); assertThat(prover.isUnsat()).isTrue(); - ProofNode proofNode = prover.getProof(); + ProofNode proofNode = prover.getProof().getProofRoot(); assertThat(proofNode).isNotNull(); } } @@ -342,7 +342,7 @@ public void testGetSimpleIntegerProof() throws InterruptedException, SolverExcep assertThat(prover.isUnsat()).isTrue(); // Test getProof() - ProofNode proofNode = prover.getProof(); + ProofNode proofNode = prover.getProof().getProofRoot(); verifyProofObjectValidity(proofNode); } } @@ -366,7 +366,7 @@ public void getProofAfterGetProofAndAddingAssertionsTest() assertThat(prover.isUnsat()).isTrue(); // Test getProof() - ProofNode proofNode = prover.getProof(); + ProofNode proofNode = prover.getProof().getProofRoot(); verifyProofObjectValidity(proofNode); // assert integer formulas and test again @@ -376,7 +376,7 @@ public void getProofAfterGetProofAndAddingAssertionsTest() assertThat(prover.isUnsat()).isTrue(); // Test getProof() - ProofNode secondProofNode = prover.getProof(); + ProofNode secondProofNode = prover.getProof().getProofRoot(); verifyProofObjectValidity(secondProofNode); assertThat(proofNode).isNotEqualTo(secondProofNode); @@ -405,7 +405,7 @@ public void getProofAfterGetProofClearingStackAndAddingDifferentAssertionsTest() assertThat(prover.isUnsat()).isTrue(); // Test getProof() - ProofNode proofNode = prover.getProof(); + ProofNode proofNode = prover.getProof().getProofRoot(); verifyProofObjectValidity(proofNode); prover.pop(); @@ -419,7 +419,7 @@ public void getProofAfterGetProofClearingStackAndAddingDifferentAssertionsTest() assertThat(prover.isUnsat()).isTrue(); // Test getProof() - ProofNode secondProofNode = prover.getProof(); + ProofNode secondProofNode = prover.getProof().getProofRoot(); verifyProofObjectValidity(secondProofNode); assertThat(proofNode).isNotEqualTo(secondProofNode); @@ -438,7 +438,7 @@ public void getProofWithoutProofProductionEnabledTest() assertThat(prover.isUnsat()).isTrue(); @SuppressWarnings("unused") - ProofNode proofNode = prover.getProof(); + ProofNode proofNode = prover.getProof().getProofRoot(); throw new AssertionError("Expected IllegalStateException was not thrown"); } catch (IllegalStateException e) { @@ -481,7 +481,7 @@ public void getBitVectorProofTest() throws InterruptedException, SolverException assertThat(prover.isUnsat()).isTrue(); // Test getProof() - ProofNode proofNode = prover.getProof(); + ProofNode proofNode = prover.getProof().getProofRoot(); verifyProofObjectValidity(proofNode); } } @@ -511,7 +511,7 @@ public void getArrayProofTest() throws InterruptedException, SolverException { assertThat(prover.isUnsat()).isTrue(); // Test getProof() - ProofNode proofNode = prover.getProof(); + ProofNode proofNode = prover.getProof().getProofRoot(); verifyProofObjectValidity(proofNode); } } From 76d8d716ddc92985fb16f8df7dc0422bb96f03ac Mon Sep 17 00:00:00 2001 From: gcarpio21 Date: Tue, 17 Feb 2026 12:09:36 +0000 Subject: [PATCH 43/44] Update year in copyright. --- src/org/sosy_lab/java_smt/api/proofs/Proof.java | 2 +- src/org/sosy_lab/java_smt/basicimpl/AbstractProof.java | 2 +- src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Proof.java | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/org/sosy_lab/java_smt/api/proofs/Proof.java b/src/org/sosy_lab/java_smt/api/proofs/Proof.java index 56f872b225..4a5ab07cc6 100644 --- a/src/org/sosy_lab/java_smt/api/proofs/Proof.java +++ b/src/org/sosy_lab/java_smt/api/proofs/Proof.java @@ -3,7 +3,7 @@ * an API wrapper for a collection of SMT solvers: * https://github.com/sosy-lab/java-smt * - * SPDX-FileCopyrightText: 2024 Dirk Beyer + * SPDX-FileCopyrightText: 2026 Dirk Beyer * * SPDX-License-Identifier: Apache-2.0 */ diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractProof.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractProof.java index db15e58aad..d9ff7bf44a 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProof.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProof.java @@ -3,7 +3,7 @@ * an API wrapper for a collection of SMT solvers: * https://github.com/sosy-lab/java-smt * - * SPDX-FileCopyrightText: 2024 Dirk Beyer + * SPDX-FileCopyrightText: 2026 Dirk Beyer * * SPDX-License-Identifier: Apache-2.0 */ diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Proof.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Proof.java index c4134a29d4..a6a0e46653 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Proof.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Proof.java @@ -3,7 +3,7 @@ * an API wrapper for a collection of SMT solvers: * https://github.com/sosy-lab/java-smt * - * SPDX-FileCopyrightText: 2024 Dirk Beyer + * SPDX-FileCopyrightText: 2026 Dirk Beyer * * SPDX-License-Identifier: Apache-2.0 */ From cdca7ce57ac947dfe467445d9888f967a9be2910 Mon Sep 17 00:00:00 2001 From: gcarpio21 Date: Tue, 17 Feb 2026 14:27:57 +0000 Subject: [PATCH 44/44] Proofs: Fix no exception when passing null to constructor of `AbstractProof`. Checkstyle. --- src/org/sosy_lab/java_smt/api/proofs/Proof.java | 2 +- src/org/sosy_lab/java_smt/basicimpl/AbstractProof.java | 7 ++++--- 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/src/org/sosy_lab/java_smt/api/proofs/Proof.java b/src/org/sosy_lab/java_smt/api/proofs/Proof.java index 4a5ab07cc6..0df15c7c57 100644 --- a/src/org/sosy_lab/java_smt/api/proofs/Proof.java +++ b/src/org/sosy_lab/java_smt/api/proofs/Proof.java @@ -22,5 +22,5 @@ public interface Proof { * @return an object of type {@link ProofNode} the root proof node. * @see ProofNode */ - public ProofNode getProofRoot(); + ProofNode getProofRoot(); } diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractProof.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractProof.java index d9ff7bf44a..7a346722ea 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProof.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProof.java @@ -10,14 +10,15 @@ 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 class AbstractProof implements Proof { - public final ProofNode root; +public abstract class AbstractProof implements Proof { + private final ProofNode root; public AbstractProof(ProofNode pRoot) { - root = pRoot; + root = Objects.requireNonNull(pRoot); } @Override