Develop a common proof format and export proofs

src/org/sosy_lab/java_smt/ResProofRule.java

@@ -0,0 +1,161 @@
+/*
+ * 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;
+
+import java.util.HashMap;
+import java.util.Locale;
+import java.util.Map;
+import org.sosy_lab.java_smt.api.proofs.ProofRule;
+
+/**
+ * A proof rule in the proof DAG of the proof format RESOLUTE used by SMTInterpol. See: <a
+ * href="https://ultimate.informatik.uni-freiburg.de/smtinterpol/proof-format.html">...</a>
+ *
+ * <p>The conversion from other formats to RESOLUTE appears to be simple and as such, it is a good
+ * candidate for a common proof format.
+ *
+ * @author Gabriel Carpio
+ */
+public final class ResProofRule {
+
+  private static final Map<String, ResAxiom> RULE_MAP = new HashMap<>();
+
+  private ResProofRule() {
+    // prevent instantiation
+  }
+
+  static {
+    for (ResAxiom rule : ResAxiom.values()) {
+      RULE_MAP.put(rule.getName().toLowerCase(Locale.ROOT), rule);
+    }
+  }
+
+  /** Any operation that proves a term. */
+  public enum ResAxiom implements ProofRule {
+    // Resolution Rule
+    RESOLUTION("res", "(res t proof1 proof2)"),
+    ASSUME("assume", "(assume t)"),
+    // Logical operators
+    TRUE_POSITIVE("true+", "(+ true)"),
+    FALSE_NEGATIVE("false-", "(- false)"),
+    NOT_POSITIVE("not+", "(+ (not p0) + p0)"),
+    NOT_NEGATIVE("not-", "(- (not p0) - p0)"),
+    AND_POSITIVE("and+", "(+ (and p0 … pn) - p0 … - pn)"),
+    AND_NEGATIVE("and-", "(- (and p0 … pn) + pi)"),
+    OR_POSITIVE("or+", "(+ (or p0 … pn) - pi)"),
+    OR_NEGATIVE("or-", "(- (or p0 … pn) + p0 … + pn)"),
+    IMPLIES_POSITIVE("=>+", "(+ (=> p0 … pn) +/- pi)"),
+    IMPLIES_NEGATIVE("=>-", "(- (=> p0 … pn) - p0 … + pn)"),
+    EQUAL_POSITIVE1("=+1", "(+ (= p0 p1) + p0 + p1)"),
+    EQUAL_NEGATIVE1("=-1", "(- (= p0 p1) + p0 - p1)"),
+    EQUAL_POSITIVE2("=+2", "(+ (= p0 p1) - p0 - p1)"),
+    EQUAL_NEGATIVE2("=-2", "(- (= p0 p1) - p0 + p1)"),
+    XOR_POSITIVE("xor+", "(+(xor l1) +(xor l2) -(xor l3))"),
+    XOR_NEGATIVE("xor-", "(-(xor l1) -(xor l2) -(xor l3))"),
+
+    // Quantifiers
+    FORALL_POSITIVE("forall+", "(+ (forall x (F x)) - (F (choose x (F x))))"),
+    FORALL_NEGATIVE("forall-", "(- (forall x (F x)) + (F t))"),
+    EXISTS_POSITIVE("exists+", "(+ (exists x (F x)) - (F t))"),
+    EXISTS_NEGATIVE("exists-", "(- (exists x (F x)) + (F (choose x (F x))))"),
+
+    // Equality axioms
+    REFLEXIVITY("refl", "(+ (= t t))"),
+    SYMMETRY("symm", "(+(= t0 t1) -(= t1 t0))"),
+    TRANSITIVITY("trans", "(+(= t0 tn) -(= t0 t1) … -(= tn-1 tn))"),
+    CONGRUENCE("cong", "(+(= (f t0 … tn) (f t0' … tn')) -(= t0 t0') … -(= tn tn'))"),
+    EQUALITY_POSITIVE("=+", "(+ (= t0 … tn) -(= t0 t1) … -(= tn-1 tn))"),
+    EQUALITY_NEGATIVE("=-", "(- (= t0 … tn) +(= ti tj))"),
+    DISTINCT_POSITIVE("distinct+", "(+ (distinct t0 … tn) +(= t0 t1) … +(= t0 tn) … +(= tn-1 tn))"),
+    DISTINCT_NEGATIVE("distinct-", "(- (distinct t0 … tn) -(= ti tj))"),
+
+    // ITE, define-fun, annotations
+    ITE1("ite1", "(+(= (ite t0 t1 t2) t1) - t0)"),
+    ITE2("ite2", "(+(= (ite t0 t1 t2) t2) + t0)"),
+    DEL("del!", "(+(= (! t :annotation…) t))"),
+    EXPAND("expand", "(+(= (f t0 … tn) (let ((x0 t0)…(xn tn)) d)))"),
+
+    // Array Theory
+    SELECTSTORE1("selectstore1", "(+ (= (select (store a i v) i) v))"),
+    SELECTSTORE2("selectstore2", "(+ (= (select (store a i v) j) (select a j)) (= i j))"),
+    EXTDIFF("extdiff", "(+ (= a b) (- (= (select a (@diff a b)) (select b (@diff a b)))))"),
+    CONST("const", "(+ (= (select (@const v) i) v))"),
+
+    // Linear Arithmetic
+    POLY_ADD("poly+", "(+ (= (+ a1 ... an) a))"),
+    POLY_MUL("poly*", "(+ (= (* a1 ... an) a))"),
+    TO_REAL("to_real", "(+ (= (to_real a) a'))"),
+    FARKAS("farkas", "(- (<=? a1 b1) ... - (<=? an bn))"),
+    TRICHOTOMY("trichotomy", "(+ (< a b) (= a b) (< b a))"),
+    TOTAL("total", "(+ (<= a b) (< b a))"),
+    GT_DEF("gt_def", "(+ (= (> a b) (< b a)))"),
+    GE_DEF("ge_def", "(+ (= (>= a b) (<= b a)))"),
+    DIV_DEF("div_def", "(+ (= a (* b1 ... bn (/ a b1 ... bn))) (= b1 0) ... (= bn 0))"),
+    NEG_DEF("neg_def", "(+ (= (- a) (* (- 1) a)))"),
+    NEG_DEF2("neg_def2", "(+ (= (- a b1 ... bn) (+ a (* (- 1) b1)) ... (* (- 1) bn)))"),
+    ABS_DEF("abs_def", "(+ (= (abs x) (ite (< x 0) (- x) x)))"),
+    TOTAL_INT("total_int", "(+ (<= a c) (<= (c+1) a))"),
+    TO_INT_LOW("to_int_low", "(+ (<= (to_real (to_int x)) x))"),
+    TO_INT_HIGH("to_int_high", "(+ (< x (+ (to_real (to_int x)) 1.0)))"),
+    DIV_LOW("div_low", "(+ (<= (* d (div x d)) x) (= d 0))"),
+    DIV_HIGH("div_high", "(+ (< x (+ (* d (div x d)) (abs d))) (= d 0))"),
+    MOD_DEF("mod_def", "(+ (= (mod x d) (- x (* d (div x d)))) (= d 0))"),
+    DIVISIBLE_DEF("divisible_def", "(+ (= ((_ divisible c) x) (= x (* c (div x c)))))"),
+    EXPAND_IS_INT("expand_is_int", "(+ (= (is_int x) (= x (to_real (to_int x)))))"),
+
+    // Data Types
+    DT_PROJECT("dt_project", "(= (seli (cons a1 ... an)) ai)"),
+    DT_CONS("dt_cons", "(~ ((_ is cons) x), (= (cons (sel1 x) ... (seln x)) x))"),
+    DT_TEST_CONS("dt_test_cons", "((_ is cons) (cons a1 ... an))"),
+    DT_TEST_CONS_PRIME("dt_test_cons_prime", "(~ ((_ is cons') (cons a1 ... an)))"),
+    DT_EXHAUST("dt_exhaust", "((_ is cons1) x), ..., ((_ is consn) x)"),
+    DT_ACYCLIC("dt_acyclic", "(~ (= (cons ... x ...) x))"),
+    DT_MATCH(
+        "dt_match",
+        "(= (match t ((p1 x1) c1) ...) (ite ((_ is p1) t) (let (x1 (sel1 t)) c1) ...))");
+
+    private final String name;
+    private final String formula;
+
+    ResAxiom(String pName, String pFormula) {
+      name = pName;
+      formula = pFormula;
+    }
+
+    @Override
+    public String getName() {
+      return name;
+    }
+
+    @Override
+    public String getFormula() {
+      return formula;
+    }
+  }
+
+  /**
+   * Retrieves a ProofRule by its name.
+   *
+   * @param name The name of the proof rule.
+   * @return The matching ProofRule.
+   * @throws NullPointerException if the name is null.
+   * @throws IllegalArgumentException if the name does not match any rule.
+   */
+  public static ResAxiom getFromName(String name) {
+
+    ResAxiom rule = RULE_MAP.get(name.toLowerCase(Locale.ROOT));
+    if (rule == null) {
+      throw new IllegalArgumentException("Rule not found or not specified: " + name);
+    }
+
+    return rule;
+  }
+}

