From f9aeeeef367ecafff815c9758e30a50e75c0d24d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 6 Mar 2013 08:29:29 -0800 Subject: [PATCH] LRA tactic Signed-off-by: Nikolaj Bjorner --- src/muz_qe/pdr_context.cpp | 113 ++++++++++++++++++++----- src/muz_qe/pdr_context.h | 4 +- src/muz_qe/qe_sat_tactic.h | 2 +- src/tactic/smtlogics/quant_tactics.cpp | 8 +- 4 files changed, 99 insertions(+), 28 deletions(-) diff --git a/src/muz_qe/pdr_context.cpp b/src/muz_qe/pdr_context.cpp index 73bffd4e4..348bf9154 100644 --- a/src/muz_qe/pdr_context.cpp +++ b/src/muz_qe/pdr_context.cpp @@ -723,24 +723,17 @@ namespace pdr { m_closed = true; } - expr_ref model_node::get_trace() const { + expr_ref model_node::get_trace(context const& ctx) { pred_transformer& p = pt(); ast_manager& m = p.get_manager(); - manager& pm = p.get_pdr_manager(); - TRACE("pdr", model_smt2_pp(tout, m, get_model(), 0);); - func_decl* f = p.head(); - unsigned arity = f->get_arity(); - model_ref model = get_model_ptr(); - expr_ref_vector args(m); - expr_ref v(m); - model_evaluator mev(m); - - for (unsigned i = 0; i < arity; ++i) { - v = m.mk_const(pm.o2n(p.sig(i),0)); - expr_ref e = mev.eval(model, v); - args.push_back(e); - } - return expr_ref(m.mk_app(f, args.size(), args.c_ptr()), m); + datalog::context& dctx = ctx.get_context(); + datalog::rule_manager& rm = dctx.get_rule_manager(); + datalog::rule_ref r0(rm), r1(rm); + expr_ref_vector binding(m); + expr_ref fml(m); + mk_instantiate(r0, r1, binding); + r1->to_formula(fml); + return fml; } static bool is_ini(datalog::rule const& r) { @@ -961,21 +954,95 @@ namespace pdr { return out; } - expr_ref model_search::get_trace() const { + expr_ref model_search::get_trace(context const& ctx) const { pred_transformer& pt = get_root().pt(); ast_manager& m = pt.get_manager(); manager& pm = pt.get_pdr_manager(); - expr_ref result(m.mk_true(),m); expr_ref_vector rules(m); - ptr_vector nodes; - nodes.push_back(m_root); + expr_ref_vector binding(m); + ptr_vector todo; + datalog::rule_ref r0(rm), r1(rm), r2(rm); + model_node* n = m_root; + todo.push_back(n); + while (!todo.empty()) { + n = todo.back(); + ptr_vector const& chs = n->children(); + rls.push_back(0); + for (unsigned i = 0; i < chs.size(); ++i) { + todo.push_back(chs[i]); + } + if (!chs.empty()) { + continue; + } + expr_ref fml0(m); + binding.reset(); + n->mk_instantiate(r0, r1, binding); + r0->to_formula(fml0); + datalog::rule_ref reduced_rule(rm), r3(rm); + reduced_rule = rls[0]; + // check if binding is identity. + bool binding_is_id = true; + for (unsigned i = 0; binding_is_id && i < binding.size(); ++i) { + expr* v = binding[i].get(); + binding_is_id = is_var(v) && to_var(v)->get_idx() == i; + } + if (rls.size() > 1 || !binding_is_id) { + expr_ref tmp(m); + vector substs; + svector > positions; + substs.push_back(binding); // TODO base substitution. + for (unsigned i = 1; i < rls.size(); ++i) { + datalog::rule& src = *rls[i]; + bool unified = unifier.unify_rules(*reduced_rule, 0, src); + if (!unified) { + IF_VERBOSE(0, + verbose_stream() << "Could not unify rules: "; + reduced_rule->display(dctx, verbose_stream()); + src.display(dctx, verbose_stream());); + } + expr_ref_vector sub1 = unifier.get_rule_subst(*reduced_rule, true); + TRACE("pdr", + for (unsigned k = 0; k < sub1.size(); ++k) { + tout << mk_pp(sub1[k].get(), m) << " "; + } + tout << "\n"; + ); + + for (unsigned j = 0; j < substs.size(); ++j) { + for (unsigned k = 0; k < substs[j].size(); ++k) { + var_subst(m, false)(substs[j][k].get(), sub1.size(), sub1.c_ptr(), tmp); + substs[j][k] = tmp; + } + while (substs[j].size() < sub1.size()) { + substs[j].push_back(sub1[substs[j].size()].get()); + } + } + + positions.push_back(std::make_pair(i,0)); + substs.push_back(unifier.get_rule_subst(src, false)); + VERIFY(unifier.apply(*reduced_rule.get(), 0, src, r3)); + reduced_rule = r3; + } + + expr_ref fml_concl(m); + reduced_rule->to_formula(fml_concl); + p1 = m.mk_hyper_resolve(pfs.size(), pfs.c_ptr(), fml_concl, positions, substs); + + } + cache.insert(n->state(), p1); + rules.insert(n->state(), reduced_rule); + trail.push_back(p1); + rules_trail.push_back(reduced_rule); + todo.pop_back(); + } + while (!nodes.empty()) { model_node* current = nodes.back(); nodes.pop_back(); - rules.push_back(current->get_trace()); + rules.push_back(current->get_trace(ctx)); nodes.append(current->children()); } - return pm.mk_and(rules); + return expr_ref(m.mk_and(rules.size(), rules.c_ptr()), m); } proof_ref model_search::get_proof_trace(context const& ctx) const { @@ -1594,7 +1661,7 @@ namespace pdr { proof_ref pr = get_proof(); return expr_ref(pr.get(), m); } - return m_search.get_trace(); + return m_search.get_trace(*this); } expr_ref context::mk_unsat_answer() const { diff --git a/src/muz_qe/pdr_context.h b/src/muz_qe/pdr_context.h index 7491327dd..412577fb4 100644 --- a/src/muz_qe/pdr_context.h +++ b/src/muz_qe/pdr_context.h @@ -223,7 +223,7 @@ namespace pdr { void set_rule(datalog::rule const* r) { m_rule = r; } datalog::rule* get_rule(); - expr_ref get_trace() const; + expr_ref get_trace(context const& ctx); void mk_instantiate(datalog::rule_ref& r0, datalog::rule_ref& r1, expr_ref_vector& binding); std::ostream& display(std::ostream& out, unsigned indent); @@ -253,7 +253,7 @@ 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() const; + expr_ref get_trace(context const& ctx) const; proof_ref get_proof_trace(context const& ctx) const; void backtrack_level(bool uses_level, model_node& n); }; diff --git a/src/muz_qe/qe_sat_tactic.h b/src/muz_qe/qe_sat_tactic.h index c539216be..15228c534 100644 --- a/src/muz_qe/qe_sat_tactic.h +++ b/src/muz_qe/qe_sat_tactic.h @@ -26,7 +26,7 @@ Revision History: namespace qe { - tactic * mk_sat_tactic(ast_manager& m, params_ref const& p); + tactic * mk_sat_tactic(ast_manager& m, params_ref const& p = params_ref()); }; /* diff --git a/src/tactic/smtlogics/quant_tactics.cpp b/src/tactic/smtlogics/quant_tactics.cpp index 85f53eff0..937b0229e 100644 --- a/src/tactic/smtlogics/quant_tactics.cpp +++ b/src/tactic/smtlogics/quant_tactics.cpp @@ -22,6 +22,7 @@ Revision History: #include"solve_eqs_tactic.h" #include"elim_uncnstr_tactic.h" #include"qe_tactic.h" +#include"qe_sat_tactic.h" #include"ctx_simplify_tactic.h" #include"smt_tactic.h" @@ -98,8 +99,11 @@ tactic * mk_aufnira_tactic(ast_manager & m, params_ref const & p) { tactic * mk_lra_tactic(ast_manager & m, params_ref const & p) { tactic * st = and_then(mk_quant_preprocessor(m), - mk_qe_tactic(m), - mk_smt_tactic()); + or_else(try_for(mk_smt_tactic(), 100), + try_for(qe::mk_sat_tactic(m), 1000), + try_for(mk_smt_tactic(), 1000), + and_then(mk_qe_tactic(m), mk_smt_tactic()))); + st->updt_params(p); return st; }