From 324dc5869da434d84d8d09cf360d36e260456896 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 25 Jun 2013 13:07:28 -0500 Subject: [PATCH] fix substitution bug in qe, working on boogie trace Signed-off-by: Nikolaj Bjorner --- src/api/api_datalog.cpp | 7 +- src/api/z3_api.h | 6 +- src/ast/rewriter/expr_safe_replace.cpp | 7 + src/ast/rewriter/expr_safe_replace.h | 2 + src/muz_qe/clp_context.cpp | 1 + src/muz_qe/clp_context.h | 17 +- src/muz_qe/dl_bmc_engine.cpp | 1 + src/muz_qe/dl_bmc_engine.h | 2 +- src/muz_qe/dl_boogie_proof.cpp | 297 ++++++++++++++++++ src/muz_qe/dl_boogie_proof.h | 87 ++++++ src/muz_qe/dl_cmds.cpp | 4 +- src/muz_qe/dl_compiler.cpp | 8 +- src/muz_qe/dl_context.cpp | 331 ++++++--------------- src/muz_qe/dl_context.h | 35 +-- src/muz_qe/dl_instruction.cpp | 2 +- src/muz_qe/dl_mk_backwards.cpp | 2 +- src/muz_qe/dl_mk_explanations.cpp | 6 +- src/muz_qe/dl_mk_karr_invariants.cpp | 10 +- src/muz_qe/dl_mk_karr_invariants.h | 1 + src/muz_qe/dl_mk_magic_sets.cpp | 2 +- src/muz_qe/dl_mk_partial_equiv.cpp | 2 +- src/muz_qe/dl_mk_rule_inliner.cpp | 5 +- src/muz_qe/dl_mk_similarity_compressor.cpp | 2 +- src/muz_qe/dl_mk_simple_joins.cpp | 8 +- src/muz_qe/dl_mk_subsumption_checker.cpp | 6 +- src/muz_qe/dl_mk_unbound_compressor.cpp | 6 +- src/muz_qe/dl_relation_manager.cpp | 62 +++- src/muz_qe/dl_relation_manager.h | 1 + src/muz_qe/dl_util.h | 38 +++ src/muz_qe/fixedpoint_params.pyg | 2 + src/muz_qe/pdr_context.cpp | 29 +- src/muz_qe/pdr_dl_interface.cpp | 1 + src/muz_qe/pdr_dl_interface.h | 29 +- src/muz_qe/proof_utils.cpp | 2 + src/muz_qe/proof_utils.h | 1 + src/muz_qe/qe_arith_plugin.cpp | 39 ++- src/muz_qe/qe_array_plugin.cpp | 12 +- src/muz_qe/qe_bool_plugin.cpp | 16 +- src/muz_qe/qe_bv_plugin.cpp | 10 +- src/muz_qe/qe_datatype_plugin.cpp | 24 +- src/muz_qe/qe_dl_plugin.cpp | 14 +- src/muz_qe/rel_context.cpp | 3 +- src/muz_qe/rel_context.h | 9 +- src/muz_qe/tab_context.cpp | 1 + src/muz_qe/tab_context.h | 17 +- src/shell/datalog_frontend.cpp | 12 +- src/smt/theory_array_base.cpp | 4 +- 47 files changed, 769 insertions(+), 414 deletions(-) create mode 100644 src/muz_qe/dl_boogie_proof.cpp create mode 100644 src/muz_qe/dl_boogie_proof.h diff --git a/src/api/api_datalog.cpp b/src/api/api_datalog.cpp index f6eadfea0..bf4752645 100644 --- a/src/api/api_datalog.cpp +++ b/src/api/api_datalog.cpp @@ -48,8 +48,11 @@ namespace api { if (!m.has_plugin(name)) { m.register_plugin(name, alloc(datalog::dl_decl_plugin)); } - datalog::relation_manager& r = m_context.get_rel_context().get_rmanager(); - r.register_plugin(alloc(datalog::external_relation_plugin, *this, r)); + datalog::rel_context* rel = m_context.get_rel_context(); + if (rel) { + datalog::relation_manager& r = rel->get_rmanager(); + r.register_plugin(alloc(datalog::external_relation_plugin, *this, r)); + } } void fixedpoint_context::reduce(func_decl* f, unsigned num_args, expr * const* args, expr_ref& result) { diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 6d59cf650..458e2f53f 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -778,11 +778,11 @@ typedef enum } or \nicebox{ - (=> (and ln+1 ln+2 .. ln+m) l0) + (=> (and l1 l2 .. ln) l0) } or in the most general (ground) form: \nicebox{ - (=> (and ln+1 ln+2 .. ln+m) (or l0 l1 .. ln-1)) + (=> (and ln+1 ln+2 .. ln+m) (or l0 l1 .. ln)) } In other words we use the following (Prolog style) convention for Horn implications: @@ -798,7 +798,7 @@ typedef enum general non-ground form is: \nicebox{ - (forall (vars) (=> (and ln+1 ln+2 .. ln+m) (or l0 l1 .. ln-1))) + (forall (vars) (=> (and ln+1 ln+2 .. ln+m) (or l0 l1 .. ln))) } The hyper-resolution rule takes a sequence of parameters. diff --git a/src/ast/rewriter/expr_safe_replace.cpp b/src/ast/rewriter/expr_safe_replace.cpp index 1ec810414..a4886ad1a 100644 --- a/src/ast/rewriter/expr_safe_replace.cpp +++ b/src/ast/rewriter/expr_safe_replace.cpp @@ -106,3 +106,10 @@ void expr_safe_replace::reset() { m_dst.reset(); m_subst.reset(); } + +void expr_safe_replace::apply_substitution(expr* s, expr* def, expr_ref& t) { + reset(); + insert(s, def); + (*this)(t, t); + reset(); +} diff --git a/src/ast/rewriter/expr_safe_replace.h b/src/ast/rewriter/expr_safe_replace.h index b6131906a..ad626d18f 100644 --- a/src/ast/rewriter/expr_safe_replace.h +++ b/src/ast/rewriter/expr_safe_replace.h @@ -39,6 +39,8 @@ public: void operator()(expr* src, expr_ref& e); + void apply_substitution(expr* s, expr* def, expr_ref& t); + void reset(); }; diff --git a/src/muz_qe/clp_context.cpp b/src/muz_qe/clp_context.cpp index 94a956eb9..3a3908f59 100644 --- a/src/muz_qe/clp_context.cpp +++ b/src/muz_qe/clp_context.cpp @@ -205,6 +205,7 @@ namespace datalog { }; clp::clp(context& ctx): + engine_base(ctx.get_manager(), "clp"), m_imp(alloc(imp, ctx)) { } clp::~clp() { diff --git a/src/muz_qe/clp_context.h b/src/muz_qe/clp_context.h index 635891205..5184b474d 100644 --- a/src/muz_qe/clp_context.h +++ b/src/muz_qe/clp_context.h @@ -22,23 +22,24 @@ Revision History: #include "ast.h" #include "lbool.h" #include "statistics.h" +#include "dl_util.h" namespace datalog { class context; - class clp { + class clp : public datalog::engine_base { class imp; imp* m_imp; public: clp(context& ctx); ~clp(); - lbool query(expr* query); - void cancel(); - void cleanup(); - void reset_statistics(); - void collect_statistics(statistics& st) const; - void display_certificate(std::ostream& out) const; - expr_ref get_answer(); + virtual lbool query(expr* query); + virtual void cancel(); + virtual void cleanup(); + virtual void reset_statistics(); + virtual void collect_statistics(statistics& st) const; + virtual void display_certificate(std::ostream& out) const; + virtual expr_ref get_answer(); }; }; diff --git a/src/muz_qe/dl_bmc_engine.cpp b/src/muz_qe/dl_bmc_engine.cpp index 8e9fb510e..65a60cdeb 100644 --- a/src/muz_qe/dl_bmc_engine.cpp +++ b/src/muz_qe/dl_bmc_engine.cpp @@ -1416,6 +1416,7 @@ namespace datalog { }; bmc::bmc(context& ctx): + engine_base(ctx.get_manager(), "bmc"), m_ctx(ctx), m(ctx.get_manager()), m_solver(m, m_fparams), diff --git a/src/muz_qe/dl_bmc_engine.h b/src/muz_qe/dl_bmc_engine.h index 5911f5f72..e20987002 100644 --- a/src/muz_qe/dl_bmc_engine.h +++ b/src/muz_qe/dl_bmc_engine.h @@ -30,7 +30,7 @@ Revision History: namespace datalog { class context; - class bmc { + class bmc : public engine_base { context& m_ctx; ast_manager& m; smt_params m_fparams; diff --git a/src/muz_qe/dl_boogie_proof.cpp b/src/muz_qe/dl_boogie_proof.cpp new file mode 100644 index 000000000..8720b3544 --- /dev/null +++ b/src/muz_qe/dl_boogie_proof.cpp @@ -0,0 +1,297 @@ +/** + +Example from Boogie: + +(derivation +(step s!4 (main_loop_LoopHead true true) + rule!3 (subst + (= assertsPassed@@1 true) + (= assertsPassed@2@@0 true) + (= main_loop_LoopHead_assertsPassed true) + ) + (labels @950 +895 +668 +670 +893 +899 ) + (ref true )) +(step s!3 (main true false) + rule!1 (subst + (= assertsPassed true) + (= assertsPassed@0 true) + (= assertsPassed@2 false) + (= main_assertsPassed false) + ) + (labels @839 +763 +547 +546 +761 +544 +545 +si_fcall_805 +681 +768 ) + (ref s!4 )) +(step s!2 (main_SeqInstr true false) + rule!2 (subst + (= assertsPassed@@0 true) + (= assertsPassed@0@@0 false) + (= main_SeqInstr_assertsPassed false) + ) + (labels @890 +851 +572 +si_fcall_883 +853 ) + (ref s!3 )) +(step s!1 (@Fail!0) + rule!4 (subst + (= assertsPassed@@2 true) + (= main_SeqInstr_assertsPassed@@0 false) + ) + (labels ) + (ref s!2 )) +) +(model +"tickleBool -> { + true -> true + false -> true + else -> true +} +") +*/ + +#include "dl_boogie_proof.h" +#include "model_pp.h" +#include "proof_utils.h" +#include "ast_pp.h" +#include "dl_util.h" + +namespace datalog { + + /** + \brief push hyper-resolution steps upwards such that every use of + hyper-resolution uses a premise that is not derived from hyper-resolution. + + perform the following rewrite: + + hr(hr(p1,p2,p3,..),p4,p5) => hr(p1,hr(p2,p4),p3,..,p5) + + */ + + void mk_input_resolution(proof_ref& pr) { + ast_manager& m = pr.get_manager(); + proof_ref pr1(m); + proof_ref_vector premises1(m), premises2(m), premises(m); + expr_ref conclusion1(m), conclusion2(m), conclusion(m); + svector > positions1, positions2, positions; + vector substs1, substs2, substs; + + if (m.is_hyper_resolve(pr, premises1, conclusion1, positions1, substs1) && + m.is_hyper_resolve(premises1[0].get(), premises, conclusion2, positions, substs2)) { + for (unsigned i = 1; i < premises1.size(); ++i) { + pr1 = premises1[i].get(); + mk_input_resolution(pr1); + premises1[i] = pr1; + } + for (unsigned i = 0; i < premises.size(); ++i) { + pr1 = premises[i].get(); + mk_input_resolution(pr1); + premises[i] = pr1; + } + unsigned sz = premises.size(); + for (unsigned i = 1; i < sz; ++i) { + proof* premise = premises[i].get(); + expr_ref_vector literals(m); + expr* l1, *l2; + if (!m.is_implies(premise, l1, l2)) { + continue; + } + datalog::flatten_and(l1, literals); + positions2.reset(); + premises2.reset(); + premises2.push_back(premise); + substs2.reset(); + for (unsigned j = 0; j < literals.size(); ++j) { + expr* lit = literals[j].get(); + for (unsigned k = 1; k < premises1.size(); ++k) { + if (m.get_fact(premises1[k].get()) == lit) { + premises2.push_back(premises1[k].get()); + positions2.push_back(std::make_pair(j+1,0)); + substs2.push_back(expr_ref_vector(m)); + break; + } + } + } + premises[i] = m.mk_hyper_resolve(premises2.size(), premises2.c_ptr(), l2, positions2, substs2); + } + conclusion = conclusion1; + pr = m.mk_hyper_resolve(premises.size(), premises.c_ptr(), conclusion, positions, substs); + } + } + + void boogie_proof::set_proof(proof* p) { + std::cout << "set proof\n"; + m_proof = p; + proof_utils::push_instantiations_up(m_proof); + mk_input_resolution(m_proof); + std::cout << "proof set\n"; + } + + void boogie_proof::set_model(model* m) { + m_model = m; + } + + void boogie_proof::pp(std::ostream& out) { + if (m_proof) { + pp_proof(out); + } + if (m_model) { + model_pp(out, *m_model); + } + } + + void boogie_proof::pp_proof(std::ostream& out) { + vector steps; + ptr_vector rules; + rules.push_back(m_proof); + steps.push_back(step()); + obj_map index; + index.insert(m_proof, 0); + + for (unsigned j = 0; j < rules.size(); ++j) { + proof* p = rules[j]; + proof_ref_vector premises(m); + expr_ref conclusion(m); + svector > positions; + vector substs; + + expr* tmp; + steps[j].m_fact = m.get_fact(p); + m.is_implies(steps[j].m_fact, tmp, steps[j].m_fact); + get_subst(p, steps[j].m_subst); + get_labels(p, steps[j].m_labels); + + if (m.is_hyper_resolve(p, premises, conclusion, positions, substs)) { + for (unsigned i = 1; i < premises.size(); ++i) { + proof* premise = premises[i].get(); + unsigned position = 0; + if (!index.find(premise, position)) { + position = rules.size(); + rules.push_back(premise); + steps.push_back(step()); + index.insert(premise, position); + } + steps[j].m_refs.push_back(position); + } + get_rule_name(premises[0].get(), steps[j].m_rule_name); + } + } + for (unsigned j = steps.size(); j > 0; ) { + --j; + step &s = steps[j]; + + // TBD + s.m_labels; + + // set references, compensate for reverse ordering. + for (unsigned i = 0; i < s.m_refs.size(); ++i) { + s.m_refs[i] = rules.size()-1-s.m_refs[i]; + } + } + steps.reverse(); + pp_steps(out, steps); + } + + /** + \brief extract the instantiation by searching for the first occurrence of a hyper-resolution + rule that produces an instance. + */ + void boogie_proof::get_subst(proof* p, subst& s) { + ptr_vector todo; + todo.push_back(p); + ast_mark visited; + std::cout << "get_subst\n" << mk_pp(p, m) << "\n"; + while (!todo.empty()) { + proof* p = todo.back(); + todo.pop_back(); + if (visited.is_marked(p)) { + continue; + } + visited.mark(p, true); + proof_ref_vector premises(m); + expr_ref conclusion(m); + svector > positions; + vector substs; + if (m.is_hyper_resolve(p, premises, conclusion, positions, substs)) { + expr_ref_vector const& sub = substs[0]; + if (!sub.empty()) { + quantifier* q = to_quantifier(m.get_fact(premises[0].get())); + unsigned sz = sub.size(); + SASSERT(sz == q->get_num_decls()); + for (unsigned i = 0; i < sz; ++i) { + s.push_back(std::make_pair(q->get_decl_name(sz-1-i), sub[i])); + } + return; + } + } + unsigned sz = m.get_num_parents(p); + for (unsigned i = 0; i < sz; ++i) { + todo.push_back(m.get_parent(p, i)); + } + } + } + + void boogie_proof::get_rule_name(proof* p, symbol& n) { + + } + + void boogie_proof::get_labels(proof* p, labels& lbls) { + + } + + void boogie_proof::pp_steps(std::ostream& out, vector& steps) { + out << "(derivation\n"; + for (unsigned i = 0; i < steps.size(); ++i) { + pp_step(out, i, steps[i]); + } + out << ")\n"; + + } + + // step :: "(" "step" step-name fact rule-name subst labels premises ")" + void boogie_proof::pp_step(std::ostream& out, unsigned id, step& s) { + out << "(step\n"; + out << " s!" << id << " "; + pp_fact(out, s.m_fact); + out << " " << s.m_rule_name << "\n"; + pp_subst(out << " ", s.m_subst); + pp_labels(out << " ", s.m_labels); + pp_premises(out << " ", s.m_refs); + out << ")\n"; + } + + // fact :: "(" predicate theory-term* ")" + void boogie_proof::pp_fact(std::ostream& out, expr* fact) { + out << mk_pp(fact, m) << "\n"; + } + + // subst :: "(" "subst" assignment* ")" + void boogie_proof::pp_subst(std::ostream& out, subst& s) { + out << "(subst"; + for (unsigned i = 0; i < s.size(); ++i) { + pp_assignment(out, s[i].first, s[i].second); + } + out << ")\n"; + } + + // assignment :: "(" "=" variable theory-term ")" + void boogie_proof::pp_assignment(std::ostream& out, symbol const& v, expr* t) { + out << "\n (= " << v << " " << mk_pp(t, m) << ")"; + } + + + // labels :: "(" "labels" label* ")" + void boogie_proof::pp_labels(std::ostream& out, labels& lbls) { + out << "(labels"; + for (unsigned i = 0; i < lbls.size(); ++i) { + out << " " << lbls[i]; + } + out << ")\n"; + } + + // premises "(" "ref" step-name* ")" + void boogie_proof::pp_premises(std::ostream& out, refs& refs) { + out << "(ref"; + for (unsigned i = 0; i < refs.size(); ++i) { + out << " s!" << refs[i]; + } + out << ")\n"; + } + + +} diff --git a/src/muz_qe/dl_boogie_proof.h b/src/muz_qe/dl_boogie_proof.h new file mode 100644 index 000000000..6c8fbbae3 --- /dev/null +++ b/src/muz_qe/dl_boogie_proof.h @@ -0,0 +1,87 @@ +/** + +output :: derivation model + +derivation :: "(" "derivation" step* ")" + +step :: "(" "step" step-name fact rule-name subst labels premises ")" + +step-name :: identifier + +rule-name :: identifier + +fact :: "(" predicate theory-term* ")" + +subst :: "(" "subst" assignment* ")" + +assignment :: "(" "=" variable theory-term ")" + +labels :: "(" "labels" label* ")" + +premises :: "(" "ref" step-name* ")" + +model :: "(" "model" smtlib2-model ")" + +In each step the "fact" is derivable by hyper-resolution from the named +premises and the named rule, under the given substitution for the +universally quantified variables in the rule. The premises of each +step must have occurred previously in the step sequence. The last fact +is a nullary placeholder predicate representing satisfaction of the query +(its name is arbitrary). + +The labels list consists of all the positively labeled sub-formulas whose +truth is used in the proof, and all the negatively labeled formulas whose +negation is used. A theory-term is a ground term using only interpreted +constants of the background theories. + +The smtlib2-model gives an interpretation of the uninterpreted constants +in the background theory under which the derivation is valid. Currently +it is a quoted string in the old z3 model format, for compatibility with +Boogie, however, this should be changed to the new model format (using +define-fun) when Boogie supports this. + +*/ + +#include "ast.h" +#include "model.h" + +namespace datalog { + class boogie_proof { + typedef vector > subst; + typedef svector labels; + typedef unsigned_vector refs; + struct step { + symbol m_rule_name; + expr* m_fact; + subst m_subst; + labels m_labels; + refs m_refs; + }; + + ast_manager& m; + proof_ref m_proof; + model_ref m_model; + + void pp_proof(std::ostream& out); + void pp_steps(std::ostream& out, vector& steps); + void pp_step(std::ostream& out, unsigned i, step& s); + void pp_fact(std::ostream& out, expr* fact); + void pp_subst(std::ostream& out, subst& s); + void pp_assignment(std::ostream& out, symbol const& v, expr* t); + void pp_labels(std::ostream& out, labels& lbls); + void pp_premises(std::ostream& out, refs& refs); + + void get_subst(proof* p, subst& sub); + void get_rule_name(proof* p, symbol&); + void get_labels(proof* p, labels&); + + public: + boogie_proof(ast_manager& m): m(m), m_proof(m), m_model(0) {} + + void set_proof(proof* p); + + void set_model(model* m); + + void pp(std::ostream& out); + }; +} diff --git a/src/muz_qe/dl_cmds.cpp b/src/muz_qe/dl_cmds.cpp index b82225785..693105e6e 100644 --- a/src/muz_qe/dl_cmds.cpp +++ b/src/muz_qe/dl_cmds.cpp @@ -328,9 +328,7 @@ private: void print_certificate(cmd_context& ctx) { if (m_dl_ctx->get_params().print_certificate()) { datalog::context& dlctx = m_dl_ctx->dlctx(); - if (!dlctx.display_certificate(ctx.regular_stream())) { - throw cmd_exception("certificates are not supported for the selected engine"); - } + dlctx.display_certificate(ctx.regular_stream()); ctx.regular_stream() << "\n"; } } diff --git a/src/muz_qe/dl_compiler.cpp b/src/muz_qe/dl_compiler.cpp index 3f16d0dab..a5f8009e7 100644 --- a/src/muz_qe/dl_compiler.cpp +++ b/src/muz_qe/dl_compiler.cpp @@ -42,7 +42,7 @@ namespace datalog { return; } relation_signature sig; - m_context.get_rel_context().get_rmanager().from_predicate(pred, sig); + m_context.get_rel_context()->get_rmanager().from_predicate(pred, sig); reg_idx reg = get_fresh_register(sig); e->get_data().m_value=reg; @@ -606,7 +606,7 @@ namespace datalog { } SASSERT(is_app(e)); relation_sort arg_sort; - m_context.get_rel_context().get_rmanager().from_predicate(neg_pred, i, arg_sort); + m_context.get_rel_context()->get_rmanager().from_predicate(neg_pred, i, arg_sort); reg_idx new_reg; bool new_dealloc; make_add_constant_column(head_pred, filtered_res, arg_sort, to_app(e), new_reg, new_dealloc, acc); @@ -1252,7 +1252,7 @@ namespace datalog { func_decl_set::iterator fdit = preds.begin(); func_decl_set::iterator fdend = preds.end(); for(; fdit!=fdend; ++fdit) { - if(!m_context.get_rel_context().get_rmanager().is_saturated(*fdit)) { + if(!m_context.get_rel_context()->get_rmanager().is_saturated(*fdit)) { return false; } } @@ -1337,7 +1337,7 @@ namespace datalog { acc.set_observer(0); - TRACE("dl", execution_code.display(m_context.get_rel_context(), tout);); + TRACE("dl", execution_code.display(*m_context.get_rel_context(), tout);); } diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp index f8e572ab1..2627cbbec 100644 --- a/src/muz_qe/dl_context.cpp +++ b/src/muz_qe/dl_context.cpp @@ -45,6 +45,7 @@ Revision History: #include"dl_mk_bit_blast.h" #include"dl_mk_array_blast.h" #include"dl_mk_karr_invariants.h" +#include"dl_mk_magic_symbolic.h" #include"dl_mk_quantifier_abstraction.h" #include"dl_mk_quantifier_instantiation.h" #include"datatype_decl_plugin.h" @@ -238,11 +239,13 @@ namespace datalog { m_rule_fmls(m), m_background(m), m_mc(0), + m_rel(0), + m_engine(0), m_closed(false), m_saturation_was_run(false), m_last_status(OK), m_last_answer(m), - m_engine(LAST_ENGINE), + m_engine_type(LAST_ENGINE), m_cancel(false) { } @@ -260,8 +263,7 @@ namespace datalog { m_preds.reset(); m_preds_by_name.reset(); reset_dealloc_values(m_sorts); - m_pdr = 0; - m_bmc = 0; + m_engine = 0; m_rel = 0; } @@ -432,8 +434,7 @@ namespace datalog { void context::set_predicate_representation(func_decl * pred, unsigned relation_name_cnt, symbol const * relation_names) { - if (relation_name_cnt > 0) { - ensure_rel(); + if (m_rel && relation_name_cnt > 0) { m_rel->set_predicate_representation(pred, relation_name_cnt, relation_names); } } @@ -445,7 +446,7 @@ namespace datalog { register_predicate(new_pred, true); - if (m_rel.get()) { + if (m_rel) { m_rel->inherit_predicate_kind(new_pred, orig_pred); } return new_pred; @@ -542,64 +543,18 @@ namespace datalog { } unsigned context::get_num_levels(func_decl* pred) { - switch(get_engine()) { - case DATALOG_ENGINE: - throw default_exception("get_num_levels is not supported for datalog engine"); - case PDR_ENGINE: - case QPDR_ENGINE: - ensure_pdr(); - return m_pdr->get_num_levels(pred); - case BMC_ENGINE: - case QBMC_ENGINE: - throw default_exception("get_num_levels is not supported for bmc"); - case TAB_ENGINE: - throw default_exception("get_num_levels is not supported for tab"); - case CLP_ENGINE: - throw default_exception("get_num_levels is not supported for clp"); - default: - throw default_exception("unknown engine"); - } + ensure_engine(); + return m_engine->get_num_levels(pred); } expr_ref context::get_cover_delta(int level, func_decl* pred) { - switch(get_engine()) { - case DATALOG_ENGINE: - throw default_exception("operation is not supported for datalog engine"); - case PDR_ENGINE: - case QPDR_ENGINE: - ensure_pdr(); - return m_pdr->get_cover_delta(level, pred); - case BMC_ENGINE: - case QBMC_ENGINE: - throw default_exception("operation is not supported for BMC engine"); - case TAB_ENGINE: - throw default_exception("operation is not supported for TAB engine"); - case CLP_ENGINE: - throw default_exception("operation is not supported for CLP engine"); - default: - throw default_exception("unknown engine"); - } + ensure_engine(); + return m_engine->get_cover_delta(level, pred); } void context::add_cover(int level, func_decl* pred, expr* property) { - switch(get_engine()) { - case DATALOG_ENGINE: - throw default_exception("operation is not supported for datalog engine"); - case PDR_ENGINE: - case QPDR_ENGINE: - ensure_pdr(); - m_pdr->add_cover(level, pred, property); - break; - case BMC_ENGINE: - case QBMC_ENGINE: - throw default_exception("operation is not supported for BMC engine"); - case TAB_ENGINE: - throw default_exception("operation is not supported for TAB engine"); - case CLP_ENGINE: - throw default_exception("operation is not supported for CLP engine"); - default: - throw default_exception("unknown engine"); - } + ensure_engine(); + m_engine->add_cover(level, pred, property); } void context::check_uninterpreted_free(rule_ref& r) { @@ -743,7 +698,7 @@ namespace datalog { void context::add_fact(func_decl * pred, const relation_fact & fact) { if (get_engine() == DATALOG_ENGINE) { - ensure_rel(); + ensure_engine(); m_rel->add_fact(pred, fact); } else { @@ -769,7 +724,7 @@ namespace datalog { void context::add_table_fact(func_decl * pred, const table_fact & fact) { if (get_engine() == DATALOG_ENGINE) { - ensure_rel(); + ensure_engine(); m_rel->add_fact(pred, fact); } else { @@ -907,6 +862,9 @@ namespace datalog { m_transf.register_plugin(alloc(datalog::mk_bit_blast, *this, 35000)); m_transf.register_plugin(alloc(datalog::mk_array_blast, *this, 36000)); m_transf.register_plugin(alloc(datalog::mk_karr_invariants, *this, 36010)); + if (get_params().magic()) { + m_transf.register_plugin(alloc(datalog::mk_magic_symbolic, *this, 36020)); + } transform_rules(m_transf); } @@ -917,7 +875,7 @@ namespace datalog { void context::updt_params(params_ref const& p) { m_params_ref.copy(p); - if (m_pdr.get()) m_pdr->updt_params(); + if (m_engine.get()) m_engine->updt_params(); } expr_ref context::get_background_assertion() { @@ -940,45 +898,39 @@ namespace datalog { m_cancel = true; m_last_status = CANCELED; m_transf.cancel(); - if (m_pdr.get()) m_pdr->cancel(); - if (m_bmc.get()) m_bmc->cancel(); - if (m_tab.get()) m_tab->cancel(); - if (m_rel.get()) m_rel->set_cancel(true); + if (m_engine) m_engine->cancel(); } void context::cleanup() { m_cancel = false; m_last_status = OK; - if (m_pdr.get()) m_pdr->cleanup(); - if (m_bmc.get()) m_bmc->cleanup(); - if (m_tab.get()) m_tab->cleanup(); - if (m_rel.get()) m_rel->set_cancel(false); + if (m_engine) m_engine->cleanup(); } class context::engine_type_proc { ast_manager& m; arith_util a; datatype_util dt; - DL_ENGINE m_engine; + DL_ENGINE m_engine_type; public: - engine_type_proc(ast_manager& m): m(m), a(m), dt(m), m_engine(DATALOG_ENGINE) {} + engine_type_proc(ast_manager& m): m(m), a(m), dt(m), m_engine_type(DATALOG_ENGINE) {} - DL_ENGINE get_engine() const { return m_engine; } + DL_ENGINE get_engine() const { return m_engine_type; } void operator()(expr* e) { if (is_quantifier(e)) { - m_engine = QPDR_ENGINE; + m_engine_type = QPDR_ENGINE; } - else if (m_engine != QPDR_ENGINE) { + else if (m_engine_type != QPDR_ENGINE) { if (a.is_int_real(e)) { - m_engine = PDR_ENGINE; + m_engine_type = PDR_ENGINE; } else if (is_var(e) && m.is_bool(e)) { - m_engine = PDR_ENGINE; + m_engine_type = PDR_ENGINE; } else if (dt.is_datatype(m.get_sort(e))) { - m_engine = PDR_ENGINE; + m_engine_type = PDR_ENGINE; } } } @@ -988,46 +940,46 @@ namespace datalog { symbol e = m_params.engine(); if (e == symbol("datalog")) { - m_engine = DATALOG_ENGINE; + m_engine_type = DATALOG_ENGINE; } else if (e == symbol("pdr")) { - m_engine = PDR_ENGINE; + m_engine_type = PDR_ENGINE; } else if (e == symbol("qpdr")) { - m_engine = QPDR_ENGINE; + m_engine_type = QPDR_ENGINE; } else if (e == symbol("bmc")) { - m_engine = BMC_ENGINE; + m_engine_type = BMC_ENGINE; } else if (e == symbol("qbmc")) { - m_engine = QBMC_ENGINE; + m_engine_type = QBMC_ENGINE; } else if (e == symbol("tab")) { - m_engine = TAB_ENGINE; + m_engine_type = TAB_ENGINE; } else if (e == symbol("clp")) { - m_engine = CLP_ENGINE; + m_engine_type = CLP_ENGINE; } - if (m_engine == LAST_ENGINE) { + if (m_engine_type == LAST_ENGINE) { expr_fast_mark1 mark; engine_type_proc proc(m); - m_engine = DATALOG_ENGINE; - for (unsigned i = 0; m_engine == DATALOG_ENGINE && i < m_rule_set.get_num_rules(); ++i) { + m_engine_type = DATALOG_ENGINE; + for (unsigned i = 0; m_engine_type == 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()); for (unsigned j = 0; j < r->get_tail_size(); ++j) { quick_for_each_expr(proc, mark, r->get_tail(j)); } - m_engine = proc.get_engine(); + m_engine_type = proc.get_engine(); } - for (unsigned i = m_rule_fmls_head; m_engine == DATALOG_ENGINE && i < m_rule_fmls.size(); ++i) { + for (unsigned i = m_rule_fmls_head; m_engine_type == 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(); + m_engine_type = proc.get_engine(); } } } @@ -1038,170 +990,78 @@ namespace datalog { 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); + break; default: UNREACHABLE(); - return rel_query(query); } + ensure_engine(); + return m_engine->query(query); } model_ref context::get_model() { - switch(get_engine()) { - case PDR_ENGINE: - case QPDR_ENGINE: - ensure_pdr(); - return m_pdr->get_model(); - default: - return model_ref(alloc(model, m)); - } + ensure_engine(); + return m_engine->get_model(); } proof_ref context::get_proof() { - switch(get_engine()) { - case PDR_ENGINE: - case QPDR_ENGINE: - ensure_pdr(); - return m_pdr->get_proof(); - default: - return proof_ref(m.mk_asserted(m.mk_true()), m); - } + ensure_engine(); + return m_engine->get_proof(); } - void context::ensure_pdr() { - if (!m_pdr.get()) { - m_pdr = alloc(pdr::dl_interface, *this); + void context::ensure_engine() { + if (!m_engine.get()) { + switch (get_engine()) { + case PDR_ENGINE: + case QPDR_ENGINE: + m_engine = alloc(pdr::dl_interface, *this); + break; + case DATALOG_ENGINE: + m_rel = alloc(rel_context, *this); + m_engine = m_rel; + break; + case BMC_ENGINE: + case QBMC_ENGINE: + m_engine = alloc(bmc, *this); + break; + case TAB_ENGINE: + m_engine = alloc(tab, *this); + break; + case CLP_ENGINE: + m_engine = alloc(clp, *this); + break; + } } } - lbool context::pdr_query(expr* query) { - ensure_pdr(); - return m_pdr->query(query); - } - - void context::ensure_bmc() { - if (!m_bmc.get()) { - m_bmc = alloc(bmc, *this); + lbool context::rel_query(unsigned num_rels, func_decl * const* rels) { + ensure_engine(); + if (m_rel) { + return m_rel->query(num_rels, rels); + } + else { + return l_undef; } } - - lbool context::bmc_query(expr* query) { - ensure_bmc(); - return m_bmc->query(query); - } - - void context::ensure_tab() { - if (!m_tab.get()) { - m_tab = alloc(tab, *this); - } - } - - void context::ensure_clp() { - if (!m_clp.get()) { - m_clp = alloc(clp, *this); - } - } - - lbool context::tab_query(expr* query) { - ensure_tab(); - return m_tab->query(query); - } - - lbool context::clp_query(expr* query) { - ensure_clp(); - return m_clp->query(query); - } - - void context::ensure_rel() { - if (!m_rel.get()) { - m_rel = alloc(rel_context, *this); - } - } - - lbool context::rel_query(unsigned num_rels, func_decl * const* rels) { - ensure_rel(); - return m_rel->query(num_rels, rels); - } - - lbool context::rel_query(expr* query) { - ensure_rel(); - return m_rel->query(query); - } - - + expr* context::get_answer_as_formula() { if (m_last_answer) { return m_last_answer.get(); } - switch(get_engine()) { - case PDR_ENGINE: - case QPDR_ENGINE: - ensure_pdr(); - m_last_answer = m_pdr->get_answer(); - return m_last_answer.get(); - case BMC_ENGINE: - case QBMC_ENGINE: - ensure_bmc(); - m_last_answer = m_bmc->get_answer(); - return m_last_answer.get(); - case DATALOG_ENGINE: - ensure_rel(); - m_last_answer = m_rel->get_last_answer(); - return m_last_answer.get(); - case TAB_ENGINE: - ensure_tab(); - m_last_answer = m_tab->get_answer(); - return m_last_answer.get(); - case CLP_ENGINE: - ensure_clp(); - m_last_answer = m_clp->get_answer(); - return m_last_answer.get(); - default: - UNREACHABLE(); - } - m_last_answer = m.mk_false(); + ensure_engine(); + m_last_answer = m_engine->get_answer(); return m_last_answer.get(); } - bool context::display_certificate(std::ostream& out) { - switch(get_engine()) { - case DATALOG_ENGINE: - return false; - case PDR_ENGINE: - case QPDR_ENGINE: - ensure_pdr(); - m_pdr->display_certificate(out); - return true; - case BMC_ENGINE: - case QBMC_ENGINE: - ensure_bmc(); - m_bmc->display_certificate(out); - return true; - case TAB_ENGINE: - ensure_tab(); - m_tab->display_certificate(out); - return true; - case CLP_ENGINE: - ensure_clp(); - m_clp->display_certificate(out); - return true; - default: - return false; - } + void context::display_certificate(std::ostream& out) { + ensure_engine(); + m_engine->display_certificate(out); } void context::display_profile(std::ostream& out) const { @@ -1219,26 +1079,14 @@ namespace datalog { } void context::reset_statistics() { - if (m_pdr) { - m_pdr->reset_statistics(); - } - if (m_bmc) { - m_bmc->reset_statistics(); - } - if (m_tab) { - m_tab->reset_statistics(); + if (m_engine) { + m_engine->reset_statistics(); } } void context::collect_statistics(statistics& st) const { - if (m_pdr) { - m_pdr->collect_statistics(st); - } - if (m_bmc) { - m_bmc->collect_statistics(st); - } - if (m_tab) { - m_tab->collect_statistics(st); + if (m_engine) { + m_engine->collect_statistics(st); } } @@ -1246,8 +1094,7 @@ namespace datalog { execution_result context::get_status() { return m_last_status; } bool context::result_contains_fact(relation_fact const& f) { - ensure_rel(); - return m_rel->result_contains_fact(f); + return m_rel && m_rel->result_contains_fact(f); } // NB: algebraic data-types declarations will not be printed. diff --git a/src/muz_qe/dl_context.h b/src/muz_qe/dl_context.h index e9abf7f23..c54f7d591 100644 --- a/src/muz_qe/dl_context.h +++ b/src/muz_qe/dl_context.h @@ -121,17 +121,14 @@ namespace datalog { model_converter_ref m_mc; proof_converter_ref m_pc; - scoped_ptr m_pdr; - scoped_ptr m_bmc; - scoped_ptr m_rel; - scoped_ptr m_tab; - scoped_ptr m_clp; + rel_context* m_rel; + scoped_ptr m_engine; bool m_closed; bool m_saturation_was_run; execution_result m_last_status; expr_ref m_last_answer; - DL_ENGINE m_engine; + DL_ENGINE m_engine_type; volatile bool m_cancel; @@ -161,7 +158,7 @@ namespace datalog { rule_manager & get_rule_manager() { return m_rule_manager; } smt_params & get_fparams() const { return m_fparams; } fixedpoint_params const& get_params() const { return m_params; } - DL_ENGINE get_engine() { configure_engine(); return m_engine; } + DL_ENGINE get_engine() { configure_engine(); return m_engine_type; } th_rewriter& get_rewriter() { return m_rewriter; } var_subst & get_var_subst() { return m_var_subst; } dl_decl_util & get_decl_util() { return m_decl_util; } @@ -454,14 +451,14 @@ namespace datalog { /** \brief Display a certificate for reachability and/or unreachability. */ - bool display_certificate(std::ostream& out); + void display_certificate(std::ostream& out); /** \brief query result if it contains fact. */ bool result_contains_fact(relation_fact const& f); - rel_context& get_rel_context() { ensure_rel(); return *m_rel; } + rel_context* get_rel_context() { ensure_engine(); return m_rel; } private: @@ -473,25 +470,7 @@ namespace datalog { void flush_add_rules(); - void ensure_pdr(); - - void ensure_bmc(); - - void ensure_tab(); - - void ensure_clp(); - - void ensure_rel(); - - lbool rel_query(expr* query); - - lbool pdr_query(expr* query); - - lbool bmc_query(expr* query); - - lbool tab_query(expr* query); - - lbool clp_query(expr* query); + void ensure_engine(); void check_quantifier_free(rule_ref& r); void check_uninterpreted_free(rule_ref& r); diff --git a/src/muz_qe/dl_instruction.cpp b/src/muz_qe/dl_instruction.cpp index 637d9a17f..df4736b8e 100644 --- a/src/muz_qe/dl_instruction.cpp +++ b/src/muz_qe/dl_instruction.cpp @@ -59,7 +59,7 @@ namespace datalog { } rel_context& execution_context::get_rel_context() { - return m_context.get_rel_context(); + return *m_context.get_rel_context(); } struct compare_size_proc { diff --git a/src/muz_qe/dl_mk_backwards.cpp b/src/muz_qe/dl_mk_backwards.cpp index b1d8b7d36..771de0dc3 100644 --- a/src/muz_qe/dl_mk_backwards.cpp +++ b/src/muz_qe/dl_mk_backwards.cpp @@ -48,7 +48,7 @@ namespace datalog { neg.reset(); rule & r = *source.get_rule(i); unsigned utsz = r.get_uninterpreted_tail_size(); - unsigned tsz = r.get_tail_size(); + unsigned tsz = r.get_tail_size(); if (!source.is_output_predicate(r.get_decl())) { tail.push_back(r.get_head()); neg.push_back(false); diff --git a/src/muz_qe/dl_mk_explanations.cpp b/src/muz_qe/dl_mk_explanations.cpp index 004b1823d..253bbbec7 100644 --- a/src/muz_qe/dl_mk_explanations.cpp +++ b/src/muz_qe/dl_mk_explanations.cpp @@ -604,7 +604,7 @@ namespace datalog { m_e_sort = m_decl_util.mk_rule_sort(); m_pinned.push_back(m_e_sort); - relation_manager & rmgr = ctx.get_rel_context().get_rmanager(); + relation_manager & rmgr = ctx.get_rel_context()->get_rmanager(); symbol er_symbol = explanation_relation_plugin::get_name(m_relation_level); m_er_plugin = static_cast(rmgr.get_relation_plugin(er_symbol)); if (!m_er_plugin) { @@ -637,7 +637,7 @@ namespace datalog { void mk_explanations::assign_rel_level_kind(func_decl * e_decl, func_decl * orig) { SASSERT(m_relation_level); - relation_manager & rmgr = m_context.get_rel_context().get_rmanager(); + relation_manager & rmgr = m_context.get_rel_context()->get_rmanager(); unsigned sz = e_decl->get_arity(); relation_signature sig; rmgr.from_predicate(e_decl, sig); @@ -871,7 +871,7 @@ namespace datalog { return 0; } rule_set * res = alloc(rule_set, m_context); - transform_facts(m_context.get_rel_context().get_rmanager(), source, *res); + transform_facts(m_context.get_rel_context()->get_rmanager(), source, *res); transform_rules(source, *res); return res; } diff --git a/src/muz_qe/dl_mk_karr_invariants.cpp b/src/muz_qe/dl_mk_karr_invariants.cpp index 143a38636..4987a7e3d 100644 --- a/src/muz_qe/dl_mk_karr_invariants.cpp +++ b/src/muz_qe/dl_mk_karr_invariants.cpp @@ -49,7 +49,8 @@ namespace datalog { rm(ctx.get_rule_manager()), m_inner_ctx(m, ctx.get_fparams()), a(m), - m_pinned(m) { + m_pinned(m), + m_cancel(false) { params_ref params; params.set_sym("default_relation", symbol("karr_relation")); params.set_sym("engine", symbol("datalog")); @@ -189,6 +190,7 @@ namespace datalog { }; void mk_karr_invariants::cancel() { + m_cancel = true; m_inner_ctx.cancel(); } @@ -211,6 +213,10 @@ namespace datalog { get_invariants(*src_loop); + if (m_cancel) { + return 0; + } + // figure out whether to update same rules as used for saturation. scoped_ptr rev_source = bwd(*src_loop); get_invariants(*rev_source); @@ -225,7 +231,7 @@ namespace datalog { void mk_karr_invariants::get_invariants(rule_set const& src) { m_inner_ctx.reset(); - rel_context& rctx = m_inner_ctx.get_rel_context(); + rel_context& rctx = *m_inner_ctx.get_rel_context(); ptr_vector heads; func_decl_set const& predicates = m_ctx.get_predicates(); for (func_decl_set::iterator fit = predicates.begin(); fit != predicates.end(); ++fit) { diff --git a/src/muz_qe/dl_mk_karr_invariants.h b/src/muz_qe/dl_mk_karr_invariants.h index ec554e284..3d993e60a 100644 --- a/src/muz_qe/dl_mk_karr_invariants.h +++ b/src/muz_qe/dl_mk_karr_invariants.h @@ -57,6 +57,7 @@ namespace datalog { arith_util a; obj_map m_fun2inv; ast_ref_vector m_pinned; + volatile bool m_cancel; void get_invariants(rule_set const& src); diff --git a/src/muz_qe/dl_mk_magic_sets.cpp b/src/muz_qe/dl_mk_magic_sets.cpp index f6f79f348..24d9d01cb 100644 --- a/src/muz_qe/dl_mk_magic_sets.cpp +++ b/src/muz_qe/dl_mk_magic_sets.cpp @@ -362,7 +362,7 @@ namespace datalog { rule * r = *it; transform_rule(task.m_adornment, r, *result); } - if (!m_context.get_rel_context().get_relation(task.m_pred).empty()) { + if (!m_context.get_rel_context()->get_relation(task.m_pred).empty()) { //we need a rule to copy facts that are already in a relation into the adorned //relation (since out intentional predicates can have facts, not only rules) create_transfer_rule(task, *result); diff --git a/src/muz_qe/dl_mk_partial_equiv.cpp b/src/muz_qe/dl_mk_partial_equiv.cpp index 5ba1e71dd..4d1a1e860 100644 --- a/src/muz_qe/dl_mk_partial_equiv.cpp +++ b/src/muz_qe/dl_mk_partial_equiv.cpp @@ -97,7 +97,7 @@ namespace datalog { return 0; } - relation_manager & rm = m_context.get_rel_context().get_rmanager(); + relation_manager & rm = m_context.get_rel_context()->get_rmanager(); rule_set::decl2rules::iterator it = source.begin_grouped_rules(); rule_set::decl2rules::iterator end = source.end_grouped_rules(); diff --git a/src/muz_qe/dl_mk_rule_inliner.cpp b/src/muz_qe/dl_mk_rule_inliner.cpp index 4afc1d323..5e0d6446b 100644 --- a/src/muz_qe/dl_mk_rule_inliner.cpp +++ b/src/muz_qe/dl_mk_rule_inliner.cpp @@ -206,7 +206,10 @@ namespace datalog { void mk_rule_inliner::count_pred_occurrences(rule_set const & orig) { - m_context.get_rel_context().get_rmanager().collect_non_empty_predicates(m_preds_with_facts); + rel_context* rel = m_context.get_rel_context(); + if (rel) { + rel->get_rmanager().collect_non_empty_predicates(m_preds_with_facts); + } rule_set::iterator rend = orig.end(); for (rule_set::iterator rit = orig.begin(); rit!=rend; ++rit) { diff --git a/src/muz_qe/dl_mk_similarity_compressor.cpp b/src/muz_qe/dl_mk_similarity_compressor.cpp index b600811f0..d4f410130 100644 --- a/src/muz_qe/dl_mk_similarity_compressor.cpp +++ b/src/muz_qe/dl_mk_similarity_compressor.cpp @@ -368,7 +368,7 @@ namespace datalog { collect_orphan_consts(*it, const_infos, val_fact); m_context.add_fact(aux_pred, val_fact); } - m_context.get_rel_context().get_rmanager().mark_saturated(aux_pred); + m_context.get_rel_context()->get_rmanager().mark_saturated(aux_pred); app * new_head = r->get_head(); ptr_vector new_tail; diff --git a/src/muz_qe/dl_mk_simple_joins.cpp b/src/muz_qe/dl_mk_simple_joins.cpp index 990125475..300ed0879 100644 --- a/src/muz_qe/dl_mk_simple_joins.cpp +++ b/src/muz_qe/dl_mk_simple_joins.cpp @@ -570,11 +570,15 @@ namespace datalog { cost estimate_size(app * t) const { func_decl * pred = t->get_decl(); unsigned n=pred->get_arity(); - relation_manager& rm = m_context.get_rel_context().get_rmanager(); + rel_context* rel = m_context.get_rel_context(); + if (!rel) { + return cost(1); + } + relation_manager& rm = rel->get_rmanager(); if( (m_context.saturation_was_run() && rm.try_get_relation(pred)) || rm.is_saturated(pred)) { SASSERT(rm.try_get_relation(pred)); //if it is saturated, it should exist - unsigned rel_size_int = m_context.get_rel_context().get_relation(pred).get_size_estimate_rows(); + unsigned rel_size_int = rel->get_relation(pred).get_size_estimate_rows(); if(rel_size_int!=0) { cost rel_size = static_cast(rel_size_int); cost curr_size = rel_size; diff --git a/src/muz_qe/dl_mk_subsumption_checker.cpp b/src/muz_qe/dl_mk_subsumption_checker.cpp index 8c9e7e69f..0d32a5c3b 100644 --- a/src/muz_qe/dl_mk_subsumption_checker.cpp +++ b/src/muz_qe/dl_mk_subsumption_checker.cpp @@ -249,7 +249,11 @@ namespace datalog { } void mk_subsumption_checker::scan_for_relations_total_due_to_facts(rule_set const& source) { - relation_manager& rm = m_context.get_rel_context().get_rmanager(); + rel_context* rel = m_context.get_rel_context(); + if (!rel) { + return; + } + relation_manager& rm = rel->get_rmanager(); decl_set const& candidate_preds = m_context.get_predicates(); diff --git a/src/muz_qe/dl_mk_unbound_compressor.cpp b/src/muz_qe/dl_mk_unbound_compressor.cpp index 7eb6f829d..71d4d5479 100644 --- a/src/muz_qe/dl_mk_unbound_compressor.cpp +++ b/src/muz_qe/dl_mk_unbound_compressor.cpp @@ -334,8 +334,10 @@ namespace datalog { // TODO mc m_modified = false; - m_context.get_rel_context().get_rmanager().collect_non_empty_predicates(m_non_empty_rels); - + rel_context* rel = m_context.get_rel_context(); + if (rel) { + rel->get_rmanager().collect_non_empty_predicates(m_non_empty_rels); + } unsigned init_rule_cnt = source.get_num_rules(); SASSERT(m_rules.empty()); for (unsigned i=0; i m_filter; + scoped_ptr m_project; + unsigned_vector m_removed_cols; + public: + /** + This constructor should be used only if we know that the projection operation + exists for the result of the join. + */ + default_relation_filter_interpreted_and_project_fn( + relation_mutator_fn* filter, + unsigned removed_col_cnt, + const unsigned * removed_cols) + : m_filter(filter), + m_project(0), + m_removed_cols(removed_col_cnt, removed_cols) {} + + virtual relation_base * operator()(const relation_base & t) { + scoped_rel t1 = t.clone(); + (*m_filter)(*t1); + if( !m_project) { + relation_manager & rmgr = t1->get_plugin().get_manager(); + m_project = rmgr.mk_project_fn(*t1, m_removed_cols.size(), m_removed_cols.c_ptr()); + if (!m_project) { + throw default_exception("projection does not exist"); + } + } + return (*m_project)(*t1); + } + }; + + relation_transformer_fn * relation_manager::mk_filter_interpreted_and_project_fn( + const relation_base & t, app * condition, + unsigned removed_col_cnt, const unsigned * removed_cols) { + + relation_transformer_fn* res = + t.get_plugin().mk_filter_interpreted_and_project_fn( + t, + condition, + removed_col_cnt, + removed_cols); + + if (!res) { + relation_mutator_fn* filter_fn = mk_filter_interpreted_fn(t, condition); + if (filter_fn) { + res = alloc(default_relation_filter_interpreted_and_project_fn, + filter_fn, + removed_col_cnt, + removed_cols); + } + } + return res; + } + class relation_manager::default_relation_join_project_fn : public relation_join_fn { scoped_ptr m_join; @@ -720,14 +774,6 @@ namespace datalog { return t.get_plugin().mk_filter_interpreted_fn(t, condition); } - relation_transformer_fn * relation_manager::mk_filter_interpreted_and_project_fn(const relation_base & t, - app * condition, - unsigned removed_col_cnt, - const unsigned * removed_cols) { - return t.get_plugin().mk_filter_interpreted_and_project_fn(t, condition, removed_col_cnt, removed_cols); - } - - class relation_manager::default_relation_select_equal_and_project_fn : public relation_transformer_fn { scoped_ptr m_filter; scoped_ptr m_project; diff --git a/src/muz_qe/dl_relation_manager.h b/src/muz_qe/dl_relation_manager.h index ccdba2783..9f12b4bb6 100644 --- a/src/muz_qe/dl_relation_manager.h +++ b/src/muz_qe/dl_relation_manager.h @@ -42,6 +42,7 @@ namespace datalog { class default_relation_join_project_fn; class default_relation_select_equal_and_project_fn; class default_relation_intersection_filter_fn; + class default_relation_filter_interpreted_and_project_fn; class auxiliary_table_transformer_fn; class auxiliary_table_filter_fn; diff --git a/src/muz_qe/dl_util.h b/src/muz_qe/dl_util.h index ea2def025..b92a33d1a 100644 --- a/src/muz_qe/dl_util.h +++ b/src/muz_qe/dl_util.h @@ -28,6 +28,8 @@ Revision History: #include"substitution.h" #include"fixedpoint_params.hpp" #include"ast_counter.h" +#include"statistics.h" +#include"lbool.h" namespace datalog { @@ -58,6 +60,42 @@ namespace datalog { LAST_ENGINE }; + class engine_base { + ast_manager& m; + std::string m_name; + public: + engine_base(ast_manager& m, char const* name): m(m), m_name(name) {} + virtual ~engine_base() {} + + virtual expr_ref get_answer() = 0; + virtual lbool query(expr* q) = 0; + + virtual void reset_statistics() {} + virtual void display_profile(std::ostream& out) const {} + virtual void collect_statistics(statistics& st) const {} + virtual unsigned get_num_levels(func_decl* pred) { + throw default_exception(std::string("get_num_levels is not supported for ") + m_name); + } + virtual expr_ref get_cover_delta(int level, func_decl* pred) { + throw default_exception(std::string("operation is not supported for ") + m_name); + } + virtual void add_cover(int level, func_decl* pred, expr* property) { + throw default_exception(std::string("operation is not supported for ") + m_name); + } + virtual void display_certificate(std::ostream& out) const { + throw default_exception(std::string("certificates are not supported for ") + m_name); + } + virtual model_ref get_model() { + return model_ref(alloc(model, m)); + } + virtual proof_ref get_proof() { + return proof_ref(m.mk_asserted(m.mk_true()), m); + } + virtual void updt_params() {} + virtual void cancel() {} + virtual void cleanup() {} + }; + struct std_string_hash_proc { unsigned operator()(const std::string & s) const { return string_hash(s.c_str(), static_cast(s.length()), 17); } diff --git a/src/muz_qe/fixedpoint_params.pyg b/src/muz_qe/fixedpoint_params.pyg index c2996dd8f..860dcb68e 100644 --- a/src/muz_qe/fixedpoint_params.pyg +++ b/src/muz_qe/fixedpoint_params.pyg @@ -10,6 +10,7 @@ def_module_params('fixedpoint', ('bit_blast', BOOL, False, '(PDR) bit-blast bit-vectors'), ('explanations_on_relation_level', BOOL, False, '(DATALOG) if true, explanations are generated as history of each relation, rather than per fact (generate_explanations must be set to true for this option to have any effect)'), ('magic_sets_for_queries', BOOL, False, "(DATALOG) magic set transformation will be used for queries"), + ('magic', BOOL, False, "perform symbolic magic set transformation"), ('unbound_compressor', BOOL, True, "auxiliary relations will be introduced to avoid unbound variables in rule heads"), ('similarity_compressor', BOOL, True, "(DATALOG) rules that differ only in values of constants will be merged into a single rule"), ('similarity_compressor_threshold', UINT, 11, "(DATALOG) if similarity_compressor is on, this value determines how many similar rules there must be in order for them to be merged"), @@ -60,6 +61,7 @@ def_module_params('fixedpoint', "by putting in half of the table columns, if it would have been empty otherwise"), ('print_answer', BOOL, False, 'print answer instance(s) to query'), ('print_certificate', BOOL, False, 'print certificate for reachability or non-reachability'), + ('print_boogie_certificate', BOOL, False, 'print certificate for reachability or non-reachability using a format understood by Boogie'), ('print_statistics', BOOL, False, 'print statistics'), ('use_utvpi', BOOL, True, 'PDR: Enable UTVPI strategy'), ('tab_selection', SYMBOL, 'weight', 'selection method for tabular strategy: weight (default), first, var-use'), diff --git a/src/muz_qe/pdr_context.cpp b/src/muz_qe/pdr_context.cpp index 1c49e0c83..6f81d93d8 100644 --- a/src/muz_qe/pdr_context.cpp +++ b/src/muz_qe/pdr_context.cpp @@ -44,6 +44,7 @@ Notes: #include "proof_checker.h" #include "smt_value_sort.h" #include "proof_utils.h" +#include "dl_boogie_proof.h" namespace pdr { @@ -1063,7 +1064,7 @@ namespace pdr { ast_manager& m = pt.get_manager(); datalog::context& dctx = ctx.get_context(); datalog::rule_manager& rm = dctx.get_rule_manager(); - datalog::rule_unifier unifier(dctx); + datalog::rule_unifier unif(dctx); datalog::dl_decl_util util(m); datalog::rule_ref r0(rm), r1(rm); obj_map cache; @@ -1072,7 +1073,7 @@ namespace pdr { proof_ref_vector trail(m); datalog::rule_ref_vector rules_trail(rm); proof* pr = 0; - unifier.set_normalize(false); + unif.set_normalize(true); todo.push_back(m_root); update_models(); while (!todo.empty()) { @@ -1134,14 +1135,14 @@ namespace pdr { substs.push_back(binding); // TODO base substitution. for (unsigned i = 1; i < rls.size(); ++i) { datalog::rule& src = *rls[i]; - bool unified = unifier.unify_rules(*reduced_rule, 0, src); + bool unified = unif.unify_rules(*reduced_rule, 0, src); if (!unified) { IF_VERBOSE(0, verbose_stream() << "Could not unify rules: "; reduced_rule->display(dctx, verbose_stream()); src.display(dctx, verbose_stream());); } - expr_ref_vector sub1 = unifier.get_rule_subst(*reduced_rule, true); + expr_ref_vector sub1 = unif.get_rule_subst(*reduced_rule, true); TRACE("pdr", for (unsigned k = 0; k < sub1.size(); ++k) { tout << mk_pp(sub1[k].get(), m) << " "; @@ -1160,8 +1161,8 @@ namespace pdr { } positions.push_back(std::make_pair(i,0)); - substs.push_back(unifier.get_rule_subst(src, false)); - VERIFY(unifier.apply(*reduced_rule.get(), 0, src, r3)); + substs.push_back(unif.get_rule_subst(src, false)); + VERIFY(unif.apply(*reduced_rule.get(), 0, src, r3)); reduced_rule = r3; } @@ -1620,6 +1621,12 @@ namespace pdr { IF_VERBOSE(1, verbose_stream() << "\n"; m_search.display(verbose_stream());); m_last_result = l_true; validate(); + + IF_VERBOSE(1, + if (m_params.print_boogie_certificate()) { + display_certificate(verbose_stream()); + }); + return l_true; } catch (inductive_exception) { @@ -2129,7 +2136,15 @@ namespace pdr { break; } case l_true: { - strm << mk_pp(mk_sat_answer(), m); + if (m_params.print_boogie_certificate()) { + datalog::boogie_proof bp(m); + bp.set_proof(get_proof()); + bp.set_model(0); + bp.pp(strm); + } + else { + strm << mk_pp(mk_sat_answer(), m); + } break; } case l_undef: { diff --git a/src/muz_qe/pdr_dl_interface.cpp b/src/muz_qe/pdr_dl_interface.cpp index 437c08f6a..05a13dfc7 100644 --- a/src/muz_qe/pdr_dl_interface.cpp +++ b/src/muz_qe/pdr_dl_interface.cpp @@ -37,6 +37,7 @@ Revision History: using namespace pdr; dl_interface::dl_interface(datalog::context& ctx) : + engine_base(ctx.get_manager(), "pdr"), m_ctx(ctx), m_pdr_rules(ctx), m_old_rules(ctx), diff --git a/src/muz_qe/pdr_dl_interface.h b/src/muz_qe/pdr_dl_interface.h index c4844f892..2075dff47 100644 --- a/src/muz_qe/pdr_dl_interface.h +++ b/src/muz_qe/pdr_dl_interface.h @@ -23,6 +23,7 @@ Revision History: #include "lbool.h" #include "dl_rule.h" #include "dl_rule_set.h" +#include "dl_util.h" #include "statistics.h" namespace datalog { @@ -33,7 +34,7 @@ namespace pdr { class context; - class dl_interface { + class dl_interface : public datalog::engine_base { datalog::context& m_ctx; datalog::rule_set m_pdr_rules; datalog::rule_set m_old_rules; @@ -47,31 +48,31 @@ namespace pdr { dl_interface(datalog::context& ctx); ~dl_interface(); - lbool query(expr* query); + virtual lbool query(expr* query); - void cancel(); + virtual void cancel(); - void cleanup(); + virtual void cleanup(); - void display_certificate(std::ostream& out) const; + virtual void display_certificate(std::ostream& out) const; - void collect_statistics(statistics& st) const; + virtual void collect_statistics(statistics& st) const; - void reset_statistics(); + virtual void reset_statistics(); - expr_ref get_answer(); + virtual expr_ref get_answer(); - unsigned get_num_levels(func_decl* pred); + virtual unsigned get_num_levels(func_decl* pred); - expr_ref get_cover_delta(int level, func_decl* pred); + virtual expr_ref get_cover_delta(int level, func_decl* pred); - void add_cover(int level, func_decl* pred, expr* property); + virtual void add_cover(int level, func_decl* pred, expr* property); - void updt_params(); + virtual void updt_params(); - model_ref get_model(); + virtual model_ref get_model(); - proof_ref get_proof(); + virtual proof_ref get_proof(); }; } diff --git a/src/muz_qe/proof_utils.cpp b/src/muz_qe/proof_utils.cpp index 36e721b5c..87ecf9985 100644 --- a/src/muz_qe/proof_utils.cpp +++ b/src/muz_qe/proof_utils.cpp @@ -608,3 +608,5 @@ void proof_utils::push_instantiations_up(proof_ref& pr) { push_instantiations_up_cl push(pr.get_manager()); push(pr); } + + diff --git a/src/muz_qe/proof_utils.h b/src/muz_qe/proof_utils.h index dc3cdc3ef..383b5c379 100644 --- a/src/muz_qe/proof_utils.h +++ b/src/muz_qe/proof_utils.h @@ -42,6 +42,7 @@ public: */ static void push_instantiations_up(proof_ref& pr); + }; #endif diff --git a/src/muz_qe/qe_arith_plugin.cpp b/src/muz_qe/qe_arith_plugin.cpp index 1baee51fa..7bf0978f6 100644 --- a/src/muz_qe/qe_arith_plugin.cpp +++ b/src/muz_qe/qe_arith_plugin.cpp @@ -20,7 +20,7 @@ Revision History: #include "qe.h" #include "ast_pp.h" -#include "expr_replacer.h" +#include "expr_safe_replace.h" #include "bool_rewriter.h" #include "bv_decl_plugin.h" #include "arith_decl_plugin.h" @@ -93,7 +93,7 @@ namespace qe { expr_ref m_one_r; expr_ref m_tmp; public: - scoped_ptr m_replace; + expr_safe_replace m_replace; bool_rewriter m_bool_rewriter; arith_rewriter m_arith_rewriter; @@ -111,7 +111,7 @@ namespace qe { m_zero_r(m_arith.mk_numeral(numeral(0), false), m), m_one_r(m_arith.mk_numeral(numeral(1), false), m), m_tmp(m), - m_replace(mk_default_expr_replacer(m)), + m_replace(m), m_bool_rewriter(m), m_arith_rewriter(m) { } @@ -827,7 +827,7 @@ namespace qe { while (index <= up) { expr* n = mk_numeral(index); result = body; - m_replace->apply_substitution(x, n, result); + m_replace.apply_substitution(x, n, result); ors.push_back(result); ++index; } @@ -857,7 +857,7 @@ namespace qe { mk_flat_and(e1, body, result); app_ref z(m); mk_bounded_var(up, z_bv, z); - m_replace->apply_substitution(x, z, result); + m_replace.apply_substitution(x, z, result); } @@ -966,7 +966,7 @@ namespace qe { << mk_pp(e, m) << "\n"; ); expr_ref result(fml, m); - m_replace->apply_substitution(x, e, result); + m_replace.apply_substitution(x, e, result); simplify(result); TRACE("qe", tout << "singular solved:\n" @@ -1044,7 +1044,7 @@ namespace qe { tout << " = 0\n"; ); expr_ref result(fml, m); - m_replace->apply_substitution(x, p1, result); + m_replace.apply_substitution(x, p1, result); simplify(result); m_ctx.elim_var(index-1, result, p1); TRACE("qe", tout << "Reduced: " << mk_pp(result, m) << "\n";); @@ -2080,7 +2080,7 @@ public: app* atm = atoms[i]; t1 = m_util.mk_add(m_util.mk_mul(coeffs[i], z), terms[i]); m_util.mk_divides(divisors[i], t1, new_atom); - m_util.m_replace->apply_substitution(atm, new_atom.get(), result); + m_util.m_replace.apply_substitution(atm, new_atom.get(), result); m_ctx.add_constraint(false, mk_not(atm), new_atom); m_ctx.add_constraint(false, mk_not(new_atom), atm); @@ -2121,7 +2121,7 @@ public: m_util.simplify(mod_term2); m_ctx.add_constraint(false, m.mk_eq(mod_term2, m_util.mk_zero(mod_term2))); - m_util.m_replace->apply_substitution(atm, z1, result); + m_util.m_replace.apply_substitution(atm, z1, result); // // conjoin (coeff*z + rest - z1) mod k == 0 to result @@ -2153,7 +2153,7 @@ public: for (unsigned i = 0; i < sz; ++i) { app* e = bounds.atoms(is_strict, is_lower)[i]; m_ctx.add_constraint(true, mk_not(e)); - m_util.m_replace->apply_substitution(e, m.mk_false(), result); + m_util.m_replace.apply_substitution(e, m.mk_false(), result); } } @@ -2162,7 +2162,7 @@ public: for (unsigned i = 0; i < sz; ++i) { app* e = bounds.atoms(is_strict, !is_lower)[i]; m_ctx.add_constraint(true, e); - m_util.m_replace->apply_substitution(e, m.mk_true(), result); + m_util.m_replace.apply_substitution(e, m.mk_true(), result); } } @@ -2276,7 +2276,7 @@ public: else { m_ctx.add_constraint(true, e); } - m_util.m_replace->apply_substitution(atm, m.mk_true(), result); + m_util.m_replace.apply_substitution(atm, m.mk_true(), result); continue; } @@ -2293,7 +2293,7 @@ public: (same_strict && i < index); mk_bound(result_is_strict, is_lower, a, t, b, s, tmp); - m_util.m_replace->apply_substitution(e, tmp.get(), result); + m_util.m_replace.apply_substitution(e, tmp.get(), result); TRACE("qe", tout << (result_is_strict?"strict result":"non-strict result") << "\n"; @@ -2330,7 +2330,7 @@ public: s = x_t.mk_term(b, s); b = x_t.mk_coeff(b); m_util.mk_resolve(x, strict_resolve, a, t, b, s, tmp); - m_util.m_replace->apply_substitution(e, tmp.get(), result); + m_util.m_replace.apply_substitution(e, tmp.get(), result); m_ctx.add_constraint(true, mk_not(e), tmp); @@ -2398,7 +2398,7 @@ public: weights_t m_weights; th_rewriter m_rewriter; nlarith::util m_util; - scoped_ptr m_replacer; + expr_safe_replace m_replace; expr_ref_vector m_trail; factor_rewriter_star m_factor_rw; bool m_produce_models; @@ -2407,7 +2407,7 @@ public: qe_solver_plugin(m, m.mk_family_id("arith"), ctx), m_rewriter(m), m_util(m), - m_replacer(mk_default_expr_replacer(m)), + m_replace(m), m_trail(m), m_factor_rw(m), m_produce_models(produce_models) { @@ -2480,12 +2480,11 @@ public: SASSERT(vl.is_unsigned()); SASSERT(vl.get_unsigned() < brs->size()); unsigned j = vl.get_unsigned(); - expr_substitution sub(m); + m_replace.reset(); for (unsigned i = 0; i < brs->preds().size(); ++i) { - sub.insert(to_app(brs->preds(i)), brs->subst(j)[i]); + m_replace.insert(brs->preds(i), brs->subst(j)[i]); } - m_replacer->set_substitution(&sub); - (*m_replacer)(fml); + m_replace(fml); expr_ref tmp(m.mk_and(brs->constraints(j), fml), m); m_factor_rw(tmp, fml); if (def) { diff --git a/src/muz_qe/qe_array_plugin.cpp b/src/muz_qe/qe_array_plugin.cpp index 106a42338..c9de1d745 100644 --- a/src/muz_qe/qe_array_plugin.cpp +++ b/src/muz_qe/qe_array_plugin.cpp @@ -1,7 +1,7 @@ #include "qe.h" #include "array_decl_plugin.h" -#include "expr_replacer.h" +#include "expr_safe_replace.h" #include "ast_pp.h" #include "arith_decl_plugin.h" @@ -11,13 +11,13 @@ namespace qe { class array_plugin : public qe_solver_plugin { - scoped_ptr m_replace; + expr_safe_replace m_replace; public: array_plugin(i_solver_context& ctx, ast_manager& m) : qe_solver_plugin(m, m.mk_family_id("array"), ctx), - m_replace(mk_default_expr_replacer(m)) + m_replace(m) { } @@ -123,7 +123,7 @@ namespace qe { if (m_ctx.is_var(a, idx) && !m_ctx.contains(idx)(rhs)) { expr_ref result(fml, m); - m_replace->apply_substitution(a, rhs, result); + m_replace.apply_substitution(a, rhs, result); m_ctx.elim_var(idx, result, rhs); return true; } @@ -175,7 +175,7 @@ namespace qe { tout << "eq: " << mk_pp(lhs, m) << " == " << mk_pp(rhs, m) << "\n"; ); expr_ref result(fml, m); - m_replace->apply_substitution(A, store_B_i_t, result); + m_replace.apply_substitution(A, store_B_i_t, result); m_ctx.add_var(B); m_ctx.elim_var(idx, result, store_B_i_t); return true; @@ -248,7 +248,7 @@ namespace qe { tout << "eq: " << mk_pp(lhs, m) << " == " << mk_pp(rhs, m) << "\n"; ); expr_ref result(fml, m); - m_replace->apply_substitution(A, store_t, result); + m_replace.apply_substitution(A, store_t, result); m_ctx.elim_var(idx, result, store_t); return true; } diff --git a/src/muz_qe/qe_bool_plugin.cpp b/src/muz_qe/qe_bool_plugin.cpp index 782644c28..39a46ae55 100644 --- a/src/muz_qe/qe_bool_plugin.cpp +++ b/src/muz_qe/qe_bool_plugin.cpp @@ -25,18 +25,18 @@ Notes: --*/ #include "qe.h" -#include "expr_replacer.h" +#include "expr_safe_replace.h" #include "ast_pp.h" #include "model_evaluator.h" namespace qe { class bool_plugin : public qe_solver_plugin { - scoped_ptr m_replace; + expr_safe_replace m_replace; public: bool_plugin(i_solver_context& ctx, ast_manager& m): qe_solver_plugin(m, m.get_basic_family_id(), ctx), - m_replace(mk_default_expr_replacer(m)) + m_replace(m) {} virtual void assign(contains_app& x, expr* fml, rational const& vl) { @@ -51,7 +51,7 @@ namespace qe { virtual void subst(contains_app& x, rational const& vl, expr_ref& fml, expr_ref* def) { SASSERT(vl.is_one() || vl.is_zero()); expr* tf = (vl.is_one())?m.mk_true():m.mk_false(); - m_replace->apply_substitution(x.x(), tf, 0, fml); + m_replace.apply_substitution(x.x(), tf, fml); if (def) { *def = tf; } @@ -103,12 +103,12 @@ namespace qe { app* a = to_app(e); expr* e1; if (m_ctx.is_var(a, idx)) { - m_replace->apply_substitution(a, m.mk_true(), 0, fml); + m_replace.apply_substitution(a, m.mk_true(), fml); m_ctx.elim_var(idx, fml, m.mk_true()); return true; } else if (m.is_not(e, e1) && m_ctx.is_var(e1, idx)) { - m_replace->apply_substitution(to_app(e1), m.mk_false(), 0, fml); + m_replace.apply_substitution(to_app(e1), m.mk_false(), fml); m_ctx.elim_var(idx, fml, m.mk_false()); return true; } @@ -148,7 +148,7 @@ namespace qe { } // only occurrences of 'x' must be in positive atoms def = m.mk_true(); - m_replace->apply_substitution(x, def, 0, fml); + m_replace.apply_substitution(x, def, fml); return true; } else if (!p && n) { @@ -161,7 +161,7 @@ namespace qe { if (x != *it && contains_x(*it)) return false; } def = m.mk_false(); - m_replace->apply_substitution(x, def, 0, fml); + m_replace.apply_substitution(x, def, fml); return true; } else if (contains_x(fml)) { diff --git a/src/muz_qe/qe_bv_plugin.cpp b/src/muz_qe/qe_bv_plugin.cpp index cae567111..df1f8c619 100644 --- a/src/muz_qe/qe_bv_plugin.cpp +++ b/src/muz_qe/qe_bv_plugin.cpp @@ -21,19 +21,19 @@ Notes: --*/ #include "qe.h" -#include "expr_replacer.h" +#include "expr_safe_replace.h" #include "bv_decl_plugin.h" #include "model_evaluator.h" namespace qe { class bv_plugin : public qe_solver_plugin { - scoped_ptr m_replace; - bv_util m_bv; + expr_safe_replace m_replace; + bv_util m_bv; public: bv_plugin(i_solver_context& ctx, ast_manager& m): qe_solver_plugin(m, m.mk_family_id("bv"), ctx), - m_replace(mk_default_expr_replacer(m)), + m_replace(m), m_bv(m) {} @@ -48,7 +48,7 @@ namespace qe { virtual void subst(contains_app& x, rational const& vl, expr_ref& fml, expr_ref* def) { app_ref c(m_bv.mk_numeral(vl, m_bv.get_bv_size(x.x())), m); - m_replace->apply_substitution(x.x(), c, 0, fml); + m_replace.apply_substitution(x.x(), c, fml); if (def) { *def = m_bv.mk_numeral(vl, m_bv.get_bv_size(x.x())); } diff --git a/src/muz_qe/qe_datatype_plugin.cpp b/src/muz_qe/qe_datatype_plugin.cpp index 0b51f26af..9b77de42a 100644 --- a/src/muz_qe/qe_datatype_plugin.cpp +++ b/src/muz_qe/qe_datatype_plugin.cpp @@ -95,7 +95,7 @@ #include "qe.h" #include "datatype_decl_plugin.h" -#include "expr_replacer.h" +#include "expr_safe_replace.h" #include "obj_pair_hashtable.h" #include "for_each_expr.h" #include "ast_pp.h" @@ -415,7 +415,7 @@ namespace qe { typedef obj_pair_map subst_map; datatype_util m_datatype_util; - scoped_ptr m_replace; + expr_safe_replace m_replace; eqs_cache m_eqs_cache; subst_map m_subst_cache; ast_ref_vector m_trail; @@ -424,7 +424,7 @@ namespace qe { datatype_plugin(i_solver_context& ctx, ast_manager& m) : qe_solver_plugin(m, m.mk_family_id("datatype"), ctx), m_datatype_util(m), - m_replace(mk_default_expr_replacer(m)), + m_replace(m), m_trail(m) { } @@ -518,7 +518,7 @@ namespace qe { subst_clos* sub = 0; if (m_subst_cache.find(x.x(), c, sub)) { - m_replace->apply_substitution(x.x(), sub->first, 0, fml); + m_replace.apply_substitution(x.x(), sub->first, fml); add_def(sub->first, def); for (unsigned i = 0; i < sub->second.size(); ++i) { m_ctx.add_var(sub->second[i]); @@ -541,7 +541,7 @@ namespace qe { m_trail.push_back(t); add_def(t, def); - m_replace->apply_substitution(x.x(), t, 0, fml); + m_replace.apply_substitution(x.x(), t, fml); sub->first = t; m_subst_cache.insert(x.x(), c, sub); } @@ -673,7 +673,7 @@ namespace qe { fml = m.mk_and(is_c, fml); app_ref fresh_x(m.mk_fresh_const("x", s), m); m_ctx.add_var(fresh_x); - m_replace->apply_substitution(x, fresh_x, 0, fml); + m_replace.apply_substitution(x, fresh_x, fml); add_def(fresh_x, def); TRACE("qe", tout << "Add recognizer " << mk_pp(is_c, m) << "\n";); return; @@ -697,33 +697,33 @@ namespace qe { for (unsigned i = 0; i < eqs.num_recognizers(); ++i) { app* rec = eqs.recognizer(i); if (rec->get_decl() == r) { - m_replace->apply_substitution(rec, m.mk_true(), fml); + m_replace.apply_substitution(rec, m.mk_true(), fml); } else { - m_replace->apply_substitution(rec, m.mk_false(), fml); + m_replace.apply_substitution(rec, m.mk_false(), fml); } } for (unsigned i = 0; i < eqs.num_unsat(); ++i) { - m_replace->apply_substitution(eqs.unsat_atom(i), m.mk_false(), fml); + m_replace.apply_substitution(eqs.unsat_atom(i), m.mk_false(), fml); } if (idx < eqs.num_eqs()) { expr* t = eqs.eq(idx); expr* c = eqs.eq_cond(idx); add_def(t, def); - m_replace->apply_substitution(x, t, fml); + m_replace.apply_substitution(x, t, fml); if (!m.is_true(c)) { fml = m.mk_and(c, fml); } } else { for (unsigned i = 0; i < eqs.num_eqs(); ++i) { - m_replace->apply_substitution(eqs.eq_atom(i), m.mk_false(), fml); + m_replace.apply_substitution(eqs.eq_atom(i), m.mk_false(), fml); } for (unsigned i = 0; i < eqs.num_neqs(); ++i) { - m_replace->apply_substitution(eqs.neq_atom(i), m.mk_false(), fml); + m_replace.apply_substitution(eqs.neq_atom(i), m.mk_false(), fml); } if (def) { sort* s = m.get_sort(x); diff --git a/src/muz_qe/qe_dl_plugin.cpp b/src/muz_qe/qe_dl_plugin.cpp index 61466795b..a93301b4f 100644 --- a/src/muz_qe/qe_dl_plugin.cpp +++ b/src/muz_qe/qe_dl_plugin.cpp @@ -1,6 +1,6 @@ #include "qe.h" -#include "expr_replacer.h" +#include "expr_safe_replace.h" #include "dl_decl_plugin.h" #include "obj_pair_hashtable.h" #include "ast_pp.h" @@ -35,7 +35,7 @@ namespace qe { class dl_plugin : public qe_solver_plugin { typedef obj_pair_map eqs_cache; - scoped_ptr m_replace; + expr_safe_replace m_replace; datalog::dl_decl_util m_util; expr_ref_vector m_trail; eqs_cache m_eqs_cache; @@ -44,7 +44,7 @@ namespace qe { public: dl_plugin(i_solver_context& ctx, ast_manager& m) : qe_solver_plugin(m, m.mk_family_id("datalog_relation"), ctx), - m_replace(mk_default_expr_replacer(m)), + m_replace(m), m_util(m), m_trail(m) { @@ -140,7 +140,7 @@ namespace qe { void subst_small_domain(contains_app & x,eq_atoms& eqs, unsigned v,expr_ref & fml) { expr_ref vl(m_util.mk_numeral(v, m.get_sort(x.x())), m); - m_replace->apply_substitution(x.x(), vl, fml); + m_replace.apply_substitution(x.x(), vl, fml); } // assumes that all disequalities can be satisfied. @@ -148,15 +148,15 @@ namespace qe { SASSERT(w <= eqs.num_eqs()); if (w < eqs.num_eqs()) { expr* e = eqs.eq(w); - m_replace->apply_substitution(x.x(), e, fml); + m_replace.apply_substitution(x.x(), e, fml); } else { for (unsigned i = 0; i < eqs.num_eqs(); ++i) { - m_replace->apply_substitution(eqs.eq_atom(i), m.mk_false(), fml); + m_replace.apply_substitution(eqs.eq_atom(i), m.mk_false(), fml); } for (unsigned i = 0; i < eqs.num_neqs(); ++i) { - m_replace->apply_substitution(eqs.neq_atom(i), m.mk_true(), fml); + m_replace.apply_substitution(eqs.neq_atom(i), m.mk_true(), fml); } } } diff --git a/src/muz_qe/rel_context.cpp b/src/muz_qe/rel_context.cpp index 7aade28e2..4ebcbf2fd 100644 --- a/src/muz_qe/rel_context.cpp +++ b/src/muz_qe/rel_context.cpp @@ -75,7 +75,8 @@ namespace datalog { }; rel_context::rel_context(context& ctx) - : m_context(ctx), + : engine_base(ctx.get_manager(), "datalog"), + m_context(ctx), m(ctx.get_manager()), m_rmanager(ctx), m_answer(m), diff --git a/src/muz_qe/rel_context.h b/src/muz_qe/rel_context.h index 7b4ee551c..057d1c15f 100644 --- a/src/muz_qe/rel_context.h +++ b/src/muz_qe/rel_context.h @@ -30,7 +30,7 @@ namespace datalog { class context; typedef vector > fact_vector; - class rel_context { + class rel_context : public engine_base { context& m_context; ast_manager& m; relation_manager m_rmanager; @@ -59,11 +59,11 @@ namespace datalog { context& get_context() const { return m_context; } relation_base & get_relation(func_decl * pred); relation_base * try_get_relation(func_decl * pred) const; - expr_ref get_last_answer() { return m_answer; } + virtual expr_ref get_answer() { return m_answer; } bool output_profile() const; - lbool query(expr* q); + virtual lbool query(expr* q); lbool query(unsigned num_rels, func_decl * const* rels); void set_predicate_representation(func_decl * pred, unsigned relation_name_cnt, @@ -73,6 +73,9 @@ namespace datalog { void set_cancel(bool f); + virtual void cancel() { set_cancel(true); } + virtual void cleanup() { set_cancel(false);} + /** \brief Restrict the set of used predicates to \c res. diff --git a/src/muz_qe/tab_context.cpp b/src/muz_qe/tab_context.cpp index 653f5f188..4f4c14cc7 100644 --- a/src/muz_qe/tab_context.cpp +++ b/src/muz_qe/tab_context.cpp @@ -1657,6 +1657,7 @@ namespace datalog { }; tab::tab(context& ctx): + datalog::engine_base(ctx.get_manager(),"tabulation"), m_imp(alloc(imp, ctx)) { } tab::~tab() { diff --git a/src/muz_qe/tab_context.h b/src/muz_qe/tab_context.h index f0a2eefed..c23ccb7d3 100644 --- a/src/muz_qe/tab_context.h +++ b/src/muz_qe/tab_context.h @@ -22,23 +22,24 @@ Revision History: #include "ast.h" #include "lbool.h" #include "statistics.h" +#include "dl_util.h" namespace datalog { class context; - class tab { + class tab : public engine_base { class imp; imp* m_imp; public: tab(context& ctx); ~tab(); - lbool query(expr* query); - void cancel(); - void cleanup(); - void reset_statistics(); - void collect_statistics(statistics& st) const; - void display_certificate(std::ostream& out) const; - expr_ref get_answer(); + virtual lbool query(expr* query); + virtual void cancel(); + virtual void cleanup(); + virtual void reset_statistics(); + virtual void collect_statistics(statistics& st) const; + virtual void display_certificate(std::ostream& out) const; + virtual expr_ref get_answer(); }; }; diff --git a/src/shell/datalog_frontend.cpp b/src/shell/datalog_frontend.cpp index efcab14ea..56f60bfa0 100644 --- a/src/shell/datalog_frontend.cpp +++ b/src/shell/datalog_frontend.cpp @@ -75,7 +75,7 @@ static void display_statistics( out << "--------------\n"; out << "instructions \n"; - code.display(ctx.get_rel_context(), out); + code.display(*ctx.get_rel_context(), out); out << "--------------\n"; out << "big relations \n"; @@ -83,7 +83,7 @@ static void display_statistics( } out << "--------------\n"; out << "relation sizes\n"; - ctx.get_rel_context().get_rmanager().display_relation_sizes(out); + ctx.get_rel_context()->get_rmanager().display_relation_sizes(out); if (verbose) { out << "--------------\n"; @@ -125,7 +125,7 @@ unsigned read_datalog(char const * file) { params.set_sym("engine", symbol("datalog")); datalog::context ctx(m, s_params, params); - datalog::relation_manager & rmgr = ctx.get_rel_context().get_rmanager(); + datalog::relation_manager & rmgr = ctx.get_rel_context()->get_rmanager(); datalog::relation_plugin & inner_plg = *rmgr.get_relation_plugin(symbol("tr_hashtable")); SASSERT(&inner_plg); rmgr.register_plugin(alloc(datalog::finite_product_relation_plugin, inner_plg, rmgr)); @@ -187,7 +187,7 @@ unsigned read_datalog(char const * file) { datalog::compiler::compile(ctx, ctx.get_rules(), rules_code, termination_code); - TRACE("dl_compiler", rules_code.display(ctx.get_rel_context(), tout);); + TRACE("dl_compiler", rules_code.display(*ctx.get_rel_context(), tout);); rules_code.make_annotations(ex_ctx); @@ -227,10 +227,10 @@ unsigned read_datalog(char const * file) { TRACE("dl_compiler", ctx.display(tout); - rules_code.display(ctx.get_rel_context(), tout);); + rules_code.display(*ctx.get_rel_context(), tout);); if (ctx.get_params().output_tuples()) { - ctx.get_rel_context().display_output_facts(ctx.get_rules(), std::cout); + ctx.get_rel_context()->display_output_facts(ctx.get_rules(), std::cout); } display_statistics( diff --git a/src/smt/theory_array_base.cpp b/src/smt/theory_array_base.cpp index c2c50567f..3f96a1d62 100644 --- a/src/smt/theory_array_base.cpp +++ b/src/smt/theory_array_base.cpp @@ -688,7 +688,7 @@ namespace smt { } } } - + void theory_array_base::propagate_select_to_store_parents(enode * r, enode * sel, svector & todo) { SASSERT(r->get_root() == r); SASSERT(is_select(sel)); @@ -880,7 +880,7 @@ namespace smt { } else { theory_var r = mg_find(v); - void * else_val = m_else_values[r]; + void * else_val = m_else_values[r]; // DISABLED. It seems wrong, since different nodes can share the same // else_val according to the mg class. // SASSERT(else_val == 0 || get_context().is_relevant(UNTAG(app*, else_val)));