src/org/sosy_lab/java_smt/ResolutionProofDAG.java

@@ -0,0 +1,59 @@
+/*
+ * 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;
+
+import java.util.Objects;
+import org.sosy_lab.java_smt.ResProofRule.ResAxiom;
+import org.sosy_lab.java_smt.api.Formula;
+import org.sosy_lab.java_smt.api.proofs.ProofNode;
+import org.sosy_lab.java_smt.api.proofs.ProofRule;
+import org.sosy_lab.java_smt.basicimpl.AbstractProofDAG;
+
+/**
+ * This class represents a resolution proof DAG. Its nodes might be of the type {@link
+ * AxiomProofNode} or {@link ResolutionProofNode}. It is used to represent proofs based on the
+ * RESOLUTE proof format from SMTInterpol.
+ *
+ * @see ResProofRule
+ */
+@SuppressWarnings("all")
+public class ResolutionProofDAG extends AbstractProofDAG {
+  // Work in progress. The functionality of producing just nodes should be provided first.
+  // The idea is to provide extended functionality (by providng a set of edges for example).
+
+  public static class ResolutionProofNode extends AbstractProofNode implements ProofNode {
+
+    private final Formula pivot;
+
+    public ResolutionProofNode(Formula formula, Formula pivot) {
+      super(ResAxiom.RESOLUTION, Objects.requireNonNull(formula, "Formula must not be null"));
+      this.pivot = Objects.requireNonNull(pivot, "Pivot must not be null");
+    }
+
+    public Formula getPivot() {
+      return pivot;
+    }
+
+    @Override
+    public ProofRule getRule() {
+      return super.getRule();
+    }
+  }
+
+  public static class AxiomProofNode extends AbstractProofNode implements ProofNode {
+
+    public AxiomProofNode(ResAxiom rule, Formula formula) {
+      super(
+          Objects.requireNonNull(rule, "Rule must not be null"),
+          Objects.requireNonNull(formula, "Formula must not be null"));
+    }
+  }
+}

