From ec21c7bbc5953d08a08bd05c6329a4c242b0c114 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 21 Nov 2012 16:54:41 -0800 Subject: [PATCH] rewrite quantifier module Signed-off-by: Nikolaj Bjorner --- src/muz_qe/pdr_context.cpp | 48 +--- src/muz_qe/pdr_context.h | 17 +- src/muz_qe/pdr_dl_interface.cpp | 23 +- src/muz_qe/pdr_quantifiers.cpp | 420 +++++++++++++++++--------------- src/muz_qe/pdr_quantifiers.h | 63 ++--- 5 files changed, 275 insertions(+), 296 deletions(-) diff --git a/src/muz_qe/pdr_context.cpp b/src/muz_qe/pdr_context.cpp index 451ec2e7d..404e81c24 100644 --- a/src/muz_qe/pdr_context.cpp +++ b/src/muz_qe/pdr_context.cpp @@ -65,10 +65,6 @@ namespace pdr { m_reachable(pm, pm.get_params()) {} pred_transformer::~pred_transformer() { - qinst_map::iterator it = m_rule2qinst.begin(), end = m_rule2qinst.end(); - for (; it != end; ++it) { - dealloc(it->m_value); - } rule2inst::iterator it2 = m_rule2inst.begin(), end2 = m_rule2inst.end(); for (; it2 != end2; ++it2) { dealloc(it2->m_value); @@ -556,7 +552,6 @@ namespace pdr { // positions the variables occur are made equivalent with these. expr_ref_vector conj(m); app_ref_vector& var_reprs = *(alloc(app_ref_vector, m)); - qinst* qi = 0; ptr_vector aux_vars; unsigned ut_size = rule.get_uninterpreted_tail_size(); @@ -581,19 +576,6 @@ namespace pdr { for (unsigned i = 0; i < tail.size(); ++i) { expr_ref tmp(m); var_subst(m, false)(tail[i].get(), var_reprs.size(), (expr*const*)var_reprs.c_ptr(), tmp); - quantifier* q; - if (datalog::rule_manager::is_forall(m, tmp, q)) { - - if (!qi) { - qi = alloc(qinst, m); - } - // - // The contract is to instantiate q with - // sufficient witnesses to validate body. - // - qi->quantifiers.push_back(q); - tmp = m.mk_true(); - } conj.push_back(tmp); TRACE("pdr", tout << mk_pp(tail[i].get(), m) << "\n" << mk_pp(tmp, m) << "\n";); SASSERT(is_ground(tmp)); @@ -607,12 +589,10 @@ namespace pdr { TRACE("pdr", tout << mk_pp(fml, m) << "\n";); SASSERT(is_ground(fml)); if (m.is_false(fml)) { - dealloc(qi); - qi = 0; // no-op. } else { - if (ut_size == 0 && !qi) { + if (ut_size == 0) { init = m.mk_or(init, fml); } transitions.push_back(fml); @@ -620,9 +600,6 @@ namespace pdr { m_rule2transition.insert(&rule, fml.get()); rules.push_back(&rule); } - if (qi) { - m_rule2qinst.insert(&rule, qi); - } m_rule2inst.insert(&rule,&var_reprs); m_rule2vars.insert(&rule, aux_vars); } @@ -1119,7 +1096,6 @@ namespace pdr { m_params(params), m(m), m_context(0), - m_quantifier_inst(*this, m), m_pm(m_fparams, m_params, m), m_query_pred(m), m_query(0), @@ -1491,7 +1467,6 @@ namespace pdr { UNREACHABLE(); } catch (model_exception) { - check_quantifiers(); IF_VERBOSE(1, verbose_stream() << "\n"; m_search.display(verbose_stream());); m_last_result = l_true; validate(); @@ -1605,24 +1580,6 @@ namespace pdr { } } - // - // Check that quantifiers are satisfied in the produced model. - // - void context::check_quantifiers() { - if (has_quantifiers()) { - m_quantifier_inst.model_check(m_search.get_root()); - } - } - - bool context::has_quantifiers() const { - decl2rel const& dr = get_pred_transformers(); - decl2rel::iterator it = dr.begin(), end = dr.end(); - for (; it != end; ++it) { - pred_transformer* pt = it->m_value; - if (pt->has_quantifiers()) return true; - } - return false; - } // // Pick a potential counter example state. @@ -1832,8 +1789,7 @@ namespace pdr { for (unsigned i = 0; i < sig_size; ++i) { vars.push_back(m.mk_const(m_pm.o2n(pt.sig(i), 0))); } - ptr_vector aux_vars; - pt.get_aux_vars(r, aux_vars); + ptr_vector& aux_vars = pt.get_aux_vars(r); vars.append(aux_vars.size(), aux_vars.c_ptr()); scoped_ptr rep; diff --git a/src/muz_qe/pdr_context.h b/src/muz_qe/pdr_context.h index 14be82dae..4b578a188 100644 --- a/src/muz_qe/pdr_context.h +++ b/src/muz_qe/pdr_context.h @@ -29,7 +29,6 @@ Revision History: #include "dl_base.h" #include "pdr_prop_solver.h" #include "pdr_reachable_cache.h" -#include "pdr_quantifiers.h" namespace datalog { class rule_set; @@ -42,7 +41,6 @@ namespace pdr { class model_node; class context; - typedef obj_map qinst_map; typedef obj_map rule2inst; typedef obj_map decl2rel; @@ -78,7 +76,6 @@ namespace pdr { obj_map m_prop2level; // map property to level where it occurs. obj_map m_tag2rule; // map tag predicate to rule. rule2expr m_rule2tag; // map rule to predicate tag. - qinst_map m_rule2qinst; // map tag to quantifier instantiation. rule2inst m_rule2inst; // map rules to instantiations of indices rule2expr m_rule2transition; // map rules to transition rule2apps m_rule2vars; // map rule to auxiliary variables @@ -99,7 +96,6 @@ namespace pdr { void init_rule(decl2rel const& pts, datalog::rule const& rule, expr_ref& init, ptr_vector& rules, expr_ref_vector& transition); void init_atom(decl2rel const& pts, app * atom, app_ref_vector& var_reprs, expr_ref_vector& conj, unsigned tail_idx); - void ground_free_vars(expr* e, app_ref_vector& vars, ptr_vector& aux_vars); void simplify_formulas(tactic& tac, expr_ref_vector& fmls); @@ -122,8 +118,6 @@ namespace pdr { func_decl* const* sig() { init_sig(); return m_sig.c_ptr(); } expr* transition() const { return m_transition; } expr* initial_state() const { return m_initial_state; } - bool has_quantifiers() const { return !m_rule2qinst.empty(); } - qinst* get_quantifiers(datalog::rule const* r) const { qinst* q = 0; m_rule2qinst.find(r, q); return q; } expr* rule2tag(datalog::rule const* r) { return m_rule2tag.find(r); } unsigned get_num_levels() { return m_levels.size(); } expr_ref get_cover_delta(func_decl* p_orig, int level); @@ -140,7 +134,7 @@ namespace pdr { void find_predecessors(model_core const& model, ptr_vector& preds) const; datalog::rule const& find_rule(model_core const& model) const; expr* get_transition(datalog::rule const& r) { return m_rule2transition.find(&r); } - void get_aux_vars(datalog::rule const& r, ptr_vector& vs) { m_rule2vars.find(&r, vs); } + ptr_vector& get_aux_vars(datalog::rule const& r) { return m_rule2vars.find(&r); } bool propagate_to_next_level(unsigned level); void add_property(expr * lemma, unsigned lvl); // add property 'p' to state at level. @@ -166,6 +160,8 @@ namespace pdr { void inherit_properties(pred_transformer& other); + void ground_free_vars(expr* e, app_ref_vector& vars, ptr_vector& aux_vars); + }; @@ -292,7 +288,6 @@ namespace pdr { params_ref const& m_params; ast_manager& m; datalog::context* m_context; - quantifier_model_checker m_quantifier_inst; manager m_pm; decl2rel m_rels; // Map from relation predicate to fp-operator. func_decl_ref m_query_pred; @@ -309,8 +304,6 @@ namespace pdr { // Functions used by search. void solve_impl(); bool check_reachability(unsigned level); - void check_quantifiers(); - bool has_quantifiers() const; void propagate(unsigned max_prop_lvl); void close_node(model_node& n); void check_pre_closed(model_node& n); @@ -396,8 +389,6 @@ namespace pdr { void set_axioms(expr* axioms) { m_pm.set_background(axioms); } - void refine(qi& q, datalog::rule_set& rules) { m_quantifier_inst.refine(q, rules); } - unsigned get_num_levels(func_decl* p); expr_ref get_cover_delta(int level, func_decl* p_orig, func_decl* p); @@ -408,6 +399,8 @@ namespace pdr { proof_ref get_proof() const; + model_node& get_root() const { return m_search.get_root(); } + }; }; diff --git a/src/muz_qe/pdr_dl_interface.cpp b/src/muz_qe/pdr_dl_interface.cpp index 532019025..eced4c128 100644 --- a/src/muz_qe/pdr_dl_interface.cpp +++ b/src/muz_qe/pdr_dl_interface.cpp @@ -25,6 +25,7 @@ Revision History: #include "dl_mk_rule_inliner.h" #include "dl_rule.h" #include "dl_rule_transformer.h" +#include "dl_mk_extract_quantifiers.h" #include "smt2parser.h" #include "pdr_context.h" #include "pdr_dl_interface.h" @@ -32,6 +33,7 @@ Revision History: #include "dl_mk_slice.h" #include "dl_mk_unfold.h" #include "dl_mk_coalesce.h" +#include "pdr_quantifiers.h" using namespace pdr; @@ -145,12 +147,20 @@ lbool dl_interface::query(expr * query) { } } + // remove universal quantifiers from body. + datalog::mk_extract_quantifiers* extract_quantifiers = alloc(datalog::mk_extract_quantifiers, m_ctx); + datalog::rule_transformer extract_q_tr(m_ctx); + extract_q_tr.register_plugin(extract_quantifiers); + m_ctx.transform_rules(extract_q_tr, mc, pc); + + IF_VERBOSE(2, m_ctx.display_rules(verbose_stream());); m_pdr_rules.add_rules(m_ctx.get_rules()); m_pdr_rules.close(); m_ctx.reopen(); m_ctx.replace_rules(old_rules); + quantifier_model_checker quantifier_mc(*m_context, m, extract_quantifiers->quantifiers(), m_pdr_rules); m_context->set_proof_converter(pc); m_context->set_model_converter(mc); @@ -163,12 +173,17 @@ lbool dl_interface::query(expr * query) { return l_false; } + lbool result; while (true) { - try { - return m_context->solve(); + result = m_context->solve(); + if (result == l_true && extract_quantifiers->has_quantifiers()) { + if (quantifier_mc.check()) { + return l_true; + } + // else continue } - catch (pdr::qi& q) { - m_context->refine(q, m_pdr_rules); + else { + return result; } } } diff --git a/src/muz_qe/pdr_quantifiers.cpp b/src/muz_qe/pdr_quantifiers.cpp index 362575a8b..d52a0bf07 100644 --- a/src/muz_qe/pdr_quantifiers.cpp +++ b/src/muz_qe/pdr_quantifiers.cpp @@ -115,166 +115,21 @@ namespace pdr { var_subst vs(m, false); vs(q->get_expr(), binding.size(), binding.c_ptr(), e); (*rep)(e); - m_rules.push_back(m_current_rule); - m_apps.push_back(to_app(e)); + m_instantiated_rules.push_back(m_current_rule); + m_instantiations.push_back(to_app(e)); TRACE("pdr", tout << mk_pp(e, m) << "\n";); } - void quantifier_model_checker::model_check(model_node& root) { - m_apps.reset(); - m_rules.reset(); - ptr_vector nodes; - get_nodes(root, nodes); - for (unsigned i = nodes.size(); i > 0; ) { - --i; - model_check_node(*nodes[i]); - } - if (m_apps.empty()) { - return; - } - qi q(m); - for (unsigned i = 0; i < m_apps.size(); ++i) { - q.add(m_rules[i], m_apps[i].get()); - } - throw q; - } // As & not Body_i is satisfiable // then instantiate with model for parameters to Body_i - bool quantifier_model_checker::find_instantiations(qinst& qi, unsigned level) { + bool quantifier_model_checker::find_instantiations(quantifier_ref_vector const& qs, unsigned level) { return - find_instantiations_proof_based(qi, level); // || - // find_instantiations_qe_based(qi, level); + find_instantiations_proof_based(qs, level); // || + // find_instantiations_qe_based(qs, level); } - bool quantifier_model_checker::find_instantiations_model_based(qinst& qi, unsigned level) { - bool found_instance = false; - expr_ref C(m); - front_end_params fparams; - smt::kernel solver(m, fparams); - solver.assert_expr(m_A); - for (unsigned i = 0; i < m_Bs.size(); ++i) { - expr_ref_vector fresh_vars(m); - quantifier* q = qi.quantifiers[i].get(); - for (unsigned j = 0; j < q->get_num_decls(); ++j) { - fresh_vars.push_back(m.mk_fresh_const("V",q->get_decl_sort(j))); - } - var_subst varsubst(m, false); - varsubst(m_Bs[i].get(), fresh_vars.size(), fresh_vars.c_ptr(), C); - TRACE("pdr", tout << "updated propagation formula: " << mk_pp(C,m) << "\n";); - - solver.push(); - // TBD: what to do with the different tags when unfolding the same predicate twice? - solver.assert_expr(m.mk_not(C)); - lbool result = solver.check(); - if (result == l_true) { - found_instance = true; - model_ref mr; - solver.get_model(mr); - TRACE("pdr", model_smt2_pp(tout, m, *mr, 0);); - - expr_ref_vector insts(m); - for (unsigned j = 0; j < fresh_vars.size(); ++j) { - expr* interp = mr->get_const_interp(to_app(fresh_vars[j].get())->get_decl()); - if (interp) { - insts.push_back(interp); - } - else { - insts.push_back(fresh_vars[j].get()); - } - TRACE("pdr", tout << mk_pp(insts.back(), m) << "\n";); - } - add_binding(q, insts); - } - solver.pop(1); - } - return found_instance; - } - - // - // Build: - // - // A & forall x . B1 & forall y . B2 & ... - // = - // not exists x y . (!A or !B1 or !B2 or ...) - // - // Find an instance that satisfies formula. - // (or find all instances?) - // - bool quantifier_model_checker::find_instantiations_qe_based(qinst& qi, unsigned level) { - expr_ref_vector fmls(m), conjs(m), fresh_vars(m); - app_ref_vector all_vars(m); - expr_ref C(m); - qe::def_vector defs(m); - front_end_params fparams; - qe::expr_quant_elim qe(m, fparams); - for (unsigned i = 0; i < m_Bs.size(); ++i) { - quantifier* q = qi.quantifiers[i].get(); - unsigned num_decls = q->get_num_decls(); - unsigned offset = all_vars.size(); - for (unsigned j = 0; j < num_decls; ++j) { - all_vars.push_back(m.mk_fresh_const("V",q->get_decl_sort(j))); - } - var_subst varsubst(m, false); - varsubst(m_Bs[i].get(), num_decls, (expr**)(all_vars.c_ptr() + offset), C); - fmls.push_back(C); - } - conjs.push_back(m_A); - conjs.push_back(m.mk_not(m.mk_and(fmls.size(), fmls.c_ptr()))); - // add previous instances. - expr* r = m.mk_and(m_Bs.size(), m_Bs.c_ptr()); - m_trail.push_back(r); - expr* inst; - if (!m_bound.find(m_current_rule, r, inst)) { - TRACE("pdr", tout << "did not find: " << mk_pp(r, m) << "\n";); - m_trail.push_back(r); - inst = m.mk_true(); - m_bound.insert(m_current_rule, r, inst); - } - else { - TRACE("pdr", tout << "blocking: " << mk_pp(inst, m) << "\n";); - conjs.push_back(inst); - } - C = m.mk_and(conjs.size(), conjs.c_ptr()); - lbool result = qe.first_elim(all_vars.size(), all_vars.c_ptr(), C, defs); - TRACE("pdr", tout << mk_pp(C.get(), m) << "\n" << result << "\n";); - if (result != l_true) { - return false; - } - inst = m.mk_and(inst, m.mk_not(C)); - m_trail.push_back(inst); - m_bound.insert(m_current_rule, r, inst); - TRACE("pdr", - tout << "Instantiating\n"; - for (unsigned i = 0; i < defs.size(); ++i) { - tout << defs.var(i)->get_name() << " " << mk_pp(defs.def(i), m) << "\n"; - } - ); - expr_substitution sub(m); - for (unsigned i = 0; i < defs.size(); ++i) { - sub.insert(m.mk_const(defs.var(i)), defs.def(i)); - } - scoped_ptr rep = mk_default_expr_replacer(m); - rep->set_substitution(&sub); - for (unsigned i = 0; i < all_vars.size(); ++i) { - expr_ref tmp(all_vars[i].get(), m); - (*rep)(tmp); - all_vars[i] = to_app(tmp); - } - unsigned offset = 0; - for (unsigned i = 0; i < m_Bs.size(); ++i) { - quantifier* q = qi.quantifiers[i].get(); - unsigned num_decls = q->get_num_decls(); - expr_ref_vector new_binding(m); - for (unsigned j = 0; j < num_decls; ++j) { - new_binding.push_back(all_vars[offset+j].get()); - } - offset += num_decls; - add_binding(q, new_binding); - } - return true; - } class collect_insts { ast_manager& m; @@ -322,7 +177,7 @@ namespace pdr { }; - bool quantifier_model_checker::find_instantiations_proof_based(qinst& qi, unsigned level) { + bool quantifier_model_checker::find_instantiations_proof_based(quantifier_ref_vector const& qs, unsigned level) { bool found_instance = false; TRACE("pdr", tout << mk_pp(m_A,m) << "\n";); @@ -336,7 +191,7 @@ namespace pdr { expr_ref C(m); fmls.push_back(tr(m_A.get())); for (unsigned i = 0; i < m_Bs.size(); ++i) { - C = m.update_quantifier(qi.quantifiers[i].get(), m_Bs[i].get()); + C = m.update_quantifier(qs[i], m_Bs[i].get()); fmls.push_back(tr(C.get())); } TRACE("pdr", @@ -355,8 +210,8 @@ namespace pdr { } map qid_map; quantifier* q; - for (unsigned i = 0; i < qi.quantifiers.size(); ++i) { - q = qi.quantifiers[i].get(); + for (unsigned i = 0; i < qs.size(); ++i) { + q = qs[i]; qid_map.insert(q->get_qid(), q); } @@ -391,7 +246,7 @@ namespace pdr { if (collector.size() == 0) { // Try to create dummy instances. for (unsigned i = 0; i < m_Bs.size(); ++i) { - q = qi.quantifiers[i].get(); + q = qs[i]; expr_ref_vector binding(m); for (unsigned j = 0; j < q->get_num_decls(); ++j) { binding.push_back(m.mk_fresh_const("B", q->get_decl_sort(j))); @@ -403,7 +258,6 @@ namespace pdr { return found_instance; } - void quantifier_model_checker::model_check_node(model_node& node) { TRACE("pdr", node.display(tout, 0);); pred_transformer& pt = node.pt(); @@ -411,9 +265,6 @@ namespace pdr { expr_ref A(m), B(m), C(m); expr_ref_vector As(m); m_Bs.reset(); - if (!pt.has_quantifiers()) { - return; - } // // nodes from leaves that are repeated // inside the search tree don't have models. @@ -427,10 +278,12 @@ namespace pdr { if (!m_current_rule) { return; } - qinst* qi = pt.get_quantifiers(m_current_rule); - if (!qi) { + + quantifier_ref_vector* qis = 0; + m_quantifiers.find(m_current_rule, qis); + if (!qis) { return; - } + } unsigned level = node.level(); unsigned previous_level = (level == 0)?0:(level-1); @@ -440,42 +293,69 @@ namespace pdr { m_A = pm.mk_and(As); // Add quantifiers: - scoped_ptr rep = mk_default_expr_replacer(m); - for (unsigned j = 0; j < qi->quantifiers.size(); ++j) { - quantifier* q = qi->quantifiers[j].get(); - app* a = to_app(q->get_expr()); - func_decl* f = a->get_decl(); - pred_transformer& pt2 = m_ctx.get_pred_transformer(f); - B = pt2.get_formulas(previous_level, true); - TRACE("pdr", tout << mk_pp(B, m) << "\n";); - - expr_substitution sub(m); - for (unsigned i = 0; i < a->get_num_args(); ++i) { - expr* v = m.mk_const(pm.o2n(pt2.sig(i),0)); - sub.insert(v, a->get_arg(i)); + + { + datalog::scoped_no_proof _no_proof(m); + scoped_ptr rep = mk_default_expr_replacer(m); + for (unsigned j = 0; j < qis->size(); ++j) { + quantifier* q = (*qis)[j].get(); + app* a = to_app(q->get_expr()); + func_decl* f = a->get_decl(); + pred_transformer& pt2 = m_ctx.get_pred_transformer(f); + B = pt2.get_formulas(previous_level, true); + + expr_substitution sub(m); + expr_ref_vector refs(m); + for (unsigned i = 0; i < a->get_num_args(); ++i) { + expr* v = m.mk_const(pm.o2n(pt2.sig(i),0)); + sub.insert(v, a->get_arg(i)); + refs.push_back(v); + } + rep->set_substitution(&sub); + (*rep)(B); + app_ref_vector& inst = pt.get_inst(m_current_rule); + ptr_vector& aux_vars = pt.get_aux_vars(*m_current_rule); + pt.ground_free_vars(B, inst, aux_vars); + var_subst vs(m, false); + vs(B, inst.size(), (expr*const*)inst.c_ptr(), B); + m_Bs.push_back(B); } - rep->set_substitution(&sub); - // TBD: exclude previous bindings here. - (*rep)(B); - m_Bs.push_back(B); - TRACE("pdr", - tout << mk_pp(q, m) << "\n"; - tout << "propagation formula: " << mk_pp(B, m) << "\n";); } - find_instantiations(*qi, level); + + TRACE("pdr", + tout << "A:\n" << mk_pp(m_A, m) << "\n"; + tout << "B:\n"; + for (unsigned i = 0; i < m_Bs.size(); ++i) { + tout << mk_pp((*qis)[i].get(), m) << "\n" << mk_pp(m_Bs[i].get(), m) << "\n"; + } + ); + + find_instantiations(*qis, level); } - void quantifier_model_checker::refine(qi& q, datalog::rule_set& rules) { + bool quantifier_model_checker::model_check(model_node& root) { + m_instantiations.reset(); + m_instantiated_rules.reset(); + ptr_vector nodes; + get_nodes(root, nodes); + for (unsigned i = nodes.size(); i > 0; ) { + --i; + model_check_node(*nodes[i]); + } + return m_instantiations.empty(); + } + + void quantifier_model_checker::refine() { IF_VERBOSE(1, verbose_stream() << "instantiating quantifiers\n";); - datalog::rule_manager& rule_m = rules.get_rule_manager(); - datalog::rule_set new_rules(rules.get_context()); - datalog::rule_set::iterator it = rules.begin(), end = rules.end(); + datalog::rule_manager& rule_m = m_rules.get_rule_manager(); + datalog::rule_set new_rules(m_rules.get_context()); + datalog::rule_set::iterator it = m_rules.begin(), end = m_rules.end(); for (; it != end; ++it) { datalog::rule* r = *it; - app_ref_vector body(m); - for (unsigned i = 0; i < q.size(); ++i) { - if (r == q.get_rule(i)) { - body.push_back(q.get_app(i)); + expr_ref_vector body(m); + for (unsigned i = 0; i < m_instantiations.size(); ++i) { + if (r == m_instantiated_rules[i]) { + body.push_back(m_instantiations[i].get()); } } if (body.empty()) { @@ -485,19 +365,165 @@ namespace pdr { for (unsigned i = 0; i < r->get_tail_size(); ++i) { body.push_back(r->get_tail(i)); } + quantifier_ref_vector* qs = 0; + m_quantifiers.find(r, qs); + m_quantifiers.remove(r); datalog::rule_ref_vector rules(rule_m); - expr_ref rule(m.mk_implies(m.mk_and(body.size(), (expr*const*)body.c_ptr()), r->get_head()), m); + expr_ref rule(m.mk_implies(m.mk_and(body.size(), body.c_ptr()), r->get_head()), m); rule_m.mk_rule(rule, rules, r->name()); for (unsigned i = 0; i < rules.size(); ++i) { new_rules.add_rule(rules[i].get()); + m_quantifiers.insert(rules[i].get(), qs); } } } new_rules.close(); - rules.reset(); - rules.add_rules(new_rules); - rules.close(); - m_ctx.update_rules(rules); - TRACE("pdr", rules.display(tout);); + m_rules.reset(); + m_rules.add_rules(new_rules); + m_rules.close(); + m_ctx.update_rules(m_rules); + TRACE("pdr", m_rules.display(tout);); + } + + bool quantifier_model_checker::check() { + if (model_check(m_ctx.get_root())) { + return true; + } + refine(); + return false; } }; + + +#if 0 + // + // Build: + // + // A & forall x . B1 & forall y . B2 & ... + // = + // not exists x y . (!A or !B1 or !B2 or ...) + // + // Find an instance that satisfies formula. + // (or find all instances?) + // + bool quantifier_model_checker::find_instantiations_qe_based(quantifier_ref_vector const& qs, unsigned level) { + expr_ref_vector fmls(m), conjs(m), fresh_vars(m); + app_ref_vector all_vars(m); + expr_ref C(m); + qe::def_vector defs(m); + front_end_params fparams; + qe::expr_quant_elim qe(m, fparams); + for (unsigned i = 0; i < m_Bs.size(); ++i) { + quantifier* q = qs[i]; + unsigned num_decls = q->get_num_decls(); + unsigned offset = all_vars.size(); + for (unsigned j = 0; j < num_decls; ++j) { + all_vars.push_back(m.mk_fresh_const("V",q->get_decl_sort(j))); + } + var_subst varsubst(m, false); + varsubst(m_Bs[i].get(), num_decls, (expr**)(all_vars.c_ptr() + offset), C); + fmls.push_back(C); + } + conjs.push_back(m_A); + conjs.push_back(m.mk_not(m.mk_and(fmls.size(), fmls.c_ptr()))); + // add previous instances. + expr* r = m.mk_and(m_Bs.size(), m_Bs.c_ptr()); + m_trail.push_back(r); + expr* inst; + if (!m_bound.find(m_current_rule, r, inst)) { + TRACE("pdr", tout << "did not find: " << mk_pp(r, m) << "\n";); + m_trail.push_back(r);Newton Sanches + inst = m.mk_true(); + m_bound.insert(m_current_rule, r, inst); + } + else { + TRACE("pdr", tout << "blocking: " << mk_pp(inst, m) << "\n";); + conjs.push_back(inst); + } + C = m.mk_and(conjs.size(), conjs.c_ptr()); + lbool result = qe.first_elim(all_vars.size(), all_vars.c_ptr(), C, defs); + TRACE("pdr", tout << mk_pp(C.get(), m) << "\n" << result << "\n";); + if (result != l_true) { + return false; + } + inst = m.mk_and(inst, m.mk_not(C)); + m_trail.push_back(inst); + m_bound.insert(m_current_rule, r, inst); + TRACE("pdr", + tout << "Instantiating\n"; + for (unsigned i = 0; i < defs.size(); ++i) { + tout << defs.var(i)->get_name() << " " << mk_pp(defs.def(i), m) << "\n"; + } + ); + expr_substitution sub(m); + for (unsigned i = 0; i < defs.size(); ++i) { + sub.insert(m.mk_const(defs.var(i)), defs.def(i)); + } + scoped_ptr rep = mk_default_expr_replacer(m); + rep->set_substitution(&sub); + for (unsigned i = 0; i < all_vars.size(); ++i) { + expr_ref tmp(all_vars[i].get(), m); + (*rep)(tmp); + all_vars[i] = to_app(tmp); + } + unsigned offset = 0; + for (unsigned i = 0; i < m_Bs.size(); ++i) { + quantifier* q = qs[i]; + unsigned num_decls = q->get_num_decls(); + expr_ref_vector new_binding(m); + for (unsigned j = 0; j < num_decls; ++j) { + new_binding.push_back(all_vars[offset+j].get()); + } + offset += num_decls; + add_binding(q, new_binding); + } + return true; + } + + bool quantifier_model_checker::find_instantiations_model_based(quantifier_ref_vector const& qs, unsigned level) { + bool found_instance = false; + expr_ref C(m); + front_end_params fparams; + smt::kernel solver(m, fparams); + solver.assert_expr(m_A); + for (unsigned i = 0; i < m_Bs.size(); ++i) { + expr_ref_vector fresh_vars(m); + quantifier* q = qs[i]; + for (unsigned j = 0; j < q->get_num_decls(); ++j) { + fresh_vars.push_back(m.mk_fresh_const("V",q->get_decl_sort(j))); + } + var_subst varsubst(m, false); + varsubst(m_Bs[i].get(), fresh_vars.size(), fresh_vars.c_ptr(), C); + TRACE("pdr", tout << "updated propagation formula: " << mk_pp(C,m) << "\n";); + + solver.push(); + // TBD: what to do with the different tags when unfolding the same predicate twice? + solver.assert_expr(m.mk_not(C)); + lbool result = solver.check(); + if (result == l_true) { + found_instance = true; + model_ref mr; + solver.get_model(mr); + TRACE("pdr", model_smt2_pp(tout, m, *mr, 0);); + + expr_ref_vector insts(m); + for (unsigned j = 0; j < fresh_vars.size(); ++j) { + expr* interp = mr->get_const_interp(to_app(fresh_vars[j].get())->get_decl()); + if (interp) { + insts.push_back(interp); + } + else { + insts.push_back(fresh_vars[j].get()); + } + TRACE("pdr", tout << mk_pp(insts.back(), m) << "\n";); + } + add_binding(q, insts); + } + solver.pop(1); + } + return found_instance; + } + + +#endif + diff --git a/src/muz_qe/pdr_quantifiers.h b/src/muz_qe/pdr_quantifiers.h index 45e8640e4..bae323cf8 100644 --- a/src/muz_qe/pdr_quantifiers.h +++ b/src/muz_qe/pdr_quantifiers.h @@ -33,52 +33,31 @@ namespace pdr { class model_node; class pred_transformer; class context; - - struct qinst { - quantifier_ref_vector quantifiers; // quantifiers in rule body. - func_decl_ref_vector predicates; // predicates in order of bindings. - expr_ref_vector bindings; // the actual instantiations of the predicates - qinst(ast_manager& m): quantifiers(m), predicates(m), bindings(m) {} - }; - - class qi { - ptr_vector m_rules; - app_ref_vector m_apps; - public: - qi(ast_manager& m) : m_apps(m) {} - void add(datalog::rule const* r, app* a) { - m_rules.push_back(r); - m_apps.push_back(a); - } - unsigned size() const { return m_rules.size(); } - datalog::rule const* get_rule(unsigned i) const { return m_rules[i]; } - app* get_app(unsigned i) const { return m_apps[i]; } - }; class quantifier_model_checker { context& m_ctx; ast_manager& m; - obj_pair_map m_bound; + obj_map& m_quantifiers; + datalog::rule_set& m_rules; expr_ref_vector m_trail; expr_ref m_A; expr_ref_vector m_Bs; pred_transformer* m_current_pt; datalog::rule const* m_current_rule; model_node* m_current_node; - - ptr_vector m_rules; - app_ref_vector m_apps; + app_ref_vector m_instantiations; + ptr_vector m_instantiated_rules; void model_check_node(model_node& node); - bool find_instantiations(qinst& qi, unsigned level); + bool find_instantiations(quantifier_ref_vector const& qs, unsigned level); - bool find_instantiations_model_based(qinst& qi, unsigned level); + bool find_instantiations_model_based(quantifier_ref_vector const& qs, unsigned level); - bool find_instantiations_proof_based(qinst& qi, unsigned level); + bool find_instantiations_proof_based(quantifier_ref_vector const& qs, unsigned level); - bool find_instantiations_qe_based(qinst& qi, unsigned level); + bool find_instantiations_qe_based(quantifier_ref_vector const& qs, unsigned level); void add_binding(quantifier* q, expr_ref_vector& binding); @@ -88,12 +67,8 @@ namespace pdr { void generalize_binding(expr_ref_vector const& binding, unsigned idx, expr_ref_vector& new_binding, vector& bindings); - public: - quantifier_model_checker(context& ctx, ast_manager& m): - m_ctx(ctx), - m(m), m_trail(m), m_A(m), m_Bs(m), - m_current_pt(0), m_current_rule(0), - m_current_node(0), m_apps(m) {} + void refine(); + /** \brief model check a potential model against quantifiers in bodies of rules. @@ -102,9 +77,23 @@ namespace pdr { 'false' and a set of instantiations that contradict the current model. */ - void model_check(model_node& root); + bool model_check(model_node& root); - void refine(qi& q, datalog::rule_set& rules); + public: + quantifier_model_checker( + context& ctx, + ast_manager& m, + obj_map& quantifiers, + datalog::rule_set& rules) : + m_ctx(ctx), + m(m), + m_quantifiers(quantifiers), + m_rules(rules), + m_trail(m), m_A(m), m_Bs(m), + m_current_pt(0), m_current_rule(0), + m_current_node(0), m_instantiations(m) {} + + bool check(); }; };