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,12 @@ default ImmutableMap<String, String> 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 <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,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
   }

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: 2024 Dirk Beyer <https://www.sosy-lab.org>
+ *
+ * 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. */
+public interface Proof {
+
+  /** Get the children of the proof node. */
+  Set<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/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 <https://www.sosy-lab.org>
+ *
+ * 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 <T> The type of the proof object.
+ */
+public abstract class ProofFrame<T> {
+  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;
+  }
+}

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

@@ -0,0 +1,18 @@
+/*
+ * 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 <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. */
+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: 2024 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,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 <https://www.sosy-lab.org>
+ *
+ * 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 <TFormulaInfo, TType, TEnv, TFuncDecl, T> Transformation(
+  //      FormulaCreator<TFormulaInfo, TType, TEnv, TFuncDecl> formulaCreator, T proof) {}
+
+  //    protected abstract Proof generateProof();
+  // }
+
+  private final Set<Proof> children = new LinkedHashSet<>();
+  private ProofRule rule;
+  protected Optional<Formula> 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<Formula> getFormula() {
+    return this.formula;
+  }
+
+  @Override
+  public Set<Proof> 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();
+  }
+}

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();