From 87e9015675c2e14ca35ad0853e4c8ece6641af21 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 20 Jan 2013 18:41:41 -0800 Subject: [PATCH] working on tab_context Signed-off-by: Nikolaj Bjorner --- src/ast/substitution/substitution.cpp | 1 + src/muz_qe/qe_lite.cpp | 210 ++++++-- src/muz_qe/tab_context.cpp | 680 +++++++++++++++++++------- 3 files changed, 662 insertions(+), 229 deletions(-) diff --git a/src/ast/substitution/substitution.cpp b/src/ast/substitution/substitution.cpp index 2420a4d3f..82d1fbfef 100644 --- a/src/ast/substitution/substitution.cpp +++ b/src/ast/substitution/substitution.cpp @@ -58,6 +58,7 @@ void substitution::pop_scope(unsigned num_scopes) { } m_vars.shrink(old_sz); m_scopes.shrink(new_lvl); + m_apply_cache.reset(); } inline void substitution::apply_visit(expr_offset const & n, bool & visited) { diff --git a/src/muz_qe/qe_lite.cpp b/src/muz_qe/qe_lite.cpp index 6949c4264..53702700e 100644 --- a/src/muz_qe/qe_lite.cpp +++ b/src/muz_qe/qe_lite.cpp @@ -36,6 +36,7 @@ Revision History: #include "for_each_expr.h" #include "expr_safe_replace.h" #include "cooperate.h" +#include "datatype_decl_plugin.h" class is_variable_proc { public: @@ -80,6 +81,7 @@ namespace eq { class der { ast_manager & m; arith_util a; + datatype_util dt; is_variable_proc* m_is_variable; var_subst m_subst; expr_ref_vector m_new_exprs; @@ -215,14 +217,15 @@ namespace eq { (not T) is used because this formula is equivalent to (not (iff (VAR 2) (not T))), and can be viewed as a disequality. */ - bool is_var_diseq(expr * e, var * & v, expr_ref & t) { + bool is_var_diseq(expr * e, ptr_vector& vs, expr_ref_vector& ts) { expr* e1; if (m.is_not(e, e1)) { - return is_var_eq(e, v, t); + return is_var_eq(e, vs, ts); } - else if (is_var_eq(e, v, t) && m.is_bool(v)) { - bool_rewriter(m).mk_not(t, t); - m_new_exprs.push_back(t); + else if (is_var_eq(e, vs, ts) && vs.size() == 1 && m.is_bool(vs[0])) { + expr_ref tmp(m); + bool_rewriter(m).mk_not(ts[0].get(), tmp); + ts[0] = tmp; return true; } else { @@ -230,11 +233,11 @@ namespace eq { } } - bool solve_arith_core(app * lhs, expr * rhs, expr * eq, var* & var, expr_ref & def) { + bool solve_arith_core(app * lhs, expr * rhs, expr * eq, ptr_vector& vs, expr_ref_vector& ts) { SASSERT(a.is_add(lhs)); bool is_int = a.is_int(lhs); - expr * a1; - expr * v; + expr * a1, *v; + expr_ref def(m); rational a_val; unsigned num = lhs->get_num_args(); unsigned i; @@ -255,7 +258,7 @@ namespace eq { } if (i == num) return false; - var = to_var(v); + vs.push_back(to_var(v)); expr_ref inv_a(m); if (!a_val.is_one()) { inv_a = a.mk_numeral(rational(1)/a_val, is_int); @@ -282,35 +285,48 @@ namespace eq { def = a.mk_sub(rhs, a.mk_add(other_args.size(), other_args.c_ptr())); break; } - m_new_exprs.push_back(def); + ts.push_back(def); return true; } + - bool arith_solve(expr * lhs, expr * rhs, expr * eq, var* & var, expr_ref & t) { + bool arith_solve(expr * lhs, expr * rhs, expr * eq, ptr_vector& vs, expr_ref_vector& ts) { return - (a.is_add(lhs) && solve_arith_core(to_app(lhs), rhs, eq, var, t)) || - (a.is_add(rhs) && solve_arith_core(to_app(rhs), lhs, eq, var, t)); + (a.is_add(lhs) && solve_arith_core(to_app(lhs), rhs, eq, vs, ts)) || + (a.is_add(rhs) && solve_arith_core(to_app(rhs), lhs, eq, vs, ts)); } - bool trival_solve(expr* lhs, expr* rhs, expr* eq, var* & v, expr_ref& t) { + bool trivial_solve(expr* lhs, expr* rhs, expr* eq, ptr_vector& vs, expr_ref_vector& ts) { if (!is_variable(lhs)) { std::swap(lhs, rhs); } if (!is_variable(lhs)) { return false; } - v = to_var(lhs); - t = rhs; - TRACE("der", tout << mk_pp(eq, m) << "\n";); + vs.push_back(to_var(lhs)); + ts.push_back(rhs); + TRACE("qe_lite", tout << mk_pp(eq, m) << "\n";); return true; } + bool same_vars(ptr_vector const& vs1, ptr_vector const& vs2) const { + if (vs1.size() != vs2.size()) { + return false; + } + for (unsigned i = 0; i < vs1.size(); ++i) { + if (vs1[i] != vs2[i]) { + return false; + } + } + return true; + } + /** \brief Return true if e can be viewed as a variable equality. */ - bool is_var_eq(expr * e, var * & v, expr_ref & t) { + bool is_var_eq(expr * e, ptr_vector& vs, expr_ref_vector & ts) { expr* lhs, *rhs; // (= VAR t), (iff VAR t), (iff (not VAR) t), (iff t (not VAR)) cases @@ -323,16 +339,15 @@ namespace eq { if (!is_neg_var(m, lhs)) { return false; } - v = to_var(lhs); - t = m.mk_not(rhs); - m_new_exprs.push_back(t); - TRACE("der", tout << mk_pp(e, m) << "\n";); + vs.push_back(to_var(lhs)); + ts.push_back(m.mk_not(rhs)); + TRACE("qe_lite", tout << mk_pp(e, m) << "\n";); return true; } - if (trival_solve(lhs, rhs, e, v, t)) { + if (trivial_solve(lhs, rhs, e, vs, ts)) { return true; } - if (arith_solve(lhs, rhs, e, v, t)) { + if (arith_solve(lhs, rhs, e, vs, ts)) { return true; } return false; @@ -341,12 +356,13 @@ namespace eq { // (ite cond (= VAR t) (= VAR t2)) case expr* cond, *e2, *e3; if (m.is_ite(e, cond, e2, e3)) { - if (is_var_eq(e2, v, t)) { - expr_ref t2(m); - var* v2; - if (is_var_eq(e3, v2, t2) && v2 == v) { - t = m.mk_ite(cond, t, t2); - m_new_exprs.push_back(t); + if (is_var_eq(e2, vs, ts)) { + expr_ref_vector ts2(m); + ptr_vector vs2; + if (is_var_eq(e3, vs2, ts2) && same_vars(vs, vs2)) { + for (unsigned i = 0; i < vs.size(); ++i) { + ts[i] = m.mk_ite(cond, ts[i].get(), ts2[i].get()); + } return true; } } @@ -355,17 +371,17 @@ namespace eq { // VAR = true case if (is_variable(e)) { - t = m.mk_true(); - v = to_var(e); - TRACE("der", tout << mk_pp(e, m) << "\n";); + ts.push_back(m.mk_true()); + vs.push_back(to_var(e)); + TRACE("qe_lite", tout << mk_pp(e, m) << "\n";); return true; } // VAR = false case if (is_neg_var(m, e)) { - t = m.mk_false(); - v = to_var(to_app(e)->get_arg(0)); - TRACE("der", tout << mk_pp(e, m) << "\n";); + ts.push_back(m.mk_false()); + vs.push_back(to_var(to_app(e)->get_arg(0))); + TRACE("qe_lite", tout << mk_pp(e, m) << "\n";); return true; } @@ -373,12 +389,12 @@ namespace eq { } - bool is_var_def(bool check_eq, expr* e, var*& v, expr_ref& t) { + bool is_var_def(bool check_eq, expr* e, ptr_vector& vs, expr_ref_vector& ts) { if (check_eq) { - return is_var_eq(e, v, t); + return is_var_eq(e, vs, ts); } else { - return is_var_diseq(e, v, t); + return is_var_diseq(e, vs, ts); } } @@ -393,7 +409,7 @@ namespace eq { der_sort_vars(m_inx2var, m_map, m_order); - TRACE("der", + TRACE("qe_lite", tout << "Elimination m_order:" << std::endl; for(unsigned i=0; iget_idx(); - if(m_map.get(idx, 0) == 0) { - m_map.reserve(idx + 1, 0); - m_inx2var.reserve(idx + 1, 0); - m_map[idx] = t; - m_inx2var[idx] = v; - m_pos2var[i] = idx; - def_count++; - largest_vinx = std::max(idx, largest_vinx); + ptr_vector vs; + expr_ref_vector ts(m); + if (is_var_def(is_exists, args[i], vs, ts)) { + for (unsigned j = 0; j < vs.size(); ++j) { + var* v = vs[j]; + expr* t = ts[j].get(); + unsigned idx = v->get_idx(); + if (m_map.get(idx, 0) == 0) { + m_map.reserve(idx + 1, 0); + m_inx2var.reserve(idx + 1, 0); + m_map[idx] = t; + m_inx2var[idx] = v; + m_pos2var[i] = idx; + def_count++; + largest_vinx = std::max(idx, largest_vinx); + m_new_exprs.push_back(t); + } } } } } + + void flatten_definitions(expr_ref_vector& conjs) { + TRACE("qe_lite", + expr_ref tmp(m); + tmp = m.mk_and(conjs.size(), conjs.c_ptr()); + tout << mk_pp(tmp, m) << "\n";); + for (unsigned i = 0; i < conjs.size(); ++i) { + expr* c = conjs[i].get(); + expr* l, *r; + if (m.is_false(c)) { + conjs[0] = c; + conjs.resize(1); + break; + } + if (is_ground(c)) { + continue; + } + if (!m.is_eq(c, l, r)) { + continue; + } + if (!is_app(l) || !is_app(r)) { + continue; + } + if (dt.is_constructor(to_app(l)->get_decl())) { + flatten_constructor(to_app(l), to_app(r), conjs); + conjs[i] = conjs.back(); + conjs.pop_back(); + --i; + continue; + } + if (dt.is_constructor(to_app(r)->get_decl())) { + flatten_constructor(to_app(r), to_app(l), conjs); + conjs[i] = conjs.back(); + conjs.pop_back(); + --i; + continue; + } + } + TRACE("qe_lite", + expr_ref tmp(m); + tmp = m.mk_and(conjs.size(), conjs.c_ptr()); + tout << "after flatten\n" << mk_pp(tmp, m) << "\n";); + } + + void flatten_constructor(app* c, app* r, expr_ref_vector& conjs) { + SASSERT(dt.is_constructor(c)); + + func_decl* d = c->get_decl(); + + if (dt.is_constructor(r->get_decl())) { + app* b = to_app(r); + if (d == b->get_decl()) { + for (unsigned j = 0; j < c->get_num_args(); ++j) { + conjs.push_back(m.mk_eq(c->get_arg(j), b->get_arg(j))); + } + } + else { + conjs.push_back(m.mk_false()); + } + } + else { + func_decl* rec = dt.get_constructor_recognizer(d); + conjs.push_back(m.mk_app(rec, r)); + ptr_vector const& acc = *dt.get_constructor_accessors(d); + for (unsigned i = 0; i < acc.size(); ++i) { + conjs.push_back(m.mk_eq(c->get_arg(i), m.mk_app(acc[i], r))); + } + } + } bool reduce_var_set(expr_ref_vector& conjs) { unsigned def_count = 0; unsigned largest_vinx = 0; + + flatten_definitions(conjs); find_definitions(conjs.size(), conjs.c_ptr(), true, def_count, largest_vinx); @@ -578,12 +670,22 @@ namespace eq { } public: - der(ast_manager & m): m(m), a(m), m_is_variable(0), m_subst(m), m_new_exprs(m), m_subst_map(m), m_new_args(m), m_rewriter(m), m_cancel(false) {} + der(ast_manager & m): + m(m), + a(m), + dt(m), + m_is_variable(0), + m_subst(m), + m_new_exprs(m), + m_subst_map(m), + m_new_args(m), + m_rewriter(m), + m_cancel(false) {} void set_is_variable_proc(is_variable_proc& proc) { m_is_variable = &proc;} void operator()(quantifier * q, expr_ref & r, proof_ref & pr) { - TRACE("der", tout << mk_pp(q, m) << "\n";); + TRACE("qe_lite", tout << mk_pp(q, m) << "\n";); pr = 0; r = q; reduce_quantifier(q, r, pr); diff --git a/src/muz_qe/tab_context.cpp b/src/muz_qe/tab_context.cpp index 0eb9331d2..f4efe78f0 100644 --- a/src/muz_qe/tab_context.cpp +++ b/src/muz_qe/tab_context.cpp @@ -23,93 +23,324 @@ Revision History: #include "dl_context.h" #include "dl_mk_rule_inliner.h" #include "smt_kernel.h" -#include "matcher.h" #include "qe_lite.h" #include "bool_rewriter.h" +#include "th_rewriter.h" +#include "datatype_decl_plugin.h" -namespace datalog { +namespace tb { -#if 0 // semantic matcher. - class tab_matcher { + class matcher { typedef std::pair expr_pair; + ast_manager& m; svector m_todo; + datatype_util m_dt; + + lbool is_eq(expr* _s, expr* _t) { + if (_s == _t) { + return l_true; + } + if (!is_app(_s) || !is_app(_t)) { + return l_undef; + } + app* s = to_app(_s); + app* t = to_app(_t); + + if (m.is_value(s) && m.is_value(t)) { + IF_VERBOSE(2, verbose_stream() << "different:" << mk_pp(s, m) << " " << mk_pp(t, m) << "\n";); + return l_false; + } + + if (m_dt.is_constructor(s) && m_dt.is_constructor(t)) { + if (s->get_decl() == t->get_decl()) { + lbool state = l_true; + for (unsigned i = 0; i < s->get_num_args(); ++i) { + // move is_eq: decompose arguments to constraints. + switch (is_eq(s->get_arg(i), t->get_arg(i))) { + case l_undef: + state = l_undef; + break; + case l_false: + return l_false; + default: + break; + } + } + return state; + } + else { + IF_VERBOSE(2, verbose_stream() << "different constructors:" << mk_pp(s, m) << " " << mk_pp(t, m) << "\n";); + return l_false; + } + } + return l_undef; + } + + bool match_var(var* v, app* t, substitution& s, expr_ref_vector& conds) { + expr_offset r; + if (s.find(v, 0, r)) { + app* p = to_app(r.get_expr()); + switch (is_eq(p, t)) { + case l_true: + break; + case l_false: + return false; + default: + conds.push_back(m.mk_eq(p, t)); + break; + } + } + else { + s.insert(v, 0, expr_offset(t, 1)); + } + return true; + } + + bool match_app(app* p, app* t, substitution& s, expr_ref_vector& conds) { + if (p->get_decl() == t->get_decl() && + p->get_num_args() == t->get_num_args()) { + for (unsigned i = 0; i < p->get_num_args(); ++i) { + m_todo.push_back(expr_pair(p->get_arg(i), t->get_arg(i))); + } + return true; + } + else { + switch(is_eq(p, t)) { + case l_true: + return true; + case l_false: + return false; + default: + conds.push_back(m.mk_eq(p, t)); + return true; + } + } + } + public: - matcher(ast_manager& m): m(m) {} + matcher(ast_manager& m): m(m), m_dt(m) {} - bool operator()(expr* pat, expr* term, substitution& s, expr_ref_vector& side_conds) { + bool operator()(expr* pat, expr* term, substitution& s, expr_ref_vector& conds) { m_todo.reset(); m_todo.push_back(expr_pair(pat, term)); while (!m_todo.empty()) { expr_pair const& p = m_todo.back(); - pat = p.first; + pat = p.first; term = p.second; - if (is_var(pat)) { - + m_todo.pop_back(); + if (!is_app(term)) { + IF_VERBOSE(2, verbose_stream() << "term is not app\n";); + return false; + } + else if (is_var(pat) && match_var(to_var(pat), to_app(term), s, conds)) { + continue; + } + else if (!is_app(pat)) { + IF_VERBOSE(2, verbose_stream() << "pattern is not app\n";); + return false; + } + else if (!match_app(to_app(pat), to_app(term), s, conds)) { + return false; } } + return true; } }; -#endif + + class goal { + th_rewriter m_rw; + datalog::rule_ref m_goal; + app_ref m_head; + app_ref_vector m_predicates; + expr_ref m_constraint; + unsigned m_index; + unsigned m_num_vars; + unsigned m_predicate_index; + unsigned m_rule_index; + unsigned m_ref; + + public: + + goal(datalog::rule_manager& rm): + m_rw(rm.get_manager()), + m_goal(rm), + m_head(rm.get_manager()), + m_predicates(rm.get_manager()), + m_constraint(rm.get_manager()), + m_index(0), + m_num_vars(0), + m_predicate_index(0), + m_rule_index(0), + m_ref(0) { + } + + void set_rule_index(unsigned i) { m_rule_index = i; } + unsigned get_rule_index() const { return m_rule_index; } + void inc_rule_index() { m_rule_index++; } + unsigned get_predicate_index() const { return m_predicate_index; } + void set_predicate_index(unsigned i) { m_predicate_index = i; } + unsigned get_num_predicates() const { return m_predicates.size(); } + app* get_predicate(unsigned i) const { return m_predicates[i]; } + expr* get_constraint() const { return m_constraint; } + datalog::rule const& get_rule() const { return *m_goal; } + unsigned get_num_vars() const { return m_num_vars; } + unsigned get_index() const { return m_index; } + app* get_head() const { return m_head; } + + void init(datalog::rule_ref& g) { + m_goal = g; + m_index = 0; + m_predicate_index = 0; + m_rule_index = 0; + m_num_vars = 1 + g.get_manager().get_var_counter().get_max_var(*g); + init(); + + // IF_VERBOSE(1, display(verbose_stream());); + } + + void set_index(unsigned index) { + m_index = index; + } + + void inc_ref() { + m_ref++; + } + + void dec_ref() { + --m_ref; + if (m_ref == 0) { + dealloc(this); + } + } + + void display(std::ostream& out) const { + ast_manager& m = m_head.get_manager(); + expr_ref_vector fmls(m); + expr_ref fml(m); + for (unsigned i = 0; i < m_predicates.size(); ++i) { + fmls.push_back(m_predicates[i]); + } + fmls.push_back(m_constraint); + bool_rewriter(m).mk_and(fmls.size(), fmls.c_ptr(), fml); + out << mk_pp(fml, m) << "\n"; + } + + private: + // x = t[y], if x does not occur in t[y], then add t[y] to subst. + + void init() { + m_predicates.reset(); + ast_manager& m = m_head.get_manager(); + unsigned delta[1] = { 0 }; + datalog::rule_manager& rm = m_goal.m(); + unsigned num_vars = rm.get_var_counter().get_max_var(*m_goal); + substitution subst(m); + subst.reserve(1, num_vars+1); + expr_ref_vector fmls(m); + expr_ref tmp(m); + unsigned utsz = m_goal->get_uninterpreted_tail_size(); + unsigned tsz = m_goal->get_tail_size(); + for (unsigned i = utsz; i < tsz; ++i) { + fmls.push_back(m_goal->get_tail(i)); + } + datalog::flatten_and(fmls); + for (unsigned i = 0; i < fmls.size(); ++i) { + expr* e = fmls[i].get(); + expr* t, *v; + if ((m.is_eq(e, v, t) && is_var(v) && !subst.contains(to_var(v), 0)) || + (m.is_eq(e, t, v) && is_var(v) && !subst.contains(to_var(v), 0))) { + subst.push_scope(); + subst.insert(to_var(v)->get_idx(), 0, expr_offset(t, 0)); + if (!subst.acyclic()) { + subst.pop_scope(); + } + } + } + bool_rewriter(m).mk_and(fmls.size(), fmls.c_ptr(), m_constraint); + subst.apply(1, delta, expr_offset(m_constraint, 0), m_constraint); + subst.apply(1, delta, expr_offset(m_goal->get_head(), 0), tmp); + m_head = to_app(tmp); + m_rw(m_constraint); + for (unsigned i = 0; i < utsz; ++i) { + subst.apply(1, delta, expr_offset(m_goal->get_tail(i), 0), tmp); + m_predicates.push_back(to_app(tmp)); + } + } + }; // subsumption index structure. - class tab_index { - ast_manager& m; - rule_manager& rm; - context& m_ctx; - app_ref_vector m_preds; - expr_ref m_precond; - rule_ref_vector m_rules; - svector m_num_vars; - matcher m_matcher; - substitution m_subst; - qe_lite m_qe; - uint_set m_empty_set; - bool_rewriter m_rw; - smt_params m_fparams; - smt::kernel m_solver; + class index { + ast_manager& m; + datalog::rule_manager& rm; + datalog::context& m_ctx; + app_ref_vector m_preds; + expr_ref m_precond; + expr_ref_vector m_sideconds; + vector > m_index; + matcher m_matcher; + substitution m_subst; + qe_lite m_qe; + uint_set m_empty_set; + bool_rewriter m_rw; + smt_params m_fparams; + smt::kernel m_solver; + volatile bool m_cancel; public: - tab_index(ast_manager& m, rule_manager& rm, context& ctx): - m(m), - rm(rm), + index(datalog::context& ctx): + m(ctx.get_manager()), + rm(ctx.get_rule_manager()), m_ctx(ctx), m_preds(m), m_precond(m), - m_rules(rm), + m_sideconds(m), m_matcher(m), m_subst(m), m_qe(m), m_rw(m), - m_solver(m, m_fparams) {} + m_solver(m, m_fparams), + m_cancel(false) {} - void insert(rule* r) { - m_rules.push_back(r); - m_num_vars.push_back(1+rm.get_var_counter().get_max_var(*r)); + void insert(ref& g) { + m_index.push_back(g); } - bool is_subsumed(rule const& r) { - setup(r); + bool is_subsumed(goal const& g, unsigned& subsumer) { + setup(g); m_solver.push(); m_solver.assert_expr(m_precond); - bool found = find_match(); + bool found = find_match(subsumer); m_solver.pop(1); return found; } + void cancel() { + m_cancel = true; + m_solver.cancel(); + m_qe.set_cancel(true); + } + + void cleanup() { + m_solver.reset_cancel(); + m_qe.set_cancel(false); + m_cancel = false; + } + private: - void setup(rule const& r) { + void setup(goal const& g) { m_preds.reset(); expr_ref_vector fmls(m); expr_ref_vector vars(m); expr_ref fml(m); ptr_vector sorts; - r.get_vars(sorts); - unsigned utsz = r.get_uninterpreted_tail_size(); - unsigned tsz = r.get_tail_size(); + for (unsigned i = 0; i < g.get_num_predicates(); ++i) { + get_free_vars(g.get_predicate(i), sorts); + } + get_free_vars(g.get_constraint(), sorts); var_subst vs(m, false); for (unsigned i = 0; i < sorts.size(); ++i) { if (!sorts[i]) { @@ -117,24 +348,27 @@ namespace datalog { } vars.push_back(m.mk_const(symbol(i), sorts[i])); } - for (unsigned i = 0; i < utsz; ++i) { - fml = r.get_tail(i); - vs(fml, vars.size(), vars.c_ptr(), fml); + for (unsigned i = 0; i < g.get_num_predicates(); ++i) { + vs(g.get_predicate(i), vars.size(), vars.c_ptr(), fml); m_preds.push_back(to_app(fml)); } - for (unsigned i = utsz; i < tsz; ++i) { - fml = r.get_tail(i); - vs(fml, vars.size(), vars.c_ptr(), fml); - fmls.push_back(fml); - } + vs(g.get_constraint(), vars.size(), vars.c_ptr(), fml); + fmls.push_back(fml); m_precond = m.mk_and(fmls.size(), fmls.c_ptr()); + IF_VERBOSE(2, + verbose_stream() << "setup-match: "; + for (unsigned i = 0; i < m_preds.size(); ++i) { + verbose_stream() << mk_pp(m_preds[i].get(), m) << " "; + } + verbose_stream() << mk_pp(m_precond, m) << "\n";); } // extract pre_cond => post_cond validation obligation from match. - bool find_match() { - for (unsigned i = 0; i < m_rules.size(); ++i) { + bool find_match(unsigned& subsumer) { + for (unsigned i = 0; !m_cancel && i < m_index.size(); ++i) { if (match_rule(i)) { + subsumer = m_index[i]->get_index(); return true; } } @@ -145,44 +379,62 @@ namespace datalog { // for now: skip multiple matches within the same rule (incomplete). // bool match_rule(unsigned rule_index) { - rule const& r = *m_rules[rule_index]; - unsigned num_vars = m_num_vars[rule_index]; + goal const& g = *m_index[rule_index]; m_subst.reset(); - m_subst.reserve(2, num_vars); + m_subst.reserve(2, g.get_num_vars()); - // IF_VERBOSE(1, r.display(m_ctx, verbose_stream() << "try-match\n");); + IF_VERBOSE(2, g.display(verbose_stream() << "try-match\n");); - return match_predicates(0, r); + return match_predicates(0, g); } - bool match_predicates(unsigned predicate_index, rule const& r) { - if (predicate_index == r.get_uninterpreted_tail_size()) { - return check_substitution(r); + + bool match_predicates(unsigned predicate_index, goal const& g) { + if (predicate_index == g.get_num_predicates()) { + return check_substitution(g); } - app* p = r.get_tail(predicate_index); - for (unsigned i = 0; i < m_preds.size(); ++i) { + + app* q = g.get_predicate(predicate_index); + + for (unsigned i = 0; !m_cancel && i < m_preds.size(); ++i) { + app* p = m_preds[i].get(); m_subst.push_scope(); - if (m_matcher(p, m_preds[i].get(), m_subst) && - match_predicates(predicate_index + 1, r)) { + unsigned limit = m_sideconds.size(); + IF_VERBOSE(2, + for (unsigned j = 0; j < predicate_index; ++j) verbose_stream() << " "; + verbose_stream() << mk_pp(q, m) << " = " << mk_pp(p, m) << "\n"; + ); + + + if (q->get_decl() == p->get_decl() && + m_matcher(q, p, m_subst, m_sideconds) && + match_predicates(predicate_index + 1, g)) { return true; } - m_subst.pop_scope(); + m_subst.pop_scope(1); + m_sideconds.resize(limit); } return false; } - bool check_substitution(rule const& r) { - unsigned utsz = r.get_uninterpreted_tail_size(); - unsigned tsz = r.get_tail_size(); + bool check_substitution(goal const& g) { unsigned deltas[2] = {0, 0}; - expr_ref_vector fmls(m); expr_ref q(m), postcond(m); + expr_ref_vector fmls(m_sideconds); - for (unsigned i = utsz; i < tsz; ++i) { - app* p = r.get_tail(i); - m_subst.apply(2, deltas, expr_offset(p, 0), q); - fmls.push_back(q); + for (unsigned i = 0; i < fmls.size(); ++i) { + m_subst.apply(2, deltas, expr_offset(fmls[i].get(), 0), q); + fmls[i] = q; } + m_subst.apply(2, deltas, expr_offset(g.get_constraint(), 0), q); + fmls.push_back(q); + + IF_VERBOSE(2, + for (unsigned i = 0; i < g.get_num_predicates(); ++i) { + verbose_stream() << " "; + } + q = m.mk_and(fmls.size(), fmls.c_ptr()); + verbose_stream() << "check: " << mk_pp(q, m) << "\n";); m_qe(m_empty_set, false, fmls); m_rw.mk_and(fmls.size(), fmls.c_ptr(), postcond); @@ -205,7 +457,107 @@ namespace datalog { } }; - enum tab_instruction { + // predicate selection strategy. + class selection { + datalog::context& m_ctx; + ast_manager& m; + datalog::rule_manager& rm; + datatype_util dt; + obj_map m_scores; + unsigned_vector m_score_values; + + + public: + selection(datalog::context& ctx): + m_ctx(ctx), + m(ctx.get_manager()), + rm(ctx.get_rule_manager()), + dt(m) { + } + + void init(datalog::rule_set const& rules) { + m_scores.reset(); + goal g(rm); + datalog::rule_ref r(rm); + datalog::rule_set::iterator it = rules.begin(); + datalog::rule_set::iterator end = rules.end(); + for (; it != end; ++it) { + r = *it; + g.init(r); + app* p = g.get_head(); + unsigned_vector scores; + score_predicate(p, scores); + insert_score(p->get_decl(), scores); + } + } + + unsigned select(goal const& g) { + unsigned min_distance = UINT_MAX; + unsigned result = 0; + unsigned_vector& scores = m_score_values; + for (unsigned i = 0; i < g.get_num_predicates(); ++i) { + scores.reset(); + score_predicate(g.get_predicate(i), scores); + unsigned dist = compute_distance(g.get_predicate(i)->get_decl(), scores); + if (dist < min_distance) { + min_distance = dist; + result = i; + } + } + return result; + } + + private: + + unsigned compute_distance(func_decl* f, unsigned_vector const& scores) { + unsigned_vector f_scores; + unsigned dist = 0; + if (m_scores.find(f, f_scores)) { + SASSERT(f_scores.size() == scores.size()); + for (unsigned i = 0; i < scores.size(); ++i) { + unsigned d1 = scores[i] - f_scores[i]; + dist += d1*d1; + } + } + // else there is no rule. + return dist; + } + + void score_predicate(app* p, unsigned_vector& scores) { + for (unsigned i = 0; i < p->get_num_args(); ++i) { + scores.push_back(score_argument(p->get_arg(i))); + } + } + + unsigned score_argument(expr* arg) { + if (is_var(arg)) { + return 0; + } + if (m.is_value(arg)) { + return 3; + } + if (is_app(arg) && dt.is_constructor(to_app(arg)->get_decl())) { + return 2; + } + return 1; + } + + void insert_score(func_decl* f, unsigned_vector const& scores) { + obj_map::obj_map_entry* e = m_scores.find_core(f); + if (e) { + unsigned_vector & old_scores = e->get_data().m_value; + SASSERT(scores.size() == old_scores.size()); + for (unsigned i = 0; i < scores.size(); ++i) { + old_scores[i] += scores[i]; + } + } + else { + m_scores.insert(f, scores); + } + } + }; + + enum instruction { SELECT_RULE, SELECT_PREDICATE, BACKTRACK, @@ -214,7 +566,7 @@ namespace datalog { CANCEL }; - std::ostream& operator<<(std::ostream& out, tab_instruction i) { + std::ostream& operator<<(std::ostream& out, instruction i) { switch(i) { case SELECT_RULE: return out << "select-rule"; case SELECT_PREDICATE: return out << "select-predicate"; @@ -225,8 +577,9 @@ namespace datalog { } return out << "unmatched instruction"; } +}; - +namespace datalog { class tab::imp { struct stats { @@ -234,58 +587,20 @@ namespace datalog { void reset() { memset(this, 0, sizeof(*this)); } unsigned m_num_unfold; unsigned m_num_no_unfold; - unsigned m_num_subsume; + unsigned m_num_subsumed; }; - class goal { - public: - rule_ref m_goal; -// app_ref m_head; -// app_ref_vector m_predicates; -// expr_ref m_constraint; - unsigned m_index; - unsigned m_predicate_index; - unsigned m_rule_index; - - goal(rule_manager& rm): - m_goal(rm), -// m_head(m), -// m_predicates(m), -// m_constraint(m), - m_index(0), - m_predicate_index(0), - m_rule_index(0) { - } - -#if 0 - private: - void init() { - m_head = m_goal.get_head(); - unsigned utsz = m_goal->get_uninterpreted_tail_size(); - unsigned tsz = m_goal->get_tail_size(); - for (unsigned i = 0; i < utsz; ++i) { - m_predicates.push_back(m_goal->get_tail(i)); - } - expr_ref fmls(m); - for (unsigned i = utsz; i < tsz; ++i) { - fmls.push_back(m_goal->get_tail(i)); - } - bool_rewriter(m).mk_and(fmls.size(), fmls.c_ptr(), m_constraint); - } -#endif - }; - context& m_ctx; ast_manager& m; rule_manager& rm; - tab_index m_subsumption_index; + tb::index m_index; + tb::selection m_selection; smt_params m_fparams; smt::kernel m_solver; rule_unifier m_unifier; rule_set m_rules; - vector m_goals; - goal m_goal; - tab_instruction m_instruction; + vector > m_goals; + tb::instruction m_instruction; unsigned m_goal_index; volatile bool m_cancel; stats m_stats; @@ -294,12 +609,12 @@ namespace datalog { m_ctx(ctx), m(ctx.get_manager()), rm(ctx.get_rule_manager()), - m_subsumption_index(m, rm, ctx), + m_index(ctx), + m_selection(ctx), m_solver(m, m_fparams), m_unifier(ctx), m_rules(ctx), - m_goal(rm), - m_instruction(SELECT_PREDICATE), + m_instruction(tb::SELECT_PREDICATE), m_cancel(false), m_goal_index(0) { @@ -314,21 +629,27 @@ namespace datalog { m_ctx.ensure_opened(); m_rules.reset(); m_rules.add_rules(m_ctx.get_rules()); + m_selection.init(m_rules); rule_ref_vector query_rules(rm); rule_ref goal(rm); func_decl_ref query_pred(m); rm.mk_query(query, query_pred, query_rules, goal); init_goal(goal); - IF_VERBOSE(1, display_goal(m_goal, verbose_stream());); + IF_VERBOSE(1, display_goal(*get_goal(), verbose_stream() << "g" << get_goal()->get_index() << " ");); return run(); } void cancel() { m_cancel = true; + m_index.cleanup(); + m_solver.cancel(); } + void cleanup() { m_cancel = false; m_goals.reset(); + m_index.cleanup(); + m_solver.reset_cancel(); } void reset_statistics() { m_stats.reset(); @@ -336,7 +657,7 @@ namespace datalog { void collect_statistics(statistics& st) const { st.update("tab.num_unfold", m_stats.m_num_unfold); st.update("tab.num_unfold_fail", m_stats.m_num_no_unfold); - st.update("tab.num_subsume", m_stats.m_num_subsume); + st.update("tab.num_subsumed", m_stats.m_num_subsumed); } void display_certificate(std::ostream& out) const { // TBD @@ -348,90 +669,100 @@ namespace datalog { private: void select_predicate() { - rule_ref& query = m_goal.m_goal; - unsigned num_predicates = query->get_uninterpreted_tail_size(); + unsigned num_predicates = get_goal()->get_num_predicates(); if (num_predicates == 0) { - m_instruction = UNSATISFIABLE; - IF_VERBOSE(2, query->display(m_ctx, verbose_stream()); ); + m_instruction = tb::UNSATISFIABLE; + IF_VERBOSE(2, get_goal()->display(verbose_stream()); ); } else { - m_instruction = SELECT_RULE; - unsigned pi = 0; // TBD replace by better selection function. - m_goal.m_predicate_index = pi; - m_goal.m_rule_index = 0; - IF_VERBOSE(2, verbose_stream() << mk_pp(query->get_tail(pi), m) << "\n";); + m_instruction = tb::SELECT_RULE; + unsigned pi = m_selection.select(*get_goal()); + get_goal()->set_predicate_index(pi); + get_goal()->set_rule_index(0); + IF_VERBOSE(2, verbose_stream() << mk_pp(get_goal()->get_predicate(pi), m) << "\n";); } } void apply_rule(rule const& r) { - rule_ref& query = m_goal.m_goal; + ref goal = get_goal(); + rule const& query = goal->get_rule(); rule_ref new_query(rm); - if (m_unifier.unify_rules(*query, m_goal.m_predicate_index, r) && - m_unifier.apply(*query, m_goal.m_predicate_index, r, new_query) && - l_false != query_is_sat(*new_query.get()) && - !query_is_subsumed(*new_query.get())) { - m_stats.m_num_unfold++; - m_subsumption_index.insert(query.get()); - m_goals.push_back(m_goal); - init_goal(new_query); + if (m_unifier.unify_rules(query, goal->get_predicate_index(), r) && + m_unifier.apply(query, goal->get_predicate_index(), r, new_query) && + l_false != query_is_sat(*new_query.get())) { + ref next_goal = init_goal(new_query); + unsigned subsumer = 0; IF_VERBOSE(1, - display_premise(m_goals.back(), verbose_stream()); - display_goal(m_goal, verbose_stream());); - m_instruction = SELECT_PREDICATE; + display_premise(*goal, verbose_stream() << "g" << next_goal->get_index() << " "); + display_goal(*next_goal, verbose_stream());); + if (m_index.is_subsumed(*next_goal, subsumer)) { + IF_VERBOSE(1, verbose_stream() << "subsumed by " << subsumer << "\n";); + m_stats.m_num_subsumed++; + m_goals.pop_back(); + m_instruction = tb::SELECT_RULE; + } + else { + m_stats.m_num_unfold++; + m_index.insert(next_goal); + m_instruction = tb::SELECT_PREDICATE; + } } else { m_stats.m_num_no_unfold++; - m_instruction = SELECT_RULE; + m_instruction = tb::SELECT_RULE; } } void select_rule() { - func_decl* p = m_goal.m_goal->get_decl(m_goal.m_predicate_index); + func_decl* p = get_goal()->get_predicate(get_goal()->get_predicate_index())->get_decl(); rule_vector const& rules = m_rules.get_predicate_rules(p); - if (rules.size() <= m_goal.m_rule_index) { - m_instruction = BACKTRACK; + if (rules.size() <= get_goal()->get_rule_index()) { + m_instruction = tb::BACKTRACK; } else { - apply_rule(*rules[m_goal.m_rule_index++]); + unsigned index = get_goal()->get_rule_index(); + get_goal()->inc_rule_index(); + apply_rule(*rules[index]); } } void backtrack() { + SASSERT(!m_goals.empty()); + m_goals.pop_back(); if (m_goals.empty()) { - m_instruction = SATISFIABLE; + m_instruction = tb::SATISFIABLE; } else { - m_goal = m_goals.back(); - m_goals.pop_back(); - m_instruction = SELECT_RULE; + m_instruction = tb::SELECT_RULE; } } lbool run() { - m_instruction = SELECT_PREDICATE; + m_instruction = tb::SELECT_PREDICATE; while (true) { + IF_VERBOSE(2, verbose_stream() << m_instruction << "\n";); if (m_cancel) { cleanup(); return l_undef; } switch(m_instruction) { - case SELECT_PREDICATE: + case tb::SELECT_PREDICATE: select_predicate(); break; - case SELECT_RULE: + case tb::SELECT_RULE: select_rule(); break; - case BACKTRACK: + case tb::BACKTRACK: backtrack(); break; - case SATISFIABLE: + case tb::SATISFIABLE: return l_false; - case UNSATISFIABLE: + case tb::UNSATISFIABLE: return l_true; - case CANCEL: - m_cancel = false; + case tb::CANCEL: + cleanup(); return l_undef; } } @@ -456,7 +787,9 @@ namespace datalog { names.push_back(symbol(i)); } fml = m.mk_and(fmls.size(), fmls.c_ptr()); - fml = m.mk_exists(sorts.size(), sorts.c_ptr(), names.c_ptr(), fml); + if (!sorts.empty()) { + fml = m.mk_exists(sorts.size(), sorts.c_ptr(), names.c_ptr(), fml); + } m_solver.push(); m_solver.assert_expr(fml); lbool is_sat = m_solver.check(); @@ -467,24 +800,21 @@ namespace datalog { return is_sat; } - bool query_is_subsumed(rule const& query) { - return m_subsumption_index.is_subsumed(query); + ref init_goal(rule_ref& new_query) { + ref goal = alloc(tb::goal, rm); + goal->init(new_query); + goal->set_index(m_goal_index++); + m_goals.push_back(goal); + return goal; } - void init_goal(rule_ref& new_query) { - m_goal.m_goal = new_query; - m_goal.m_index = m_goal_index++; - m_goal.m_predicate_index = 0; - m_goal.m_rule_index = 0; - } + ref get_goal() const { return m_goals.back(); } - - void display_premise(goal& p, std::ostream& out) { - out << "[" << p.m_index << "]: " << p.m_predicate_index << ":" << p.m_rule_index << "\n"; + void display_premise(tb::goal& p, std::ostream& out) { + out << "{g" << p.get_index() << " p" << p.get_predicate_index() << " r" << p.get_rule_index() << "}\n"; } - void display_goal(goal& g, std::ostream& out) { - out << g.m_index << " "; - g.m_goal->display(m_ctx, out); + void display_goal(tb::goal& g, std::ostream& out) { + g.display(out); } };