From b19a47176bfc8f973b46207d089eabfa3cf20ccb Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 17 Jan 2013 08:17:21 -0800 Subject: [PATCH 1/2] working on tab Signed-off-by: Nikolaj Bjorner --- src/muz_qe/dl_context.cpp | 55 ++++++++++++++-- src/muz_qe/dl_context.h | 6 ++ src/muz_qe/dl_util.h | 1 + src/muz_qe/pdr_farkas_learner.cpp | 33 ---------- src/muz_qe/pdr_farkas_learner.h | 2 - src/muz_qe/tab_context.cpp | 103 ++++++++++++++++++++++-------- src/tactic/tactical.cpp | 1 - 7 files changed, 131 insertions(+), 70 deletions(-) diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp index 5581732c8..8ef2ffa22 100644 --- a/src/muz_qe/dl_context.cpp +++ b/src/muz_qe/dl_context.cpp @@ -544,14 +544,16 @@ namespace datalog { unsigned context::get_num_levels(func_decl* pred) { switch(get_engine()) { case DATALOG_ENGINE: - throw default_exception("get_num_levels is unsupported for datalog engine"); + throw default_exception("get_num_levels is not supported for datalog engine"); case PDR_ENGINE: case QPDR_ENGINE: ensure_pdr(); return m_pdr->get_num_levels(pred); case BMC_ENGINE: case QBMC_ENGINE: - throw default_exception("get_num_levels is unsupported for bmc"); + throw default_exception("get_num_levels is not supported for bmc"); + case TAB_ENGINE: + throw default_exception("get_num_levels is not supported for tab"); default: throw default_exception("unknown engine"); } @@ -560,14 +562,16 @@ namespace datalog { expr_ref context::get_cover_delta(int level, func_decl* pred) { switch(get_engine()) { case DATALOG_ENGINE: - throw default_exception("operation is unsupported for datalog engine"); + throw default_exception("operation is not supported for datalog engine"); case PDR_ENGINE: case QPDR_ENGINE: ensure_pdr(); return m_pdr->get_cover_delta(level, pred); case BMC_ENGINE: case QBMC_ENGINE: - throw default_exception("operation is unsupported for BMC engine"); + throw default_exception("operation is not supported for BMC engine"); + case TAB_ENGINE: + throw default_exception("operation is not supported for TAB engine"); default: throw default_exception("unknown engine"); } @@ -576,7 +580,7 @@ namespace datalog { void context::add_cover(int level, func_decl* pred, expr* property) { switch(get_engine()) { case DATALOG_ENGINE: - throw default_exception("operation is unsupported for datalog engine"); + throw default_exception("operation is not supported for datalog engine"); case PDR_ENGINE: case QPDR_ENGINE: ensure_pdr(); @@ -584,7 +588,9 @@ namespace datalog { break; case BMC_ENGINE: case QBMC_ENGINE: - throw default_exception("operation is unsupported for BMC engine"); + throw default_exception("operation is not supported for BMC engine"); + case TAB_ENGINE: + throw default_exception("operation is not supported for TAB engine"); default: throw default_exception("unknown engine"); } @@ -720,7 +726,11 @@ namespace datalog { case QBMC_ENGINE: check_existential_tail(r); check_positive_predicates(r); - break; + break; + case TAB_ENGINE: + check_existential_tail(r); + check_positive_predicates(r); + break; default: UNREACHABLE(); break; @@ -921,6 +931,7 @@ namespace datalog { if (m_pdr.get()) m_pdr->cancel(); if (m_bmc.get()) m_bmc->cancel(); if (m_rel.get()) m_rel->cancel(); + if (m_tab.get()) m_tab->cancel(); } void context::cleanup() { @@ -928,6 +939,7 @@ namespace datalog { if (m_pdr.get()) m_pdr->cleanup(); if (m_bmc.get()) m_bmc->cleanup(); if (m_rel.get()) m_rel->cleanup(); + if (m_tab.get()) m_tab->cleanup(); } class context::engine_type_proc { @@ -974,6 +986,9 @@ namespace datalog { else if (e == symbol("qbmc")) { m_engine = QBMC_ENGINE; } + else if (e == symbol("tab")) { + m_engine = TAB_ENGINE; + } if (m_engine == LAST_ENGINE) { expr_fast_mark1 mark; @@ -1008,6 +1023,8 @@ namespace datalog { case BMC_ENGINE: case QBMC_ENGINE: return bmc_query(query); + case TAB_ENGINE: + return tab_query(query); default: UNREACHABLE(); return rel_query(query); @@ -1064,6 +1081,17 @@ namespace datalog { return m_bmc->query(query); } + void context::ensure_tab() { + if (!m_tab.get()) { + m_tab = alloc(tab, *this); + } + } + + lbool context::tab_query(expr* query) { + ensure_tab(); + return m_tab->query(query); + } + void context::ensure_rel() { if (!m_rel.get()) { m_rel = alloc(rel_context, *this); @@ -1100,6 +1128,10 @@ namespace datalog { ensure_rel(); m_last_answer = m_rel->get_last_answer(); return m_last_answer.get(); + case TAB_ENGINE: + ensure_tab(); + m_last_answer = m_tab->get_answer(); + return m_last_answer.get(); default: UNREACHABLE(); } @@ -1120,6 +1152,10 @@ namespace datalog { ensure_bmc(); m_bmc->display_certificate(out); return true; + case TAB_ENGINE: + ensure_tab(); + m_tab->display_certificate(out); + return true; default: return false; } @@ -1151,6 +1187,11 @@ namespace datalog { m_bmc->collect_statistics(st); } break; + case TAB_ENGINE: + if (m_tab) { + m_tab->collect_statistics(st); + } + break; default: break; } diff --git a/src/muz_qe/dl_context.h b/src/muz_qe/dl_context.h index d3309beb5..98380c9c8 100644 --- a/src/muz_qe/dl_context.h +++ b/src/muz_qe/dl_context.h @@ -35,6 +35,7 @@ Revision History: #include"dl_rule_set.h" #include"pdr_dl_interface.h" #include"dl_bmc_engine.h" +#include"tab_context.h" #include"rel_context.h" #include"lbool.h" #include"statistics.h" @@ -100,6 +101,7 @@ namespace datalog { scoped_ptr m_pdr; scoped_ptr m_bmc; scoped_ptr m_rel; + scoped_ptr m_tab; bool m_closed; bool m_saturation_was_run; @@ -434,6 +436,8 @@ namespace datalog { void ensure_bmc(); + void ensure_tab(); + void ensure_rel(); void new_query(); @@ -444,6 +448,8 @@ namespace datalog { lbool bmc_query(expr* query); + lbool tab_query(expr* query); + void check_quantifier_free(rule_ref& r); void check_uninterpreted_free(rule_ref& r); void check_existential_tail(rule_ref& r); diff --git a/src/muz_qe/dl_util.h b/src/muz_qe/dl_util.h index d9e437ccc..99256e70a 100644 --- a/src/muz_qe/dl_util.h +++ b/src/muz_qe/dl_util.h @@ -52,6 +52,7 @@ namespace datalog { QPDR_ENGINE, BMC_ENGINE, QBMC_ENGINE, + TAB_ENGINE, LAST_ENGINE }; diff --git a/src/muz_qe/pdr_farkas_learner.cpp b/src/muz_qe/pdr_farkas_learner.cpp index b8e043806..489b2437e 100644 --- a/src/muz_qe/pdr_farkas_learner.cpp +++ b/src/muz_qe/pdr_farkas_learner.cpp @@ -860,38 +860,5 @@ namespace pdr { } - void farkas_learner::test(char const* filename) { -#if 0 - // [Leo]: disabled because it uses an external component: SMT 1.0 parser - if (!filename) { - test(); - return; - } - ast_manager m; - reg_decl_plugins(m); - scoped_ptr p = smtlib::parser::create(m); - p->initialize_smtlib(); - - if (!p->parse_file(filename)) { - warning_msg("Failed to parse file %s\n", filename); - return; - } - expr_ref A(m), B(m); - - smtlib::theory::expr_iterator it = p->get_benchmark()->begin_axioms(); - smtlib::theory::expr_iterator end = p->get_benchmark()->end_axioms(); - A = m.mk_and(static_cast(end-it), it); - - it = p->get_benchmark()->begin_formulas(); - end = p->get_benchmark()->end_formulas(); - B = m.mk_and(static_cast(end-it), it); - - smt_params params; - pdr::farkas_learner fl(params, m); - expr_ref_vector lemmas(m); - bool res = fl.get_lemma_guesses(A, B, lemmas); - std::cout << "lemmas: " << pp_cube(lemmas, m) << "\n"; -#endif - } }; diff --git a/src/muz_qe/pdr_farkas_learner.h b/src/muz_qe/pdr_farkas_learner.h index 809f4cd7e..eb38455ab 100644 --- a/src/muz_qe/pdr_farkas_learner.h +++ b/src/muz_qe/pdr_farkas_learner.h @@ -99,8 +99,6 @@ public: void collect_statistics(statistics& st) const; - static void test(char const* filename); - }; diff --git a/src/muz_qe/tab_context.cpp b/src/muz_qe/tab_context.cpp index 81db5c5d0..c025a9ec5 100644 --- a/src/muz_qe/tab_context.cpp +++ b/src/muz_qe/tab_context.cpp @@ -30,7 +30,9 @@ namespace datalog { rule_ref_vector& m_rules; rule_ref& m_rule; - restore_rule(rule_ref_vector& rules, rule_ref& rule): m_rules(rules), m_rule(rule) { + restore_rule(rule_ref_vector& rules, rule_ref& rule): + m_rules(rules), + m_rule(rule) { m_rules.push_back(m_rule); } @@ -40,28 +42,51 @@ namespace datalog { } }; + enum tab_instruction { + SELECT_RULE, + SELECT_PREDICATE, + BACKTRACK, + NEXT_RULE, + SATISFIABLE, + UNSATISFIABLE, + CANCEL + }; + + std::ostream& operator<<(std::ostream& out, tab_instruction i) { + switch(i) { + 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"; + } + return out << "unmatched instruction"; + } + class tab::imp { - enum instruction { - SELECT_RULE, - SELECT_PREDICATE, - BACKTRACK, - NEXT_RULE, - SATISFIABLE, - UNSATISFIABLE, - CANCEL + struct stats { + stats() { reset(); } + void reset() { memset(this, 0, sizeof(*this)); } + unsigned m_num_unfold; + unsigned m_num_no_unfold; + unsigned m_num_subsume; }; + context& m_ctx; ast_manager& m; rule_manager& rm; rule_unifier m_unifier; rule_set m_rules; trail_stack m_trail; - instruction m_instruction; + tab_instruction m_instruction; rule_ref m_query; rule_ref_vector m_query_trail; unsigned m_predicate_index; unsigned m_rule_index; volatile bool m_cancel; + stats m_stats; public: imp(context& ctx): m_ctx(ctx), @@ -99,10 +124,12 @@ namespace datalog { m_query_trail.reset(); } void reset_statistics() { - // TBD + m_stats.reset(); } void collect_statistics(statistics& st) const { - // TBD + 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); } void display_certificate(std::ostream& out) const { // TBD @@ -111,12 +138,13 @@ namespace datalog { // TBD return expr_ref(0, m); } -private: + private: void select_predicate() { unsigned num_predicates = m_query->get_uninterpreted_tail_size(); if (num_predicates == 0) { m_instruction = UNSATISFIABLE; + IF_VERBOSE(1, m_query->display(m_ctx, verbose_stream()); ); } else { m_instruction = SELECT_RULE; @@ -125,37 +153,47 @@ private: } } - void apply_rule(rule const& r) { + void apply_rule(rule const& r) { + m_rule_index++; bool can_unify = m_unifier.unify_rules(*m_query, m_predicate_index, r); if (can_unify) { + m_stats.m_num_unfold++; + m_trail.push_scope(); + 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(); + } + else { + m_instruction = SELECT_PREDICATE; + } } else { - m_instruction = NEXT_RULE; + m_stats.m_num_no_unfold++; + m_instruction = SELECT_RULE; } } void select_rule() { func_decl* p = m_query->get_decl(m_predicate_index); rule_vector const& rules = m_rules.get_predicate_rules(p); - if (rules.size() >= m_rule_index) { + if (rules.size() <= m_rule_index) { m_instruction = BACKTRACK; } else { - rule* r = rules[m_rule_index]; - m_trail.push_scope(); - m_rule_index++; - m_trail.push(value_trail(m_rule_index)); - m_trail.push(value_trail(m_predicate_index)); - apply_rule(*r); + apply_rule(*rules[m_rule_index]); } } - void backtrack() { + void backtrack() { if (m_trail.get_num_scopes() == 0) { m_instruction = SATISFIABLE; } @@ -174,8 +212,9 @@ private: lbool run() { m_instruction = SELECT_PREDICATE; while (true) { + IF_VERBOSE(1, verbose_stream() << "run " << m_instruction << "\n";); if (m_cancel) { - m_cancel = false; + cleanup(); return l_undef; } switch(m_instruction) { @@ -192,15 +231,25 @@ private: next_rule(); break; case SATISFIABLE: - return l_true; - case UNSATISFIABLE: return l_false; + case UNSATISFIABLE: + return l_true; case CANCEL: m_cancel = false; return l_undef; } } - } + } + + lbool query_is_sat() { + expr_ref_vector fmls(m); + + return l_undef; + } + + lbool query_is_subsumed() { + return l_undef; + } }; diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp index ca66b7a14..c3152ed58 100644 --- a/src/tactic/tactical.cpp +++ b/src/tactic/tactical.cpp @@ -19,7 +19,6 @@ Notes: #include"tactical.h" #include"scoped_timer.h" #include"cancel_eh.h" -#include"cooperate.h" #include"scoped_ptr_vector.h" #include"z3_omp.h" From c0f22039e41880069311f90ca8ebf5f772f0c4b5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 17 Jan 2013 08:23:09 -0800 Subject: [PATCH 2/2] add back cooperate.h include (not used now, but will be) Signed-off-by: Nikolaj Bjorner --- src/tactic/tactical.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp index c3152ed58..ca66b7a14 100644 --- a/src/tactic/tactical.cpp +++ b/src/tactic/tactical.cpp @@ -19,6 +19,7 @@ Notes: #include"tactical.h" #include"scoped_timer.h" #include"cancel_eh.h" +#include"cooperate.h" #include"scoped_ptr_vector.h" #include"z3_omp.h"