src/org/sosy_lab/java_smt/SolverContextFactory.java

@@ -282,7 +282,8 @@ private SolverContext generateContext0(Solvers solverToCreate)
       case Z3:
         return Z3SolverContext.create(
             logger,
-            config,
+            Configuration.builder().copyFrom(config)
+                .setOption("solver.z3.requireProofs", "true").build(),
             shutdownNotifier,
             logfile,
             randomSeed,

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.ProofNode;
 
 /**
  * Super interface for {@link ProverEnvironment} and {@link InterpolatingProverEnvironment} that
@@ -149,6 +150,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>.
+   */
+  ProofNode 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/ProofDAG.java

@@ -0,0 +1,49 @@
+/*
+ * 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.Collection;
+import org.sosy_lab.java_smt.api.proofs.visitors.ProofVisitor;
+
+/**
+ * A DAG representing a proof. Each node in the DAG is a {@link ProofNode} and each edge is a
+ * directed edge from a parent node to a child node.
+ */
+public interface ProofDAG {
+
+  /**
+   * Add a node to the DAG.
+   *
+   * @param node The node to be added to the DAG.
+   */
+  void addNode(ProofNode node);
+
+  /**
+   * Get a node from the DAG.
+   *
+   * @param nodeId The ID of the node.
+   * @return A {@link ProofNode} based on its ID.
+   */
+  ProofNode getNode(int nodeId);
+
+  /**
+   * Add an edge to the DAG.
+   *
+   * @param parentNodeId Predecessor
+   * @param childNodeId Successor
+   */
+  void addEdge(int parentNodeId, int childNodeId);
+
+  /** Get all nodes in the DAG. */
+  Collection<ProofNode> getNodes();
+
+  void accept(ProofVisitor visitor); // To allow traversal of the entire DAG
+}

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

@@ -0,0 +1,80 @@
+/*
+ * 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 org.sosy_lab.java_smt.ResProofRule.ResAxiom;
+import org.sosy_lab.java_smt.ResolutionProofDAG.AxiomProofNode;
+import org.sosy_lab.java_smt.ResolutionProofDAG.ResolutionProofNode;
+import org.sosy_lab.java_smt.api.Formula;
+import org.sosy_lab.java_smt.api.ProverEnvironment;
+import org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5ProofNode;
+
+/**
+ * A factory for creating proof nodes. The methods of this class are to be used in the ProofNode
+ * implementations of each solver to be able to convert the proof object given back by the solver to
+ * a proof in JavaSMT.
+ *
+ * @param <T> The type of the proof object.
+ */
+public class ProofFactory<T> {
+
+  // private final FormulaCreator<?, ?, ?, ?> formulaCreator;
+  private final ProverEnvironment prover;
+  private final Solvers solver;
+
+  enum Solvers {
+    OPENSMT,
+    MATHSAT5,
+    SMTINTERPOL,
+    Z3,
+    PRINCESS,
+    BOOLECTOR,
+    CVC4,
+    CVC5,
+    YICES2,
+    BITWUZLA
+  }
+
+  protected ProofFactory(ProverEnvironment pProver, String pSolver) {
+    if (pProver == null) {
+      throw new NullPointerException("ProverEnvironment must not be null");
+    }
+    if (pSolver == null) {
+      throw new NullPointerException("Solver name must not be null");
+    }
+    prover = pProver;
+    solver = Solvers.valueOf(pSolver);
+  }
+
+  protected ProofNode createProofNode(T proof) {
+    return createProofNode0(proof);
+  }
+
+  protected ProofNode createProofNode0(T proof) {
+
+    switch (solver) {
+      case MATHSAT5:
+        return Mathsat5ProofNode.fromMsatProof(prover, (long) proof);
+      case CVC5:
+        return null;
+      default:
+        throw new UnsupportedOperationException("Unsupported solver: " + solver);
+    }
+  }
+
+  protected static ProofNode createSourceNode(ResAxiom rule, Formula formula) {
+    return new AxiomProofNode(rule, formula);
+  }
+
+  protected static ProofNode createResolutionNode(Formula formula, Formula pivot) {
+    return new ResolutionProofNode(formula, pivot);
+  }
+}