From 622484929f6b4665362f968311de2e8a9bd5188d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 6 May 2013 01:33:40 +0200 Subject: [PATCH] postpone rule flushing dependent on engine Signed-off-by: Nikolaj Bjorner --- src/api/python/z3.py | 3 ++ src/muz_qe/dl_context.cpp | 79 +++++++++++++++++++-------------- src/muz_qe/dl_context.h | 3 +- src/muz_qe/dl_mk_slice.cpp | 24 +++++----- src/muz_qe/pdr_dl_interface.cpp | 4 +- 5 files changed, 66 insertions(+), 47 deletions(-) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index c138bcd62..bbd267292 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -585,6 +585,9 @@ class FuncDeclRef(AstRef): def as_ast(self): return Z3_func_decl_to_ast(self.ctx_ref(), self.ast) + def as_func_decl(self): + return self.ast + def name(self): """Return the name of the function declaration `self`. diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp index dfcaac791..f8e572ab1 100644 --- a/src/muz_qe/dl_context.cpp +++ b/src/muz_qe/dl_context.cpp @@ -234,6 +234,7 @@ namespace datalog { m_vars(m), m_rule_set(*this), m_transformed_rule_set(*this), + m_rule_fmls_head(0), m_rule_fmls(m), m_background(m), m_mc(0), @@ -243,8 +244,6 @@ namespace datalog { m_last_answer(m), m_engine(LAST_ENGINE), m_cancel(false) { - - //register plugins for builtin tables } context::~context() { @@ -254,6 +253,9 @@ namespace datalog { void context::reset() { m_trail.reset(); m_rule_set.reset(); + m_rule_fmls_head = 0; + m_rule_fmls.reset(); + m_rule_names.reset(); m_argument_var_names.reset(); m_preds.reset(); m_preds_by_name.reset(); @@ -457,13 +459,18 @@ namespace datalog { void context::flush_add_rules() { datalog::rule_manager& rm = get_rule_manager(); scoped_proof_mode _scp(m, generate_proof_trace()?PGM_FINE:PGM_DISABLED); - for (unsigned i = 0; i < m_rule_fmls.size(); ++i) { - expr* fml = m_rule_fmls[i].get(); + while (m_rule_fmls_head < m_rule_fmls.size()) { + expr* fml = m_rule_fmls[m_rule_fmls_head].get(); proof* p = generate_proof_trace()?m.mk_asserted(fml):0; - rm.mk_rule(fml, p, m_rule_set, m_rule_names[i]); + rm.mk_rule(fml, p, m_rule_set, m_rule_names[m_rule_fmls_head]); + ++m_rule_fmls_head; + } + rule_set::iterator it = m_rule_set.begin(), end = m_rule_set.end(); + rule_ref r(m_rule_manager); + for (; it != end; ++it) { + r = *it; + check_rule(r); } - m_rule_fmls.reset(); - m_rule_names.reset(); } // @@ -958,18 +965,21 @@ namespace datalog { engine_type_proc(ast_manager& m): m(m), a(m), dt(m), m_engine(DATALOG_ENGINE) {} DL_ENGINE get_engine() const { return m_engine; } + void operator()(expr* e) { if (is_quantifier(e)) { m_engine = QPDR_ENGINE; } - else if (a.is_int_real(e) && m_engine != QPDR_ENGINE) { - m_engine = PDR_ENGINE; - } - else if (is_var(e) && m.is_bool(e)) { - m_engine = PDR_ENGINE; - } - else if (dt.is_datatype(m.get_sort(e))) { - m_engine = PDR_ENGINE; + else if (m_engine != QPDR_ENGINE) { + if (a.is_int_real(e)) { + m_engine = PDR_ENGINE; + } + else if (is_var(e) && m.is_bool(e)) { + m_engine = PDR_ENGINE; + } + else if (dt.is_datatype(m.get_sort(e))) { + m_engine = PDR_ENGINE; + } } } }; @@ -1002,7 +1012,7 @@ namespace datalog { if (m_engine == LAST_ENGINE) { expr_fast_mark1 mark; engine_type_proc proc(m); - m_engine = DATALOG_ENGINE; + m_engine = DATALOG_ENGINE; for (unsigned i = 0; m_engine == DATALOG_ENGINE && i < m_rule_set.get_num_rules(); ++i) { rule * r = m_rule_set.get_rule(i); quick_for_each_expr(proc, mark, r->get_head()); @@ -1011,29 +1021,38 @@ namespace datalog { } m_engine = proc.get_engine(); } + for (unsigned i = m_rule_fmls_head; m_engine == DATALOG_ENGINE && i < m_rule_fmls.size(); ++i) { + expr* fml = m_rule_fmls[i].get(); + while (is_quantifier(fml)) { + fml = to_quantifier(fml)->get_expr(); + } + quick_for_each_expr(proc, mark, fml); + m_engine = proc.get_engine(); + } } } lbool context::query(expr* query) { - new_query(); - rule_set::iterator it = m_rule_set.begin(), end = m_rule_set.end(); - rule_ref r(m_rule_manager); - for (; it != end; ++it) { - r = *it; - check_rule(r); - } - switch(get_engine()) { + m_mc = mk_skip_model_converter(); + m_last_status = OK; + m_last_answer = 0; + switch (get_engine()) { case DATALOG_ENGINE: + flush_add_rules(); return rel_query(query); case PDR_ENGINE: case QPDR_ENGINE: + flush_add_rules(); return pdr_query(query); case BMC_ENGINE: case QBMC_ENGINE: + flush_add_rules(); return bmc_query(query); case TAB_ENGINE: + flush_add_rules(); return tab_query(query); case CLP_ENGINE: + flush_add_rules(); return clp_query(query); default: UNREACHABLE(); @@ -1041,14 +1060,6 @@ namespace datalog { } } - void context::new_query() { - m_mc = mk_skip_model_converter(); - - flush_add_rules(); - m_last_status = OK; - m_last_answer = 0; - } - model_ref context::get_model() { switch(get_engine()) { case PDR_ENGINE: @@ -1277,7 +1288,7 @@ namespace datalog { datalog::rule_manager& rm = get_rule_manager(); // ensure that rules are all using bound variables. - for (unsigned i = 0; i < m_rule_fmls.size(); ++i) { + for (unsigned i = m_rule_fmls_head; i < m_rule_fmls.size(); ++i) { ptr_vector sorts; get_free_vars(m_rule_fmls[i].get(), sorts); if (!sorts.empty()) { @@ -1295,7 +1306,7 @@ namespace datalog { rules.push_back(fml); names.push_back((*it)->name()); } - for (unsigned i = 0; i < m_rule_fmls.size(); ++i) { + for (unsigned i = m_rule_fmls_head; i < m_rule_fmls.size(); ++i) { rules.push_back(m_rule_fmls[i].get()); names.push_back(m_rule_names[i]); } diff --git a/src/muz_qe/dl_context.h b/src/muz_qe/dl_context.h index 0a01b3e01..e9abf7f23 100644 --- a/src/muz_qe/dl_context.h +++ b/src/muz_qe/dl_context.h @@ -114,6 +114,7 @@ namespace datalog { pred2syms m_argument_var_names; rule_set m_rule_set; rule_set m_transformed_rule_set; + unsigned m_rule_fmls_head; expr_ref_vector m_rule_fmls; svector m_rule_names; expr_ref_vector m_background; @@ -482,8 +483,6 @@ namespace datalog { void ensure_rel(); - void new_query(); - lbool rel_query(expr* query); lbool pdr_query(expr* query); diff --git a/src/muz_qe/dl_mk_slice.cpp b/src/muz_qe/dl_mk_slice.cpp index 89804447b..1a97c1b81 100644 --- a/src/muz_qe/dl_mk_slice.cpp +++ b/src/muz_qe/dl_mk_slice.cpp @@ -120,12 +120,11 @@ namespace datalog { obj_map::iterator end = m_rule2slice.end(); expr_ref fml(m); for (; it != end; ++it) { - TRACE("dl", - it->m_key->display(m_ctx, tout << "orig:\n"); - it->m_value->display(m_ctx, tout << "new:\n");); - it->m_value->to_formula(fml); m_pinned_exprs.push_back(fml); + TRACE("dl", + tout << "orig: " << mk_pp(fml, m) << "\n"; + it->m_value->display(m_ctx, tout << "new:\n");); m_sliceform2rule.insert(fml, it->m_key); } } @@ -202,9 +201,10 @@ namespace datalog { proof* p0_new = m_new_proof.find(p0); expr* fact0 = m.get_fact(p0); TRACE("dl", tout << "fact0: " << mk_pp(fact0, m) << "\n";); - rule* orig0 = m_sliceform2rule.find(fact0); - /* rule* slice0 = */ m_rule2slice.find(orig0); - /* unsigned_vector const& renaming0 = m_renaming.find(orig0); */ + rule* orig0; + if (!m_sliceform2rule.find(fact0, orig0)) { + return false; + } premises.push_back(p0_new); rule_ref r1(rm), r2(rm), r3(rm); r1 = orig0; @@ -214,9 +214,10 @@ namespace datalog { proof* p1_new = m_new_proof.find(p1); expr* fact1 = m.get_fact(p1); TRACE("dl", tout << "fact1: " << mk_pp(fact1, m) << "\n";); - rule* orig1 = m_sliceform2rule.find(fact1); - /* rule* slice1 = */ m_rule2slice.find(orig1); - /* unsigned_vector const& renaming1 = m_renaming.find(orig1); TBD */ + rule* orig1 = 0; + if (!m_sliceform2rule.find(fact1, orig1)) { + return false; + } premises.push_back(p1_new); // TODO: work with substitutions. @@ -241,6 +242,9 @@ namespace datalog { proof* new_p = m.mk_hyper_resolve(premises.size(), premises.c_ptr(), concl, positions, substs); m_pinned_exprs.push_back(new_p); m_pinned_rules.push_back(r1.get()); + TRACE("dl", + tout << "orig: " << mk_pp(slice_concl, m) << "\n"; + r1->display(m_ctx, tout << "new:");); m_sliceform2rule.insert(slice_concl, r1.get()); m_rule2slice.insert(r1.get(), 0); m_renaming.insert(r1.get(), unsigned_vector()); diff --git a/src/muz_qe/pdr_dl_interface.cpp b/src/muz_qe/pdr_dl_interface.cpp index 63ac6cf4b..3ff54e68e 100644 --- a/src/muz_qe/pdr_dl_interface.cpp +++ b/src/muz_qe/pdr_dl_interface.cpp @@ -32,6 +32,7 @@ Revision History: #include "dl_mk_slice.h" #include "dl_mk_unfold.h" #include "dl_mk_coalesce.h" +#include "model_smt2_pp.h" using namespace pdr; @@ -134,10 +135,10 @@ lbool dl_interface::query(expr * query) { } query_pred = m_ctx.get_rules().get_output_predicate(); - IF_VERBOSE(2, m_ctx.display_rules(verbose_stream());); m_pdr_rules.replace_rules(m_ctx.get_rules()); m_pdr_rules.close(); + m_ctx.record_transformed_rules(); m_ctx.reopen(); m_ctx.replace_rules(old_rules); @@ -151,6 +152,7 @@ lbool dl_interface::query(expr * query) { if (m_pdr_rules.get_rules().empty()) { m_context->set_unsat(); + IF_VERBOSE(1, model_smt2_pp(verbose_stream(), m, *m_context->get_model(),0);); return l_false; }