From 3c9c7574f7f4b33baddbac6e31daa7df0b076c83 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 31 Jan 2013 17:32:07 -0800 Subject: [PATCH] add release mode to vs build, work on delta extraction Signed-off-by: Nikolaj Bjorner --- scripts/mk_util.py | 41 +++++++++++++++++ src/muz_qe/tab_context.cpp | 90 ++++++++++++++++++++++++++++++++++---- 2 files changed, 123 insertions(+), 8 deletions(-) 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);