From d3025569c2fc3c04b1ce07d7901ec7d1c74ebcc1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 24 Jan 2013 12:45:58 -0800 Subject: [PATCH] working on tab-context Signed-off-by: Nikolaj Bjorner --- src/muz_qe/dl_context.cpp | 3 +- src/muz_qe/tab_context.cpp | 95 ++++++++++++++++++++------------------ 2 files changed, 50 insertions(+), 48 deletions(-) diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp index 8ef2ffa22..da702d4e3 100644 --- a/src/muz_qe/dl_context.cpp +++ b/src/muz_qe/dl_context.cpp @@ -1012,8 +1012,7 @@ namespace datalog { for (; it != end; ++it) { r = *it; check_rule(r); - } - + } switch(get_engine()) { case DATALOG_ENGINE: return rel_query(query); diff --git a/src/muz_qe/tab_context.cpp b/src/muz_qe/tab_context.cpp index a2c7e6215..35b15ae1b 100644 --- a/src/muz_qe/tab_context.cpp +++ b/src/muz_qe/tab_context.cpp @@ -190,6 +190,7 @@ namespace tb { unsigned get_index() const { return m_index; } void set_index(unsigned index) { m_index = index; } app* get_head() const { return m_head; } + void set_head(app* h) { m_head = h; } unsigned get_parent_index() const { return m_parent_index; } unsigned get_parent_rule() const { return m_parent_rule; } void set_parent(ref& parent) { @@ -200,12 +201,14 @@ namespace tb { expr_ref get_body() const { ast_manager& m = 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); datalog::flatten_and(fmls); - return expr_ref(m.mk_and(fmls.size(), fmls.c_ptr()), m); + bool_rewriter(m).mk_and(fmls.size(), fmls.c_ptr(), fml); + return fml; } void get_free_vars(ptr_vector& vars) const { @@ -219,7 +222,12 @@ namespace tb { expr_ref to_formula() const { ast_manager& m = get_manager(); expr_ref body = get_body(); - body = m.mk_implies(body, m_head); + if (m.is_true(body)) { + body = m_head; + } + else { + body = m.mk_implies(body, m_head); + } ptr_vector vars; svector names; get_free_vars(vars); @@ -233,7 +241,7 @@ namespace tb { vars.reverse(); if (!vars.empty()) { body = m.mk_forall(vars.size(), vars.c_ptr(), names.c_ptr(), body); - } + } return body; } @@ -280,6 +288,14 @@ namespace tb { } fmls.push_back(m_constraint); bool_rewriter(m).mk_and(fmls.size(), fmls.c_ptr(), fml); + if (!m.is_false(m_head)) { + if (m.is_true(fml)) { + fml = m_head; + } + else { + fml = m.mk_implies(fml, m_head); + } + } out << mk_pp(fml, m) << "\n"; } @@ -420,10 +436,11 @@ namespace tb { datalog::rule_ref r(rm); datalog::rule_set::iterator it = rules.begin(); datalog::rule_set::iterator end = rules.end(); - for (; it != end; ++it) { + for (unsigned i = 0; it != end; ++it) { r = *it; ref g = alloc(clause, rm); g->init(r); + g->set_index(i++); insert(g); } } @@ -764,7 +781,8 @@ namespace tb { datalog::context& m_ctx; ::unifier m_unifier; substitution m_S1; - substitution m_S2; + var_subst m_S2; + expr_ref_vector m_rename; expr_ref_vector m_sub1; expr_ref_vector m_sub2; public: @@ -773,7 +791,8 @@ namespace tb { m_ctx(ctx), m_unifier(m), m_S1(m), - m_S2(m), + m_S2(m, false), + m_rename(m), m_sub1(m), m_sub2(m) {} @@ -844,27 +863,26 @@ namespace tb { result->init(head, predicates, constraint); vars.reset(); result->get_free_vars(vars); - m_S2.reserve(1, vars.size()); bool change = false; + var_ref w(m); for (unsigned i = 0, j = 0; i < vars.size(); ++i) { if (vars[i]) { - if (i != j) { - var_ref v(m), w(m); - v = m.mk_var(i, vars[i]); - w = m.mk_var(j, vars[i]); - m_S2.insert(v, 0, expr_offset(w, 0)); - change = true; - } + w = m.mk_var(j, vars[i]); + m_rename.push_back(w); ++j; } + else { + change = true; + m_rename.push_back(0); + } } if (change) { - m_S2.apply(1, delta, expr_offset(result->get_constraint(), 0), constraint); + m_S2(result->get_constraint(), m_rename.size(), m_rename.c_ptr(), constraint); for (unsigned i = 0; i < result->get_num_predicates(); ++i) { - m_S2.apply(1, delta, expr_offset(result->get_predicate(i), 0), tmp); + m_S2(result->get_predicate(i), m_rename.size(), m_rename.c_ptr(), tmp); predicates[i] = to_app(tmp); } - m_S2.apply(1, delta, expr_offset(result->get_head(), 0), tmp); + m_S2(result->get_head(), m_rename.size(), m_rename.c_ptr(), tmp); head = to_app(tmp); result->init(head, predicates, constraint); } @@ -872,11 +890,6 @@ namespace tb { extract_subst(delta, tgt, 0); extract_subst(delta, src, 1); } - - IF_VERBOSE(1, - verbose_stream() << "New unify:\n"; - result->display(verbose_stream());); - // init result using head, predicates, constraint return true; } @@ -886,6 +899,7 @@ namespace tb { void reset() { m_S1.reset(); m_S2.reset(); + m_rename.reset(); m_sub1.reset(); m_sub2.reset(); } @@ -899,7 +913,7 @@ namespace tb { if (vars[i]) { v = m.mk_var(i, vars[i]); m_S1.apply(2, delta, expr_offset(v, offset), tmp); - m_S2.apply(1, delta, expr_offset(tmp, 0), tmp); + m_S2(tmp, m_rename.size(), m_rename.c_ptr(), tmp); insert_subst(offset, tmp); } else { @@ -1001,19 +1015,9 @@ namespace datalog { func_decl_ref query_pred(m); rm.mk_query(query, query_pred, query_rules, clause); - // ensure clause predicate does not take free variables. - ptr_vector tail; - svector is_neg; - for (unsigned i = 0; i < clause->get_tail_size(); ++i) { - tail.push_back(clause->get_tail(i)); - is_neg.push_back(clause->is_neg_tail(i)); - } - app_ref query_app(m); - query_app = m.mk_const(symbol("query"), m.mk_bool_sort()); - m_ctx.register_predicate(query_app->get_decl()); - clause = rm.mk(query_app, tail.size(), tail.c_ptr(), is_neg.c_ptr()); ref g = alloc(tb::clause, rm); g->init(clause); + g->set_head(m.mk_false()); init_clause(g); IF_VERBOSE(1, display_clause(*get_clause(), verbose_stream() << "g" << get_clause()->get_seqno() << " ");); return run(); @@ -1214,7 +1218,7 @@ namespace datalog { unsigned idx = rl->get_index(); if (!m_displayed_rules.contains(idx)) { m_displayed_rules.insert(idx); - rl->display(out << p.get_next_rule() << ":"); + rl->display(out << "r" << p.get_next_rule() << ": "); } } @@ -1242,6 +1246,7 @@ namespace datalog { SASSERT(clause->get_num_predicates() == 0); expr_ref root = clause->to_formula(); + vector substs; while (0 != clause->get_index()) { SASSERT(clause->get_parent_index() < clause->get_index()); unsigned p_index = clause->get_parent_index(); @@ -1255,21 +1260,19 @@ namespace datalog { expr_ref_vector s2(m_unifier.get_rule_subst(false)); resolve_rule(pc, *parent, *rl, s1, s2, *clause); clause = parent; - IF_VERBOSE(1000, - verbose_stream() << "substitution\n"; - for (unsigned i = 0; i < s1.size(); ++i) { - verbose_stream() << mk_pp(s1[i].get(), m) << "\n"; - }); - // apply_subst(subst, s1); + substs.push_back(s1); } + for (unsigned i = substs.size(); i > 0; ) { + --i; + apply_subst(subst, substs[i]); + } + expr_ref body = clause->get_body(); + var_subst vs(m, false); + vs(body, subst.size(), subst.c_ptr(), body); + IF_VERBOSE(1, verbose_stream() << mk_pp(body, m) << "\n";); pc.invert(); prs.push_back(m.mk_asserted(root)); pc(m, 1, prs.c_ptr(), pr); - IF_VERBOSE(1000, - verbose_stream() << "substitution\n"; - for (unsigned i = 0; i < subst.size(); ++i) { - verbose_stream() << mk_pp(subst[i].get(), m) << "\n"; - }); return pr; }