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