mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

track assumptions when parsing into a solver. This enables solver.from_file/solver.from_string to support assumptions/cores #6587

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-02-14 11:09:11 -08:00
parent 3dc91de531
commit 9ce5fe707d
4 changed files with 17 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/api/api_parsers.cpp
View file

@ -128,7 +128,8 @@ extern "C" {
static Z3_ast_vector Z3_parser_context_parse_stream(Z3_context c, scoped_ptr<cmd_context>& ctx, bool owned, std::istream& is) { static Z3_ast_vector Z3_parser_context_parse_stream(Z3_context c, scoped_ptr<cmd_context>& ctx, bool owned, std::istream& is) {
Z3_TRY; Z3_TRY;
Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m()); ast_manager& m = mk_c(c)->m();
Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), m);
mk_c(c)->save_object(v); mk_c(c)->save_object(v);
std::stringstream errstrm; std::stringstream errstrm;
ctx->set_regular_stream(errstrm); ctx->set_regular_stream(errstrm);
@ -147,8 +148,11 @@ extern "C" {
SET_ERROR_CODE(Z3_PARSER_ERROR, errstrm.str()); SET_ERROR_CODE(Z3_PARSER_ERROR, errstrm.str());
return of_ast_vector(v); return of_ast_vector(v);
} }
for (expr* e : ctx->tracked_assertions()) for (auto const& [asr, an] : ctx->tracked_assertions())
v->m_ast_vector.push_back(e); if (an)
v->m_ast_vector.push_back(m.mk_implies(an, asr));
else
v->m_ast_vector.push_back(asr);
ctx->reset_tracked_assertions(); ctx->reset_tracked_assertions();
return of_ast_vector(v); return of_ast_vector(v);
Z3_CATCH_RETURN(nullptr); Z3_CATCH_RETURN(nullptr);

7
src/api/api_solver.cpp
View file

@ -314,8 +314,11 @@ extern "C" {
bool initialized = to_solver(s)->m_solver.get() != nullptr; bool initialized = to_solver(s)->m_solver.get() != nullptr;
if (!initialized) if (!initialized)
init_solver(c, s); init_solver(c, s);
for (expr* e : ctx->tracked_assertions()) for (auto const& [asr, an] : ctx->tracked_assertions())
to_solver(s)->assert_expr(e); if (an)
to_solver(s)->assert_expr(asr, an);
else
to_solver(s)->assert_expr(asr);
ctx->reset_tracked_assertions(); ctx->reset_tracked_assertions();
to_solver_ref(s)->set_model_converter(ctx->get_model_converter()); to_solver_ref(s)->set_model_converter(ctx->get_model_converter());
auto* ctx_s = ctx->get_solver(); auto* ctx_s = ctx->get_solver();

11
src/cmd_context/cmd_context.cpp
View file

@ -2201,21 +2201,18 @@ void cmd_context::display_statistics(bool show_total_time, double total_time) {
} }
expr_ref_vector cmd_context::tracked_assertions() { vector<std::pair<expr*,expr*>> cmd_context::tracked_assertions() {
expr_ref_vector result(m()); vector<std::pair<expr*,expr*>> result;
if (assertion_names().size() == assertions().size()) { if (assertion_names().size() == assertions().size()) {
for (unsigned i = 0; i < assertions().size(); ++i) { for (unsigned i = 0; i < assertions().size(); ++i) {
expr* an = assertion_names()[i]; expr* an = assertion_names()[i];
expr* asr = assertions()[i]; expr* asr = assertions()[i];
if (an) result.push_back({ asr, an });
result.push_back(m().mk_implies(an, asr));
else
result.push_back(asr);
} }
} }
else { else {
for (expr * e : assertions()) for (expr * e : assertions())
result.push_back(e); result.push_back({ e, nullptr});
} }
return result; return result;
} }

2
src/cmd_context/cmd_context.h
View file

@ -523,7 +523,7 @@ public:
ptr_vector<expr> const& assertions() const { return m_assertions; } ptr_vector<expr> const& assertions() const { return m_assertions; }
ptr_vector<expr> const& assertion_names() const { return m_assertion_names; } ptr_vector<expr> const& assertion_names() const { return m_assertion_names; }
expr_ref_vector tracked_assertions(); vector<std::pair<expr*,expr*>> tracked_assertions();
void reset_tracked_assertions(); void reset_tracked_assertions();
/** /**