558 add general proof api

src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java

@@ -16,6 +16,7 @@
 import java.util.Optional;
 import org.checkerframework.checker.nullness.qual.Nullable;
 import org.sosy_lab.java_smt.api.SolverContext.ProverOptions;
+import org.sosy_lab.java_smt.api.proofs.Proof;
 
 /**
  * Super interface for {@link ProverEnvironment} and {@link InterpolatingProverEnvironment} that
@@ -160,6 +161,13 @@ default ImmutableMap<String, String> getStatistics() {
     return ImmutableMap.of();
   }
 
+  /**
+   * Get proof of unsatisfiability of the conjuction of the current satck of all formulas. This
+   * method should be called only immediately after an {@link #isUnsat()} call that returned <code>
+   * true</code>.
+   */
+  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

src/org/sosy_lab/java_smt/api/SolverContext.java

@@ -52,6 +52,9 @@ enum ProverOptions {
      */
     GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS,
 
+    /** Whether the solver should generate proofs for unsatisfiable formulas. */
+    GENERATE_PROOFS,
+
     /** Whether the solver should enable support for formulae build in SL theory. */
     ENABLE_SEPARATION_LOGIC
   }

src/org/sosy_lab/java_smt/api/proofs/Proof.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 <https://www.sosy-lab.org>
+ *
+ * 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 Proof {
+
+  /** Get the children of the proof node. */
+  ImmutableSet<Proof> 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<Formula> getFormula();
+
+  /**
+   * Get the rule of the proof node.
+   *
+   * @return The rule of the proof node.
+   */
+  ProofRule getRule();
+}

src/org/sosy_lab/java_smt/api/proofs/ProofRule.java

@@ -0,0 +1,31 @@
+/*
+ * This file is part of JavaSMT,
+ * an API wrapper for a collection of SMT solvers:
+ * https://github.com/sosy-lab/java-smt
+ *
+ * SPDX-FileCopyrightText: 2026 Dirk Beyer <https://www.sosy-lab.org>
+ *
+ * SPDX-License-Identifier: Apache-2.0
+ */
+
+package org.sosy_lab.java_smt.api.proofs;
+
+/**
+ * A proof rule from a given proof format. E.g.:
+ *
+ * <p>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: <a
+ * href="https://cvc5.github.io/docs/cvc5-1.3.2/api/java/io/github/cvc5/ProofRule.html">...</a>
+ * Note: Other solvers may return just a String, the name of the rule applied.
+ *
+ * <p>We can look at RESOLUTION: Given two nodes viewed as clauses C_1 and C_2, as well as the pivot
+ * which is a literal occurring in C_1 and C_2 (positively and negatively or the other way around)
+ * and its polarity, it produces C which "is a clause resulting from collecting all the literals in
+ * C_1, minus the first occurrence of the pivot or its negation, and C_2, minus the first occurrence
+ * of the pivot or its negation, according to the policy above". See the link given earlier.
+ */
+public interface ProofRule {
+
+  /** Get the name of the proof rule. */
+  String getName();
+}

src/org/sosy_lab/java_smt/api/proofs/package-info.java

@@ -0,0 +1,14 @@
+/*
+ * This file is part of JavaSMT,
+ * an API wrapper for a collection of SMT solvers:
+ * https://github.com/sosy-lab/java-smt
+ *
+ * SPDX-FileCopyrightText: 2026 Dirk Beyer <https://www.sosy-lab.org>
+ *
+ * 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;

src/org/sosy_lab/java_smt/basicimpl/AbstractProof.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 <https://www.sosy-lab.org>
+ *
+ * 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;
+
+/**
+ * A proof DAG of a proof.
+ *
+ * @author Gabriel Carpio
+ */
+public abstract class AbstractProof implements Proof {
+
+  private ImmutableSet<Proof> children = ImmutableSet.of();
+  private ProofRule rule;
+  protected Optional<Formula> formula = Optional.empty();
+
+  protected AbstractProof(ProofRule pRule, @Nullable Formula pFormula) {
+    this.rule = pRule;
+    this.formula = Optional.ofNullable(pFormula);
+  }
+
+  @Override
+  public Optional<Formula> getFormula() {
+    return this.formula;
+  }
+
+  @Override
+  public ImmutableSet<Proof> getChildren() {
+    return this.children;
+  }
+
+  protected void addChild(Proof pChild) {
+    Set<Proof> 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<T> {
+    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;
+    }
+  }
+}

