From 8daf100c6502da11ff5eabe8d0981917a91ea530 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 17 Jan 2013 18:03:34 -0800 Subject: [PATCH] working on tab Horn solver Signed-off-by: Nikolaj Bjorner --- src/ast/substitution/matcher.cpp | 4 + src/ast/substitution/matcher.h | 2 +- src/muz_qe/dl_mk_interp_tail_simplifier.cpp | 2 +- src/muz_qe/tab_context.cpp | 229 ++++++++++++++++++-- src/test/matcher.cpp | 3 + 5 files changed, 214 insertions(+), 26 deletions(-) diff --git a/src/ast/substitution/matcher.cpp b/src/ast/substitution/matcher.cpp index cf0eff6b4..a5560c6a2 100644 --- a/src/ast/substitution/matcher.cpp +++ b/src/ast/substitution/matcher.cpp @@ -49,6 +49,10 @@ bool matcher::operator()(expr * e1, expr * e2, substitution & s) { if (is_var(p.second)) return false; + if (!is_app(p.first)) + return false; + if (!is_app(p.second)) + return false; app * n1 = to_app(p.first); app * n2 = to_app(p.second); diff --git a/src/ast/substitution/matcher.h b/src/ast/substitution/matcher.h index 662cfd371..1a71a51ed 100644 --- a/src/ast/substitution/matcher.h +++ b/src/ast/substitution/matcher.h @@ -32,7 +32,7 @@ class matcher { ast_manager & m_manager; substitution * m_subst; - cache m_cache; + // cache m_cache; svector m_todo; void reset(); diff --git a/src/muz_qe/dl_mk_interp_tail_simplifier.cpp b/src/muz_qe/dl_mk_interp_tail_simplifier.cpp index 9861c48ca..d028c8751 100644 --- a/src/muz_qe/dl_mk_interp_tail_simplifier.cpp +++ b/src/muz_qe/dl_mk_interp_tail_simplifier.cpp @@ -518,7 +518,7 @@ namespace datalog { if (m.is_false(itail.get())) { //the tail member is never true, so we may delete the rule - TRACE("dl", r->display(m_context, tout << "rule in infeasible\n");); + TRACE("dl", r->display(m_context, tout << "rule is infeasible\n");); return false; } if (!m.is_true(itail.get())) { diff --git a/src/muz_qe/tab_context.cpp b/src/muz_qe/tab_context.cpp index c025a9ec5..f96fd9a1e 100644 --- a/src/muz_qe/tab_context.cpp +++ b/src/muz_qe/tab_context.cpp @@ -22,6 +22,8 @@ Revision History: #include "dl_rule_set.h" #include "dl_context.h" #include "dl_mk_rule_inliner.h" +#include "smt_kernel.h" +#include "matcher.h" namespace datalog { @@ -42,6 +44,129 @@ namespace datalog { } }; + // 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; + unsigned m_index; + matcher m_matcher; + substitution m_subst; + + public: + tab_index(ast_manager& m, rule_manager& rm, context& ctx): + m(m), + rm(rm), + m_ctx(ctx), + m_preds(m), + m_precond(m), + m_rules(rm), + m_matcher(m), + m_subst(m) {} + + void insert(rule* r) { + m_rules.push_back(r); + m_num_vars.push_back(1+rm.get_var_counter().get_max_var(*r)); + } + + void setup(rule const& r) { + m_preds.reset(); + m_index = 0; + 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(); + var_subst vs(m, false); + for (unsigned i = 0; i < sorts.size(); ++i) { + if (!sorts[i]) { + sorts[i] = m.mk_bool_sort(); + } + 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); + 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); + } + m_precond = m.mk_and(fmls.size(), fmls.c_ptr()); + IF_VERBOSE(1, r.display(m_ctx, verbose_stream() << "setup-match\n");); + } + + // extract pre_cond => post_cond validation obligation from match. + bool next_match(expr_ref& pre_cond, expr_ref& post_cond) { + for (; m_index < m_rules.size(); ++m_index) { + if (try_match(pre_cond, post_cond)) { + return true; + } + } + return false; + } + private: + // + // check that each predicate in r is matched by some predicate in premise. + // for now: skip multiple matches within the same rule (incomplete). + // + bool try_match(expr_ref& pre_cond, expr_ref& post_cond) { + rule const& r = *m_rules[m_index]; + unsigned num_vars = m_num_vars[m_index]; + m_subst.reset(); + m_subst.reserve(2, num_vars); + unsigned deltas[2] = {0, 0}; + expr_ref_vector fmls(m); + expr_ref q(m); + unsigned utsz = r.get_uninterpreted_tail_size(); + unsigned tsz = r.get_tail_size(); + + IF_VERBOSE(1, r.display(m_ctx, verbose_stream() << "try-match\n");); + + for (unsigned i = 0; i < utsz; ++i) { + m_subst.push_scope(); + if (!try_match(r.get_tail(i))) { + return false; + } + } + 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); + } + + pre_cond = m_precond; + post_cond = m.mk_and(fmls.size(), fmls.c_ptr()); + IF_VERBOSE(1, verbose_stream() << "match: " << mk_pp(post_cond, m) << "\n";); + // TBD: + // - existential closure of post_cond + // - eliminate variables from post_cond + return true; + } + + bool try_match(expr* q) { + for (unsigned i = 0; i < m_preds.size(); ++i) { + if (m_matcher(q, m_preds[i].get(), m_subst)) { + return true; + } + else { + // undo effect of failed match attempt. + m_subst.pop_scope(); + m_subst.push_scope(); + } + } + return false; + } + }; + enum tab_instruction { SELECT_RULE, SELECT_PREDICATE, @@ -54,13 +179,13 @@ namespace datalog { std::ostream& operator<<(std::ostream& out, tab_instruction i) { switch(i) { - case SELECT_RULE: return out << "select-rule"; + case SELECT_RULE: return out << "select-rule"; case SELECT_PREDICATE: return out << "select-predicate"; - case BACKTRACK: return out << "backtrack"; - case NEXT_RULE: return out << "next-rule"; - case SATISFIABLE: return out << "sat"; - case UNSATISFIABLE: return out << "unsat"; - case CANCEL: return out << "cancel"; + case BACKTRACK: return out << "backtrack"; + case NEXT_RULE: return out << "next-rule"; + case SATISFIABLE: return out << "sat"; + case UNSATISFIABLE: return out << "unsat"; + case CANCEL: return out << "cancel"; } return out << "unmatched instruction"; } @@ -77,6 +202,9 @@ namespace datalog { context& m_ctx; ast_manager& m; rule_manager& rm; + tab_index m_subsumption_index; + smt_params m_fparams; + smt::kernel m_solver; rule_unifier m_unifier; rule_set m_rules; trail_stack m_trail; @@ -92,6 +220,8 @@ namespace datalog { m_ctx(ctx), m(ctx.get_manager()), rm(ctx.get_rule_manager()), + m_subsumption_index(m, rm, ctx), + m_solver(m, m_fparams), m_unifier(ctx), m_rules(ctx), m_trail(*this), @@ -101,7 +231,11 @@ namespace datalog { m_predicate_index(0), m_rule_index(0), m_cancel(false) - {} + { + // m_fparams.m_relevancy_lvl = 0; + m_fparams.m_mbqi = false; + m_fparams.m_soft_timeout = 1000; + } ~imp() {} @@ -148,13 +282,15 @@ namespace datalog { } else { m_instruction = SELECT_RULE; - m_predicate_index = 0; // TBD replace by better selection function. + m_predicate_index = 0; // TBD replace by better selection function. m_rule_index = 0; + IF_VERBOSE(1, verbose_stream() << mk_pp(m_query->get_tail(m_predicate_index), m) << "\n";); } } void apply_rule(rule const& r) { m_rule_index++; + IF_VERBOSE(1, r.display(m_ctx, verbose_stream());); bool can_unify = m_unifier.unify_rules(*m_query, m_predicate_index, r); if (can_unify) { m_stats.m_num_unfold++; @@ -162,18 +298,24 @@ namespace datalog { m_trail.push(value_trail(m_rule_index)); m_trail.push(value_trail(m_predicate_index)); rule_ref new_query(rm); - m_unifier.apply(*m_query, m_predicate_index, r, new_query); - m_trail.push(restore_rule(m_query_trail, m_query)); - m_query = new_query; - TRACE("dl", m_query->display(m_ctx, tout);); - if (l_false == query_is_sat()) { - m_instruction = BACKTRACK; - } - else if (l_true == query_is_subsumed()) { - NOT_IMPLEMENTED_YET(); + bool is_feasible = m_unifier.apply(*m_query, m_predicate_index, r, new_query); + if (is_feasible) { + TRACE("dl", m_query->display(m_ctx, tout);); + if (l_false == query_is_sat(*new_query.get())) { + m_instruction = BACKTRACK; + } + else if (l_true == query_is_subsumed(*new_query.get())) { + m_instruction = BACKTRACK; + } + else { + m_subsumption_index.insert(m_query.get()); + m_trail.push(restore_rule(m_query_trail, m_query)); + m_query = new_query; + m_instruction = SELECT_PREDICATE; + } } else { - m_instruction = SELECT_PREDICATE; + m_instruction = BACKTRACK; } } else { @@ -212,7 +354,7 @@ namespace datalog { lbool run() { m_instruction = SELECT_PREDICATE; while (true) { - IF_VERBOSE(1, verbose_stream() << "run " << m_instruction << "\n";); + IF_VERBOSE(1, verbose_stream() << "run " << m_trail.get_num_scopes() << " " << m_instruction << "\n";); if (m_cancel) { cleanup(); return l_undef; @@ -241,16 +383,55 @@ namespace datalog { } } - lbool query_is_sat() { + lbool query_is_sat(rule const& query) { expr_ref_vector fmls(m); + expr_ref fml(m); + unsigned utsz = query.get_uninterpreted_tail_size(); + unsigned tsz = query.get_tail_size(); + for (unsigned i = utsz; i < tsz; ++i) { + fmls.push_back(query.get_tail(i)); + } + ptr_vector sorts; + svector names; + query.get_vars(sorts); + sorts.reverse(); + for (unsigned i = 0; i < sorts.size(); ++i) { + if (!sorts[i]) { + sorts[i] = m.mk_bool_sort(); + } + 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); + m_solver.push(); + m_solver.assert_expr(fml); + lbool is_sat = m_solver.check(); + m_solver.pop(1); - return l_undef; + TRACE("dl", tout << is_sat << ":\n" << mk_pp(fml, m) << "\n";); + + return is_sat; } - lbool query_is_subsumed() { - return l_undef; + lbool query_is_subsumed(rule const& query) { + lbool is_subsumed = l_false; + m_subsumption_index.setup(query); + expr_ref precond(m), postcond(m); + while (m_subsumption_index.next_match(precond, postcond)) { + if (is_ground(postcond)) { + postcond = m.mk_not(postcond); + m_solver.push(); + m_solver.assert_expr(precond); + m_solver.assert_expr(postcond); + lbool is_sat = m_solver.check(); + m_solver.pop(1); + if (is_sat == l_false) { + return l_true; + } + } + } + return is_subsumed; } - }; tab::tab(context& ctx): diff --git a/src/test/matcher.cpp b/src/test/matcher.cpp index aaab9905c..cfbab2d3c 100644 --- a/src/test/matcher.cpp +++ b/src/test/matcher.cpp @@ -19,6 +19,8 @@ Revision History: #ifdef _WINDOWS #include"matcher.h" #include"ast_pp.h" +#include "reg_decl_plugins.h" + void tst_match(ast_manager & m, app * t, app * i) { substitution s(m); @@ -72,6 +74,7 @@ void tst_match(ast_manager & m, app * t, app * i) { void tst1() { ast_manager m; + reg_decl_plugins(m); sort_ref s( m.mk_sort(symbol("S")), m); func_decl_ref g( m.mk_func_decl(symbol("g"), s, s), m); func_decl_ref h( m.mk_func_decl(symbol("h"), s, s), m);