mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

supply bits on demand

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-07-31 15:52:21 -07:00
parent 114f31c16a
commit 22a5687e16
2 changed files with 33 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

34
src/smt/theory_bv.cpp
View file

@ -162,10 +162,14 @@ namespace smt {
if (v == null_theory_var) { if (v == null_theory_var) {
v = mk_var(n); v = mk_var(n);
} }
ensure_bits(v);
return v;
}
void theory_bv::ensure_bits(theory_var v) {
if (m_bits[v].empty()) { if (m_bits[v].empty()) {
mk_bits(v); mk_bits(v);
} }
return v;
} }
enode * theory_bv::get_arg(enode * n, unsigned idx) { 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) { void theory_bv::get_bits(theory_var v, expr_ref_vector & r) {
context & ctx = get_context(); context & ctx = get_context();
ensure_bits(v);
literal_vector & bits = m_bits[v]; literal_vector & bits = m_bits[v];
for (literal lit : bits) { for (literal lit : bits) {
expr_ref l(get_manager()); expr_ref l(get_manager());
@ -223,6 +228,7 @@ namespace smt {
\brief v1[idx] = ~v2[idx], then v1 /= v2 is a theory axiom. \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) { 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]); 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);); TRACE("bv_diseq_axiom", tout << "found new diseq axiom\n"; display_var(tout, v1); display_var(tout, v2););
// found new disequality // found new disequality
@ -241,6 +247,7 @@ namespace smt {
} }
void theory_bv::register_true_false_bit(theory_var v, unsigned idx) { 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); SASSERT(m_bits[v][idx] == true_literal || m_bits[v][idx] == false_literal);
bool is_true = (m_bits[v][idx] == true_literal); bool is_true = (m_bits[v][idx] == true_literal);
zero_one_bits & bits = m_zero_one_bits[v]; 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. \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) { 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]; literal l = m_bits[v][idx];
l.neg(); l.neg();
while (occs) { while (occs) {
theory_var v2 = occs->m_var; theory_var v2 = occs->m_var;
unsigned idx2 = occs->m_idx; unsigned idx2 = occs->m_idx;
ensure_bits(v2);
if (idx == idx2 && m_bits[v2][idx2] == l && get_bv_size(v2) == get_bv_size(v)) if (idx == idx2 && m_bits[v2][idx2] == l && get_bv_size(v2) == get_bv_size(v))
mk_new_diseq_axiom(v, v2, idx); mk_new_diseq_axiom(v, v2, idx);
occs = occs->m_next; occs = occs->m_next;
@ -267,6 +276,7 @@ namespace smt {
*/ */
void theory_bv::add_bit(theory_var v, literal l) { void theory_bv::add_bit(theory_var v, literal l) {
context & ctx = get_context(); context & ctx = get_context();
ensure_bits(v);
literal_vector & bits = m_bits[v]; literal_vector & bits = m_bits[v];
unsigned idx = bits.size(); unsigned idx = bits.size();
bits.push_back(l); bits.push_back(l);
@ -329,6 +339,7 @@ namespace smt {
*/ */
void theory_bv::find_wpos(theory_var v) { void theory_bv::find_wpos(theory_var v) {
context & ctx = get_context(); context & ctx = get_context();
ensure_bits(v);
literal_vector const & bits = m_bits[v]; literal_vector const & bits = m_bits[v];
unsigned sz = bits.size(); unsigned sz = bits.size();
unsigned & wpos = m_wpos[v]; unsigned & wpos = m_wpos[v];
@ -435,6 +446,7 @@ namespace smt {
tout << mk_pp(o1, m) << " = " << mk_pp(o2, m) << " " tout << mk_pp(o1, m) << " = " << mk_pp(o2, m) << " "
<< ctx.get_scope_level() << "\n";); << ctx.get_scope_level() << "\n";);
literal_vector eqs; literal_vector eqs;
ensure_bits(v1); ensure_bits(v2);
for (unsigned i = 0; i < sz; ++i) { for (unsigned i = 0; i < sz; ++i) {
literal l1 = m_bits[v1][i]; literal l1 = m_bits[v1][i];
literal l2 = m_bits[v2][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(); context & ctx = get_context();
result.reset(); result.reset();
literal_vector const & bits = m_bits[v]; literal_vector const & bits = m_bits[v];
@ -844,6 +856,7 @@ namespace smt {
unsigned start = n->get_decl()->get_parameter(1).get_int(); unsigned start = n->get_decl()->get_parameter(1).get_int();
unsigned end = n->get_decl()->get_parameter(0).get_int(); unsigned end = n->get_decl()->get_parameter(0).get_int();
SASSERT(start <= end); SASSERT(start <= end);
ensure_bits(arg);
literal_vector & arg_bits = m_bits[arg]; literal_vector & arg_bits = m_bits[arg];
m_bits[v].reset(); m_bits[v].reset();
for (unsigned i = start; i <= end; ++i) 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) { void theory_bv::new_diseq_eh(theory_var v1, theory_var v2) {
if (is_bv(v1)) { if (is_bv(v1)) {
ensure_bits(v1); ensure_bits(v2);
SASSERT(m_bits[v1].size() == m_bits[v2].size()); SASSERT(m_bits[v1].size() == m_bits[v2].size());
expand_diseq(v1, v2); expand_diseq(v1, v2);
} }
@ -1124,6 +1138,7 @@ namespace smt {
literal_vector & lits = m_tmp_literals; literal_vector & lits = m_tmp_literals;
lits.reset(); lits.reset();
lits.push_back(mk_eq(get_enode(v1)->get_owner(), get_enode(v2)->get_owner(), true)); 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 & bits1 = m_bits[v1];
literal_vector::const_iterator it1 = bits1.begin(); literal_vector::const_iterator it1 = bits1.begin();
literal_vector::const_iterator end1 = bits1.end(); literal_vector::const_iterator end1 = bits1.end();
@ -1190,6 +1205,7 @@ namespace smt {
if (m_wpos[v] == idx) if (m_wpos[v] == idx)
find_wpos(v); find_wpos(v);
ensure_bits(v);
literal_vector & bits = m_bits[v]; literal_vector & bits = m_bits[v];
literal bit = bits[idx]; literal bit = bits[idx];
lbool val = ctx.get_assignment(bit); lbool val = ctx.get_assignment(bit);
@ -1204,6 +1220,7 @@ namespace smt {
antecedent.neg(); antecedent.neg();
} }
while (v2 != v) { while (v2 != v) {
ensure_bits(v2);
literal_vector & bits2 = m_bits[v2]; literal_vector & bits2 = m_bits[v2];
literal bit2 = bits2[idx]; literal bit2 = bits2[idx];
SASSERT(bit != ~bit2); SASSERT(bit != ~bit2);
@ -1234,6 +1251,7 @@ namespace smt {
m_stats.m_num_bit2core++; m_stats.m_num_bit2core++;
context & ctx = get_context(); context & ctx = get_context();
SASSERT(ctx.get_assignment(antecedent) == l_true); SASSERT(ctx.get_assignment(antecedent) == l_true);
ensure_bits(v2);
SASSERT(m_bits[v2][idx].var() == consequent.var()); SASSERT(m_bits[v2][idx].var() == consequent.var());
SASSERT(consequent.var() != antecedent.var()); SASSERT(consequent.var() != antecedent.var());
TRACE("bv_bit_prop", tout << "assigning: "; ctx.display_literal(tout, consequent); TRACE("bv_bit_prop", tout << "assigning: "; ctx.display_literal(tout, consequent);
@ -1304,6 +1322,7 @@ namespace smt {
enode * e = ctx.get_enode(n); enode * e = ctx.get_enode(n);
theory_var v = e->get_th_var(get_id()); theory_var v = e->get_th_var(get_id());
if (v != null_theory_var) { if (v != null_theory_var) {
ensure_bits(v);
literal_vector & bits = m_bits[v]; literal_vector & bits = m_bits[v];
for (literal lit : bits) { for (literal lit : bits) {
ctx.mark_as_relevant(lit); ctx.mark_as_relevant(lit);
@ -1385,6 +1404,7 @@ namespace smt {
} }
m_prop_queue.reset(); m_prop_queue.reset();
context & ctx = get_context(); context & ctx = get_context();
ensure_bits(v1); ensure_bits(v2);
literal_vector & bits1 = m_bits[v1]; literal_vector & bits1 = m_bits[v1];
literal_vector & bits2 = m_bits[v2]; literal_vector & bits2 = m_bits[v2];
SASSERT(bits1.size() == bits2.size()); SASSERT(bits1.size() == bits2.size());
@ -1471,6 +1491,7 @@ namespace smt {
theory_var v1 = m_merge_aux[!zo.m_is_true][zo.m_idx]; theory_var v1 = m_merge_aux[!zo.m_is_true][zo.m_idx];
if (v1 != null_theory_var) { if (v1 != null_theory_var) {
// conflict was detected ... v1 and v2 have complementary bits // 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][zo.m_idx] == ~(m_bits[v2][zo.m_idx]));
SASSERT(m_bits[v1].size() == m_bits[v2].size()); SASSERT(m_bits[v1].size() == m_bits[v2].size());
mk_new_diseq_axiom(v1, v2, zo.m_idx); mk_new_diseq_axiom(v1, v2, zo.m_idx);
@ -1654,7 +1675,7 @@ namespace smt {
} }
#ifdef Z3DEBUG #ifdef Z3DEBUG
bool theory_bv::check_assignment(theory_var v) const { bool theory_bv::check_assignment(theory_var v) {
context & ctx = get_context(); context & ctx = get_context();
if (!is_root(v)) if (!is_root(v))
return true; return true;
@ -1663,9 +1684,11 @@ namespace smt {
} }
theory_var v2 = v; theory_var v2 = v;
ensure_bits(v2);
literal_vector const & bits2 = m_bits[v2]; literal_vector const & bits2 = m_bits[v2];
theory_var v1 = v2; theory_var v1 = v2;
do { do {
ensure_bits(v1);
literal_vector const & bits1 = m_bits[v1]; literal_vector const & bits1 = m_bits[v1];
SASSERT(bits1.size() == bits2.size()); SASSERT(bits1.size() == bits2.size());
unsigned sz = bits1.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. \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()) if (get_context().inconsistent())
return true; // property is only valid if the context is not in a conflict. return true; // property is only valid if the context is not in a conflict.
if (is_root(v) && is_bv(v)) { if (is_root(v) && is_bv(v)) {
@ -1706,6 +1729,7 @@ namespace smt {
bits[1].resize(bv_sz, false); bits[1].resize(bv_sz, false);
theory_var curr = v; theory_var curr = v;
do { do {
ensure_bits(curr);
literal_vector const & lits = m_bits[curr]; literal_vector const & lits = m_bits[curr];
for (unsigned i = 0; i < lits.size(); i++) { for (unsigned i = 0; i < lits.size(); i++) {
literal l = lits[i]; literal l = lits[i];
@ -1736,7 +1760,7 @@ namespace smt {
return true; return true;
} }
bool theory_bv::check_invariant() const { bool theory_bv::check_invariant() {
unsigned num = get_num_vars(); unsigned num = get_num_vars();
for (unsigned v = 0; v < num; v++) { for (unsigned v = 0; v < num; v++) {
check_assignment(v); check_assignment(v);

7
src/smt/theory_bv.h
View file

@ -141,6 +141,7 @@ namespace smt {
bool is_numeral(theory_var v) const { return m_util.is_numeral(get_enode(v)->get_owner()); } bool is_numeral(theory_var v) const { return m_util.is_numeral(get_enode(v)->get_owner()); }
app * mk_bit2bool(app * bv, unsigned idx); app * mk_bit2bool(app * bv, unsigned idx);
void ensure_bits(theory_var v);
void mk_bits(theory_var v); void mk_bits(theory_var v);
friend class mk_atom_trail; friend class mk_atom_trail;
void mk_bit2bool(app * n); void mk_bit2bool(app * n);
@ -266,9 +267,9 @@ namespace smt {
#ifdef Z3DEBUG #ifdef Z3DEBUG
bool check_assignment(theory_var v) const; bool check_assignment(theory_var v);
bool check_invariant() const; bool check_invariant();
bool check_zero_one_bits(theory_var v) const; bool check_zero_one_bits(theory_var v);
#endif #endif
}; };
}; };