From 26f4d3be202606ff0189aefc103de187caf06d5d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 23 Mar 2013 14:11:54 -0700 Subject: [PATCH] significant update to Horn routines: add module hnf to extract Horn normal form (removed from rule_manager). Associate proof objects with rules to track (all) rewrites, so that proof traces can be tracked back to original rules after transformations Signed-off-by: Nikolaj Bjorner --- src/api/z3_api.h | 2 +- src/ast/rewriter/quant_hoist.cpp | 30 +- src/ast/rewriter/quant_hoist.h | 2 +- src/muz_qe/dl_base.cpp | 2 +- src/muz_qe/dl_bmc_engine.cpp | 40 ++- src/muz_qe/dl_bmc_engine.h | 1 - src/muz_qe/dl_cmds.cpp | 4 +- src/muz_qe/dl_context.cpp | 32 +- src/muz_qe/dl_context.h | 13 +- src/muz_qe/dl_mk_array_blast.cpp | 18 +- src/muz_qe/dl_mk_array_blast.h | 3 +- src/muz_qe/dl_mk_bit_blast.cpp | 119 ++++++- src/muz_qe/dl_mk_bit_blast.h | 2 +- src/muz_qe/dl_mk_coalesce.cpp | 20 +- src/muz_qe/dl_mk_coalesce.h | 3 +- src/muz_qe/dl_mk_coi_filter.cpp | 3 +- src/muz_qe/dl_mk_coi_filter.h | 3 +- src/muz_qe/dl_mk_explanations.cpp | 4 +- src/muz_qe/dl_mk_explanations.h | 2 +- src/muz_qe/dl_mk_extract_quantifiers.cpp | 12 +- src/muz_qe/dl_mk_extract_quantifiers.h | 2 +- src/muz_qe/dl_mk_filter_rules.cpp | 6 +- src/muz_qe/dl_mk_filter_rules.h | 2 +- src/muz_qe/dl_mk_interp_tail_simplifier.cpp | 7 +- src/muz_qe/dl_mk_interp_tail_simplifier.h | 2 +- src/muz_qe/dl_mk_karr_invariants.cpp | 5 +- src/muz_qe/dl_mk_karr_invariants.h | 2 +- src/muz_qe/dl_mk_magic_sets.cpp | 4 +- src/muz_qe/dl_mk_magic_sets.h | 2 +- src/muz_qe/dl_mk_partial_equiv.cpp | 4 +- src/muz_qe/dl_mk_partial_equiv.h | 2 +- src/muz_qe/dl_mk_rule_inliner.cpp | 14 +- src/muz_qe/dl_mk_rule_inliner.h | 4 +- src/muz_qe/dl_mk_similarity_compressor.cpp | 4 +- src/muz_qe/dl_mk_similarity_compressor.h | 2 +- src/muz_qe/dl_mk_simple_joins.cpp | 9 +- src/muz_qe/dl_mk_simple_joins.h | 2 +- src/muz_qe/dl_mk_slice.cpp | 15 +- src/muz_qe/dl_mk_slice.h | 2 +- src/muz_qe/dl_mk_subsumption_checker.cpp | 13 +- src/muz_qe/dl_mk_subsumption_checker.h | 2 +- src/muz_qe/dl_mk_unbound_compressor.cpp | 5 +- src/muz_qe/dl_mk_unbound_compressor.h | 2 +- src/muz_qe/dl_mk_unfold.cpp | 15 +- src/muz_qe/dl_mk_unfold.h | 3 +- src/muz_qe/dl_rule.cpp | 333 ++++++++++---------- src/muz_qe/dl_rule.h | 45 ++- src/muz_qe/dl_rule_transformer.cpp | 4 +- src/muz_qe/dl_rule_transformer.h | 6 +- src/muz_qe/dl_util.cpp | 38 +++ src/muz_qe/dl_util.h | 3 + src/muz_qe/equiv_proof_converter.cpp | 18 +- src/muz_qe/horn_tactic.cpp | 14 +- src/muz_qe/pdr_context.cpp | 49 ++- src/muz_qe/pdr_context.h | 7 +- src/muz_qe/pdr_dl_interface.cpp | 13 +- src/muz_qe/pdr_generalizers.cpp | 6 +- src/muz_qe/qe_lite.cpp | 8 +- src/muz_qe/tab_context.cpp | 13 +- src/util/vector.h | 17 - 60 files changed, 591 insertions(+), 428 deletions(-) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index ea3b05e40..6d59cf650 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -701,7 +701,7 @@ typedef enum over Boolean connectives 'and' and 'or'. - - Z3_OP_PR_NFF_NEG: Proof for a (negative) NNF step. Examples: + - Z3_OP_PR_NNF_NEG: Proof for a (negative) NNF step. Examples: \nicebox{ T1: (not s_1) ~ r_1 ... diff --git a/src/ast/rewriter/quant_hoist.cpp b/src/ast/rewriter/quant_hoist.cpp index 9e8db0d11..57b693aca 100644 --- a/src/ast/rewriter/quant_hoist.cpp +++ b/src/ast/rewriter/quant_hoist.cpp @@ -80,7 +80,7 @@ public: instantiate(m, q, exprs, result); } - unsigned pull_quantifier(bool is_forall, expr_ref& fml, svector* names) { + unsigned pull_quantifier(bool is_forall, expr_ref& fml, ptr_vector* sorts, svector* names) { unsigned index = var_counter().get_next_var(fml); while (is_quantifier(fml) && (is_forall == to_quantifier(fml)->is_forall())) { quantifier* q = to_quantifier(fml); @@ -88,6 +88,9 @@ public: if (names) { names->append(q->get_num_decls(), q->get_decl_names()); } + if (sorts) { + sorts->append(q->get_num_decls(), q->get_decl_sorts()); + } fml = q->get_expr(); } if (!has_quantifiers(fml)) { @@ -100,12 +103,29 @@ public: } // replace vars by de-bruijn indices expr_safe_replace rep(m); + svector bound_names; + ptr_vector bound_sorts; for (unsigned i = 0; i < vars.size(); ++i) { app* v = vars[i].get(); if (names) { - names->push_back(v->get_decl()->get_name()); + bound_names.push_back(v->get_decl()->get_name()); } - rep.insert(v, m.mk_var(index++,m.get_sort(v))); + if (sorts) { + bound_sorts.push_back(m.get_sort(v)); + } + rep.insert(v, m.mk_var(index++, m.get_sort(v))); + } + if (names && !bound_names.empty()) { + bound_names.reverse(); + bound_names.append(*names); + names->reset(); + names->append(bound_names); + } + if (sorts && !bound_sorts.empty()) { + bound_sorts.reverse(); + bound_sorts.append(*sorts); + sorts->reset(); + sorts->append(bound_sorts); } rep(fml); return index; @@ -270,6 +290,6 @@ void quantifier_hoister::pull_quantifier(bool is_forall, expr_ref& fml, app_ref_ m_impl->pull_quantifier(is_forall, fml, vars); } -unsigned quantifier_hoister::pull_quantifier(bool is_forall, expr_ref& fml, svector* names) { - return m_impl->pull_quantifier(is_forall, fml, names); +unsigned quantifier_hoister::pull_quantifier(bool is_forall, expr_ref& fml, ptr_vector* sorts, svector* names) { + return m_impl->pull_quantifier(is_forall, fml, sorts, names); } diff --git a/src/ast/rewriter/quant_hoist.h b/src/ast/rewriter/quant_hoist.h index 70a79a0e2..dc586d437 100644 --- a/src/ast/rewriter/quant_hoist.h +++ b/src/ast/rewriter/quant_hoist.h @@ -66,7 +66,7 @@ public: Return index of maximal variable. */ - unsigned pull_quantifier(bool is_forall, expr_ref& fml, svector* names); + unsigned pull_quantifier(bool is_forall, expr_ref& fml, ptr_vector* sorts, svector* names); }; #endif diff --git a/src/muz_qe/dl_base.cpp b/src/muz_qe/dl_base.cpp index dd817754f..0f250d76c 100644 --- a/src/muz_qe/dl_base.cpp +++ b/src/muz_qe/dl_base.cpp @@ -233,7 +233,7 @@ namespace datalog { table_fact row; for(; it!=iend; ++it) { it->get_fact(row); - to_remove.append(row); + to_remove.push_back(row); } remove_facts(to_remove.size(), to_remove.c_ptr()); } diff --git a/src/muz_qe/dl_bmc_engine.cpp b/src/muz_qe/dl_bmc_engine.cpp index 200338b86..2961b3f54 100644 --- a/src/muz_qe/dl_bmc_engine.cpp +++ b/src/muz_qe/dl_bmc_engine.cpp @@ -307,7 +307,7 @@ namespace datalog { r1->to_formula(concl); scoped_proof _sp(m); - proof* p = m.mk_asserted(fml); + proof* p = r->get_proof(); proof* premises[2] = { pr, p }; positions.push_back(std::make_pair(0, 1)); @@ -320,7 +320,7 @@ namespace datalog { else { r2->to_formula(concl); scoped_proof _sp(m); - proof* p = m.mk_asserted(fml); + proof* p = r->get_proof(); if (sub.empty()) { pr = p; } @@ -340,7 +340,7 @@ namespace datalog { pred = r->get_decl(0); } scoped_proof _sp(m); - apply(m, b.m_pc.get(), pr); + apply(m, b.m_ctx.get_proof_converter().get(), pr); b.m_answer = pr; return l_true; } @@ -474,6 +474,9 @@ namespace datalog { } proof_ref get_proof(model_ref& md, func_decl* pred, app* prop, unsigned level) { + if (b.m_cancel) { + return proof_ref(0, m); + } TRACE("bmc", tout << "Predicate: " << pred->get_name() << "\n";); expr_ref prop_r(m), prop_v(m), fml(m), prop_body(m), tmp(m), body(m); @@ -497,7 +500,7 @@ namespace datalog { SASSERT(r); r->to_formula(fml); IF_VERBOSE(1, verbose_stream() << mk_pp(fml, m) << "\n";); - prs.push_back(m.mk_asserted(fml)); + prs.push_back(r->get_proof()); unsigned sz = r->get_uninterpreted_tail_size(); ptr_vector rule_vars; @@ -536,8 +539,9 @@ namespace datalog { model_ref md; b.m_solver.get_model(md); IF_VERBOSE(2, model_smt2_pp(verbose_stream(), m, *md, 0);); - proof_ref pr = get_proof(md, b.m_query_pred, to_app(level_query), level); - apply(m, b.m_pc.get(), pr); + proof_ref pr(m); + pr = get_proof(md, b.m_query_pred, to_app(level_query), level); + apply(m, b.m_ctx.get_proof_converter().get(), pr); b.m_answer = pr; } @@ -1034,7 +1038,7 @@ namespace datalog { var_subst vs(m, false); mk_subst(*rules[i], path, trace, sub); rules[i]->to_formula(fml); - prs.push_back(m.mk_asserted(fml)); + prs.push_back(rules[i]->get_proof()); unsigned sz = trace->get_num_args(); if (sub.empty() && sz == 0) { pr = prs[0].get(); @@ -1112,7 +1116,6 @@ namespace datalog { } void mk_answer(model_ref& md, expr_ref& trace, expr_ref& path) { - proof_ref pr(m); IF_VERBOSE(2, model_smt2_pp(verbose_stream(), m, *md, 0);); md->eval(trace, trace); md->eval(path, path); @@ -1120,7 +1123,11 @@ namespace datalog { for (unsigned i = 0; i < b.m_solver.size(); ++i) { verbose_stream() << mk_pp(b.m_solver.get_formulas()[i], m) << "\n"; }); - b.m_answer = get_proof(md, to_app(trace), to_app(path)); + scoped_proof _sp(m); + proof_ref pr(m); + pr = get_proof(md, to_app(trace), to_app(path)); + apply(m, b.m_ctx.get_proof_converter().get(), pr); + b.m_answer = pr; } }; @@ -1155,6 +1162,9 @@ namespace datalog { private: void get_model(unsigned level) { + if (b.m_cancel) { + return; + } rule_manager& rm = b.m_ctx.get_rule_manager(); expr_ref level_query = mk_level_predicate(b.m_query_pred, level); model_ref md; @@ -1212,7 +1222,7 @@ namespace datalog { r1->to_formula(concl); scoped_proof _sp(m); - proof* p = m.mk_asserted(fml); + proof* p = r->get_proof(); proof* premises[2] = { pr, p }; positions.push_back(std::make_pair(0, 1)); @@ -1225,7 +1235,7 @@ namespace datalog { else { r2->to_formula(concl); scoped_proof _sp(m); - proof* p = m.mk_asserted(fml); + proof* p = r->get_proof(); if (sub.empty()) { pr = p; } @@ -1245,7 +1255,7 @@ namespace datalog { pred = r->get_decl(0); } scoped_proof _sp(m); - apply(m, b.m_pc.get(), pr); + apply(m, b.m_ctx.get_proof_converter().get(), pr); b.m_answer = pr; } @@ -1409,6 +1419,7 @@ namespace datalog { m_ctx.ensure_opened(); m_rules.reset(); + datalog::rule_manager& rule_manager = m_ctx.get_rule_manager(); datalog::rule_set old_rules(m_ctx.get_rules()); datalog::rule_ref_vector query_rules(rule_manager); @@ -1417,11 +1428,8 @@ namespace datalog { m_ctx.add_rules(query_rules); expr_ref bg_assertion = m_ctx.get_background_assertion(); - model_converter_ref mc = datalog::mk_skip_model_converter(); - m_pc = datalog::mk_skip_proof_converter(); + m_ctx.set_output_predicate(m_query_pred); - m_ctx.set_model_converter(mc); - m_ctx.set_proof_converter(m_pc); m_ctx.apply_default_transformation(); if (m_ctx.get_params().slice()) { diff --git a/src/muz_qe/dl_bmc_engine.h b/src/muz_qe/dl_bmc_engine.h index 06901a160..5911f5f72 100644 --- a/src/muz_qe/dl_bmc_engine.h +++ b/src/muz_qe/dl_bmc_engine.h @@ -39,7 +39,6 @@ namespace datalog { func_decl_ref m_query_pred; expr_ref m_answer; volatile bool m_cancel; - proof_converter_ref m_pc; void checkpoint(); diff --git a/src/muz_qe/dl_cmds.cpp b/src/muz_qe/dl_cmds.cpp index c88e7346e..d49a8a671 100644 --- a/src/muz_qe/dl_cmds.cpp +++ b/src/muz_qe/dl_cmds.cpp @@ -262,8 +262,10 @@ public: case datalog::OK: break; + default: - UNREACHABLE(); + // exception was raised. + break; } break; } diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp index 839aa93f9..7d9fe8d7e 100644 --- a/src/muz_qe/dl_context.cpp +++ b/src/muz_qe/dl_context.cpp @@ -231,6 +231,7 @@ namespace datalog { m_rule_set(*this), m_rule_fmls(m), m_background(m), + m_mc(0), m_closed(false), m_saturation_was_run(false), m_last_answer(m), @@ -474,8 +475,11 @@ namespace datalog { void context::flush_add_rules() { datalog::rule_manager& rm = get_rule_manager(); datalog::rule_ref_vector rules(rm); + scoped_proof_mode _scp(m, generate_proof_trace()?PGM_FINE:PGM_DISABLED); for (unsigned i = 0; i < m_rule_fmls.size(); ++i) { - rm.mk_rule(m_rule_fmls[i].get(), rules, m_rule_names[i]); + expr* fml = m_rule_fmls[i].get(); + proof* p = generate_proof_trace()?m.mk_asserted(fml):0; + rm.mk_rule(fml, p, rules, m_rule_names[i]); } add_rules(rules); m_rule_fmls.reset(); @@ -489,7 +493,11 @@ namespace datalog { void context::update_rule(expr* rl, symbol const& name) { datalog::rule_manager& rm = get_rule_manager(); datalog::rule_ref_vector rules(rm); - rm.mk_rule(rl, rules, name); + proof* p = 0; + if (generate_proof_trace()) { + p = m.mk_asserted(rl); + } + rm.mk_rule(rl, p, rules, name); if (rules.size() != 1) { std::stringstream strm; strm << "Rule " << name << " has a non-trivial body. It cannot be modified"; @@ -683,7 +691,7 @@ namespace datalog { todo.push_back(e2); } else if (is_quantifier(e)) { - todo.append(to_quantifier(e)->get_expr()); + todo.push_back(to_quantifier(e)->get_expr()); } else if ((m.is_eq(e, e1, e2) || m.is_iff(e, e1, e2)) && m.is_true(e1)) { @@ -737,6 +745,9 @@ namespace datalog { UNREACHABLE(); break; } + if (generate_proof_trace() && !r->get_proof()) { + m_rule_manager.mk_rule_asserted_proof(*r.get()); + } } void context::add_rule(rule_ref& r) { @@ -847,7 +858,7 @@ namespace datalog { void context::transform_rules(rule_transformer& transf) { SASSERT(m_closed); //we must finish adding rules before we start transforming them TRACE("dl", display_rules(tout);); - if (transf(m_rule_set, m_mc, m_pc)) { + if (transf(m_rule_set, m_mc)) { //we have already ensured the negation is stratified and transformations //should not break the stratification m_rule_set.ensure_closed(); @@ -887,9 +898,9 @@ namespace datalog { m_transf.register_plugin(alloc(datalog::mk_rule_inliner, *this, 34890)); m_transf.register_plugin(alloc(datalog::mk_subsumption_checker, *this, 34880)); - 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)); + m_transf.register_plugin(alloc(datalog::mk_bit_blast, *this, 34870)); + m_transf.register_plugin(alloc(datalog::mk_array_blast, *this, 34860)); + m_transf.register_plugin(alloc(datalog::mk_karr_invariants, *this, 34850)); transform_rules(m_transf); } @@ -1035,6 +1046,8 @@ namespace datalog { } void context::new_query() { + m_mc = mk_skip_model_converter(); + flush_add_rules(); m_last_status = OK; m_last_answer = 0; @@ -1146,6 +1159,7 @@ namespace datalog { switch(get_engine()) { case DATALOG_ENGINE: return false; + case PDR_ENGINE: case QPDR_ENGINE: ensure_pdr(); m_pdr->display_certificate(out); @@ -1239,7 +1253,7 @@ namespace datalog { ptr_vector sorts; get_free_vars(m_rule_fmls[i].get(), sorts); if (!sorts.empty()) { - rm.mk_rule(m_rule_fmls[i].get(), rule_refs, m_rule_names[i]); + rm.mk_rule(m_rule_fmls[i].get(), 0, rule_refs, m_rule_names[i]); m_rule_fmls[i] = m_rule_fmls.back(); m_rule_names[i] = m_rule_names.back(); m_rule_fmls.pop_back(); @@ -1256,7 +1270,7 @@ namespace datalog { } for (unsigned i = 0; i < m_rule_fmls.size(); ++i) { rules.push_back(m_rule_fmls[i].get()); - names.push_back(m_rule_names[i]); + names.push_back(m_rule_names[i]); } } diff --git a/src/muz_qe/dl_context.h b/src/muz_qe/dl_context.h index f9a1f1737..778cccc0c 100644 --- a/src/muz_qe/dl_context.h +++ b/src/muz_qe/dl_context.h @@ -42,7 +42,6 @@ Revision History: #include"params.h" #include"trail.h" #include"model_converter.h" -#include"proof_converter.h" #include"model2expr.h" #include"smt_params.h" #include"dl_rule_transformer.h" @@ -142,6 +141,7 @@ namespace datalog { var_subst & get_var_subst() { return m_var_subst; } dl_decl_util & get_decl_util() { return m_decl_util; } + bool generate_proof_trace() const { return m_params.generate_proof_trace(); } bool output_profile() const { return m_params.output_profile(); } bool fix_unbound_vars() const { return m_params.fix_unbound_vars(); } symbol default_table() const { return m_params.default_table(); } @@ -315,14 +315,15 @@ namespace datalog { void reopen(); void ensure_opened(); - void set_model_converter(model_converter_ref& mc) { m_mc = mc; } - void set_proof_converter(proof_converter_ref& pc) { m_pc = pc; } + model_converter_ref& get_model_converter() { return m_mc; } + proof_converter_ref& get_proof_converter() { return m_pc; } + void add_proof_converter(proof_converter* pc) { m_pc = concat(m_pc.get(), pc); } - void transform_rules(); // model_converter_ref& mc, proof_converter_ref& pc); - void transform_rules(rule_transformer& transf); // , model_converter_ref& mc, proof_converter_ref& pc); + void transform_rules(); + void transform_rules(rule_transformer& transf); void replace_rules(rule_set & rs); - void apply_default_transformation(); // model_converter_ref& mc, proof_converter_ref& pc); + void apply_default_transformation(); void collect_params(param_descrs& r); diff --git a/src/muz_qe/dl_mk_array_blast.cpp b/src/muz_qe/dl_mk_array_blast.cpp index b22fdf7ef..537b0b5ac 100644 --- a/src/muz_qe/dl_mk_array_blast.cpp +++ b/src/muz_qe/dl_mk_array_blast.cpp @@ -197,25 +197,18 @@ namespace datalog { } fml2 = m.mk_implies(body, head); - rm.mk_rule(fml2, new_rules, r.name()); + proof_ref p(m); + rm.mk_rule(fml2, p, new_rules, r.name()); SASSERT(new_rules.size() == 1); TRACE("dl", new_rules[0]->display(m_ctx, tout << "new rule\n");); rules.add_rule(new_rules[0].get()); - if (m_pc) { - new_rules[0]->to_formula(fml2); - m_pc->insert(fml1, fml2); - } + rm.mk_rule_rewrite_proof(r, *new_rules[0].get()); return true; } - rule_set * mk_array_blast::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) { - ref epc; - if (pc) { - epc = alloc(equiv_proof_converter, m); - } - m_pc = epc.get(); + rule_set * mk_array_blast::operator()(rule_set const & source, model_converter_ref& mc) { rule_set* rules = alloc(rule_set, m_ctx); rule_set::iterator it = source.begin(), end = source.end(); @@ -227,9 +220,6 @@ namespace datalog { dealloc(rules); rules = 0; } - if (pc) { - pc = concat(pc.get(), epc.get()); - } return rules; } diff --git a/src/muz_qe/dl_mk_array_blast.h b/src/muz_qe/dl_mk_array_blast.h index c0bb39da0..94eb64601 100644 --- a/src/muz_qe/dl_mk_array_blast.h +++ b/src/muz_qe/dl_mk_array_blast.h @@ -37,7 +37,6 @@ namespace datalog { rule_manager& rm; params_ref m_params; th_rewriter m_rewriter; - equiv_proof_converter* m_pc; typedef obj_map defs_t; @@ -55,7 +54,7 @@ namespace datalog { virtual ~mk_array_blast(); - rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc); + rule_set * operator()(rule_set const & source, model_converter_ref& mc); }; diff --git a/src/muz_qe/dl_mk_bit_blast.cpp b/src/muz_qe/dl_mk_bit_blast.cpp index 1fa93a0ca..1e984f254 100644 --- a/src/muz_qe/dl_mk_bit_blast.cpp +++ b/src/muz_qe/dl_mk_bit_blast.cpp @@ -21,7 +21,8 @@ Revision History: #include "bit_blaster_rewriter.h" #include "rewriter_def.h" #include "ast_pp.h" - +#include "expr_safe_replace.h" +#include "filter_model_converter.h" namespace datalog { @@ -35,6 +36,73 @@ namespace datalog { // P(bv(x,y)) :- P_bv(x,y) // Query + // this model converter should be composed with a filter converter + // that gets rid of the new functions. + class bit_blast_model_converter : public model_converter { + ast_manager& m; + bv_util m_bv; + func_decl_ref_vector m_old_funcs; + func_decl_ref_vector m_new_funcs; + public: + bit_blast_model_converter(ast_manager& m): + m(m), + m_bv(m), + m_old_funcs(m), + m_new_funcs(m) {} + + void insert(func_decl* old_f, func_decl* new_f) { + m_old_funcs.push_back(old_f); + m_new_funcs.push_back(new_f); + } + + virtual model_converter * translate(ast_translation & translator) { + return alloc(bit_blast_model_converter, m); + } + + virtual void operator()(model_ref & model) { + for (unsigned i = 0; i < m_new_funcs.size(); ++i) { + func_decl* p = m_new_funcs[i].get(); + func_decl* q = m_old_funcs[i].get(); + func_interp* f = model->get_func_interp(p); + expr_ref body(m); + unsigned arity_p = p->get_arity(); + unsigned arity_q = q->get_arity(); + SASSERT(0 < arity_p); + model->register_decl(p, f); + func_interp* g = alloc(func_interp, m, arity_q); + + if (f) { + body = f->get_interp(); + SASSERT(!f->is_partial()); + SASSERT(body); + } + else { + body = m.mk_false(); + } + unsigned idx = 0; + expr_ref arg(m), proj(m); + expr_safe_replace sub(m); + for (unsigned j = 0; j < arity_q; ++j) { + sort* s = q->get_domain(j); + arg = m.mk_var(j, s); + if (m_bv.is_bv_sort(s)) { + expr* args[1] = { arg }; + unsigned sz = m_bv.get_bv_size(s); + for (unsigned k = 0; k < sz; ++k) { + proj = m.mk_app(m_bv.get_family_id(), OP_BIT2BOOL, 1, args); + sub.insert(m.mk_var(idx++, m.mk_bool_sort()), proj); + } + } + else { + sub.insert(m.mk_var(idx++, s), arg); + } + } + sub(body); + g->set_else(body); + model->register_decl(q, g); + } + } + }; class expand_mkbv_cfg : public default_rewriter_cfg { @@ -43,7 +111,8 @@ namespace datalog { ast_manager& m; bv_util m_util; expr_ref_vector m_args, m_f_vars, m_g_vars; - func_decl_ref_vector m_pinned; + func_decl_ref_vector m_old_funcs; + func_decl_ref_vector m_new_funcs; obj_map m_pred2blast; @@ -57,10 +126,14 @@ namespace datalog { m_args(m), m_f_vars(m), m_g_vars(m), - m_pinned(m) + m_old_funcs(m), + m_new_funcs(m) {} ~expand_mkbv_cfg() {} + + func_decl_ref_vector const& old_funcs() const { return m_old_funcs; } + func_decl_ref_vector const& new_funcs() const { return m_new_funcs; } br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { rule_manager& rm = m_context.get_rule_manager(); @@ -105,13 +178,18 @@ namespace datalog { domain.push_back(m.get_sort(m_args[i].get())); } g = m_context.mk_fresh_head_predicate(f->get_name(), symbol("bv"), m_args.size(), domain.c_ptr(), f); - m_pinned.push_back(g); + m_old_funcs.push_back(f); + m_new_funcs.push_back(g); m_pred2blast.insert(f, g); // Create rule f(mk_mkbv(args)) :- g(args) fml = m.mk_implies(m.mk_app(g, m_g_vars.size(), m_g_vars.c_ptr()), m.mk_app(f, m_f_vars.size(), m_f_vars.c_ptr())); - rm.mk_rule(fml, m_rules, g->get_name()); + proof_ref pr(m); + if (m_context.generate_proof_trace()) { + pr = m.mk_asserted(fml); // or a def? + } + rm.mk_rule(fml, pr, m_rules, g->get_name()); } result = m.mk_app(g, m_args.size(), m_args.c_ptr()); result_pr = 0; @@ -170,14 +248,11 @@ namespace datalog { m_blaster.updt_params(m_params); } - rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) { - // TODO mc, pc + rule_set * operator()(rule_set const & source, model_converter_ref& mc) { + // TODO pc if (!m_context.get_params().bit_blast()) { return 0; } - if (m_context.get_engine() != PDR_ENGINE) { - return 0; - } rule_manager& rm = m_context.get_rule_manager(); unsigned sz = source.get_num_rules(); expr_ref fml(m); @@ -185,9 +260,13 @@ namespace datalog { rule_set * result = alloc(rule_set, m_context); for (unsigned i = 0; i < sz; ++i) { rule * r = source.get_rule(i); - r->to_formula(fml); + r->to_formula(fml); if (blast(fml)) { - rm.mk_rule(fml, m_rules, r->name()); + proof_ref pr(m); + if (m_context.generate_proof_trace()) { + pr = m.mk_asserted(fml); // loses original proof of r. + } + rm.mk_rule(fml, pr, m_rules, r->name()); } else { m_rules.push_back(r); @@ -197,6 +276,18 @@ namespace datalog { for (unsigned i = 0; i < m_rules.size(); ++i) { result->add_rule(m_rules.get(i)); } + + if (mc) { + filter_model_converter* fmc = alloc(filter_model_converter, m); + bit_blast_model_converter* bvmc = alloc(bit_blast_model_converter, m); + func_decl_ref_vector const& old_funcs = m_rewriter.m_cfg.old_funcs(); + func_decl_ref_vector const& new_funcs = m_rewriter.m_cfg.new_funcs(); + for (unsigned i = 0; i < old_funcs.size(); ++i) { + fmc->insert(new_funcs[i]); + bvmc->insert(old_funcs[i], new_funcs[i]); + } + mc = concat(mc.get(), concat(bvmc, fmc)); + } return result; } @@ -210,8 +301,8 @@ namespace datalog { dealloc(m_impl); } - rule_set * mk_bit_blast::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) { - return (*m_impl)(source, mc, pc); + rule_set * mk_bit_blast::operator()(rule_set const & source, model_converter_ref& mc) { + return (*m_impl)(source, mc); } }; diff --git a/src/muz_qe/dl_mk_bit_blast.h b/src/muz_qe/dl_mk_bit_blast.h index e16c2058b..3a6de75e3 100644 --- a/src/muz_qe/dl_mk_bit_blast.h +++ b/src/muz_qe/dl_mk_bit_blast.h @@ -44,7 +44,7 @@ namespace datalog { mk_bit_blast(context & ctx, unsigned priority = 35000); ~mk_bit_blast(); - rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc); + rule_set * operator()(rule_set const & source, model_converter_ref& mc); }; }; diff --git a/src/muz_qe/dl_mk_coalesce.cpp b/src/muz_qe/dl_mk_coalesce.cpp index 222881bc4..de5388312 100644 --- a/src/muz_qe/dl_mk_coalesce.cpp +++ b/src/muz_qe/dl_mk_coalesce.cpp @@ -133,7 +133,7 @@ namespace datalog { tail.push_back(to_app(fml)); is_neg.push_back(false); res = rm.mk(head, tail.size(), tail.c_ptr(), is_neg.c_ptr(), tgt->name()); - if (m_pc) { + if (m_ctx.generate_proof_trace()) { src.to_formula(fml1); tgt->to_formula(fml2); res->to_formula(fml); @@ -142,12 +142,13 @@ namespace datalog { sort* domain[3] = { ps, ps, m.mk_bool_sort() }; func_decl* merge = m.mk_func_decl(symbol("merge-clauses"), 3, domain, ps); // TBD: ad-hoc proof rule expr* args[3] = { m.mk_asserted(fml1), m.mk_asserted(fml2), fml }; - m_pc->insert(m.mk_app(merge, 3, args)); + // ...m_pc->insert(m.mk_app(merge, 3, args)); #else svector > pos; vector substs; - proof* p = m.mk_asserted(fml1); - m_pc->insert(m.mk_hyper_resolve(1, &p, fml, pos, substs)); + proof* p = src.get_proof(); + p = m.mk_hyper_resolve(1, &p, fml, pos, substs); + res->set_proof(m, p); #endif } tgt = res; @@ -170,13 +171,7 @@ namespace datalog { return true; } - rule_set * mk_coalesce::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) { - m_pc = 0; - ref rpc; - if (pc) { - rpc = alloc(replace_proof_converter, m); - m_pc = rpc.get(); - } + rule_set * mk_coalesce::operator()(rule_set const & source, model_converter_ref& mc) { rule_set* rules = alloc(rule_set, m_ctx); rule_set::decl2rules::iterator it = source.begin_grouped_rules(), end = source.end_grouped_rules(); for (; it != end; ++it) { @@ -195,9 +190,6 @@ namespace datalog { rules->add_rule(r1.get()); } } - if (pc) { - pc = concat(pc.get(), rpc.get()); - } return rules; } diff --git a/src/muz_qe/dl_mk_coalesce.h b/src/muz_qe/dl_mk_coalesce.h index 4259d31fe..ab0b74479 100644 --- a/src/muz_qe/dl_mk_coalesce.h +++ b/src/muz_qe/dl_mk_coalesce.h @@ -37,7 +37,6 @@ namespace datalog { rule_manager& rm; expr_ref_vector m_sub1, m_sub2; unsigned m_idx; - replace_proof_converter* m_pc; void mk_pred(app_ref& pred, app* p1, app* p2); @@ -53,7 +52,7 @@ namespace datalog { */ mk_coalesce(context & ctx); - rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc); + rule_set * operator()(rule_set const & source, model_converter_ref& mc); }; }; diff --git a/src/muz_qe/dl_mk_coi_filter.cpp b/src/muz_qe/dl_mk_coi_filter.cpp index 04d654120..915dd4306 100644 --- a/src/muz_qe/dl_mk_coi_filter.cpp +++ b/src/muz_qe/dl_mk_coi_filter.cpp @@ -35,8 +35,7 @@ namespace datalog { rule_set * mk_coi_filter::operator()( rule_set const & source, - model_converter_ref& mc, - proof_converter_ref& pc) + model_converter_ref& mc) { if (source.get_num_rules()==0) { return 0; diff --git a/src/muz_qe/dl_mk_coi_filter.h b/src/muz_qe/dl_mk_coi_filter.h index b8fb37964..2191048d3 100644 --- a/src/muz_qe/dl_mk_coi_filter.h +++ b/src/muz_qe/dl_mk_coi_filter.h @@ -40,8 +40,7 @@ namespace datalog { rule_set * operator()(rule_set const & source, - model_converter_ref& mc, - proof_converter_ref& pc); + model_converter_ref& mc); }; }; diff --git a/src/muz_qe/dl_mk_explanations.cpp b/src/muz_qe/dl_mk_explanations.cpp index 464ec838e..af5b1d97a 100644 --- a/src/muz_qe/dl_mk_explanations.cpp +++ b/src/muz_qe/dl_mk_explanations.cpp @@ -875,8 +875,8 @@ namespace datalog { } } - rule_set * mk_explanations::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) { - SASSERT(!mc && !pc); + rule_set * mk_explanations::operator()(rule_set const & source, model_converter_ref& mc) { + SASSERT(!mc); if(source.get_num_rules()==0) { return 0; } diff --git a/src/muz_qe/dl_mk_explanations.h b/src/muz_qe/dl_mk_explanations.h index 36fb1a3a1..40606f8df 100644 --- a/src/muz_qe/dl_mk_explanations.h +++ b/src/muz_qe/dl_mk_explanations.h @@ -82,7 +82,7 @@ namespace datalog { return get_union_decl(m_context); } - rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc); + rule_set * operator()(rule_set const & source, model_converter_ref& mc); static expr* get_explanation(relation_base const& r); }; diff --git a/src/muz_qe/dl_mk_extract_quantifiers.cpp b/src/muz_qe/dl_mk_extract_quantifiers.cpp index 35f7485d5..a3d5cc2ab 100644 --- a/src/muz_qe/dl_mk_extract_quantifiers.cpp +++ b/src/muz_qe/dl_mk_extract_quantifiers.cpp @@ -168,7 +168,15 @@ namespace datalog { fml = m.mk_implies(m.mk_and(fmls.size(), fmls.c_ptr()), r.get_head()); TRACE("dl", tout << "new rule\n" << mk_pp(fml, m) << "\n";); rule_ref_vector rules(rm); - rm.mk_rule(fml, rules, r.name()); + proof_ref pr(m); + if (m_ctx.generate_proof_trace()) { + scoped_proof _scp(m); + expr_ref fml1(m); + r.to_formula(fml1); + pr = m.mk_rewrite(fml1, fml); + pr = m.mk_modus_ponens(r.get_proof(), pr); + } + rm.mk_rule(fml, pr, rules, r.name()); for (unsigned i = 0; i < rules.size(); ++i) { new_rules.add_rule(rules[i].get()); m_quantifiers.insert(rules[i].get(), alloc(quantifier_ref_vector, qs)); @@ -347,7 +355,7 @@ namespace datalog { m_quantifiers.reset(); } - rule_set * mk_extract_quantifiers::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) { + rule_set * mk_extract_quantifiers::operator()(rule_set const & source, model_converter_ref& mc) { reset(); rule_set::iterator it = source.begin(), end = source.end(); for (; !m_has_quantifiers && it != end; ++it) { diff --git a/src/muz_qe/dl_mk_extract_quantifiers.h b/src/muz_qe/dl_mk_extract_quantifiers.h index b32dbc32d..7d2f7b149 100644 --- a/src/muz_qe/dl_mk_extract_quantifiers.h +++ b/src/muz_qe/dl_mk_extract_quantifiers.h @@ -77,7 +77,7 @@ namespace datalog { void set_query(func_decl* q); - rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc); + rule_set * operator()(rule_set const & source, model_converter_ref& mc); bool has_quantifiers() { return m_has_quantifiers; } diff --git a/src/muz_qe/dl_mk_filter_rules.cpp b/src/muz_qe/dl_mk_filter_rules.cpp index 4f01a3651..46fde4bc2 100644 --- a/src/muz_qe/dl_mk_filter_rules.cpp +++ b/src/muz_qe/dl_mk_filter_rules.cpp @@ -90,6 +90,7 @@ namespace datalog { rule * filter_rule = m_context.get_rule_manager().mk(filter_head, 1, &filter_tail, (const bool *)0); filter_rule->set_accounting_parent_object(m_context, m_current); m_result->add_rule(filter_rule); + m_context.get_rule_manager().mk_rule_asserted_proof(*filter_rule); } else { dealloc(key); @@ -135,12 +136,13 @@ namespace datalog { } new_is_negated.push_back(r->is_neg_tail(i)); } - if(rule_modified) { + if (rule_modified) { remove_duplicate_tails(new_tail, new_is_negated); SASSERT(new_tail.size() == new_is_negated.size()); rule * new_rule = m_context.get_rule_manager().mk(new_head, new_tail.size(), new_tail.c_ptr(), new_is_negated.c_ptr()); new_rule->set_accounting_parent_object(m_context, m_current); m_result->add_rule(new_rule); + m_context.get_rule_manager().mk_rule_rewrite_proof(*r, *new_rule); m_modified = true; } else { @@ -148,7 +150,7 @@ namespace datalog { } } - rule_set * mk_filter_rules::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) { + rule_set * mk_filter_rules::operator()(rule_set const & source, model_converter_ref& mc) { // TODO mc, pc m_tail2filter.reset(); m_result = alloc(rule_set, m_context); diff --git a/src/muz_qe/dl_mk_filter_rules.h b/src/muz_qe/dl_mk_filter_rules.h index cd1d10997..daa72e36f 100644 --- a/src/muz_qe/dl_mk_filter_rules.h +++ b/src/muz_qe/dl_mk_filter_rules.h @@ -72,7 +72,7 @@ namespace datalog { /** \brief Return a new rule set where only filter rules contain atoms with repeated variables and/or values. */ - rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc); + rule_set * operator()(rule_set const & source, model_converter_ref& mc); }; }; diff --git a/src/muz_qe/dl_mk_interp_tail_simplifier.cpp b/src/muz_qe/dl_mk_interp_tail_simplifier.cpp index d1b7f15dd..a48b7b32f 100644 --- a/src/muz_qe/dl_mk_interp_tail_simplifier.cpp +++ b/src/muz_qe/dl_mk_interp_tail_simplifier.cpp @@ -554,11 +554,13 @@ namespace datalog { bool mk_interp_tail_simplifier::transform_rules(const rule_set & orig, rule_set & tgt) { bool modified = false; + rule_manager& rm = m_context.get_rule_manager(); rule_set::iterator rit = orig.begin(); rule_set::iterator rend = orig.end(); for (; rit!=rend; ++rit) { - rule_ref new_rule(m_context.get_rule_manager()); + rule_ref new_rule(rm); if (transform_rule(*rit, new_rule)) { + rm.mk_rule_rewrite_proof(**rit, *new_rule.get()); bool is_modified = *rit != new_rule; modified |= is_modified; tgt.add_rule(new_rule); @@ -570,8 +572,7 @@ namespace datalog { return modified; } - rule_set * mk_interp_tail_simplifier::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) { - // TODO mc, pc + rule_set * mk_interp_tail_simplifier::operator()(rule_set const & source, model_converter_ref& mc) { if (source.get_num_rules() == 0) { return 0; } diff --git a/src/muz_qe/dl_mk_interp_tail_simplifier.h b/src/muz_qe/dl_mk_interp_tail_simplifier.h index 5e4fd8fbc..4cb14914a 100644 --- a/src/muz_qe/dl_mk_interp_tail_simplifier.h +++ b/src/muz_qe/dl_mk_interp_tail_simplifier.h @@ -93,7 +93,7 @@ namespace datalog { */ bool transform_rule(rule * r, rule_ref& res); - rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc); + rule_set * operator()(rule_set const & source, model_converter_ref& mc); }; }; diff --git a/src/muz_qe/dl_mk_karr_invariants.cpp b/src/muz_qe/dl_mk_karr_invariants.cpp index 9c034c890..18b152589 100644 --- a/src/muz_qe/dl_mk_karr_invariants.cpp +++ b/src/muz_qe/dl_mk_karr_invariants.cpp @@ -310,7 +310,7 @@ namespace datalog { m_hb.reset(); for (unsigned i = 0; i < src.size(); ++i) { vector v(src.A[i]); - v.append(src.b[i]); + v.push_back(src.b[i]); if (src.eq[i]) { m_hb.add_eq(v, rational(0)); } @@ -420,6 +420,7 @@ namespace datalog { new_rule = rm.mk(r.get_head(), tail.size(), tail.c_ptr(), 0, r.name()); } rules.add_rule(new_rule); + rm.mk_rule_rewrite_proof(r, *new_rule); // should be weakening rule. } class mk_karr_invariants::add_invariant_model_converter : public model_converter { @@ -519,7 +520,7 @@ namespace datalog { m_hb.set_cancel(true); } - rule_set * mk_karr_invariants::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) { + rule_set * mk_karr_invariants::operator()(rule_set const & source, model_converter_ref& mc) { if (!m_ctx.get_params().karr()) { return 0; } diff --git a/src/muz_qe/dl_mk_karr_invariants.h b/src/muz_qe/dl_mk_karr_invariants.h index 3b82578a4..7cd26d495 100644 --- a/src/muz_qe/dl_mk_karr_invariants.h +++ b/src/muz_qe/dl_mk_karr_invariants.h @@ -69,7 +69,7 @@ namespace datalog { virtual void cancel(); - rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc); + rule_set * operator()(rule_set const & source, model_converter_ref& mc); }; diff --git a/src/muz_qe/dl_mk_magic_sets.cpp b/src/muz_qe/dl_mk_magic_sets.cpp index 373a90969..990040ab8 100644 --- a/src/muz_qe/dl_mk_magic_sets.cpp +++ b/src/muz_qe/dl_mk_magic_sets.cpp @@ -317,8 +317,8 @@ namespace datalog { m_rules.push_back(r); } - rule_set * mk_magic_sets::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) { - SASSERT(!mc && !pc); + rule_set * mk_magic_sets::operator()(rule_set const & source, model_converter_ref& mc) { + SASSERT(!mc); unsigned init_rule_cnt = source.get_num_rules(); { func_decl_set intentional; diff --git a/src/muz_qe/dl_mk_magic_sets.h b/src/muz_qe/dl_mk_magic_sets.h index f98ad55a3..3f50e6713 100644 --- a/src/muz_qe/dl_mk_magic_sets.h +++ b/src/muz_qe/dl_mk_magic_sets.h @@ -121,7 +121,7 @@ namespace datalog { */ mk_magic_sets(context & ctx, rule * goal_rule); - rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc); + rule_set * operator()(rule_set const & source, model_converter_ref& mc); }; }; diff --git a/src/muz_qe/dl_mk_partial_equiv.cpp b/src/muz_qe/dl_mk_partial_equiv.cpp index 367a15743..b55f5294e 100644 --- a/src/muz_qe/dl_mk_partial_equiv.cpp +++ b/src/muz_qe/dl_mk_partial_equiv.cpp @@ -86,8 +86,8 @@ namespace datalog { } - rule_set * mk_partial_equivalence_transformer::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) { - // TODO mc, pc + rule_set * mk_partial_equivalence_transformer::operator()(rule_set const & source, model_converter_ref& mc) { + // TODO mc if (source.get_num_rules() == 0) { return 0; diff --git a/src/muz_qe/dl_mk_partial_equiv.h b/src/muz_qe/dl_mk_partial_equiv.h index 8fef4aea9..c44d59e8c 100644 --- a/src/muz_qe/dl_mk_partial_equiv.h +++ b/src/muz_qe/dl_mk_partial_equiv.h @@ -35,7 +35,7 @@ namespace datalog { m(ctx.get_manager()), m_context(ctx) {} - rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc); + rule_set * operator()(rule_set const & source, model_converter_ref& mc); private: diff --git a/src/muz_qe/dl_mk_rule_inliner.cpp b/src/muz_qe/dl_mk_rule_inliner.cpp index 1404c9c8c..047ed768f 100644 --- a/src/muz_qe/dl_mk_rule_inliner.cpp +++ b/src/muz_qe/dl_mk_rule_inliner.cpp @@ -181,10 +181,10 @@ namespace datalog { } if (m_unifier.apply(tgt, tail_index, src, res)) { - if (m_pc) { + if (m_context.generate_proof_trace()) { expr_ref_vector s1 = m_unifier.get_rule_subst(tgt, true); expr_ref_vector s2 = m_unifier.get_rule_subst(src, false); - datalog::resolve_rule(m_pc, tgt, src, tail_index, s1, s2, *res.get()); + datalog::resolve_rule(tgt, src, tail_index, s1, s2, *res.get()); } return true; } @@ -837,11 +837,10 @@ namespace datalog { return done_something; } - rule_set * mk_rule_inliner::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) { + rule_set * mk_rule_inliner::operator()(rule_set const & source, model_converter_ref& mc) { bool something_done = false; ref hsmc; - ref hpc; if (source.get_num_rules() == 0) { return 0; @@ -858,11 +857,7 @@ namespace datalog { if (mc) { hsmc = alloc(horn_subsume_model_converter, m); } - if (pc) { - hpc = alloc(replace_proof_converter, m); - } m_mc = hsmc.get(); - m_pc = hpc.get(); scoped_ptr res = alloc(rule_set, m_context); @@ -889,9 +884,6 @@ namespace datalog { if (mc) { mc = concat(mc.get(), hsmc.get()); } - if (pc) { - pc = concat(pc.get(), hpc.get()); - } } return res.detach(); diff --git a/src/muz_qe/dl_mk_rule_inliner.h b/src/muz_qe/dl_mk_rule_inliner.h index 6d5448cd6..a58b3b473 100644 --- a/src/muz_qe/dl_mk_rule_inliner.h +++ b/src/muz_qe/dl_mk_rule_inliner.h @@ -114,7 +114,6 @@ namespace datalog { ast_counter m_tail_pred_ctr; rule_set m_inlined_rules; horn_subsume_model_converter* m_mc; - replace_proof_converter* m_pc; //used in try_to_inline_rule and do_eager_inlining @@ -188,7 +187,6 @@ namespace datalog { m_pinned(m_rm), m_inlined_rules(m_context), m_mc(0), - m_pc(0), m_unifier(ctx), m_head_index(m), m_tail_index(m), @@ -198,7 +196,7 @@ namespace datalog { {} virtual ~mk_rule_inliner() { } - rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc); + rule_set * operator()(rule_set const & source, model_converter_ref& mc); }; }; diff --git a/src/muz_qe/dl_mk_similarity_compressor.cpp b/src/muz_qe/dl_mk_similarity_compressor.cpp index a040a623a..dfd0a4d81 100644 --- a/src/muz_qe/dl_mk_similarity_compressor.cpp +++ b/src/muz_qe/dl_mk_similarity_compressor.cpp @@ -500,8 +500,8 @@ namespace datalog { } } - rule_set * mk_similarity_compressor::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) { - // TODO mc, pc + rule_set * mk_similarity_compressor::operator()(rule_set const & source, model_converter_ref& mc) { + // TODO mc m_modified = false; unsigned init_rule_cnt = source.get_num_rules(); SASSERT(m_rules.empty()); diff --git a/src/muz_qe/dl_mk_similarity_compressor.h b/src/muz_qe/dl_mk_similarity_compressor.h index ad4a5e246..d1ded01e7 100644 --- a/src/muz_qe/dl_mk_similarity_compressor.h +++ b/src/muz_qe/dl_mk_similarity_compressor.h @@ -69,7 +69,7 @@ namespace datalog { public: mk_similarity_compressor(context & ctx, unsigned threshold_count); - rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc); + rule_set * operator()(rule_set const & source, model_converter_ref& mc); }; }; diff --git a/src/muz_qe/dl_mk_simple_joins.cpp b/src/muz_qe/dl_mk_simple_joins.cpp index 77c6c2951..f19e34fec 100644 --- a/src/muz_qe/dl_mk_simple_joins.cpp +++ b/src/muz_qe/dl_mk_simple_joins.cpp @@ -706,19 +706,20 @@ namespace datalog { negs.c_ptr()); new_rule->set_accounting_parent_object(m_context, orig_r); - + m_context.get_rule_manager().mk_rule_rewrite_proof(*orig_r, *new_rule); result->add_rule(new_rule); } - while(!m_introduced_rules.empty()) { + while (!m_introduced_rules.empty()) { result->add_rule(m_introduced_rules.back()); + m_context.get_rule_manager().mk_rule_asserted_proof(*m_introduced_rules.back()); m_introduced_rules.pop_back(); } return result; } }; - rule_set * mk_simple_joins::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) { - // TODO mc, pc + rule_set * mk_simple_joins::operator()(rule_set const & source, model_converter_ref& mc) { + // TODO mc rule_set rs_aux_copy(m_context); rs_aux_copy.add_rules(source); if(!rs_aux_copy.is_closed()) { diff --git a/src/muz_qe/dl_mk_simple_joins.h b/src/muz_qe/dl_mk_simple_joins.h index 5431c4117..df8d3f55c 100644 --- a/src/muz_qe/dl_mk_simple_joins.h +++ b/src/muz_qe/dl_mk_simple_joins.h @@ -53,7 +53,7 @@ namespace datalog { public: mk_simple_joins(context & ctx); - rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc); + rule_set * operator()(rule_set const & source, model_converter_ref& mc); }; }; diff --git a/src/muz_qe/dl_mk_slice.cpp b/src/muz_qe/dl_mk_slice.cpp index 84b732280..0adab78ce 100644 --- a/src/muz_qe/dl_mk_slice.cpp +++ b/src/muz_qe/dl_mk_slice.cpp @@ -164,10 +164,8 @@ namespace datalog { TRACE("dl", tout << "does not have fact\n" << mk_pp(fact, m) << "\n";); return false; } - expr_ref fml(m); proof_ref new_p(m); - r->to_formula(fml); - new_p = m.mk_asserted(fml); + new_p = r->get_proof(); m_pinned_exprs.push_back(new_p); m_todo.pop_back(); m_new_proof.insert(p, new_p); @@ -784,6 +782,9 @@ namespace datalog { rm.fix_unbound_vars(new_rule, false); TRACE("dl", r.display(m_ctx, tout << "replacing:\n"); new_rule->display(m_ctx, tout << "by:\n");); + if (m_ctx.generate_proof_trace()) { + rm.mk_rule_asserted_proof(*new_rule.get()); + } } else { new_rule = &r; @@ -801,7 +802,7 @@ namespace datalog { } } - rule_set * mk_slice::operator()(rule_set const & src, model_converter_ref& mc, proof_converter_ref& pc) { + rule_set * mk_slice::operator()(rule_set const & src, model_converter_ref& mc) { for (unsigned i = 0; i < src.get_num_rules(); ++i) { if (src.get_rule(i)->has_quantifiers()) { return 0; @@ -809,8 +810,8 @@ namespace datalog { } ref spc; ref smc; - if (pc) { - spc = alloc(slice_proof_converter, m_ctx); + if (m_ctx.generate_proof_trace()) { + spc = alloc(slice_proof_converter, m_ctx); } if (mc) { smc = alloc(slice_model_converter, *this, m); @@ -834,7 +835,7 @@ namespace datalog { m_mc->add_sliceable(it->m_key, it->m_value); } } - pc = concat(pc.get(), spc.get()); + m_ctx.add_proof_converter(spc.get()); mc = concat(mc.get(), smc.get()); return result; } diff --git a/src/muz_qe/dl_mk_slice.h b/src/muz_qe/dl_mk_slice.h index 26a8175f2..4290ee4b9 100644 --- a/src/muz_qe/dl_mk_slice.h +++ b/src/muz_qe/dl_mk_slice.h @@ -102,7 +102,7 @@ namespace datalog { virtual ~mk_slice() { } - rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc); + rule_set * operator()(rule_set const & source, model_converter_ref& mc); func_decl* get_predicate(func_decl* p) { func_decl* q = p; m_predicates.find(p, q); return q; } diff --git a/src/muz_qe/dl_mk_subsumption_checker.cpp b/src/muz_qe/dl_mk_subsumption_checker.cpp index 19c28c036..2f0d56475 100644 --- a/src/muz_qe/dl_mk_subsumption_checker.cpp +++ b/src/muz_qe/dl_mk_subsumption_checker.cpp @@ -166,7 +166,8 @@ namespace datalog { res = m_context.get_rule_manager().mk(head, tail.size(), tail.c_ptr(), tail_neg.c_ptr()); res->set_accounting_parent_object(m_context, r); m_context.get_rule_manager().fix_unbound_vars(res, true); - + m_context.get_rule_manager().mk_rule_rewrite_proof(*r, *res.get()); + return true; } @@ -208,10 +209,10 @@ namespace datalog { continue; } rule * defining_rule; - TRUSTME(m_total_relation_defining_rules.find(head_pred, defining_rule)); - if(defining_rule) { + VERIFY(m_total_relation_defining_rules.find(head_pred, defining_rule)); + if (defining_rule) { rule_ref totality_rule(m_context.get_rule_manager()); - TRUSTME(transform_rule(defining_rule, subs_index, totality_rule)); + VERIFY(transform_rule(defining_rule, subs_index, totality_rule)); if(defining_rule!=totality_rule) { modified = true; } @@ -331,8 +332,8 @@ namespace datalog { } } - rule_set * mk_subsumption_checker::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) { - // TODO mc, pc + rule_set * mk_subsumption_checker::operator()(rule_set const & source, model_converter_ref& mc) { + // TODO mc m_have_new_total_rule = false; collect_ground_unconditional_rule_heads(source); diff --git a/src/muz_qe/dl_mk_subsumption_checker.h b/src/muz_qe/dl_mk_subsumption_checker.h index ce33e7574..a95f08c5d 100644 --- a/src/muz_qe/dl_mk_subsumption_checker.h +++ b/src/muz_qe/dl_mk_subsumption_checker.h @@ -84,7 +84,7 @@ namespace datalog { reset_dealloc_values(m_ground_unconditional_rule_heads); } - rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc); + rule_set * operator()(rule_set const & source, model_converter_ref& mc); }; }; diff --git a/src/muz_qe/dl_mk_unbound_compressor.cpp b/src/muz_qe/dl_mk_unbound_compressor.cpp index e3db82759..54b6f4ebe 100644 --- a/src/muz_qe/dl_mk_unbound_compressor.cpp +++ b/src/muz_qe/dl_mk_unbound_compressor.cpp @@ -238,6 +238,7 @@ namespace datalog { unsigned new_rule_index = m_rules.size(); m_rules.push_back(new_rule); + m_context.get_rule_manager().mk_rule_rewrite_proof(*r, *new_rule.get()); m_head_occurrence_ctr.inc(new_rule->get_head()->get_decl()); @@ -333,8 +334,8 @@ namespace datalog { } } - rule_set * mk_unbound_compressor::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) { - // TODO mc, pc + rule_set * mk_unbound_compressor::operator()(rule_set const & source, model_converter_ref& mc) { + // TODO mc m_modified = false; m_context.get_rel_context().get_rmanager().collect_non_empty_predicates(m_non_empty_rels); diff --git a/src/muz_qe/dl_mk_unbound_compressor.h b/src/muz_qe/dl_mk_unbound_compressor.h index 0e13bad75..256be180d 100644 --- a/src/muz_qe/dl_mk_unbound_compressor.h +++ b/src/muz_qe/dl_mk_unbound_compressor.h @@ -82,7 +82,7 @@ namespace datalog { public: mk_unbound_compressor(context & ctx); - rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc); + rule_set * operator()(rule_set const & source, model_converter_ref& mc); }; }; diff --git a/src/muz_qe/dl_mk_unfold.cpp b/src/muz_qe/dl_mk_unfold.cpp index d26a0a290..7af82110a 100644 --- a/src/muz_qe/dl_mk_unfold.cpp +++ b/src/muz_qe/dl_mk_unfold.cpp @@ -42,29 +42,20 @@ namespace datalog { if (m_unify.unify_rules(r, tail_idx, r2) && m_unify.apply(r, tail_idx, r2, new_rule)) { expr_ref_vector s1 = m_unify.get_rule_subst(r, true); - expr_ref_vector s2 = m_unify.get_rule_subst(r2, false); - resolve_rule(m_pc, r, r2, tail_idx, s1, s2, *new_rule.get()); + expr_ref_vector s2 = m_unify.get_rule_subst(r2, false); + resolve_rule(r, r2, tail_idx, s1, s2, *new_rule.get()); expand_tail(*new_rule.get(), tail_idx+r2.get_uninterpreted_tail_size(), src, dst); } } } } - rule_set * mk_unfold::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) { - m_pc = 0; - ref rpc; - if (pc) { - rpc = alloc(replace_proof_converter, m); - m_pc = rpc.get(); - } + rule_set * mk_unfold::operator()(rule_set const & source, model_converter_ref& mc) { rule_set* rules = alloc(rule_set, m_ctx); rule_set::iterator it = source.begin(), end = source.end(); for (; it != end; ++it) { expand_tail(**it, 0, source, *rules); } - if (pc) { - pc = concat(pc.get(), rpc.get()); - } return rules; } diff --git a/src/muz_qe/dl_mk_unfold.h b/src/muz_qe/dl_mk_unfold.h index 3d20686a7..90aefa86e 100644 --- a/src/muz_qe/dl_mk_unfold.h +++ b/src/muz_qe/dl_mk_unfold.h @@ -35,7 +35,6 @@ namespace datalog { ast_manager& m; rule_manager& rm; rule_unifier m_unify; - replace_proof_converter* m_pc; void expand_tail(rule& r, unsigned tail_idx, rule_set const& src, rule_set& dst); @@ -45,7 +44,7 @@ namespace datalog { */ mk_unfold(context & ctx); - rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc); + rule_set * operator()(rule_set const & source, model_converter_ref& mc); }; }; diff --git a/src/muz_qe/dl_rule.cpp b/src/muz_qe/dl_rule.cpp index 59a245cc4..1896e7e64 100644 --- a/src/muz_qe/dl_rule.cpp +++ b/src/muz_qe/dl_rule.cpp @@ -42,13 +42,13 @@ Revision History: #include"bool_rewriter.h" #include"qe_lite.h" #include"expr_safe_replace.h" +#include"hnf.h" namespace datalog { rule_manager::rule_manager(context& ctx) : m(ctx.get_manager()), - m_ctx(ctx), - m_refs(ctx.get_manager()) {} + m_ctx(ctx) {} bool rule_manager::is_predicate(func_decl * f) const { return m_ctx.is_predicate(f); @@ -89,72 +89,32 @@ namespace datalog { } }; - void rule_manager::remove_labels(expr_ref& fml) { + void rule_manager::remove_labels(expr_ref& fml, proof_ref& pr) { expr_ref tmp(m); remove_label_cfg r_cfg(m); rewriter_tpl rwr(m, false, r_cfg); rwr(fml, tmp); + if (pr && fml != tmp) { + + pr = m.mk_modus_ponens(pr, m.mk_rewrite(fml, tmp)); + } fml = tmp; } - void rule_manager::mk_rule(expr* fml, rule_ref_vector& rules, symbol const& name) { + void rule_manager::mk_rule(expr* fml, proof* p, rule_ref_vector& rules, symbol const& name) { + scoped_proof_mode _sc(m, m_ctx.generate_proof_trace()?PGM_FINE:PGM_DISABLED); + proof_ref pr(p, m); expr_ref fml1(m); - m_memoize_disj.reset(); - m_refs.reset(); bind_variables(fml, true, fml1); - remove_labels(fml1); - mk_rule_core(fml1, rules, name); + if (fml1 != fml && pr) { + pr = m.mk_asserted(fml1); + } + remove_labels(fml1, pr); + mk_rule_core_new(fml1, pr, rules, name); } - - void rule_manager::mk_rule_core(expr* _fml, rule_ref_vector& rules, symbol const& name) { - app_ref_vector body(m); - app_ref head(m); - expr_ref e(m), fml(_fml, m); - svector is_negated; - TRACE("dl_rule", tout << mk_pp(fml, m) << "\n";); - quantifier_hoister qh(m); - unsigned index = qh.pull_quantifier(true, fml, 0); - check_app(fml); - head = to_app(fml); - - while (m.is_implies(head)) { - e = head->get_arg(0); - th_rewriter th_rwr(m); - th_rwr(e); - body.push_back(ensure_app(e)); - e = to_app(head)->get_arg(1); - check_app(e); - head = to_app(e.get()); - } - symbol head_name = (name == symbol::null)?head->get_decl()->get_name():name; - flatten_body(body); - if (body.size() == 1 && m.is_or(body[0].get()) && contains_predicate(body[0].get())) { - app* _or = to_app(body[0].get()); - for (unsigned i = 0; i < _or->get_num_args(); ++i) { - e = m.mk_implies(_or->get_arg(i), head); - mk_rule_core(e, rules, head_name); - } - return; - } - - eliminate_disjunctions(body, rules, head_name); - eliminate_quantifier_body(body, rules, head_name); - hoist_compound(index, head, body); - unsigned sz = body.size(); - for (unsigned i = 0; i < sz; ++i) { - app_ref b(body[i].get(), m); - hoist_compound(index, b, body); - body[i] = b; - } - TRACE("dl_rule", - tout << mk_pp(head, m) << " :- "; - for (unsigned i = 0; i < body.size(); ++i) { - tout << mk_pp(body[i].get(), m) << " "; - } - tout << "\n";); - + void rule_manager::mk_negations(app_ref_vector& body, svector& is_negated) { for (unsigned i = 0; i < body.size(); ++i) { expr* e = body[i].get(), *e1; if (m.is_not(e, e1) && is_predicate(e1)) { @@ -165,23 +125,105 @@ namespace datalog { else { is_negated.push_back(false); } - } - check_valid_rule(head, body.size(), body.c_ptr()); + } + } - rules.push_back(mk(head.get(), body.size(), body.c_ptr(), is_negated.c_ptr(), name)); - - if (m_ctx.fix_unbound_vars()) { - unsigned rule_cnt = rules.size(); - for (unsigned i=0; i is_negated; + unsigned index = extract_horn(fml, body, head); + hoist_compound_predicates(index, head, body); + TRACE("dl_rule", + tout << mk_pp(head, m) << " :- "; + for (unsigned i = 0; i < body.size(); ++i) { + tout << mk_pp(body[i].get(), m) << " "; + } + tout << "\n";); + + + mk_negations(body, is_negated); + check_valid_rule(head, body.size(), body.c_ptr()); + + rule_ref r(*this); + r = mk(head.get(), body.size(), body.c_ptr(), is_negated.c_ptr(), name); + + expr_ref fml1(m); + if (p) { + r->to_formula(fml1); + if (fml1 == fml) { + // no-op. + } + else if (is_quantifier(fml1)) { + p = m.mk_modus_ponens(p, m.mk_symmetry(m.mk_der(to_quantifier(fml1), fml))); + } + else { + p = m.mk_modus_ponens(p, m.mk_rewrite(fml, fml1)); + } + } + + if (m_ctx.fix_unbound_vars()) { + fix_unbound_vars(r, true); + } + + if (p) { + expr_ref fml2(m); + r->to_formula(fml2); + if (fml1 != fml2) { + p = m.mk_modus_ponens(p, m.mk_rewrite(fml1, fml2)); + } + r->set_proof(m, p); + } + rules.push_back(r); + } + + unsigned rule_manager::extract_horn(expr* fml, app_ref_vector& body, app_ref& head) { + expr* e1, *e2; + unsigned index = m_counter.get_next_var(fml); + if (::is_forall(fml)) { + index += to_quantifier(fml)->get_num_decls(); + fml = to_quantifier(fml)->get_expr(); + } + if (m.is_implies(fml, e1, e2)) { + expr_ref_vector es(m); + head = ensure_app(e2); + datalog::flatten_and(e1, es); + for (unsigned i = 0; i < es.size(); ++i) { + body.push_back(ensure_app(es[i].get())); + } + } + else { + head = ensure_app(fml); + } + return index; + } + + void rule_manager::hoist_compound_predicates(unsigned index, app_ref& head, app_ref_vector& body) { + unsigned sz = body.size(); + hoist_compound(index, head, body); + for (unsigned i = 0; i < sz; ++i) { + app_ref b(body[i].get(), m); + hoist_compound(index, b, body); + body[i] = b; + } + } + + void rule_manager::mk_query(expr* query, func_decl_ref& qpred, rule_ref_vector& query_rules, rule_ref& query_rule) { ptr_vector vars; svector names; @@ -192,7 +234,7 @@ namespace datalog { // Remove existential prefix. bind_variables(query, false, q); quantifier_hoister qh(m); - qh.pull_quantifier(false, q, &names); + qh.pull_quantifier(false, q, 0, &names); // retrieve free variables. get_free_vars(q, vars); if (vars.contains(static_cast(0))) { @@ -250,7 +292,12 @@ namespace datalog { rule_expr = m.mk_forall(vars.size(), vars.c_ptr(), names.c_ptr(), impl); } - mk_rule(rule_expr, query_rules); + scoped_proof_mode _sc(m, m_ctx.generate_proof_trace()?PGM_FINE:PGM_DISABLED); + proof_ref pr(m); + if (m_ctx.generate_proof_trace()) { + pr = m.mk_asserted(rule_expr); + } + mk_rule(rule_expr, pr, query_rules); SASSERT(query_rules.size() >= 1); query_rule = query_rules.back(); } @@ -330,73 +377,6 @@ namespace datalog { return false; } - void rule_manager::eliminate_disjunctions(app_ref_vector::element_ref& body, rule_ref_vector& rules, symbol const& name) { - - app* b = body.get(); - expr* e1; - bool negate_args = false; - bool is_disj = false; - unsigned num_disj = 0; - expr* const* disjs = 0; - if (!contains_predicate(b)) { - return; - } - TRACE("dl_rule", tout << mk_ismt2_pp(b, m) << "\n";); - if (m.is_or(b)) { - is_disj = true; - negate_args = false; - num_disj = b->get_num_args(); - disjs = b->get_args(); - } - if (m.is_not(b, e1) && m.is_and(e1)) { - is_disj = true; - negate_args = true; - num_disj = to_app(e1)->get_num_args(); - disjs = to_app(e1)->get_args(); - } - if (is_disj) { - ptr_vector sorts0, sorts1; - get_free_vars(b, sorts0); - expr_ref_vector args(m); - for (unsigned i = 0; i < sorts0.size(); ++i) { - if (sorts0[i]) { - args.push_back(m.mk_var(i,sorts0[i])); - sorts1.push_back(sorts0[i]); - } - } - app* old_head = 0; - if (m_memoize_disj.find(b, old_head)) { - body = old_head; - } - else { - app_ref head(m); - func_decl_ref f(m); - f = m.mk_fresh_func_decl(name.str().c_str(),"", sorts1.size(), sorts1.c_ptr(), m.mk_bool_sort()); - m_ctx.register_predicate(f); - head = m.mk_app(f, args.size(), args.c_ptr()); - - for (unsigned i = 0; i < num_disj; ++i) { - expr_ref fml(m); - expr* e = disjs[i]; - if (negate_args) e = m.mk_not(e); - fml = m.mk_implies(e,head); - mk_rule_core(fml, rules, name); - } - m_memoize_disj.insert(b, head); - m_refs.push_back(b); - m_refs.push_back(head); - // update the body to be the newly introduced head relation - body = head; - } - } - } - - void rule_manager::eliminate_disjunctions(app_ref_vector& body, rule_ref_vector& rules, symbol const& name) { - for (unsigned i = 0; i < body.size(); ++i) { - app_ref_vector::element_ref t = body[i]; - eliminate_disjunctions(t, rules, name); - } - } bool rule_manager::is_forall(ast_manager& m, expr* e, quantifier*& q) { expr* e1, *e2; @@ -415,40 +395,6 @@ namespace datalog { return false; } - void rule_manager::eliminate_quantifier_body(app_ref_vector::element_ref& body, rule_ref_vector& rules, symbol const& name) { - quantifier* q; - if (is_forall(m, body.get(), q) && contains_predicate(q)) { - expr* e = q->get_expr(); - if (!is_predicate(e)) { - ptr_vector sorts0, sorts1; - get_free_vars(e, sorts0); - expr_ref_vector args(m); - for (unsigned i = 0; i < sorts0.size(); ++i) { - if (sorts0[i]) { - args.push_back(m.mk_var(i,sorts0[i])); - sorts1.push_back(sorts0[i]); - } - } - app_ref head(m), fml(m); - func_decl_ref f(m); - f = m.mk_fresh_func_decl(name.str().c_str(),"", sorts1.size(), sorts1.c_ptr(), m.mk_bool_sort()); - m_ctx.register_predicate(f); - head = m.mk_app(f, args.size(), args.c_ptr()); - fml = m.mk_implies(e, head); - mk_rule_core(fml, rules, name); - // update the body to be the newly introduced head relation - body = m.mk_eq(m.mk_true(), m.update_quantifier(q, head)); - } - } - } - - void rule_manager::eliminate_quantifier_body(app_ref_vector& body, rule_ref_vector& rules, symbol const& name) { - for (unsigned i = 0; i < body.size(); ++i) { - app_ref_vector::element_ref t = body[i]; - eliminate_quantifier_body(t, rules, name); - } - } - app_ref rule_manager::ensure_app(expr* e) { SASSERT(m.is_bool(e)); @@ -476,6 +422,7 @@ namespace datalog { r->m_head = head; r->m_name = name; r->m_tail_size = n; + r->m_proof = 0; m.inc_ref(r->m_head); app * * uninterp_tail = r->m_tail; //grows upwards @@ -533,6 +480,11 @@ namespace datalog { if (normalize) { r->norm_vars(*this); } + DEBUG_CODE(ptr_vector sorts; + ::get_free_vars(head, sorts); + for (unsigned i = 0; i < n; ++i) { + ::get_free_vars(tail[i], sorts); + }); return r; } @@ -754,6 +706,27 @@ namespace datalog { r->set_accounting_parent_object(m_ctx, old_r); } + void rule_manager::mk_rule_rewrite_proof(rule& old_rule, rule& new_rule) { + if (&old_rule != &new_rule && + !new_rule.get_proof() && + old_rule.get_proof()) { + expr_ref fml(m); + new_rule.to_formula(fml); + scoped_proof _sc(m); + proof* p = m.mk_rewrite(m.get_fact(old_rule.get_proof()), fml); + new_rule.set_proof(m, m.mk_modus_ponens(old_rule.get_proof(), p)); + } + } + + void rule_manager::mk_rule_asserted_proof(rule& r) { + if (m_ctx.generate_proof_trace()) { + scoped_proof _scp(m); + expr_ref fml(m); + r.to_formula(fml); + r.set_proof(m, m.mk_asserted(fml)); + } + } + void rule_manager::substitute(rule_ref& r, unsigned sz, expr*const* es) { expr_ref tmp(m); app_ref new_head(m); @@ -812,10 +785,23 @@ namespace datalog { for (unsigned i = 0; i < n; i++) { m.dec_ref(get_tail(i)); } + if (m_proof) { + m.dec_ref(m_proof); + } this->~rule(); m.get_allocator().deallocate(get_obj_size(n), this); } + void rule::set_proof(ast_manager& m, proof* p) { + if (p) { + m.inc_ref(p); + } + if (m_proof) { + m.dec_ref(m_proof); + } + m_proof = p; + } + bool rule::is_in_tail(const func_decl * p, bool only_positive) const { unsigned len = only_positive ? get_positive_tail_size() : get_uninterpreted_tail_size(); for (unsigned i = 0; i < len; i++) { @@ -993,6 +979,9 @@ namespace datalog { out << '}'; } out << '\n'; + if (m_proof) { + out << mk_pp(m_proof, m) << '\n'; + } } void rule::to_formula(expr_ref& fml) const { diff --git a/src/muz_qe/dl_rule.h b/src/muz_qe/dl_rule.h index a8c6e0314..5b1338b22 100644 --- a/src/muz_qe/dl_rule.h +++ b/src/muz_qe/dl_rule.h @@ -43,11 +43,9 @@ namespace datalog { */ class rule_manager { - ast_manager& m; - context& m_ctx; - rule_counter m_counter; - obj_map m_memoize_disj; - expr_ref_vector m_refs; + ast_manager& m; + context& m_ctx; + rule_counter m_counter; // only the context can create a rule_manager friend class context; @@ -57,19 +55,13 @@ namespace datalog { /** \brief Move functions from predicate tails into the interpreted tail by introducing new variables. */ + void hoist_compound_predicates(unsigned num_bound, app_ref& head, app_ref_vector& body); + void hoist_compound(unsigned& num_bound, app_ref& fml, app_ref_vector& body); void flatten_body(app_ref_vector& body); - void remove_labels(expr_ref& fml); - - void eliminate_disjunctions(app_ref_vector::element_ref& body, rule_ref_vector& rules, symbol const& name); - - void eliminate_disjunctions(app_ref_vector& body, rule_ref_vector& rules, symbol const& name); - - void eliminate_quantifier_body(app_ref_vector::element_ref& body, rule_ref_vector& rules, symbol const& name); - - void eliminate_quantifier_body(app_ref_vector& body, rule_ref_vector& rules, symbol const& name); + void remove_labels(expr_ref& fml, proof_ref& pr); app_ref ensure_app(expr* e); @@ -81,6 +73,16 @@ namespace datalog { void mk_rule_core(expr* fml, rule_ref_vector& rules, symbol const& name); + void mk_negations(app_ref_vector& body, svector& is_negated); + + void mk_rule_core_new(expr* fml, proof* p, rule_ref_vector& rules, symbol const& name); + + void mk_rule_core2(expr* fml, proof* p, rule_ref_vector& rules, symbol const& name); + + static expr_ref mk_implies(app_ref_vector const& body, expr* head); + + unsigned extract_horn(expr* fml, app_ref_vector& body, app_ref& head); + /** \brief Perform cheap quantifier elimination to reduce the number of variables in the interpreted tail. */ @@ -99,7 +101,7 @@ namespace datalog { The formula is of the form (forall (...) (forall (...) (=> (and ...) head))) */ - void mk_rule(expr* fml, rule_ref_vector& rules, symbol const& name = symbol::null); + void mk_rule(expr* fml, proof* p, rule_ref_vector& rules, symbol const& name = symbol::null); /** \brief Create a Datalog query from an expression. @@ -129,7 +131,15 @@ namespace datalog { /** make sure there are not non-quantified variables that occur only in interpreted predicates */ void fix_unbound_vars(rule_ref& r, bool try_quantifier_elimination); + /** + \brief add proof that new rule is obtained by rewriting old rule. + */ + void mk_rule_rewrite_proof(rule& old_rule, rule& new_rule); + /** + \brief tag rule as asserted. + */ + void mk_rule_asserted_proof(rule& r); /** \brief apply substitution to variables of rule. @@ -168,6 +178,7 @@ namespace datalog { friend class rule_manager; app * m_head; + proof* m_proof; unsigned m_tail_size:20; // unsigned m_reserve:12; unsigned m_ref_cnt; @@ -199,6 +210,10 @@ namespace datalog { void get_used_vars(used_vars& uv) const; public: + + proof * get_proof() const { return m_proof; } + + void set_proof(ast_manager& m, proof* p); app * get_head() const { return m_head; } diff --git a/src/muz_qe/dl_rule_transformer.cpp b/src/muz_qe/dl_rule_transformer.cpp index a246d9d61..5ecbf2b45 100644 --- a/src/muz_qe/dl_rule_transformer.cpp +++ b/src/muz_qe/dl_rule_transformer.cpp @@ -73,7 +73,7 @@ namespace datalog { m_dirty=true; } - bool rule_transformer::operator()(rule_set & rules, model_converter_ref& mc, proof_converter_ref& pc) { + bool rule_transformer::operator()(rule_set & rules, model_converter_ref& mc) { ensure_ordered(); bool modified = false; @@ -87,7 +87,7 @@ namespace datalog { for(; it!=end && !m_cancel; ++it) { plugin & p = **it; - rule_set * new_rules = p(rules, mc, pc); + rule_set * new_rules = p(rules, mc); if (!new_rules) { continue; } diff --git a/src/muz_qe/dl_rule_transformer.h b/src/muz_qe/dl_rule_transformer.h index cf1a9be75..3b2140caf 100644 --- a/src/muz_qe/dl_rule_transformer.h +++ b/src/muz_qe/dl_rule_transformer.h @@ -24,7 +24,6 @@ Revision History: #include"dl_rule.h" #include"dl_rule_set.h" #include"model_converter.h" -#include"proof_converter.h" namespace datalog { @@ -69,7 +68,7 @@ namespace datalog { \brief Transform the rule set using the registered transformation plugins. If the rule set has changed, return true; otherwise return false. */ - bool operator()(rule_set & rules, model_converter_ref& mc, proof_converter_ref& pc); + bool operator()(rule_set & rules, model_converter_ref& mc); }; class rule_transformer::plugin { @@ -106,8 +105,7 @@ namespace datalog { The caller takes ownership of the returned \c rule_set object. */ virtual rule_set * operator()(rule_set const & source, - model_converter_ref& mc, - proof_converter_ref& pc) = 0; + model_converter_ref& mc) = 0; virtual void cancel() { m_cancel = true; } diff --git a/src/muz_qe/dl_util.cpp b/src/muz_qe/dl_util.cpp index bde03e765..28634d30e 100644 --- a/src/muz_qe/dl_util.cpp +++ b/src/muz_qe/dl_util.cpp @@ -511,6 +511,44 @@ namespace datalog { pc->insert(pr); } + void resolve_rule(rule const& r1, rule const& r2, unsigned idx, + expr_ref_vector const& s1, expr_ref_vector const& s2, rule& res) { + if (!r1.get_proof()) { + return; + } + SASSERT(r2.get_proof()); + ast_manager& m = s1.get_manager(); + expr_ref fml(m); + res.to_formula(fml); + vector substs; + svector > positions; + substs.push_back(s1); + substs.push_back(s2); + + scoped_proof _sc(m); + proof_ref pr(m); + proof_ref_vector premises(m); + premises.push_back(r1.get_proof()); + premises.push_back(r2.get_proof()); + positions.push_back(std::make_pair(idx+1, 0)); + + TRACE("dl", + tout << premises[0]->get_id() << " " << mk_pp(premises[0].get(), m) << "\n"; + for (unsigned i = 0; i < s1.size(); ++i) { + tout << mk_pp(s1[i], m) << " "; + } + tout << "\n"; + tout << premises[1]->get_id() << " " << mk_pp(premises[1].get(), m) << "\n"; + for (unsigned i = 0; i < s2.size(); ++i) { + tout << mk_pp(s2[i], m) << " "; + } + tout << "\n"; + ); + + pr = m.mk_hyper_resolve(2, premises.c_ptr(), fml, positions, substs); + res.set_proof(m, pr); + } + class skip_model_converter : public model_converter { public: skip_model_converter() {} diff --git a/src/muz_qe/dl_util.h b/src/muz_qe/dl_util.h index 45d327d44..e53e6c998 100644 --- a/src/muz_qe/dl_util.h +++ b/src/muz_qe/dl_util.h @@ -425,6 +425,9 @@ namespace datalog { void resolve_rule(replace_proof_converter* pc, rule const& r1, rule const& r2, unsigned idx, expr_ref_vector const& s1, expr_ref_vector const& s2, rule const& res); + void resolve_rule(rule const& r1, rule const& r2, unsigned idx, + expr_ref_vector const& s1, expr_ref_vector const& s2, rule& res); + model_converter* mk_skip_model_converter(); proof_converter* mk_skip_proof_converter(); diff --git a/src/muz_qe/equiv_proof_converter.cpp b/src/muz_qe/equiv_proof_converter.cpp index 53db01900..98ea88044 100644 --- a/src/muz_qe/equiv_proof_converter.cpp +++ b/src/muz_qe/equiv_proof_converter.cpp @@ -22,12 +22,14 @@ Revision History: #include "dl_util.h" void equiv_proof_converter::insert(expr* fml1, expr* fml2) { - datalog::scoped_proof _sp(m); - proof_ref p1(m), p2(m), p3(m); - p1 = m.mk_asserted(fml1); - p2 = m.mk_rewrite(fml1, fml2); - p3 = m.mk_modus_ponens(p1, p2); - TRACE("proof_converter", tout << mk_pp(p3.get(), m) << "\n";); - SASSERT(m.has_fact(p3)); - m_replace.insert(p3); + if (fml1 != fml2) { + datalog::scoped_proof _sp(m); + proof_ref p1(m), p2(m), p3(m); + p1 = m.mk_asserted(fml1); + p2 = m.mk_rewrite(fml1, fml2); + p3 = m.mk_modus_ponens(p1, p2); + TRACE("proof_converter", tout << mk_pp(p3.get(), m) << "\n";); + SASSERT(m.has_fact(p3)); + m_replace.insert(p3); + } } diff --git a/src/muz_qe/horn_tactic.cpp b/src/muz_qe/horn_tactic.cpp index c87874b29..02c41c091 100644 --- a/src/muz_qe/horn_tactic.cpp +++ b/src/muz_qe/horn_tactic.cpp @@ -113,8 +113,8 @@ class horn_tactic : public tactic { todo.append(to_app(a)->get_num_args(), to_app(a)->get_args()); } else if (m.is_ite(a)) { - todo.append(to_app(a)->get_arg(1)); - todo.append(to_app(a)->get_arg(2)); + todo.push_back(to_app(a)->get_arg(1)); + todo.push_back(to_app(a)->get_arg(2)); } else if (is_predicate(a)) { register_predicate(a); @@ -270,20 +270,10 @@ class horn_tactic : public tactic { proof_converter_ref & pc) { expr_ref fml(m); - bool produce_models = g->models_enabled(); - bool produce_proofs = g->proofs_enabled(); - if (produce_models) { - mc = datalog::mk_skip_model_converter(); - } - if (produce_proofs) { - pc = datalog::mk_skip_proof_converter(); - } func_decl* query_pred = to_app(q)->get_decl(); m_ctx.set_output_predicate(query_pred); - m_ctx.set_model_converter(mc); - m_ctx.set_proof_converter(pc); m_ctx.get_rules(); // flush adding rules. m_ctx.apply_default_transformation(); diff --git a/src/muz_qe/pdr_context.cpp b/src/muz_qe/pdr_context.cpp index d6718c33c..d4027d73d 100644 --- a/src/muz_qe/pdr_context.cpp +++ b/src/muz_qe/pdr_context.cpp @@ -950,16 +950,45 @@ namespace pdr { return out; } + /** + \brief Ensure that all nodes in the tree have associated models. + get_trace and get_proof_trace rely on models to extract rules. + */ + void model_search::update_models() { + obj_map models; + ptr_vector todo; + todo.push_back(m_root); + while (!todo.empty()) { + model_node* n = todo.back(); + if (n->get_model_ptr()) { + models.insert(n->state(), n->get_model_ptr()); + } + todo.pop_back(); + todo.append(n->children().size(), n->children().c_ptr()); + } + + todo.push_back(m_root); + while (!todo.empty()) { + model_node* n = todo.back(); + model* md = 0; + if (!n->get_model_ptr() && models.find(n->state(), md)) { + model_ref mr(md); + n->set_model(mr); + } + todo.pop_back(); + todo.append(n->children().size(), n->children().c_ptr()); + } + } + /** Extract trace comprising of constraints and predicates that are satisfied from facts to the query. The resulting trace */ - expr_ref model_search::get_trace(context const& ctx) const { + expr_ref model_search::get_trace(context const& ctx) { pred_transformer& pt = get_root().pt(); ast_manager& m = pt.get_manager(); manager& pm = pt.get_pdr_manager(); - datalog::context& dctx = ctx.get_context(); datalog::rule_manager& rm = dctx.get_rule_manager(); expr_ref_vector constraints(m), predicates(m); @@ -974,13 +1003,15 @@ namespace pdr { rule = n->get_rule(); unsigned max_var = vc.get_max_rule_var(*rule); predicates.push_back(rule->get_head()); - children.append(n); + children.push_back(n); bool first = true; + update_models(); while (!children.empty()) { SASSERT(children.size() == predicates.size()); expr_ref_vector binding(m); n = children.back(); children.pop_back(); + TRACE("pdr", n->display(tout, 0);); n->mk_instantiate(r0, rule, binding); max_var = std::max(max_var, vc.get_max_rule_var(*rule)); @@ -1026,7 +1057,7 @@ namespace pdr { return pm.mk_and(constraints); } - proof_ref model_search::get_proof_trace(context const& ctx) const { + proof_ref model_search::get_proof_trace(context const& ctx) { pred_transformer& pt = get_root().pt(); ast_manager& m = pt.get_manager(); datalog::context& dctx = ctx.get_context(); @@ -1042,8 +1073,10 @@ namespace pdr { proof* pr = 0; unifier.set_normalize(false); todo.push_back(m_root); + update_models(); while (!todo.empty()) { model_node* n = todo.back(); + TRACE("pdr", n->display(tout, 0);); if (cache.find(n->state(), pr)) { todo.pop_back(); continue; @@ -1066,12 +1099,14 @@ namespace pdr { continue; } proof_ref rl(m); - expr_ref fml0(m); expr_ref_vector binding(m); n->mk_instantiate(r0, r1, binding); - r0->to_formula(fml0); proof_ref p1(m), p2(m); - p1 = m.mk_asserted(fml0); + p1 = r0->get_proof(); + if (!p1) { + r0->display(dctx, std::cout); + } + SASSERT(p1); pfs[0] = p1; rls[0] = r1; TRACE("pdr", diff --git a/src/muz_qe/pdr_context.h b/src/muz_qe/pdr_context.h index 32f13cdd4..6aa02ef10 100644 --- a/src/muz_qe/pdr_context.h +++ b/src/muz_qe/pdr_context.h @@ -240,6 +240,7 @@ namespace pdr { void erase_leaf(model_node& n); void remove_node(model_node& n); void enqueue_leaf(model_node& n); // add leaf to priority queue. + void update_models(); public: model_search(bool bfs): m_bfs(bfs), m_root(0) {} ~model_search(); @@ -253,8 +254,8 @@ namespace pdr { void set_root(model_node* n); model_node& get_root() const { return *m_root; } std::ostream& display(std::ostream& out) const; - expr_ref get_trace(context const& ctx) const; - proof_ref get_proof_trace(context const& ctx) const; + expr_ref get_trace(context const& ctx); + proof_ref get_proof_trace(context const& ctx); void backtrack_level(bool uses_level, model_node& n); }; @@ -299,7 +300,7 @@ namespace pdr { decl2rel m_rels; // Map from relation predicate to fp-operator. func_decl_ref m_query_pred; pred_transformer* m_query; - model_search m_search; + mutable model_search m_search; lbool m_last_result; unsigned m_inductive_lvl; ptr_vector m_core_generalizers; diff --git a/src/muz_qe/pdr_dl_interface.cpp b/src/muz_qe/pdr_dl_interface.cpp index b55f302ed..08f7acfdd 100644 --- a/src/muz_qe/pdr_dl_interface.cpp +++ b/src/muz_qe/pdr_dl_interface.cpp @@ -85,6 +85,7 @@ lbool dl_interface::query(expr * query) { m_pred2slice.reset(); ast_manager& m = m_ctx.get_manager(); datalog::rule_manager& rule_manager = m_ctx.get_rule_manager(); + datalog::rule_set old_rules(m_ctx.get_rules()); func_decl_ref query_pred(m); datalog::rule_ref_vector query_rules(rule_manager); @@ -105,14 +106,8 @@ lbool dl_interface::query(expr * query) { m_ctx.display_rules(tout); ); - model_converter_ref mc = datalog::mk_skip_model_converter(); - proof_converter_ref pc; - if (m_ctx.get_params().generate_proof_trace()) { - pc = datalog::mk_skip_proof_converter(); - } + m_ctx.set_output_predicate(query_pred); - m_ctx.set_model_converter(mc); - m_ctx.set_proof_converter(pc); m_ctx.apply_default_transformation(); if (m_ctx.get_params().slice()) { @@ -164,8 +159,8 @@ lbool dl_interface::query(expr * query) { datalog::scoped_restore_proof _sc(m); // update_rules may overwrite the proof mode. - m_context->set_proof_converter(pc); - m_context->set_model_converter(mc); + m_context->set_proof_converter(m_ctx.get_proof_converter()); + m_context->set_model_converter(m_ctx.get_model_converter()); m_context->set_query(query_pred); m_context->set_axioms(bg_assertion); m_context->update_rules(m_pdr_rules); diff --git a/src/muz_qe/pdr_generalizers.cpp b/src/muz_qe/pdr_generalizers.cpp index 4cdfb186e..1b8ea22f9 100644 --- a/src/muz_qe/pdr_generalizers.cpp +++ b/src/muz_qe/pdr_generalizers.cpp @@ -228,11 +228,13 @@ namespace pdr { is_lower = !is_lower; } + vector bound; + bound.push_back(std::make_pair(x, i)); if (is_lower) { - m_lb.insert(abs(r), std::make_pair(x, i)); + m_lb.insert(abs(r), bound); } else { - m_ub.insert(abs(r), std::make_pair(x, i)); + m_ub.insert(abs(r), bound); } } diff --git a/src/muz_qe/qe_lite.cpp b/src/muz_qe/qe_lite.cpp index 5f018895c..be3f80f92 100644 --- a/src/muz_qe/qe_lite.cpp +++ b/src/muz_qe/qe_lite.cpp @@ -2492,7 +2492,13 @@ class qe_lite_tactic : public tactic { new_f = f; m_qe(new_f, new_pr); if (produce_proofs) { - new_pr = m.mk_modus_ponens(g->pr(i), new_pr); + expr* fact = m.get_fact(new_pr); + if (to_app(fact)->get_arg(0) != to_app(fact)->get_arg(1)) { + new_pr = m.mk_modus_ponens(g->pr(i), new_pr); + } + else { + new_pr = g->pr(i); + } } g->update(i, new_f, new_pr, g->dep(i)); } diff --git a/src/muz_qe/tab_context.cpp b/src/muz_qe/tab_context.cpp index 681d3d4b2..9ee059f44 100644 --- a/src/muz_qe/tab_context.cpp +++ b/src/muz_qe/tab_context.cpp @@ -1644,9 +1644,7 @@ namespace datalog { void resolve_rule(replace_proof_converter& pc, tb::clause const& r1, tb::clause const& r2, expr_ref_vector const& s1, expr_ref_vector const& s2, tb::clause const& res) const { unsigned idx = r1.get_predicate_index(); - expr_ref fml1 = r1.to_formula(); - expr_ref fml2 = r2.to_formula(); - expr_ref fml3 = res.to_formula(); + expr_ref fml = res.to_formula(); vector substs; svector > positions; substs.push_back(s1); @@ -1654,13 +1652,12 @@ namespace datalog { scoped_proof _sc(m); proof_ref pr(m); proof_ref_vector premises(m); - premises.push_back(m.mk_asserted(fml1)); - premises.push_back(m.mk_asserted(fml2)); + premises.push_back(m.mk_asserted(r1.to_formula())); + premises.push_back(m.mk_asserted(r2.to_formula())); positions.push_back(std::make_pair(idx+1, 0)); - pr = m.mk_hyper_resolve(2, premises.c_ptr(), fml3, positions, substs); + pr = m.mk_hyper_resolve(2, premises.c_ptr(), fml, positions, substs); pc.insert(pr); - } - + } }; tab::tab(context& ctx): diff --git a/src/util/vector.h b/src/util/vector.h index a9d36b202..704452d0f 100644 --- a/src/util/vector.h +++ b/src/util/vector.h @@ -151,23 +151,6 @@ public: } } - vector(T const & e) : - m_data(0) { - push_back(e); - } - - vector(T const & t1, T const & t2) : - m_data(0) { - push_back(t1); - push_back(t2); - } - - vector(T const & t1, T const & t2, T const & t3) : - m_data(0) { - push_back(t1); - push_back(t2); - push_back(t3); - } ~vector() { destroy();