From b65adc10da41a90f883592424c52e1f9bd683d12 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 7 May 2013 17:58:43 +0100 Subject: [PATCH 01/26] FPA: bugfix for quantified FP -> quantified BV conversion. Signed-off-by: Christoph M. Wintersteiger --- src/tactic/fpa/fpa2bv_rewriter.h | 41 ++++++++++++++++---------------- 1 file changed, 21 insertions(+), 20 deletions(-) diff --git a/src/tactic/fpa/fpa2bv_rewriter.h b/src/tactic/fpa/fpa2bv_rewriter.h index aec00d30c..a891337ec 100644 --- a/src/tactic/fpa/fpa2bv_rewriter.h +++ b/src/tactic/fpa/fpa2bv_rewriter.h @@ -166,9 +166,11 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { bool pre_visit(expr * t) { + TRACE("fpa2bv", tout << "pre_visit: " << mk_ismt2_pp(t, m()) << std::endl;); + if (is_quantifier(t)) { quantifier * q = to_quantifier(t); - TRACE("fpa2bv", tout << "pre_visit [" << q->get_id() << "]: " << mk_ismt2_pp(q->get_expr(), m()) << std::endl;); + TRACE("fpa2bv", tout << "pre_visit quantifier [" << q->get_id() << "]: " << mk_ismt2_pp(q->get_expr(), m()) << std::endl;); sort_ref_vector new_bindings(m_manager); for (unsigned i = 0 ; i < q->get_num_decls(); i++) new_bindings.push_back(q->get_decl_sort(i)); @@ -199,17 +201,9 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { unsigned ebits = m_conv.fu().get_ebits(s); unsigned sbits = m_conv.fu().get_sbits(s); name_buffer.reset(); - name_buffer << n << ".exp"; + name_buffer << n << ".bv"; new_decl_names.push_back(symbol(name_buffer.c_str())); - new_decl_sorts.push_back(m_conv.bu().mk_sort(ebits)); - name_buffer.reset(); - name_buffer << n << ".sig"; - new_decl_names.push_back(symbol(name_buffer.c_str())); - new_decl_sorts.push_back(m_conv.bu().mk_sort(sbits-1)); - name_buffer.reset(); - name_buffer << n << ".sgn"; - new_decl_names.push_back(symbol(name_buffer.c_str())); - new_decl_sorts.push_back(m_conv.bu().mk_sort(1)); + new_decl_sorts.push_back(m_conv.bu().mk_sort(sbits+ebits)); } else { new_decl_sorts.push_back(s); @@ -231,19 +225,26 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { bool reduce_var(var * t, expr_ref & result, proof_ref & result_pr) { if (t->get_idx() >= m_bindings.size()) - return false; + return false; unsigned inx = m_bindings.size() - t->get_idx() - 1; if (m_mappings[inx] == 0) { - unsigned shift = 0; - for (unsigned i = m_bindings.size() - 1; i > inx; i--) - if (m_conv.is_float(m_bindings[i].get())) shift += 2; - expr_ref new_var(m()); - if (m_conv.is_float(t->get_sort())) - m_conv.mk_var(t->get_idx() + shift, t->get_sort(), new_var); + expr_ref new_exp(m()); + sort * s = t->get_sort(); + if (m_conv.is_float(s)) + { + expr_ref new_var(m()); + unsigned ebits = m_conv.fu().get_ebits(s); + unsigned sbits = m_conv.fu().get_sbits(s); + new_var = m().mk_var(t->get_idx(), m_conv.bu().mk_sort(sbits+ebits)); + m_conv.mk_triple(m_conv.bu().mk_extract(sbits+ebits-1, sbits+ebits-1, new_var), + m_conv.bu().mk_extract(sbits+ebits-2, ebits, new_var), + m_conv.bu().mk_extract(ebits-1, 0, new_var), + new_exp); + } else - new_var = m().mk_var(t->get_idx() + shift, t->get_sort()); - m_mappings[inx] = new_var; + new_exp = m().mk_var(t->get_idx(), s); + m_mappings[inx] = new_exp; } result = m_mappings[inx].get(); result_pr = 0; From 787a65be299e88eb7dd4628e5858b5ecb53026ba Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 7 May 2013 18:27:47 +0100 Subject: [PATCH 02/26] FPA: bugfix for QFPA -> QBV conversion. Signed-off-by: Christoph M. Wintersteiger --- src/tactic/fpa/fpa2bv_rewriter.h | 36 ++++++++++++++++---------------- 1 file changed, 18 insertions(+), 18 deletions(-) diff --git a/src/tactic/fpa/fpa2bv_rewriter.h b/src/tactic/fpa/fpa2bv_rewriter.h index a891337ec..3398874f5 100644 --- a/src/tactic/fpa/fpa2bv_rewriter.h +++ b/src/tactic/fpa/fpa2bv_rewriter.h @@ -30,7 +30,8 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { expr_ref_vector m_out; fpa2bv_converter & m_conv; sort_ref_vector m_bindings; - expr_ref_vector m_mappings; + expr_ref_vector m_mappings; + unsigned long long m_max_memory; unsigned m_max_steps; @@ -227,25 +228,24 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { if (t->get_idx() >= m_bindings.size()) return false; unsigned inx = m_bindings.size() - t->get_idx() - 1; - if (m_mappings[inx] == 0) + + expr_ref new_exp(m()); + sort * s = t->get_sort(); + if (m_conv.is_float(s)) { - expr_ref new_exp(m()); - sort * s = t->get_sort(); - if (m_conv.is_float(s)) - { - expr_ref new_var(m()); - unsigned ebits = m_conv.fu().get_ebits(s); - unsigned sbits = m_conv.fu().get_sbits(s); - new_var = m().mk_var(t->get_idx(), m_conv.bu().mk_sort(sbits+ebits)); - m_conv.mk_triple(m_conv.bu().mk_extract(sbits+ebits-1, sbits+ebits-1, new_var), - m_conv.bu().mk_extract(sbits+ebits-2, ebits, new_var), - m_conv.bu().mk_extract(ebits-1, 0, new_var), - new_exp); - } - else - new_exp = m().mk_var(t->get_idx(), s); - m_mappings[inx] = new_exp; + expr_ref new_var(m()); + unsigned ebits = m_conv.fu().get_ebits(s); + unsigned sbits = m_conv.fu().get_sbits(s); + new_var = m().mk_var(t->get_idx(), m_conv.bu().mk_sort(sbits+ebits)); + m_conv.mk_triple(m_conv.bu().mk_extract(sbits+ebits-1, sbits+ebits-1, new_var), + m_conv.bu().mk_extract(sbits+ebits-2, ebits, new_var), + m_conv.bu().mk_extract(ebits-1, 0, new_var), + new_exp); } + else + new_exp = m().mk_var(t->get_idx(), s); + m_mappings[inx] = new_exp; + result = m_mappings[inx].get(); result_pr = 0; TRACE("fpa2bv", tout << "reduce_var: " << mk_ismt2_pp(t, m()) << " -> " << mk_ismt2_pp(result, m()) << std::endl;); From c8c5f30b49405fe2ae9bcd74021f84258f91ed5d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 9 May 2013 21:30:31 -0700 Subject: [PATCH 03/26] Add new C++ APIs for creating forall/exists expressions. Signed-off-by: Leonardo de Moura --- examples/c++/example.cpp | 25 +++++++++ src/api/c++/z3++.h | 106 +++++++++++++++++++++++---------------- 2 files changed, 88 insertions(+), 43 deletions(-) diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp index bec8c59a1..55dbebe27 100644 --- a/examples/c++/example.cpp +++ b/examples/c++/example.cpp @@ -907,6 +907,7 @@ void enum_sort_example() { } void expr_vector_example() { + std::cout << "expr_vector example\n"; context c; const unsigned N = 10; @@ -928,6 +929,29 @@ void expr_vector_example() { std::cout << "solution\n" << m; } +void exists_expr_vector_example() { + std::cout << "exists expr_vector example\n"; + context c; + const unsigned N = 10; + + expr_vector xs(c); + expr x(c); + expr b(c); + b = c.bool_val(true); + + for (unsigned i = 0; i < N; i++) { + std::stringstream x_name; + x_name << "x_" << i; + x = c.int_const(x_name.str().c_str()); + xs.push_back(x); + b = b && x >= 0; + } + + expr ex(c); + ex = exists(xs, b); + std::cout << ex << std::endl; +} + int main() { try { demorgan(); std::cout << "\n"; @@ -964,6 +988,7 @@ int main() { incremental_example3(); std::cout << "\n"; enum_sort_example(); std::cout << "\n"; expr_vector_example(); std::cout << "\n"; + exists_expr_vector_example(); std::cout << "\n"; std::cout << "done\n"; } catch (exception & ex) { diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index a044149e3..a255c2d97 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -249,6 +249,8 @@ namespace z3 { array & operator=(array const & s); public: array(unsigned sz):m_size(sz) { m_array = new T[sz]; } + template + array(ast_vector_tpl const & v); ~array() { delete[] m_array; } unsigned size() const { return m_size; } T & operator[](int i) { assert(0 <= i); assert(static_cast(i) < m_size); return m_array[i]; } @@ -939,49 +941,6 @@ namespace z3 { inline expr udiv(expr const & a, int b) { return udiv(a, a.ctx().num_val(b, a.get_sort())); } inline expr udiv(int a, expr const & b) { return udiv(b.ctx().num_val(a, b.get_sort()), b); } - // Basic functions for creating quantified formulas. - // The C API should be used for creating quantifiers with patterns, weights, many variables, etc. - inline expr forall(expr const & x, expr const & b) { - check_context(x, b); - Z3_app vars[] = {(Z3_app) x}; - Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r); - } - inline expr forall(expr const & x1, expr const & x2, expr const & b) { - check_context(x1, b); check_context(x2, b); - Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2}; - Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r); - } - inline expr forall(expr const & x1, expr const & x2, expr const & x3, expr const & b) { - check_context(x1, b); check_context(x2, b); check_context(x3, b); - Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 }; - Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r); - } - inline expr forall(expr const & x1, expr const & x2, expr const & x3, expr const & x4, expr const & b) { - check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b); - Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 }; - Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r); - } - inline expr exists(expr const & x, expr const & b) { - check_context(x, b); - Z3_app vars[] = {(Z3_app) x}; - Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r); - } - inline expr exists(expr const & x1, expr const & x2, expr const & b) { - check_context(x1, b); check_context(x2, b); - Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2}; - Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r); - } - inline expr exists(expr const & x1, expr const & x2, expr const & x3, expr const & b) { - check_context(x1, b); check_context(x2, b); check_context(x3, b); - Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 }; - Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r); - } - inline expr exists(expr const & x1, expr const & x2, expr const & x3, expr const & x4, expr const & b) { - check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b); - Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 }; - Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r); - } - template class cast_ast; template<> class cast_ast { @@ -1043,6 +1002,67 @@ namespace z3 { friend std::ostream & operator<<(std::ostream & out, ast_vector_tpl const & v) { out << Z3_ast_vector_to_string(v.ctx(), v); return out; } }; + template + template + array::array(ast_vector_tpl const & v) { + m_array = new T[v.size()]; + m_size = v.size(); + for (unsigned i = 0; i < m_size; i++) { + m_array[i] = v[i]; + } + } + + // Basic functions for creating quantified formulas. + // The C API should be used for creating quantifiers with patterns, weights, many variables, etc. + inline expr forall(expr const & x, expr const & b) { + check_context(x, b); + Z3_app vars[] = {(Z3_app) x}; + Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r); + } + inline expr forall(expr const & x1, expr const & x2, expr const & b) { + check_context(x1, b); check_context(x2, b); + Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2}; + Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r); + } + inline expr forall(expr const & x1, expr const & x2, expr const & x3, expr const & b) { + check_context(x1, b); check_context(x2, b); check_context(x3, b); + Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 }; + Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r); + } + inline expr forall(expr const & x1, expr const & x2, expr const & x3, expr const & x4, expr const & b) { + check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b); + Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 }; + Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r); + } + inline expr forall(expr_vector const & xs, expr const & b) { + array vars(xs); + Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, vars.size(), vars.ptr(), 0, 0, b); b.check_error(); return expr(b.ctx(), r); + } + inline expr exists(expr const & x, expr const & b) { + check_context(x, b); + Z3_app vars[] = {(Z3_app) x}; + Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r); + } + inline expr exists(expr const & x1, expr const & x2, expr const & b) { + check_context(x1, b); check_context(x2, b); + Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2}; + Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r); + } + inline expr exists(expr const & x1, expr const & x2, expr const & x3, expr const & b) { + check_context(x1, b); check_context(x2, b); check_context(x3, b); + Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 }; + Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r); + } + inline expr exists(expr const & x1, expr const & x2, expr const & x3, expr const & x4, expr const & b) { + check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b); + Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 }; + Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r); + } + inline expr exists(expr_vector const & xs, expr const & b) { + array vars(xs); + Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, vars.size(), vars.ptr(), 0, 0, b); b.check_error(); return expr(b.ctx(), r); + } + class func_entry : public object { Z3_func_entry m_entry; void init(Z3_func_entry e) { From 5eed106ffe81565dcfb345d25c7f9f69dcbfbc0b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 12 May 2013 17:02:25 -0700 Subject: [PATCH 04/26] fix parameters in utvpi and make Karr invariants use backward propagation Signed-off-by: Nikolaj Bjorner --- src/muz_qe/dl_compiler.cpp | 3 +- src/muz_qe/dl_mk_karr_invariants.cpp | 83 +++++++++++++++++----------- src/muz_qe/dl_mk_karr_invariants.h | 16 +++--- src/muz_qe/dl_product_relation.cpp | 10 ++-- src/muz_qe/dl_sieve_relation.cpp | 5 +- src/smt/theory_utvpi.h | 13 +++-- src/smt/theory_utvpi_def.h | 37 ++++++++----- 7 files changed, 101 insertions(+), 66 deletions(-) diff --git a/src/muz_qe/dl_compiler.cpp b/src/muz_qe/dl_compiler.cpp index 57d9880c0..05a0d24b2 100644 --- a/src/muz_qe/dl_compiler.cpp +++ b/src/muz_qe/dl_compiler.cpp @@ -499,8 +499,7 @@ namespace datalog { expr * arg = a->get_arg(i); if(is_app(arg)) { app * c = to_app(arg); //argument is a constant - SASSERT(c->get_num_args()==0); - SASSERT(m_context.get_decl_util().is_numeral_ext(arg)); + SASSERT(m.is_value(c)); reg_idx new_reg; make_select_equal_and_project(single_res, c, single_res_expr.size(), new_reg, acc); if(single_res!=t_reg) { diff --git a/src/muz_qe/dl_mk_karr_invariants.cpp b/src/muz_qe/dl_mk_karr_invariants.cpp index d676c3dd4..143a38636 100644 --- a/src/muz_qe/dl_mk_karr_invariants.cpp +++ b/src/muz_qe/dl_mk_karr_invariants.cpp @@ -37,6 +37,7 @@ Revision History: #include"bool_rewriter.h" #include"dl_mk_backwards.h" #include"dl_mk_loop_counter.h" +#include "for_each_expr.h" namespace datalog { @@ -47,7 +48,8 @@ namespace datalog { m(ctx.get_manager()), rm(ctx.get_rule_manager()), m_inner_ctx(m, ctx.get_fparams()), - a(m) { + a(m), + m_pinned(m) { params_ref params; params.set_sym("default_relation", symbol("karr_relation")); params.set_sym("engine", symbol("datalog")); @@ -201,29 +203,27 @@ namespace datalog { return 0; } } - mk_loop_counter lc(m_ctx); mk_backwards bwd(m_ctx); scoped_ptr src_loop = lc(source); TRACE("dl", src_loop->display(tout << "source loop\n");); - // run propagation forwards, then backwards - scoped_ptr src_annot = update_using_propagation(*src_loop, *src_loop); - TRACE("dl", src_annot->display(tout << "updated using propagation\n");); + get_invariants(*src_loop); -#if 0 // figure out whether to update same rules as used for saturation. - scoped_ptr rev_source = bwd(*src_annot); - src_annot = update_using_propagation(*src_annot, *rev_source); -#endif + scoped_ptr rev_source = bwd(*src_loop); + get_invariants(*rev_source); + scoped_ptr src_annot = update_rules(*src_loop); rule_set* rules = lc.revert(*src_annot); rules->inherit_predicates(source); TRACE("dl", rules->display(tout);); + m_pinned.reset(); + m_fun2inv.reset(); return rules; } - rule_set* mk_karr_invariants::update_using_propagation(rule_set const& src, rule_set const& srcref) { + void mk_karr_invariants::get_invariants(rule_set const& src) { m_inner_ctx.reset(); rel_context& rctx = m_inner_ctx.get_rel_context(); ptr_vector heads; @@ -232,19 +232,41 @@ namespace datalog { m_inner_ctx.register_predicate(*fit, false); } m_inner_ctx.ensure_opened(); - m_inner_ctx.replace_rules(srcref); + m_inner_ctx.replace_rules(src); m_inner_ctx.close(); - rule_set::decl2rules::iterator dit = srcref.begin_grouped_rules(); - rule_set::decl2rules::iterator dend = srcref.end_grouped_rules(); + rule_set::decl2rules::iterator dit = src.begin_grouped_rules(); + rule_set::decl2rules::iterator dend = src.end_grouped_rules(); for (; dit != dend; ++dit) { heads.push_back(dit->m_key); } m_inner_ctx.rel_query(heads.size(), heads.c_ptr()); - - rule_set* dst = alloc(rule_set, m_ctx); + + // retrieve invariants. + dit = src.begin_grouped_rules(); + for (; dit != dend; ++dit) { + func_decl* p = dit->m_key; + relation_base* rb = rctx.try_get_relation(p); + if (rb) { + expr_ref fml(m); + rb->to_formula(fml); + if (m.is_true(fml)) { + continue; + } + expr* inv = 0; + if (m_fun2inv.find(p, inv)) { + fml = m.mk_and(inv, fml); + } + m_pinned.push_back(fml); + m_fun2inv.insert(p, fml); + } + } + } + + rule_set* mk_karr_invariants::update_rules(rule_set const& src) { + scoped_ptr dst = alloc(rule_set, m_ctx); rule_set::iterator it = src.begin(), end = src.end(); for (; it != end; ++it) { - update_body(rctx, *dst, **it); + update_body(*dst, **it); } if (m_ctx.get_model_converter()) { add_invariant_model_converter* kmc = alloc(add_invariant_model_converter, m); @@ -252,10 +274,8 @@ namespace datalog { rule_set::decl2rules::iterator gend = src.end_grouped_rules(); for (; git != gend; ++git) { func_decl* p = git->m_key; - expr_ref fml(m); - relation_base* rb = rctx.try_get_relation(p); - if (rb) { - rb->to_formula(fml); + expr* fml = 0; + if (m_fun2inv.find(p, fml)) { kmc->add(p, fml); } } @@ -263,10 +283,10 @@ namespace datalog { } dst->inherit_predicates(src); - return dst; + return dst.detach(); } - void mk_karr_invariants::update_body(rel_context& rctx, rule_set& rules, rule& r) { + void mk_karr_invariants::update_body(rule_set& rules, rule& r) { unsigned utsz = r.get_uninterpreted_tail_size(); unsigned tsz = r.get_tail_size(); app_ref_vector tail(m); @@ -275,17 +295,17 @@ namespace datalog { tail.push_back(r.get_tail(i)); } for (unsigned i = 0; i < utsz; ++i) { - func_decl* q = r.get_decl(i); - relation_base* rb = rctx.try_get_relation(r.get_decl(i)); - if (rb) { - rb->to_formula(fml); + func_decl* q = r.get_decl(i); + expr* fml = 0; + if (m_fun2inv.find(q, fml)) { expr_safe_replace rep(m); for (unsigned j = 0; j < q->get_arity(); ++j) { rep.insert(m.mk_var(j, q->get_domain(j)), r.get_tail(i)->get_arg(j)); } - rep(fml); - tail.push_back(to_app(fml)); + expr_ref tmp(fml, m); + rep(tmp); + tail.push_back(to_app(tmp)); } } rule* new_rule = &r; @@ -1029,16 +1049,17 @@ namespace datalog { class karr_relation_plugin::filter_equal_fn : public relation_mutator_fn { unsigned m_col; rational m_value; + bool m_valid; public: filter_equal_fn(relation_manager & m, const relation_element & value, unsigned col) : m_col(col) { arith_util arith(m.get_context().get_manager()); - VERIFY(arith.is_numeral(value, m_value)); + m_valid = arith.is_numeral(value, m_value) && m_value.is_int(); } virtual void operator()(relation_base & _r) { karr_relation & r = get(_r); - if (m_value.is_int()) { + if (m_valid) { r.get_ineqs(); vector row; row.resize(r.get_signature().size()); @@ -1054,7 +1075,7 @@ namespace datalog { relation_mutator_fn * karr_relation_plugin::mk_filter_equal_fn(const relation_base & r, const relation_element & value, unsigned col) { - if(check_kind(r)) { + if (check_kind(r)) { return alloc(filter_equal_fn, get_manager(), value, col); } return 0; diff --git a/src/muz_qe/dl_mk_karr_invariants.h b/src/muz_qe/dl_mk_karr_invariants.h index 330260671..ec554e284 100644 --- a/src/muz_qe/dl_mk_karr_invariants.h +++ b/src/muz_qe/dl_mk_karr_invariants.h @@ -55,8 +55,13 @@ namespace datalog { rule_manager& rm; context m_inner_ctx; arith_util a; - void update_body(rel_context& rctx, rule_set& result, rule& r); - rule_set* update_using_propagation(rule_set const& src, rule_set const& srcref); + obj_map m_fun2inv; + ast_ref_vector m_pinned; + + void get_invariants(rule_set const& src); + + void update_body(rule_set& result, rule& r); + rule_set* update_rules(rule_set const& src); public: mk_karr_invariants(context & ctx, unsigned priority); @@ -89,12 +94,7 @@ namespace datalog { {} virtual bool can_handle_signature(const relation_signature & sig) { - for (unsigned i = 0; i < sig.size(); ++i) { - if (a.is_int(sig[i])) { - return true; - } - } - return false; + return true; } static symbol get_name() { return symbol("karr_relation"); } diff --git a/src/muz_qe/dl_product_relation.cpp b/src/muz_qe/dl_product_relation.cpp index 66074d463..c10b5799a 100644 --- a/src/muz_qe/dl_product_relation.cpp +++ b/src/muz_qe/dl_product_relation.cpp @@ -269,7 +269,7 @@ namespace datalog { unsigned_vector r1_tables_indexes; unsigned_vector r2_tables_indexes; for (unsigned i = 0; i < num_rels1; ++i) { - if(is_tableish_relation(*r1[i])) { + if (is_tableish_relation(*r1[i])) { r1_tables_indexes.push_back(i); continue; } @@ -291,7 +291,7 @@ namespace datalog { if (!found) { relation_plugin & r1_plugin = get_nonsieve_plugin(*r1[i]); relation_base* rel2; - if(r1_plugin.can_handle_signature(r2_sig)) { + if (r1_plugin.can_handle_signature(r2_sig)) { rel2 = r1_plugin.mk_full(p, r2_sig, r1_kind); } else { @@ -307,7 +307,7 @@ namespace datalog { } } for (unsigned i = 0; i < num_rels2; ++i) { - if(is_tableish_relation(*r2[i])) { + if (is_tableish_relation(*r2[i])) { r2_tables_indexes.push_back(i); continue; } @@ -315,7 +315,7 @@ namespace datalog { relation_plugin & r2_plugin = get_nonsieve_plugin(*r2[i]); family_id r2_kind = get_nonsieve_kind(*r2[i]); relation_base* rel1; - if(r2_plugin.can_handle_signature(r1_sig)) { + if (r2_plugin.can_handle_signature(r1_sig)) { rel1 = r2_plugin.mk_full(p, r1_sig, r2_kind); } else { @@ -331,7 +331,7 @@ namespace datalog { } } - if(!r1_tables_indexes.empty() && !r2_tables_indexes.empty()) { + if (!r1_tables_indexes.empty() && !r2_tables_indexes.empty()) { //We may perhaps want to group the table relations by kinds so that tables of the same kind //get joined... diff --git a/src/muz_qe/dl_sieve_relation.cpp b/src/muz_qe/dl_sieve_relation.cpp index e80462900..9f9419089 100644 --- a/src/muz_qe/dl_sieve_relation.cpp +++ b/src/muz_qe/dl_sieve_relation.cpp @@ -158,7 +158,7 @@ namespace datalog { inner_sig_singleton.push_back(s[i]); inner_columns[i] = inner.can_handle_signature(inner_sig_singleton); } -#if Z3DEBUG +#if Z3DEBUG //we assume that if a relation plugin can handle two sets of columns separetely, //it can also handle them in one relation relation_signature inner_sig; @@ -246,7 +246,8 @@ namespace datalog { relation_base * sieve_relation_plugin::mk_full(func_decl* p, const relation_signature & s) { relation_signature empty_sig; - relation_base * inner = get_manager().mk_full_relation(empty_sig, p, null_family_id); + relation_plugin& plugin = get_manager().get_appropriate_plugin(s); + relation_base * inner = plugin.mk_full(p, empty_sig, null_family_id); svector inner_cols; inner_cols.resize(s.size(), false); return mk_from_inner(s, inner_cols, inner); diff --git a/src/smt/theory_utvpi.h b/src/smt/theory_utvpi.h index 9e8073ec2..a9dd869a9 100644 --- a/src/smt/theory_utvpi.h +++ b/src/smt/theory_utvpi.h @@ -65,7 +65,7 @@ namespace smt { class parent_trail; struct GExt : public Ext { - typedef literal explanation; + typedef std::pair explanation; }; class atom { @@ -113,15 +113,18 @@ namespace smt { // a negative cycle. class nc_functor { literal_vector m_antecedents; + unsigned_vector m_coeffs; theory_utvpi& m_super; public: nc_functor(theory_utvpi& s) : m_super(s) {} - void reset() { m_antecedents.reset(); } + void reset() { m_antecedents.reset(); m_coeffs.reset(); } literal_vector const& get_lits() const { return m_antecedents; } + unsigned_vector const& get_coeffs() const { return m_coeffs; } - void operator()(literal const & ex) { - if (ex != null_literal) { - m_antecedents.push_back(ex); + void operator()(std::pair const & ex) { + if (ex.first != null_literal) { + m_antecedents.push_back(ex.first); + m_coeffs.push_back(ex.second); } } diff --git a/src/smt/theory_utvpi_def.h b/src/smt/theory_utvpi_def.h index af372ea50..457ac83ad 100644 --- a/src/smt/theory_utvpi_def.h +++ b/src/smt/theory_utvpi_def.h @@ -197,6 +197,15 @@ namespace smt { inc_conflicts(); literal_vector const& lits = m_nc_functor.get_lits(); context & ctx = get_context(); + IF_VERBOSE(2, + verbose_stream() << "conflict:\n"; + for (unsigned i = 0; i < lits.size(); ++i) { + ast_manager& m = get_manager(); + expr_ref e(m); + ctx.literal2expr(lits[i], e); + verbose_stream() << mk_pp(e, m) << "\n"; + } + verbose_stream() << "\n";); TRACE("utvpi", tout << "conflict: "; for (unsigned i = 0; i < lits.size(); ++i) { @@ -213,7 +222,9 @@ namespace smt { vector params; if (get_manager().proofs_enabled()) { params.push_back(parameter(symbol("farkas"))); - params.resize(lits.size()+1, parameter(rational(1))); + for (unsigned i = 0; i < m_nc_functor.get_coeffs().size(); ++i) { + params.push_back(parameter(rational(m_nc_functor.get_coeffs()[i]))); + } } ctx.set_conflict( @@ -620,28 +631,28 @@ namespace smt { edge_id id = m_graph.get_num_edges(); th_var w1 = to_var(v1), w2 = to_var(v2); if (terms.size() == 1 && pos1) { - m_graph.add_edge(neg(w1), pos(w1), -weight-weight, l); - m_graph.add_edge(neg(w1), pos(w1), -weight-weight, l); + m_graph.add_edge(neg(w1), pos(w1), -weight-weight, std::make_pair(l,2)); + m_graph.add_edge(neg(w1), pos(w1), -weight-weight, std::make_pair(l,2)); } else if (terms.size() == 1 && !pos1) { - m_graph.add_edge(pos(w1), neg(w1), -weight-weight, l); - m_graph.add_edge(pos(w1), neg(w1), -weight-weight, l); + m_graph.add_edge(pos(w1), neg(w1), -weight-weight, std::make_pair(l,2)); + m_graph.add_edge(pos(w1), neg(w1), -weight-weight, std::make_pair(l,2)); } else if (pos1 && pos2) { - m_graph.add_edge(neg(w2), pos(w1), -weight, l); - m_graph.add_edge(neg(w1), pos(w2), -weight, l); + m_graph.add_edge(neg(w2), pos(w1), -weight, std::make_pair(l,1)); + m_graph.add_edge(neg(w1), pos(w2), -weight, std::make_pair(l,1)); } else if (pos1 && !pos2) { - m_graph.add_edge(pos(w2), pos(w1), -weight, l); - m_graph.add_edge(neg(w1), neg(w2), -weight, l); + m_graph.add_edge(pos(w2), pos(w1), -weight, std::make_pair(l,1)); + m_graph.add_edge(neg(w1), neg(w2), -weight, std::make_pair(l,1)); } else if (!pos1 && pos2) { - m_graph.add_edge(neg(w2), neg(w1), -weight, l); - m_graph.add_edge(pos(w1), pos(w2), -weight, l); + m_graph.add_edge(neg(w2), neg(w1), -weight, std::make_pair(l,1)); + m_graph.add_edge(pos(w1), pos(w2), -weight, std::make_pair(l,1)); } else { - m_graph.add_edge(pos(w1), neg(w2), -weight, l); - m_graph.add_edge(pos(w2), neg(w1), -weight, l); + m_graph.add_edge(pos(w1), neg(w2), -weight, std::make_pair(l,1)); + m_graph.add_edge(pos(w2), neg(w1), -weight, std::make_pair(l,1)); } return id; } From e35fd58968ec08dd4184e20b639e81a6aa4a9aa6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 13 May 2013 11:43:30 -0700 Subject: [PATCH 05/26] add rewriting option to simplify store equalities Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/array_rewriter.cpp | 38 ++++++++++++++++++++++ src/ast/rewriter/array_rewriter.h | 3 ++ src/ast/rewriter/array_rewriter_params.pyg | 1 + src/ast/rewriter/mk_simplified_app.cpp | 2 ++ src/ast/rewriter/th_rewriter.cpp | 4 ++- 5 files changed, 47 insertions(+), 1 deletion(-) diff --git a/src/ast/rewriter/array_rewriter.cpp b/src/ast/rewriter/array_rewriter.cpp index 0bb7378f4..1f4418fd5 100644 --- a/src/ast/rewriter/array_rewriter.cpp +++ b/src/ast/rewriter/array_rewriter.cpp @@ -25,6 +25,7 @@ void array_rewriter::updt_params(params_ref const & _p) { array_rewriter_params p(_p); m_sort_store = p.sort_store(); m_expand_select_store = p.expand_select_store(); + m_expand_store_eq = p.expand_store_eq(); } void array_rewriter::get_param_descrs(param_descrs & r) { @@ -365,3 +366,40 @@ br_status array_rewriter::mk_set_subset(expr * arg1, expr * arg2, expr_ref & res return BR_REWRITE3; } +br_status array_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) { + if (!m_expand_store_eq) { + return BR_FAILED; + } + expr* lhs1 = lhs; + while (m_util.is_store(lhs1)) { + lhs1 = to_app(lhs1)->get_arg(0); + } + expr* rhs1 = rhs; + while (m_util.is_store(rhs1)) { + rhs1 = to_app(rhs1)->get_arg(0); + } + if (lhs1 != rhs1) { + return BR_FAILED; + } + ptr_buffer fmls, args; + expr* e; + expr_ref tmp1(m()), tmp2(m()); +#define MK_EQ() \ + while (m_util.is_store(e)) { \ + args.push_back(lhs); \ + args.append(to_app(e)->get_num_args()-2,to_app(e)->get_args()+1); \ + mk_select(args.size(), args.c_ptr(), tmp1); \ + args[0] = rhs; \ + mk_select(args.size(), args.c_ptr(), tmp2); \ + fmls.push_back(m().mk_eq(tmp1, tmp2)); \ + e = to_app(e)->get_arg(0); \ + args.reset(); \ + } \ + + e = lhs; + MK_EQ(); + e = rhs; + MK_EQ(); + result = m().mk_and(fmls.size(), fmls.c_ptr()); + return BR_REWRITE_FULL; +} diff --git a/src/ast/rewriter/array_rewriter.h b/src/ast/rewriter/array_rewriter.h index f1362802d..5f20f61ba 100644 --- a/src/ast/rewriter/array_rewriter.h +++ b/src/ast/rewriter/array_rewriter.h @@ -31,12 +31,14 @@ class array_rewriter { array_util m_util; bool m_sort_store; bool m_expand_select_store; + bool m_expand_store_eq; template lbool compare_args(unsigned num_args, expr * const * args1, expr * const * args2); public: array_rewriter(ast_manager & m, params_ref const & p = params_ref()): m_util(m) { updt_params(p); + } ast_manager & m() const { return m_util.get_manager(); } family_id get_fid() const { return m_util.get_family_id(); } @@ -60,6 +62,7 @@ public: br_status mk_set_complement(expr * arg, expr_ref & result); br_status mk_set_difference(expr * arg1, expr * arg2, expr_ref & result); br_status mk_set_subset(expr * arg1, expr * arg2, expr_ref & result); + br_status mk_eq_core(expr * lhs, expr * rhs, expr_ref & result); }; #endif diff --git a/src/ast/rewriter/array_rewriter_params.pyg b/src/ast/rewriter/array_rewriter_params.pyg index 2e3ae9f6a..a43fadecf 100644 --- a/src/ast/rewriter/array_rewriter_params.pyg +++ b/src/ast/rewriter/array_rewriter_params.pyg @@ -2,4 +2,5 @@ def_module_params(module_name='rewriter', class_name='array_rewriter_params', export=True, params=(("expand_select_store", BOOL, False, "replace a (select (store ...) ...) term by an if-then-else term"), + ("expand_store_eq", BOOL, False, "reduce (store ...) = (store ...) with a common base into selects"), ("sort_store", BOOL, False, "sort nested stores when the indices are known to be different"))) diff --git a/src/ast/rewriter/mk_simplified_app.cpp b/src/ast/rewriter/mk_simplified_app.cpp index da615e195..a46e71582 100644 --- a/src/ast/rewriter/mk_simplified_app.cpp +++ b/src/ast/rewriter/mk_simplified_app.cpp @@ -62,6 +62,8 @@ struct mk_simplified_app::imp { st = m_dt_rw.mk_eq_core(args[0], args[1], result); else if (s_fid == m_f_rw.get_fid()) st = m_f_rw.mk_eq_core(args[0], args[1], result); + else if (s_fid == m_ar_rw.get_fid()) + st = m_ar_rw.mk_eq_core(args[0], args[1], result); if (st != BR_FAILED) return st; diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index 966544b78..5d19c53e3 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -169,7 +169,9 @@ struct th_rewriter_cfg : public default_rewriter_cfg { st = m_dt_rw.mk_eq_core(args[0], args[1], result); else if (s_fid == m_f_rw.get_fid()) st = m_f_rw.mk_eq_core(args[0], args[1], result); - + else if (s_fid == m_ar_rw.get_fid()) + st = m_ar_rw.mk_eq_core(args[0], args[1], result); + if (st != BR_FAILED) return st; } From ac6488a19533166798b9cb733748cd844d3ed343 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 13 May 2013 13:21:45 -0700 Subject: [PATCH 06/26] relax pre-processing to untangle non-horn formulas, based on Eldarica/linear benchmarks Signed-off-by: Nikolaj Bjorner --- src/muz_qe/horn_tactic.cpp | 25 +++++++++++++++++++++++-- 1 file changed, 23 insertions(+), 2 deletions(-) diff --git a/src/muz_qe/horn_tactic.cpp b/src/muz_qe/horn_tactic.cpp index 5db4f1a00..9d331cbfa 100644 --- a/src/muz_qe/horn_tactic.cpp +++ b/src/muz_qe/horn_tactic.cpp @@ -124,6 +124,15 @@ class horn_tactic : public tactic { enum formula_kind { IS_RULE, IS_QUERY, IS_NONE }; + bool is_implication(expr* f) { + expr* e1; + while (is_forall(f)) { + f = to_quantifier(f)->get_expr(); + } + while (m.is_implies(f, e1, f)) ; + return is_predicate(f); + } + formula_kind get_formula_kind(expr_ref& f) { expr_ref tmp(f); normalize(tmp); @@ -149,7 +158,10 @@ class horn_tactic : public tactic { } } if (head) { - // f = m.mk_implies(f, head); + if (!is_implication(f)) { + f = m.mk_and(body.size(), body.c_ptr()); + f = m.mk_implies(f, head); + } return IS_RULE; } else { @@ -200,6 +212,7 @@ class horn_tactic : public tactic { break; default: msg << "formula is not in Horn fragment: " << mk_pp(g->form(i), m) << "\n"; + TRACE("horn", tout << msg.str();); throw tactic_exception(msg.str().c_str()); } } @@ -230,7 +243,15 @@ class horn_tactic : public tactic { model_converter_ref & mc, proof_converter_ref & pc) { - lbool is_reachable = m_ctx.query(q); + lbool is_reachable = l_undef; + + try { + is_reachable = m_ctx.query(q); + } + catch (default_exception& ex) { + IF_VERBOSE(1, verbose_stream() << ex.msg() << "\n";); + throw ex; + } g->inc_depth(); bool produce_models = g->models_enabled(); From 7fc93b94f54439fec2dc993415fdb0c6c0c86342 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Tue, 14 May 2013 08:54:04 -0700 Subject: [PATCH 07/26] remove unimplemented method Signed-off-by: Nuno Lopes --- src/tactic/aig/aig.h | 1 - 1 file changed, 1 deletion(-) diff --git a/src/tactic/aig/aig.h b/src/tactic/aig/aig.h index 96aa59ee6..c8befd9b2 100644 --- a/src/tactic/aig/aig.h +++ b/src/tactic/aig/aig.h @@ -70,7 +70,6 @@ public: void max_sharing(aig_ref & r); void to_formula(aig_ref const & r, expr_ref & result); void to_formula(aig_ref const & r, goal & result); - void to_cnf(aig_ref const & r, goal & result); void display(std::ostream & out, aig_ref const & r) const; void display_smt2(std::ostream & out, aig_ref const & r) const; unsigned get_num_aigs() const; From 878d57d139b4be7344dfb2c0678b06efa8bf06ad Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Wed, 15 May 2013 09:23:57 -0700 Subject: [PATCH 08/26] minor code simplification Signed-off-by: Nuno Lopes --- src/tactic/aig/aig.cpp | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/src/tactic/aig/aig.cpp b/src/tactic/aig/aig.cpp index 997ec642e..9fdce96e9 100644 --- a/src/tactic/aig/aig.cpp +++ b/src/tactic/aig/aig.cpp @@ -869,11 +869,7 @@ struct aig_manager::imp { void mk_ite(aig * n) { aig_lit c, t, e; -#ifdef Z3DEBUG - bool ok = -#endif - m.is_ite(n, c, t, e); - SASSERT(ok); + VERIFY(m.is_ite(n, c, t, e)); if (c.is_inverted()) { c.invert(); std::swap(t, e); From e6c814987328f1bc7951f78bf66724f956e19a84 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Wed, 15 May 2013 10:50:46 -0700 Subject: [PATCH 09/26] horn rule bit blaster: fix propagation of output predicates when arity == 0 Signed-off-by: Nuno Lopes --- src/muz_qe/dl_mk_bit_blast.cpp | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) diff --git a/src/muz_qe/dl_mk_bit_blast.cpp b/src/muz_qe/dl_mk_bit_blast.cpp index 51a9d5927..a1eeac6f5 100644 --- a/src/muz_qe/dl_mk_bit_blast.cpp +++ b/src/muz_qe/dl_mk_bit_blast.cpp @@ -141,13 +141,17 @@ namespace datalog { func_decl_ref_vector const& new_funcs() const { return m_new_funcs; } br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { - bool found = false; - for (unsigned j = 0; !found && j < num; ++j) { - found = m_util.is_mkbv(args[j]); - } - if (!found) { + if (num == 0) { + if (m_src->is_output_predicate(f)) + m_dst->set_output_predicate(f); return BR_FAILED; } + + for (unsigned i = 0; i < num; ++i) { + if (!m_util.is_mkbv(args[i])) + return BR_FAILED; + } + // // f(mk_bv(args),...) // @@ -260,7 +264,7 @@ namespace datalog { m_rewriter.m_cfg.set_dst(result); for (unsigned i = 0; !m_context.canceled() && i < sz; ++i) { rule * r = source.get_rule(i); - r->to_formula(fml); + r->to_formula(fml); if (blast(r, fml)) { proof_ref pr(m); if (m_context.generate_proof_trace()) { From 5efdc58194ccc00490772c49ff4ba783fb80d520 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Wed, 15 May 2013 13:17:00 -0700 Subject: [PATCH 10/26] horn clause bit blasting: propagate output predicates for predicates without rules (most likely an UNSAT prog) Signed-off-by: Nuno Lopes --- src/muz_qe/dl_mk_bit_blast.cpp | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/muz_qe/dl_mk_bit_blast.cpp b/src/muz_qe/dl_mk_bit_blast.cpp index a1eeac6f5..136b8ffae 100644 --- a/src/muz_qe/dl_mk_bit_blast.cpp +++ b/src/muz_qe/dl_mk_bit_blast.cpp @@ -279,6 +279,13 @@ namespace datalog { result->add_rule(r); } } + + // copy output predicates without any rule (bit-blasting not really needed) + const func_decl_set& decls = source.get_output_predicates(); + for (func_decl_set::iterator I = decls.begin(), E = decls.end(); I != E; ++I) { + if (!result->contains(*I)) + result->set_output_predicate(*I); + } if (m_context.get_model_converter()) { filter_model_converter* fmc = alloc(filter_model_converter, m); From 100e396618cef0f836304b24a15572d21146c46c Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Wed, 15 May 2013 13:33:42 -0700 Subject: [PATCH 11/26] fix typo in my previous commit Signed-off-by: Nuno Lopes --- src/muz_qe/dl_mk_bit_blast.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/muz_qe/dl_mk_bit_blast.cpp b/src/muz_qe/dl_mk_bit_blast.cpp index 136b8ffae..271003fff 100644 --- a/src/muz_qe/dl_mk_bit_blast.cpp +++ b/src/muz_qe/dl_mk_bit_blast.cpp @@ -283,7 +283,7 @@ namespace datalog { // copy output predicates without any rule (bit-blasting not really needed) const func_decl_set& decls = source.get_output_predicates(); for (func_decl_set::iterator I = decls.begin(), E = decls.end(); I != E; ++I) { - if (!result->contains(*I)) + if (!source.contains(*I)) result->set_output_predicate(*I); } From 6560fc0a2c85d8acb4289fc6d760b71877b36500 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Thu, 16 May 2013 09:58:31 -0700 Subject: [PATCH 12/26] add experimental Horn clause to AIG (AAG format) converter. Clauses should be over booleans only (or bit-blasted with fixedpoint.bit_blast=true). We will crash if that's not the case. Only linear clauses supported for now Signed-off-by: Nuno Lopes --- scripts/mk_project.py | 2 +- src/muz_qe/aig_exporter.cpp | 321 +++++++++++++++++++++++++++++++ src/muz_qe/aig_exporter.h | 66 +++++++ src/muz_qe/fixedpoint_params.pyg | 1 + src/muz_qe/rel_context.cpp | 8 + src/muz_qe/rel_context.h | 3 +- 6 files changed, 398 insertions(+), 3 deletions(-) create mode 100755 src/muz_qe/aig_exporter.cpp create mode 100755 src/muz_qe/aig_exporter.h diff --git a/scripts/mk_project.py b/scripts/mk_project.py index 6ea794040..e6e7d5dc8 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -54,7 +54,7 @@ def init_project_def(): add_lib('smt_tactic', ['smt'], 'smt/tactic') add_lib('sls_tactic', ['tactic', 'normal_forms', 'core_tactics', 'bv_tactics'], 'tactic/sls') # TODO: split muz_qe into muz, qe. Perhaps, we should also consider breaking muz into muz and pdr. - add_lib('muz_qe', ['smt', 'sat', 'smt2parser']) + add_lib('muz_qe', ['smt', 'sat', 'smt2parser', 'aig_tactic']) add_lib('smtlogic_tactics', ['arith_tactics', 'bv_tactics', 'nlsat_tactic', 'smt_tactic', 'aig_tactic', 'muz_qe'], 'tactic/smtlogics') add_lib('ufbv_tactic', ['normal_forms', 'core_tactics', 'macros', 'smt_tactic', 'rewriter'], 'tactic/ufbv') add_lib('portfolio', ['smtlogic_tactics', 'ufbv_tactic', 'fpa', 'aig_tactic', 'muz_qe', 'sls_tactic', 'subpaving_tactic'], 'tactic/portfolio') diff --git a/src/muz_qe/aig_exporter.cpp b/src/muz_qe/aig_exporter.cpp new file mode 100755 index 000000000..1b0dae1ba --- /dev/null +++ b/src/muz_qe/aig_exporter.cpp @@ -0,0 +1,321 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + aig_exporter.cpp + +Abstract: + + Export AIG files from horn clauses + +--*/ + +#include "aig_exporter.h" +#include "dl_context.h" +#include + +namespace datalog { + + aig_exporter::aig_exporter(const rule_set& rules, context& ctx, const fact_vector *facts) : + m_rules(rules), m_facts(facts), m(ctx.get_manager()), m_rm(ctx.get_rule_manager()), + m_aigm(m), m_next_decl_id(1), m_next_aig_expr_id(2), m_num_and_gates(0), + m_latch_vars(m), m_latch_varsp(m), m_ruleid_var_set(m), m_ruleid_varp_set(m) + { + std::set predicates; + unsigned num_variables = 0; + for (rule_set::decl2rules::iterator I = m_rules.begin_grouped_rules(), + E = m_rules.end_grouped_rules(); I != E; ++I) { + predicates.insert(I->m_key); + num_variables = std::max(num_variables, I->m_key->get_arity()); + } + + for (fact_vector::const_iterator I = facts->begin(), E = facts->end(); I != E; ++I) { + predicates.insert(I->first); + num_variables = std::max(num_variables, I->first->get_arity()); + } + + // reserve pred id = 0 for initalization purposes + unsigned num_preds = (unsigned)predicates.size() + 1; + + // poor's man round-up log2 + unsigned preds_bitsize = log2(num_preds); + if ((1U << preds_bitsize) < num_preds) + ++preds_bitsize; + SASSERT((1U << preds_bitsize) >= num_preds); + + for (unsigned i = 0; i < preds_bitsize; ++i) { + m_ruleid_var_set.push_back(m.mk_fresh_const("rule_id", m.mk_bool_sort())); + m_ruleid_varp_set.push_back(m.mk_fresh_const("rule_id_p", m.mk_bool_sort())); + } + + for (unsigned i = 0; i < num_variables; ++i) { + m_latch_vars.push_back(m.mk_fresh_const("latch_var", m.mk_bool_sort())); + m_latch_varsp.push_back(m.mk_fresh_const("latch_varp", m.mk_bool_sort())); + } + } + + void aig_exporter::assert_pred_id(func_decl *decl, const expr_ref_vector& vars, expr_ref_vector& exprs) { + unsigned id = 0; + if (decl && !m_decl_id_map.find(decl, id)) { + id = m_next_decl_id++; + SASSERT(id < (1U << vars.size())); + m_decl_id_map.insert(decl, id); + } + + for (unsigned i = 0; i < vars.size(); ++i) { + exprs.push_back((id & (1U << i)) ? vars[i] : m.mk_not(vars[i])); + } + } + + void aig_exporter::collect_var_substs(substitution& subst, const app *h, + const expr_ref_vector& vars, expr_ref_vector& eqs) { + for (unsigned i = 0; i < h->get_num_args(); ++i) { + expr *arg = h->get_arg(i); + expr *latchvar = vars.get(i); + + if (is_var(arg)) { + var *v = to_var(arg); + expr_offset othervar; + if (subst.find(v, 0, othervar)) { + eqs.push_back(m.mk_eq(latchvar, othervar.get_expr())); + } else { + subst.insert(v, 0, expr_offset(latchvar, 0)); + } + } else { + eqs.push_back(m.mk_eq(latchvar, arg)); + } + } + } + + void aig_exporter::operator()(std::ostream& out) { + expr_ref_vector transition_function(m), output_preds(m); + var_ref_vector input_vars(m); + + rule_counter& vc = m_rm.get_counter(); + expr_ref_vector exprs(m); + substitution subst(m); + + for (rule_set::decl2rules::iterator I = m_rules.begin_grouped_rules(), + E = m_rules.end_grouped_rules(); I != E; ++I) { + for (rule_vector::iterator II = I->get_value()->begin(), + EE = I->get_value()->end(); II != EE; ++II) { + rule *r = *II; + unsigned numqs = r->get_positive_tail_size(); + if (numqs > 1) { + std::cerr << "non-linear clauses not supported\n"; + exit(-1); + } + + if (numqs != r->get_uninterpreted_tail_size()) { + std::cerr << "negation of queries not supported\n"; + exit(-1); + } + + exprs.reset(); + assert_pred_id(numqs ? r->get_tail(0)->get_decl() : 0, m_ruleid_var_set, exprs); + assert_pred_id(r->get_head()->get_decl(), m_ruleid_varp_set, exprs); + + subst.reset(); + subst.reserve(1, vc.get_max_rule_var(*r)+1); + if (numqs) + collect_var_substs(subst, r->get_tail(0), m_latch_vars, exprs); + collect_var_substs(subst, r->get_head(), m_latch_varsp, exprs); + + for (unsigned i = numqs; i < r->get_tail_size(); ++i) { + expr_ref e(m); + subst.apply(r->get_tail(i), e); + exprs.push_back(e); + } + + transition_function.push_back(m.mk_and(exprs.size(), exprs.c_ptr())); + } + } + + // collect table facts + if (m_facts) { + for (fact_vector::const_iterator I = m_facts->begin(), E = m_facts->end(); I != E; ++I) { + exprs.reset(); + assert_pred_id(0, m_ruleid_var_set, exprs); + assert_pred_id(I->first, m_ruleid_varp_set, exprs); + + for (unsigned i = 0; i < I->second.size(); ++i) { + exprs.push_back(m.mk_eq(m_latch_varsp.get(i), I->second[i])); + } + + transition_function.push_back(m.mk_and(exprs.size(), exprs.c_ptr())); + } + } + + expr *tr = m.mk_or(transition_function.size(), transition_function.c_ptr()); + aig_ref aig = m_aigm.mk_aig(tr); + expr_ref aig_expr(m); + m_aigm.to_formula(aig, aig_expr); + +#if 0 + std::cout << mk_pp(tr, m) << "\n\n"; + std::cout << mk_pp(aig_expr, m) << "\n\n"; +#endif + + // make rule_id vars latches + for (unsigned i = 0; i < m_ruleid_var_set.size(); ++i) { + m_latch_vars.push_back(m_ruleid_var_set.get(i)); + m_latch_varsp.push_back(m_ruleid_varp_set.get(i)); + } + + // create vars for latches + for (unsigned i = 0; i < m_latch_vars.size(); ++i) { + mk_var(m_latch_vars.get(i)); + mk_input_var(m_latch_varsp.get(i)); + } + + unsigned tr_id = expr_to_aig(aig_expr); + + // create latch next state variables: (ite tr varp var) + unsigned_vector latch_varp_ids; + for (unsigned i = 0; i < m_latch_vars.size(); ++i) { + unsigned in_val = mk_and(tr_id, get_var(m_latch_varsp.get(i))); + unsigned latch_val = mk_and(neg(tr_id), get_var(m_latch_vars.get(i))); + latch_varp_ids.push_back(mk_or(in_val, latch_val)); + } + m_latch_varsp.reset(); + + // create output variable (true iff an output predicate is derivable) + unsigned output_id = 0; + { + expr_ref_vector output(m); + const func_decl_set& preds = m_rules.get_output_predicates(); + + for (func_decl_set::iterator I = preds.begin(), E = preds.end(); I != E; ++I) { + exprs.reset(); + assert_pred_id(*I, m_ruleid_var_set, exprs); + output.push_back(m.mk_and(exprs.size(), exprs.c_ptr())); + } + + expr *out = m.mk_or(output.size(), output.c_ptr()); + aig = m_aigm.mk_aig(out); + m_aigm.to_formula(aig, aig_expr); + output_id = expr_to_aig(aig_expr); + +#if 0 + std::cout << "output formula\n"; + std::cout << mk_pp(out, m) << "\n\n"; + std::cout << mk_pp(aig_expr, m) << "\n\n"; +#endif + } + + // 1) print header + // aag var_index inputs latches outputs andgates + out << "aag " << (m_next_aig_expr_id-1)/2 << ' ' << m_input_vars.size() + << ' ' << m_latch_vars.size() << " 1 " << m_num_and_gates << '\n'; + + // 2) print inputs + for (unsigned i = 0; i < m_input_vars.size(); ++i) { + out << m_input_vars[i] << '\n'; + } + + // 3) print latches + for (unsigned i = 0; i < m_latch_vars.size(); ++i) { + out << get_var(m_latch_vars.get(i)) << ' ' << latch_varp_ids[i] << '\n'; + } + + // 4) print outputs (just one for now) + out << output_id << '\n'; + + // 5) print formula + out << m_buffer.str(); + } + + unsigned aig_exporter::expr_to_aig(const expr *e) { + unsigned id; + if (m_aig_expr_id_map.find(e, id)) + return id; + + switch (e->get_kind()) { + case AST_APP: { + const app *a = to_app(e); + switch (a->get_decl_kind()) { + case OP_OR: + SASSERT(a->get_num_args() > 0); + id = expr_to_aig(a->get_arg(0)); + for (unsigned i = 1; i < a->get_num_args(); ++i) { + id = mk_or(id, expr_to_aig(a->get_arg(i))); + } + m_aig_expr_id_map.insert(e, id); + return id; + + case null_decl_kind: + return get_var(a); + + case OP_NOT: + return neg(expr_to_aig(a->get_arg(0))); + + case OP_FALSE: + return 0; + + case OP_TRUE: + return 1; + } + break;} + + case AST_VAR: + return get_var(e); + } + + UNREACHABLE(); + return 0; + } + + unsigned aig_exporter::neg(unsigned id) const { + return (id % 2) ? (id-1) : (id+1); + } + + unsigned aig_exporter::mk_and(unsigned id1, unsigned id2) { + if (id1 > id2) + std::swap(id1, id2); + + std::pair key(id1, id2); + and_gates_map::const_iterator I = m_and_gates_map.find(key); + if (I != m_and_gates_map.end()) + return I->second; + + unsigned id = mk_expr_id(); + m_buffer << id << ' ' << id1 << ' ' << id2 << '\n'; + m_and_gates_map[key] = id; + ++m_num_and_gates; + return id; + } + + unsigned aig_exporter::mk_or(unsigned id1, unsigned id2) { + return neg(mk_and(neg(id1), neg(id2))); + } + + unsigned aig_exporter::get_var(const expr *e) { + unsigned id; + if (m_aig_expr_id_map.find(e, id)) + return id; + return mk_input_var(e); + } + + unsigned aig_exporter::mk_var(const expr *e) { + SASSERT(!m_aig_expr_id_map.contains(e)); + unsigned id = mk_expr_id(); + m_aig_expr_id_map.insert(e, id); + return id; + } + + unsigned aig_exporter::mk_input_var(const expr *e) { + SASSERT(!m_aig_expr_id_map.contains(e)); + unsigned id = mk_expr_id(); + m_input_vars.push_back(id); + if (e) + m_aig_expr_id_map.insert(e, id); + return id; + } + + unsigned aig_exporter::mk_expr_id() { + unsigned id = m_next_aig_expr_id; + m_next_aig_expr_id += 2; + return id; + } +} diff --git a/src/muz_qe/aig_exporter.h b/src/muz_qe/aig_exporter.h new file mode 100755 index 000000000..f70945e7f --- /dev/null +++ b/src/muz_qe/aig_exporter.h @@ -0,0 +1,66 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + aig_exporter.h + +Abstract: + + Export AIG files from horn clauses + +--*/ + +#ifndef _AIG_EXPORTER_H_ +#define _AIG_EXPORTER_H_ + +#include "aig.h" +#include "dl_rule_set.h" +#include "rel_context.h" +#include +#include + +namespace datalog { + class aig_exporter { + public: + aig_exporter(const rule_set& rules, context& ctx, const fact_vector *facts = 0); + void operator()(std::ostream& out); + + private: + typedef obj_map decl_id_map; + typedef obj_map aig_expr_id_map; + typedef std::map, unsigned> and_gates_map; + + const rule_set& m_rules; + const fact_vector *m_facts; + ast_manager& m; + rule_manager& m_rm; + aig_manager m_aigm; + decl_id_map m_decl_id_map; + unsigned m_next_decl_id; + aig_expr_id_map m_aig_expr_id_map; + unsigned m_next_aig_expr_id; + and_gates_map m_and_gates_map; + unsigned m_num_and_gates; + + expr_ref_vector m_latch_vars, m_latch_varsp; + expr_ref_vector m_ruleid_var_set, m_ruleid_varp_set; + unsigned_vector m_input_vars; + + std::stringstream m_buffer; + + void assert_pred_id(func_decl *decl, const expr_ref_vector& vars, expr_ref_vector& exprs); + void collect_var_substs(substitution& subst, const app *h, + const expr_ref_vector& vars, expr_ref_vector& eqs); + unsigned expr_to_aig(const expr *e); + unsigned neg(unsigned id) const; + unsigned mk_and(unsigned id1, unsigned id2); + unsigned mk_or(unsigned id1, unsigned id2); + unsigned get_var(const expr *e); + unsigned mk_var(const expr *e); + unsigned mk_input_var(const expr *e = 0); + unsigned mk_expr_id(); + }; +} + +#endif diff --git a/src/muz_qe/fixedpoint_params.pyg b/src/muz_qe/fixedpoint_params.pyg index c516806a6..c2d33cb05 100644 --- a/src/muz_qe/fixedpoint_params.pyg +++ b/src/muz_qe/fixedpoint_params.pyg @@ -62,6 +62,7 @@ def_module_params('fixedpoint', ('print_statistics', BOOL, False, 'print statistics'), ('use_utvpi', BOOL, False, 'experimental use UTVPI strategy'), ('tab_selection', SYMBOL, 'weight', 'selection method for tabular strategy: weight (default), first, var-use'), + ('dump_aig', SYMBOL, '', 'Dump clauses in AIG text format (AAG) to the given file name'), )) diff --git a/src/muz_qe/rel_context.cpp b/src/muz_qe/rel_context.cpp index b42adca79..7ad91ecb6 100644 --- a/src/muz_qe/rel_context.cpp +++ b/src/muz_qe/rel_context.cpp @@ -32,6 +32,7 @@ Revision History: #include"dl_sparse_table.h" #include"dl_table.h" #include"dl_table_relation.h" +#include"aig_exporter.h" namespace datalog { @@ -127,6 +128,13 @@ namespace datalog { } TRACE("dl", m_context.display(tout);); + if (m_context.get_params().dump_aig().size()) { + const char *filename = static_cast(m_context.get_params().dump_aig().c_ptr()); + aig_exporter aig(m_context.get_rules(), get_context(), &m_table_facts); + aig(std::ofstream(filename, std::ios_base::binary)); + exit(0); + } + compiler::compile(m_context, m_context.get_rules(), m_code, termination_code); TRACE("dl", m_code.display(*this, tout); ); diff --git a/src/muz_qe/rel_context.h b/src/muz_qe/rel_context.h index 8e4c6f2de..7b4ee551c 100644 --- a/src/muz_qe/rel_context.h +++ b/src/muz_qe/rel_context.h @@ -28,10 +28,9 @@ Revision History: namespace datalog { class context; + typedef vector > fact_vector; class rel_context { - typedef vector > fact_vector; - context& m_context; ast_manager& m; relation_manager m_rmanager; From 69b7c3ede7ef06e90a8529aac2c29975c3cb9d41 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 16 May 2013 15:36:27 -0700 Subject: [PATCH 13/26] fixing parity bug in model generation for UTVPI Signed-off-by: Nikolaj Bjorner --- src/smt/diff_logic.h | 80 +++++++++++++++++++++++--- src/smt/theory_utvpi.h | 6 +- src/smt/theory_utvpi_def.h | 115 ++++++++++++++++++++++++++++++++----- 3 files changed, 179 insertions(+), 22 deletions(-) diff --git a/src/smt/diff_logic.h b/src/smt/diff_logic.h index 7216bba7e..020268e57 100644 --- a/src/smt/diff_logic.h +++ b/src/smt/diff_logic.h @@ -306,14 +306,6 @@ private: return true; } - // Update the assignment of variable v, that is, - // m_assignment[v] += inc - // This method also stores the old value of v in the assignment stack. - void acc_assignment(dl_var v, const numeral & inc) { - TRACE("diff_logic_bug", tout << "update v: " << v << " += " << inc << " m_assignment[v] " << m_assignment[v] << "\n";); - m_assignment_stack.push_back(assignment_trail(v, m_assignment[v])); - m_assignment[v] += inc; - } // Restore the assignment using the information in m_assignment_stack. // This method is called when make_feasible fails. @@ -827,6 +819,16 @@ public: } } + // Update the assignment of variable v, that is, + // m_assignment[v] += inc + // This method also stores the old value of v in the assignment stack. + void acc_assignment(dl_var v, const numeral & inc) { + TRACE("diff_logic_bug", tout << "update v: " << v << " += " << inc << " m_assignment[v] " << m_assignment[v] << "\n";); + m_assignment_stack.push_back(assignment_trail(v, m_assignment[v])); + m_assignment[v] += inc; + } + + struct every_var_proc { bool operator()(dl_var v) const { return true; @@ -837,6 +839,36 @@ public: display_core(out, every_var_proc()); } + void display_agl(std::ostream & out) const { + uint_set vars; + typename edges::const_iterator it = m_edges.begin(); + typename edges::const_iterator end = m_edges.end(); + for (; it != end; ++it) { + edge const& e = *it; + if (e.is_enabled()) { + vars.insert(e.get_source()); + vars.insert(e.get_target()); + } + } + out << "digraph "" {\n"; + + unsigned n = m_assignment.size(); + for (unsigned v = 0; v < n; v++) { + if (vars.contains(v)) { + out << "\"" << v << "\" [label=\"" << v << ":" << m_assignment[v] << "\"]\n"; + } + } + it = m_edges.begin(); + for (; it != end; ++it) { + edge const& e = *it; + if (e.is_enabled()) { + out << "\"" << e.get_source() << "\"->\"" << e.get_target() << "\"[label=\"" << e.get_weight() << "\"]\n"; + } + } + + out << "}\n"; + } + template void display_core(std::ostream & out, FilterAssignmentProc p) const { display_edges(out); @@ -1000,6 +1032,38 @@ public: } } + void compute_zero_succ(dl_var v, int_vector& succ) { + unsigned n = m_assignment.size(); + m_dfs_time.reset(); + m_dfs_time.resize(n, -1); + m_dfs_time[v] = 0; + succ.push_back(v); + numeral gamma; + for (unsigned i = 0; i < succ.size(); ++i) { + v = succ[i]; + edge_id_vector & edges = m_out_edges[v]; + typename edge_id_vector::iterator it = edges.begin(); + typename edge_id_vector::iterator end = edges.end(); + for (; it != end; ++it) { + edge_id e_id = *it; + edge & e = m_edges[e_id]; + if (!e.is_enabled()) { + continue; + } + SASSERT(e.get_source() == v); + set_gamma(e, gamma); + if (gamma.is_zero()) { + dl_var target = e.get_target(); + if (m_dfs_time[target] == -1) { + succ.push_back(target); + m_dfs_time[target] = 0; + } + } + } + + } + } + numeral get_assignment(dl_var v) const { return m_assignment[v]; } diff --git a/src/smt/theory_utvpi.h b/src/smt/theory_utvpi.h index a9dd869a9..4a5d97d52 100644 --- a/src/smt/theory_utvpi.h +++ b/src/smt/theory_utvpi.h @@ -262,7 +262,11 @@ namespace smt { private: - rational mk_value(theory_var v); + rational mk_value(theory_var v, bool is_int); + + bool is_parity_ok(unsigned v) const; + + void enforce_parity(); void validate_model(); diff --git a/src/smt/theory_utvpi_def.h b/src/smt/theory_utvpi_def.h index 457ac83ad..6c59b568e 100644 --- a/src/smt/theory_utvpi_def.h +++ b/src/smt/theory_utvpi_def.h @@ -397,7 +397,6 @@ namespace smt { template final_check_status theory_utvpi::final_check_eh() { SASSERT(is_consistent()); - TRACE("utvpi", display(tout);); if (can_propagate()) { propagate(); return FC_CONTINUE; @@ -424,7 +423,7 @@ namespace smt { unsigned sz = get_num_vars(); for (unsigned i = 0; i < sz; ++i) { enode* e = get_enode(i); - if (a.is_int(e->get_owner())) { + if (!a.is_int(e->get_owner())) { continue; } th_var v1 = to_var(i); @@ -511,7 +510,7 @@ namespace smt { template theory_var theory_utvpi::mk_term(app* n) { - TRACE("utvpi", tout << mk_pp(n, get_manager()) << "\n";); + TRACE("utvpi", tout << mk_pp(n, get_manager()) << "\n";); context& ctx = get_context(); bool cl = m_test.linearize(n); @@ -519,7 +518,7 @@ namespace smt { found_non_utvpi_expr(n); return null_theory_var; } - + coeffs coeffs; rational w; mk_coeffs(m_test.get_linearization(), coeffs, w); @@ -667,14 +666,80 @@ namespace smt { return m_graph.is_feasible(); } + + template + bool theory_utvpi::is_parity_ok(unsigned i) const { + th_var v1 = to_var(i); + th_var v2 = neg(v1); + rational r1 = m_graph.get_assignment(v1).get_rational(); + rational r2 = m_graph.get_assignment(v2).get_rational(); + return r1.is_even() == r2.is_even(); + } + + + template + void theory_utvpi::enforce_parity() { + unsigned_vector todo; + + unsigned sz = get_num_vars(); + for (unsigned i = 0; i < sz; ++i) { + enode* e = get_enode(i); + if (a.is_int(e->get_owner()) && !is_parity_ok(i)) { + todo.push_back(i); + } + } + if (todo.empty()) { + return; + } + while (!todo.empty()) { + unsigned i = todo.back(); + if (is_parity_ok(i)) { + continue; + } + todo.pop_back(); + th_var v1 = to_var(i); + th_var v2 = neg(v1); + TRACE("utvpi", tout << "disparity: " << v1 << "\n";); + int_vector zero_v; + m_graph.compute_zero_succ(v1, zero_v); + bool found0 = false; + for (unsigned j = 0; !found0 && j < zero_v.size(); ++j) { + found0 = + (to_var(m_zero_int) == zero_v[j]) || + (neg(to_var(m_zero_int)) == zero_v[j]); + } + if (found0) { + zero_v.reset(); + m_graph.compute_zero_succ(v2, zero_v); + } + TRACE("utvpi", + for (unsigned j = 0; j < zero_v.size(); ++j) { + tout << "increment: " << zero_v[j] << "\n"; + }); + + for (unsigned j = 0; j < zero_v.size(); ++j) { + int v = zero_v[j]; + m_graph.acc_assignment(v, numeral(1)); + th_var k = from_var(v); + if (!is_parity_ok(k)) { + TRACE("utvpi", tout << "new disparity: " << k << "\n";); + todo.push_back(k); + } + } + } + } + + // models: template void theory_utvpi::init_model(model_generator & m) { m_factory = alloc(arith_factory, get_manager()); m.register_factory(m_factory); - // TBD: enforce strong or tight coherence? + // TBD: enforce strong or tight coherence + enforce_parity(); compute_delta(); - DEBUG_CODE(validate_model();); + // DEBUG_CODE(validate_model();); + validate_model(); } template @@ -688,7 +753,8 @@ namespace smt { } bool ok = true; expr* e = ctx.bool_var2expr(b); - switch(ctx.get_assignment(b)) { + lbool assign = ctx.get_assignment(b); + switch(assign) { case l_true: ok = eval(e); break; @@ -698,7 +764,23 @@ namespace smt { default: break; } - CTRACE("utvpi", !ok, tout << "validation failed: " << mk_pp(e, get_manager()) << "\n";); + CTRACE("utvpi", !ok, + tout << "validation failed:\n"; + tout << "Assignment: " << assign << "\n"; + m_atoms[i].display(*this, tout); + tout << "\n"; + display(tout); + m_graph.display_agl(tout); + ); + if (!ok) { + std::cout << "validation failed:\n"; + std::cout << "Assignment: " << assign << "\n"; + m_atoms[i].display(*this, std::cout); + std::cout << "\n"; + display(std::cout); + m_graph.display_agl(std::cout); + + } // CTRACE("utvpi", ok, tout << "validation success: " << mk_pp(e, get_manager()) << "\n";); SASSERT(ok); } @@ -751,7 +833,7 @@ namespace smt { return eval_num(e1); } if (is_uninterp_const(e)) { - return mk_value(mk_var(e)); + return mk_value(mk_var(e), a.is_int(e)); } TRACE("utvpi", tout << "expression not handled: " << mk_pp(e, get_manager()) << "\n";); UNREACHABLE(); @@ -760,23 +842,30 @@ namespace smt { template - rational theory_utvpi::mk_value(th_var v) { + rational theory_utvpi::mk_value(th_var v, bool is_int) { SASSERT(v != null_theory_var); numeral val1 = m_graph.get_assignment(to_var(v)); numeral val2 = m_graph.get_assignment(neg(to_var(v))); numeral val = val1 - val2; rational num = val.get_rational() + (m_delta * val.get_infinitesimal().to_rational()); num = num/rational(2); - num = floor(num); + if (is_int && !num.is_int()) { + num = floor(num); + } + TRACE("utvpi", + expr* n = get_enode(v)->get_owner(); + tout << mk_pp(n, get_manager()) << " |-> (" << val1 << " - " << val2 << ")/2 = " << num << "\n";); + return num; } template model_value_proc * theory_utvpi::mk_value(enode * n, model_generator & mg) { theory_var v = n->get_th_var(get_id()); - rational num = mk_value(v); + bool is_int = a.is_int(n->get_owner()); + rational num = mk_value(v, is_int); TRACE("utvpi", tout << mk_pp(n->get_owner(), get_manager()) << " |-> " << num << "\n";); - return alloc(expr_wrapper_proc, m_factory->mk_value(num, a.is_int(n->get_owner()))); + return alloc(expr_wrapper_proc, m_factory->mk_value(num, is_int)); } /** From ef2a9994a92ca23f683862371677fbe7ff7eea76 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 16 May 2013 19:58:14 -0700 Subject: [PATCH 14/26] fix UTVPI model generation Signed-off-by: Nikolaj Bjorner --- src/smt/theory_utvpi_def.h | 48 ++++++++++++++++++++++++++++++-------- 1 file changed, 38 insertions(+), 10 deletions(-) diff --git a/src/smt/theory_utvpi_def.h b/src/smt/theory_utvpi_def.h index 6c59b568e..6c85e40b9 100644 --- a/src/smt/theory_utvpi_def.h +++ b/src/smt/theory_utvpi_def.h @@ -33,7 +33,17 @@ Revision History: 3. Solve for x^+ and x^- 4. Check parity condition for integers (see Lahiri and Musuvathi 05) - 5. extract model for M(x) := (M(x^+)- M(x^-))/2 + This checks if x^+ and x^- are in the same component but of different + parities. + 5. Enforce parity on variables. This checks if x^+ and x^- have different + parities. If they have different parities, the assignment to one + of the variables is decremented (choose the variable that is not tightly + constrained with 0). + The process that adjusts parities converges: Suppose we break a parity + of a different variable y while fixing x's parity. A cyclic breaking/fixing + of parities implies there is a strongly connected component between x, y + and the two polarities of the variables. This contradicts the test in 4. + 6. extract model for M(x) := (M(x^+)- M(x^-))/2 --*/ @@ -677,6 +687,17 @@ namespace smt { } + /** + \brief adjust values for variables in the difference graph + such that for variables of integer sort it is + the case that x^+ - x^- is even. + The informal justification for the procedure enforce_parity is that + the graph does not contain a strongly connected component where + x^+ and x+- are connected. They can be independently changed. + Since we would like variables representing 0 (zero) map to 0, + we selectively update the subgraph that can be updated without + changing the value of zero (which should be 0). + */ template void theory_utvpi::enforce_parity() { unsigned_vector todo; @@ -693,10 +714,10 @@ namespace smt { } while (!todo.empty()) { unsigned i = todo.back(); + todo.pop_back(); if (is_parity_ok(i)) { continue; } - todo.pop_back(); th_var v1 = to_var(i); th_var v2 = neg(v1); TRACE("utvpi", tout << "disparity: " << v1 << "\n";); @@ -708,18 +729,20 @@ namespace smt { (to_var(m_zero_int) == zero_v[j]) || (neg(to_var(m_zero_int)) == zero_v[j]); } + // variables that are tightly connected + // to 0 should not have their values changed. if (found0) { zero_v.reset(); m_graph.compute_zero_succ(v2, zero_v); } TRACE("utvpi", for (unsigned j = 0; j < zero_v.size(); ++j) { - tout << "increment: " << zero_v[j] << "\n"; + tout << "decrement: " << zero_v[j] << "\n"; }); for (unsigned j = 0; j < zero_v.size(); ++j) { int v = zero_v[j]; - m_graph.acc_assignment(v, numeral(1)); + m_graph.acc_assignment(v, numeral(-1)); th_var k = from_var(v); if (!is_parity_ok(k)) { TRACE("utvpi", tout << "new disparity: " << k << "\n";); @@ -727,6 +750,15 @@ namespace smt { } } } + SASSERT(m_graph.is_feasible()); + DEBUG_CODE( + for (unsigned i = 0; i < sz; ++i) { + enode* e = get_enode(i); + if (a.is_int(e->get_owner()) && !is_parity_ok(i)) { + IF_VERBOSE(0, verbose_stream() << "disparities not fixed\n";); + UNREACHABLE(); + } + }); } @@ -735,11 +767,9 @@ namespace smt { void theory_utvpi::init_model(model_generator & m) { m_factory = alloc(arith_factory, get_manager()); m.register_factory(m_factory); - // TBD: enforce strong or tight coherence enforce_parity(); compute_delta(); - // DEBUG_CODE(validate_model();); - validate_model(); + DEBUG_CODE(validate_model();); } template @@ -849,9 +879,7 @@ namespace smt { numeral val = val1 - val2; rational num = val.get_rational() + (m_delta * val.get_infinitesimal().to_rational()); num = num/rational(2); - if (is_int && !num.is_int()) { - num = floor(num); - } + SASSERT(!is_int || num.is_int()); TRACE("utvpi", expr* n = get_enode(v)->get_owner(); tout << mk_pp(n, get_manager()) << " |-> (" << val1 << " - " << val2 << ")/2 = " << num << "\n";); From 5d1339beec902151e801dba46cac633d201c2d8d Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 17 May 2013 13:43:32 +0100 Subject: [PATCH 15/26] .NET/Java: API doc update for Context constructor. Signed-off-by: Christoph M. Wintersteiger --- src/api/dotnet/Context.cs | 15 +++++++++++++++ src/api/java/Context.java | 15 +++++++++++++++ 2 files changed, 30 insertions(+) diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index 35fe6611d..68cca046e 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -44,6 +44,21 @@ namespace Microsoft.Z3 /// /// Constructor. /// + /// + /// The following parameters can be set: + /// - proof (Boolean) Enable proof generation + /// - debug_ref_count (Boolean) Enable debug support for Z3_ast reference counting + /// - trace (Boolean) Tracing support for VCC + /// - trace_file_name (String) Trace out file for VCC traces + /// - timeout (unsigned) default timeout (in milliseconds) used for solvers + /// - well_sorted_check type checker + /// - auto_config use heuristics to automatically select solver and configure it + /// - model model generation for solvers, this parameter can be overwritten when creating a solver + /// - model_validate validate models produced by solvers + /// - unsat_core unsat-core generation for solvers, this parameter can be overwritten when creating a solver + /// Note that in previous versions of Z3, this constructor was also used to set global and module parameters. + /// For this purpose we should now use + /// public Context(Dictionary settings) : base() { diff --git a/src/api/java/Context.java b/src/api/java/Context.java index 5277dab38..6b6c63ac3 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -27,6 +27,21 @@ public class Context extends IDisposable /** * Constructor. + * + * The following parameters can be set: + * - proof (Boolean) Enable proof generation + * - debug_ref_count (Boolean) Enable debug support for Z3_ast reference counting + * - trace (Boolean) Tracing support for VCC + * - trace_file_name (String) Trace out file for VCC traces + * - timeout (unsigned) default timeout (in milliseconds) used for solvers + * - well_sorted_check type checker + * - auto_config use heuristics to automatically select solver and configure it + * - model model generation for solvers, this parameter can be overwritten when creating a solver + * - model_validate validate models produced by solvers + * - unsat_core unsat-core generation for solvers, this parameter can be overwritten when creating a solver + * Note that in previous versions of Z3, this constructor was also used to set global and + * module parameters. For this purpose we should now use + * **/ public Context(Map settings) throws Z3Exception { From d1999b3424e6ad16a00867549db4ad1eb16b6000 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Fri, 17 May 2013 09:46:30 -0700 Subject: [PATCH 16/26] AIG exporter: create latches lazily properly check for constants Signed-off-by: Nuno Lopes --- src/muz_qe/aig_exporter.cpp | 23 ++++++++++++++--------- src/muz_qe/aig_exporter.h | 2 ++ 2 files changed, 16 insertions(+), 9 deletions(-) diff --git a/src/muz_qe/aig_exporter.cpp b/src/muz_qe/aig_exporter.cpp index 1b0dae1ba..c82ff7245 100755 --- a/src/muz_qe/aig_exporter.cpp +++ b/src/muz_qe/aig_exporter.cpp @@ -23,16 +23,13 @@ namespace datalog { m_latch_vars(m), m_latch_varsp(m), m_ruleid_var_set(m), m_ruleid_varp_set(m) { std::set predicates; - unsigned num_variables = 0; for (rule_set::decl2rules::iterator I = m_rules.begin_grouped_rules(), E = m_rules.end_grouped_rules(); I != E; ++I) { predicates.insert(I->m_key); - num_variables = std::max(num_variables, I->m_key->get_arity()); } for (fact_vector::const_iterator I = facts->begin(), E = facts->end(); I != E; ++I) { predicates.insert(I->first); - num_variables = std::max(num_variables, I->first->get_arity()); } // reserve pred id = 0 for initalization purposes @@ -48,11 +45,19 @@ namespace datalog { m_ruleid_var_set.push_back(m.mk_fresh_const("rule_id", m.mk_bool_sort())); m_ruleid_varp_set.push_back(m.mk_fresh_const("rule_id_p", m.mk_bool_sort())); } + } - for (unsigned i = 0; i < num_variables; ++i) { + void aig_exporter::mk_latch_vars(unsigned n) { + for (int i = m_latch_vars.size() - 1; i <= (int)n; ++i) { m_latch_vars.push_back(m.mk_fresh_const("latch_var", m.mk_bool_sort())); m_latch_varsp.push_back(m.mk_fresh_const("latch_varp", m.mk_bool_sort())); } + SASSERT(m_latch_vars.size() > n); + } + + expr* aig_exporter::get_latch_var(unsigned i, const expr_ref_vector& vars) { + mk_latch_vars(i); + return vars.get(i); } void aig_exporter::assert_pred_id(func_decl *decl, const expr_ref_vector& vars, expr_ref_vector& exprs) { @@ -72,7 +77,7 @@ namespace datalog { const expr_ref_vector& vars, expr_ref_vector& eqs) { for (unsigned i = 0; i < h->get_num_args(); ++i) { expr *arg = h->get_arg(i); - expr *latchvar = vars.get(i); + expr *latchvar = get_latch_var(i, vars); if (is_var(arg)) { var *v = to_var(arg); @@ -140,7 +145,7 @@ namespace datalog { assert_pred_id(I->first, m_ruleid_varp_set, exprs); for (unsigned i = 0; i < I->second.size(); ++i) { - exprs.push_back(m.mk_eq(m_latch_varsp.get(i), I->second[i])); + exprs.push_back(m.mk_eq(get_latch_var(i, m_latch_varsp), I->second[i])); } transition_function.push_back(m.mk_and(exprs.size(), exprs.c_ptr())); @@ -231,6 +236,9 @@ namespace datalog { if (m_aig_expr_id_map.find(e, id)) return id; + if (is_uninterp_const(e)) + return get_var(e); + switch (e->get_kind()) { case AST_APP: { const app *a = to_app(e); @@ -244,9 +252,6 @@ namespace datalog { m_aig_expr_id_map.insert(e, id); return id; - case null_decl_kind: - return get_var(a); - case OP_NOT: return neg(expr_to_aig(a->get_arg(0))); diff --git a/src/muz_qe/aig_exporter.h b/src/muz_qe/aig_exporter.h index f70945e7f..20b31f01b 100755 --- a/src/muz_qe/aig_exporter.h +++ b/src/muz_qe/aig_exporter.h @@ -49,6 +49,8 @@ namespace datalog { std::stringstream m_buffer; + void mk_latch_vars(unsigned n); + expr* get_latch_var(unsigned i, const expr_ref_vector& vars); void assert_pred_id(func_decl *decl, const expr_ref_vector& vars, expr_ref_vector& exprs); void collect_var_substs(substitution& subst, const app *h, const expr_ref_vector& vars, expr_ref_vector& eqs); From aea667d09bdac18dc244bc03a4f1b2301f5a34a8 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Fri, 17 May 2013 12:17:35 -0700 Subject: [PATCH 17/26] fix a one-too-many in my previous commit Signed-off-by: Nuno Lopes --- src/muz_qe/aig_exporter.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/muz_qe/aig_exporter.cpp b/src/muz_qe/aig_exporter.cpp index c82ff7245..1d6ef3633 100755 --- a/src/muz_qe/aig_exporter.cpp +++ b/src/muz_qe/aig_exporter.cpp @@ -48,7 +48,7 @@ namespace datalog { } void aig_exporter::mk_latch_vars(unsigned n) { - for (int i = m_latch_vars.size() - 1; i <= (int)n; ++i) { + for (unsigned i = m_latch_vars.size(); i <= n; ++i) { m_latch_vars.push_back(m.mk_fresh_const("latch_var", m.mk_bool_sort())); m_latch_varsp.push_back(m.mk_fresh_const("latch_varp", m.mk_bool_sort())); } From 56dedec740b3f7bf4c4ab35fa5758afc109a8e87 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 18 May 2013 10:02:53 -0700 Subject: [PATCH 18/26] fix build break include uint_set.h Signed-off-by: Nikolaj Bjorner --- src/smt/diff_logic.h | 1 + 1 file changed, 1 insertion(+) diff --git a/src/smt/diff_logic.h b/src/smt/diff_logic.h index 020268e57..6fd156e41 100644 --- a/src/smt/diff_logic.h +++ b/src/smt/diff_logic.h @@ -24,6 +24,7 @@ Revision History: #include"statistics.h" #include"trace.h" #include"warning.h" +#include"uint_set.h" typedef int dl_var; From dc91a754dd405b3348dd13f61a72207852869e9a Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Tue, 21 May 2013 10:48:55 -0700 Subject: [PATCH 19/26] improve clp solver - run default rule transformations - sort a predicate's rules by number of queries in the body to bias search Signed-off-by: Nuno Lopes --- src/muz_qe/clp_context.cpp | 16 ++++++++++++---- 1 file changed, 12 insertions(+), 4 deletions(-) diff --git a/src/muz_qe/clp_context.cpp b/src/muz_qe/clp_context.cpp index 25ea1455b..5dd6fb9d8 100644 --- a/src/muz_qe/clp_context.cpp +++ b/src/muz_qe/clp_context.cpp @@ -66,9 +66,10 @@ namespace datalog { m_ctx.ensure_opened(); m_solver.reset(); m_goals.reset(); - rm.mk_query(query, m_ctx.get_rules()); - expr_ref head(m); - head = m_ctx.get_rules().last()->get_head(); + func_decl *head_decl = rm.mk_query(query, m_ctx.get_rules()); + m_ctx.apply_default_transformation(); + + expr_ref head(m_ctx.get_rules().get_predicate_rules(head_decl)[0]->get_head(), m); ground(head); m_goals.push_back(to_app(head)); return search(20, 0); @@ -125,6 +126,10 @@ namespace datalog { m_var_subst(e, m_ground.size(), m_ground.c_ptr(), e); } + static bool rule_sort_fn(const rule *r1, const rule *r2) { + return r1->get_uninterpreted_tail_size() < r2->get_uninterpreted_tail_size(); + } + lbool search(unsigned depth, unsigned index) { if (index == m_goals.size()) { return l_true; @@ -135,7 +140,10 @@ namespace datalog { IF_VERBOSE(1, verbose_stream() << "search " << depth << " " << index << "\n";); unsigned num_goals = m_goals.size(); app* head = m_goals[index].get(); - rule_vector const& rules = m_ctx.get_rules().get_predicate_rules(head->get_decl()); + + rule_vector rules(m_ctx.get_rules().get_predicate_rules(head->get_decl())); + std::stable_sort(rules.begin(), rules.end(), rule_sort_fn); + lbool status = l_false; for (unsigned i = 0; i < rules.size(); ++i) { rule* r = rules[i]; From 09945dc2cb753ea80951c2f084ec65f9e3528c3e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 23 May 2013 08:07:19 -0700 Subject: [PATCH 20/26] Fix compilation error with gcc Signed-off-by: Leonardo de Moura --- src/muz_qe/rel_context.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/muz_qe/rel_context.cpp b/src/muz_qe/rel_context.cpp index 7ad91ecb6..63e8ba700 100644 --- a/src/muz_qe/rel_context.cpp +++ b/src/muz_qe/rel_context.cpp @@ -131,7 +131,8 @@ namespace datalog { if (m_context.get_params().dump_aig().size()) { const char *filename = static_cast(m_context.get_params().dump_aig().c_ptr()); aig_exporter aig(m_context.get_rules(), get_context(), &m_table_facts); - aig(std::ofstream(filename, std::ios_base::binary)); + std::ofstream strm(filename, std::ios_base::binary); + aig(strm); exit(0); } From ccf10d0abe86c86c66bc5e7908d3f5deda042d10 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 25 May 2013 14:38:02 -0700 Subject: [PATCH 21/26] fix crash in PDR engine when transformations don't produce output predicates Signed-off-by: Nikolaj Bjorner --- src/muz_qe/dl_mk_slice.cpp | 6 ++++++ src/muz_qe/pdr_dl_interface.cpp | 6 ++++++ 2 files changed, 12 insertions(+) diff --git a/src/muz_qe/dl_mk_slice.cpp b/src/muz_qe/dl_mk_slice.cpp index 1a97c1b81..5b9d43acc 100644 --- a/src/muz_qe/dl_mk_slice.cpp +++ b/src/muz_qe/dl_mk_slice.cpp @@ -710,6 +710,7 @@ namespace datalog { void mk_slice::declare_predicates(rule_set const& src, rule_set& dst) { obj_map::iterator it = m_sliceable.begin(), end = m_sliceable.end(); ptr_vector domain; + bool has_output = false; func_decl* f; for (; it != end; ++it) { domain.reset(); @@ -731,8 +732,13 @@ namespace datalog { } else if (src.is_output_predicate(p)) { dst.set_output_predicate(p); + has_output = true; } } + // disable slicing if the output predicates don't occur in rules. + if (!has_output) { + m_predicates.reset(); + } } bool mk_slice::rule_updated(rule const& r) { diff --git a/src/muz_qe/pdr_dl_interface.cpp b/src/muz_qe/pdr_dl_interface.cpp index 3ff54e68e..437c08f6a 100644 --- a/src/muz_qe/pdr_dl_interface.cpp +++ b/src/muz_qe/pdr_dl_interface.cpp @@ -133,6 +133,12 @@ lbool dl_interface::query(expr * query) { --num_unfolds; } } + + if (m_ctx.get_rules().get_output_predicates().empty()) { + m_context->set_unsat(); + return l_false; + } + query_pred = m_ctx.get_rules().get_output_predicate(); IF_VERBOSE(2, m_ctx.display_rules(verbose_stream());); From 7c12ab47165a88ab514c8cddcf65b1be6e784ec8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 25 May 2013 14:40:57 -0700 Subject: [PATCH 22/26] fix some compiler warnings Signed-off-by: Nikolaj Bjorner --- src/muz_qe/aig_exporter.cpp | 2 ++ src/muz_qe/clp_context.cpp | 3 ++- 2 files changed, 4 insertions(+), 1 deletion(-) diff --git a/src/muz_qe/aig_exporter.cpp b/src/muz_qe/aig_exporter.cpp index 1d6ef3633..ca0030fc3 100755 --- a/src/muz_qe/aig_exporter.cpp +++ b/src/muz_qe/aig_exporter.cpp @@ -265,6 +265,8 @@ namespace datalog { case AST_VAR: return get_var(e); + default: + UNREACHABLE(); } UNREACHABLE(); diff --git a/src/muz_qe/clp_context.cpp b/src/muz_qe/clp_context.cpp index 5dd6fb9d8..94a956eb9 100644 --- a/src/muz_qe/clp_context.cpp +++ b/src/muz_qe/clp_context.cpp @@ -66,8 +66,9 @@ namespace datalog { m_ctx.ensure_opened(); m_solver.reset(); m_goals.reset(); - func_decl *head_decl = rm.mk_query(query, m_ctx.get_rules()); + rm.mk_query(query, m_ctx.get_rules()); m_ctx.apply_default_transformation(); + func_decl *head_decl = m_ctx.get_rules().get_output_predicate(); expr_ref head(m_ctx.get_rules().get_predicate_rules(head_decl)[0]->get_head(), m); ground(head); From edb2f8554d7418b8a202db374d810a66a18774eb Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 27 May 2013 17:45:56 -0700 Subject: [PATCH 23/26] Add new example Signed-off-by: Leonardo de Moura --- examples/c++/example.cpp | 27 ++++++++++++++++++++++++--- 1 file changed, 24 insertions(+), 3 deletions(-) diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp index 55dbebe27..77f7702f2 100644 --- a/examples/c++/example.cpp +++ b/examples/c++/example.cpp @@ -952,6 +952,26 @@ void exists_expr_vector_example() { std::cout << ex << std::endl; } +void substitute_example() { + std::cout << "substitute example\n"; + context c; + expr x(c); + x = c.int_const("x"); + expr f(c); + f = (x == 2) || (x == 1); + std::cout << f << std::endl; + + expr two(c), three(c); + two = c.int_val(2); + three = c.int_val(3); + Z3_ast from[] = { two }; + Z3_ast to[] = { three }; + expr new_f(c); + new_f = to_expr(c, Z3_substitute(c, f, 1, from, to)); + + std::cout << new_f << std::endl; +} + int main() { try { demorgan(); std::cout << "\n"; @@ -983,12 +1003,13 @@ int main() { tactic_example9(); std::cout << "\n"; tactic_qe(); std::cout << "\n"; tst_visit(); std::cout << "\n"; - incremental_example1(); std::cout << "\n"; - incremental_example2(); std::cout << "\n"; - incremental_example3(); std::cout << "\n"; + incremental_example1(); std::cout << "\n"; + incremental_example2(); std::cout << "\n"; + incremental_example3(); std::cout << "\n"; enum_sort_example(); std::cout << "\n"; expr_vector_example(); std::cout << "\n"; exists_expr_vector_example(); std::cout << "\n"; + substitute_example(); std::cout << "\n"; std::cout << "done\n"; } catch (exception & ex) { From c6f4cdab0f0b47759c5e686462fd09449de90a0d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 27 May 2013 17:49:03 -0700 Subject: [PATCH 24/26] Fix bug reported at https://z3.codeplex.com/workitem/41 Signed-off-by: Leonardo de Moura --- src/ast/pattern/database.smt2 | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/ast/pattern/database.smt2 b/src/ast/pattern/database.smt2 index 9021e44f0..c42c9c25f 100644 --- a/src/ast/pattern/database.smt2 +++ b/src/ast/pattern/database.smt2 @@ -119,13 +119,13 @@ :pattern (?select (?select (?asElems e) a) i)))) (assert (forall ((x Int) (f Int) (a0 Int)) (! - (or (<= (+ a0 (* -1 (?fClosedTime f))) 0) + (or (<= (+ a0 (* (- 1) (?fClosedTime f))) 0) (not (= (?isAllocated x a0) 1)) (= (?isAllocated (?select f x) a0) 1)) :pattern (?isAllocated (?select f x) a0)))) (assert (forall ((a Int) (e Int) (i Int) (a0 Int)) (! - (or (<= (+ a0 (* -1 (?eClosedTime e))) 0) + (or (<= (+ a0 (* (- 1) (?eClosedTime e))) 0) (not (= (?isAllocated a a0) 1)) (= (?isAllocated (?select (?select e a) i) a0) 1)) :pattern (?isAllocated (?select (?select e a) i) a0)))) @@ -281,13 +281,13 @@ :pattern (IntsAllocated h (?StructGet_ s f))))) (assert (forall ((x Int) (f Int) (a0 Int)) (! - (or (<= (+ a0 (* -1 (?fClosedTime f))) 0) + (or (<= (+ a0 (* (- 1) (?fClosedTime f))) 0) (not (?isAllocated_ x a0)) (?isAllocated_ (?select f x) a0)) :pattern (?isAllocated_ (?select f x) a0)))) (assert (forall ((a Int) (e Int) (i Int) (a0 Int)) (! - (or (<= (+ a0 (* -1 (?eClosedTime e))) 0) + (or (<= (+ a0 (* (- 1) (?eClosedTime e))) 0) (not (?isAllocated_ a a0)) (?isAllocated_ (?select (?select e a) i) a0)) :pattern (?isAllocated_ (?select (?select e a) i) a0)))) From 9a666966398c997bfa0d0b17e5fa0d5e24a84e4d Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Wed, 29 May 2013 14:35:32 -0700 Subject: [PATCH 25/26] merge hassel table code from branch Signed-off-by: Nuno Lopes --- src/muz_qe/dl_base.h | 14 +- src/muz_qe/dl_check_table.cpp | 81 +- src/muz_qe/dl_check_table.h | 10 + src/muz_qe/dl_compiler.cpp | 125 +++- src/muz_qe/dl_compiler.h | 2 + src/muz_qe/dl_hassel_common.cpp | 434 +++++++++++ src/muz_qe/dl_hassel_common.h | 1079 +++++++++++++++++++++++++++ src/muz_qe/dl_hassel_diff_table.cpp | 219 ++++++ src/muz_qe/dl_hassel_diff_table.h | 87 +++ src/muz_qe/dl_hassel_table.cpp | 27 + src/muz_qe/dl_hassel_table.h | 39 + src/muz_qe/dl_instruction.cpp | 59 ++ src/muz_qe/dl_instruction.h | 2 + src/muz_qe/dl_relation_manager.cpp | 46 ++ src/muz_qe/dl_relation_manager.h | 7 + src/muz_qe/dl_table_relation.cpp | 15 + src/muz_qe/dl_table_relation.h | 2 + src/muz_qe/rel_context.cpp | 11 + src/util/bit_vector.h | 7 + 19 files changed, 2259 insertions(+), 7 deletions(-) create mode 100755 src/muz_qe/dl_hassel_common.cpp create mode 100755 src/muz_qe/dl_hassel_common.h create mode 100755 src/muz_qe/dl_hassel_diff_table.cpp create mode 100755 src/muz_qe/dl_hassel_diff_table.h create mode 100644 src/muz_qe/dl_hassel_table.cpp create mode 100644 src/muz_qe/dl_hassel_table.h diff --git a/src/muz_qe/dl_base.h b/src/muz_qe/dl_base.h index 491bb261d..200ce2d83 100644 --- a/src/muz_qe/dl_base.h +++ b/src/muz_qe/dl_base.h @@ -331,6 +331,10 @@ namespace datalog { virtual mutator_fn * mk_filter_interpreted_fn(const base_object & t, app * condition) { return 0; } + virtual transformer_fn * mk_filter_interpreted_and_project_fn(const base_object & t, + app * condition, unsigned removed_col_cnt, const unsigned * removed_cols) + { return 0; } + virtual transformer_fn * mk_select_equal_and_project_fn(const base_object & t, const element & value, unsigned col) { return 0; } @@ -454,8 +458,8 @@ namespace datalog { class convenient_join_fn : public join_fn { signature m_result_sig; protected: - const unsigned_vector m_cols1; - const unsigned_vector m_cols2; + unsigned_vector m_cols1; + unsigned_vector m_cols2; convenient_join_fn(const signature & o1_sig, const signature & o2_sig, unsigned col_cnt, const unsigned * cols1, const unsigned * cols2) @@ -470,8 +474,8 @@ namespace datalog { class convenient_join_project_fn : public join_fn { signature m_result_sig; protected: - const unsigned_vector m_cols1; - const unsigned_vector m_cols2; + unsigned_vector m_cols1; + unsigned_vector m_cols2; //it is non-const because it needs to be modified in sparse_table version of the join_project operator unsigned_vector m_removed_cols; @@ -498,7 +502,7 @@ namespace datalog { class convenient_project_fn : public convenient_transformer_fn { protected: - const unsigned_vector m_removed_cols; + unsigned_vector m_removed_cols; convenient_project_fn(const signature & orig_sig, unsigned col_cnt, const unsigned * removed_cols) : m_removed_cols(col_cnt, removed_cols) { diff --git a/src/muz_qe/dl_check_table.cpp b/src/muz_qe/dl_check_table.cpp index 5081654b5..ea4003e5f 100644 --- a/src/muz_qe/dl_check_table.cpp +++ b/src/muz_qe/dl_check_table.cpp @@ -82,6 +82,34 @@ namespace datalog { return alloc(join_fn, *this, t1, t2, col_cnt, cols1, cols2); } + class check_table_plugin::join_project_fn : public table_join_fn { + scoped_ptr m_tocheck; + scoped_ptr m_checker; + public: + join_project_fn(check_table_plugin& p, const table_base & t1, const table_base & t2, + unsigned col_cnt, const unsigned * cols1, const unsigned * cols2, + unsigned removed_col_cnt, const unsigned * removed_cols) { + m_tocheck = p.get_manager().mk_join_project_fn(tocheck(t1), tocheck(t2), col_cnt, cols1, cols2, removed_col_cnt, removed_cols); + m_checker = p.get_manager().mk_join_project_fn(checker(t1), checker(t2), col_cnt, cols1, cols2, removed_col_cnt, removed_cols); + } + + virtual table_base* operator()(const table_base & t1, const table_base & t2) { + table_base* ttocheck = (*m_tocheck)(tocheck(t1), tocheck(t2)); + table_base* tchecker = (*m_checker)(checker(t1), checker(t2)); + check_table* result = alloc(check_table, get(t1).get_plugin(), ttocheck->get_signature(), ttocheck, tchecker); + return result; + } + }; + + table_join_fn * check_table_plugin::mk_join_project_fn(const table_base & t1, const table_base & t2, + unsigned col_cnt, const unsigned * cols1, const unsigned * cols2, unsigned removed_col_cnt, + const unsigned * removed_cols) { + if (!check_kind(t1) || !check_kind(t2)) { + return 0; + } + return alloc(join_project_fn, *this, t1, t2, col_cnt, cols1, cols2, removed_col_cnt, removed_cols); + } + class check_table_plugin::union_fn : public table_union_fn { scoped_ptr m_tocheck; scoped_ptr m_checker; @@ -120,7 +148,6 @@ namespace datalog { } table_base* operator()(table_base const& src) { - IF_VERBOSE(1, verbose_stream() << __FUNCTION__ << "\n";); table_base* tchecker = (*m_checker)(checker(src)); table_base* ttocheck = (*m_tocheck)(tocheck(src)); check_table* result = alloc(check_table, get(src).get_plugin(), tchecker->get_signature(), ttocheck, tchecker); @@ -135,6 +162,31 @@ namespace datalog { return alloc(project_fn, *this, t, col_cnt, removed_cols); } + class check_table_plugin::select_equal_and_project_fn : public table_transformer_fn { + scoped_ptr m_checker; + scoped_ptr m_tocheck; + public: + select_equal_and_project_fn(check_table_plugin& p, const table_base & t, const table_element & value, unsigned col) { + m_checker = p.get_manager().mk_select_equal_and_project_fn(checker(t), value, col); + m_tocheck = p.get_manager().mk_select_equal_and_project_fn(tocheck(t), value, col); + } + + table_base* operator()(table_base const& src) { + table_base* tchecker = (*m_checker)(checker(src)); + table_base* ttocheck = (*m_tocheck)(tocheck(src)); + check_table* result = alloc(check_table, get(src).get_plugin(), tchecker->get_signature(), ttocheck, tchecker); + return result; + } + }; + + table_transformer_fn * check_table_plugin::mk_select_equal_and_project_fn(const table_base & t, + const table_element & value, unsigned col) { + if (!check_kind(t)) { + return 0; + } + return alloc(select_equal_and_project_fn, *this, t, value, col); + } + class check_table_plugin::rename_fn : public table_transformer_fn { scoped_ptr m_checker; scoped_ptr m_tocheck; @@ -233,6 +285,33 @@ namespace datalog { return 0; } + class check_table_plugin::filter_interpreted_and_project_fn : public table_transformer_fn { + scoped_ptr m_checker; + scoped_ptr m_tocheck; + public: + filter_interpreted_and_project_fn(check_table_plugin& p, const table_base & t, app * condition, + unsigned removed_col_cnt, const unsigned * removed_cols) + { + m_checker = p.get_manager().mk_filter_interpreted_and_project_fn(checker(t), condition, removed_col_cnt, removed_cols); + m_tocheck = p.get_manager().mk_filter_interpreted_and_project_fn(tocheck(t), condition, removed_col_cnt, removed_cols); + } + + table_base* operator()(table_base const& src) { + table_base* tchecker = (*m_checker)(checker(src)); + table_base* ttocheck = (*m_tocheck)(tocheck(src)); + check_table* result = alloc(check_table, get(src).get_plugin(), ttocheck->get_signature(), ttocheck, tchecker); + return result; + } + }; + + table_transformer_fn * check_table_plugin::mk_filter_interpreted_and_project_fn(const table_base & t, + app * condition, unsigned removed_col_cnt, const unsigned * removed_cols) { + if (check_kind(t)) { + return alloc(filter_interpreted_and_project_fn, *this, t, condition, removed_col_cnt, removed_cols); + } + return 0; + } + class check_table_plugin::filter_by_negation_fn : public table_intersection_filter_fn { scoped_ptr m_checker; scoped_ptr m_tocheck; diff --git a/src/muz_qe/dl_check_table.h b/src/muz_qe/dl_check_table.h index 40a3d5207..e4f439590 100644 --- a/src/muz_qe/dl_check_table.h +++ b/src/muz_qe/dl_check_table.h @@ -35,13 +35,16 @@ namespace datalog { unsigned m_count; protected: class join_fn; + class join_project_fn; class union_fn; class transformer_fn; class rename_fn; class project_fn; + class select_equal_and_project_fn; class filter_equal_fn; class filter_identical_fn; class filter_interpreted_fn; + class filter_interpreted_and_project_fn; class filter_by_negation_fn; public: @@ -54,10 +57,15 @@ namespace datalog { virtual table_join_fn * mk_join_fn(const table_base & t1, const table_base & t2, unsigned col_cnt, const unsigned * cols1, const unsigned * cols2); + virtual table_join_fn * mk_join_project_fn(const table_base & t1, const table_base & t2, + unsigned col_cnt, const unsigned * cols1, const unsigned * cols2, unsigned removed_col_cnt, + const unsigned * removed_cols); virtual table_union_fn * mk_union_fn(const table_base & tgt, const table_base & src, const table_base * delta); virtual table_transformer_fn * mk_project_fn(const table_base & t, unsigned col_cnt, const unsigned * removed_cols); + virtual table_transformer_fn * mk_select_equal_and_project_fn(const table_base & t, + const table_element & value, unsigned col); virtual table_transformer_fn * mk_rename_fn(const table_base & t, unsigned permutation_cycle_len, const unsigned * permutation_cycle); virtual table_mutator_fn * mk_filter_identical_fn(const table_base & t, unsigned col_cnt, @@ -65,6 +73,8 @@ namespace datalog { virtual table_mutator_fn * mk_filter_equal_fn(const table_base & t, const table_element & value, unsigned col); virtual table_mutator_fn * mk_filter_interpreted_fn(const table_base & t, app * condition); + virtual table_transformer_fn * mk_filter_interpreted_and_project_fn(const table_base & t, + app * condition, unsigned removed_col_cnt, const unsigned * removed_cols); virtual table_intersection_filter_fn * mk_filter_by_negation_fn( const table_base & t, const table_base & negated_obj, unsigned joined_col_cnt, diff --git a/src/muz_qe/dl_compiler.cpp b/src/muz_qe/dl_compiler.cpp index 05a0d24b2..3f16d0dab 100644 --- a/src/muz_qe/dl_compiler.cpp +++ b/src/muz_qe/dl_compiler.cpp @@ -73,6 +73,18 @@ namespace datalog { vars.get_cols2(), removed_cols.size(), removed_cols.c_ptr(), result)); } + void compiler::make_filter_interpreted_and_project(reg_idx src, app_ref & cond, + const unsigned_vector & removed_cols, reg_idx & result, instruction_block & acc) { + SASSERT(!removed_cols.empty()); + relation_signature res_sig; + relation_signature::from_project(m_reg_signatures[src], removed_cols.size(), + removed_cols.c_ptr(), res_sig); + result = get_fresh_register(res_sig); + + acc.push_back(instruction::mk_filter_interpreted_and_project(src, cond, + removed_cols.size(), removed_cols.c_ptr(), result)); + } + void compiler::make_select_equal_and_project(reg_idx src, const relation_element & val, unsigned col, reg_idx & result, instruction_block & acc) { relation_signature res_sig; @@ -619,6 +631,116 @@ namespace datalog { } // enforce interpreted tail predicates + unsigned ft_len = r->get_tail_size(); // full tail + ptr_vector tail; + for (unsigned tail_index = ut_len; tail_index < ft_len; ++tail_index) { + tail.push_back(r->get_tail(tail_index)); + } + + if (!tail.empty()) { + app_ref filter_cond(tail.size() == 1 ? to_app(tail.back()) : m.mk_and(tail.size(), tail.c_ptr()), m); + ptr_vector filter_vars; + get_free_vars(filter_cond, filter_vars); + + // create binding + expr_ref_vector binding(m); + binding.resize(filter_vars.size()+1); + + for (unsigned v = 0; v < filter_vars.size(); ++v) { + if (!filter_vars[v]) + continue; + + int2ints::entry * entry = var_indexes.find_core(v); + unsigned src_col; + if (entry) { + src_col = entry->get_data().m_value.back(); + } else { + // we have an unbound variable, so we add an unbound column for it + relation_sort unbound_sort = filter_vars[v]; + + reg_idx new_reg; + bool new_dealloc; + make_add_unbound_column(r, 0, head_pred, filtered_res, unbound_sort, new_reg, new_dealloc, acc); + if (dealloc) + make_dealloc_non_void(filtered_res, acc); + dealloc = new_dealloc; + filtered_res = new_reg; + + src_col = single_res_expr.size(); + single_res_expr.push_back(m.mk_var(v, unbound_sort)); + + entry = var_indexes.insert_if_not_there2(v, unsigned_vector()); + entry->get_data().m_value.push_back(src_col); + } + relation_sort var_sort = m_reg_signatures[filtered_res][src_col]; + binding[filter_vars.size()-v] = m.mk_var(src_col, var_sort); + } + + // check if there are any columns to remove + unsigned_vector remove_columns; + { + unsigned_vector var_idx_to_remove; + ptr_vector vars; + get_free_vars(r->get_head(), vars); + for (int2ints::iterator I = var_indexes.begin(), E = var_indexes.end(); + I != E; ++I) { + unsigned var_idx = I->m_key; + if (!vars.get(var_idx, 0)) { + unsigned_vector & cols = I->m_value; + for (unsigned i = 0; i < cols.size(); ++i) { + remove_columns.push_back(cols[i]); + } + var_idx_to_remove.push_back(var_idx); + } + } + + for (unsigned i = 0; i < var_idx_to_remove.size(); ++i) { + var_indexes.remove(var_idx_to_remove[i]); + } + + // update column idx for after projection state + if (!remove_columns.empty()) { + unsigned_vector offsets; + offsets.resize(single_res_expr.size(), 0); + + for (unsigned i = 0; i < remove_columns.size(); ++i) { + for (unsigned col = remove_columns[i]; col < offsets.size(); ++col) { + ++offsets[col]; + } + } + + for (int2ints::iterator I = var_indexes.begin(), E = var_indexes.end(); + I != E; ++I) { + unsigned_vector & cols = I->m_value; + for (unsigned i = 0; i < cols.size(); ++i) { + cols[i] -= offsets[cols[i]]; + } + } + } + } + + expr_ref renamed(m); + m_context.get_var_subst()(filter_cond, binding.size(), binding.c_ptr(), renamed); + app_ref app_renamed(to_app(renamed), m); + if (remove_columns.empty()) { + if (!dealloc) + make_clone(filtered_res, filtered_res, acc); + acc.push_back(instruction::mk_filter_interpreted(filtered_res, app_renamed)); + } else { + reg_idx new_reg; + std::sort(remove_columns.begin(), remove_columns.end()); + make_filter_interpreted_and_project(filtered_res, app_renamed, remove_columns, new_reg, acc); + if (dealloc) + make_dealloc_non_void(filtered_res, acc); + filtered_res = new_reg; + } + dealloc = true; + } + +#if 0 + // this version is potentially better for non-symbolic tables, + // since it constraints each unbound column at a time (reducing the + // size of intermediate results). unsigned ft_len=r->get_tail_size(); //full tail for(unsigned tail_index=ut_len; tail_indexget_tail(tail_index); @@ -686,6 +808,7 @@ namespace datalog { acc.push_back(instruction::mk_filter_interpreted(filtered_res, app_renamed)); dealloc = true; } +#endif { //put together the columns of head relation @@ -737,7 +860,7 @@ namespace datalog { make_dealloc_non_void(new_head_reg, acc); } - finish: +// finish: m_instruction_observer.finish_rule(); } diff --git a/src/muz_qe/dl_compiler.h b/src/muz_qe/dl_compiler.h index 78b4623de..e0f9af424 100644 --- a/src/muz_qe/dl_compiler.h +++ b/src/muz_qe/dl_compiler.h @@ -145,6 +145,8 @@ namespace datalog { instruction_block & acc); void make_join_project(reg_idx t1, reg_idx t2, const variable_intersection & vars, const unsigned_vector & removed_cols, reg_idx & result, instruction_block & acc); + void make_filter_interpreted_and_project(reg_idx src, app_ref & cond, + const unsigned_vector & removed_cols, reg_idx & result, instruction_block & acc); void make_select_equal_and_project(reg_idx src, const relation_element & val, unsigned col, reg_idx & result, instruction_block & acc); /** diff --git a/src/muz_qe/dl_hassel_common.cpp b/src/muz_qe/dl_hassel_common.cpp new file mode 100755 index 000000000..6201868ca --- /dev/null +++ b/src/muz_qe/dl_hassel_common.cpp @@ -0,0 +1,434 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + dl_hassel_common.cpp + +Abstract: + + + +Revision History: + +--*/ + +#include "dl_hassel_common.h" +#include "dl_context.h" + +#include + +namespace datalog { + + static void formula_to_dnf_aux(app *and, unsigned idx, std::set& conjexpr, std::set& toplevel, ast_manager& m) { + if (idx == and->get_num_args()) { + std::vector v(conjexpr.begin(), conjexpr.end()); + toplevel.insert(m.mk_and((unsigned)v.size(), &v[0])); + return; + } + + expr *e = and->get_arg(idx); + if (is_app(e) && to_app(e)->get_decl_kind() == OP_OR) { + app *or = to_app(e); + // quick subsumption test: if any of the elements of the OR is already ANDed, then we skip this OR + for (unsigned i = 0; i < or->get_num_args(); ++i) { + if (conjexpr.count(or->get_arg(i))) { + formula_to_dnf_aux(and, idx+1, conjexpr, toplevel, m); + return; + } + } + + for (unsigned i = 0; i < or->get_num_args(); ++i) { + std::set conjexpr2(conjexpr); + conjexpr2.insert(or->get_arg(i)); + formula_to_dnf_aux(and, idx+1, conjexpr2, toplevel, m); + } + } else { + conjexpr.insert(e); + formula_to_dnf_aux(and, idx+1, conjexpr, toplevel, m); + } + } + + expr_ref formula_to_dnf(expr_ref f) { + app *a = to_app(f); + SASSERT(a->get_decl_kind() == OP_AND); + std::set toplevel, conjexpr; + formula_to_dnf_aux(a, 0, conjexpr, toplevel, f.m()); + + if (toplevel.size() > 1) { + std::vector v(toplevel.begin(), toplevel.end()); + return expr_ref(f.m().mk_or((unsigned)v.size(), &v[0]), f.m()); + } else { + return expr_ref(*toplevel.begin(), f.m()); + } + } + + bool bit_vector::contains(const bit_vector & other) const { + unsigned n = num_words(); + if (n == 0) + return true; + + for (unsigned i = 0; i < n - 1; ++i) { + if ((m_data[i] & other.m_data[i]) != other.m_data[i]) + return false; + } + unsigned bit_rest = m_num_bits % 32; + unsigned mask = (1 << bit_rest) - 1; + if (mask == 0) mask = UINT_MAX; + unsigned other_data = other.m_data[n-1] & mask; + return (m_data[n-1] & other_data) == other_data; + } + + bool bit_vector::contains(const bit_vector & other, unsigned idx) const { + // TODO: optimize this to avoid copy + return slice(idx, other.size()).contains(other); + } + + bool bit_vector::contains_consecutive_zeros() const { + unsigned n = num_words(); + if (n == 0) + return false; + + for (unsigned i = 0; i < n - 1; ++i) { + if ((((m_data[i] << 1) | m_data[i]) & 0xAAAAAAAA) != 0xAAAAAAAA) + return true; + } + unsigned bit_rest = m_num_bits % 32; + unsigned mask = (1 << bit_rest) - 1; + if (mask == 0) mask = UINT_MAX; + mask &= 0xAAAAAAAA; + return ((((m_data[n-1] << 1) | m_data[n-1]) & mask) != mask); + } + + bit_vector bit_vector::slice(unsigned idx, unsigned length) const { + bit_vector Res(length); + // TODO: optimize w/ memcpy when possible + for (unsigned i = idx; i < idx + length; ++i) { + Res.push_back(get(i)); + } + SASSERT(Res.size() == length); + return Res; + } + + void bit_vector::append(const bit_vector & other) { + if (other.empty()) + return; + + if ((m_num_bits % 32) == 0) { + unsigned prev_num_bits = m_num_bits; + resize(m_num_bits + other.m_num_bits); + memcpy(&get_bit_word(prev_num_bits), other.m_data, other.num_words() * sizeof(unsigned)); + return; + } + + // TODO: optimize the other cases. + for (unsigned i = 0; i < other.m_num_bits; ++i) { + push_back(other.get(i)); + } + } + + uint64 bit_vector::to_number(unsigned idx, unsigned length) const { + SASSERT(length <= 64); + uint64 r = 0; + for (unsigned i = 0; i < length; ++i) { + r = (r << 1) | (uint64)get(idx+i); + } + return r; + } + + bool bit_vector::operator<(bit_vector const & other) const { + SASSERT(m_num_bits == other.m_num_bits); + unsigned n = num_words(); + if (n == 0) + return false; + + for (unsigned i = 0; i < n - 1; ++i) { + if (m_data[i] > other.m_data[i]) + return false; + if (m_data[i] < other.m_data[i]) + return true; + } + + unsigned bit_rest = m_num_bits % 32; + unsigned mask = (1 << bit_rest) - 1; + if (mask == 0) mask = UINT_MAX; + return (m_data[n-1] & mask) < (other.m_data[n-1] & mask); + } + + table_information::table_information(table_plugin & p, const table_signature& sig) : + m_column_info(sig.size()+1), + m_bv_util(p.get_context().get_manager()), + m_decl_util(p.get_context().get_manager()) { + + unsigned column = 0; + for (unsigned i = 0; i < sig.size(); ++i) { + unsigned num_bits = uint64_log2(sig[i]); + SASSERT(num_bits == 64 || (1ULL << num_bits) == sig[i]); + m_column_info[i] = column; + column += num_bits; + } + m_column_info[sig.size()] = column; + } + + void table_information::expand_column_vector(unsigned_vector& v, const table_information *other) const { + unsigned_vector orig; + orig.swap(v); + + for (unsigned i = 0; i < orig.size(); ++i) { + unsigned col, limit; + if (orig[i] < get_num_cols()) { + col = column_idx(orig[i]); + limit = col + column_num_bits(orig[i]); + } else { + unsigned idx = orig[i] - get_num_cols(); + col = get_num_bits() + other->column_idx(idx); + limit = col + other->column_num_bits(idx); + } + + for (; col < limit; ++col) { + v.push_back(col); + } + } + } + + void table_information::display(std::ostream & out) const { + out << '<'; + for (unsigned i = 0; i < get_num_cols(); ++i) { + if (i > 0) + out << ", "; + out << column_num_bits(i); + } + out << ">\n"; + } + + ternary_bitvector::ternary_bitvector(unsigned size, bool full) : + bit_vector() { + resize(size, full); + } + + ternary_bitvector::ternary_bitvector(uint64 n, unsigned num_bits) : + bit_vector(2 * num_bits) { + append_number(n, num_bits); + } + + ternary_bitvector::ternary_bitvector(const table_fact& f, const table_information& t) : + bit_vector(2 * t.get_num_bits()) { + for (unsigned i = 0; i < f.size(); ++i) { + SASSERT(t.column_idx(i) == size()); + append_number(f[i], t.column_num_bits(i)); + } + SASSERT(size() == t.get_num_bits()); + } + + void ternary_bitvector::fill1() { + memset(m_data, 0xFF, m_capacity * sizeof(unsigned)); + } + + unsigned ternary_bitvector::get(unsigned idx) const { + idx *= 2; + return (bit_vector::get(idx) << 1) | (unsigned)bit_vector::get(idx+1); + } + + void ternary_bitvector::set(unsigned idx, unsigned val) { + SASSERT(val == BIT_0 || val == BIT_1 || val == BIT_x); + idx *= 2; + bit_vector::set(idx, (val >> 1) != 0); + bit_vector::set(idx+1, (val & 1) != 0); + } + + void ternary_bitvector::push_back(unsigned val) { + SASSERT(val == BIT_0 || val == BIT_1 || val == BIT_x); + bit_vector::push_back((val >> 1) != 0); + bit_vector::push_back((val & 1) != 0); + } + + void ternary_bitvector::append_number(uint64 n, unsigned num_bits) { + SASSERT(num_bits <= 64); + for (int bit = num_bits-1; bit >= 0; --bit) { + if (n & (1ULL << bit)) { + push_back(BIT_1); + } else { + push_back(BIT_0); + } + } + } + + void ternary_bitvector::mk_idx_eq(unsigned idx, ternary_bitvector& val) { + for (unsigned i = 0; i < val.size(); ++i) { + set(idx+i, val.get(i)); + } + } + + ternary_bitvector ternary_bitvector::and(const ternary_bitvector& other) const{ + ternary_bitvector result(*this); + result &= other; + return result; + } + + void ternary_bitvector::neg(union_ternary_bitvector& result) const { + ternary_bitvector negated; + negated.resize(size()); + + for (unsigned i = 0; i < size(); ++i) { + switch (get(i)) { + case BIT_0: + negated.fill1(); + negated.set(i, BIT_1); + break; + case BIT_1: + negated.fill1(); + negated.set(i, BIT_0); + break; + default: + continue; + } + result.add_fact(negated); + } + } + + static void join_fix_eqs(ternary_bitvector& TBV, unsigned idx, unsigned col2_offset, + const unsigned_vector& cols1, const unsigned_vector& cols2, + union_ternary_bitvector& result) { + if (idx == cols1.size()) { + result.add_fact(TBV); + return; + } + + unsigned idx1 = cols1[idx]; + unsigned idx2 = cols2[idx] + col2_offset; + unsigned v1 = TBV.get(idx1); + unsigned v2 = TBV.get(idx2); + + if (v1 == BIT_x) { + if (v2 == BIT_x) { + // both x: duplicate row + ternary_bitvector TBV2(TBV); + TBV2.set(idx1, BIT_0); + TBV2.set(idx2, BIT_0); + join_fix_eqs(TBV2, idx+1, col2_offset, cols1, cols2, result); + + TBV.set(idx1, BIT_1); + TBV.set(idx2, BIT_1); + } else { + TBV.set(idx1, v2); + } + } else if (v2 == BIT_x) { + TBV.set(idx2, v1); + } else if (v1 != v2) { + // columns don't match + return; + } + join_fix_eqs(TBV, idx+1, col2_offset, cols1, cols2, result); + } + + void ternary_bitvector::join(const ternary_bitvector& other, + const unsigned_vector& cols1, + const unsigned_vector& cols2, + union_ternary_bitvector& result) const { + ternary_bitvector TBV(*this); + TBV.append(other); + join_fix_eqs(TBV, 0, size(), cols1, cols2, result); + } + + bool ternary_bitvector::project(const unsigned_vector& delcols, ternary_bitvector& result) const { + unsigned *rm_cols = delcols.c_ptr(); + + for (unsigned i = 0; i < size(); ++i) { + if (*rm_cols == i) { + ++rm_cols; + continue; + } + result.push_back(get(i)); + } + return true; + } + + static void copy_column(ternary_bitvector& CopyTo, const ternary_bitvector& CopyFrom, + unsigned col_dst, unsigned col_src, const table_information& src_table, + const table_information& dst_table) { + unsigned idx_dst = dst_table.column_idx(col_dst); + unsigned idx_src = src_table.column_idx(col_src); + unsigned num_bits = dst_table.column_num_bits(col_dst); + SASSERT(num_bits == src_table.column_num_bits(col_src)); + + for (unsigned i = 0; i < num_bits; ++i) { + CopyTo.set(idx_dst+i, CopyFrom.get(idx_src+i)); + } + } + + void ternary_bitvector::rename(const unsigned_vector& cyclecols, + const unsigned_vector& out_of_cycle_cols, + const table_information& src_table, + const table_information& dst_table, + ternary_bitvector& result) const { + result.resize(dst_table.get_num_bits()); + + for (unsigned i = 1; i < cyclecols.size(); ++i) { + copy_column(result, *this, cyclecols[i-1], cyclecols[i], src_table, dst_table); + } + copy_column(result, *this, cyclecols[cyclecols.size()-1], cyclecols[0], src_table, dst_table); + + for (unsigned i = 0; i < out_of_cycle_cols.size(); ++i) { + unsigned col = out_of_cycle_cols[i]; + copy_column(result, *this, col, col, src_table, dst_table); + } + } + + unsigned ternary_bitvector::size_in_bytes() const { + return sizeof(*this) + m_capacity; + } + + void ternary_bitvector::display(std::ostream & out) const { + for (unsigned i = 0; i < size(); ++i) { + switch (get(i)) { + case BIT_0: + out << '0'; + break; + case BIT_1: + out << '1'; + break; + case BIT_x: + out << 'x'; + break; + default: + UNREACHABLE(); + } + } + } + +#if Z3DEBUG + void ternary_bitvector::expand(std::set & BVs) const { + bit_vector BV(m_num_bits); + expand(BVs, BV, 0); + } + + void ternary_bitvector::expand(std::set & BVs, bit_vector &BV, unsigned idx) const { + if (idx == size()) { + BVs.insert(BV); + return; + } + + switch (get(idx)) { + case BIT_0: + BV.push_back(false); + expand(BVs, BV, idx+1); + break; + case BIT_1: + BV.push_back(true); + expand(BVs, BV, idx+1); + break; + case BIT_x: { // x: duplicate + bit_vector BV2(BV); + BV.push_back(false); + BV2.push_back(true); + expand(BVs, BV, idx+1); + expand(BVs, BV2, idx+1); + } + break; + default: + UNREACHABLE(); + } + } +#endif + +} diff --git a/src/muz_qe/dl_hassel_common.h b/src/muz_qe/dl_hassel_common.h new file mode 100755 index 000000000..7c1d1e614 --- /dev/null +++ b/src/muz_qe/dl_hassel_common.h @@ -0,0 +1,1079 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + dl_hassel_common.h + +Abstract: + + + +Revision History: + +--*/ + +#ifndef _DL_HASSEL_COMMON_H_ +#define _DL_HASSEL_COMMON_H_ + +#include "bit_vector.h" +#include "dl_base.h" +#include "bv_decl_plugin.h" +#include "union_find.h" +#include +#include + +#define BIT_0 ((0<<1)|1) +#define BIT_1 ((1<<1)|0) +#define BIT_x ((1<<1)|1) + +namespace datalog { + + expr_ref formula_to_dnf(expr_ref f); + + class bit_vector : public ::bit_vector { + public: + bit_vector() : ::bit_vector() {} + bit_vector(unsigned bits) : ::bit_vector(bits) {} + + bool contains(const bit_vector & other) const; + bool contains(const bit_vector & other, unsigned idx) const; + bool contains_consecutive_zeros() const; + + bit_vector slice(unsigned idx, unsigned length) const; + void append(const bit_vector & other); + + uint64 to_number(unsigned idx, unsigned length) const; + + // for std::less operations + bool operator<(bit_vector const & other) const; + }; + + + class table_information { + unsigned_vector m_column_info; + bv_util m_bv_util; + dl_decl_util m_decl_util; + + public: + table_information(table_plugin & p, const table_signature& sig); + + unsigned get_num_bits() const { + return m_column_info.back(); + } + + unsigned get_num_cols() const { + return m_column_info.size()-1; + } + + unsigned column_idx(unsigned col) const { + return m_column_info[col]; + } + + unsigned column_num_bits(unsigned col) const { + return m_column_info[col+1] - m_column_info[col]; + } + + void expand_column_vector(unsigned_vector& v, const table_information *other = 0) const; + + void display(std::ostream & out) const; + + const bv_util& get_bv_util() const { return m_bv_util; } + const dl_decl_util& get_decl_util() const { return m_decl_util; } + }; + + + template class union_ternary_bitvector; + + + class ternary_bitvector : private bit_vector { + public: + ternary_bitvector() : bit_vector() {} + ternary_bitvector(unsigned size) : bit_vector(2 * size) {} + + ternary_bitvector(unsigned size, bool full); + ternary_bitvector(uint64 n, unsigned num_bits); + ternary_bitvector(const table_fact& f, const table_information& t); + + void swap(ternary_bitvector& other) { + SASSERT(size() == other.size()); + bit_vector::swap(other); + } + + void resize(unsigned new_size, bool val = false) { + bit_vector::resize(2 * new_size, val); + } + + void reset() { + m_num_bits = 0; + } + + unsigned size() const { + SASSERT((m_num_bits % 2) == 0); + return m_num_bits/2; + } + + void fill1(); + + void append(const ternary_bitvector & other) { bit_vector::append(other); } + bool contains(const ternary_bitvector & other) const { return bit_vector::contains(other); } + + bool is_empty() const { return contains_consecutive_zeros(); } + + unsigned get(unsigned idx) const; + void set(unsigned idx, unsigned val); + void push_back(unsigned val); + void append_number(uint64 n, unsigned num_bits); + void mk_idx_eq(unsigned idx, ternary_bitvector& val); + + ternary_bitvector and(const ternary_bitvector& other) const; + void neg(union_ternary_bitvector& result) const; + + void join(const ternary_bitvector& other, const unsigned_vector& cols1, + const unsigned_vector& cols2, union_ternary_bitvector& result) const; + + bool project(const unsigned_vector& delcols, ternary_bitvector& result) const; + + void rename(const unsigned_vector& cyclecols, const unsigned_vector& out_of_cycle_cols, + const table_information& src_table, const table_information& dst_table, + ternary_bitvector& result) const; + + static bool has_subtract() { return false; } + void subtract(const union_ternary_bitvector& other, + union_ternary_bitvector& result) const { UNREACHABLE(); } + + void display(std::ostream & out) const; + unsigned size_in_bytes() const; + +#if Z3DEBUG + void expand(std::set & BVs) const; +#endif + + private: +#if Z3DEBUG + void expand(std::set & BVs, bit_vector &BV, unsigned idx) const; +#endif + }; + + + template + class union_ternary_bitvector { + typedef std::list union_t; + + union_t m_bitvectors; + unsigned m_bv_size; //!< number of ternary bits + + public: + union_ternary_bitvector(unsigned bv_size) : m_bv_size(bv_size) {} + + union_ternary_bitvector(unsigned bv_size, bool full) : m_bv_size(bv_size) { + if (full) + mk_full(); + } + + union_ternary_bitvector and(const union_ternary_bitvector & Other) const { + if (empty()) + return *this; + if (Other.empty()) + return Other; + + union_ternary_bitvector Ret(m_bv_size); + + for (const_iterator I = begin(), E = end(); I != E; ++I) { + for (const_iterator II = Other.begin(), EE = Other.end(); II != EE; ++II) { + T row(I->and(*II)); + if (!row.is_empty()) + Ret.add_fact(row); + } + } + return Ret; + } + + union_ternary_bitvector or(const union_ternary_bitvector & Other) const { + if (empty()) + return Other; + if (Other.empty()) + return *this; + + union_ternary_bitvector Ret(*this); + Ret.add_facts(Other); + return Ret; + } + + union_ternary_bitvector neg() const { + union_ternary_bitvector Ret(m_bv_size); + Ret.mk_full(); + + union_ternary_bitvector negated(m_bv_size); + for (const_iterator I = begin(), E = end(); I != E; ++I) { + negated.reset(); + I->neg(negated); + Ret.swap(Ret.and(negated)); + } + return Ret; + } + + void subtract(const union_ternary_bitvector& other) { + if (!T::has_subtract()) { + swap(this->and(other.neg())); + return; + } + + union_ternary_bitvector subtracted(m_bv_size); + for (const_iterator I = begin(), E = end(); I != E; ++I) { + I->subtract(other, subtracted); + } + swap(subtracted); + } + +#if 0 + union_ternary_bitvector gc() const { + // Simple subsumption-based cleaning. + union_ternary_bitvector Ret(m_bv_size); + for (union_t::const_reverse_iterator I = m_bitvectors.rbegin(), E = m_bitvectors.rend(); I != E; ++I) { + Ret.add_fact(*I); + } + return Ret; + } +#endif + + void join(const union_ternary_bitvector& other, const unsigned_vector& cols1, + const unsigned_vector& cols2, union_ternary_bitvector& result) const { + for (const_iterator I = begin(), E = end(); I != E; ++I) { + for (const_iterator II = other.begin(), EE = other.end(); II != EE; ++II) { + I->join(*II, cols1, cols2, result); + } + } + } + + void rename(const unsigned_vector& cyclecols, const unsigned_vector& out_of_cycle_cols, + const table_information& src_table, const table_information& dst_table, + union_ternary_bitvector& result) const { + T row(m_bv_size); + for (const_iterator I = begin(), E = end(); I != E; ++I) { + row.reset(); + I->rename(cyclecols, out_of_cycle_cols, src_table, dst_table, row); + result.add_new_fact(row); + } + } + + void project(const unsigned_vector& delcols, union_ternary_bitvector& result) const { + unsigned new_size = m_bv_size - (delcols.size()-1); + T row(new_size); + + for (const_iterator I = begin(), E = end(); I != E; ++I) { + row.reset(); + if (I->project(delcols, row)) { + SASSERT(!row.is_empty()); + result.add_fact(row); + } + } + } + + private: + typedef union_find<> subset_ints; + + // returns 1 if row should be removed, 0 otherwise + static int fix_single_bit(T & BV, unsigned idx, unsigned value, const subset_ints& equalities) { + unsigned root = equalities.find(idx); + idx = root; + do { + unsigned bitval = BV.get(idx); + if (bitval == BIT_x) { + BV.set(idx, value); + } else if (bitval != value) { + return 1; + } + idx = equalities.next(idx); + } while (idx != root); + return 0; + } + + static int fix_single_bit(T & BV1, unsigned idx1, T & BV2, unsigned idx2, + subset_ints& equalities, bool discard_col) { + unsigned A = BV1.get(idx1); + unsigned B = BV2.get(idx2); + + if (A == BIT_x) { + if (B == BIT_x) { + // Both are don't cares. + /////// FIXME::: don't duplicate rows with diff table + if (!discard_col) + return 2; // duplicate row + equalities.merge(idx1, idx2); + return 0; + } else { + // only A is don't care. + return fix_single_bit(BV1, idx1, B, equalities); + } + } else if (B == BIT_x) { + // Only B is don't care. + return fix_single_bit(BV2, idx2, A, equalities); + } else if (A == B) { + return 0; + } else { + return 1; // remove row + } + } + + void fix_eq_bits(unsigned idx1, const T *BV, unsigned idx2, unsigned length, + subset_ints& equalities, const bit_vector& discard_cols) { + for (unsigned i = 0; i < length; ++i) { + for (union_t::iterator I = m_bitvectors.begin(), E = m_bitvectors.end(); I != E; ) { + T *eqBV = BV ? const_cast(BV) : &*I; + bool discard_col = discard_cols.get(idx1+i) || (!BV && discard_cols.get(idx2+i)); + + switch (fix_single_bit(*I, idx1+i, *eqBV, idx2+i, equalities, discard_col)) { + case 1: + // remove row + I = m_bitvectors.erase(I); + break; + + case 2: { + // duplicate row + T BV2(*I); + I->set(idx1+i, BIT_0); + I->set(idx2+i, BIT_0); + + BV2.set(idx1+i, BIT_1); + BV2.set(idx2+i, BIT_1); + m_bitvectors.insert(I, BV2); + ++I; + break;} + + default: + // bits fixed + ++I; + } + } + } + } + + /// make bits of table [idx,idx+max_length] equal to e sliced starting at idx2 + unsigned fix_eq_bits(unsigned idx, const expr *e, unsigned idx2, unsigned max_length, + const table_information& t, subset_ints& equalities, + const bit_vector & discard_cols) { + const bv_util& bvu = t.get_bv_util(); + const dl_decl_util& dutil = t.get_decl_util(); + + rational n; + unsigned bv_size; + if (bvu.is_numeral(e, n, bv_size)) { + T num(n.get_int64(), bv_size); + SASSERT(idx2 < bv_size); + max_length = std::min(max_length, bv_size - idx2); + fix_eq_bits(idx, &num, idx2, max_length, equalities, discard_cols); + return idx + max_length; + } + + uint64 num; + if (dutil.is_numeral(e, num)) { + T num_bv(num, max_length); + fix_eq_bits(idx, &num_bv, idx2, max_length, equalities, discard_cols); + return idx + max_length; + } + + if (bvu.is_concat(e)) { + const app *a = to_app(e); + + // skip the first elements of the concat if e.g. we have a top level extract + unsigned i = 0; + for (; i < a->get_num_args(); ++i) { + unsigned arg_size = bvu.get_bv_size(a->get_arg(i)); + if (idx2 < arg_size) + break; + idx2 -= arg_size; + } + + SASSERT(i < a->get_num_args()); + for (; max_length > 0 && i < a->get_num_args(); ++i) { + unsigned idx0 = idx; + idx = fix_eq_bits(idx, a->get_arg(i), idx2, max_length, t, equalities, discard_cols); + idx2 = 0; + SASSERT((idx - idx0) <= max_length); + max_length = max_length - (idx - idx0); + } + return idx; + } + + unsigned low, high; + expr *e2; + if (bvu.is_extract(e, low, high, e2)) { + SASSERT(low <= high); + unsigned size = bvu.get_bv_size(e2); + unsigned offset = size - (high+1) + idx2; + SASSERT(idx2 < (high-low+1)); + max_length = std::min(max_length, high - low + 1 - idx2); + return fix_eq_bits(idx, e2, offset, max_length, t, equalities, discard_cols); + } + + if (e->get_kind() == AST_VAR) { + unsigned idx_var = idx2 + t.column_idx(to_var(e)->get_idx()); + SASSERT(idx2 < t.column_num_bits(to_var(e)->get_idx())); + max_length = std::min(max_length, t.column_num_bits(to_var(e)->get_idx()) - idx2); + fix_eq_bits(idx, 0, idx_var, max_length, equalities, discard_cols); + return idx + max_length; + } + + NOT_IMPLEMENTED_YET(); + return 0; + } + + void filter(const expr *e, subset_ints& equalities, const bit_vector& discard_cols, + const table_information& t) { + switch (e->get_kind()) { + case AST_APP: { + const app *app = to_app(e); + switch (app->get_decl_kind()) { + case OP_AND: + for (unsigned i = 0; i < app->get_num_args(); ++i) { + filter(app->get_arg(i), equalities, discard_cols, t); + } + return; + + case OP_EQ: { + const expr *a = app->get_arg(0); + const var *v; + unsigned vidx = 0; + unsigned length; + + unsigned low, high; + expr *e2; + if (is_var(a)) { + v = to_var(a); + length = t.column_num_bits(v->get_idx()); + } else if (t.get_bv_util().is_extract(a, low, high, e2)) { + vidx = t.get_bv_util().get_bv_size(e2) - high - 1; + length = high - low + 1; + SASSERT(is_var(e2)); + v = to_var(e2); + } else { + NOT_IMPLEMENTED_YET(); + } + vidx += t.column_idx(v->get_idx()); + + unsigned final_idx = fix_eq_bits(vidx, app->get_arg(1), 0, length, t, equalities, discard_cols); + SASSERT(final_idx == vidx + length); + (void)final_idx; + return;} + + case OP_FALSE: + reset(); + return; + + case OP_NOT: { + union_ternary_bitvector sub(m_bv_size, true); + sub.filter(app->get_arg(0), equalities, discard_cols, t); + this->subtract(sub); + return;} + + case OP_OR: { + union_ternary_bitvector orig(m_bv_size); + swap(orig); + for (unsigned i = 0; i < app->get_num_args(); ++i) { + union_ternary_bitvector tmp(orig); + subset_ints eqs(equalities); + tmp.filter(app->get_arg(i), eqs, discard_cols, t); + add_facts(tmp); + } + return;} + + case OP_TRUE: + return; + + default: + std::cerr << "app decl: " << app->get_decl()->get_name() << " (" << app->get_decl_kind() << ")\n"; + NOT_IMPLEMENTED_YET(); + } + break;} + + case AST_VAR: { + // boolean var must be true (10) + SASSERT(t.column_num_bits(to_var(e)->get_idx()) == 1); + unsigned idx = t.column_idx(to_var(e)->get_idx()); + ternary_bitvector BV(1); + BV.push_back(BIT_1); + T BV2(BV); + fix_eq_bits(idx, &BV2, 0, 2, equalities, discard_cols); + return;} + + default: + break; + } + std::cerr << "expr kind: " << get_ast_kind_name(e->get_kind()) << '\n'; + NOT_IMPLEMENTED_YET(); + } + + public: + void filter(const expr *cond, const bit_vector& discard_cols, const table_information& table) { + // datastructure to store equalities with columns that will be projected out + union_find_default_ctx union_ctx; + subset_ints equalities(union_ctx); + for (unsigned i = 0, e = discard_cols.size(); i < e; ++i) { + equalities.mk_var(); + } + + filter(cond, equalities, discard_cols, table); + } + + bool contains(const T & fact) const { + for (const_iterator I = begin(), E = end(); I != E; ++I) { + if (I->contains(fact)) + return true; + } + return false; + } + + bool contains(const union_ternary_bitvector & other) const { + for (const_iterator I = other.begin(), E = other.end(); I != E; ++I) { + for (const_iterator II = begin(), EE = end(); II != EE; ++II) { + if (II->contains(*I)) + goto next_iter; + } + return false; +next_iter: ; + } + return true; + } + + unsigned num_disjs() const { + return (unsigned)m_bitvectors.size(); + } + + unsigned num_bytes() const { + unsigned size = sizeof(*this); + for (const_iterator I = begin(), E = end(); I != E; ++I) { + size += I->size_in_bytes(); + } + return size; + } + +#if Z3DEBUG + void expand(std::set & BVs) const { + for (const_iterator I = begin(), E = end(); I != E; ++I) { + I->expand(BVs); + } + } +#endif + + void add_facts(const union_ternary_bitvector & Other, union_ternary_bitvector *Delta = 0) { + for (const_iterator I = Other.begin(), E = Other.end(); I != E; ++I) { + if (add_fact(*I) && Delta) + Delta->add_fact(*I); + } + } + + bool add_fact(const T & fact) { + if (contains(fact)) + return false; + add_new_fact(fact); + return true; + } + + void add_new_fact(const T & fact) { + SASSERT(m_bv_size == fact.size()); + + // TODO: optimize sequence (karnaugh maps??) + // At least join 1-bit different BVs + m_bitvectors.push_back(fact); + } + + void mk_full() { + reset(); + add_new_fact(T(m_bv_size, true)); + } + + typedef typename union_t::const_iterator const_iterator; + + const_iterator begin() const { return m_bitvectors.begin(); } + const_iterator end() const { return m_bitvectors.end(); } + + bool empty() const { return m_bitvectors.empty(); } + void reset() { m_bitvectors.clear(); } + + void swap(union_ternary_bitvector& other) { + SASSERT(m_bv_size == other.m_bv_size); + m_bitvectors.swap(other.m_bitvectors); + } + + void display(std::ostream & out) const { + out << '#' << num_disjs() << " (bv" << m_bv_size << ") "; + + bool first = true; + for (const_iterator I = begin(), E = end(); I != E; ++I) { + if (!first) + out << " \\/ "; + first = false; + I->display(out); + } + out << '\n'; + } + }; + + + template + class common_hassel_table_plugin : public table_plugin { + public: + common_hassel_table_plugin(symbol &s, relation_manager & manager) : + table_plugin(s, manager) { } + + virtual table_base * mk_empty(const table_signature & s) { + return alloc(T, *this, s); + } + + virtual table_base * mk_full(func_decl* p, const table_signature & s) { + T *t = static_cast(mk_empty(s)); + t->mk_full(); + return t; + } + + virtual bool can_handle_signature(const table_signature & s) { + return s.functional_columns() == 0; + } + + private: + ast_manager& get_ast_manager() { return get_context().get_manager(); } + + class join_fn : public convenient_table_join_fn { + public: + join_fn(const T & t1, const T & t2, unsigned col_cnt, const unsigned *cols1, const unsigned *cols2) + : convenient_table_join_fn(t1.get_signature(), t2.get_signature(), col_cnt, cols1, cols2) { + t1.expand_column_vector(m_cols1); + t2.expand_column_vector(m_cols2); + } + + virtual table_base * operator()(const table_base & tb1, const table_base & tb2) { + const T & T1 = static_cast(tb1); + const T & T2 = static_cast(tb2); + T * Res = static_cast(T1.get_plugin().mk_empty(get_result_signature())); + T1.m_bitsets.join(T2.m_bitsets, m_cols1, m_cols2, Res->m_bitsets); + TRACE("dl_hassel", tout << "final size: " << Res->get_size_estimate_rows() << '\n';); + return Res; + } + }; + + public: + virtual table_join_fn * mk_join_fn(const table_base & t1, const table_base & t2, + unsigned col_cnt, const unsigned * cols1, const unsigned * cols2) { + if (!check_kind(t1) || !check_kind(t2)) + return 0; + return alloc(join_fn, static_cast(t1), static_cast(t2), col_cnt, cols1, cols2); + } + + private: + class union_fn : public table_union_fn { + public: + virtual void operator()(table_base & tgt0, const table_base & src0, table_base * delta0) { + T & tgt = static_cast(tgt0); + const T & src = static_cast(src0); + T * delta = static_cast(delta0); + tgt.m_bitsets.add_facts(src.m_bitsets, delta ? &delta->m_bitsets : 0); + TRACE("dl_hassel", tout << "final size: " << tgt.get_size_estimate_rows() << '\n';); + } + }; + + public: + virtual table_union_fn * mk_union_fn(const table_base & tgt, const table_base & src, + const table_base * delta) { + if (!check_kind(tgt) || !check_kind(src)) + return 0; + return alloc(union_fn); + } + + private: + class project_fn : public convenient_table_project_fn { + public: + project_fn(const T & t, unsigned removed_col_cnt, const unsigned * removed_cols) + : convenient_table_project_fn(t.get_signature(), removed_col_cnt, removed_cols) { + t.expand_column_vector(m_removed_cols); + m_removed_cols.push_back(UINT_MAX); + } + + virtual table_base * operator()(const table_base & tb) { + const T & t = static_cast(tb); + T * res = static_cast(t.get_plugin().mk_empty(get_result_signature())); + t.m_bitsets.project(m_removed_cols, res->m_bitsets); + TRACE("dl_hassel", tout << "final size: " << res->get_size_estimate_rows() << '\n';); + return res; + } + }; + + public: + virtual table_transformer_fn * mk_project_fn(const table_base & t, unsigned col_cnt, + const unsigned * removed_cols) { + if (!check_kind(t)) + return 0; + return alloc(project_fn, static_cast(t), col_cnt, removed_cols); + } + + private: + class rename_fn : public convenient_table_rename_fn { + unsigned_vector m_out_of_cycle; + public: + rename_fn(const table_signature & orig_sig, unsigned permutation_cycle_len, const unsigned * permutation_cycle) + : convenient_table_rename_fn(orig_sig, permutation_cycle_len, permutation_cycle) { + SASSERT(permutation_cycle_len >= 2); + idx_set cycle_cols; + for (unsigned i = 0; i < permutation_cycle_len; ++i) { + cycle_cols.insert(permutation_cycle[i]); + } + for (unsigned i = 0; i < orig_sig.size(); ++i) { + if (!cycle_cols.contains(i)) + m_out_of_cycle.push_back(i); + } + } + + virtual table_base * operator()(const table_base & tb) { + const T & t = static_cast(tb); + T * res = static_cast(t.get_plugin().mk_empty(get_result_signature())); + t.m_bitsets.rename(m_cycle, m_out_of_cycle, t, *res, res->m_bitsets); + TRACE("dl_hassel", tout << "final size: " << res->get_size_estimate_rows() << '\n';); + return res; + } + }; + + public: + virtual table_transformer_fn * mk_rename_fn(const table_base & t, unsigned permutation_cycle_len, + const unsigned * permutation_cycle) { + if (!check_kind(t)) + return 0; + return alloc(rename_fn, t.get_signature(), permutation_cycle_len, permutation_cycle); + } + + private: + class filter_equal_fn : public table_mutator_fn { + typename T::bitset_t m_filter; + public: + filter_equal_fn(const T & t, const table_element val, unsigned col) : + m_filter(t.get_num_bits()) { + ternary_bitvector filter_row(t.get_num_bits(), true); + ternary_bitvector column(val, t.column_num_bits(col)); + filter_row.mk_idx_eq(t.column_idx(col), column); + m_filter.add_new_fact(filter_row); + } + + virtual void operator()(table_base & tb) { + T & t = static_cast(tb); + t.m_bitsets.swap(m_filter.and(t.m_bitsets)); + TRACE("dl_hassel", tout << "final size: " << t.get_size_estimate_rows() << '\n';); + } + }; + + public: + virtual table_mutator_fn * mk_filter_equal_fn(const table_base & t, const table_element & value, + unsigned col) { + if (!check_kind(t)) + return 0; + return alloc(filter_equal_fn, static_cast(t), value, col); + } + + private: + static bool cond_is_guard(const expr *e, const table_information& t) { + switch (e->get_kind()) { + case AST_APP: { + const app *app = to_app(e); + switch (app->get_decl_kind()) { + case OP_AND: + case OP_OR: + case OP_NOT: + for (unsigned i = 0; i < app->get_num_args(); ++i) { + if (!cond_is_guard(app->get_arg(i), t)) + return false; + } + return true; + + case OP_EQ: { + const expr *a = app->get_arg(0), *b = app->get_arg(1); + + // column equality is not succinctly representable with TBVs + if (is_var(a) && is_var(b)) + return false; + + // (= var (concat var foo)) + if (t.get_bv_util().is_concat(b)) + return false; + + return true;} + + case OP_FALSE: + case OP_TRUE: + return true; + + default: + return false; + } + break;} + + case AST_VAR: + return true; + + default: + break; + } + return false; + } + + static void split_cond_guard(app *cond, expr_ref& guard, expr_ref& leftover, const table_information& t) { + expr_ref_vector guards(guard.m()); + expr_ref_vector leftovers(leftover.m()); + + if (is_app(cond) && to_app(cond)->get_decl_kind() == OP_AND) { + app *a = to_app(cond); + for (unsigned i = 0; i < a->get_num_args(); ++i) { + expr *arg = a->get_arg(i); + if (cond_is_guard(arg, t)) { + guards.push_back(arg); + } else { + leftovers.push_back(arg); + } + } + } else if (cond_is_guard(cond, t)) { + guard = cond; + return; + } else { + leftover = cond; + return; + } + + if (guards.size() > 1) { + guard = formula_to_dnf(expr_ref(guard.m().mk_and(guards.size(), guards.c_ptr()), guard.m())); + } else if (guards.size() == 1) { + guard = guards.get(0); + } + + if (leftovers.size() > 1) { + leftover = formula_to_dnf(expr_ref(leftover.m().mk_and(leftovers.size(), leftovers.c_ptr()), leftover.m())); + } else if (leftovers.size() == 1) { + leftover = leftovers.get(0); + } + } + + class filter_fn : public table_mutator_fn { + expr_ref m_condition; + typename T::bitset_t m_filter; + bit_vector m_empty_bv; + public: + filter_fn(const T & t, ast_manager& m, app *condition) : + m_condition(m), m_filter(t.get_num_bits(), true) { + m_empty_bv.resize(t.get_num_bits(), false); + + expr_ref guard(m); + split_cond_guard(condition, guard, m_condition, t); + if (guard) + m_filter.filter(guard, m_empty_bv, t); + } + + virtual void operator()(table_base & tb) { + T & t = static_cast(tb); + // first apply guard and then run the interpreter on the leftover + t.m_bitsets.swap(m_filter.and(t.m_bitsets)); + if (m_condition) + t.m_bitsets.filter(m_condition, m_empty_bv, t); + TRACE("dl_hassel", tout << "final size: " << t.get_size_estimate_rows() << '\n';); + } + }; + + public: + virtual table_mutator_fn * mk_filter_interpreted_fn(const table_base & t, app * condition) { + if (!check_kind(t)) + return 0; + TRACE("dl_hassel", tout << mk_pp(condition, get_ast_manager()) << '\n';); + return alloc(filter_fn, static_cast(t), get_ast_manager(), condition); + } + + private: + class filter_proj_fn : public convenient_table_project_fn { + expr_ref m_condition; + typename T::bitset_t m_filter; + bit_vector m_col_list; // map: col idx -> bool (whether the column is to be removed) + public: + filter_proj_fn(const T & t, ast_manager& m, app *condition, + unsigned col_cnt, const unsigned * removed_cols) : + convenient_table_project_fn(t.get_signature(), col_cnt, removed_cols), + m_condition(m), m_filter(t.get_num_bits(), true) { + t.expand_column_vector(m_removed_cols); + + m_col_list.resize(t.get_num_bits(), false); + for (unsigned i = 0; i < m_removed_cols.size(); ++i) { + m_col_list.set(m_removed_cols[i]); + } + m_removed_cols.push_back(UINT_MAX); + + expr_ref guard(m); + split_cond_guard(condition, guard, m_condition, t); + if (guard) + m_filter.filter(guard, m_col_list, t); + } + + virtual table_base* operator()(const table_base & tb) { + const T & t = static_cast(tb); + // first apply guard and then run the interpreter on the leftover + typename T::bitset_t filtered(t.get_num_bits()); + filtered.swap(m_filter.and(t.m_bitsets)); + if (m_condition) + filtered.filter(m_condition, m_col_list, t); + + T * res = static_cast(t.get_plugin().mk_empty(get_result_signature())); + filtered.project(m_removed_cols, res->m_bitsets); + TRACE("dl_hassel", tout << "final size: " << res->get_size_estimate_rows() << '\n';); + return res; + } + }; + + public: + virtual table_transformer_fn * mk_filter_interpreted_and_project_fn(const table_base & t, app * condition, + unsigned removed_col_cnt, const unsigned * removed_cols) { + if (!check_kind(t)) + return 0; + TRACE("dl_hassel", tout << mk_pp(condition, get_ast_manager()) << '\n';); + return alloc(filter_proj_fn, static_cast(t), get_ast_manager(), + condition, removed_col_cnt, removed_cols); + } + + + virtual table_intersection_filter_fn * mk_filter_by_negation_fn(const table_base & t, + const table_base & negated_obj, unsigned joined_col_cnt, const unsigned * t_cols, + const unsigned * negated_cols) { + NOT_IMPLEMENTED_YET(); + } + }; + + template + class common_hassel_table : public table_base, public table_information { + public: + typedef T bitset_t; + + common_hassel_table(table_plugin & p, const table_signature & sig) : + table_base(p, sig), table_information(p, sig), m_bitsets(get_num_bits()) { } + + virtual table_base * complement(func_decl* p, const table_element * func_columns = 0) const { + SASSERT(!func_columns); + + if (empty()) + return get_plugin().mk_full(p, get_signature()); + + common_hassel_table *res = static_cast(get_plugin().mk_empty(get_signature())); + res->m_bitsets.swap(m_bitsets.neg()); + return res; + } + + virtual void add_fact(const table_fact & f) { + m_bitsets.add_fact(ternary_bitvector(f, *this)); + } + + virtual void add_new_fact(const table_fact & f) { + m_bitsets.add_new_fact(ternary_bitvector(f, *this)); + } + + virtual void remove_fact(table_element const* fact) { + NOT_IMPLEMENTED_YET(); + } + + virtual void reset() { + m_bitsets.reset(); + } + + void mk_full() { + m_bitsets.mk_full(); + } + + virtual table_base * clone() const { + common_hassel_table *res = static_cast(get_plugin().mk_empty(get_signature())); + res->m_bitsets = m_bitsets; + return res; + } + + virtual bool contains_fact(const table_fact & f) { + return m_bitsets.contains(ternary_bitvector(f, *this)); + } + + virtual bool empty() const { + return m_bitsets.empty(); + } + +#if Z3DEBUG + class our_iterator_core : public iterator_core { + class our_row : public row_interface { + const our_iterator_core & m_parent; + const table_information& m_table; + public: + our_row(const common_hassel_table & t, const our_iterator_core & parent) : + row_interface(t), m_parent(parent), m_table(t) {} + + virtual table_element operator[](unsigned col) const { + return m_parent.it->to_number(m_table.column_idx(col), m_table.column_num_bits(col)); + } + }; + + our_row m_row_obj; + std::set BVs; + std::set::iterator it; + + public: + our_iterator_core(const common_hassel_table & t, bool finished) : + m_row_obj(t, *this) { + if (finished) { + it = BVs.end(); + return; + } + t.m_bitsets.expand(BVs); + it = BVs.begin(); + } + + virtual bool is_finished() const { + return it == BVs.end(); + } + + virtual row_interface & operator*() { + SASSERT(!is_finished()); + return m_row_obj; + } + + virtual void operator++() { + SASSERT(!is_finished()); + ++it; + } + }; +#endif + + virtual iterator begin() const { +#if Z3DEBUG + return mk_iterator(alloc(our_iterator_core, *this, false)); +#else + SASSERT(0 && "begin() disabled"); + return mk_iterator(0); +#endif + } + + virtual iterator end() const { +#if Z3DEBUG + return mk_iterator(alloc(our_iterator_core, *this, true)); +#else + SASSERT(0 && "end() disabled"); + return mk_iterator(0); +#endif + } + + virtual void display(std::ostream & out) const { + table_information::display(out); + m_bitsets.display(out); + } + + virtual void to_formula(relation_signature const& sig, expr_ref& fml) const { + // TODO + } + + virtual unsigned get_size_estimate_rows() const { + return m_bitsets.num_disjs(); + } + + virtual unsigned get_size_estimate_bytes() const { + return m_bitsets.num_bytes(); + } + + T m_bitsets; + }; + +} + +#endif diff --git a/src/muz_qe/dl_hassel_diff_table.cpp b/src/muz_qe/dl_hassel_diff_table.cpp new file mode 100755 index 000000000..3ddcb3bbe --- /dev/null +++ b/src/muz_qe/dl_hassel_diff_table.cpp @@ -0,0 +1,219 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + dl_hassel_diff_table.cpp + +Abstract: + + + +Revision History: + +--*/ + +#include "ast_printer.h" +#include "dl_context.h" +#include "dl_util.h" +#include "dl_hassel_diff_table.h" + + +namespace datalog { + + ternary_diff_bitvector::ternary_diff_bitvector(unsigned size, bool full) : + m_pos(size, full), m_neg(size) { } + + ternary_diff_bitvector::ternary_diff_bitvector(uint64 n, unsigned num_bits) : + m_pos(n, num_bits), m_neg(num_bits) { } + + ternary_diff_bitvector::ternary_diff_bitvector(const ternary_bitvector & tbv) : + m_pos(tbv), m_neg(tbv.size()) { } + + bool ternary_diff_bitvector::contains(const ternary_diff_bitvector & other) const { + return m_pos.contains(other.m_pos) && other.m_neg.contains(m_neg); + } + + bool ternary_diff_bitvector::is_empty() const { + if (m_pos.is_empty()) + return true; + + return m_neg.contains(m_pos); + } + + ternary_diff_bitvector ternary_diff_bitvector::and(const ternary_diff_bitvector& other) const { + ternary_diff_bitvector result(m_pos.and(other.m_pos)); + result.m_neg.swap(m_neg.or(other.m_neg)); + return result; + } + + void ternary_diff_bitvector::neg(union_ternary_bitvector& result) const { + // not(A\B) <-> (T\A) U B + ternary_diff_bitvector negated(size(), true); + negated.m_neg.add_new_fact(m_pos); + result.add_fact(negated); + + for (union_ternary_bitvector::const_iterator I = m_neg.begin(), + E = m_neg.end(); I != E; ++I) { + result.add_fact(*I); + } + } + + void ternary_diff_bitvector::subtract(const union_ternary_bitvector& other, + union_ternary_bitvector& result) const { + ternary_diff_bitvector newfact(*this); + for (union_ternary_bitvector::const_iterator I = other.begin(), + E = other.end(); I != E; ++I) { + if (!I->m_neg.empty()) { + NOT_IMPLEMENTED_YET(); + } + newfact.m_neg.add_fact(I->m_pos); + } + + if (!newfact.is_empty()) + result.add_fact(newfact); + } + + void ternary_diff_bitvector::join(const ternary_diff_bitvector& other, + const unsigned_vector& cols1, + const unsigned_vector& cols2, + union_ternary_bitvector& result) const { + unsigned new_size = size() + other.size(); + ternary_diff_bitvector res(new_size); + + res.m_pos = m_pos; + res.m_pos.append(other.m_pos); + + for (unsigned i = 0; i < cols1.size(); ++i) { + unsigned idx1 = cols1[i]; + unsigned idx2 = size() + cols2[i]; + unsigned v1 = res.m_pos.get(idx1); + unsigned v2 = res.m_pos.get(idx2); + + if (v1 == BIT_x) { + if (v2 == BIT_x) { + // add to subtracted TBVs: 1xx0 and 0xx1 + { + ternary_bitvector r(new_size, true); + r.set(idx1, BIT_0); + r.set(idx2, BIT_1); + res.m_neg.add_new_fact(r); + } + { + ternary_bitvector r(new_size, true); + r.set(idx1, BIT_1); + r.set(idx2, BIT_0); + res.m_neg.add_new_fact(r); + } + } else { + res.m_pos.set(idx1, v2); + } + } else if (v2 == BIT_x) { + res.m_pos.set(idx2, v1); + } else if (v1 != v2) { + // columns don't match + return; + } + } + + // handle subtracted TBVs: 1010 -> 1010xxx + if (!m_neg.empty()) { + ternary_bitvector padding(other.size(), true); + for (union_ternary_bitvector::const_iterator I = m_neg.begin(), + E = m_neg.end(); I != E; ++I) { + ternary_bitvector BV(*I); + BV.append(padding); + res.m_neg.add_new_fact(BV); + } + } + + if (!other.m_neg.empty()) { + ternary_bitvector padding(size(), true); + for (union_ternary_bitvector::const_iterator I = other.m_neg.begin(), + E = other.m_neg.end(); I != E; ++I) { + ternary_bitvector BV(padding); + BV.append(*I); + res.m_neg.add_new_fact(BV); + } + } + + result.add_fact(res); + } + + bool ternary_diff_bitvector::project(const unsigned_vector& delcols, ternary_diff_bitvector& result) const { + m_pos.project(delcols, result.m_pos); + if (m_neg.empty()) + return true; + + ternary_bitvector newneg; + for (union_ternary_bitvector::const_iterator I = m_neg.begin(), + E = m_neg.end(); I != E; ++I) { + for (unsigned i = 0; i < delcols.size()-1; ++i) { + unsigned idx = delcols[i]; + if (I->get(idx) != BIT_x && m_pos.get(idx) == BIT_x) + goto skip_row; + } + newneg.reset(); + I->project(delcols, newneg); + result.m_neg.add_fact(newneg); +skip_row: ; + } + return !result.is_empty(); + } + + void ternary_diff_bitvector::rename(const unsigned_vector& cyclecols, + const unsigned_vector& out_of_cycle_cols, + const table_information& src_table, + const table_information& dst_table, + ternary_diff_bitvector& result) const { + m_pos.rename(cyclecols, out_of_cycle_cols, src_table, dst_table, result.m_pos); + m_neg.rename(cyclecols, out_of_cycle_cols, src_table, dst_table, result.m_neg); + } + + unsigned ternary_diff_bitvector::get(unsigned idx) { + return m_pos.get(idx); + } + + void ternary_diff_bitvector::set(unsigned idx, unsigned val) { + m_pos.set(idx, val); + } + + void ternary_diff_bitvector::swap(ternary_diff_bitvector & other) { + m_pos.swap(other.m_pos); + m_neg.swap(other.m_neg); + } + + void ternary_diff_bitvector::reset() { + m_pos.reset(); + m_neg.reset(); + } + + void ternary_diff_bitvector::display(std::ostream & out) const { + m_pos.display(out); + if (!m_neg.empty()) { + out << " \\ "; + if (m_neg.num_disjs() > 1) out << '('; + m_neg.display(out); + if (m_neg.num_disjs() > 1) out << ')'; + } + } + + unsigned ternary_diff_bitvector::size_in_bytes() const { + return m_pos.size_in_bytes() + m_neg.num_bytes(); + } + +#if Z3DEBUG + void ternary_diff_bitvector::expand(std::set & BVs) const { + m_pos.expand(BVs); + SASSERT(!BVs.empty()); + + std::set NegBVs; + m_neg.expand(NegBVs); + BVs.erase(NegBVs.begin(), NegBVs.end()); + } +#endif + + hassel_diff_table_plugin::hassel_diff_table_plugin(relation_manager & manager) + : common_hassel_table_plugin(symbol("hassel_diff"), manager) {} + +} diff --git a/src/muz_qe/dl_hassel_diff_table.h b/src/muz_qe/dl_hassel_diff_table.h new file mode 100755 index 000000000..07340c7e8 --- /dev/null +++ b/src/muz_qe/dl_hassel_diff_table.h @@ -0,0 +1,87 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + dl_hassel_diff_table.h + +Abstract: + + + +Revision History: + +--*/ + +#ifndef _DL_HASSEL_DIFF_TABLE_H_ +#define _DL_HASSEL_DIFF_TABLE_H_ + +#include "dl_hassel_common.h" + +namespace datalog { + + class hassel_diff_table; + + class ternary_diff_bitvector { + // pos \ (neg0 \/ ... \/ negn) + ternary_bitvector m_pos; + union_ternary_bitvector m_neg; + + public: + ternary_diff_bitvector() : m_pos(), m_neg(0) {} + ternary_diff_bitvector(unsigned size) : m_pos(size), m_neg(size) {} + ternary_diff_bitvector(unsigned size, bool full); + ternary_diff_bitvector(uint64 n, unsigned num_bits); + ternary_diff_bitvector(const ternary_bitvector & tbv); + + bool contains(const ternary_diff_bitvector & other) const; + bool is_empty() const; + + ternary_diff_bitvector and(const ternary_diff_bitvector& other) const; + void neg(union_ternary_bitvector& result) const; + + static bool has_subtract() { return true; } + void subtract(const union_ternary_bitvector& other, + union_ternary_bitvector& result) const; + + void join(const ternary_diff_bitvector& other, const unsigned_vector& cols1, + const unsigned_vector& cols2, union_ternary_bitvector& result) const; + + bool project(const unsigned_vector& delcols, ternary_diff_bitvector& result) const; + + void rename(const unsigned_vector& cyclecols, const unsigned_vector& out_of_cycle_cols, + const table_information& src_table, const table_information& dst_table, + ternary_diff_bitvector& result) const; + + unsigned get(unsigned idx); + void set(unsigned idx, unsigned val); + + void swap(ternary_diff_bitvector & other); + void reset(); + + unsigned size() const { return m_pos.size(); } + + void display(std::ostream & out) const; + unsigned size_in_bytes() const; + +#if Z3DEBUG + void expand(std::set & BVs) const; +#endif + }; + + typedef union_ternary_bitvector union_ternary_diff_bitvector; + + class hassel_diff_table : public common_hassel_table { + public: + hassel_diff_table(table_plugin & p, const table_signature & sig) : + common_hassel_table(p, sig) {} + }; + + class hassel_diff_table_plugin : public common_hassel_table_plugin { + public: + hassel_diff_table_plugin(relation_manager & manager); + }; + +} + +#endif diff --git a/src/muz_qe/dl_hassel_table.cpp b/src/muz_qe/dl_hassel_table.cpp new file mode 100644 index 000000000..6ec28df87 --- /dev/null +++ b/src/muz_qe/dl_hassel_table.cpp @@ -0,0 +1,27 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + dl_hassel_table.cpp + +Abstract: + + + +Revision History: + +--*/ + +#include "ast_printer.h" +#include "dl_context.h" +#include "dl_util.h" +#include "dl_hassel_table.h" + + +namespace datalog { + + hassel_table_plugin::hassel_table_plugin(relation_manager & manager) + : common_hassel_table_plugin(symbol("hassel"), manager) {} + +} diff --git a/src/muz_qe/dl_hassel_table.h b/src/muz_qe/dl_hassel_table.h new file mode 100644 index 000000000..6c4e9c1fe --- /dev/null +++ b/src/muz_qe/dl_hassel_table.h @@ -0,0 +1,39 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + dl_hassel_table.h + +Abstract: + + + +Revision History: + +--*/ + +#ifndef _DL_HASSEL_TABLE_H_ +#define _DL_HASSEL_TABLE_H_ + +#include "dl_hassel_common.h" + +namespace datalog { + + class hassel_table; + typedef union_ternary_bitvector union_ternary_bitvectors; + + class hassel_table : public common_hassel_table { + public: + hassel_table(table_plugin & p, const table_signature & sig) : + common_hassel_table(p, sig) {} + }; + + class hassel_table_plugin : public common_hassel_table_plugin { + public: + hassel_table_plugin(relation_manager & manager); + }; + +} + +#endif diff --git a/src/muz_qe/dl_instruction.cpp b/src/muz_qe/dl_instruction.cpp index b103d743e..6b16968c2 100644 --- a/src/muz_qe/dl_instruction.cpp +++ b/src/muz_qe/dl_instruction.cpp @@ -526,6 +526,64 @@ namespace datalog { return alloc(instr_filter_interpreted, reg, condition); } + class instr_filter_interpreted_and_project : public instruction { + reg_idx m_src; + reg_idx m_res; + app_ref m_cond; + unsigned_vector m_cols; + public: + instr_filter_interpreted_and_project(reg_idx src, app_ref & condition, + unsigned col_cnt, const unsigned * removed_cols, reg_idx result) + : m_src(src), m_cond(condition), m_cols(col_cnt, removed_cols), + m_res(result) {} + + virtual bool perform(execution_context & ctx) { + if (!ctx.reg(m_src)) { + ctx.make_empty(m_res); + return true; + } + + relation_transformer_fn * fn; + relation_base & reg = *ctx.reg(m_src); + if (!find_fn(reg, fn)) { + fn = reg.get_manager().mk_filter_interpreted_and_project_fn(reg, m_cond, m_cols.size(), m_cols.c_ptr()); + if (!fn) { + throw default_exception( + "trying to perform unsupported filter_interpreted_and_project operation on a relation of kind %s", + reg.get_plugin().get_name().bare_str()); + } + store_fn(reg, fn); + } + + ctx.set_reg(m_res, (*fn)(reg)); + + if (ctx.eager_emptiness_checking() && ctx.reg(m_res)->empty()) { + ctx.make_empty(m_res); + } + return true; + } + + virtual void display_head_impl(rel_context const& ctx, std::ostream & out) const { + out << "filter_interpreted_and_project " << m_src << " into " << m_res; + out << " using " << mk_pp(m_cond, m_cond.get_manager()); + out << " deleting columns "; + print_container(m_cols, out); + } + + virtual void make_annotations(execution_context & ctx) { + std::stringstream s; + std::string a = "rel_src"; + ctx.get_register_annotation(m_src, a); + s << "filter_interpreted_and_project " << mk_pp(m_cond, m_cond.get_manager()); + ctx.set_register_annotation(m_res, s.str()); + } + }; + + instruction * instruction::mk_filter_interpreted_and_project(reg_idx reg, app_ref & condition, + unsigned col_cnt, const unsigned * removed_cols, reg_idx result) { + return alloc(instr_filter_interpreted_and_project, reg, condition, col_cnt, removed_cols, result); + } + class instr_union : public instruction { reg_idx m_src; @@ -592,6 +650,7 @@ namespace datalog { } } + SASSERT(r_src.get_signature().size() == r_tgt.get_signature().size()); TRACE("dl_verbose", r_tgt.display(tout <<"pre-union:");); (*fn)(r_tgt, r_src, r_delta); diff --git a/src/muz_qe/dl_instruction.h b/src/muz_qe/dl_instruction.h index ae6310ba6..97622c6f3 100644 --- a/src/muz_qe/dl_instruction.h +++ b/src/muz_qe/dl_instruction.h @@ -260,6 +260,8 @@ namespace datalog { static instruction * mk_filter_equal(ast_manager & m, reg_idx reg, const relation_element & value, unsigned col); static instruction * mk_filter_identical(reg_idx reg, unsigned col_cnt, const unsigned * identical_cols); static instruction * mk_filter_interpreted(reg_idx reg, app_ref & condition); + static instruction * mk_filter_interpreted_and_project(reg_idx src, app_ref & condition, + unsigned col_cnt, const unsigned * removed_cols, reg_idx result); static instruction * mk_union(reg_idx src, reg_idx tgt, reg_idx delta); static instruction * mk_widen(reg_idx src, reg_idx tgt, reg_idx delta); static instruction * mk_projection(reg_idx src, unsigned col_cnt, const unsigned * removed_cols, diff --git a/src/muz_qe/dl_relation_manager.cpp b/src/muz_qe/dl_relation_manager.cpp index 986a1f2c4..ce20961f1 100644 --- a/src/muz_qe/dl_relation_manager.cpp +++ b/src/muz_qe/dl_relation_manager.cpp @@ -720,6 +720,13 @@ namespace datalog { return t.get_plugin().mk_filter_interpreted_fn(t, condition); } + relation_transformer_fn * relation_manager::mk_filter_interpreted_and_project_fn(const relation_base & t, + app * condition, + unsigned removed_col_cnt, + const unsigned * removed_cols) { + return t.get_plugin().mk_filter_interpreted_and_project_fn(t, condition, removed_col_cnt, removed_cols); + } + class relation_manager::default_relation_select_equal_and_project_fn : public relation_transformer_fn { scoped_ptr m_filter; @@ -1387,6 +1394,45 @@ namespace datalog { } + class relation_manager::default_table_filter_interpreted_and_project_fn + : public table_transformer_fn { + scoped_ptr m_filter; + scoped_ptr m_project; + app_ref m_condition; + unsigned_vector m_removed_cols; + public: + default_table_filter_interpreted_and_project_fn(context & ctx, table_mutator_fn * filter, + app * condition, unsigned removed_col_cnt, const unsigned * removed_cols) + : m_filter(filter), m_condition(condition, ctx.get_manager()), + m_removed_cols(removed_col_cnt, removed_cols) {} + + virtual table_base* operator()(const table_base & tb) { + table_base *t2 = tb.clone(); + (*m_filter)(*t2); + if (!m_project) { + relation_manager & rmgr = t2->get_plugin().get_manager(); + m_project = rmgr.mk_project_fn(*t2, m_removed_cols.size(), m_removed_cols.c_ptr()); + if (!m_project) { + throw default_exception("projection does not exist"); + } + } + return (*m_project)(*t2); + } + }; + + table_transformer_fn * relation_manager::mk_filter_interpreted_and_project_fn(const table_base & t, + app * condition, unsigned removed_col_cnt, const unsigned * removed_cols) { + table_transformer_fn * res = t.get_plugin().mk_filter_interpreted_and_project_fn(t, condition, removed_col_cnt, removed_cols); + if (res) + return res; + + table_mutator_fn * filter = mk_filter_interpreted_fn(t, condition); + SASSERT(filter); + res = alloc(default_table_filter_interpreted_and_project_fn, get_context(), filter, condition, removed_col_cnt, removed_cols); + return res; + } + + table_intersection_filter_fn * relation_manager::mk_filter_by_intersection_fn(const table_base & t, const table_base & src, unsigned joined_col_cnt, const unsigned * t_cols, const unsigned * src_cols) { table_intersection_filter_fn * res = t.get_plugin().mk_filter_by_negation_fn(t, src, joined_col_cnt, diff --git a/src/muz_qe/dl_relation_manager.h b/src/muz_qe/dl_relation_manager.h index f22ae7923..ccdba2783 100644 --- a/src/muz_qe/dl_relation_manager.h +++ b/src/muz_qe/dl_relation_manager.h @@ -55,6 +55,7 @@ namespace datalog { class default_table_filter_equal_fn; class default_table_filter_identical_fn; class default_table_filter_interpreted_fn; + class default_table_filter_interpreted_and_project_fn; class default_table_negation_filter_fn; class default_table_filter_not_equal_fn; class default_table_select_equal_and_project_fn; @@ -350,6 +351,9 @@ namespace datalog { relation_mutator_fn * mk_filter_interpreted_fn(const relation_base & t, app * condition); + relation_transformer_fn * mk_filter_interpreted_and_project_fn(const relation_base & t, app * condition, + unsigned removed_col_cnt, const unsigned * removed_cols); + /** \brief Operations that returns all rows of \c t for which is column \c col equal to \c value with the column \c col removed. @@ -522,6 +526,9 @@ namespace datalog { table_mutator_fn * mk_filter_interpreted_fn(const table_base & t, app * condition); + table_transformer_fn * mk_filter_interpreted_and_project_fn(const table_base & t, app * condition, + unsigned removed_col_cnt, const unsigned * removed_cols); + /** \brief Operations that returns all rows of \c t for which is column \c col equal to \c value with the column \c col removed. diff --git a/src/muz_qe/dl_table_relation.cpp b/src/muz_qe/dl_table_relation.cpp index fc661366d..3c30c58bb 100644 --- a/src/muz_qe/dl_table_relation.cpp +++ b/src/muz_qe/dl_table_relation.cpp @@ -354,6 +354,21 @@ namespace datalog { return alloc(tr_mutator_fn, tfun); } + relation_transformer_fn * table_relation_plugin::mk_filter_interpreted_and_project_fn(const relation_base & t, + app * condition, unsigned removed_col_cnt, const unsigned * removed_cols) { + if (!t.from_table()) + return 0; + + const table_relation & tr = static_cast(t); + table_transformer_fn * tfun = get_manager().mk_filter_interpreted_and_project_fn(tr.get_table(), + condition, removed_col_cnt, removed_cols); + SASSERT(tfun); + + relation_signature sig; + relation_signature::from_project(t.get_signature(), removed_col_cnt, removed_cols, sig); + return alloc(tr_transformer_fn, sig, tfun); + } + class table_relation_plugin::tr_intersection_filter_fn : public relation_intersection_filter_fn { scoped_ptr m_tfun; public: diff --git a/src/muz_qe/dl_table_relation.h b/src/muz_qe/dl_table_relation.h index 12f0d4eaa..f86143c0f 100644 --- a/src/muz_qe/dl_table_relation.h +++ b/src/muz_qe/dl_table_relation.h @@ -71,6 +71,8 @@ namespace datalog { virtual relation_mutator_fn * mk_filter_equal_fn(const relation_base & t, const relation_element & value, unsigned col); virtual relation_mutator_fn * mk_filter_interpreted_fn(const relation_base & t, app * condition); + virtual relation_transformer_fn * mk_filter_interpreted_and_project_fn(const relation_base & t, + app * condition, unsigned removed_col_cnt, const unsigned * removed_cols); virtual relation_intersection_filter_fn * mk_filter_by_intersection_fn(const relation_base & t, const relation_base & src, unsigned joined_col_cnt, const unsigned * t_cols, const unsigned * src_cols); virtual relation_intersection_filter_fn * mk_filter_by_negation_fn(const relation_base & t, diff --git a/src/muz_qe/rel_context.cpp b/src/muz_qe/rel_context.cpp index 63e8ba700..3d61c04f0 100644 --- a/src/muz_qe/rel_context.cpp +++ b/src/muz_qe/rel_context.cpp @@ -18,6 +18,9 @@ Revision History: Extracted from dl_context --*/ + +#define Z3_HASSEL_TABLE + #include"rel_context.h" #include"dl_context.h" #include"dl_compiler.h" @@ -30,6 +33,10 @@ Revision History: #include"dl_mk_karr_invariants.h" #include"dl_finite_product_relation.h" #include"dl_sparse_table.h" +#ifdef Z3_HASSEL_TABLE +# include"dl_hassel_table.h" +# include"dl_hassel_diff_table.h" +#endif #include"dl_table.h" #include"dl_table_relation.h" #include"aig_exporter.h" @@ -87,6 +94,10 @@ namespace datalog { get_rmanager().register_plugin(alloc(bitvector_table_plugin, get_rmanager())); get_rmanager().register_plugin(alloc(equivalence_table_plugin, get_rmanager())); +#ifdef Z3_HASSEL_TABLE + get_rmanager().register_plugin(alloc(hassel_table_plugin, get_rmanager())); + get_rmanager().register_plugin(alloc(hassel_diff_table_plugin, get_rmanager())); +#endif // register plugins for builtin relations diff --git a/src/util/bit_vector.h b/src/util/bit_vector.h index 2c641c5a6..cbe7a0618 100644 --- a/src/util/bit_vector.h +++ b/src/util/bit_vector.h @@ -28,6 +28,7 @@ COMPILE_TIME_ASSERT(sizeof(unsigned) == 4); #define BV_DEFAULT_CAPACITY 2 class bit_vector { +protected: unsigned m_num_bits; unsigned m_capacity; //!< in words unsigned * m_data; @@ -64,6 +65,12 @@ public: m_data(0) { } + bit_vector(unsigned reserve_num_bits) : + m_num_bits(0), + m_capacity(num_words(reserve_num_bits)), + m_data(alloc_svect(unsigned, m_capacity)) { + } + bit_vector(bit_vector const & source): m_num_bits(source.m_num_bits), m_capacity(source.m_capacity), From 60c4973c1d133993dbfd15f2052dd95dbc892f21 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 29 May 2013 17:56:23 -0700 Subject: [PATCH 26/26] fix crash in proof generation in BMC Signed-off-by: Nikolaj Bjorner --- src/muz_qe/dl_bmc_engine.cpp | 30 +++++++++++++++++++++++------- 1 file changed, 23 insertions(+), 7 deletions(-) diff --git a/src/muz_qe/dl_bmc_engine.cpp b/src/muz_qe/dl_bmc_engine.cpp index c313f7d7b..8e9fb510e 100644 --- a/src/muz_qe/dl_bmc_engine.cpp +++ b/src/muz_qe/dl_bmc_engine.cpp @@ -297,6 +297,7 @@ namespace datalog { r->to_formula(fml); r2 = r; rm.substitute(r2, sub.size(), sub.c_ptr()); + proof_ref p(m); if (r0) { VERIFY(unifier.unify_rules(*r0.get(), 0, *r2.get())); expr_ref_vector sub1 = unifier.get_rule_subst(*r0.get(), true); @@ -306,7 +307,10 @@ namespace datalog { r1->to_formula(concl); scoped_proof _sp(m); - proof* p = r->get_proof(); + p = r->get_proof(); + if (!p) { + p = m.mk_asserted(fml); + } proof* premises[2] = { pr, p }; positions.push_back(std::make_pair(0, 1)); @@ -319,13 +323,17 @@ namespace datalog { else { r2->to_formula(concl); scoped_proof _sp(m); - proof* p = r->get_proof(); + p = r->get_proof(); + if (!p) { + p = m.mk_asserted(fml); + } if (sub.empty()) { pr = p; } else { substs.push_back(sub); - pr = m.mk_hyper_resolve(1, &p, concl, positions, substs); + proof* ps[1] = { p }; + pr = m.mk_hyper_resolve(1, ps, concl, positions, substs); } r0 = r2; } @@ -1211,6 +1219,15 @@ namespace datalog { r->to_formula(fml); r2 = r; rm.substitute(r2, sub.size(), sub.c_ptr()); + proof_ref p(m); + { + scoped_proof _sp(m); + p = r->get_proof(); + if (!p) { + p = m.mk_asserted(fml); + } + } + if (r0) { VERIFY(unifier.unify_rules(*r0.get(), 0, *r2.get())); expr_ref_vector sub1 = unifier.get_rule_subst(*r0.get(), true); @@ -1218,9 +1235,8 @@ namespace datalog { apply_subst(sub, sub2); unifier.apply(*r0.get(), 0, *r2.get(), r1); r1->to_formula(concl); - scoped_proof _sp(m); - proof* p = r->get_proof(); + scoped_proof _sp(m); proof* premises[2] = { pr, p }; positions.push_back(std::make_pair(0, 1)); @@ -1233,13 +1249,13 @@ namespace datalog { else { r2->to_formula(concl); scoped_proof _sp(m); - proof* p = r->get_proof(); if (sub.empty()) { pr = p; } else { substs.push_back(sub); - pr = m.mk_hyper_resolve(1, &p, concl, positions, substs); + proof * ps[1] = { p }; + pr = m.mk_hyper_resolve(1, ps, concl, positions, substs); } r0 = r2; }