From 22a5687e1664be2f82f60fe166c3d2e950664584 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 31 Jul 2018 15:52:21 -0700 Subject: [PATCH] supply bits on demand Signed-off-by: Nikolaj Bjorner --- src/smt/theory_bv.cpp | 34 +++++++++++++++++++++++++++++----- src/smt/theory_bv.h | 7 ++++--- 2 files changed, 33 insertions(+), 8 deletions(-) diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index a0c62b959..cff306975 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -162,10 +162,14 @@ namespace smt { if (v == null_theory_var) { v = mk_var(n); } + ensure_bits(v); + return v; + } + + void theory_bv::ensure_bits(theory_var v) { if (m_bits[v].empty()) { mk_bits(v); } - return v; } enode * theory_bv::get_arg(enode * n, unsigned idx) { @@ -186,6 +190,7 @@ namespace smt { void theory_bv::get_bits(theory_var v, expr_ref_vector & r) { context & ctx = get_context(); + ensure_bits(v); literal_vector & bits = m_bits[v]; for (literal lit : bits) { expr_ref l(get_manager()); @@ -223,6 +228,7 @@ namespace smt { \brief v1[idx] = ~v2[idx], then v1 /= v2 is a theory axiom. */ void theory_bv::mk_new_diseq_axiom(theory_var v1, theory_var v2, unsigned idx) { + ensure_bits(v1); ensure_bits(v2); SASSERT(m_bits[v1][idx] == ~m_bits[v2][idx]); TRACE("bv_diseq_axiom", tout << "found new diseq axiom\n"; display_var(tout, v1); display_var(tout, v2);); // found new disequality @@ -241,6 +247,7 @@ namespace smt { } void theory_bv::register_true_false_bit(theory_var v, unsigned idx) { + ensure_bits(v); SASSERT(m_bits[v][idx] == true_literal || m_bits[v][idx] == false_literal); bool is_true = (m_bits[v][idx] == true_literal); zero_one_bits & bits = m_zero_one_bits[v]; @@ -251,11 +258,13 @@ namespace smt { \brief v[idx] = ~v'[idx], then v /= v' is a theory axiom. */ void theory_bv::find_new_diseq_axioms(var_pos_occ * occs, theory_var v, unsigned idx) { + ensure_bits(v); literal l = m_bits[v][idx]; l.neg(); while (occs) { theory_var v2 = occs->m_var; unsigned idx2 = occs->m_idx; + ensure_bits(v2); if (idx == idx2 && m_bits[v2][idx2] == l && get_bv_size(v2) == get_bv_size(v)) mk_new_diseq_axiom(v, v2, idx); occs = occs->m_next; @@ -267,6 +276,7 @@ namespace smt { */ void theory_bv::add_bit(theory_var v, literal l) { context & ctx = get_context(); + ensure_bits(v); literal_vector & bits = m_bits[v]; unsigned idx = bits.size(); bits.push_back(l); @@ -329,6 +339,7 @@ namespace smt { */ void theory_bv::find_wpos(theory_var v) { context & ctx = get_context(); + ensure_bits(v); literal_vector const & bits = m_bits[v]; unsigned sz = bits.size(); unsigned & wpos = m_wpos[v]; @@ -435,6 +446,7 @@ namespace smt { tout << mk_pp(o1, m) << " = " << mk_pp(o2, m) << " " << ctx.get_scope_level() << "\n";); literal_vector eqs; + ensure_bits(v1); ensure_bits(v2); for (unsigned i = 0; i < sz; ++i) { literal l1 = m_bits[v1][i]; literal l2 = m_bits[v2][i]; @@ -487,7 +499,7 @@ namespace smt { } } - bool theory_bv::get_fixed_value(theory_var v, numeral & result) const { + bool theory_bv::get_fixed_value(theory_var v, numeral & result) const { context & ctx = get_context(); result.reset(); literal_vector const & bits = m_bits[v]; @@ -844,6 +856,7 @@ namespace smt { unsigned start = n->get_decl()->get_parameter(1).get_int(); unsigned end = n->get_decl()->get_parameter(0).get_int(); SASSERT(start <= end); + ensure_bits(arg); literal_vector & arg_bits = m_bits[arg]; m_bits[v].reset(); for (unsigned i = start; i <= end; ++i) @@ -1109,6 +1122,7 @@ namespace smt { void theory_bv::new_diseq_eh(theory_var v1, theory_var v2) { if (is_bv(v1)) { + ensure_bits(v1); ensure_bits(v2); SASSERT(m_bits[v1].size() == m_bits[v2].size()); expand_diseq(v1, v2); } @@ -1124,6 +1138,7 @@ namespace smt { literal_vector & lits = m_tmp_literals; lits.reset(); lits.push_back(mk_eq(get_enode(v1)->get_owner(), get_enode(v2)->get_owner(), true)); + ensure_bits(v1); ensure_bits(v2); literal_vector const & bits1 = m_bits[v1]; literal_vector::const_iterator it1 = bits1.begin(); literal_vector::const_iterator end1 = bits1.end(); @@ -1190,6 +1205,7 @@ namespace smt { if (m_wpos[v] == idx) find_wpos(v); + ensure_bits(v); literal_vector & bits = m_bits[v]; literal bit = bits[idx]; lbool val = ctx.get_assignment(bit); @@ -1204,6 +1220,7 @@ namespace smt { antecedent.neg(); } while (v2 != v) { + ensure_bits(v2); literal_vector & bits2 = m_bits[v2]; literal bit2 = bits2[idx]; SASSERT(bit != ~bit2); @@ -1234,6 +1251,7 @@ namespace smt { m_stats.m_num_bit2core++; context & ctx = get_context(); SASSERT(ctx.get_assignment(antecedent) == l_true); + ensure_bits(v2); SASSERT(m_bits[v2][idx].var() == consequent.var()); SASSERT(consequent.var() != antecedent.var()); TRACE("bv_bit_prop", tout << "assigning: "; ctx.display_literal(tout, consequent); @@ -1304,6 +1322,7 @@ namespace smt { enode * e = ctx.get_enode(n); theory_var v = e->get_th_var(get_id()); if (v != null_theory_var) { + ensure_bits(v); literal_vector & bits = m_bits[v]; for (literal lit : bits) { ctx.mark_as_relevant(lit); @@ -1385,6 +1404,7 @@ namespace smt { } m_prop_queue.reset(); context & ctx = get_context(); + ensure_bits(v1); ensure_bits(v2); literal_vector & bits1 = m_bits[v1]; literal_vector & bits2 = m_bits[v2]; SASSERT(bits1.size() == bits2.size()); @@ -1471,6 +1491,7 @@ namespace smt { theory_var v1 = m_merge_aux[!zo.m_is_true][zo.m_idx]; if (v1 != null_theory_var) { // conflict was detected ... v1 and v2 have complementary bits + ensure_bits(v1); ensure_bits(v2); SASSERT(m_bits[v1][zo.m_idx] == ~(m_bits[v2][zo.m_idx])); SASSERT(m_bits[v1].size() == m_bits[v2].size()); mk_new_diseq_axiom(v1, v2, zo.m_idx); @@ -1654,7 +1675,7 @@ namespace smt { } #ifdef Z3DEBUG - bool theory_bv::check_assignment(theory_var v) const { + bool theory_bv::check_assignment(theory_var v) { context & ctx = get_context(); if (!is_root(v)) return true; @@ -1663,9 +1684,11 @@ namespace smt { } theory_var v2 = v; + ensure_bits(v2); literal_vector const & bits2 = m_bits[v2]; theory_var v1 = v2; do { + ensure_bits(v1); literal_vector const & bits1 = m_bits[v1]; SASSERT(bits1.size() == bits2.size()); unsigned sz = bits1.size(); @@ -1695,7 +1718,7 @@ namespace smt { \remark The method does nothing if v is not the root of the equivalence class. */ - bool theory_bv::check_zero_one_bits(theory_var v) const { + bool theory_bv::check_zero_one_bits(theory_var v) { if (get_context().inconsistent()) return true; // property is only valid if the context is not in a conflict. if (is_root(v) && is_bv(v)) { @@ -1706,6 +1729,7 @@ namespace smt { bits[1].resize(bv_sz, false); theory_var curr = v; do { + ensure_bits(curr); literal_vector const & lits = m_bits[curr]; for (unsigned i = 0; i < lits.size(); i++) { literal l = lits[i]; @@ -1736,7 +1760,7 @@ namespace smt { return true; } - bool theory_bv::check_invariant() const { + bool theory_bv::check_invariant() { unsigned num = get_num_vars(); for (unsigned v = 0; v < num; v++) { check_assignment(v); diff --git a/src/smt/theory_bv.h b/src/smt/theory_bv.h index f2e0f5bed..9e868a887 100644 --- a/src/smt/theory_bv.h +++ b/src/smt/theory_bv.h @@ -141,6 +141,7 @@ namespace smt { bool is_numeral(theory_var v) const { return m_util.is_numeral(get_enode(v)->get_owner()); } app * mk_bit2bool(app * bv, unsigned idx); + void ensure_bits(theory_var v); void mk_bits(theory_var v); friend class mk_atom_trail; void mk_bit2bool(app * n); @@ -266,9 +267,9 @@ namespace smt { #ifdef Z3DEBUG - bool check_assignment(theory_var v) const; - bool check_invariant() const; - bool check_zero_one_bits(theory_var v) const; + bool check_assignment(theory_var v); + bool check_invariant(); + bool check_zero_one_bits(theory_var v); #endif }; };