From 65bc77d5666dccf0244fc9e3e2d264c1b8af48bf Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 3 Sep 2020 08:58:08 -0700 Subject: [PATCH] na Signed-off-by: Nikolaj Bjorner --- src/sat/sat_types.h | 2 +- src/sat/smt/bv_internalize.cpp | 143 +++++++++++++++++++++++++++++++-- src/sat/smt/bv_solver.cpp | 4 +- src/sat/smt/bv_solver.h | 9 +++ src/sat/smt/sat_th.h | 1 + 5 files changed, 149 insertions(+), 10 deletions(-) diff --git a/src/sat/sat_types.h b/src/sat/sat_types.h index 82d1c23aed4..c169892922f 100644 --- a/src/sat/sat_types.h +++ b/src/sat/sat_types.h @@ -255,8 +255,8 @@ namespace sat { class status { public: enum class st { asserted, redundant, deleted }; - int m_orig; st m_st; + int m_orig; public: status(enum st s, int o) : m_st(s), m_orig(o) {}; status(status const& s) : m_st(s.m_st), m_orig(s.m_orig) {} diff --git a/src/sat/smt/bv_internalize.cpp b/src/sat/smt/bv_internalize.cpp index 28b132a3bb5..9ee3a62f737 100644 --- a/src/sat/smt/bv_internalize.cpp +++ b/src/sat/smt/bv_internalize.cpp @@ -93,6 +93,92 @@ namespace bv { return get_enode(e) != nullptr; } + void solver::mk_bits(theory_var v) { + TRACE("bv", tout << "v" << v << "\n";); + expr* e = get_expr(v); + unsigned bv_size = get_bv_size(v); + literal_vector& bits = m_bits[v]; + bits.reset(); + for (unsigned i = 0; i < bv_size; i++) { + expr_ref b2b = mk_bit2bool(e, i); + bits.push_back(ctx.internalize(b2b, false, false, m_is_redundant)); + } + } + + expr_ref solver::mk_bit2bool(expr* e, unsigned idx) { + parameter p(idx); + expr* args[1] = { e }; + return expr_ref(m.mk_app(get_id(), OP_BIT2BOOL, 1, &p, 1, args), m); + } + +#if 0 + SASSERT(!ctx.b_internalized(n)); + + TRACE("bv", tout << "bit2bool: " << mk_pp(n, ctx.get_manager()) << "\n";); + expr* first_arg = n->get_arg(0); + + if (!ctx.e_internalized(first_arg)) { + // This may happen if bit2bool(x) is in a conflict + // clause that is being reinitialized, and x was not reinitialized + // yet. + // So, we internalize x (i.e., arg) + ctx.internalize(first_arg, false); + SASSERT(ctx.e_internalized(first_arg)); + // In most cases, when x is internalized, its bits are created. + // They are created because x is a bit-vector operation or apply_sort_cnstr is invoked. + // However, there is an exception. The method apply_sort_cnstr is not invoked for ite-terms. + // So, I execute get_var on the enode attached to first_arg. + // This will force a theory variable to be created if it does not already exist. + // This will also force the creation of all bits for x. + enode* first_arg_enode = ctx.get_enode(first_arg); + get_var(first_arg_enode); + } + + enode* arg = ctx.get_enode(first_arg); + // The argument was already internalized, but it may not have a theory variable associated with it. + // For example, for ite-terms the method apply_sort_cnstr is not invoked. + // See comment in the then-branch. + theory_var v_arg = arg->get_th_var(get_id()); + if (v_arg == null_theory_var) { + // The method get_var will create a theory variable for arg. + // As a side-effect the bits for arg will also be created. + get_var(arg); + SASSERT(ctx.b_internalized(n)); + } + else if (!ctx.b_internalized(n)) { + SASSERT(v_arg != null_theory_var); + bool_var bv = ctx.mk_bool_var(n); + ctx.set_var_theory(bv, get_id()); + bit_atom* a = new (get_region()) bit_atom(); + insert_bv2a(bv, a); + m_trail_stack.push(mk_atom_trail(bv)); + unsigned idx = n->get_decl()->get_parameter(0).get_int(); + SASSERT(a->m_occs == 0); + a->m_occs = new (get_region()) var_pos_occ(v_arg, idx); + // Fix for #2182, and SPACER bit-vector + if (idx < m_bits[v_arg].size()) { + ctx.mk_th_axiom(get_id(), m_bits[v_arg][idx], literal(bv, true)); + ctx.mk_th_axiom(get_id(), ~m_bits[v_arg][idx], literal(bv, false)); + } + } + // axiomatize bit2bool on constants. + rational val; + unsigned sz; + if (m_util.is_numeral(first_arg, val, sz)) { + rational bit; + unsigned idx = n->get_decl()->get_parameter(0).get_int(); + div(val, rational::power_of_two(idx), bit); + mod(bit, rational(2), bit); + literal lit = ctx.get_literal(n); + if (bit.is_zero()) lit.neg(); + ctx.mark_as_relevant(lit); + ctx.mk_th_axiom(get_id(), 1, &lit); + } + + } +#endif + + euf::enode * solver::mk_enode(app * n, ptr_vector const& args) { euf::enode * e = ctx.get_enode(n); if (!e) { @@ -102,6 +188,49 @@ namespace bv { return e; } + euf::theory_var solver::get_var(euf::enode* n) { + theory_var v = n->get_th_var(get_id()); + if (v == euf::null_theory_var) { + v = mk_var(n); + mk_bits(v); + } + return v; + } + + euf::enode* solver::get_arg(euf::enode* n, unsigned idx) { + if (get_config().m_bv_reflect) { + return n->get_arg(idx); + } + else { + expr* arg = n->get_arg(idx)->get_owner(); + return ctx.get_enode(arg); + } + } + + inline euf::theory_var solver::get_arg_var(euf::enode* n, unsigned idx) { + return get_var(get_arg(n, idx)); + } + + void solver::get_bits(theory_var v, expr_ref_vector& r) { + literal_vector& bits = m_bits[v]; + for (literal lit : bits) { + r.push_back(get_expr(lit)); + } + } + + inline void solver::get_bits(euf::enode* n, expr_ref_vector& r) { + get_bits(get_var(n), r); + } + + inline void solver::get_arg_bits(euf::enode* n, unsigned idx, expr_ref_vector& r) { + get_bits(get_arg_var(n, idx), r); + } + + inline void solver::get_arg_bits(app* n, unsigned idx, expr_ref_vector& r) { + app* arg = to_app(n->get_arg(idx)); + get_bits(ctx.get_enode(arg), r); + } + void solver::register_true_false_bit(theory_var v, unsigned idx) { SASSERT(s().value(m_bits[v][idx]) != l_undef); bool is_true = (s().value(m_bits[v][idx]) == l_true); @@ -123,18 +252,18 @@ namespace bv { atom * a = get_bv2a(l.var()); SASSERT(!a || a->is_bit()); if (a) { - bit_atom * b = new (get_region()) bit_atom(); + bit_atom* b = static_cast(a); + find_new_diseq_axioms(b->m_occs, v, idx); + ctx.push(add_var_pos_trail(b)); + b->m_occs = new (get_region()) var_pos_occ(v, idx, b->m_occs); + } + else { + bit_atom* b = new (get_region()) bit_atom(); insert_bv2a(l.var(), b); ctx.push(mk_atom_trail(l.var(), *this)); SASSERT(b->m_occs == 0); b->m_occs = new (get_region()) var_pos_occ(v, idx); } - else { - bit_atom * b = static_cast(a); - find_new_diseq_axioms(b->m_occs, v, idx); - ctx.push(add_var_pos_trail(b)); - b->m_occs = new (get_region()) var_pos_occ(v, idx, b->m_occs); - } } } diff --git a/src/sat/smt/bv_solver.cpp b/src/sat/smt/bv_solver.cpp index f8469f7beca..d033d565f3a 100644 --- a/src/sat/smt/bv_solver.cpp +++ b/src/sat/smt/bv_solver.cpp @@ -81,8 +81,8 @@ namespace bv { TRACE("bv_solver", tout << "found new diseq axiom\n" << pp(v1) << pp(v2);); m_stats.m_num_diseq_static++; expr_ref eq(m.mk_eq(get_expr(v1), get_expr(v2)), m); - sat::literal not_eq = ctx.internalize(eq, true, false, m_is_redundant); - s().add_clause(1, ¬_eq, sat::status::th(m_is_redundant, get_id())); + sat::literal neq = ctx.internalize(eq, true, false, m_is_redundant); + s().add_clause(1, &neq, sat::status::th(m_is_redundant, get_id())); } std::ostream& solver::display(std::ostream& out, theory_var v) const { diff --git a/src/sat/smt/bv_solver.h b/src/sat/smt/bv_solver.h index b0c101ad47d..4a926dbe086 100644 --- a/src/sat/smt/bv_solver.h +++ b/src/sat/smt/bv_solver.h @@ -124,11 +124,20 @@ namespace bv { bool post_visit(expr* e, bool sign, bool root) override; unsigned get_bv_size(euf::enode* n); unsigned get_bv_size(theory_var v); + theory_var get_var(euf::enode* n); + euf::enode* get_arg(euf::enode* n, unsigned idx); + inline theory_var get_arg_var(euf::enode* n, unsigned idx); + void get_bits(theory_var v, expr_ref_vector& r); + void get_bits(euf::enode* n, expr_ref_vector& r); + void get_arg_bits(euf::enode* n, unsigned idx, expr_ref_vector& r); + void get_arg_bits(app* n, unsigned idx, expr_ref_vector& r); euf::enode* mk_enode(app* n, ptr_vector const& args); void fixed_var_eh(theory_var v); void register_true_false_bit(theory_var v, unsigned i); void add_bit(theory_var v, sat::literal lit); void init_bits(euf::enode * n, expr_ref_vector const & bits); + void mk_bits(theory_var v); + expr_ref mk_bit2bool(expr* b, unsigned idx); void internalize_num(app * n, theory_var v); void internalize_add(app * n); void internalize_sub(app * n); diff --git a/src/sat/smt/sat_th.h b/src/sat/smt/sat_th.h index 7770009c582..987bc8dc6c7 100644 --- a/src/sat/smt/sat_th.h +++ b/src/sat/smt/sat_th.h @@ -114,6 +114,7 @@ namespace euf { enode* get_enode(expr* e) const; enode* get_enode(theory_var v) const { return m_var2enode[v]; } expr* get_expr(theory_var v) const { return get_enode(v)->get_owner(); } + expr_ref get_expr(sat::literal lit) const { expr* e = get_expr(lit.var()); return lit.sign() ? expr_ref(m.mk_not(e), m) : expr_ref(e, m); } theory_var get_th_var(enode* n) const { return n->get_th_var(get_id()); } theory_var get_th_var(expr* e) const; bool is_attached_to_var(enode* n) const;