From 5a31718ffd6a983e3162d0288f4d0999eec30a4f Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Wed, 26 Jun 2024 10:58:07 -0700 Subject: [PATCH] c api: Add support for proofs. (#10877) --- include/cvc5/c/cvc5.h | 145 +++++---- include/cvc5/cvc5.h | 11 +- src/api/c/cvc5.cpp | 277 ++++++++++++++++++ src/api/c/cvc5_checks.h | 13 + src/api/cpp/cvc5.cpp | 6 +- src/proof/proof_node.cpp | 9 +- src/proof/proof_node.h | 11 + test/unit/api/c/CMakeLists.txt | 2 + test/unit/api/c/capi_proof_black.cpp | 210 +++++++++++++ test/unit/api/c/capi_proof_rule_black.cpp | 67 +++++ test/unit/api/c/capi_solver_black.cpp | 208 +++++++++++++ test/unit/api/cpp/CMakeLists.txt | 2 +- .../{proof_black.cpp => api_proof_black.cpp} | 1 + test/unit/api/cpp/api_proof_rule_black.cpp | 6 +- test/unit/api/cpp/api_solver_black.cpp | 2 +- 15 files changed, 908 insertions(+), 62 deletions(-) create mode 100644 test/unit/api/c/capi_proof_black.cpp create mode 100644 test/unit/api/c/capi_proof_rule_black.cpp rename test/unit/api/cpp/{proof_black.cpp => api_proof_black.cpp} (98%) diff --git a/include/cvc5/c/cvc5.h b/include/cvc5/c/cvc5.h index 4d259e318cf..8efe88d543e 100644 --- a/include/cvc5/c/cvc5.h +++ b/include/cvc5/c/cvc5.h @@ -120,7 +120,7 @@ typedef struct Cvc5OptionInfo Cvc5OptionInfo; /** * A cvc5 proof. */ -typedef struct Cvc5Proof Cvc5Proof; +typedef struct cvc5_proof_t* Cvc5Proof; /** * A cvc5 statistics instance. @@ -3180,83 +3180,70 @@ const char* cvc5_option_info_to_string(const Cvc5OptionInfo* info); * Get the proof rule used by the root step of a given proof. * @return The proof rule. */ -Cvc5ProofRule cvc5_proof_get_rule(Cvc5Proof* proof); +Cvc5ProofRule cvc5_proof_get_rule(Cvc5Proof proof); /** - * @return The proof rewrite rule used by the root step of the proof. + * Get the proof rewrite rule used by the root step of the proof. * - * @exception raises an exception if `getRule()` does not return - * `CVC5_PROOF_RULE_DSL_REWRITE`. + * Requires that `cvc5_proof_get_rule()` does not return + * `CVC5_PROOF_REWRITE_RULE_DSL_REWRITE` or + * `CVC5_PROOF_REWRITE_RULE_THEORY_REWRITE`. + * + * @param proof The proof. + * @return The proof rewrite rule. */ -Cvc5ProofRewriteRule cvc5_proof_get_rewrite_rule(Cvc5Proof* proof); +Cvc5ProofRewriteRule cvc5_proof_get_rewrite_rule(Cvc5Proof proof); /** * Get the conclusion of the root step of a given proof. + * @param proof The proof. * @return The conclusion term. */ -Cvc5Term cvc5_proof_get_result(Cvc5Proof* proof); +Cvc5Term cvc5_proof_get_result(Cvc5Proof proof); /** * Get the premises of the root step of a given proof. - * @param size Output parameter to store the number of resulting premise proofs. + * @param proof The proof. + * @param size Output parameter to store the number of resulting premise + * proofs. * @return The premise proofs. + * @note The returned Cvc5Proof array pointer is only valid until the next call + * to this function. */ -const Cvc5Proof** cvc5_proof_get_children(Cvc5Proof* proof); +const Cvc5Proof* cvc5_proof_get_children(Cvc5Proof proof, size_t* size); /** * Get the arguments of the root step of a given proof. - * @param size Output parameter to store the number of resulting argument terms. + * @param proof The proof. + * @param size Output parameter to store the number of resulting argument + * terms. * @return The argument terms. */ -const Cvc5Term* cvc5_proof_get_arguments(Cvc5Proof* proof); +const Cvc5Term* cvc5_proof_get_arguments(Cvc5Proof proof, size_t* size); /** * Compare two proofs for referential equality. * @param a The first proof. * @param b The second proof. - * @return `true` if both proofs point to the same internal proof object. + * @return True if both proof pointers point to the same internal proof object. */ -bool cvc5_proof_is_equal(Cvc5Proof* a, Cvc5Proof* b); +bool cvc5_proof_is_equal(Cvc5Proof a, Cvc5Proof b); /** * Compare two proofs for referential disequality. * @param a The first proof. * @param b The second proof. - * @return `true` if the proofs point to different internal proof objects. + * @return True if both proof pointers point to different internal proof + * objects. */ -bool cvc5_proof_is_disequal(Cvc5Proof* a, Cvc5Proof* b); +bool cvc5_proof_is_disequal(Cvc5Proof a, Cvc5Proof b); /** * Compute the hash value of a proof. * @param proof The proof. * @return The hash value of the proof. */ -size_t cvc5_proof_hash(Cvc5Proof* proof); - -/** - * Prints a proof as a string in a selected proof format mode. - * Other aspects of printing are taken from the solver options. - * - * @warning This function is experimental and may change in future versions. - * - * @param proof A proof, usually obtained from Solver::getProof(). - * @param format The proof format used to print the proof. Must be - * `modes::ProofFormat::NONE` if the proof is from a component other than - * `modes::ProofComponent::FULL`. - * @param assertions_size The number of assertions to names mappings given. - * @param assertions The list of assertions that are mapped to - * `assertions_names`. May be NULL if `assertions_size` is 0. - * @param assertion_names The names of the `assertions` (1:1 mapping). May - * by NULL if `assertions` is NULL. - * @return The string representation of the proof in the given format. - * @note The returned char* pointer is only valid until the next call to this - * function. - */ -const char* cvc5_proof_to_string(Cvc5Proof* proof, - Cvc5ProofFormat format, - size_t assertions_size, - const Cvc5Term assertions[], - const char* assertion_names[]); +size_t cvc5_proof_hash(Cvc5Proof proof); /* -------------------------------------------------------------------------- */ /* Cvc5 */ @@ -3290,13 +3277,13 @@ void cvc5_delete(Cvc5* cvc5); * (declare-datatype ) * \endverbatim * - * @param solver The solver instance. + * @param cvc5 The solver instance. * @param symbol The name of the datatype sort. * @param size The number of constructor declarations of the datatype sort. * @param ctors The constructor declarations. * @return The datatype sort. */ -Cvc5Sort cvc5_declare_dt(Cvc5* solver, +Cvc5Sort cvc5_declare_dt(Cvc5* cvc5, const char* symbol, size_t size, const Cvc5DatatypeConstructorDecl ctors[]); @@ -3312,7 +3299,7 @@ Cvc5Sort cvc5_declare_dt(Cvc5* solver, * (declare-fun ( * ) ) * \endverbatim * - * @param solver The solver instance. + * @param cvc5 The solver instance. * @param symbol The name of the function. * @param size The number of domain sorts of the function. * @param sorts The domain sorts of the function. @@ -3322,7 +3309,7 @@ Cvc5Sort cvc5_declare_dt(Cvc5* solver, * the given sorts and symbol where fresh is false. * @return The function. */ -Cvc5Term cvc5_declare_fun(Cvc5* solver, +Cvc5Term cvc5_declare_fun(Cvc5* cvc5, const char* symbol, size_t size, const Cvc5Sort sorts[], @@ -3344,13 +3331,13 @@ Cvc5Term cvc5_declare_fun(Cvc5* solver, * `cvc5_mk_uninterpreted_sort()` if arity = 0, and to * `cvc5_mk_uninterpreted_sort_constructor_sort()` if arity > 0. * - * @param solver The solver instance. + * @param cvc5 The solver instance. * @param symbol The name of the sort. * @param arity The arity of the sort. * @param fresh If true, then this method always returns a new Sort. * @return The sort. */ -Cvc5Sort cvc5_declare_sort(Cvc5* solver, +Cvc5Sort cvc5_declare_sort(Cvc5* cvc5, const char* symbol, uint32_t arity, bool fresh); @@ -3675,6 +3662,33 @@ const Cvc5Term* cvc5_get_unsat_assumptions(Cvc5* cvc5, size_t* size); */ const Cvc5Term* cvc5_get_unsat_core(Cvc5* cvc5, size_t* size); +/** + * Get the lemmas used to derive unsatisfiability. + * + * SMT-LIB: + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (get-unsat-core-lemmas) + * + * Requires the SAT proof unsat core mode, so to enable option + * :ref:`unsat-core-mode=sat-proof `. + * + * \endverbatim + * + * @warning This function is experimental and may change in future versions. + * + * @note The returned Cvc5Term array pointer is only valid until the next call + * to this function. + * + * @param cvc5 The solver instance. + * @param size The size of the resulting unsat core. + * @return A set of terms representing the lemmas used to derive + * unsatisfiability. + */ +const Cvc5Term* cvc5_get_unsat_core_lemmas(Cvc5* cvc5, size_t* size); + /** * Get a difficulty estimate for an asserted formula. This function is * intended to be called immediately after any response to a checkSat. @@ -3806,10 +3820,14 @@ const Cvc5Term* cvc5_get_timeout_core_assuming(Cvc5* cvc5, * @warning This function is experimental and may change in future versions. * * @param cvc5 The solver instance. - * @param c The component of the proof to return + * @param c The component of the proof to return + * @param size The size of the resulting array of proofs. * @return An array of proofs. + * + * @note The returned Cvc5Proof array pointer is only valid until the next call + * to this function. */ -Cvc5Proof** cvc5_get_proof(Cvc5* cvc5, Cvc5ProofComponent c); +const Cvc5Proof* cvc5_get_proof(Cvc5* cvc5, Cvc5ProofComponent c, size_t* size); /** * Get a list of learned literals that are entailed by the current set of @@ -4751,6 +4769,35 @@ bool cvc5_is_output_on(const char* tag); */ const char* cvc5_get_version(Cvc5* cvc5); +/** + * Prints a proof as a string in a selected proof format mode. + * Other aspects of printing are taken from the solver options. + * + * @warning This function is experimental and may change in future versions. + * + * @param cvc5 The solver instance. + * @param proof A proof, usually obtained from Solver::getProof(). + * @param format The proof format used to print the proof. Must be + * `modes::ProofFormat::NONE` if the proof is from a component + * other than `modes::ProofComponent::FULL`. + * @param size The number of assertions to names mappings given. + * @param assertions The list of assertions that are mapped to + * `assertions_names`. May be NULL if `assertions_size` is 0. + * @param names The names of the `assertions` (1:1 mapping). May by NULL + * if `assertions` is NULL. + * + * @return The string representation of the proof in the given format. + * + * @note The returned char* pointer is only valid until the next call to this + * function. + */ +const char* cvc5_proof_to_string(Cvc5* cvc5, + Cvc5Proof proof, + Cvc5ProofFormat format, + size_t size, + const Cvc5Term assertions[], + const char* names[]); + #if __cplusplus } #endif diff --git a/include/cvc5/cvc5.h b/include/cvc5/cvc5.h index deb2886f324..ca6e2b27889 100644 --- a/include/cvc5/cvc5.h +++ b/include/cvc5/cvc5.h @@ -3628,10 +3628,13 @@ class CVC5_EXPORT Proof ProofRule getRule() const; /** - * @return The proof rewrite rule used by the root step of the proof. + * Get the proof rewrite rule used by the root step of the proof. + * + * Requires that `getRule()` does not return `DSL_REWRITE` or + * `THEORY_REWRITE`. + * + * @return The proof rewrite rule. * - * @exception raises an exception if `getRule()` does not return - * `DSL_REWRITE` or `THEORY_REWRITE`. */ ProofRewriteRule getRewriteRule() const; @@ -3989,7 +3992,7 @@ class CVC5_EXPORT TermManager * Create n-ary term of given kind. * @param kind The kind of the term. * @param children The children of the term. - * @return The Term + * @return The term. */ Term mkTerm(Kind kind, const std::vector& children = {}); /** diff --git a/src/api/c/cvc5.cpp b/src/api/c/cvc5.cpp index 60326d03d1c..4d24763bb4c 100644 --- a/src/api/c/cvc5.cpp +++ b/src/api/c/cvc5.cpp @@ -147,6 +147,45 @@ const char* cvc5_modes_proof_format_to_string(Cvc5ProofFormat format) return str.c_str(); } +/* -------------------------------------------------------------------------- */ +/* Cvc5ProofRule */ +/* -------------------------------------------------------------------------- */ + +const char* cvc5_proof_rule_to_string(Cvc5ProofRule rule) +{ + static thread_local std::string str; + CVC5_CAPI_TRY_CATCH_BEGIN; + CVC5_CAPI_CHECK_PROOF_RULE(rule); + str = std::to_string(static_cast(rule)); + CVC5_CAPI_TRY_CATCH_END; + return str.c_str(); +} + +size_t cvc5_proof_rule_hash(Cvc5ProofRule rule) +{ + return std::hash{}(static_cast(rule)); +} + +/* -------------------------------------------------------------------------- */ +/* Cvc5ProofRewriteRule */ +/* -------------------------------------------------------------------------- */ + +const char* cvc5_proof_rewrite_rule_to_string(Cvc5ProofRewriteRule rule) +{ + static thread_local std::string str; + CVC5_CAPI_TRY_CATCH_BEGIN; + CVC5_CAPI_CHECK_PROOF_REWRITE_RULE(rule); + str = std::to_string(static_cast(rule)); + CVC5_CAPI_TRY_CATCH_END; + return str.c_str(); +} + +size_t cvc5_proof_rewrite_rule_hash(Cvc5ProofRewriteRule rule) +{ + return std::hash{}( + static_cast(rule)); +} + /* -------------------------------------------------------------------------- */ /* Cvc5FindSynthTarget */ /* -------------------------------------------------------------------------- */ @@ -4047,6 +4086,25 @@ struct cvc5_result_t Cvc5* d_cvc5 = nullptr; }; +/** Wrapper for cvc5 C++ proofs. */ +struct cvc5_proof_t +{ + /** + * Constructor. + * @param proof The wrapped C++ proof. + */ + cvc5_proof_t(Cvc5* cvc5, const cvc5::Proof& proof) + : d_proof(proof), d_cvc5(cvc5) + { + } + /** The wrapped C++ proof. */ + cvc5::Proof d_proof; + /** External refs count. */ + uint32_t d_refs = 1; + /** The associated solver instance. */ + Cvc5* d_cvc5 = nullptr; +}; + /** Wrapper for cvc5 C++ solver instance. */ struct Cvc5 { @@ -4071,12 +4129,32 @@ struct Cvc5 */ cvc5_result_t* copy(cvc5_result_t* result); + /** + * Export C++ proof to C API. + * @param proof The proof to export. + */ + Cvc5Proof export_proof(const cvc5::Proof& proof); + /** + * Decrement the external ref count of a proof. If the ref count reaches + * zero, the proof is released (freed). + * @param term The term to release. + */ + void release(cvc5_proof_t* proof); + /** + * Increment the external ref count of a proof. + * @param proof The proof to copy. + * @return The copied proof. + */ + cvc5_proof_t* copy(cvc5_proof_t* proof); + /** The associated cvc5 instance. */ cvc5::Solver d_solver; /** The associated term manager. */ Cvc5TermManager* d_tm = nullptr; /** Cache of allocated results. */ std::unordered_map d_alloc_results; + /** Cache of allocated proofs. */ + std::unordered_map d_alloc_proofs; }; Cvc5Result Cvc5::export_result(const cvc5::Result& result) @@ -4106,6 +4184,32 @@ cvc5_result_t* Cvc5::copy(cvc5_result_t* result) return result; } +Cvc5Proof Cvc5::export_proof(const cvc5::Proof& proof) +{ + auto [it, inserted] = d_alloc_proofs.try_emplace(proof, this, proof); + if (!inserted) + { + copy(&it->second); + } + return &it->second; +} + +void Cvc5::release(cvc5_proof_t* proof) +{ + proof->d_refs -= 1; + if (proof->d_refs == 0) + { + Assert(d_alloc_proofs.find(proof->d_proof) != d_alloc_proofs.end()); + d_alloc_proofs.erase(proof->d_proof); + } +} + +cvc5_proof_t* Cvc5::copy(cvc5_proof_t* proof) +{ + proof->d_refs += 1; + return proof; +} + /* -------------------------------------------------------------------------- */ /* Cvc5Result */ /* -------------------------------------------------------------------------- */ @@ -4222,6 +4326,116 @@ const char* cvc5_result_to_string(const Cvc5Result result) return str.c_str(); } +/* -------------------------------------------------------------------------- */ +/* Cvc5Proof */ +/* -------------------------------------------------------------------------- */ + +Cvc5ProofRule cvc5_proof_get_rule(Cvc5Proof proof) +{ + Cvc5ProofRule res = CVC5_PROOF_RULE_LAST; + CVC5_CAPI_TRY_CATCH_BEGIN; + CVC5_CAPI_CHECK_PROOF(proof); + res = static_cast(proof->d_proof.getRule()); + CVC5_CAPI_TRY_CATCH_END; + return res; +} + +Cvc5ProofRewriteRule cvc5_proof_get_rewrite_rule(Cvc5Proof proof) +{ + Cvc5ProofRewriteRule res = CVC5_PROOF_REWRITE_RULE_LAST; + CVC5_CAPI_TRY_CATCH_BEGIN; + CVC5_CAPI_CHECK_PROOF(proof); + res = static_cast(proof->d_proof.getRewriteRule()); + CVC5_CAPI_TRY_CATCH_END; + return res; +} + +Cvc5Term cvc5_proof_get_result(Cvc5Proof proof) +{ + Cvc5Term res = nullptr; + CVC5_CAPI_TRY_CATCH_BEGIN; + CVC5_CAPI_CHECK_PROOF(proof); + res = proof->d_cvc5->d_tm->export_term(proof->d_proof.getResult()); + CVC5_CAPI_TRY_CATCH_END; + return res; +} + +const Cvc5Proof* cvc5_proof_get_children(Cvc5Proof proof, size_t* size) +{ + static thread_local std::vector res; + CVC5_CAPI_TRY_CATCH_BEGIN; + CVC5_CAPI_CHECK_PROOF(proof); + CVC5_CAPI_CHECK_NOT_NULL(size); + res.clear(); + auto children = proof->d_proof.getChildren(); + for (auto& p : children) + { + res.push_back(proof->d_cvc5->export_proof(p)); + } + *size = res.size(); + CVC5_CAPI_TRY_CATCH_END; + return res.data(); +} + +const Cvc5Term* cvc5_proof_get_arguments(Cvc5Proof proof, size_t* size) +{ + static thread_local std::vector res; + CVC5_CAPI_TRY_CATCH_BEGIN; + CVC5_CAPI_CHECK_PROOF(proof); + CVC5_CAPI_CHECK_NOT_NULL(size); + res.clear(); + auto args = proof->d_proof.getArguments(); + for (auto& t : args) + { + res.push_back(proof->d_cvc5->d_tm->export_term(t)); + } + *size = res.size(); + CVC5_CAPI_TRY_CATCH_END; + return res.data(); +} + +bool cvc5_proof_is_equal(Cvc5Proof a, Cvc5Proof b) +{ + bool res = false; + CVC5_CAPI_TRY_CATCH_BEGIN; + if (a == nullptr || b == nullptr) + { + res = a == b; + } + else + { + res = a->d_proof == b->d_proof; + } + CVC5_CAPI_TRY_CATCH_END; + return res; +} + +bool cvc5_proof_is_disequal(Cvc5Proof a, Cvc5Proof b) +{ + bool res = false; + CVC5_CAPI_TRY_CATCH_BEGIN; + if (a == nullptr || b == nullptr) + { + res = a != b; + } + else + { + res = a->d_proof != b->d_proof; + } + CVC5_CAPI_TRY_CATCH_END; + return res; +} + +size_t cvc5_proof_hash(Cvc5Proof proof) +{ + size_t res = 0; + CVC5_CAPI_TRY_CATCH_BEGIN; + CVC5_CAPI_CHECK_PROOF(proof); + res = std::hash{}(proof->d_proof); + CVC5_CAPI_TRY_CATCH_END; + return res; +} + /* -------------------------------------------------------------------------- */ /* Cvc5 */ /* -------------------------------------------------------------------------- */ @@ -4763,6 +4977,23 @@ const Cvc5Term* cvc5_get_unsat_core(Cvc5* cvc5, size_t* size) return res.data(); } +const Cvc5Term* cvc5_get_unsat_core_lemmas(Cvc5* cvc5, size_t* size) +{ + static thread_local std::vector res; + CVC5_CAPI_TRY_CATCH_BEGIN; + CVC5_CAPI_CHECK_NOT_NULL(cvc5); + CVC5_CAPI_CHECK_NOT_NULL(size); + res.clear(); + auto assertions = cvc5->d_solver.getUnsatCoreLemmas(); + for (auto& t : assertions) + { + res.push_back(cvc5->d_tm->export_term(t)); + } + *size = res.size(); + CVC5_CAPI_TRY_CATCH_END; + return res.data(); +} + void cvc5_get_difficulty(Cvc5* cvc5, size_t* size, Cvc5Term* inputs[], @@ -4840,6 +5071,24 @@ const Cvc5Term* cvc5_get_timeout_core_assuming(Cvc5* cvc5, return res.data(); } +const Cvc5Proof* cvc5_get_proof(Cvc5* cvc5, Cvc5ProofComponent c, size_t* size) +{ + static thread_local std::vector res; + CVC5_CAPI_TRY_CATCH_BEGIN; + CVC5_CAPI_CHECK_NOT_NULL(cvc5); + CVC5_CAPI_CHECK_NOT_NULL(size); + res.clear(); + auto proofs = + cvc5->d_solver.getProof(static_cast(c)); + for (const auto& p : proofs) + { + res.push_back(cvc5->export_proof(p)); + } + *size = proofs.size(); + CVC5_CAPI_TRY_CATCH_END; + return res.data(); +} + const Cvc5Term* cvc5_get_learned_literals(Cvc5* cvc5, Cvc5LearnedLitType type, size_t* size) @@ -4883,3 +5132,31 @@ void cvc5_reset_assertions(Cvc5* cvc5) cvc5->d_solver.resetAssertions(); CVC5_CAPI_TRY_CATCH_END; } + +const char* cvc5_proof_to_string(Cvc5* cvc5, + Cvc5Proof proof, + Cvc5ProofFormat format, + size_t size, + const Cvc5Term assertions[], + const char* names[]) +{ + static thread_local std::string str; + CVC5_CAPI_TRY_CATCH_BEGIN; + CVC5_CAPI_CHECK_NOT_NULL(cvc5); + CVC5_CAPI_CHECK_PROOF(proof); + CVC5_API_CHECK(assertions || names == nullptr) << "unexpected NULL argument"; + std::map cassertion_names; + if (assertions) + { + for (size_t i = 0; i < size; ++i) + { + cassertion_names.emplace(assertions[i]->d_term, names[i]); + } + } + str = proof->d_cvc5->d_solver.proofToString( + proof->d_proof, + static_cast(format), + cassertion_names); + CVC5_CAPI_TRY_CATCH_END; + return str.c_str(); +} diff --git a/src/api/c/cvc5_checks.h b/src/api/c/cvc5_checks.h index 593947e323a..8a40e9d5d2c 100644 --- a/src/api/c/cvc5_checks.h +++ b/src/api/c/cvc5_checks.h @@ -121,6 +121,14 @@ class Cvc5CApiAbortStream CVC5_API_CHECK((format) >= 0 && (format) < CVC5_PROOF_FORMAT_LAST) \ << "invalid proof format" +#define CVC5_CAPI_CHECK_PROOF_RULE(rule) \ + CVC5_API_CHECK((rule) >= 0 && (rule) < CVC5_PROOF_RULE_LAST) \ + << "invalid proof rule" + +#define CVC5_CAPI_CHECK_PROOF_REWRITE_RULE(rule) \ + CVC5_API_CHECK((rule) >= 0 && (rule) < CVC5_PROOF_REWRITE_RULE_LAST) \ + << "invalid proof rewrite rule" + /* -------------------------------------------------------------------------- */ #define CVC5_CAPI_CHECK_SORT(sort) \ @@ -173,5 +181,10 @@ class Cvc5CApiAbortStream #define CVC5_CAPI_CHECK_RESULT(res) \ CVC5_API_CHECK(res != nullptr) << "invalid result" +/* -------------------------------------------------------------------------- */ + +#define CVC5_CAPI_CHECK_PROOF(proof) \ + CVC5_API_CHECK(proof != nullptr) << "invalid proof" + /* -------------------------------------------------------------------------- */ } diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index df8cb0c128e..1826c4f34c2 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -8988,13 +8988,13 @@ size_t hash::operator()(const cvc5::Datatype& dt) const return std::hash()(*dt.d_dtype); } -size_t std::hash::operator()(const cvc5::Proof& p) const +size_t hash::operator()(const cvc5::Proof& proof) const { - if (p.isNull()) + if (proof.isNull()) { return 0; } - return cvc5::internal::ProofNodeHashFunction()(p.d_proofNode); + return std::hash{}(*proof.d_proofNode); } size_t hash::operator()(const cvc5::Grammar& grammar) const diff --git a/src/proof/proof_node.cpp b/src/proof/proof_node.cpp index 46bde646ff8..cc67c3a7972 100644 --- a/src/proof/proof_node.cpp +++ b/src/proof/proof_node.cpp @@ -145,5 +145,12 @@ size_t ProofNodeHashFunction::operator()(const ProofNode* pfn) const return static_cast(ret); } - } // namespace cvc5::internal + +namespace std { +size_t hash::operator()( + const cvc5::internal::ProofNode& node) const +{ + return cvc5::internal::ProofNodeHashFunction{}(&node); +} +} // namespace std diff --git a/src/proof/proof_node.h b/src/proof/proof_node.h index 4073921d0d2..1cd1812efc9 100644 --- a/src/proof/proof_node.h +++ b/src/proof/proof_node.h @@ -139,6 +139,17 @@ class ProofNode /** Was d_proven actually checked, or is it trusted? */ bool d_provenChecked; }; +} // namespace cvc5::internal + +namespace std { +template <> +struct hash +{ + size_t operator()(const cvc5::internal::ProofNode& node) const; +}; +} // namespace std + +namespace cvc5::internal { inline size_t ProofNodeHashFunction::operator()( std::shared_ptr pfn) const diff --git a/test/unit/api/c/CMakeLists.txt b/test/unit/api/c/CMakeLists.txt index 7f10cbf4b63..3e68186dddb 100644 --- a/test/unit/api/c/CMakeLists.txt +++ b/test/unit/api/c/CMakeLists.txt @@ -16,6 +16,8 @@ # Generate and add unit test. cvc5_add_unit_test_black(capi_kind_black api/c) cvc5_add_unit_test_black(capi_op_black api/c) +cvc5_add_unit_test_black(capi_proof_black api/c) +cvc5_add_unit_test_black(capi_proof_rule_black api/c) cvc5_add_unit_test_black(capi_solver_black api/c) cvc5_add_unit_test_black(capi_sort_black api/c) cvc5_add_unit_test_black(capi_sort_kind_black api/c) diff --git a/test/unit/api/c/capi_proof_black.cpp b/test/unit/api/c/capi_proof_black.cpp new file mode 100644 index 00000000000..4f33052fcf6 --- /dev/null +++ b/test/unit/api/c/capi_proof_black.cpp @@ -0,0 +1,210 @@ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2024 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Black box testing of proof-related functions of the C API. + */ + +extern "C" { +#include +} + +#include "base/check.h" +#include "base/output.h" +#include "gtest/gtest.h" + +namespace cvc5::internal::test { + +class TestCApiBlackProof : public ::testing::Test +{ + protected: + void SetUp() override + { + d_tm = cvc5_term_manager_new(); + d_solver = cvc5_new(d_tm); + d_bool = cvc5_get_boolean_sort(d_tm); + d_int = cvc5_get_integer_sort(d_tm); + d_real = cvc5_get_real_sort(d_tm); + d_str = cvc5_get_string_sort(d_tm); + d_uninterpreted = cvc5_mk_uninterpreted_sort(d_tm, "u"); + } + void TearDown() override + { + cvc5_delete(d_solver); + cvc5_term_manager_delete(d_tm); + } + + Cvc5Proof create_proof() + { + cvc5_set_option(d_solver, "produce-proofs", "true"); + std::vector domain = {d_uninterpreted}; + Cvc5Sort u_to_int = + cvc5_mk_fun_sort(d_tm, domain.size(), domain.data(), d_int); + domain = {d_int}; + Cvc5Sort int_pred = + cvc5_mk_fun_sort(d_tm, domain.size(), domain.data(), d_bool); + + Cvc5Term x = cvc5_mk_const(d_tm, d_uninterpreted, "x"); + Cvc5Term y = cvc5_mk_const(d_tm, d_uninterpreted, "y"); + Cvc5Term f = cvc5_mk_const(d_tm, u_to_int, "f"); + Cvc5Term p = cvc5_mk_const(d_tm, int_pred, "p"); + Cvc5Term zero = cvc5_mk_integer_int64(d_tm, 0); + Cvc5Term one = cvc5_mk_integer_int64(d_tm, 1); + std::vector args = {f, x}; + Cvc5Term f_x = + cvc5_mk_term(d_tm, CVC5_KIND_APPLY_UF, args.size(), args.data()); + args = {f, y}; + Cvc5Term f_y = + cvc5_mk_term(d_tm, CVC5_KIND_APPLY_UF, args.size(), args.data()); + args = {f_x, f_y}; + Cvc5Term sum = cvc5_mk_term(d_tm, CVC5_KIND_ADD, args.size(), args.data()); + args = {p, zero}; + Cvc5Term p_0 = + cvc5_mk_term(d_tm, CVC5_KIND_APPLY_UF, args.size(), args.data()); + args = {p, f_y}; + Cvc5Term p_f_y = + cvc5_mk_term(d_tm, CVC5_KIND_APPLY_UF, args.size(), args.data()); + + args = {zero, f_x}; + cvc5_assert_formula( + d_solver, cvc5_mk_term(d_tm, CVC5_KIND_GT, args.size(), args.data())); + args = {zero, f_y}; + cvc5_assert_formula( + d_solver, cvc5_mk_term(d_tm, CVC5_KIND_GT, args.size(), args.data())); + args = {sum, one}; + cvc5_assert_formula( + d_solver, cvc5_mk_term(d_tm, CVC5_KIND_GT, args.size(), args.data())); + cvc5_assert_formula(d_solver, p_0); + args = {p_f_y}; + cvc5_assert_formula( + d_solver, cvc5_mk_term(d_tm, CVC5_KIND_NOT, args.size(), args.data())); + Cvc5Result res = cvc5_check_sat(d_solver); + Assert(cvc5_result_is_unsat(res)); + size_t size; + const Cvc5Proof* proofs = + cvc5_get_proof(d_solver, CVC5_PROOF_COMPONENT_FULL, &size); + Assert(size == 1); + return proofs[0]; + } + + Cvc5Proof create_rewrite_proof() + { + cvc5_set_option(d_solver, "produce-proofs", "true"); + cvc5_set_option(d_solver, "proof-granularity", "dsl-rewrite"); + Cvc5Term x = cvc5_mk_const(d_tm, d_int, "x"); + std::vector args = {cvc5_mk_integer_int64(d_tm, 2), x}; + Cvc5Term twox = + cvc5_mk_term(d_tm, CVC5_KIND_MULT, args.size(), args.data()); + args = {x, x}; + Cvc5Term xplusx = + cvc5_mk_term(d_tm, CVC5_KIND_ADD, args.size(), args.data()); + args = {twox, xplusx}; + cvc5_assert_formula( + d_solver, + cvc5_mk_term(d_tm, CVC5_KIND_DISTINCT, args.size(), args.data())); + Cvc5Result res = cvc5_check_sat(d_solver); + Assert(cvc5_result_is_unsat(res)); + size_t size; + const Cvc5Proof* proofs = + cvc5_get_proof(d_solver, CVC5_PROOF_COMPONENT_FULL, &size); + Assert(size == 1); + return proofs[0]; + } + + Cvc5TermManager* d_tm; + Cvc5* d_solver; + Cvc5Sort d_bool; + Cvc5Sort d_int; + Cvc5Sort d_real; + Cvc5Sort d_str; + Cvc5Sort d_uninterpreted; +}; + +TEST_F(TestCApiBlackProof, get_rule) +{ + ASSERT_DEATH(cvc5_proof_get_rule(nullptr), "invalid proof"); + Cvc5Proof proof = create_proof(); + ASSERT_EQ(cvc5_proof_get_rule(proof), CVC5_PROOF_RULE_SCOPE); +} + +TEST_F(TestCApiBlackProof, get_rewrite_rule) +{ + ASSERT_DEATH(cvc5_proof_get_rewrite_rule(nullptr), "invalid proof"); + + Cvc5Proof proof = create_rewrite_proof(); + ASSERT_DEATH(cvc5_proof_get_rewrite_rule(proof), "to return `DSL_REWRITE`"); + Cvc5ProofRule rule; + std::vector stack = {proof}; + do + { + proof = stack.back(); + stack.pop_back(); + rule = cvc5_proof_get_rule(proof); + size_t size; + const Cvc5Proof* children = cvc5_proof_get_children(proof, &size); + for (size_t i = 0; i < size; ++i) + { + stack.push_back(children[i]); + } + } while (rule != CVC5_PROOF_RULE_DSL_REWRITE); + (void)cvc5_proof_get_rewrite_rule(proof); +} + +TEST_F(TestCApiBlackProof, get_result) +{ + ASSERT_DEATH(cvc5_proof_get_result(nullptr), "invalid proof"); + Cvc5Proof proof = create_proof(); + (void)cvc5_proof_get_result(proof); +} + +TEST_F(TestCApiBlackProof, get_children) +{ + Cvc5Proof proof = create_proof(); + size_t size; + (void)cvc5_proof_get_children(proof, &size); + ASSERT_TRUE(size > 0); + ASSERT_DEATH(cvc5_proof_get_children(nullptr, &size), "invalid proof"); + ASSERT_DEATH(cvc5_proof_get_children(proof, nullptr), + "unexpected NULL argument"); +} + +TEST_F(TestCApiBlackProof, get_arguments) +{ + Cvc5Proof proof = create_proof(); + size_t size; + (void)cvc5_proof_get_arguments(proof, &size); + ASSERT_DEATH(cvc5_proof_get_arguments(nullptr, &size), "invalid proof"); + ASSERT_DEATH(cvc5_proof_get_arguments(proof, nullptr), + "unexpected NULL argument"); +} + +TEST_F(TestCApiBlackProof, is_equal_disequal_hash) +{ + Cvc5Proof proof = create_proof(); + size_t size; + Cvc5Proof x = cvc5_proof_get_children(proof, &size)[0]; + Cvc5Proof y = cvc5_proof_get_children(x, &size)[0]; + + ASSERT_TRUE(cvc5_proof_is_equal(x, x)); + ASSERT_FALSE(cvc5_proof_is_disequal(x, x)); + ASSERT_FALSE(cvc5_proof_is_equal(x, y)); + ASSERT_TRUE(cvc5_proof_is_disequal(x, y)); + ASSERT_TRUE(cvc5_proof_is_equal(nullptr, nullptr)); + ASSERT_FALSE(cvc5_proof_is_equal(x, nullptr)); + ASSERT_FALSE(cvc5_proof_is_equal(nullptr, y)); + ASSERT_TRUE(cvc5_proof_is_disequal(x, nullptr)); + ASSERT_TRUE(cvc5_proof_is_disequal(nullptr, y)); + + ASSERT_EQ(cvc5_proof_hash(x), cvc5_proof_hash(x)); + ASSERT_NE(cvc5_proof_hash(x), cvc5_proof_hash(y)); + ASSERT_DEATH(cvc5_proof_hash(nullptr), "invalid proof"); +} +} // namespace cvc5::internal::test diff --git a/test/unit/api/c/capi_proof_rule_black.cpp b/test/unit/api/c/capi_proof_rule_black.cpp new file mode 100644 index 00000000000..04c3eca498c --- /dev/null +++ b/test/unit/api/c/capi_proof_rule_black.cpp @@ -0,0 +1,67 @@ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2024 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Black box testing of proof-rule-related functions of the C API. + */ + +extern "C" { +#include +} + +#include "base/output.h" +#include "gtest/gtest.h" + +namespace cvc5::internal::test { + +class TestCApiBlackProofRule : public ::testing::Test +{ +}; +class TestCApiProofRewriteRule : public ::testing::Test +{ +}; + +TEST_F(TestCApiBlackProofRule, proofRuleToString) +{ + for (int32_t r = static_cast(CVC5_PROOF_RULE_ASSUME); + r <= static_cast(CVC5_PROOF_RULE_UNKNOWN); + ++r) + { + Cvc5ProofRule rule = static_cast(r); + // If this assertion fails, the switch is missing rule r. + ASSERT_NE(cvc5_proof_rule_to_string(rule), std::string("?")); + } +} + +TEST_F(TestCApiBlackProofRule, hash) +{ + ASSERT_EQ(cvc5_proof_rule_hash(CVC5_PROOF_RULE_UNKNOWN), + static_cast(CVC5_PROOF_RULE_UNKNOWN)); +} + +TEST_F(TestCApiProofRewriteRule, ProofRewriteRuleToString) +{ + for (int32_t r = static_cast(CVC5_PROOF_REWRITE_RULE_NONE); + r <= static_cast(CVC5_PROOF_REWRITE_RULE_DISTINCT_BINARY_ELIM); + ++r) + { + // If this assertion fails, the switch is missing rule r. + Cvc5ProofRewriteRule rule = static_cast(r); + ASSERT_NE(cvc5_proof_rewrite_rule_to_string(rule), std::string("?")); + } +} + +TEST_F(TestCApiProofRewriteRule, hash) +{ + ASSERT_EQ(cvc5_proof_rewrite_rule_hash(CVC5_PROOF_REWRITE_RULE_NONE), + static_cast(CVC5_PROOF_REWRITE_RULE_NONE)); +} +} // namespace cvc5::internal::test diff --git a/test/unit/api/c/capi_solver_black.cpp b/test/unit/api/c/capi_solver_black.cpp index 83abe61cde9..e964d407dae 100644 --- a/test/unit/api/c/capi_solver_black.cpp +++ b/test/unit/api/c/capi_solver_black.cpp @@ -1320,6 +1320,145 @@ TEST_F(TestCApiBlackSolver, get_unsat_core2) ASSERT_DEATH(cvc5_get_unsat_core(d_solver, &size), "cannot get unsat core"); } +TEST_F(TestCApiBlackSolver, get_unsat_core_and_proof) +{ + cvc5_set_option(d_solver, "incremental", "true"); + cvc5_set_option(d_solver, "produce-unsat-cores", "true"); + cvc5_set_option(d_solver, "produce-proofs", "true"); + + std::vector domain = {d_uninterpreted}; + Cvc5Sort u_to_int = + cvc5_mk_fun_sort(d_tm, domain.size(), domain.data(), d_int); + domain = {d_int}; + Cvc5Sort int_pred = + cvc5_mk_fun_sort(d_tm, domain.size(), domain.data(), d_bool); + + Cvc5Term x = cvc5_mk_const(d_tm, d_uninterpreted, "x"); + Cvc5Term y = cvc5_mk_const(d_tm, d_uninterpreted, "y"); + Cvc5Term f = cvc5_mk_const(d_tm, u_to_int, "f"); + Cvc5Term p = cvc5_mk_const(d_tm, int_pred, "p"); + Cvc5Term zero = cvc5_mk_integer_int64(d_tm, 0); + Cvc5Term one = cvc5_mk_integer_int64(d_tm, 1); + std::vector args = {f, x}; + Cvc5Term f_x = + cvc5_mk_term(d_tm, CVC5_KIND_APPLY_UF, args.size(), args.data()); + args = {f, y}; + Cvc5Term f_y = + cvc5_mk_term(d_tm, CVC5_KIND_APPLY_UF, args.size(), args.data()); + args = {f_x, f_y}; + Cvc5Term sum = cvc5_mk_term(d_tm, CVC5_KIND_ADD, args.size(), args.data()); + args = {p, zero}; + Cvc5Term p_0 = + cvc5_mk_term(d_tm, CVC5_KIND_APPLY_UF, args.size(), args.data()); + args = {p, f_y}; + Cvc5Term p_f_y = + cvc5_mk_term(d_tm, CVC5_KIND_APPLY_UF, args.size(), args.data()); + + args = {zero, f_x}; + cvc5_assert_formula( + d_solver, cvc5_mk_term(d_tm, CVC5_KIND_GT, args.size(), args.data())); + args = {zero, f_y}; + cvc5_assert_formula( + d_solver, cvc5_mk_term(d_tm, CVC5_KIND_GT, args.size(), args.data())); + args = {sum, one}; + cvc5_assert_formula( + d_solver, cvc5_mk_term(d_tm, CVC5_KIND_GT, args.size(), args.data())); + cvc5_assert_formula(d_solver, p_0); + args = {p_f_y}; + cvc5_assert_formula( + d_solver, cvc5_mk_term(d_tm, CVC5_KIND_NOT, args.size(), args.data())); + ASSERT_TRUE(cvc5_result_is_unsat(cvc5_check_sat(d_solver))); + + size_t uc_size, proof_size; + const Cvc5Term* uc = cvc5_get_unsat_core(d_solver, &uc_size); + ASSERT_TRUE(uc_size > 0); + + (void)cvc5_get_proof(d_solver, CVC5_PROOF_COMPONENT_FULL, &proof_size); + (void)cvc5_get_proof(d_solver, CVC5_PROOF_COMPONENT_SAT, &proof_size); + + cvc5_reset_assertions(d_solver); + for (size_t i = 0; i < uc_size; ++i) + { + cvc5_assert_formula(d_solver, uc[i]); + } + Cvc5Result res = cvc5_check_sat(d_solver); + ASSERT_TRUE(cvc5_result_is_unsat(res)); + (void)cvc5_get_proof(d_solver, CVC5_PROOF_COMPONENT_FULL, &proof_size); +} + +TEST_F(TestCApiBlackSolver, get_unsat_core_lemmas1) +{ + cvc5_set_option(d_solver, "produce-unsat-cores", "true"); + cvc5_set_option(d_solver, "unsat-cores-mode", "sat-proof"); + + size_t size; + // cannot ask before a check sat + ASSERT_DEATH(cvc5_get_unsat_core_lemmas(d_solver, &size), + "cannot get unsat core"); + + cvc5_assert_formula(d_solver, cvc5_mk_false(d_tm)); + ASSERT_TRUE(cvc5_result_is_unsat(cvc5_check_sat(d_solver))); + (void)cvc5_get_unsat_core_lemmas(d_solver, &size); + + ASSERT_DEATH(cvc5_get_unsat_core_lemmas(nullptr, &size), + "unexpected NULL argument"); + ASSERT_DEATH(cvc5_get_unsat_core_lemmas(d_solver, nullptr), + "unexpected NULL argument"); +} + +TEST_F(TestCApiBlackSolver, get_unsat_core_lemmas2) +{ + cvc5_set_option(d_solver, "incremental", "true"); + cvc5_set_option(d_solver, "produce-unsat-cores", "true"); + cvc5_set_option(d_solver, "produce-proofs", "true"); + + std::vector domain = {d_uninterpreted}; + Cvc5Sort u_to_int = + cvc5_mk_fun_sort(d_tm, domain.size(), domain.data(), d_int); + domain = {d_int}; + Cvc5Sort int_pred = + cvc5_mk_fun_sort(d_tm, domain.size(), domain.data(), d_bool); + + Cvc5Term x = cvc5_mk_const(d_tm, d_uninterpreted, "x"); + Cvc5Term y = cvc5_mk_const(d_tm, d_uninterpreted, "y"); + Cvc5Term f = cvc5_mk_const(d_tm, u_to_int, "f"); + Cvc5Term p = cvc5_mk_const(d_tm, int_pred, "p"); + Cvc5Term zero = cvc5_mk_integer_int64(d_tm, 0); + Cvc5Term one = cvc5_mk_integer_int64(d_tm, 1); + std::vector args = {f, x}; + Cvc5Term f_x = + cvc5_mk_term(d_tm, CVC5_KIND_APPLY_UF, args.size(), args.data()); + args = {f, y}; + Cvc5Term f_y = + cvc5_mk_term(d_tm, CVC5_KIND_APPLY_UF, args.size(), args.data()); + args = {f_x, f_y}; + Cvc5Term sum = cvc5_mk_term(d_tm, CVC5_KIND_ADD, args.size(), args.data()); + args = {p, zero}; + Cvc5Term p_0 = + cvc5_mk_term(d_tm, CVC5_KIND_APPLY_UF, args.size(), args.data()); + args = {p, f_y}; + Cvc5Term p_f_y = + cvc5_mk_term(d_tm, CVC5_KIND_APPLY_UF, args.size(), args.data()); + + args = {zero, f_x}; + cvc5_assert_formula( + d_solver, cvc5_mk_term(d_tm, CVC5_KIND_GT, args.size(), args.data())); + args = {zero, f_y}; + cvc5_assert_formula( + d_solver, cvc5_mk_term(d_tm, CVC5_KIND_GT, args.size(), args.data())); + args = {sum, one}; + cvc5_assert_formula( + d_solver, cvc5_mk_term(d_tm, CVC5_KIND_GT, args.size(), args.data())); + cvc5_assert_formula(d_solver, p_0); + args = {p_f_y}; + cvc5_assert_formula( + d_solver, cvc5_mk_term(d_tm, CVC5_KIND_NOT, args.size(), args.data())); + ASSERT_TRUE(cvc5_result_is_unsat(cvc5_check_sat(d_solver))); + + size_t size; + (void)cvc5_get_unsat_core_lemmas(d_solver, &size); +} + TEST_F(TestCApiBlackSolver, get_difficulty) { cvc5_set_option(d_solver, "produce-difficulty", "true"); @@ -1451,6 +1590,75 @@ TEST_F(TestCApiBlackSolver, get_timeout_core_assuming_empty) "unexpected NULL argument"); } +TEST_F(TestCApiBlackSolver, get_proof_and_proof_to_string) +{ + cvc5_set_option(d_solver, "produce-proofs", "true"); + + std::vector domain = {d_uninterpreted}; + Cvc5Sort u_to_int = + cvc5_mk_fun_sort(d_tm, domain.size(), domain.data(), d_int); + domain = {d_int}; + Cvc5Sort int_pred = + cvc5_mk_fun_sort(d_tm, domain.size(), domain.data(), d_bool); + + Cvc5Term x = cvc5_mk_const(d_tm, d_uninterpreted, "x"); + Cvc5Term y = cvc5_mk_const(d_tm, d_uninterpreted, "y"); + Cvc5Term f = cvc5_mk_const(d_tm, u_to_int, "f"); + Cvc5Term p = cvc5_mk_const(d_tm, int_pred, "p"); + Cvc5Term zero = cvc5_mk_integer_int64(d_tm, 0); + Cvc5Term one = cvc5_mk_integer_int64(d_tm, 1); + std::vector args = {f, x}; + Cvc5Term f_x = + cvc5_mk_term(d_tm, CVC5_KIND_APPLY_UF, args.size(), args.data()); + args = {f, y}; + Cvc5Term f_y = + cvc5_mk_term(d_tm, CVC5_KIND_APPLY_UF, args.size(), args.data()); + args = {f_x, f_y}; + Cvc5Term sum = cvc5_mk_term(d_tm, CVC5_KIND_ADD, args.size(), args.data()); + args = {p, zero}; + Cvc5Term p_0 = + cvc5_mk_term(d_tm, CVC5_KIND_APPLY_UF, args.size(), args.data()); + args = {p, f_y}; + Cvc5Term p_f_y = + cvc5_mk_term(d_tm, CVC5_KIND_APPLY_UF, args.size(), args.data()); + + args = {zero, f_x}; + cvc5_assert_formula( + d_solver, cvc5_mk_term(d_tm, CVC5_KIND_GT, args.size(), args.data())); + args = {zero, f_y}; + cvc5_assert_formula( + d_solver, cvc5_mk_term(d_tm, CVC5_KIND_GT, args.size(), args.data())); + args = {sum, one}; + cvc5_assert_formula( + d_solver, cvc5_mk_term(d_tm, CVC5_KIND_GT, args.size(), args.data())); + cvc5_assert_formula(d_solver, p_0); + args = {p_f_y}; + cvc5_assert_formula( + d_solver, cvc5_mk_term(d_tm, CVC5_KIND_NOT, args.size(), args.data())); + ASSERT_TRUE(cvc5_result_is_unsat(cvc5_check_sat(d_solver))); + + size_t size; + ASSERT_DEATH(cvc5_get_proof(nullptr, CVC5_PROOF_COMPONENT_FULL, &size), + "unexpected NULL"); + ASSERT_DEATH(cvc5_get_proof(d_solver, CVC5_PROOF_COMPONENT_FULL, nullptr), + "unexpected NULL"); + + const Cvc5Proof* proofs = + cvc5_get_proof(d_solver, CVC5_PROOF_COMPONENT_FULL, &size); + ASSERT_TRUE(size > 0); + + std::string proof_str = cvc5_proof_to_string( + d_solver, proofs[0], CVC5_PROOF_FORMAT_DEFAULT, 0, nullptr, nullptr); + ASSERT_FALSE(proof_str.empty()); + proof_str = cvc5_proof_to_string( + d_solver, proofs[0], CVC5_PROOF_FORMAT_ALETHE, 0, nullptr, nullptr); + ASSERT_FALSE(proof_str.empty()); + proofs = cvc5_get_proof(d_solver, CVC5_PROOF_COMPONENT_SAT, &size); + proof_str = cvc5_proof_to_string( + d_solver, proofs[0], CVC5_PROOF_FORMAT_NONE, 0, nullptr, nullptr); + ASSERT_FALSE(proof_str.empty()); +} + TEST_F(TestCApiBlackSolver, get_learned_literals) { cvc5_set_option(d_solver, "produce-learned-literals", "true"); diff --git a/test/unit/api/cpp/CMakeLists.txt b/test/unit/api/cpp/CMakeLists.txt index 527bf19e083..72873e6e36f 100644 --- a/test/unit/api/cpp/CMakeLists.txt +++ b/test/unit/api/cpp/CMakeLists.txt @@ -15,6 +15,7 @@ cvc5_add_unit_test_black(api_kind_black api/cpp) cvc5_add_unit_test_black(api_op_black api/cpp) cvc5_add_unit_test_white(api_op_white api/cpp) +cvc5_add_unit_test_black(api_proof_black api/cpp) cvc5_add_unit_test_black(api_proof_rule_black api/cpp) cvc5_add_unit_test_black(api_skolem_id_black api/cpp) cvc5_add_unit_test_black(api_solver_black api/cpp) @@ -29,7 +30,6 @@ cvc5_add_unit_test_black(datatype_api_black api/cpp) cvc5_add_unit_test_black(grammar_black api/cpp) cvc5_add_unit_test_black(input_parser_black api/cpp) cvc5_add_unit_test_black(parametric_datatype_black api/cpp) -cvc5_add_unit_test_black(proof_black api/cpp) cvc5_add_unit_test_black(result_black api/cpp) cvc5_add_unit_test_black(symbol_manager_black api/cpp) cvc5_add_unit_test_black(synth_result_black api/cpp) diff --git a/test/unit/api/cpp/proof_black.cpp b/test/unit/api/cpp/api_proof_black.cpp similarity index 98% rename from test/unit/api/cpp/proof_black.cpp rename to test/unit/api/cpp/api_proof_black.cpp index b2025544716..5a0a6f2fcbd 100644 --- a/test/unit/api/cpp/proof_black.cpp +++ b/test/unit/api/cpp/api_proof_black.cpp @@ -140,6 +140,7 @@ TEST_F(TestApiBlackProof, equalhash) ASSERT_TRUE(std::hash()(x) == std::hash()(x)); (void)std::hash{}(Proof()); + ASSERT_FALSE(std::hash()(x) == std::hash()(y)); } } // namespace test diff --git a/test/unit/api/cpp/api_proof_rule_black.cpp b/test/unit/api/cpp/api_proof_rule_black.cpp index 8b1603c029e..7e0b3ae1863 100644 --- a/test/unit/api/cpp/api_proof_rule_black.cpp +++ b/test/unit/api/cpp/api_proof_rule_black.cpp @@ -24,11 +24,11 @@ namespace cvc5::internal { namespace test { -class TestApiProofRule : public ::testing::Test +class TestApiBlackProofRule : public ::testing::Test { }; -TEST_F(TestApiProofRule, proofRuleToString) +TEST_F(TestApiBlackProofRule, proofRuleToString) { for (int32_t r = static_cast(ProofRule::ASSUME); r <= static_cast(ProofRule::UNKNOWN); @@ -44,7 +44,7 @@ TEST_F(TestApiProofRule, proofRuleToString) } } -TEST_F(TestApiProofRule, ProofRuleHash) +TEST_F(TestApiBlackProofRule, ProofRuleHash) { ASSERT_EQ(std::hash()(ProofRule::UNKNOWN), static_cast(ProofRule::UNKNOWN)); diff --git a/test/unit/api/cpp/api_solver_black.cpp b/test/unit/api/cpp/api_solver_black.cpp index ab6f38ec566..7f3cbbead4b 100644 --- a/test/unit/api/cpp/api_solver_black.cpp +++ b/test/unit/api/cpp/api_solver_black.cpp @@ -915,7 +915,6 @@ TEST_F(TestApiBlackSolver, getUnsatCoreLemmas1) ASSERT_THROW(d_solver->getUnsatCoreLemmas(), CVC5ApiException); d_solver->assertFormula(d_tm.mkFalse()); - d_solver->checkSat(); ASSERT_TRUE(d_solver->checkSat().isUnsat()); ASSERT_NO_THROW(d_solver->getUnsatCoreLemmas()); } @@ -1275,6 +1274,7 @@ TEST_F(TestApiBlackSolver, getProofAndProofToString) ASSERT_FALSE(printedProof.empty()); ASSERT_NO_THROW(printedProof = d_solver->proofToString( proofs[0], modes::ProofFormat::ALETHE)); + ASSERT_FALSE(printedProof.empty()); ASSERT_NO_THROW(proofs = d_solver->getProof(modes::ProofComponent::SAT)); ASSERT_NO_THROW(printedProof = d_solver->proofToString( proofs[0], modes::ProofFormat::NONE));