diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index a9b3af1cb..98d9ad6f8 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -2298,6 +2298,10 @@ def mk_vs_proj(name, components):
f.write(' Debug\n')
f.write(' Win32\n')
f.write(' \n')
+ f.write(' \n')
+ f.write(' Release\n')
+ f.write(' Win32\n')
+ f.write(' \n')
f.write(' \n')
f.write(' \n')
f.write(' {%s}\n' % mk_gui_str(0))
@@ -2320,6 +2324,9 @@ def mk_vs_proj(name, components):
f.write(' $(SolutionDir)$(Configuration)\\n')
f.write(' %s\n' % name)
f.write(' .exe\n')
+ f.write(' $(SolutionDir)$(Configuration)\\n')
+ f.write(' %s\n' % name)
+ f.write(' .exe\n')
f.write(' \n')
f.write(' \n')
f.write(' \n')
@@ -2355,6 +2362,40 @@ def mk_vs_proj(name, components):
f.write('psapi.lib;kernel32.lib;user32.lib;gdi32.lib;winspool.lib;comdlg32.lib;advapi32.lib;shell32.lib;ole32.lib;oleaut32.lib;uuid.lib;odbc32.lib;odbccp32.lib;%(AdditionalDependencies)\n')
f.write(' \n')
f.write(' \n')
+ f.write(' \n')
+ f.write(' \n')
+ f.write(' Disabled\n')
+ f.write(' WIN32;_NDEBUG;_MP_INTERNAL;_WINDOWS;%(PreprocessorDefinitions)\n')
+ f.write(' true\n')
+ f.write(' EnableFastChecks\n')
+ f.write(' Level3\n')
+ f.write(' MultiThreadedDLL\n')
+ f.write(' true\n')
+ f.write(' ProgramDatabase\n')
+ f.write(' ')
+ deps = find_all_deps(name, components)
+ first = True
+ for dep in deps:
+ if first:
+ first = False
+ else:
+ f.write(';')
+ f.write(get_component(dep).to_src_dir)
+ f.write('\n')
+ f.write(' \n')
+ f.write(' \n')
+ f.write(' $(OutDir)%s.exe\n' % name)
+ f.write(' true\n')
+ f.write(' Console\n')
+ f.write(' 8388608\n')
+ f.write(' false\n')
+ f.write(' \n')
+ f.write(' \n')
+ f.write(' MachineX86\n')
+ f.write(' %(AdditionalLibraryDirectories)\n')
+ f.write('psapi.lib;kernel32.lib;user32.lib;gdi32.lib;winspool.lib;comdlg32.lib;advapi32.lib;shell32.lib;ole32.lib;oleaut32.lib;uuid.lib;odbc32.lib;odbccp32.lib;%(AdditionalDependencies)\n')
+ f.write(' \n')
+ f.write(' \n')
f.write(' \n')
for dep in deps:
dep = get_component(dep)
diff --git a/src/muz_qe/tab_context.cpp b/src/muz_qe/tab_context.cpp
index ee6692d6c..333a96de0 100644
--- a/src/muz_qe/tab_context.cpp
+++ b/src/muz_qe/tab_context.cpp
@@ -164,10 +164,10 @@ namespace tb {
public:
- clause(datalog::rule_manager& rm):
- m_head(rm.get_manager()),
- m_predicates(rm.get_manager()),
- m_constraint(rm.get_manager()),
+ clause(ast_manager& m):
+ m_head(m),
+ m_predicates(m),
+ m_constraint(m),
m_seqno(0),
m_index(0),
m_num_vars(0),
@@ -437,7 +437,7 @@ namespace tb {
datalog::rule_set::iterator end = rules.end();
for (unsigned i = 0; it != end; ++it) {
r = *it;
- ref g = alloc(clause, rm);
+ ref g = alloc(clause, rm.get_manager());
g->init(r);
g->set_index(i++);
insert(g);
@@ -455,7 +455,7 @@ namespace tb {
unsigned get_num_rules(func_decl* p) const {
map::obj_map_entry* e = m_index.find_core(p);
- if (p) {
+ if (e) {
return e->get_data().get_value().size();
}
else {
@@ -727,6 +727,7 @@ namespace tb {
}
};
+
// predicate selection strategy.
class selection {
enum strategy {
@@ -1091,7 +1092,7 @@ namespace tb {
app_ref_vector predicates(m);
expr_ref tmp(m), tmp2(m), constraint(m);
app_ref head(m);
- result = alloc(clause, m_ctx.get_rule_manager());
+ result = alloc(clause, m);
unsigned delta[2] = { 0, var_cnt };
m_S1.apply(2, delta, expr_offset(tgt.get_head(), 0), tmp);
head = to_app(tmp);
@@ -1199,6 +1200,79 @@ namespace tb {
}
};
+ //
+ // Given a clause
+ // P(s) :- P(t), Phi(x).
+ // Compute the clauses:
+ // acc: P(s) :- Delta(z,t), P(z), Phi(x).
+ // delta1: Delta(z,z).
+ // delta2: Delta(z,s) :- Delta(z,t), Phi(x).
+ //
+
+ class extract_delta {
+ ast_manager& m;
+ public:
+ extract_delta(ast_manager& m):
+ m(m)
+ {}
+
+ void operator()(clause const& g, ref& acc, ref& delta1, ref& delta2) {
+ SASSERT(g.get_num_predicates() > 0);
+ app* p = g.get_head();
+ app* q = g.get_predicate(0);
+ SASSERT(p->get_decl() == q->get_decl());
+ expr_ref_vector zs = mk_fresh_vars(g);
+ expr_ref_vector zszs(m);
+ func_decl_ref delta(m);
+ sort_ref_vector dom(m);
+ for (unsigned j = 0; j < 1; ++j) {
+ for (unsigned i = 0; i < zs.size(); ++i) {
+ dom.push_back(m.get_sort(zs[i].get()));
+ zszs.push_back(zs[i].get());
+ }
+ }
+ app_ref_vector preds(m);
+ delta = m.mk_fresh_func_decl("Delta", dom.size(), dom.c_ptr(), m.mk_bool_sort());
+ acc = alloc(clause, m);
+ delta1 = alloc(clause, m);
+ delta2 = alloc(clause, m);
+ delta1->init(m.mk_app(delta, zszs.size(), zszs.c_ptr()), preds, m.mk_true());
+ for (unsigned i = 0; i < zs.size(); ++i) {
+ zszs[i+zs.size()] = p->get_arg(i);
+ }
+ app_ref head(m), pred(m);
+ head = m.mk_app(delta, zszs.size(), zszs.c_ptr());
+ for (unsigned i = 0; i < zs.size(); ++i) {
+ zszs[i+zs.size()] = q->get_arg(i);
+ }
+ pred = m.mk_app(delta, zszs.size(), zszs.c_ptr());
+ preds.push_back(pred);
+ for (unsigned i = 1; i < g.get_num_predicates(); ++i) {
+ preds.push_back(g.get_predicate(i));
+ }
+ delta2->init(head, preds, g.get_constraint());
+ preds.push_back(m.mk_app(q->get_decl(), zs.size(), zs.c_ptr()));
+ acc->init(p, preds, g.get_constraint());
+
+ IF_VERBOSE(1,
+ delta1->display(verbose_stream() << "delta1:\n");
+ delta2->display(verbose_stream() << "delta2:\n");
+ acc->display(verbose_stream() << "acc:\n"););
+ }
+
+ private:
+
+ expr_ref_vector mk_fresh_vars(clause const& g) {
+ expr_ref_vector result(m);
+ app* p = g.get_head();
+ unsigned num_vars = g.get_num_vars();
+ for (unsigned i = 0; i < p->get_num_args(); ++i) {
+ result.push_back(m.mk_var(num_vars+i, m.get_sort(p->get_arg(i))));
+ }
+ return result;
+ }
+ };
+
enum instruction {
SELECT_RULE,
SELECT_PREDICATE,
@@ -1282,7 +1356,7 @@ namespace datalog {
func_decl_ref query_pred(m);
rm.mk_query(query, query_pred, query_rules, clause);
- ref g = alloc(tb::clause, rm);
+ ref g = alloc(tb::clause, m);
g->init(clause);
g->set_head(m.mk_false());
init_clause(g);