From 269ac90f181a7c53f6c7828c3c85c63e9a5e216f Mon Sep 17 00:00:00 2001 From: BaierD Date: Wed, 19 Mar 2025 18:54:08 +0100 Subject: [PATCH 1/9] Add proof Java API for the MathSAT5 native wrapper --- .../solvers/mathsat5/Mathsat5NativeApi.java | 42 +++++++++++++++++++ 1 file changed, 42 insertions(+) diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApi.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApi.java index 227a91713d..c76858c392 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApi.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApi.java @@ -1064,4 +1064,46 @@ 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. + // 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. + + /** + * 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); + + // Non-zero if term, 0 for no term + 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); } From e2b6434889faaa172dcceea45fd44eb9b5503880 Mon Sep 17 00:00:00 2001 From: BaierD Date: Wed, 19 Mar 2025 18:54:31 +0100 Subject: [PATCH 2/9] Add proof definitions for the MathSAT5 wrapper --- lib/native/source/libmathsat5j/includes/defines.h | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/lib/native/source/libmathsat5j/includes/defines.h b/lib/native/source/libmathsat5j/includes/defines.h index 296479e1d5..57d1b5e0b4 100644 --- a/lib/native/source/libmathsat5j/includes/defines.h +++ b/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) From 1d05d3b25e5ee51037bbea1b221b041e2901621e Mon Sep 17 00:00:00 2001 From: BaierD Date: Wed, 19 Mar 2025 18:54:42 +0100 Subject: [PATCH 3/9] Add proof native API macros for the MathSAT5 wrapper --- ..._1smt_solvers_mathsat5_Mathsat5NativeApi.c | 45 +++++++++++++++++++ 1 file changed, 45 insertions(+) diff --git a/lib/native/source/libmathsat5j/org_sosy_1lab_java_1smt_solvers_mathsat5_Mathsat5NativeApi.c b/lib/native/source/libmathsat5j/org_sosy_1lab_java_1smt_solvers_mathsat5_Mathsat5NativeApi.c index 1c43edf726..9258c15184 100644 --- a/lib/native/source/libmathsat5j/org_sosy_1lab_java_1smt_solvers_mathsat5_Mathsat5NativeApi.c +++ b/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(int, 1proof_1is_1term) WITH_ONE_ARG(jproof) +PROOF_ARG(1) +CALL1(int, proof_is_term) +INT_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(1) +VOID_CALL1(destroy_proof_manager) + /* * msat_type msat_get_bool_type(msat_env env); */ From 08c5594c7896c72af99fc03b7723da308ad3674b Mon Sep 17 00:00:00 2001 From: BaierD Date: Wed, 19 Mar 2025 18:55:07 +0100 Subject: [PATCH 4/9] Add native test for Mathsat5 proof API --- .../mathsat5/Mathsat5NativeApiTest.java | 58 +++++++++++++++++++ 1 file changed, 58 insertions(+) diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApiTest.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApiTest.java index d9021f64cd..261c2f305f 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApiTest.java +++ b/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 { From 120c2c6f9387982c772a5fba25973bfdabfc9eaa Mon Sep 17 00:00:00 2001 From: BaierD Date: Thu, 20 Mar 2025 12:02:36 +0100 Subject: [PATCH 5/9] Switch int return to bool return for boolean Mathsat5 5 native call in the wrapper --- ...g_sosy_1lab_java_1smt_solvers_mathsat5_Mathsat5NativeApi.c | 4 ++-- .../sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApi.java | 1 - 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/lib/native/source/libmathsat5j/org_sosy_1lab_java_1smt_solvers_mathsat5_Mathsat5NativeApi.c b/lib/native/source/libmathsat5j/org_sosy_1lab_java_1smt_solvers_mathsat5_Mathsat5NativeApi.c index 9258c15184..32b4182eed 100644 --- a/lib/native/source/libmathsat5j/org_sosy_1lab_java_1smt_solvers_mathsat5_Mathsat5NativeApi.c +++ b/lib/native/source/libmathsat5j/org_sosy_1lab_java_1smt_solvers_mathsat5_Mathsat5NativeApi.c @@ -158,10 +158,10 @@ PROOF_ARG(1) CALL1(const char *, proof_get_name) PLAIN_CONST_STRING_RETURN -DEFINE_FUNC(int, 1proof_1is_1term) WITH_ONE_ARG(jproof) +DEFINE_FUNC(jboolean, 1proof_1is_1term) WITH_ONE_ARG(jproof) PROOF_ARG(1) CALL1(int, proof_is_term) -INT_RETURN +BOOLEAN_RETURN DEFINE_FUNC(jterm, 1proof_1get_1term) WITH_ONE_ARG(jproof) PROOF_ARG(1) diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApi.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApi.java index c76858c392..d17fb7a643 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApi.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApi.java @@ -1095,7 +1095,6 @@ private static native int msat_all_sat( public static native String msat_proof_get_name(long proof); - // Non-zero if term, 0 for no term public static native boolean msat_proof_is_term(long proof); // Term representation of the current proof From 9a6f40093fc347daf3a4b6d64ee7d3689ae3bc64 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sat, 22 Mar 2025 21:14:39 +0100 Subject: [PATCH 6/9] MathSAT5: remove redundant code documentation. --- .../java_smt/solvers/mathsat5/Mathsat5NativeApi.java | 8 -------- 1 file changed, 8 deletions(-) diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApi.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApi.java index d17fb7a643..f0862ddaf8 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApi.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApi.java @@ -1065,14 +1065,6 @@ private static native int msat_all_sat( */ 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. - // 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. - /** * 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 From ed6cd8a6c35d5714ce0e8988075bd5a1c8d6ca10 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sat, 22 Mar 2025 21:39:57 +0100 Subject: [PATCH 7/9] MathSAT5: fix compilation warning. The return-value for an invalid argument needs to match VOID if the function-call itself has VOID return type. --- ...org_sosy_1lab_java_1smt_solvers_mathsat5_Mathsat5NativeApi.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/native/source/libmathsat5j/org_sosy_1lab_java_1smt_solvers_mathsat5_Mathsat5NativeApi.c b/lib/native/source/libmathsat5j/org_sosy_1lab_java_1smt_solvers_mathsat5_Mathsat5NativeApi.c index 32b4182eed..e8c2d2120f 100644 --- a/lib/native/source/libmathsat5j/org_sosy_1lab_java_1smt_solvers_mathsat5_Mathsat5NativeApi.c +++ b/lib/native/source/libmathsat5j/org_sosy_1lab_java_1smt_solvers_mathsat5_Mathsat5NativeApi.c @@ -174,7 +174,7 @@ CALL1(int, proof_id) INT_RETURN DEFINE_FUNC(void, 1destroy_1proof_1manager) WITH_ONE_ARG(jproofmgr) -PROOF_MGR_ARG(1) +PROOF_MGR_ARG_VOID(1) VOID_CALL1(destroy_proof_manager) /* From 6e7849ed0e1450d2f39c155b025c07f7a4fab0f2 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sat, 22 Mar 2025 21:42:28 +0100 Subject: [PATCH 8/9] MathSAT5: update to compiled version in v 5.6.11. The new version comes with proof-support in the API. --- lib/ivy.xml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/ivy.xml b/lib/ivy.xml index 38d7d17d16..2e3e8de469 100644 --- a/lib/ivy.xml +++ b/lib/ivy.xml @@ -186,7 +186,7 @@ SPDX-License-Identifier: Apache-2.0 - + From 734da44d77d1ddd835d3345953f2c8f23356940c Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sat, 22 Mar 2025 21:56:24 +0100 Subject: [PATCH 9/9] OptiMathSAT: update to compiled version in v1.7.3. The new version comes with proof-support in the API. --- lib/ivy.xml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/ivy.xml b/lib/ivy.xml index 2e3e8de469..9bc2230cb6 100644 --- a/lib/ivy.xml +++ b/lib/ivy.xml @@ -189,7 +189,7 @@ SPDX-License-Identifier: Apache-2.0 - +