1 /*++ 2 Copyright (c) 2020 Microsoft Corporation 3 4 Module Name: 5 6 bv_internalize.cpp 7 8 Abstract: 9 10 Internalize utilities for bit-vector solver plugin. 11 12 Author: 13 14 Nikolaj Bjorner (nbjorner) 2020-08-30 15 16 --*/ 17 18 #include "params/bv_rewriter_params.hpp" 19 #include "sat/smt/bv_solver.h" 20 #include "sat/smt/euf_solver.h" 21 #include "sat/smt/sat_th.h" 22 #include "tactic/tactic_exception.h" 23 24 namespace bv { 25 26 class solver::add_var_pos_trail : public trail<euf::solver> { 27 solver::atom* m_atom; 28 public: add_var_pos_trail(solver::atom * a)29 add_var_pos_trail(solver::atom* a) :m_atom(a) {} undo(euf::solver & euf)30 void undo(euf::solver& euf) override { 31 SASSERT(m_atom->m_occs); 32 m_atom->m_occs = m_atom->m_occs->m_next; 33 } 34 }; 35 36 class solver::add_eq_occurs_trail : public trail<euf::solver> { 37 atom* m_atom; 38 public: add_eq_occurs_trail(atom * a)39 add_eq_occurs_trail(atom* a) :m_atom(a) {} undo(euf::solver & euf)40 void undo(euf::solver& euf) override { 41 SASSERT(m_atom->m_eqs); 42 m_atom->m_eqs = m_atom->m_eqs->m_next; 43 if (m_atom->m_eqs) 44 m_atom->m_eqs->m_prev = nullptr; 45 } 46 }; 47 48 class solver::del_eq_occurs_trail : public trail<euf::solver> { 49 atom* m_atom; 50 eq_occurs* m_node; 51 public: del_eq_occurs_trail(atom * a,eq_occurs * n)52 del_eq_occurs_trail(atom* a, eq_occurs* n) : m_atom(a), m_node(n) {} undo(euf::solver & euf)53 void undo(euf::solver& euf) override { 54 if (m_node->m_next) 55 m_node->m_next->m_prev = m_node; 56 if (m_node->m_prev) 57 m_node->m_prev->m_next = m_node; 58 else 59 m_atom->m_eqs = m_node; 60 } 61 }; 62 del_eq_occurs(atom * a,eq_occurs * occ)63 void solver::del_eq_occurs(atom* a, eq_occurs* occ) { 64 eq_occurs* prev = occ->m_prev; 65 if (prev) 66 prev->m_next = occ->m_next; 67 else 68 a->m_eqs = occ->m_next; 69 if (occ->m_next) 70 occ->m_next->m_prev = prev; 71 ctx.push(del_eq_occurs_trail(a, occ)); 72 } 73 74 class solver::mk_atom_trail : public trail<euf::solver> { 75 solver& th; 76 sat::bool_var m_var; 77 public: mk_atom_trail(sat::bool_var v,solver & th)78 mk_atom_trail(sat::bool_var v, solver& th) : th(th), m_var(v) {} undo(euf::solver & euf)79 void undo(euf::solver& euf) override { 80 solver::atom* a = th.get_bv2a(m_var); 81 a->~atom(); 82 th.erase_bv2a(m_var); 83 } 84 }; 85 mk_var(euf::enode * n)86 euf::theory_var solver::mk_var(euf::enode* n) { 87 theory_var r = euf::th_euf_solver::mk_var(n); 88 m_find.mk_var(); 89 m_bits.push_back(sat::literal_vector()); 90 m_wpos.push_back(0); 91 m_zero_one_bits.push_back(zero_one_bits()); 92 ctx.attach_th_var(n, this, r); 93 TRACE("bv", tout << "mk-var: " << r << " " << n->get_expr_id() << " " << mk_bounded_pp(n->get_expr(), m) << "\n";); 94 return r; 95 } 96 apply_sort_cnstr(euf::enode * n,sort * s)97 void solver::apply_sort_cnstr(euf::enode * n, sort * s) { 98 force_push(); 99 get_var(n); 100 } 101 internalize(expr * e,bool sign,bool root,bool redundant)102 sat::literal solver::internalize(expr* e, bool sign, bool root, bool redundant) { 103 force_push(); 104 SASSERT(m.is_bool(e)); 105 if (!visit_rec(m, e, sign, root, redundant)) 106 return sat::null_literal; 107 sat::literal lit = expr2literal(e); 108 if (sign) 109 lit.neg(); 110 return lit; 111 } 112 internalize(expr * e,bool redundant)113 void solver::internalize(expr* e, bool redundant) { 114 force_push(); 115 visit_rec(m, e, false, false, redundant); 116 } 117 visit(expr * e)118 bool solver::visit(expr* e) { 119 if (!is_app(e) || to_app(e)->get_family_id() != get_id()) { 120 ctx.internalize(e, m_is_redundant); 121 return true; 122 } 123 m_stack.push_back(sat::eframe(e)); 124 return false; 125 } 126 visited(expr * e)127 bool solver::visited(expr* e) { 128 euf::enode* n = expr2enode(e); 129 return n && n->is_attached_to(get_id()); 130 } 131 post_visit(expr * e,bool sign,bool root)132 bool solver::post_visit(expr* e, bool sign, bool root) { 133 euf::enode* n = expr2enode(e); 134 app* a = to_app(e); 135 136 if (visited(e)) 137 return true; 138 139 SASSERT(!n || !n->is_attached_to(get_id())); 140 bool suppress_args = !get_config().m_bv_reflect && !m.is_considered_uninterpreted(a->get_decl()); 141 if (!n) 142 n = mk_enode(e, suppress_args); 143 144 SASSERT(!n->is_attached_to(get_id())); 145 mk_var(n); 146 SASSERT(n->is_attached_to(get_id())); 147 if (internalize_mode::no_delay_i != get_internalize_mode(a)) 148 mk_bits(n->get_th_var(get_id())); 149 else 150 internalize_circuit(a); 151 return true; 152 } 153 internalize_circuit(app * a)154 bool solver::internalize_circuit(app* a) { 155 156 std::function<void(unsigned sz, expr* const* xs, expr* const* ys, expr_ref_vector& bits)> bin; 157 std::function<void(unsigned sz, expr* const* xs, expr* const* ys, expr_ref& bit)> ebin; 158 std::function<void(unsigned sz, expr* const* xs, expr_ref_vector& bits)> un; 159 std::function<void(unsigned sz, expr* const* xs, unsigned p, expr_ref_vector& bits)> pun; 160 #define internalize_bin(F) bin = [&](unsigned sz, expr* const* xs, expr* const* ys, expr_ref_vector& bits) { m_bb.F(sz, xs, ys, bits); }; internalize_binary(a, bin); 161 #define internalize_un(F) un = [&](unsigned sz, expr* const* xs, expr_ref_vector& bits) { m_bb.F(sz, xs, bits);}; internalize_unary(a, un); 162 #define internalize_ac(F) bin = [&](unsigned sz, expr* const* xs, expr* const* ys, expr_ref_vector& bits) { m_bb.F(sz, xs, ys, bits); }; internalize_ac_binary(a, bin); 163 #define internalize_pun(F) pun = [&](unsigned sz, expr* const* xs, unsigned p, expr_ref_vector& bits) { m_bb.F(sz, xs, p, bits);}; internalize_par_unary(a, pun); 164 #define internalize_nfl(F) ebin = [&](unsigned sz, expr* const* xs, expr* const* ys, expr_ref& out) { m_bb.F(sz, xs, ys, out);}; internalize_novfl(a, ebin); 165 166 switch (a->get_decl_kind()) { 167 case OP_BV_NUM: internalize_num(a); break; 168 case OP_BNOT: internalize_un(mk_not); break; 169 case OP_BNEG: internalize_un(mk_neg); break; 170 case OP_BREDAND: internalize_un(mk_redand); break; 171 case OP_BREDOR: internalize_un(mk_redor); break; 172 case OP_BSDIV_I: internalize_bin(mk_sdiv); break; 173 case OP_BUDIV_I: internalize_bin(mk_udiv); break; 174 case OP_BUREM_I: internalize_bin(mk_urem); break; 175 case OP_BSREM_I: internalize_bin(mk_srem); break; 176 case OP_BSMOD_I: internalize_bin(mk_smod); break; 177 case OP_BSHL: internalize_bin(mk_shl); break; 178 case OP_BLSHR: internalize_bin(mk_lshr); break; 179 case OP_BASHR: internalize_bin(mk_ashr); break; 180 case OP_EXT_ROTATE_LEFT: internalize_bin(mk_ext_rotate_left); break; 181 case OP_EXT_ROTATE_RIGHT: internalize_bin(mk_ext_rotate_right); break; 182 case OP_BADD: internalize_ac(mk_adder); break; 183 case OP_BMUL: internalize_ac(mk_multiplier); break; 184 case OP_BAND: internalize_ac(mk_and); break; 185 case OP_BOR: internalize_ac(mk_or); break; 186 case OP_BXOR: internalize_ac(mk_xor); break; 187 case OP_BNAND: internalize_bin(mk_nand); break; 188 case OP_BNOR: internalize_bin(mk_nor); break; 189 case OP_BXNOR: internalize_bin(mk_xnor); break; 190 case OP_BCOMP: internalize_bin(mk_comp); break; 191 case OP_SIGN_EXT: internalize_pun(mk_sign_extend); break; 192 case OP_ZERO_EXT: internalize_pun(mk_zero_extend); break; 193 case OP_ROTATE_LEFT: internalize_pun(mk_rotate_left); break; 194 case OP_ROTATE_RIGHT: internalize_pun(mk_rotate_right); break; 195 case OP_BUMUL_NO_OVFL: internalize_nfl(mk_umul_no_overflow); break; 196 case OP_BSMUL_NO_OVFL: internalize_nfl(mk_smul_no_overflow); break; 197 case OP_BSMUL_NO_UDFL: internalize_nfl(mk_smul_no_underflow); break; 198 case OP_BIT2BOOL: internalize_bit2bool(a); break; 199 case OP_ULEQ: internalize_le<false, false, false>(a); break; 200 case OP_SLEQ: internalize_le<true, false, false>(a); break; 201 case OP_UGEQ: internalize_le<false, true, false>(a); break; 202 case OP_SGEQ: internalize_le<true, true, false>(a); break; 203 case OP_ULT: internalize_le<false, true, true>(a); break; 204 case OP_SLT: internalize_le<true, true, true>(a); break; 205 case OP_UGT: internalize_le<false, false, true>(a); break; 206 case OP_SGT: internalize_le<true, false, true>(a); break; 207 case OP_XOR3: internalize_xor3(a); break; 208 case OP_CARRY: internalize_carry(a); break; 209 case OP_BSUB: internalize_sub(a); break; 210 case OP_CONCAT: internalize_concat(a); break; 211 case OP_EXTRACT: internalize_extract(a); break; 212 case OP_MKBV: internalize_mkbv(a); break; 213 case OP_INT2BV: internalize_int2bv(a); break; 214 case OP_BV2INT: internalize_bv2int(a); break; 215 case OP_BUDIV: internalize_udiv(a); break; 216 case OP_BSDIV0: break; 217 case OP_BUDIV0: break; 218 case OP_BSREM0: break; 219 case OP_BUREM0: break; 220 case OP_BSMOD0: break; 221 default: 222 IF_VERBOSE(0, verbose_stream() << mk_bounded_pp(a, m) << "\n"); 223 UNREACHABLE(); 224 break; 225 } 226 return true; 227 } 228 mk_bits(theory_var v)229 void solver::mk_bits(theory_var v) { 230 TRACE("bv", tout << "v" << v << "@" << s().scope_lvl() << "\n";); 231 expr* e = var2expr(v); 232 unsigned bv_size = get_bv_size(v); 233 m_bits[v].reset(); 234 for (unsigned i = 0; i < bv_size; i++) { 235 expr_ref b2b(bv.mk_bit2bool(e, i), m); 236 m_bits[v].push_back(sat::null_literal); 237 sat::literal lit = ctx.internalize(b2b, false, false, m_is_redundant); 238 (void)lit; 239 TRACE("bv", tout << "add-bit: " << lit << " " << literal2expr(lit) << "\n";); 240 SASSERT(m_bits[v].back() == lit); 241 } 242 } 243 get_var(euf::enode * n)244 euf::theory_var solver::get_var(euf::enode* n) { 245 theory_var v = n->get_th_var(get_id()); 246 if (v == euf::null_theory_var) { 247 v = mk_var(n); 248 if (bv.is_bv(n->get_expr())) 249 mk_bits(v); 250 } 251 return v; 252 } 253 get_arg(euf::enode * n,unsigned idx)254 euf::enode* solver::get_arg(euf::enode* n, unsigned idx) { 255 app* o = to_app(n->get_expr()); 256 return ctx.get_enode(o->get_arg(idx)); 257 } 258 get_arg_var(euf::enode * n,unsigned idx)259 inline euf::theory_var solver::get_arg_var(euf::enode* n, unsigned idx) { 260 return get_var(get_arg(n, idx)); 261 } 262 get_bits(theory_var v,expr_ref_vector & r)263 void solver::get_bits(theory_var v, expr_ref_vector& r) { 264 for (literal lit : m_bits[v]) 265 r.push_back(literal2expr(lit)); 266 } 267 get_bits(euf::enode * n,expr_ref_vector & r)268 inline void solver::get_bits(euf::enode* n, expr_ref_vector& r) { 269 get_bits(get_var(n), r); 270 } 271 get_arg_bits(app * n,unsigned idx,expr_ref_vector & r)272 inline void solver::get_arg_bits(app* n, unsigned idx, expr_ref_vector& r) { 273 app* arg = to_app(n->get_arg(idx)); 274 get_bits(ctx.get_enode(arg), r); 275 } 276 register_true_false_bit(theory_var v,unsigned idx)277 void solver::register_true_false_bit(theory_var v, unsigned idx) { 278 SASSERT(s().value(m_bits[v][idx]) != l_undef); 279 bool is_true = (s().value(m_bits[v][idx]) == l_true); 280 zero_one_bits& bits = m_zero_one_bits[v]; 281 bits.push_back(zero_one_bit(v, idx, is_true)); 282 } 283 284 /** 285 \brief Add bit l to the given variable. 286 */ add_bit(theory_var v,literal l)287 void solver::add_bit(theory_var v, literal l) { 288 unsigned idx = m_bits[v].size(); 289 m_bits[v].push_back(l); 290 TRACE("bv", tout << "add-bit: v" << v << "[" << idx << "] " << l << " " << literal2expr(l) << "@" << s().scope_lvl() << "\n";); 291 SASSERT(m_num_scopes == 0); 292 s().set_external(l.var()); 293 euf::enode* n = bool_var2enode(l.var()); 294 if (!n->is_attached_to(get_id())) 295 mk_var(n); 296 297 set_bit_eh(v, l, idx); 298 } 299 mk_atom(sat::bool_var bv)300 solver::atom* solver::mk_atom(sat::bool_var bv) { 301 atom* a = get_bv2a(bv); 302 if (a) 303 return a; 304 a = new (get_region()) atom(bv); 305 insert_bv2a(bv, a); 306 ctx.push(mk_atom_trail(bv, *this)); 307 return a; 308 } 309 set_bit_eh(theory_var v,literal l,unsigned idx)310 void solver::set_bit_eh(theory_var v, literal l, unsigned idx) { 311 SASSERT(m_bits[v][idx] == l); 312 if (s().value(l) != l_undef && s().lvl(l) == 0) 313 register_true_false_bit(v, idx); 314 else { 315 atom* b = mk_atom(l.var()); 316 if (b->m_occs) 317 find_new_diseq_axioms(*b, v, idx); 318 ctx.push(add_var_pos_trail(b)); 319 b->m_occs = new (get_region()) var_pos_occ(v, idx, b->m_occs); 320 } 321 } 322 init_bits(expr * e,expr_ref_vector const & bits)323 void solver::init_bits(expr* e, expr_ref_vector const& bits) { 324 euf::enode* n = expr2enode(e); 325 SASSERT(get_bv_size(n) == bits.size()); 326 SASSERT(euf::null_theory_var != n->get_th_var(get_id())); 327 theory_var v = n->get_th_var(get_id()); 328 329 if (!m_bits[v].empty()) { 330 SASSERT(bits.size() == m_bits[v].size()); 331 unsigned i = 0; 332 for (expr* bit : bits) { 333 sat::literal lit = ctx.internalize(bit, false, false, m_is_redundant); 334 TRACE("bv", tout << "set " << m_bits[v][i] << " == " << lit << "\n";); 335 add_clause(~lit, m_bits[v][i]); 336 add_clause(lit, ~m_bits[v][i]); 337 ++i; 338 } 339 return; 340 } 341 for (expr* bit : bits) 342 add_bit(v, ctx.internalize(bit, false, false, m_is_redundant)); 343 for (expr* bit : bits) 344 get_var(expr2enode(bit)); 345 SASSERT(get_bv_size(n) == bits.size()); 346 find_wpos(v); 347 } 348 get_bv_size(euf::enode * n)349 unsigned solver::get_bv_size(euf::enode* n) { 350 return bv.get_bv_size(n->get_expr()); 351 } 352 get_bv_size(theory_var v)353 unsigned solver::get_bv_size(theory_var v) { 354 return get_bv_size(var2enode(v)); 355 } 356 internalize_num(app * a)357 void solver::internalize_num(app* a) { 358 numeral val; 359 unsigned sz = 0; 360 euf::enode* n = expr2enode(a); 361 theory_var v = n->get_th_var(get_id()); 362 SASSERT(n->interpreted()); 363 VERIFY(bv.is_numeral(a, val, sz)); 364 expr_ref_vector bits(m); 365 m_bb.num2bits(val, sz, bits); 366 SASSERT(bits.size() == sz); 367 SASSERT(m_bits[v].empty()); 368 sat::literal true_literal = ctx.internalize(m.mk_true(), false, false, false); 369 for (unsigned i = 0; i < sz; i++) { 370 expr* l = bits.get(i); 371 SASSERT(m.is_true(l) || m.is_false(l)); 372 m_bits[v].push_back(m.is_true(l) ? true_literal : ~true_literal); 373 register_true_false_bit(v, i); 374 } 375 fixed_var_eh(v); 376 } 377 internalize_mkbv(app * n)378 void solver::internalize_mkbv(app* n) { 379 expr_ref_vector bits(m); 380 bits.append(n->get_num_args(), n->get_args()); 381 init_bits(n, bits); 382 } 383 internalize_bv2int(app * n)384 void solver::internalize_bv2int(app* n) { 385 assert_bv2int_axiom(n); 386 } 387 388 /** 389 * create the axiom: 390 * n = bv2int(k) = ite(bit2bool(k[sz-1],2^{sz-1},0) + ... + ite(bit2bool(k[0],1,0)) 391 */ 392 assert_bv2int_axiom(app * n)393 void solver::assert_bv2int_axiom(app* n) { 394 expr* k = nullptr; 395 VERIFY(bv.is_bv2int(n, k)); 396 SASSERT(bv.is_bv_sort(m.get_sort(k))); 397 expr_ref_vector k_bits(m); 398 euf::enode* k_enode = expr2enode(k); 399 get_bits(k_enode, k_bits); 400 unsigned sz = bv.get_bv_size(k); 401 expr_ref_vector args(m); 402 expr_ref zero(m_autil.mk_int(0), m); 403 unsigned i = 0; 404 for (expr* b : k_bits) 405 args.push_back(m.mk_ite(b, m_autil.mk_int(power2(i++)), zero)); 406 expr_ref sum(m_autil.mk_add(sz, args.c_ptr()), m); 407 expr_ref eq = mk_eq(n, sum); 408 sat::literal lit = ctx.internalize(eq, false, false, m_is_redundant); 409 add_unit(lit); 410 } 411 internalize_int2bv(app * n)412 void solver::internalize_int2bv(app* n) { 413 SASSERT(bv.is_int2bv(n)); 414 euf::enode* e = expr2enode(n); 415 mk_bits(e->get_th_var(get_id())); 416 assert_int2bv_axiom(n); 417 } 418 419 /** 420 * create the axiom: 421 * bv2int(n) = e mod 2^bit_width 422 * where n = int2bv(e) 423 * 424 * Create the axioms: 425 * bit2bool(i,n) == ((e div 2^i) mod 2 != 0) 426 * for i = 0,.., sz-1 427 */ assert_int2bv_axiom(app * n)428 void solver::assert_int2bv_axiom(app* n) { 429 expr* e = nullptr; 430 VERIFY(bv.is_int2bv(n, e)); 431 euf::enode* n_enode = expr2enode(n); 432 expr_ref lhs(m), rhs(m); 433 lhs = bv.mk_bv2int(n); 434 unsigned sz = bv.get_bv_size(n); 435 numeral mod = power(numeral(2), sz); 436 rhs = m_autil.mk_mod(e, m_autil.mk_int(mod)); 437 expr_ref eq = mk_eq(lhs, rhs); 438 TRACE("bv", tout << eq << "\n";); 439 add_unit(ctx.internalize(eq, false, false, m_is_redundant)); 440 441 expr_ref_vector n_bits(m); 442 get_bits(n_enode, n_bits); 443 444 for (unsigned i = 0; i < sz; ++i) { 445 numeral div = power2(i); 446 rhs = m_autil.mk_idiv(e, m_autil.mk_int(div)); 447 rhs = m_autil.mk_mod(rhs, m_autil.mk_int(2)); 448 rhs = mk_eq(rhs, m_autil.mk_int(1)); 449 lhs = n_bits.get(i); 450 expr_ref eq = mk_eq(lhs, rhs); 451 TRACE("bv", tout << eq << "\n";); 452 add_unit(ctx.internalize(eq, false, false, m_is_redundant)); 453 } 454 } 455 456 template<bool Signed, bool Rev, bool Negated> internalize_le(app * n)457 void solver::internalize_le(app* n) { 458 SASSERT(n->get_num_args() == 2); 459 expr_ref_vector arg1_bits(m), arg2_bits(m); 460 get_arg_bits(n, Rev ? 1 : 0, arg1_bits); 461 get_arg_bits(n, Rev ? 0 : 1, arg2_bits); 462 expr_ref le(m); 463 if (Signed) 464 m_bb.mk_sle(arg1_bits.size(), arg1_bits.c_ptr(), arg2_bits.c_ptr(), le); 465 else 466 m_bb.mk_ule(arg1_bits.size(), arg1_bits.c_ptr(), arg2_bits.c_ptr(), le); 467 literal def = ctx.internalize(le, false, false, m_is_redundant); 468 if (Negated) 469 def.neg(); 470 add_def(def, expr2literal(n)); 471 } 472 internalize_carry(app * n)473 void solver::internalize_carry(app* n) { 474 SASSERT(n->get_num_args() == 3); 475 literal r = expr2literal(n); 476 literal l1 = expr2literal(n->get_arg(0)); 477 literal l2 = expr2literal(n->get_arg(1)); 478 literal l3 = expr2literal(n->get_arg(2)); 479 add_clause(~r, l1, l2); 480 add_clause(~r, l1, l3); 481 add_clause(~r, l2, l3); 482 add_clause(r, ~l1, ~l2); 483 add_clause(r, ~l1, ~l3); 484 add_clause(r, ~l2, ~l3); 485 } 486 internalize_xor3(app * n)487 void solver::internalize_xor3(app* n) { 488 SASSERT(n->get_num_args() == 3); 489 literal r = expr2literal(n); 490 literal l1 = expr2literal(n->get_arg(0)); 491 literal l2 = expr2literal(n->get_arg(1)); 492 literal l3 = expr2literal(n->get_arg(2)); 493 add_clause(~r, l1, l2, l3); 494 add_clause(~r, ~l1, ~l2, l3); 495 add_clause(~r, ~l1, l2, ~l3); 496 add_clause(~r, l1, ~l2, ~l3); 497 add_clause(r, ~l1, l2, l3); 498 add_clause(r, l1, ~l2, l3); 499 add_clause(r, l1, l2, ~l3); 500 add_clause(r, ~l1, ~l2, ~l3); 501 } 502 internalize_udiv_i(app * a)503 void solver::internalize_udiv_i(app* a) { 504 std::function<void(unsigned sz, expr* const* xs, expr* const* ys, expr_ref_vector& bits)> bin; 505 bin = [&](unsigned sz, expr* const* xs, expr* const* ys, expr_ref_vector& bits) { m_bb.mk_udiv(sz, xs, ys, bits); }; 506 internalize_binary(a, bin); 507 } 508 internalize_udiv(app * n)509 void solver::internalize_udiv(app* n) { 510 bv_rewriter_params p(s().params()); 511 expr* arg1 = n->get_arg(0); 512 expr* arg2 = n->get_arg(1); 513 if (p.hi_div0()) { 514 add_unit(eq_internalize(n, bv.mk_bv_udiv_i(arg1, arg2))); 515 return; 516 } 517 unsigned sz = bv.get_bv_size(n); 518 expr_ref zero(bv.mk_numeral(0, sz), m); 519 expr_ref eq(m.mk_eq(arg2, zero), m); 520 expr_ref udiv(m.mk_ite(eq, bv.mk_bv_udiv0(arg1), bv.mk_bv_udiv_i(arg1, arg2)), m); 521 add_unit(eq_internalize(n, udiv)); 522 } 523 internalize_unary(app * n,std::function<void (unsigned,expr * const *,expr_ref_vector &)> & fn)524 void solver::internalize_unary(app* n, std::function<void(unsigned, expr* const*, expr_ref_vector&)>& fn) { 525 SASSERT(n->get_num_args() == 1); 526 expr_ref_vector arg1_bits(m), bits(m); 527 get_arg_bits(n, 0, arg1_bits); 528 fn(arg1_bits.size(), arg1_bits.c_ptr(), bits); 529 init_bits(n, bits); 530 } 531 internalize_par_unary(app * n,std::function<void (unsigned,expr * const *,unsigned p,expr_ref_vector &)> & fn)532 void solver::internalize_par_unary(app* n, std::function<void(unsigned, expr* const*, unsigned p, expr_ref_vector&)>& fn) { 533 SASSERT(n->get_num_args() == 1); 534 expr_ref_vector arg1_bits(m), bits(m); 535 get_arg_bits(n, 0, arg1_bits); 536 unsigned param = n->get_decl()->get_parameter(0).get_int(); 537 fn(arg1_bits.size(), arg1_bits.c_ptr(), param, bits); 538 init_bits(n, bits); 539 } 540 internalize_binary(app * e,std::function<void (unsigned,expr * const *,expr * const *,expr_ref_vector &)> & fn)541 void solver::internalize_binary(app* e, std::function<void(unsigned, expr* const*, expr* const*, expr_ref_vector&)>& fn) { 542 SASSERT(e->get_num_args() == 2); 543 expr_ref_vector arg1_bits(m), arg2_bits(m), bits(m); 544 get_arg_bits(e, 0, arg1_bits); 545 get_arg_bits(e, 1, arg2_bits); 546 SASSERT(arg1_bits.size() == arg2_bits.size()); 547 fn(arg1_bits.size(), arg1_bits.c_ptr(), arg2_bits.c_ptr(), bits); 548 init_bits(e, bits); 549 } 550 internalize_ac_binary(app * e,std::function<void (unsigned,expr * const *,expr * const *,expr_ref_vector &)> & fn)551 void solver::internalize_ac_binary(app* e, std::function<void(unsigned, expr* const*, expr* const*, expr_ref_vector&)>& fn) { 552 SASSERT(e->get_num_args() >= 2); 553 expr_ref_vector bits(m), new_bits(m), arg_bits(m); 554 unsigned i = e->get_num_args() - 1; 555 get_arg_bits(e, i, bits); 556 for (; i-- > 0; ) { 557 arg_bits.reset(); 558 get_arg_bits(e, i, arg_bits); 559 SASSERT(arg_bits.size() == bits.size()); 560 new_bits.reset(); 561 fn(arg_bits.size(), arg_bits.c_ptr(), bits.c_ptr(), new_bits); 562 bits.swap(new_bits); 563 } 564 init_bits(e, bits); 565 TRACE("bv_verbose", tout << arg_bits << " " << bits << " " << new_bits << "\n";); 566 } 567 internalize_novfl(app * n,std::function<void (unsigned,expr * const *,expr * const *,expr_ref &)> & fn)568 void solver::internalize_novfl(app* n, std::function<void(unsigned, expr* const*, expr* const*, expr_ref&)>& fn) { 569 SASSERT(n->get_num_args() == 2); 570 expr_ref_vector arg1_bits(m), arg2_bits(m); 571 get_arg_bits(n, 0, arg1_bits); 572 get_arg_bits(n, 1, arg2_bits); 573 expr_ref out(m); 574 fn(arg1_bits.size(), arg1_bits.c_ptr(), arg2_bits.c_ptr(), out); 575 sat::literal def = ctx.internalize(out, false, false, m_is_redundant); 576 add_def(def, expr2literal(n)); 577 } 578 add_def(sat::literal def,sat::literal l)579 void solver::add_def(sat::literal def, sat::literal l) { 580 atom* a = new (get_region()) atom(l.var()); 581 a->m_var = l; 582 a->m_def = def; 583 insert_bv2a(l.var(), a); 584 ctx.push(mk_atom_trail(l.var(), *this)); 585 add_clause(l, ~def); 586 add_clause(def, ~l); 587 } 588 internalize_concat(app * n)589 void solver::internalize_concat(app* n) { 590 euf::enode* e = expr2enode(n); 591 theory_var v = e->get_th_var(get_id()); 592 m_bits[v].reset(); 593 for (unsigned i = n->get_num_args(); i-- > 0; ) 594 for (literal lit : m_bits[get_arg_var(e, i)]) 595 add_bit(v, lit); 596 find_wpos(v); 597 } 598 internalize_sub(app * n)599 void solver::internalize_sub(app* n) { 600 SASSERT(n->get_num_args() == 2); 601 expr_ref_vector arg1_bits(m), arg2_bits(m), bits(m); 602 get_arg_bits(n, 0, arg1_bits); 603 get_arg_bits(n, 1, arg2_bits); 604 SASSERT(arg1_bits.size() == arg2_bits.size()); 605 expr_ref carry(m); 606 m_bb.mk_subtracter(arg1_bits.size(), arg1_bits.c_ptr(), arg2_bits.c_ptr(), bits, carry); 607 init_bits(n, bits); 608 } 609 internalize_extract(app * e)610 void solver::internalize_extract(app* e) { 611 expr* arg_e = nullptr; 612 unsigned lo = 0, hi = 0; 613 VERIFY(bv.is_extract(e, lo, hi, arg_e)); 614 euf::enode* n = expr2enode(e); 615 theory_var v = n->get_th_var(get_id()); 616 theory_var arg_v = get_arg_var(n, 0); 617 SASSERT(hi - lo + 1 == get_bv_size(v)); 618 SASSERT(lo <= hi && hi < get_bv_size(arg_v)); 619 m_bits[v].reset(); 620 for (unsigned i = lo; i <= hi; ++i) 621 add_bit(v, m_bits[arg_v][i]); 622 find_wpos(v); 623 } 624 internalize_bit2bool(app * n)625 void solver::internalize_bit2bool(app* n) { 626 unsigned idx = 0; 627 expr* arg = nullptr; 628 VERIFY(bv.is_bit2bool(n, arg, idx)); 629 euf::enode* argn = expr2enode(arg); 630 if (!argn->is_attached_to(get_id())) { 631 mk_var(argn); 632 } 633 theory_var v_arg = argn->get_th_var(get_id()); 634 unsigned arg_sz = get_bv_size(v_arg); 635 SASSERT(idx < arg_sz); 636 sat::literal lit = expr2literal(n); 637 sat::literal lit0 = m_bits[v_arg][idx]; 638 if (lit0 == sat::null_literal) { 639 m_bits[v_arg][idx] = lit; 640 TRACE("bv", tout << "add-bit: " << lit << " " << literal2expr(lit) << "\n";); 641 if (arg_sz > 1) { 642 atom* a = new (get_region()) atom(lit.var()); 643 a->m_occs = new (get_region()) var_pos_occ(v_arg, idx); 644 insert_bv2a(lit.var(), a); 645 ctx.push(mk_atom_trail(lit.var(), *this)); 646 } 647 } 648 else if (lit != lit0) { 649 add_clause(lit0, ~lit); 650 add_clause(~lit0, lit); 651 } 652 653 // validate_atoms(); 654 // axiomatize bit2bool on constants. 655 rational val; 656 unsigned sz; 657 if (bv.is_numeral(arg, val, sz)) { 658 rational bit; 659 div(val, rational::power_of_two(idx), bit); 660 mod(bit, rational(2), bit); 661 if (bit.is_zero()) lit.neg(); 662 add_unit(lit); 663 } 664 } 665 eq_internalized(euf::enode * n)666 void solver::eq_internalized(euf::enode* n) { 667 SASSERT(m.is_eq(n->get_expr())); 668 sat::literal lit = literal(n->bool_var(), false); 669 theory_var v1 = n->get_arg(0)->get_th_var(get_id()); 670 theory_var v2 = n->get_arg(1)->get_th_var(get_id()); 671 SASSERT(v1 != euf::null_theory_var); 672 SASSERT(v2 != euf::null_theory_var); 673 674 #if 0 675 if (!n->is_attached_to(get_id())) 676 mk_var(n); 677 #endif 678 679 unsigned sz = m_bits[v1].size(); 680 if (sz == 1) { 681 literal bit1 = m_bits[v1][0]; 682 literal bit2 = m_bits[v2][0]; 683 add_clause(~lit, ~bit1, bit2); 684 add_clause(~lit, ~bit2, bit1); 685 add_clause(~bit1, ~bit2, lit); 686 add_clause(bit2, bit1, lit); 687 return; 688 } 689 for (unsigned i = 0; i < sz; ++i) { 690 literal bit1 = m_bits[v1][i]; 691 literal bit2 = m_bits[v2][i]; 692 lbool val1 = s().value(bit1); 693 lbool val2 = s().value(bit2); 694 if (val1 != l_undef) 695 eq_internalized(bit2.var(), bit1.var(), i, v2, v1, lit, n); 696 else if (val2 != l_undef) 697 eq_internalized(bit1.var(), bit2.var(), i, v1, v2, lit, n); 698 else if ((s().rand()() % 2) == 0) 699 eq_internalized(bit2.var(), bit1.var(), i, v2, v1, lit, n); 700 else 701 eq_internalized(bit1.var(), bit2.var(), i, v1, v2, lit, n); 702 } 703 } 704 eq_internalized(sat::bool_var b1,sat::bool_var b2,unsigned idx,theory_var v1,theory_var v2,literal lit,euf::enode * n)705 void solver::eq_internalized(sat::bool_var b1, sat::bool_var b2, unsigned idx, theory_var v1, theory_var v2, literal lit, euf::enode* n) { 706 atom* a = mk_atom(b1); 707 if (a) { 708 ctx.push(add_eq_occurs_trail(a)); 709 auto* next = a->m_eqs; 710 a->m_eqs = new (get_region()) eq_occurs(b1, b2, idx, v1, v2, lit, n, next); 711 if (next) 712 next->m_prev = a->m_eqs; 713 } 714 } 715 assert_ackerman(theory_var v1,theory_var v2)716 void solver::assert_ackerman(theory_var v1, theory_var v2) { 717 if (v1 == v2) 718 return; 719 if (v1 > v2) 720 std::swap(v1, v2); 721 flet<bool> _red(m_is_redundant, true); 722 ++m_stats.m_ackerman; 723 expr* o1 = var2expr(v1); 724 expr* o2 = var2expr(v2); 725 expr_ref oe = mk_var_eq(v1, v2); 726 literal oeq = ctx.internalize(oe, false, false, m_is_redundant); 727 unsigned sz = m_bits[v1].size(); 728 TRACE("bv", tout << "ackerman-eq: " << s().scope_lvl() << " " << oe << "\n";); 729 literal_vector eqs; 730 eqs.push_back(oeq); 731 for (unsigned i = 0; i < sz; ++i) { 732 expr_ref e1(m), e2(m); 733 e1 = bv.mk_bit2bool(o1, i); 734 e2 = bv.mk_bit2bool(o2, i); 735 expr_ref e = mk_eq(e1, e2); 736 literal eq = ctx.internalize(e, false, false, m_is_redundant); 737 add_clause(eq, ~oeq); 738 eqs.push_back(~eq); 739 } 740 TRACE("bv", for (auto l : eqs) tout << mk_bounded_pp(literal2expr(l), m) << " "; tout << "\n";); 741 s().add_clause(eqs.size(), eqs.c_ptr(), sat::status::th(m_is_redundant, get_id())); 742 } 743 } 744