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<pdr::dl_interface> m_pdr;
scoped_ptr<bmc> m_bmc;
scoped_ptr<rel_context> m_rel;
+ scoped_ptr<tab> 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<smtlib::parser> 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<unsigned>(end-it), it);
-
- it = p->get_benchmark()->begin_formulas();
- end = p->get_benchmark()->end_formulas();
- B = m.mk_and(static_cast<unsigned>(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<imp> 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<imp,unsigned>(m_rule_index));
+ m_trail.push(value_trail<imp,unsigned>(m_predicate_index));
rule_ref new_query(rm);
m_unifier.apply(*m_query, m_predicate_index, r, new_query);
m_trail.push(restore_rule<imp>(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<imp,unsigned>(m_rule_index));
- m_trail.push(value_trail<imp,unsigned>(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;
+ }
};