136 void bit_blaster_tpl<Cfg>::mk_adder(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr…  in mk_adder()  argument
142             mk_full_adder(a_bits[idx], b_bits[idx], cin, out, cout);  in mk_adder()
144             mk_xor3(a_bits[idx], b_bits[idx], cin, out);  in mk_adder()
157 void bit_blaster_tpl<Cfg>::mk_subtracter(unsigned sz, expr * const * a_bits, expr * const * b_bits,…  in mk_subtracter()  argument
163         mk_not(b_bits[j], not_b);  in mk_subtracter()
172         std::cout << mk_pp(b_bits[j], m()) << "\n";  in mk_subtracter()
180 void bit_blaster_tpl<Cfg>::mk_multiplier(unsigned sz, expr * const * a_bits, expr * const * b_bits,…  in mk_multiplier()  argument
185         std::swap(a_bits, b_bits);  in mk_multiplier()
186     if (is_minus_one(sz, b_bits)) {  in mk_multiplier()
198     if (mk_const_case_multiplier(sz, a_bits, b_bits, out_bits)) {  in mk_multiplier()
212     mk_and(a_bits[0], b_bits[0], out);  in mk_multiplier()
242         mk_and(a_bits[0], b_bits[i], i1);  in mk_multiplier()
243         mk_and(a_bits[1], b_bits[i - 1], i2);  in mk_multiplier()
251                 mk_and(a_bits[j], b_bits[i - j], i3);  in mk_multiplier()
263                 mk_and(a_bits[j], b_bits[i - j], i3);  in mk_multiplier()
274 …Cfg>::mk_umul_no_overflow(unsigned sz, expr* const* a_bits, expr* const* b_bits, expr_ref& result)…  in mk_umul_no_overflow()  argument
281     ext_b_bits.append(sz, b_bits);  in mk_umul_no_overflow()
303         mk_and(ovf, b_bits[i], tmp);  in mk_umul_no_overflow()
313 …mul_no_overflow_core(unsigned sz, expr * const * a_bits,  expr * const * b_bits, bool is_overflow,…  in mk_smul_no_overflow_core()  argument
320     ext_b_bits.append(sz, b_bits);  in mk_smul_no_overflow_core()
322     ext_b_bits.push_back(b_bits[sz-1]);  in mk_smul_no_overflow_core()
345         mk_xor(b_bits[sz-1], b_bits[i], b);  in mk_smul_no_overflow_core()
358         mk_iff(a_bits[sz-1], b_bits[sz-1], sign);  in mk_smul_no_overflow_core()
363         mk_xor(a_bits[sz-1], b_bits[sz-1], sign);  in mk_smul_no_overflow_core()
370 …:mk_smul_no_overflow(unsigned sz, expr * const * a_bits,  expr * const * b_bits, expr_ref & result…  in mk_smul_no_overflow()  argument
371     mk_smul_no_overflow_core(sz, a_bits, b_bits, true, result);  in mk_smul_no_overflow()
375 …mk_smul_no_underflow(unsigned sz, expr * const * a_bits,  expr * const * b_bits, expr_ref & result…  in mk_smul_no_underflow()  argument
376     mk_smul_no_overflow_core(sz, a_bits, b_bits, false, result);  in mk_smul_no_underflow()
380 void bit_blaster_tpl<Cfg>::mk_udiv_urem(unsigned sz, expr * const * a_bits, expr * const * b_bits, …  in mk_udiv_urem()  argument
401         mk_subtracter(sz, p.data(), b_bits, t, q);  in mk_udiv_urem()
430           for (unsigned i = 0; i < sz; ++i) tout << mk_pp(b_bits[i], m()) << " ";                in mk_udiv_urem()
440 void bit_blaster_tpl<Cfg>::mk_udiv(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_…  in mk_udiv()  argument
442     mk_udiv_urem(sz, a_bits, b_bits, q_bits, aux);  in mk_udiv()
446 void bit_blaster_tpl<Cfg>::mk_urem(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_…  in mk_urem()  argument
448     mk_udiv_urem(sz, a_bits, b_bits, aux, r_bits);  in mk_urem()
482 …g>::mk_sdiv_srem_smod(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector &…  in mk_sdiv_srem_smod()  argument
488     expr * b_msb   = b_bits[sz - 1];  in mk_sdiv_srem_smod()
494     mk_neg(sz, b_bits, neg_b_bits);  in mk_sdiv_srem_smod()
499         mk_udiv_urem(sz, a_bits, b_bits, pp_q, pp_r);  in mk_sdiv_srem_smod()
507         mk_udiv_urem(sz, neg_a_bits.data(), b_bits, np_q, np_r);  in mk_sdiv_srem_smod()
580             mk_subtracter(sz, b_bits, np_r.data(), np_out, cout);  in mk_sdiv_srem_smod()
586             mk_adder(sz, b_bits, pn_r.data(), pn_out);  in mk_sdiv_srem_smod()
600 void bit_blaster_tpl<Cfg>::mk_sdiv(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_…  in mk_sdiv()  argument
602     expr * b_msb = b_bits[sz - 1];  in mk_sdiv()
604         mk_udiv(sz, a_bits, b_bits, out_bits);  in mk_sdiv()
608         mk_neg(sz, b_bits, neg_b_bits);  in mk_sdiv()
617         mk_udiv(sz, neg_a_bits.data(), b_bits, tmp);  in mk_sdiv()
624         mk_neg(sz, b_bits, neg_b_bits);  in mk_sdiv()
630         mk_sdiv_srem_smod<SDIV>(sz, a_bits, b_bits, out_bits);  in mk_sdiv()
636         mk_abs(sz, b_bits, abs_b_bits);  in mk_sdiv()
649 void bit_blaster_tpl<Cfg>::mk_srem(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_…  in mk_srem()  argument
651     expr * b_msb = b_bits[sz - 1];  in mk_srem()
653         mk_urem(sz, a_bits, b_bits, out_bits);  in mk_srem()
657         mk_neg(sz, b_bits, neg_b_bits);  in mk_srem()
664         mk_urem(sz, neg_a_bits.data(), b_bits, tmp);  in mk_srem()
671         mk_neg(sz, b_bits, neg_b_bits);  in mk_srem()
679         mk_sdiv_srem_smod<SREM>(sz, a_bits, b_bits, out_bits);  in mk_srem()
685         mk_abs(sz, b_bits, abs_b_bits);  in mk_srem()
730 void bit_blaster_tpl<Cfg>::mk_smod(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_…  in mk_smod()  argument
732     expr * b_msb = b_bits[sz - 1];  in mk_smod()
737     mk_abs(sz, b_bits, abs_b_bits);  in mk_smod()
743     mk_adder(sz, neg_u_bits.data(), b_bits, neg_u_add_b);  in mk_smod()
745     mk_adder(sz, u_bits.data(), b_bits, u_add_b);  in mk_smod()
767 void bit_blaster_tpl<Cfg>::mk_eq(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_re…  in mk_eq()  argument
770         mk_iff(a_bits[i], b_bits[i], out);  in mk_eq()
849 void bit_blaster_tpl<Cfg>::mk_shl(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_r…  in mk_shl()  argument
851     if (is_numeral(sz, b_bits, k)) {  in mk_shl()
874                 mk_ite(b_bits[i], a_j, out_bits[j].get(), new_out);  in mk_shl()
884             mk_or(is_large, b_bits[i], is_large);  in mk_shl()
895 void bit_blaster_tpl<Cfg>::mk_lshr(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_…  in mk_lshr()  argument
897     if (is_numeral(sz, b_bits, k)) {  in mk_lshr()
918                 mk_ite(b_bits[i], a_j, out_bits[j].get(), new_out);  in mk_lshr()
927             mk_or(is_large, b_bits[i], is_large);  in mk_lshr()
938 void bit_blaster_tpl<Cfg>::mk_ashr(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_…  in mk_ashr()  argument
940     if (is_numeral(sz, b_bits, k)) {  in mk_ashr()
961                 mk_ite(b_bits[i], a_j, out_bits[j].get(), new_out);  in mk_ashr()
970             mk_or(is_large, b_bits[i], is_large);  in mk_ashr()
982 …ext_rotate_left_right(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector &…  in mk_ext_rotate_left_right()  argument
984     if (is_numeral(sz, b_bits, k) && k.is_unsigned()) {  in mk_ext_rotate_left_right()
1001         mk_urem(sz, b_bits, sz_bits.data(), masked_b_bits);  in mk_ext_rotate_left_right()
1019 …>::mk_ext_rotate_left(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector &…  in mk_ext_rotate_left()  argument
1020     mk_ext_rotate_left_right<true>(sz, a_bits, b_bits, out_bits);  in mk_ext_rotate_left()
1024 …::mk_ext_rotate_right(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector &…  in mk_ext_rotate_right()  argument
1025     mk_ext_rotate_left_right<false>(sz, a_bits, b_bits, out_bits);  in mk_ext_rotate_right()
1030 void bit_blaster_tpl<Cfg>::mk_le(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_re…  in mk_le()  argument
1034     mk_or(not_a, b_bits[0], out);  in mk_le()
1037         mk_ge2(not_a, b_bits[idx], out, out);  in mk_le()
1041         mk_not(b_bits[sz-1], not_b);  in mk_le()
1047 void bit_blaster_tpl<Cfg>::mk_sle(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_r…  in mk_sle()  argument
1048     mk_le<true>(sz, a_bits, b_bits, out);  in mk_sle()
1052 void bit_blaster_tpl<Cfg>::mk_ule(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_r…  in mk_ule()  argument
1053     mk_le<false>(sz, a_bits, b_bits, out);  in mk_ule()
1067 void bit_blaster_tpl<Cfg>::NAME(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref…
1070 …OP(a_bits[i], b_bits[i], t);                                                                      …
1097 void bit_blaster_tpl<Cfg>::mk_comp(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_…  in mk_comp()  argument
1099     mk_eq(sz, a_bits, b_bits, tmp);  in mk_comp()
1104 …::mk_carry_save_adder(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr * const * c_…  in mk_carry_save_adder()  argument
1107         mk_xor3(a_bits[i], b_bits[i], c_bits[i], t);  in mk_carry_save_adder()
1109         mk_carry(a_bits[i], b_bits[i], c_bits[i], t);  in mk_carry_save_adder()
1115 …const_case_multiplier(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector &…  in mk_const_case_multiplier()  argument
1121         if (!is_bool_const(b_bits[i]))   in mk_const_case_multiplier()
1131     nb_bits.append(sz, b_bits);  in mk_const_case_multiplier()
1137 …ed i, unsigned sz, ptr_buffer<expr, 128>& a_bits, ptr_buffer<expr, 128>& b_bits, expr_ref_vector &…  in mk_const_case_multiplier()  argument
1143     while (!is_a && i < sz && is_bool_const(b_bits[i]))   in mk_const_case_multiplier()
1148         x = is_a?a_bits[i]:b_bits[i];  in mk_const_case_multiplier()
1149         if (is_a) a_bits[i] = m().mk_true(); else b_bits[i] = m().mk_true();  in mk_const_case_multiplier()
1150         mk_const_case_multiplier(is_a, i+1, sz, a_bits, b_bits, out1);  in mk_const_case_multiplier()
1151         if (is_a) a_bits[i] = m().mk_false(); else b_bits[i] = m().mk_false();  in mk_const_case_multiplier()
1152         mk_const_case_multiplier(is_a, i+1, sz, a_bits, b_bits, out2);  in mk_const_case_multiplier()
1153         if (is_a) a_bits[i] = x; else b_bits[i] = x;  in mk_const_case_multiplier()
1165         VERIFY(is_numeral(sz, b_bits.data(), n_b));  in mk_const_case_multiplier()