From 7e91fb5c1527f1f930328856f472a0737e640d56 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 16 Sep 2014 22:14:58 -0700 Subject: [PATCH] remove mk_or_reduced Signed-off-by: Nikolaj Bjorner --- src/ast/ast.cpp | 7 -- src/ast/ast.h | 1 - src/muz/ddnf/doc.h | 17 ++++ src/muz/ddnf/udoc_relation.cpp | 144 +++++++--------------------- src/muz/ddnf/udoc_relation.h | 1 + src/tactic/arith/card2bv_tactic.cpp | 3 +- 6 files changed, 53 insertions(+), 120 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 95d47dc03..7dd320e06 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -2058,13 +2058,6 @@ app * ast_manager::mk_app(func_decl * decl, unsigned num_args, expr * const * ar return r; } -expr* ast_manager::mk_or_reduced(unsigned n, expr* const* args) { - switch (n) { - case 0: return mk_false(); - case 1: return args[0]; - default: return mk_or(n, args); - } -} func_decl * ast_manager::mk_fresh_func_decl(symbol const & prefix, symbol const & suffix, unsigned arity, diff --git a/src/ast/ast.h b/src/ast/ast.h index 1c4771e7f..f21f821b9 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -2004,7 +2004,6 @@ public: app * mk_true() { return m_true; } app * mk_false() { return m_false; } app * mk_interp(expr * arg) { return mk_app(m_basic_family_id, OP_INTERP, arg); } - expr * mk_or_reduced(unsigned num_args, expr * const * args); func_decl* mk_and_decl() { diff --git a/src/muz/ddnf/doc.h b/src/muz/ddnf/doc.h index 074045c95..42db3c545 100644 --- a/src/muz/ddnf/doc.h +++ b/src/muz/ddnf/doc.h @@ -157,6 +157,23 @@ public: std::swap(result, *this); result.reset(m); } + void subtract(M& m, union_bvec const& other) { + unsigned sz = other.size(); + for (unsigned i = 0; !empty() && i < sz; ++i) { + subtract(m, other[i]); + } + // TBD compress? + } + void subtract(M& m, T& t) { + unsigned sz = size(); + bool found = false; + union_bvec result; + for (unsigned i = 0; i < sz; ++i) { + m.subtract(*m_elems[i], t, result.m_elems); + } + std::swap(m_elems, result.m_elems); + result.reset(m); + } void complement(M& m, union_bvec& result) { union_bvec negated; result.reset(m); diff --git a/src/muz/ddnf/udoc_relation.cpp b/src/muz/ddnf/udoc_relation.cpp index e14e5b98c..393b85d54 100644 --- a/src/muz/ddnf/udoc_relation.cpp +++ b/src/muz/ddnf/udoc_relation.cpp @@ -444,9 +444,10 @@ namespace datalog { apply_guard(g, result, equalities, discard_cols); } void udoc_relation::apply_guard( - expr* g, udoc& result, subset_ints& equalities, - bit_vector const& discard_cols) { + expr* g, udoc& result, + subset_ints& equalities, bit_vector const& discard_cols) { ast_manager& m = get_plugin().get_ast_manager(); + bv_util& bv = get_plugin().bv; expr* e1, *e2; if (result.empty()) { } @@ -459,23 +460,17 @@ namespace datalog { udoc sub; sub.push_back(dm.allocateX()); apply_guard(e1, sub, equalities, discard_cols); - // TBD: result.subtract(dm, sub); + result.subtract(dm, sub); } else if (m.is_or(g)) { udoc sub; sub.push_back(dm.allocateX()); for (unsigned i = 0; !sub.empty() && i < to_app(g)->get_num_args(); ++i) { expr_ref arg(m); - arg = to_app(g)->get_arg(i); - if (m.is_not(arg, e1)) { - arg = e1; - } - else { - arg = m.mk_not(arg); - } + arg = mk_not(m, to_app(g)->get_arg(i)); apply_guard(arg, result, equalities, discard_cols); } - // TBD: result.subtract(dm, sub); + result.subtract(dm, sub); } else if (m.is_true(g)) { } @@ -491,37 +486,36 @@ namespace datalog { bit1 = dm1.tbv().allocate1(); result.fix_eq_bits(idx, bit1.get(), 0, 1, equalities, discard_cols); } - else if (m.is_eq(g, e1, e2)) { -#if 0 - const var *v; - unsigned vidx = 0; - unsigned length; - - unsigned low, high; - expr *e2; - if (is_var(e1)) { - v = to_var(e1); - length = column_num_bits(v->get_idx()); - } else if (bv.is_extract(e1, low, high, e11)) { - vidx = bv.get_bv_size(e11) - high - 1; - length = high - low + 1; - SASSERT(is_var(e11)); - v = to_var(e11); - } else { - NOT_IMPLEMENTED_YET(); + else if (m.is_eq(g, e1, e2) && bv.is_bv(e1)) { + unsigned hi, lo; + expr* e3; + // TBD: equalities and discard_cols? + if (is_var(e1) && is_ground(e2)) { + apply_eq(g, result, to_var(e1), bv.get_bv_size(e1)-1, 0, e2); } - vidx += t.column_idx(v->get_idx()); - - unsigned final_idx = fix_eq_bits(vidx, e2, 0, length, t, equalities, discard_cols); - SASSERT(final_idx == vidx + length); - (void)final_idx; -#endif + else if (is_var(e2) && is_ground(e1)) { + apply_eq(g, result, to_var(e2), bv.get_bv_size(e2)-1, 0, e1); + } + else if (bv.is_extract(e1, lo, hi, e3) && is_var(e3) && is_ground(e2)) { + apply_eq(g, result, to_var(e3), hi, lo, e2); + } + else if (bv.is_extract(e2, lo, hi, e3) && is_var(e3) && is_ground(e1)) { + apply_eq(g, result, to_var(e3), hi, lo, e1); + } + else if (is_var(e1) && is_var(e2)) { + var* v1 = to_var(e1); + var* v2 = to_var(e2); + // TBD + } + else { + goto failure_case; + } } else { - // std::ostringstream strm; - // strm << "Guard expression is not handled" << mk_pp(g, m); - // throw default_exception(strm.str()); - throw 0; + failure_case: + std::ostringstream strm; + strm << "Guard expression is not handled" << mk_pp(g, m); + throw default_exception(strm.str()); } } @@ -594,76 +588,4 @@ namespace datalog { return alloc(negation_filter_fn, get(t), get(neg), joined_col_cnt, t_cols, negated_cols); } -#if 0 - /// make bits of table [idx,idx+max_length] equal to e sliced starting at idx2 - unsigned fix_eq_bits(unsigned idx, 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)) { - SASSERT(idx2 < bv_size); - max_length = std::min(max_length, bv_size - idx2); - T num(n, max_length); - 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(rational(num,rational::ui64()), 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; - } -#endif - } diff --git a/src/muz/ddnf/udoc_relation.h b/src/muz/ddnf/udoc_relation.h index 6c10a62bb..197e16fb9 100644 --- a/src/muz/ddnf/udoc_relation.h +++ b/src/muz/ddnf/udoc_relation.h @@ -66,6 +66,7 @@ namespace datalog { void compile_guard(expr* g, udoc& d) const; void apply_guard(expr* g, udoc& result, bit_vector const& discard_cols); void apply_guard(expr* g, udoc& result, subset_ints& equalities, bit_vector const& discard_cols); + void apply_eq(expr* g, udoc& result, var* v, unsigned hi, unsigned lo, expr* c); }; class udoc_plugin : public relation_plugin { diff --git a/src/tactic/arith/card2bv_tactic.cpp b/src/tactic/arith/card2bv_tactic.cpp index 3d112e36f..5f9f28898 100644 --- a/src/tactic/arith/card2bv_tactic.cpp +++ b/src/tactic/arith/card2bv_tactic.cpp @@ -23,6 +23,7 @@ Notes: #include"expr_substitution.h" #include"card2bv_tactic.h" #include"pb_rewriter.h" +#include"ast_util.h" namespace pb { unsigned card2bv_rewriter::get_num_bits(func_decl* f) { @@ -85,7 +86,7 @@ namespace pb { } void card2bv_rewriter::mk_clause(unsigned n, literal const* lits) { - m_lemmas.push_back(m.mk_or_reduced(n, lits)); + m_lemmas.push_back(mk_or(m, n, lits)); }