src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java

@@ -32,6 +32,7 @@
 import org.sosy_lab.java_smt.api.OptimizationProverEnvironment.OptStatus;
 import org.sosy_lab.java_smt.api.SolverContext.ProverOptions;
 import org.sosy_lab.java_smt.api.SolverException;
+import org.sosy_lab.java_smt.api.proofs.Proof;
 
 public abstract class AbstractProver<T> implements BasicProverEnvironment<T> {
 
@@ -40,6 +41,7 @@ public abstract class AbstractProver<T> implements BasicProverEnvironment<T> {
   protected final boolean generateAllSat;
   protected final boolean generateUnsatCores;
   private final boolean generateUnsatCoresOverAssumptions;
+  protected final boolean generateProofs;
   protected final boolean enableSL;
 
   // flags for status
@@ -64,6 +66,7 @@ protected AbstractProver(Set<ProverOptions> pOptions) {
     generateUnsatCores = pOptions.contains(ProverOptions.GENERATE_UNSAT_CORE);
     generateUnsatCoresOverAssumptions =
         pOptions.contains(ProverOptions.GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS);
+    generateProofs = pOptions.contains(ProverOptions.GENERATE_PROOFS);
     enableSL = pOptions.contains(ProverOptions.ENABLE_SEPARATION_LOGIC);
 
     assertedFormulas.add(LinkedHashMultimap.create());
@@ -97,6 +100,13 @@ protected final void checkGenerateUnsatCoresOverAssumptions() {
     Preconditions.checkState(!wasLastSatCheckSatisfiable);
   }
 
+  protected final void checkGenerateProofs() {
+    Preconditions.checkState(generateProofs, TEMPLATE, ProverOptions.GENERATE_PROOFS);
+    Preconditions.checkState(!closed);
+    Preconditions.checkState(!changedSinceLastSatQuery);
+    Preconditions.checkState(!wasLastSatCheckSatisfiable);
+  }
+
   protected final void checkGenerateInterpolants() {
     Preconditions.checkState(!closed);
     Preconditions.checkState(
@@ -276,4 +286,10 @@ public void close() {
     closeAllEvaluators();
     closed = true;
   }
+
+  @Override
+  public Proof getProof() throws InterruptedException, SolverException {
+    throw new UnsupportedOperationException(
+        "Proof generation is not available for the current solver.");
+  }
 }

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<T, P extends BasicProverEnvironment<T>>
     implements BasicProverEnvironment<T> {
@@ -128,4 +129,9 @@ public <R> R allSat(AllSatCallback<R> pCallback, List<BooleanFormula> pImportant
     clearAssumptions();
     return delegate.allSat(pCallback, pImportant);
   }
+
+  @Override
+  public Proof getProof() throws SolverException, InterruptedException {
+    return delegate.getProof();
+  }
 }

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<T> implements BasicProverEnvironment<T> {
   private final BasicProverEnvironment<T> delegate;
@@ -93,6 +94,11 @@ public Optional<List<BooleanFormula>> unsatCoreOverAssumptions(
     return delegate.unsatCoreOverAssumptions(assumptions);
   }
 
+  @Override
+  public Proof getProof() throws SolverException, InterruptedException {
+    return delegate.getProof();
+  }
+
   @Override
   public void close() {
     debugging.assertThreadLocal();

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<T> implements BasicProverEnvironment<T> {
@@ -120,6 +121,12 @@ public ImmutableMap<String, String> getStatistics() {
     return wrapped.getStatistics();
   }
 
+  @Override
+  public Proof getProof() throws SolverException, InterruptedException {
+    Proof p = wrapped.getProof();
+    return p;
+  }
+
   @Override
   public void close() {
     wrapped.close();

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<T> implements BasicProverEnvironment<T> {
@@ -99,6 +100,11 @@ public Optional<List<BooleanFormula>> unsatCoreOverAssumptions(
     return delegate.unsatCoreOverAssumptions(pAssumptions);
   }
 
+  @Override
+  public Proof getProof() throws SolverException, InterruptedException {
+    return delegate.getProof();
+  }
+
   @Override
   public void close() {
     delegate.close();