From 5796e150886e7479c5e35261cd4cda12b0593af9 Mon Sep 17 00:00:00 2001 From: Doug Woos Date: Fri, 27 Jan 2017 11:06:14 -0800 Subject: [PATCH 1/3] Thread labels through tactic system --- src/cmd_context/tactic_cmds.cpp | 21 ++++++++++++-- src/smt/tactic/smt_tactic.cpp | 8 ++++-- src/solver/tactic2solver.cpp | 3 +- src/tactic/filter_model_converter.cpp | 3 ++ src/tactic/filter_model_converter.h | 2 ++ src/tactic/model_converter.cpp | 40 ++++++++++++++++++++++++++- src/tactic/model_converter.h | 4 +++ src/tactic/tactic.cpp | 8 ++++-- src/tactic/tactic.h | 2 +- 9 files changed, 82 insertions(+), 9 deletions(-) diff --git a/src/cmd_context/tactic_cmds.cpp b/src/cmd_context/tactic_cmds.cpp index 86900e175..158f361dd 100644 --- a/src/cmd_context/tactic_cmds.cpp +++ b/src/cmd_context/tactic_cmds.cpp @@ -165,7 +165,23 @@ public: } }; -typedef simple_check_sat_result check_sat_tactic_result; +struct check_sat_tactic_result : public simple_check_sat_result { +public: + svector labels; + + check_sat_tactic_result(ast_manager & m) : simple_check_sat_result(m) { + } + + virtual void get_labels(svector & r) { + r.append(labels); + } + + virtual void add_labels(svector & r) { + labels.append(r); + } +}; + +typedef svector & labels_ref; class check_sat_using_tactict_cmd : public exec_given_tactic_cmd { public: @@ -189,6 +205,7 @@ public: ast_manager & m = ctx.m(); unsigned timeout = p.get_uint("timeout", ctx.params().m_timeout); unsigned rlimit = p.get_uint("rlimit", ctx.params().m_rlimit); + svector labels; goal_ref g = alloc(goal, m, ctx.produce_proofs(), ctx.produce_models(), ctx.produce_unsat_cores()); assert_exprs_from(ctx, *g); TRACE("check_sat_using", g->display(tout);); @@ -208,7 +225,7 @@ public: cmd_context::scoped_watch sw(ctx); lbool r = l_undef; try { - r = check_sat(t, g, md, pr, core, reason_unknown); + r = check_sat(t, g, md, result->labels, pr, core, reason_unknown); ctx.display_sat_result(r); result->set_status(r); if (r == l_undef) { diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp index f2fbcf6d9..d9e6da303 100644 --- a/src/smt/tactic/smt_tactic.cpp +++ b/src/smt/tactic/smt_tactic.cpp @@ -256,7 +256,9 @@ public: if (in->models_enabled()) { model_ref md; m_ctx->get_model(md); - mc = model2model_converter(md.get()); + buffer r; + m_ctx->get_relevant_labels(0, r); + mc = model_and_labels2model_converter(md.get(), r); mc = concat(fmc.get(), mc.get()); } pc = 0; @@ -308,7 +310,9 @@ public: if (in->models_enabled()) { model_ref md; m_ctx->get_model(md); - mc = model2model_converter(md.get()); + buffer r; + m_ctx->get_relevant_labels(0, r); + mc = model_and_labels2model_converter(md.get(), r); } pc = 0; core = 0; diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp index f53301948..586d59d4f 100644 --- a/src/solver/tactic2solver.cpp +++ b/src/solver/tactic2solver.cpp @@ -144,8 +144,9 @@ lbool tactic2solver::check_sat_core(unsigned num_assumptions, expr * const * ass proof_ref pr(m); expr_dependency_ref core(m); std::string reason_unknown = "unknown"; + svector labels; try { - switch (::check_sat(*m_tactic, g, md, pr, core, reason_unknown)) { + switch (::check_sat(*m_tactic, g, md, labels, pr, core, reason_unknown)) { case l_true: m_result->set_status(l_true); break; diff --git a/src/tactic/filter_model_converter.cpp b/src/tactic/filter_model_converter.cpp index ba6ee4f0d..247f2e91d 100644 --- a/src/tactic/filter_model_converter.cpp +++ b/src/tactic/filter_model_converter.cpp @@ -51,6 +51,9 @@ void filter_model_converter::operator()(model_ref & old_model, unsigned goal_idx TRACE("filter_mc", tout << "after filter_model_converter\n"; model_v2_pp(tout, *old_model);); } +void filter_model_converter::operator()(svector & labels, unsigned goal_idx) { +} + void filter_model_converter::display(std::ostream & out) { out << "(filter-model-converter"; for (unsigned i = 0; i < m_decls.size(); i++) { diff --git a/src/tactic/filter_model_converter.h b/src/tactic/filter_model_converter.h index 6fc8fdd77..0b67a6c5a 100644 --- a/src/tactic/filter_model_converter.h +++ b/src/tactic/filter_model_converter.h @@ -32,6 +32,8 @@ public: virtual void operator()(model_ref & md, unsigned goal_idx); + virtual void operator()(svector & labels, unsigned goal_idx); + virtual void operator()(model_ref & md) { operator()(md, 0); } // TODO: delete virtual void cancel() {} diff --git a/src/tactic/model_converter.cpp b/src/tactic/model_converter.cpp index 7ac3e898a..061d12afa 100644 --- a/src/tactic/model_converter.cpp +++ b/src/tactic/model_converter.cpp @@ -33,6 +33,12 @@ public: this->m_c1->operator()(m, 0); } + virtual void operator()(svector & r, unsigned goal_idx) { + this->m_c2->operator()(r, goal_idx); + this->m_c1->operator()(r, 0); + } + + virtual char const * get_name() const { return "concat-model-converter"; } virtual model_converter * translate(ast_translation & translator) { @@ -76,6 +82,24 @@ public: } UNREACHABLE(); } + + virtual void operator()(svector & r, unsigned goal_idx) { + unsigned num = this->m_c2s.size(); + for (unsigned i = 0; i < num; i++) { + if (goal_idx < this->m_szs[i]) { + // found the model converter that should be used + model_converter * c2 = this->m_c2s[i]; + if (c2) + c2->operator()(r, goal_idx); + if (m_c1) + this->m_c1->operator()(r, i); + return; + } + // invalid goal + goal_idx -= this->m_szs[i]; + } + UNREACHABLE(); + } virtual char const * get_name() const { return "concat-star-model-converter"; } @@ -102,8 +126,12 @@ model_converter * concat(model_converter * mc1, unsigned num, model_converter * class model2mc : public model_converter { model_ref m_model; + buffer m_labels; public: model2mc(model * m):m_model(m) {} + + model2mc(model * m, buffer r):m_model(m), m_labels(r) {} + virtual ~model2mc() {} virtual void operator()(model_ref & m) { @@ -114,7 +142,11 @@ public: m = m_model; } - virtual void cancel() { + virtual void operator()(svector & r, unsigned goal_idx) { + r.append(m_labels.size(), m_labels.c_ptr()); + } + + virtual void cancel() { } virtual void display(std::ostream & out) { @@ -135,6 +167,12 @@ model_converter * model2model_converter(model * m) { return alloc(model2mc, m); } +model_converter * model_and_labels2model_converter(model * m, buffer & r) { + if (m == 0) + return 0; + return alloc(model2mc, m, r); +} + void model_converter2model(ast_manager & mng, model_converter * mc, model_ref & m) { if (mc) { m = alloc(model, mng); diff --git a/src/tactic/model_converter.h b/src/tactic/model_converter.h index 00c50a15f..4395fc546 100644 --- a/src/tactic/model_converter.h +++ b/src/tactic/model_converter.h @@ -32,6 +32,8 @@ public: SASSERT(goal_idx == 0); operator()(m); } + + virtual void operator()(svector & r, unsigned goal_idx) {} virtual model_converter * translate(ast_translation & translator) = 0; }; @@ -49,6 +51,8 @@ model_converter * concat(model_converter * mc1, unsigned num, model_converter * model_converter * model2model_converter(model * m); +model_converter * model_and_labels2model_converter(model * m, buffer &r); + void model_converter2model(ast_manager & mng, model_converter * mc, model_ref & m); void apply(model_converter_ref & mc, model_ref & m, unsigned gidx); diff --git a/src/tactic/tactic.cpp b/src/tactic/tactic.cpp index 92e916d80..6eec018c7 100644 --- a/src/tactic/tactic.cpp +++ b/src/tactic/tactic.cpp @@ -174,7 +174,7 @@ void exec(tactic & t, goal_ref const & in, goal_ref_buffer & result, model_conve } } -lbool check_sat(tactic & t, goal_ref & g, model_ref & md, proof_ref & pr, expr_dependency_ref & core, std::string & reason_unknown) { +lbool check_sat(tactic & t, goal_ref & g, model_ref & md, svector & labels, proof_ref & pr, expr_dependency_ref & core, std::string & reason_unknown) { bool models_enabled = g->models_enabled(); bool proofs_enabled = g->proofs_enabled(); bool cores_enabled = g->unsat_core_enabled(); @@ -199,6 +199,7 @@ lbool check_sat(tactic & t, goal_ref & g, model_ref & md, proof_ref & pr, expr_d if (is_decided_sat(r)) { if (models_enabled) { + (*mc)(labels, 0); model_converter2model(m, mc.get(), md); if (!md) { // create empty model. @@ -215,7 +216,10 @@ lbool check_sat(tactic & t, goal_ref & g, model_ref & md, proof_ref & pr, expr_d return l_false; } else { - if (models_enabled) model_converter2model(m, mc.get(), md); + if (models_enabled) { + model_converter2model(m, mc.get(), md); + (*mc)(labels, 0); + } reason_unknown = "incomplete"; return l_undef; } diff --git a/src/tactic/tactic.h b/src/tactic/tactic.h index a9e50ff10..7c65c83e5 100644 --- a/src/tactic/tactic.h +++ b/src/tactic/tactic.h @@ -153,7 +153,7 @@ public: #define MK_SIMPLE_TACTIC_FACTORY(NAME, ST) MK_TACTIC_FACTORY(NAME, return ST;) void exec(tactic & t, goal_ref const & in, goal_ref_buffer & result, model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core); -lbool check_sat(tactic & t, goal_ref & g, model_ref & md, proof_ref & pr, expr_dependency_ref & core, std::string & reason_unknown); +lbool check_sat(tactic & t, goal_ref & g, model_ref & md, svector & labels, proof_ref & pr, expr_dependency_ref & core, std::string & reason_unknown); // Throws an exception if goal \c in requires proof generation. void fail_if_proof_generation(char const * tactic_name, goal_ref const & in); From 379181092032b105c35d2b0576233633d212e97e Mon Sep 17 00:00:00 2001 From: Doug Woos Date: Mon, 30 Jan 2017 15:09:57 -0800 Subject: [PATCH 2/3] add const & --- src/tactic/model_converter.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/tactic/model_converter.cpp b/src/tactic/model_converter.cpp index 061d12afa..efe80f226 100644 --- a/src/tactic/model_converter.cpp +++ b/src/tactic/model_converter.cpp @@ -130,7 +130,7 @@ class model2mc : public model_converter { public: model2mc(model * m):m_model(m) {} - model2mc(model * m, buffer r):m_model(m), m_labels(r) {} + model2mc(model * m, buffer const & r):m_model(m), m_labels(r) {} virtual ~model2mc() {} From 8196173e293032fb298ebd9b8e25907725a7201e Mon Sep 17 00:00:00 2001 From: Doug Woos Date: Mon, 30 Jan 2017 15:50:34 -0800 Subject: [PATCH 3/3] Introduce and use labels_vec --- src/cmd_context/tactic_cmds.cpp | 6 ++---- src/solver/tactic2solver.cpp | 2 +- src/tactic/model_converter.cpp | 6 +++--- src/tactic/model_converter.h | 4 +++- src/tactic/tactic.cpp | 2 +- src/tactic/tactic.h | 2 +- 6 files changed, 11 insertions(+), 11 deletions(-) diff --git a/src/cmd_context/tactic_cmds.cpp b/src/cmd_context/tactic_cmds.cpp index 158f361dd..4febb1597 100644 --- a/src/cmd_context/tactic_cmds.cpp +++ b/src/cmd_context/tactic_cmds.cpp @@ -167,7 +167,7 @@ public: struct check_sat_tactic_result : public simple_check_sat_result { public: - svector labels; + labels_vec labels; check_sat_tactic_result(ast_manager & m) : simple_check_sat_result(m) { } @@ -181,8 +181,6 @@ public: } }; -typedef svector & labels_ref; - class check_sat_using_tactict_cmd : public exec_given_tactic_cmd { public: check_sat_using_tactict_cmd(): @@ -205,7 +203,7 @@ public: ast_manager & m = ctx.m(); unsigned timeout = p.get_uint("timeout", ctx.params().m_timeout); unsigned rlimit = p.get_uint("rlimit", ctx.params().m_rlimit); - svector labels; + labels_vec labels; goal_ref g = alloc(goal, m, ctx.produce_proofs(), ctx.produce_models(), ctx.produce_unsat_cores()); assert_exprs_from(ctx, *g); TRACE("check_sat_using", g->display(tout);); diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp index 586d59d4f..6b1a7916f 100644 --- a/src/solver/tactic2solver.cpp +++ b/src/solver/tactic2solver.cpp @@ -144,7 +144,7 @@ lbool tactic2solver::check_sat_core(unsigned num_assumptions, expr * const * ass proof_ref pr(m); expr_dependency_ref core(m); std::string reason_unknown = "unknown"; - svector labels; + labels_vec labels; try { switch (::check_sat(*m_tactic, g, md, labels, pr, core, reason_unknown)) { case l_true: diff --git a/src/tactic/model_converter.cpp b/src/tactic/model_converter.cpp index efe80f226..6f6dd3da1 100644 --- a/src/tactic/model_converter.cpp +++ b/src/tactic/model_converter.cpp @@ -33,7 +33,7 @@ public: this->m_c1->operator()(m, 0); } - virtual void operator()(svector & r, unsigned goal_idx) { + virtual void operator()(labels_vec & r, unsigned goal_idx) { this->m_c2->operator()(r, goal_idx); this->m_c1->operator()(r, 0); } @@ -83,7 +83,7 @@ public: UNREACHABLE(); } - virtual void operator()(svector & r, unsigned goal_idx) { + virtual void operator()(labels_vec & r, unsigned goal_idx) { unsigned num = this->m_c2s.size(); for (unsigned i = 0; i < num; i++) { if (goal_idx < this->m_szs[i]) { @@ -142,7 +142,7 @@ public: m = m_model; } - virtual void operator()(svector & r, unsigned goal_idx) { + virtual void operator()(labels_vec & r, unsigned goal_idx) { r.append(m_labels.size(), m_labels.c_ptr()); } diff --git a/src/tactic/model_converter.h b/src/tactic/model_converter.h index 4395fc546..e2bc3cf83 100644 --- a/src/tactic/model_converter.h +++ b/src/tactic/model_converter.h @@ -23,6 +23,8 @@ Notes: #include"converter.h" #include"ref.h" +class labels_vec : public svector {}; + class model_converter : public converter { public: virtual void operator()(model_ref & m) {} // TODO: delete @@ -33,7 +35,7 @@ public: operator()(m); } - virtual void operator()(svector & r, unsigned goal_idx) {} + virtual void operator()(labels_vec & r, unsigned goal_idx) {} virtual model_converter * translate(ast_translation & translator) = 0; }; diff --git a/src/tactic/tactic.cpp b/src/tactic/tactic.cpp index 6eec018c7..0a95e8f65 100644 --- a/src/tactic/tactic.cpp +++ b/src/tactic/tactic.cpp @@ -174,7 +174,7 @@ void exec(tactic & t, goal_ref const & in, goal_ref_buffer & result, model_conve } } -lbool check_sat(tactic & t, goal_ref & g, model_ref & md, svector & labels, proof_ref & pr, expr_dependency_ref & core, std::string & reason_unknown) { +lbool check_sat(tactic & t, goal_ref & g, model_ref & md, labels_vec & labels, proof_ref & pr, expr_dependency_ref & core, std::string & reason_unknown) { bool models_enabled = g->models_enabled(); bool proofs_enabled = g->proofs_enabled(); bool cores_enabled = g->unsat_core_enabled(); diff --git a/src/tactic/tactic.h b/src/tactic/tactic.h index 7c65c83e5..645b53681 100644 --- a/src/tactic/tactic.h +++ b/src/tactic/tactic.h @@ -153,7 +153,7 @@ public: #define MK_SIMPLE_TACTIC_FACTORY(NAME, ST) MK_TACTIC_FACTORY(NAME, return ST;) void exec(tactic & t, goal_ref const & in, goal_ref_buffer & result, model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core); -lbool check_sat(tactic & t, goal_ref & g, model_ref & md, svector & labels, proof_ref & pr, expr_dependency_ref & core, std::string & reason_unknown); +lbool check_sat(tactic & t, goal_ref & g, model_ref & md, labels_vec & labels, proof_ref & pr, expr_dependency_ref & core, std::string & reason_unknown); // Throws an exception if goal \c in requires proof generation. void fail_if_proof_generation(char const * tactic_name, goal_ref const & in);