Extend Mathsat5 Native Wrapper with API for Proofs

lib/ivy.xml

@@ -186,10 +186,10 @@ SPDX-License-Identifier: Apache-2.0
         <dependency org="edu.tum.cs" name="java-cup" rev="11b-20160615" conf="runtime-princess->runtime"/>
 
         <!-- Solver Binaries -->
-        <dependency org="org.sosy_lab" name="javasmt-solver-mathsat" rev="5.6.11-sosy0" conf="runtime-mathsat-x64->solver-mathsat-x64; runtime-mathsat-arm64->solver-mathsat-arm64" />
+        <dependency org="org.sosy_lab" name="javasmt-solver-mathsat" rev="5.6.11-sosy1" conf="runtime-mathsat-x64->solver-mathsat-x64; runtime-mathsat-arm64->solver-mathsat-arm64" />
         <dependency org="org.sosy_lab" name="javasmt-solver-z3" rev="4.14.0" conf="runtime-z3-x64->solver-z3-x64; runtime-z3-arm64->solver-z3-arm64; contrib->sources,javadoc" />
         <dependency org="org.sosy_lab" name="javasmt-solver-opensmt" rev="2.8.0-sosy0-ge831bf23" conf="runtime-opensmt-x64->solver-opensmt-x64; runtime-opensmt-arm64->solver-opensmt-arm64; contrib->sources,javadoc"/>
-        <dependency org="org.sosy_lab" name="javasmt-solver-optimathsat" rev="1.7.3-sosy0" conf="runtime-optimathsat->solver-optimathsat" />
+        <dependency org="org.sosy_lab" name="javasmt-solver-optimathsat" rev="1.7.3-sosy1" conf="runtime-optimathsat->solver-optimathsat" />
         <dependency org="org.sosy_lab" name="javasmt-solver-cvc4" rev="1.8-prerelease-2020-06-24-g7825d8f28" conf="runtime-cvc4->solver-cvc4" />
         <dependency org="org.sosy_lab" name="javasmt-solver-cvc5" rev="1.0.5-g4cb2ab9eb" conf="runtime-cvc5->solver-cvc5" />
         <dependency org="org.sosy_lab" name="javasmt-solver-boolector" rev="3.2.2-g1a89c229" conf="runtime-boolector->solver-boolector" />

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

@@ -310,6 +310,16 @@ typedef jlong jjenv;
 #define ENV_ARG_VOID(num) STRUCT_ARG_VOID(msat_env, num)
 #define ENV_RETURN STRUCT_RETURN
 
+typedef jlong jjproofmgr;
+#define PROOF_MGR_ARG(num) STRUCT_ARG(msat_proof_manager, num)
+#define PROOF_MGR_ARG_VOID(num) STRUCT_ARG_VOID(msat_proof_manager, num)
+#define PROOF_MGR_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
+
 typedef jlong jjconf;
 #define CONF_ARG(num) STRUCT_ARG(msat_config, num)
 #define CONF_ARG_VOID(num) STRUCT_ARG_VOID(msat_config, num)

lib/native/source/libmathsat5j/org_sosy_1lab_java_1smt_solvers_mathsat5_Mathsat5NativeApi.c

@@ -132,6 +132,51 @@ FREE_STRING_ARG(3)
 FREE_STRING_ARG(2)
 INT_RETURN
 
+DEFINE_FUNC(long, 1get_1proof_1manager) WITH_ONE_ARG(jenv)
+ENV_ARG(1)
+CALL1(msat_proof_manager, get_proof_manager)
+STRUCT_RETURN_WITH_ENV
+
+DEFINE_FUNC(jproof, 1get_1proof) WITH_ONE_ARG(jproofmgr)
+PROOF_MGR_ARG(1)
+CALL1(msat_proof, get_proof)
+PROOF_RETURN
+
+DEFINE_FUNC(int, 1proof_1get_1arity) WITH_ONE_ARG(jproof)
+PROOF_ARG(1)
+CALL1(int, proof_get_arity)
+INT_RETURN
+
+DEFINE_FUNC(jproof, 1proof_1get_1child) WITH_TWO_ARGS(jproof, int)
+PROOF_ARG(1)
+SIMPLE_ARG(int, 2)
+CALL2(msat_proof, proof_get_child)
+PROOF_RETURN
+
+DEFINE_FUNC(string, 1proof_1get_1name) WITH_ONE_ARG(jproof)
+PROOF_ARG(1)
+CALL1(const char *, proof_get_name)
+PLAIN_CONST_STRING_RETURN
+
+DEFINE_FUNC(jboolean, 1proof_1is_1term) WITH_ONE_ARG(jproof)
+PROOF_ARG(1)
+CALL1(int, proof_is_term)
+BOOLEAN_RETURN
+
+DEFINE_FUNC(jterm, 1proof_1get_1term) WITH_ONE_ARG(jproof)
+PROOF_ARG(1)
+CALL1(msat_term, proof_get_term)
+STRUCT_RETURN
+
+DEFINE_FUNC(int, 1proof_1id) WITH_ONE_ARG(jproof)
+PROOF_ARG(1)
+CALL1(int, proof_id)
+INT_RETURN
+
+DEFINE_FUNC(void, 1destroy_1proof_1manager) WITH_ONE_ARG(jproofmgr)
+PROOF_MGR_ARG_VOID(1)
+VOID_CALL1(destroy_proof_manager)
+
 /*
  * msat_type msat_get_bool_type(msat_env env);
  */

