1 /*++ 2 Copyright (c) 2020 Microsoft Corporation 3 4 Module Name: 5 6 bv_solver.cpp 7 8 Abstract: 9 10 Solving utilities for bit-vectors. 11 12 Author: 13 14 Nikolaj Bjorner (nbjorner) 2020-09-02 15 based on smt/theory_bv 16 17 --*/ 18 19 #include "ast/ast_ll_pp.h" 20 #include "sat/smt/bv_solver.h" 21 #include "sat/smt/euf_solver.h" 22 #include "sat/smt/sat_th.h" 23 #include "tactic/tactic_exception.h" 24 25 namespace bv { 26 27 class solver::bit_trail : public trail { 28 solver& s; 29 solver::var_pos vp; 30 sat::literal lit; 31 public: bit_trail(solver & s,var_pos vp)32 bit_trail(solver& s, var_pos vp) : s(s), vp(vp), lit(s.m_bits[vp.first][vp.second]) {} 33 undo()34 void undo() override { 35 s.m_bits[vp.first][vp.second] = lit; 36 } 37 }; 38 39 class solver::bit_occs_trail : public trail { 40 atom& a; 41 var_pos_occ* m_occs; 42 43 public: bit_occs_trail(solver & s,atom & a)44 bit_occs_trail(solver& s, atom& a): a(a), m_occs(a.m_occs) {} 45 undo()46 void undo() override { 47 a.m_occs = m_occs; 48 } 49 }; 50 solver(euf::solver & ctx,theory_id id)51 solver::solver(euf::solver& ctx, theory_id id) : 52 euf::th_euf_solver(ctx, symbol("bv"), id), 53 bv(m), 54 m_autil(m), 55 m_ackerman(*this), 56 m_bb(m, get_config()), 57 m_find(*this) { 58 m_bb.set_flat(false); 59 } 60 fixed_var_eh(theory_var v1)61 void solver::fixed_var_eh(theory_var v1) { 62 numeral val1, val2; 63 VERIFY(get_fixed_value(v1, val1)); 64 euf::enode* n1 = var2enode(v1); 65 unsigned sz = m_bits[v1].size(); 66 value_sort_pair key(val1, sz); 67 theory_var v2; 68 if (ctx.watches_fixed(n1)) { 69 expr_ref value(bv.mk_numeral(val1, sz), m); 70 ctx.assign_fixed(n1, value, m_bits[v1]); 71 } 72 bool is_current = 73 m_fixed_var_table.find(key, v2) && 74 v2 < static_cast<int>(get_num_vars()) && 75 is_bv(v2) && 76 m_bits[v2].size() == sz && 77 get_fixed_value(v2, val2) && val1 == val2; 78 if (!is_current) 79 m_fixed_var_table.insert(key, v1); 80 else if (n1->get_root() != var2enode(v2)->get_root()) { 81 SASSERT(get_bv_size(v1) == get_bv_size(v2)); 82 TRACE("bv", tout << "detected equality: v" << v1 << " = v" << v2 << "\n" << pp(v1) << pp(v2);); 83 m_stats.m_num_bit2eq++; 84 add_fixed_eq(v1, v2); 85 ctx.propagate(n1, var2enode(v2), mk_bit2eq_justification(v1, v2)); 86 } 87 } 88 add_fixed_eq(theory_var v1,theory_var v2)89 void solver::add_fixed_eq(theory_var v1, theory_var v2) { 90 if (!get_config().m_bv_eq_axioms) 91 return; 92 m_ackerman.used_eq_eh(v1, v2); 93 } 94 get_fixed_value(theory_var v,numeral & result) const95 bool solver::get_fixed_value(theory_var v, numeral& result) const { 96 result.reset(); 97 unsigned i = 0; 98 for (literal b : m_bits[v]) { 99 if (b == ~m_true) 100 ; 101 else if (b == m_true) 102 result += power2(i); 103 else { 104 switch (ctx.s().value(b)) { 105 case l_false: 106 break; 107 case l_undef: 108 return false; 109 case l_true: 110 result += power2(i); 111 break; 112 } 113 } 114 ++i; 115 } 116 return true; 117 } 118 119 /** 120 \brief Find an unassigned bit for m_wpos[v], if such bit cannot be found invoke fixed_var_eh 121 */ find_wpos(theory_var v)122 void solver::find_wpos(theory_var v) { 123 literal_vector const& bits = m_bits[v]; 124 unsigned sz = bits.size(); 125 unsigned& wpos = m_wpos[v]; 126 for (unsigned i = 0; i < sz; ++i) { 127 unsigned idx = (i + wpos) % sz; 128 if (s().value(bits[idx]) == l_undef) { 129 wpos = idx; 130 TRACE("bv", tout << "moved wpos of v" << v << " to " << wpos << "\n";); 131 return; 132 } 133 } 134 TRACE("bv", tout << "v" << v << " is a fixed variable.\n";); 135 fixed_var_eh(v); 136 } 137 138 /** 139 *\brief v[idx] = ~v'[idx], then v /= v' is a theory axiom. 140 */ find_new_diseq_axioms(atom & a,theory_var v,unsigned idx)141 void solver::find_new_diseq_axioms(atom& a, theory_var v, unsigned idx) { 142 if (!get_config().m_bv_eq_axioms) 143 return; 144 literal l = m_bits[v][idx]; 145 l.neg(); 146 for (auto vp : a) { 147 theory_var v2 = vp.first; 148 unsigned idx2 = vp.second; 149 if (idx == idx2 && m_bits[v2].size() == m_bits[v].size() && m_bits[v2][idx2] == l ) 150 mk_new_diseq_axiom(v, v2, idx); 151 } 152 } 153 154 /** 155 \brief v1[idx] = ~v2[idx], then v1 /= v2 is a theory axiom. 156 */ mk_new_diseq_axiom(theory_var v1,theory_var v2,unsigned idx)157 void solver::mk_new_diseq_axiom(theory_var v1, theory_var v2, unsigned idx) { 158 SASSERT(m_bits[v1][idx] == ~m_bits[v2][idx]); 159 TRACE("bv", tout << "found new diseq axiom\n" << pp(v1) << pp(v2);); 160 m_stats.m_num_diseq_static++; 161 expr_ref eq = mk_var_eq(v1, v2); 162 add_unit(~ctx.internalize(eq, false, false, m_is_redundant)); 163 } 164 display(std::ostream & out,theory_var v) const165 std::ostream& solver::display(std::ostream& out, theory_var v) const { 166 expr* e = var2expr(v); 167 out << "v"; 168 out.width(4); 169 out << std::left << v; 170 out << " "; 171 out.width(4); 172 out << e->get_id() << " -> "; 173 out.width(4); 174 out << var2enode(find(v))->get_expr_id(); 175 out << std::right; 176 out.flush(); 177 atom* a = nullptr; 178 if (is_bv(v)) { 179 numeral val; 180 if (get_fixed_value(v, val)) 181 out << " (= " << val << ")"; 182 for (literal lit : m_bits[v]) { 183 out << " " << lit << ":" << mk_bounded_pp(literal2expr(lit), m, 1); 184 } 185 } 186 else if (m.is_bool(e) && (a = m_bool_var2atom.get(expr2literal(e).var(), nullptr))) { 187 for (var_pos vp : *a) 188 out << " " << var2enode(vp.first)->get_expr_id() << "[" << vp.second << "]"; 189 } 190 else 191 out << " " << mk_bounded_pp(e, m, 1); 192 out << "\n"; 193 return out; 194 } 195 new_eq_eh(euf::th_eq const & eq)196 void solver::new_eq_eh(euf::th_eq const& eq) { 197 force_push(); 198 TRACE("bv", tout << "new eq " << mk_bounded_pp(var2expr(eq.v1()), m) << " == " << mk_bounded_pp(var2expr(eq.v2()), m) << "\n";); 199 if (is_bv(eq.v1())) { 200 m_find.merge(eq.v1(), eq.v2()); 201 VERIFY(eq.is_eq()); 202 } 203 } 204 new_diseq_eh(euf::th_eq const & ne)205 void solver::new_diseq_eh(euf::th_eq const& ne) { 206 theory_var v1 = ne.v1(), v2 = ne.v2(); 207 if (!is_bv(v1)) 208 return; 209 if (s().is_probing()) 210 return; 211 212 TRACE("bv", tout << "diff: " << v1 << " != " << v2 << " @" << s().scope_lvl() << "\n";); 213 unsigned sz = m_bits[v1].size(); 214 if (sz == 1) 215 return; 216 unsigned num_undef = 0; 217 int undef_idx = 0; 218 for (unsigned i = 0; i < sz; ++i) { 219 sat::literal a = m_bits[v1][i]; 220 sat::literal b = m_bits[v2][i]; 221 if (a == ~b) 222 return; 223 auto va = s().value(a); 224 auto vb = s().value(b); 225 if (va != l_undef && vb != l_undef && va != vb) 226 return; 227 if (va == l_undef) { 228 ++num_undef; 229 undef_idx = i + 1; 230 } 231 if (vb == l_undef) { 232 ++num_undef; 233 undef_idx = -static_cast<int>(i + 1); 234 } 235 if (num_undef > 1 && get_config().m_bv_eq_axioms) 236 return; 237 } 238 if (num_undef == 0) 239 return; 240 else if (num_undef == 1) { 241 if (undef_idx < 0) { 242 undef_idx = -undef_idx; 243 std::swap(v1, v2); 244 } 245 undef_idx--; 246 sat::literal consequent = m_bits[v1][undef_idx]; 247 sat::literal b = m_bits[v2][undef_idx]; 248 sat::literal antecedent = ~expr2literal(ne.eq()); 249 SASSERT(s().value(antecedent) == l_true); 250 SASSERT(s().value(consequent) == l_undef); 251 SASSERT(s().value(b) != l_undef); 252 if (s().value(b) == l_true) 253 consequent.neg(); 254 ++m_stats.m_num_ne2bit; 255 s().assign(consequent, mk_ne2bit_justification(undef_idx, v1, v2, consequent, antecedent)); 256 } 257 else if (s().at_search_lvl()) { 258 force_push(); 259 assert_ackerman(v1, v2); 260 } 261 else 262 m_ackerman.used_diseq_eh(v1, v2); 263 } 264 get_reward(literal l,sat::ext_constraint_idx idx,sat::literal_occs_fun & occs) const265 double solver::get_reward(literal l, sat::ext_constraint_idx idx, sat::literal_occs_fun& occs) const { return 0; } is_extended_binary(sat::ext_justification_idx idx,literal_vector & r)266 bool solver::is_extended_binary(sat::ext_justification_idx idx, literal_vector& r) { return false; } is_external(bool_var v)267 bool solver::is_external(bool_var v) { return true; } 268 get_antecedents(literal l,sat::ext_justification_idx idx,literal_vector & r,bool probing)269 void solver::get_antecedents(literal l, sat::ext_justification_idx idx, literal_vector& r, bool probing) { 270 auto& c = bv_justification::from_index(idx); 271 TRACE("bv", display_constraint(tout, idx) << "\n";); 272 switch (c.m_kind) { 273 case bv_justification::kind_t::eq2bit: 274 SASSERT(s().value(c.m_antecedent) == l_true); 275 r.push_back(c.m_antecedent); 276 ctx.add_antecedent(var2enode(c.m_v1), var2enode(c.m_v2)); 277 break; 278 case bv_justification::kind_t::ne2bit: { 279 r.push_back(c.m_antecedent); 280 SASSERT(s().value(c.m_antecedent) == l_true); 281 SASSERT(c.m_consequent == l); 282 unsigned idx = c.m_idx; 283 for (unsigned i = m_bits[c.m_v1].size(); i-- > 0; ) { 284 sat::literal a = m_bits[c.m_v1][i]; 285 sat::literal b = m_bits[c.m_v2][i]; 286 SASSERT(a == b || s().value(a) != l_undef); 287 SASSERT(i == idx || s().value(a) == s().value(b)); 288 if (a == b) 289 continue; 290 if (i == idx) { 291 if (s().value(b) == l_false) 292 b.neg(); 293 r.push_back(b); 294 295 continue; 296 } 297 if (s().value(a) == l_false) { 298 a.neg(); 299 b.neg(); 300 } 301 r.push_back(a); 302 r.push_back(b); 303 } 304 305 break; 306 } 307 case bv_justification::kind_t::bit2eq: 308 SASSERT(m_bits[c.m_v1].size() == m_bits[c.m_v2].size()); 309 for (unsigned i = m_bits[c.m_v1].size(); i-- > 0; ) { 310 sat::literal a = m_bits[c.m_v1][i]; 311 sat::literal b = m_bits[c.m_v2][i]; 312 SASSERT(a == b || s().value(a) != l_undef); 313 SASSERT(s().value(a) == s().value(b)); 314 if (a == b) 315 continue; 316 if (s().value(a) == l_false) { 317 a.neg(); 318 b.neg(); 319 } 320 r.push_back(a); 321 r.push_back(b); 322 } 323 break; 324 case bv_justification::kind_t::bit2ne: { 325 SASSERT(c.m_consequent.sign()); 326 sat::bool_var v = c.m_consequent.var(); 327 expr* eq = bool_var2expr(v); 328 SASSERT(m.is_eq(eq)); 329 euf::enode* n = expr2enode(eq); 330 theory_var v1 = n->get_arg(0)->get_th_var(get_id()); 331 theory_var v2 = n->get_arg(1)->get_th_var(get_id()); 332 sat::literal a = m_bits[v1][c.m_idx]; 333 sat::literal b = m_bits[v2][c.m_idx]; 334 lbool val_a = s().value(a); 335 lbool val_b = s().value(b); 336 SASSERT(val_a != l_undef && val_b != l_undef && val_a != val_b); 337 if (val_a == l_false) a.neg(); 338 if (val_b == l_false) b.neg(); 339 r.push_back(a); 340 r.push_back(b); 341 break; 342 } 343 } 344 if (!probing && ctx.use_drat()) 345 log_drat(c); 346 } 347 log_drat(bv_justification const & c)348 void solver::log_drat(bv_justification const& c) { 349 // introduce dummy literal for equality. 350 sat::literal leq(s().num_vars() + 1, false); 351 expr_ref eq(m); 352 if (c.m_kind != bv_justification::kind_t::bit2ne) { 353 expr* e1 = var2expr(c.m_v1); 354 expr* e2 = var2expr(c.m_v2); 355 eq = m.mk_eq(e1, e2); 356 ctx.drat_eq_def(leq, eq); 357 } 358 359 sat::literal_vector lits; 360 switch (c.m_kind) { 361 case bv_justification::kind_t::eq2bit: 362 lits.push_back(~leq); 363 lits.push_back(~c.m_antecedent); 364 lits.push_back(c.m_consequent); 365 break; 366 case bv_justification::kind_t::ne2bit: 367 get_antecedents(c.m_consequent, c.to_index(), lits, true); 368 lits.push_back(c.m_consequent); 369 break; 370 case bv_justification::kind_t::bit2eq: 371 get_antecedents(leq, c.to_index(), lits, true); 372 for (auto& lit : lits) 373 lit.neg(); 374 lits.push_back(leq); 375 break; 376 case bv_justification::kind_t::bit2ne: 377 get_antecedents(c.m_consequent, c.to_index(), lits, true); 378 for (auto& lit : lits) 379 lit.neg(); 380 lits.push_back(c.m_consequent); 381 break; 382 } 383 ctx.get_drat().add(lits, status()); 384 // TBD, a proper way would be to delete the lemma after use. 385 } 386 asserted(literal l)387 void solver::asserted(literal l) { 388 389 atom* a = get_bv2a(l.var()); 390 TRACE("bv", tout << "asserted: " << l << "\n";); 391 if (a) { 392 force_push(); 393 m_prop_queue.push_back(propagation_item(a)); 394 for (auto p : a->m_bit2occ) { 395 del_eq_occurs(p.first, p.second); 396 } 397 } 398 } 399 unit_propagate()400 bool solver::unit_propagate() { 401 if (m_prop_queue_head == m_prop_queue.size()) 402 return false; 403 force_push(); 404 ctx.push(value_trail<unsigned>(m_prop_queue_head)); 405 for (; m_prop_queue_head < m_prop_queue.size() && !s().inconsistent(); ++m_prop_queue_head) { 406 auto const p = m_prop_queue[m_prop_queue_head]; 407 if (p.m_atom) { 408 for (auto vp : *p.m_atom) 409 propagate_bits(vp); 410 for (eq_occurs const& eq : p.m_atom->eqs()) 411 propagate_eq_occurs(eq); 412 } 413 else 414 propagate_bits(p.m_vp); 415 } 416 // check_missing_propagation(); 417 return true; 418 } 419 propagate_eq_occurs(eq_occurs const & occ)420 bool solver::propagate_eq_occurs(eq_occurs const& occ) { 421 auto lit = occ.m_literal; 422 423 if (s().value(lit) != l_undef) { 424 IF_VERBOSE(20, verbose_stream() << "assigned " << lit << " " << s().value(lit) << "\n"); 425 return false; 426 } 427 literal bit1 = m_bits[occ.m_v1][occ.m_idx]; 428 literal bit2 = m_bits[occ.m_v2][occ.m_idx]; 429 lbool val2 = s().value(bit2); 430 431 if (val2 == l_undef) { 432 IF_VERBOSE(20, verbose_stream() << "add " << occ.m_bv2 << " " << occ.m_v2 << "\n"); 433 eq_internalized(occ.m_bv2, occ.m_bv1, occ.m_idx, occ.m_v2, occ.m_v1, occ.m_literal, occ.m_node); 434 return false; 435 } 436 lbool val1 = s().value(bit1); 437 SASSERT(val1 != l_undef); 438 if (val1 != val2 && val2 != l_undef) { 439 ++m_stats.m_num_bit2ne; 440 IF_VERBOSE(20, verbose_stream() << "assign " << ~lit << "\n"); 441 s().assign(~lit, mk_bit2ne_justification(occ.m_idx, ~lit)); 442 return true; 443 } 444 IF_VERBOSE(20, verbose_stream() << "eq " << lit << "\n"); 445 return false; 446 } 447 propagate_bits(var_pos entry)448 bool solver::propagate_bits(var_pos entry) { 449 theory_var v1 = entry.first; 450 unsigned idx = entry.second; 451 SASSERT(idx < m_bits[v1].size()); 452 if (m_wpos[v1] == idx) 453 find_wpos(v1); 454 455 literal bit1 = m_bits[v1][idx]; 456 lbool val = s().value(bit1); 457 TRACE("bv", tout << "propagating v" << v1 << " #" << var2enode(v1)->get_expr_id() << "[" << idx << "] = " << val << "\n";); 458 if (val == l_undef) 459 return false; 460 461 if (val == l_false) 462 bit1.neg(); 463 464 unsigned num_bits = 0, num_assigned = 0; 465 for (theory_var v2 = m_find.next(v1); v2 != v1; v2 = m_find.next(v2)) { 466 literal bit2 = m_bits[v2][idx]; 467 SASSERT(m_bits[v1][idx] != ~m_bits[v2][idx]); 468 TRACE("bv", tout << "propagating #" << var2enode(v2)->get_expr_id() << "[" << idx << "] = " << s().value(bit2) << "\n";); 469 470 if (val == l_false) 471 bit2.neg(); 472 ++num_bits; 473 if (num_bits > 3 && num_assigned == 0) 474 break; 475 if (s().value(bit2) == l_true) 476 continue; 477 ++num_assigned; 478 if (!assign_bit(bit2, v1, v2, idx, bit1, false)) 479 break; 480 } 481 if (s().value(m_bits[v1][m_wpos[v1]]) != l_undef) 482 find_wpos(v1); 483 484 return num_assigned > 0; 485 } 486 487 /** 488 * Check each delay internalized bit-vector operation for compliance. 489 * 490 * TBD: add model-repair attempt after cheap propagation axioms have been added 491 */ check()492 sat::check_result solver::check() { 493 force_push(); 494 SASSERT(m_prop_queue.size() == m_prop_queue_head); 495 bool ok = true; 496 svector<std::pair<expr*, internalize_mode>> delay; 497 for (auto kv : m_delay_internalize) 498 delay.push_back(std::make_pair(kv.m_key, kv.m_value)); 499 flet<bool> _cheap1(m_cheap_axioms, true); 500 for (auto kv : delay) 501 if (!check_delay_internalized(kv.first)) 502 ok = false; 503 if (!ok) 504 return sat::check_result::CR_CONTINUE; 505 506 // if (repair_model()) return sat::check_result::DONE; 507 508 flet<bool> _cheap2(m_cheap_axioms, false); 509 for (auto kv : delay) 510 if (!check_delay_internalized(kv.first)) 511 ok = false; 512 513 if (!ok) 514 return sat::check_result::CR_CONTINUE; 515 return sat::check_result::CR_DONE; 516 } 517 push_core()518 void solver::push_core() { 519 TRACE("bv", tout << "push: " << get_num_vars() << "@" << m_prop_queue_lim.size() << "\n";); 520 th_euf_solver::push_core(); 521 m_prop_queue_lim.push_back(m_prop_queue.size()); 522 } 523 pop_core(unsigned n)524 void solver::pop_core(unsigned n) { 525 SASSERT(m_num_scopes == 0); 526 unsigned old_sz = m_prop_queue_lim.size() - n; 527 m_prop_queue.shrink(m_prop_queue_lim[old_sz]); 528 m_prop_queue_lim.shrink(old_sz); 529 th_euf_solver::pop_core(n); 530 old_sz = get_num_vars(); 531 m_bits.shrink(old_sz); 532 m_wpos.shrink(old_sz); 533 m_zero_one_bits.shrink(old_sz); 534 TRACE("bv", tout << "num vars " << old_sz << "@" << m_prop_queue_lim.size() << "\n";); 535 } 536 simplify()537 void solver::simplify() { 538 m_ackerman.propagate(); 539 } 540 set_root(literal l,literal r)541 bool solver::set_root(literal l, literal r) { 542 return false; 543 atom* a = get_bv2a(l.var()); 544 if (!a) 545 return true; 546 for (auto vp : *a) { 547 sat::literal l2 = m_bits[vp.first][vp.second]; 548 if (l2.var() == r.var()) 549 continue; 550 SASSERT(l2.var() == l.var()); 551 VERIFY(l2.var() == l.var()); 552 sat::literal r2 = (l.sign() == l2.sign()) ? r : ~r; 553 ctx.push(vector2_value_trail<bits_vector, sat::literal>(m_bits, vp.first, vp.second)); 554 m_bits[vp.first][vp.second] = r2; 555 set_bit_eh(vp.first, r2, vp.second); 556 } 557 ctx.push(bit_occs_trail(*this, *a)); 558 a->m_occs = nullptr; 559 // validate_atoms(); 560 return true; 561 } 562 563 /** 564 * Instantiate Ackerman axioms for bit-vectors that have become equal after roots have been added. 565 */ flush_roots()566 void solver::flush_roots() { 567 struct eq { 568 solver& s; 569 eq(solver& s) :s(s) {} 570 bool operator()(theory_var v1, theory_var v2) const { 571 return s.m_bits[v1] == s.m_bits[v2]; 572 } 573 }; 574 struct hash { 575 solver& s; 576 hash(solver& s) :s(s) {} 577 bool operator()(theory_var v) const { 578 literal_vector const& a = s.m_bits[v]; 579 return string_hash(reinterpret_cast<char*>(a.data()), a.size() * sizeof(sat::literal), 3); 580 } 581 }; 582 eq eq_proc(*this); 583 hash hash_proc(*this); 584 map<theory_var, theory_var, hash, eq> table(hash_proc, eq_proc); 585 for (theory_var v = 0; v < static_cast<theory_var>(get_num_vars()); ++v) { 586 if (!m_bits[v].empty()) { 587 theory_var w = table.insert_if_not_there(v, v); 588 if (v != w && m_find.find(v) != m_find.find(w)) 589 assert_ackerman(v, w); 590 } 591 } 592 TRACE("bv", tout << "infer new equations for bit-vectors that are now equal\n";); 593 } 594 clauses_modifed()595 void solver::clauses_modifed() {} get_phase(bool_var v)596 lbool solver::get_phase(bool_var v) { return l_undef; } display(std::ostream & out) const597 std::ostream& solver::display(std::ostream& out) const { 598 unsigned num_vars = get_num_vars(); 599 if (num_vars > 0) 600 out << "bv-solver:\n"; 601 for (unsigned v = 0; v < num_vars; v++) 602 out << pp(v); 603 return out; 604 } 605 display_justification(std::ostream & out,sat::ext_justification_idx idx) const606 std::ostream& solver::display_justification(std::ostream& out, sat::ext_justification_idx idx) const { 607 return display_constraint(out, idx); 608 } 609 display_constraint(std::ostream & out,sat::ext_constraint_idx idx) const610 std::ostream& solver::display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const { 611 auto& c = bv_justification::from_index(idx); 612 theory_var v1 = c.m_v1; 613 theory_var v2 = c.m_v2; 614 unsigned cidx = c.m_idx; 615 switch (c.m_kind) { 616 case bv_justification::kind_t::eq2bit: 617 return out << "bv <- " << c.m_antecedent << " v" << v1 << " == v" << v2; 618 case bv_justification::kind_t::bit2eq: 619 return out << "bv " << m_bits[v1] << " == " << m_bits[v2] << " -> v" << v1 << " == v" << v2; 620 case bv_justification::kind_t::bit2ne: { 621 expr* e = bool_var2expr(c.m_consequent.var()); 622 SASSERT(m.is_eq(e)); 623 euf::enode* n = expr2enode(e); 624 v1 = n->get_arg(0)->get_th_var(get_id()); 625 v2 = n->get_arg(1)->get_th_var(get_id()); 626 return out << "bv <- v" << v1 << "[" << cidx << "] != v" << v2 << "[" << cidx << "] " << m_bits[v1][cidx] << " != " << m_bits[v2][cidx]; 627 } 628 case bv_justification::kind_t::ne2bit: 629 return out << "bv <- " << m_bits[v1] << " != " << m_bits[v2] << " @" << cidx; 630 default: 631 UNREACHABLE(); 632 break; 633 } 634 return out; 635 } 636 display(std::ostream & out,atom const & a) const637 std::ostream& solver::display(std::ostream& out, atom const& a) const { 638 out << a.m_bv << "\n"; 639 for (auto vp : a) 640 out << vp.first << "[" << vp.second << "]\n"; 641 for (auto e : a.eqs()) 642 out << e.m_bv1 << " " << e.m_bv2 << "\n"; 643 return out; 644 } 645 646 collect_statistics(statistics & st) const647 void solver::collect_statistics(statistics& st) const { 648 st.update("bv conflicts", m_stats.m_num_conflicts); 649 st.update("bv diseqs", m_stats.m_num_diseq_static); 650 st.update("bv dynamic diseqs", m_stats.m_num_diseq_dynamic); 651 st.update("bv eq2bit", m_stats.m_num_eq2bit); 652 st.update("bv ne2bit", m_stats.m_num_ne2bit); 653 st.update("bv bit2eq", m_stats.m_num_bit2eq); 654 st.update("bv bit2ne", m_stats.m_num_bit2ne); 655 st.update("bv ackerman", m_stats.m_ackerman); 656 } 657 copy(sat::solver * s)658 sat::extension* solver::copy(sat::solver* s) { UNREACHABLE(); return nullptr; } 659 clone(euf::solver & ctx)660 euf::th_solver* solver::clone(euf::solver& ctx) { 661 bv::solver* result = alloc(bv::solver, ctx, get_id()); 662 ast_translation tr(m, ctx.get_manager()); 663 for (unsigned i = 0; i < get_num_vars(); ++i) { 664 expr* e1 = var2expr(i); 665 expr* e2 = tr(e1); 666 euf::enode* n2 = ctx.get_enode(e2); 667 SASSERT(n2); 668 result->mk_var(n2); 669 result->m_bits[i].append(m_bits[i]); 670 result->m_zero_one_bits[i].append(m_zero_one_bits[i]); 671 } 672 result->set_solver(&ctx.s()); 673 for (theory_var i = 0; i < static_cast<theory_var>(get_num_vars()); ++i) 674 if (find(i) != i) 675 result->m_find.set_root(i, find(i)); 676 677 auto clone_atom = [&](atom const& a) { 678 atom* new_a = new (result->get_region()) atom(a.m_bv); 679 result->m_bool_var2atom.setx(a.m_bv, new_a, nullptr); 680 for (auto [v, p] : a) 681 new_a->m_occs = new (result->get_region()) var_pos_occ(v, p, new_a->m_occs); 682 for (eq_occurs const& occ : a.eqs()) { 683 expr* e = occ.m_node->get_expr(); 684 expr_ref e2(tr(e), tr.to()); 685 euf::enode* n = ctx.get_enode(e2); 686 SASSERT(tr.to().contains(e2)); 687 new_a->m_eqs = new (result->get_region()) eq_occurs(occ.m_bv1, occ.m_bv2, occ.m_idx, occ.m_v1, occ.m_v2, occ.m_literal, n, new_a->m_eqs); 688 } 689 new_a->m_def = a.m_def; 690 new_a->m_var = a.m_var; 691 }; 692 693 for (atom* a : m_bool_var2atom) 694 if (a) 695 clone_atom(*a); 696 // validate_atoms(); 697 698 for (auto p : m_prop_queue) { 699 propagation_item q = p; 700 if (p.is_atom()) 701 q = propagation_item(result->get_bv2a(p.m_atom->m_bv)); 702 result->m_prop_queue.push_back(q); 703 } 704 return result; 705 } 706 pop_reinit()707 void solver::pop_reinit() {} validate()708 bool solver::validate() { return true; } init_use_list(sat::ext_use_list & ul)709 void solver::init_use_list(sat::ext_use_list& ul) {} is_blocked(literal l,sat::ext_constraint_idx)710 bool solver::is_blocked(literal l, sat::ext_constraint_idx) { return false; } check_model(sat::model const & m) const711 bool solver::check_model(sat::model const& m) const { return true; } finalize_model(model & mdl)712 void solver::finalize_model(model& mdl) {} 713 add_value(euf::enode * n,model & mdl,expr_ref_vector & values)714 void solver::add_value(euf::enode* n, model& mdl, expr_ref_vector& values) { 715 SASSERT(bv.is_bv(n->get_expr())); 716 if (bv.is_numeral(n->get_expr())) { 717 values[n->get_root_id()] = n->get_expr(); 718 return; 719 } 720 theory_var v = n->get_th_var(get_id()); 721 rational val; 722 unsigned i = 0; 723 for (auto l : m_bits[v]) { 724 switch (s().value(l)) { 725 case l_true: 726 val += power2(i); 727 break; 728 default: 729 break; 730 } 731 ++i; 732 } 733 values[n->get_root_id()] = bv.mk_numeral(val, m_bits[v].size()); 734 } 735 get_trail_stack()736 trail_stack& solver::get_trail_stack() { 737 return ctx.get_trail_stack(); 738 } 739 merge_eh(theory_var r1,theory_var r2,theory_var v1,theory_var v2)740 void solver::merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) { 741 742 TRACE("bv", tout << "merging: v" << v1 << " #" << var2enode(v1)->get_expr_id() << " v" << v2 << " #" << var2enode(v2)->get_expr_id() << "\n";); 743 if (!merge_zero_one_bits(r1, r2)) { 744 TRACE("bv", tout << "conflict detected\n";); 745 return; // conflict was detected 746 } 747 SASSERT(m_bits[v1].size() == m_bits[v2].size()); 748 unsigned sz = m_bits[v1].size(); 749 if (sz == 1) 750 return; 751 for (unsigned idx = 0; !s().inconsistent() && idx < sz; idx++) { 752 literal bit1 = m_bits[v1][idx]; 753 literal bit2 = m_bits[v2][idx]; 754 CTRACE("bv", bit1 == ~bit2, tout << pp(v1) << pp(v2) << "idx: " << idx << "\n";); 755 if (bit1 == ~bit2) { 756 mk_new_diseq_axiom(v1, v2, idx); 757 return; 758 } 759 SASSERT(bit1 != ~bit2); 760 lbool val1 = s().value(bit1); 761 lbool val2 = s().value(bit2); 762 TRACE("bv", tout << "merge v" << v1 << " " << bit1 << ":= " << val1 << " " << bit2 << ":= " << val2 << "\n";); 763 if (val1 == val2) 764 continue; 765 CTRACE("bv", (val1 != l_undef && val2 != l_undef), tout << "inconsistent "; tout << pp(v1) << pp(v2) << "idx: " << idx << "\n";); 766 if (val1 == l_false) 767 assign_bit(~bit2, v1, v2, idx, ~bit1, true); 768 else if (val1 == l_true) 769 assign_bit(bit2, v1, v2, idx, bit1, true); 770 else if (val2 == l_false) 771 assign_bit(~bit1, v2, v1, idx, ~bit2, true); 772 else if (val2 == l_true) 773 assign_bit(bit1, v2, v1, idx, bit2, true); 774 } 775 } 776 mk_eq2bit_justification(theory_var v1,theory_var v2,sat::literal c,sat::literal a)777 sat::justification solver::mk_eq2bit_justification(theory_var v1, theory_var v2, sat::literal c, sat::literal a) { 778 void* mem = get_region().allocate(bv_justification::get_obj_size()); 779 sat::constraint_base::initialize(mem, this); 780 auto* constraint = new (sat::constraint_base::ptr2mem(mem)) bv_justification(v1, v2, c, a); 781 return sat::justification::mk_ext_justification(s().scope_lvl(), constraint->to_index()); 782 } 783 mk_bit2eq_justification(theory_var v1,theory_var v2)784 sat::ext_justification_idx solver::mk_bit2eq_justification(theory_var v1, theory_var v2) { 785 void* mem = get_region().allocate(bv_justification::get_obj_size()); 786 sat::constraint_base::initialize(mem, this); 787 auto* constraint = new (sat::constraint_base::ptr2mem(mem)) bv_justification(v1, v2); 788 return constraint->to_index(); 789 } 790 mk_bit2ne_justification(unsigned idx,sat::literal c)791 sat::justification solver::mk_bit2ne_justification(unsigned idx, sat::literal c) { 792 void* mem = get_region().allocate(bv_justification::get_obj_size()); 793 sat::constraint_base::initialize(mem, this); 794 auto* constraint = new (sat::constraint_base::ptr2mem(mem)) bv_justification(idx, c); 795 return sat::justification::mk_ext_justification(s().scope_lvl(), constraint->to_index()); 796 } 797 mk_ne2bit_justification(unsigned idx,theory_var v1,theory_var v2,sat::literal c,sat::literal a)798 sat::justification solver::mk_ne2bit_justification(unsigned idx, theory_var v1, theory_var v2, sat::literal c, sat::literal a) { 799 void* mem = get_region().allocate(bv_justification::get_obj_size()); 800 sat::constraint_base::initialize(mem, this); 801 auto* constraint = new (sat::constraint_base::ptr2mem(mem)) bv_justification(idx, v1, v2, c, a); 802 return sat::justification::mk_ext_justification(s().scope_lvl(), constraint->to_index()); 803 } 804 assign_bit(literal consequent,theory_var v1,theory_var v2,unsigned idx,literal antecedent,bool propagate_eqc)805 bool solver::assign_bit(literal consequent, theory_var v1, theory_var v2, unsigned idx, literal antecedent, bool propagate_eqc) { 806 m_stats.m_num_eq2bit++; 807 SASSERT(ctx.s().value(antecedent) == l_true); 808 SASSERT(m_bits[v2][idx].var() == consequent.var()); 809 SASSERT(consequent.var() != antecedent.var()); 810 s().assign(consequent, mk_eq2bit_justification(v1, v2, consequent, antecedent)); 811 if (s().value(consequent) == l_false) { 812 m_stats.m_num_conflicts++; 813 SASSERT(s().inconsistent()); 814 return false; 815 } 816 else { 817 if (m_wpos[v2] == idx) 818 find_wpos(v2); 819 bool_var cv = consequent.var(); 820 atom* a = get_bv2a(cv); 821 force_push(); 822 if (a) 823 for (auto curr : *a) 824 if (propagate_eqc || find(curr.first) != find(v2) || curr.second != idx) 825 m_prop_queue.push_back(propagation_item(curr)); 826 return true; 827 } 828 } 829 unmerge_eh(theory_var v1,theory_var v2)830 void solver::unmerge_eh(theory_var v1, theory_var v2) { 831 // v1 was the root of the equivalence class 832 // I must remove the zero_one_bits that are from v2. 833 zero_one_bits& bits = m_zero_one_bits[v1]; 834 if (bits.empty()) 835 return; 836 for (unsigned j = bits.size(); j-- > 0; ) { 837 zero_one_bit& bit = bits[j]; 838 if (find(bit.m_owner) == v1) { 839 bits.shrink(j + 1); 840 return; 841 } 842 } 843 bits.shrink(0); 844 } 845 merge_zero_one_bits(theory_var r1,theory_var r2)846 bool solver::merge_zero_one_bits(theory_var r1, theory_var r2) { 847 zero_one_bits& bits2 = m_zero_one_bits[r2]; 848 if (bits2.empty()) 849 return true; 850 zero_one_bits& bits1 = m_zero_one_bits[r1]; 851 unsigned bv_size = get_bv_size(r1); 852 SASSERT(bv_size == get_bv_size(r2)); 853 m_merge_aux[0].reserve(bv_size + 1, euf::null_theory_var); 854 m_merge_aux[1].reserve(bv_size + 1, euf::null_theory_var); 855 856 struct scoped_reset { 857 solver& s; 858 zero_one_bits& bits1; 859 scoped_reset(solver& s, zero_one_bits& bits1) :s(s), bits1(bits1) {} 860 ~scoped_reset() { 861 for (auto& zo : bits1) 862 s.m_merge_aux[zo.m_is_true][zo.m_idx] = euf::null_theory_var; 863 } 864 }; 865 scoped_reset _sr(*this, bits1); 866 867 DEBUG_CODE(for (unsigned i = 0; i < bv_size; i++) SASSERT(m_merge_aux[0][i] == euf::null_theory_var || m_merge_aux[1][i] == euf::null_theory_var);); 868 869 // save info about bits1 870 for (auto& zo : bits1) 871 m_merge_aux[zo.m_is_true][zo.m_idx] = zo.m_owner; 872 // check if bits2 is consistent with bits1, and copy new bits to bits1 873 for (auto& zo : bits2) { 874 theory_var v2 = zo.m_owner; 875 theory_var v1 = m_merge_aux[!zo.m_is_true][zo.m_idx]; 876 if (v1 != euf::null_theory_var) { 877 // conflict was detected ... v1 and v2 have complementary bits 878 SASSERT(m_bits[v1][zo.m_idx] == ~(m_bits[v2][zo.m_idx])); 879 SASSERT(m_bits[v1].size() == m_bits[v2].size()); 880 mk_new_diseq_axiom(v1, v2, zo.m_idx); 881 return false; 882 } 883 // copy missing variable to bits1 884 if (m_merge_aux[zo.m_is_true][zo.m_idx] == euf::null_theory_var) 885 bits1.push_back(zo); 886 } 887 // reset m_merge_aux vector 888 DEBUG_CODE(for (unsigned i = 0; i < bv_size; i++) { SASSERT(m_merge_aux[0][i] == euf::null_theory_var || m_merge_aux[1][i] == euf::null_theory_var); }); 889 return true; 890 } 891 power2(unsigned i) const892 rational const& solver::power2(unsigned i) const { 893 while (m_power2.size() <= i) 894 m_power2.push_back(m_bb.power(m_power2.size())); 895 return m_power2[i]; 896 } 897 898 } 899