Develop a common proof format and export proofs

src/org/sosy_lab/java_smt/ResProofRule.java

@@ -0,0 +1,156 @@
+/*
+ * 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.ENGLISH), 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.ENGLISH));
+    return rule;
+  }
+}

src/org/sosy_lab/java_smt/ResolutionProof.java

@@ -0,0 +1,68 @@
+/*
+ * 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.ProofRule;
+import org.sosy_lab.java_smt.basicimpl.AbstractProof;
+
+/**
+ * This class represents a resolution proof DAG. Its nodes might be of the type {@link
+ * AxiomSubproof} or {@link ResolutionSubproof}. It is used to represent proofs based on the
+ * RESOLUTE proof format from SMTInterpol.
+ *
+ * @see ResProofRule
+ */
+public class ResolutionProof extends AbstractProof {
+  // 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 ResolutionSubproof extends AbstractSubproof implements Subproof {
+
+    private final Formula pivot;
+
+    @Override
+    public void addChild(Subproof pSubproof) {
+      super.addChild(pSubproof);
+    }
+
+    public ResolutionSubproof(Formula formula, Formula pivot, AbstractProof p) {
+      super(ResAxiom.RESOLUTION, Objects.requireNonNull(formula, "Formula must not be null"), p);
+      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 AxiomSubproof extends AbstractSubproof implements Subproof {
+
+    public AxiomSubproof(ResAxiom rule, Formula formula, AbstractProof proof) {
+      super(
+          Objects.requireNonNull(rule, "Rule must not be null"),
+          Objects.requireNonNull(formula, "Formula must not be null"),
+          proof);
+    }
+
+    @Override
+    protected void addChild(Subproof pSubproof) {
+      super.addChild(pSubproof);
+    }
+  }
+}

src/org/sosy_lab/java_smt/SolverContextFactory.java

@@ -282,7 +282,7 @@ private SolverContext generateContext0(Solvers solverToCreate)
       case Z3:
         return Z3SolverContext.create(
             logger,
-            config,
+            Configuration.builder().copyFrom(config).setOption("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.Proof.Subproof;
 
 /**
  * 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>.
+   */
+  Subproof 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,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 java.util.Set;
+import org.sosy_lab.java_smt.api.Formula;
+
+/**
+ * A DAG representing a proof. Each node in the DAG is a {@link Subproof} and each edge is a
+ * directed edge from a parent node to a child node.
+ */
+public interface Proof {
+
+  /** Get all proof steps in the proof. */
+  Collection<Subproof> getSubproofs();
+
+  /**
+   * A proof node in the proof DAG of a proof.
+   *
+   * @author Gabriel Carpio
+   */
+  interface Subproof {
+
+    /** Get the children of the proof node. */
+    Set<Subproof> getArguments();
+
+    boolean isLeaf();
+
+    /**
+     * Get the formula of the proof node.
+     *
+     * @return The formula of the proof node.
+     */
+    Formula getFormula();
+
+    ProofRule getRule();
+
+    Proof getDAG();
+  }
+}

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,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 <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();
+
+  /** Get the formula of the proof rule. */
+  default String getFormula() {
+    return "no formula available";
+  }
+}