src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApi.java

@@ -1064,4 +1064,37 @@ private static native int msat_all_sat(
    * @param o msat_objective to push on the stack
    */
   public static native void msat_assert_objective(long e, long o);
+
+  /**
+   * Returns a proof manager for the given environment. The manager must be destroyed by the user,
+   * with msat_destroy_proof_manager. In order to obtain a non-error result, the option
+   * "proof_generation" must be set to "true" in the configuration used for creating the
+   * environment.
+   *
+   * @param env The environment in which to operate.
+   * @return A proof manager for the environment. MSAT_ERROR_PROOF_MANAGER can be used to check
+   *     whether an error occurred.
+   */
+  public static native long msat_get_proof_manager(long env);
+
+  /** Get current proof from a manager. */
+  public static native long msat_get_proof(long proofMgr);
+
+  public static native int msat_proof_get_arity(long proof);
+
+  // Child is also a proof
+  public static native long msat_proof_get_child(long proof, int i);
+
+  public static native String msat_proof_get_name(long proof);
+
+  public static native boolean msat_proof_is_term(long proof);
+
+  // Term representation of the current proof
+  public static native long msat_proof_get_term(long proof);
+
+  // Can be used to check for the equality of proofs
+  public static native int msat_proof_id(long proof);
+
+  // Cleans up the proof manager and the associated proof
+  public static native void msat_destroy_proof_manager(long proofMgr);
 }

src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApiTest.java

@@ -17,12 +17,15 @@
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_decl_get_name;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_destroy_config;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_destroy_model_iterator;
+import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_destroy_proof_manager;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_from_smtlib2;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_get_enum_constants;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_get_enum_type;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_get_integer_type;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_get_model;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_get_model_value;
+import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_get_proof;
+import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_get_proof_manager;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_get_rational_type;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_is_enum_type;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_is_integer_type;
@@ -43,6 +46,11 @@
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_model_iterator_has_next;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_model_iterator_next;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_pop_backtrack_point;
+import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_proof_get_arity;
+import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_proof_get_child;
+import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_proof_get_name;
+import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_proof_id;
+import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_proof_is_term;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_push_backtrack_point;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_set_option_checked;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_term_get_type;
@@ -90,6 +98,56 @@ public void createEnvironment() {
     var = msat_make_variable(env, "rat", rationalType);
   }
 
+  @Test
+  public void proofTest() throws IllegalStateException, InterruptedException, SolverException {
+    long cfg = msat_create_config();
+
+    msat_set_option_checked(cfg, "proof_generation", "true");
+
+    env = msat_create_env(cfg);
+    msat_destroy_config(cfg);
+
+    const0 = msat_make_number(env, "0");
+    const1 = msat_make_number(env, "1");
+    long rationalType = msat_get_rational_type(env);
+    var = msat_make_variable(env, "rat", rationalType);
+
+    msat_push_backtrack_point(env);
+
+    msat_assert_formula(env, msat_make_equal(env, var, const0));
+    msat_assert_formula(env, msat_make_equal(env, var, const1));
+
+    // UNSAT
+    assertThat(msat_check_sat(env)).isFalse();
+
+    long proofMgr = msat_get_proof_manager(env);
+    long proof = msat_get_proof(proofMgr);
+
+    assertThat(msat_proof_is_term(proof)).isFalse();
+
+    assertThat(msat_proof_get_arity(proof)).isEqualTo(1);
+
+    String proofName = msat_proof_get_name(proof);
+    assertThat(proofName).isEqualTo("res-chain");
+
+    // Child is also a proof
+    long proofChild = msat_proof_get_child(proof, 0);
+    assertThat(msat_proof_get_name(proofChild)).isEqualTo("clause-hyp");
+    assertThat(msat_proof_is_term(proofChild)).isFalse();
+    assertThat(msat_proof_get_arity(proofChild)).isEqualTo(0);
+
+    // Can be used to check for the equality of proofs
+    int proofID = msat_proof_id(proof);
+    int proofChildID = msat_proof_id(proofChild);
+    assertThat(proofChildID).isNotEqualTo(proofID);
+
+    // TODO: test term representation of a proof
+    // long term = msat_proof_get_term(proofChild2);
+
+    // Cleans up the proof manager and the associated proof
+    msat_destroy_proof_manager(proofMgr);
+  }
+
   /** x == 0 and sin(x) == 0 SAT; x == 1 and sin(x) == 0 UNSAT. */
   @Test
   public void sinTest() throws IllegalStateException, InterruptedException, SolverException {