Develop a common proof format and export proofs

lib/native/source/libmathsat5j/includes/defines.h

@@ -372,6 +372,16 @@ typedef jvoid jjfailureCode;
 
 typedef jobject jjnamedtermswrapper;
 
+typedef jlong jjproofManager;
+#define MANAGER_ARG(num) STRUCT_ARG(msat_proof_manager, num)
+#define MANAGER_ARG_VOID(num) STRUCT_ARG_VOID(msat_proof_manager, num)
+#define MANAGER_RETURN STRUCT_RETURN
+
+typedef jlong jjproof;
+#define PROOF_ARG(num) STRUCT_ARG(msat_proof, num)
+#define PROOF_ARG_VOID(num) STRUCT_ARG_VOID(msat_proof, num)
+#define PROOF_RETURN STRUCT_RETURN
+
 // Abbreviations for common combinations of return and argument types
 //
 // Parameter explanation:

lib/native/source/libmathsat5j/org_sosy_1lab_java_1smt_solvers_mathsat5_Mathsat5NativeApi.c

@@ -1220,6 +1220,79 @@ TERM_ARRAY_OUTPUT_ARG(2)
 CALL2(msat_term*, get_unsat_core)
 RETURN_TERM_ARRAY(2)
 
+//Proof functions
+/*
+ * msat_proof_manager msat_get_proof_manager(msat_env e)
+ */
+DEFINE_FUNC(jproofManager, 1get_1proof_1manager) WITH_ONE_ARG(jenv)
+ENV_ARG(1)
+CALL1(msat_proof_manager, get_proof_manager)
+STRUCT_RETURN_WITH_ENV
+
+/*
+ * void msat_destroy_proof_manager(msat_proof_manager m)
+ */
+DEFINE_FUNC(void, 1destroy_1proof_1manager) WITH_ONE_ARG(jproofManager)
+MANAGER_ARG_VOID(1)
+VOID_CALL1(destroy_proof_manager)
+
+/*
+ * msat_proof msat_get_proof(msat_proof_manager m)
+ */
+DEFINE_FUNC(jproof, 1get_1proof) WITH_ONE_ARG(jproofManager)
+MANAGER_ARG(1)
+CALL1(msat_proof, get_proof)
+PROOF_RETURN
+
+/*
+ * size_t msat_proof_id(msat_proof p)
+ */
+DEFINE_FUNC(int, 1proof_1id) WITH_ONE_ARG(jproof)
+PROOF_ARG(1)
+CALL1(int, proof_id)
+INT_RETURN
+
+/*
+ * int msat_proof_is_term(msat_proof p)
+ */
+DEFINE_FUNC(int, 1proof_1is_1term) WITH_ONE_ARG(jproof)
+PROOF_ARG(1)
+CALL1(int, proof_is_term)
+BOOLEAN_RETURN
+
+/*
+ * msat_term msat_proof_get_term(msat_proof p)
+ */
+DEFINE_FUNC(jterm, 1proof_1get_1term) WITH_ONE_ARG(jproof)
+PROOF_ARG(1)
+CALL1(msat_term, proof_get_term)
+STRUCT_RETURN
+
+/*
+ * const char* msat_proof_get_name(msat_proof p)
+ */
+DEFINE_FUNC(string, 1proof_1get_1name) WITH_ONE_ARG(jproof)
+PROOF_ARG(1)
+CALL1(const char*, proof_get_name)
+PLAIN_CONST_STRING_RETURN
+
+/*
+ * size_t msat_proof_get_arity(msat_proof p)
+ */
+DEFINE_FUNC(int, 1proof_1get_1arity) WITH_ONE_ARG(jproof)
+PROOF_ARG(1)
+CALL1(size_t, proof_get_arity)
+INT_RETURN
+
+/*
+ * msat_proof msat_proof_get_child(msat_proof p, size_t i)
+ */
+DEFINE_FUNC(jproof, 1proof_1get_1child) WITH_TWO_ARGS(jproof, int)
+PROOF_ARG(1)
+SIMPLE_ARG(size_t, 2)
+CALL2(msat_proof, proof_get_child)
+PROOF_RETURN
+
 DEFINE_FUNC(jterm, 1simplify) WITH_FOUR_ARGS(jenv, jterm, jtermArray, int)
 ENV_ARG(1)
 TERM_ARG(2)

src/org/sosy_lab/java_smt/ResProofRule.java

@@ -0,0 +1,149 @@
+/*
+ * 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 org.sosy_lab.java_smt.api.proofs.ProofRule;
+
+/**
+ * A proof rule in the proof DAG of the internal proof format of JavaSMT.
+ *
+ * @author Gabriel Carpio
+ */
+public class ResProofRule {
+
+  /**
+   * 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 getResAxiomRuleByName(String name) {
+    if (name == null) {
+      throw new NullPointerException("Rule name cannot be null");
+    }
+
+    for (ResAxiom rule : ResAxiom.values()) {
+      if (rule.getName().equalsIgnoreCase(name)) {
+        return rule;
+      }
+    }
+
+    throw new IllegalArgumentException("Rule not found or not specified: " + name);
+  }
+
+}

src/org/sosy_lab/java_smt/ResolutionProofDag.java

@@ -0,0 +1,72 @@
+/*
+ * 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 org.sosy_lab.java_smt.basicimpl.AbstractProofDag;
+
+@SuppressWarnings("all")
+public class ResolutionProofDag extends AbstractProofDag {
+
+  /*
+  public ResolutionProofDAG() {
+    super();
+  }
+
+
+  public static ResolutionProofDAG fromTerm(
+      Term proof, FormulaManager pManager,
+      Map<String, BooleanFormula> pAnnotatedTerms) {
+
+    // Use our new ProofTermParser to convert the proof term to a ResolutionProofDAG
+    return ProofTermParser.convert(proof, pManager, pAnnotatedTerms);
+  }
+
+  private static void traverseTerm(Term term, ResolutionProofDAG dag, ProofNode parentClause) {
+    if (term instanceof AnnotatedTerm) {
+      AnnotatedTerm annotatedTerm = (AnnotatedTerm) term;
+      for (Annotation annotation : annotatedTerm.getAnnotations()) {
+        /*
+        if (annotation.getKey().equals(ProofConstants.ANNOTKEY_PROVES)) {
+          //ProofNode<ResAxiom> clause = annotation.getValue().toString();
+          if (parentClause != null) {
+            dag.addEdge(parentClause, clause);
+          } else {
+            dag.addNode(clause);
+          }
+          for (Term subTerm : annotatedTerm.getSubterms()) {
+            traverseTerm(subTerm, dag, clause);
+          }
+        }
+
+
+      }
+    }
+  }
+
+
+
+  @Override
+  public void addNode(ProofNode node) {
+    super.addNode(node);
+  }
+
+  @Override
+  public ProofNode getNode(int nodeId) {
+    return super.getNode(nodeId);
+  }
+
+  @Override
+  public void addEdge(int parentNodeId, int childNodeId) {
+    super.addEdge(parentNodeId, childNodeId);
+  }
+
+   */
+}

src/org/sosy_lab/java_smt/ResolutionProofNode.java

@@ -0,0 +1,45 @@
+/*
+ * 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.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.AbstractProofNode;
+import org.sosy_lab.java_smt.ResProofRule.ResAxiom;
+
+public 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");
+  }
+
+
+
+  @Override
+  public boolean isSource() {
+    return false;
+  }
+
+  public Formula getPivot() {
+    return pivot;
+  }
+
+  @Override
+  public ProofRule getRule() {
+    return super.getRule();
+  }
+}