20 assert(n_str.size()==width);
21 for(std::size_t i=0; i<width; i++)
31 tmp.erase(tmp.begin(), tmp.begin()+1);
37 assert(a.size()==b.size());
38 for(std::size_t i=0; i<a.size(); i++)
45 assert(first<a.size());
46 assert(last<a.size());
50 result.resize(last+1);
52 result.erase(result.begin(), result.begin()+first);
54 assert(result.size()==last-first+1);
64 result.erase(result.begin(), result.begin()+(result.size()-n));
66 assert(result.size()==n);
84 result.resize(a.size()+b.size());
86 for(std::size_t i=0; i<a.size(); i++)
89 for(std::size_t i=0; i<b.size(); i++)
90 result[i+a.size()]=b[i];
98 assert(a.size()==b.size());
102 result.resize(a.size());
103 for(std::size_t i=0; i<result.size(); i++)
111 std::size_t new_size,
114 std::size_t old_size=bv.size();
116 result.resize(new_size);
124 for(std::size_t i=old_size; i<new_size; i++)
125 result[i]=extend_with;
138 #define OPTIMAL_FULL_ADDER 146 #ifdef OPTIMAL_FULL_ADDER 151 int constantProp = -1;
157 constantProp = (a.
is_true()) ? 1 : 0;
163 constantProp = (b.
is_true()) ? 1 : 0;
169 constantProp = (carry_in.
is_true()) ? 1 : 0;
175 if(constantProp == 1)
181 else if(constantProp == 0)
194 prop.
lcnf(!a, !carry_in, carry_out);
195 prop.
lcnf(!b, !carry_in, carry_out);
205 prop.
lcnf(carry_in, !sum, !carry_out);
210 prop.
lcnf(!carry_in, sum, carry_out);
220 #endif // OPTIMAL_FULL_ADDER 223 carry_out=
carry(a, b, carry_in);
229 #define COMPACT_CARRY 237 unsigned const_count=
284 #endif // COMPACT_CARRY 303 assert(sum.size()==op.size());
307 for(std::size_t i=0; i<sum.size(); i++)
309 sum[i] =
full_adder(sum[i], op[i], carry_out, carry_out);
318 assert(op0.size()==op1.size());
322 for(std::size_t i=0; i<op0.size(); i++)
323 carry_out=
carry(op0[i], op1[i], carry_out);
341 assert(op0.size()==op1.size());
349 adder(result, tmp_op1, carry_in, carry_out);
356 const bvt op1_sign_applied=
362 adder(result, op1_sign_applied, subtract, carry_out);
375 literalt old_sign=op0[op0.size()-1];
400 literalt op0_is_negative=op0[op0.size()-1];
429 literalt old_sign=sum[sum.size()-1];
431 prop.
lequal(sum[sum.size()-1], tmp_op[tmp_op.size()-1]);
454 adder(sum, op, carry_out, carry_out);
461 std::size_t d=1, width=op.size();
464 for(std::size_t stage=0; stage<dist.size(); stage++)
470 for(std::size_t i=0; i<width; i++)
471 result[i]=
prop.
lselect(dist[stage], tmp[i], result[i]);
483 result.resize(src.size());
485 for(std::size_t i=0; i<src.size(); i++)
496 l=(i+dist<src.size()?src[i+dist]:src[src.size()-1]);
533 zeros.erase(--zeros.end());
571 assert(!pps.empty());
575 else if(pps.size()==2)
576 return add(pps[0], pps[1]);
579 std::vector<bvt> new_pps;
580 std::size_t no_full_adders=pps.size()/3;
583 for(std::size_t i=0; i<no_full_adders; i++)
585 const bvt &a=pps[i*3+0],
589 assert(a.size()==b.size() && a.size()==c.size());
591 bvt s(a.size()), t(a.size());
593 for(std::size_t bit=0; bit<a.size(); bit++)
598 carry(a[bit-1], b[bit-1], c[bit-1]);
601 new_pps.push_back(s);
602 new_pps.push_back(t);
606 for(std::size_t i=no_full_adders*3; i<pps.size(); i++)
607 new_pps.push_back(pps[i]);
609 assert(new_pps.size()<pps.size());
617 bvt op0=_op0, op1=_op1;
623 product.resize(op0.size());
625 for(std::size_t i=0; i<product.size(); i++)
628 for(std::size_t sum=0; sum<op0.size(); sum++)
633 tmpop.reserve(op0.size());
635 for(std::size_t idx=0; idx<sum; idx++)
638 for(std::size_t idx=sum; idx<op0.size(); idx++)
639 tmpop.push_back(
prop.
land(op1[idx-sum], op0[sum]));
641 product=
add(product, tmpop);
651 bvt op0=_op0, op1=_op1;
656 std::vector<bvt> pps;
657 pps.reserve(op0.size());
659 for(std::size_t bit=0; bit<op0.size(); bit++)
664 pp.reserve(op0.size());
667 for(std::size_t idx=0; idx<bit; idx++)
670 for(std::size_t idx=bit; idx<op0.size(); idx++)
671 pp.push_back(
prop.
land(op1[idx-bit], op0[bit]));
677 return zeros(op0.size());
688 bvt _op0=op0, _op1=op1;
693 assert(_op0.size()==_op1.size());
696 product.resize(_op0.size());
698 for(std::size_t i=0; i<product.size(); i++)
701 for(std::size_t sum=0; sum<op0.size(); sum++)
706 tmpop.reserve(product.size());
708 for(std::size_t idx=0; idx<sum; idx++)
711 for(std::size_t idx=sum; idx<product.size(); idx++)
712 tmpop.push_back(
prop.
land(op1[idx-sum], op0[sum]));
716 for(std::size_t idx=op1.size()-sum; idx<op1.size(); idx++)
725 if(op0.empty() || op1.empty())
746 result.resize(bv.size());
748 for(std::size_t i=0; i<bv.size(); i++)
773 if(op0.empty() || op1.empty())
800 default: assert(
false);
815 default: assert(
false);
825 if(op0.empty() || op1.empty())
828 bvt _op0(op0), _op1(op1);
830 literalt sign_0=_op0[_op0.size()-1];
831 literalt sign_1=_op1[_op1.size()-1];
835 for(std::size_t i=0; i<_op0.size(); i++)
838 for(std::size_t i=0; i<_op1.size(); i++)
847 for(std::size_t i=0; i<res.size(); i++)
848 res[i]=
prop.
lselect(result_sign, neg_res[i], res[i]);
850 for(std::size_t i=0; i<res.size(); i++)
869 default: assert(
false);
879 std::size_t width=op0.size();
884 std::size_t one_count=0, non_const_count=0, one_pos=0;
886 for(std::size_t i=0; i<op1.size(); i++)
898 if(non_const_count==0 && one_count==1 && one_pos!=0)
901 res=
shift(op0, LRIGHT, one_pos);
905 for(std::size_t i=one_pos; i<rem.size(); i++)
924 for(std::size_t i=0; i<width; i++)
959 #ifdef COMPACT_EQUAL_CONST 965 void bv_utilst::equal_const_register(
const bvt &var)
968 equal_const_registered.insert(var);
981 std::size_t size = var.size();
984 assert(size == constant.size());
996 var_constant_pairt index(var, constant);
998 equal_const_cachet::iterator entry = equal_const_cache.find(index);
1000 if(entry != equal_const_cache.end())
1002 return entry->second;
1008 constant.pop_back();
1010 literalt rec = equal_const_rec(var, constant);
1013 equal_const_cache.insert(
1014 std::pair<var_constant_pairt, literalt>(index, compare));
1029 literalt bv_utilst::equal_const(
const bvt &var,
const bvt &constant)
1031 std::size_t size = constant.size();
1033 assert(var.size() == size);
1049 literalt top_bit = constant[size - 1];
1051 std::size_t split = size - 1;
1052 var_upper.push_back(var[size - 1]);
1053 constant_upper.push_back(constant[size - 1]);
1055 for(split = size - 2; split != 0; --split)
1057 if(constant[split] != top_bit)
1063 var_upper.push_back(var[split]);
1064 constant_upper.push_back(constant[split]);
1068 for(std::size_t i = 0; i <= split; ++i)
1070 var_lower.push_back(var[i]);
1071 constant_lower.push_back(constant[i]);
1075 assert(var_upper.size() + var_lower.size() == size);
1076 assert(constant_upper.size() + constant_lower.size() == size);
1078 literalt top_comparison = equal_const_rec(var_upper, constant_upper);
1079 literalt bottom_comparison = equal_const_rec(var_lower, constant_lower);
1081 return prop.
land(top_comparison, bottom_comparison);
1091 assert(op0.size()==op1.size());
1093 #ifdef COMPACT_EQUAL_CONST 1097 equal_const_registered.find(op1) != equal_const_registered.end())
1098 return equal_const(op1, op0);
1100 equal_const_registered.find(op0) != equal_const_registered.end())
1101 return equal_const(op0, op1);
1105 equal_bv.resize(op0.size());
1107 for(std::size_t i=0; i<op0.size(); i++)
1134 assert(bv0.size() == bv1.size());
1137 top1=bv1[bv1.size()-1];
1139 #ifdef COMPACT_LT_OR_LE 1147 compareBelow.resize(bv0.size());
1153 assert(bv0.size() >= 2);
1154 start = compareBelow.size() - 2;
1156 literalt firstComp=compareBelow[start];
1159 #ifdef INCLUDE_REDUNDANT_CLAUSES 1167 prop.
lcnf(!top0, !top1, firstComp);
1169 #ifdef INCLUDE_REDUNDANT_CLAUSES 1170 prop.
lcnf(top0, !top1, !firstComp);
1171 prop.
lcnf(!top0, top1, !firstComp);
1177 start = compareBelow.size() - 1;
1187 prop.
lcnf(!compareBelow[i], bv0[i], !bv1[i], result);
1188 prop.
lcnf(!compareBelow[i], !bv0[i], bv1[i], !result);
1195 for(i = start; i > 0; i--)
1197 prop.
lcnf(!compareBelow[i], !bv0[i], !bv1[i], compareBelow[i-1]);
1198 prop.
lcnf(!compareBelow[i], bv0[i], bv1[i], compareBelow[i-1]);
1202 #ifdef INCLUDE_REDUNDANT_CLAUSES 1207 for(i = start; i > 0; i--)
1209 prop.
lcnf(compareBelow[i], !compareBelow[i-1]);
1210 prop.
lcnf(!compareBelow[i], bv0[i], !bv1[i], !compareBelow[i-1]);
1211 prop.
lcnf(!compareBelow[i], !bv0[i], bv1[i], !compareBelow[i-1]);
1216 prop.
lcnf(!compareBelow[0], !bv0[0], !bv1[0], (or_equal)?result:!result);
1217 prop.
lcnf(!compareBelow[0], bv0[0], bv1[0], (or_equal)?result:!result);
1247 #ifdef COMPACT_LT_OR_LE 1248 return lt_or_le(
false, op0, op1, UNSIGNED);
1269 return equal(bv0, bv1);
1270 else if(
id==ID_notequal)
1271 return !
equal(bv0, bv1);
1273 return lt_or_le(
true, bv0, bv1, rep);
1275 return lt_or_le(
false, bv0, bv1, rep);
1277 return lt_or_le(
true, bv1, bv0, rep);
1279 return lt_or_le(
false, bv1, bv0, rep);
1287 if(!it->is_constant())
1298 assert(a.size()==b.size());
1302 for(std::size_t i=0; i<a.size(); i++)
1319 odd_bits.reserve(src.size()/2);
1322 for(std::size_t i=0; i<src.size(); i++)
1325 odd_bits.push_back(src[i]);
1334 even_bits.reserve(src.size()/2);
1337 for(std::size_t i=0; i<src.size(); i++)
1340 even_bits.push_back(src[i]);
bvt wallace_tree(const std::vector< bvt > &pps)
bvt inverted(const bvt &op)
bvt extension(const bvt &bv, std::size_t new_size, representationt rep)
bvt multiplier_no_overflow(const bvt &op0, const bvt &op1, representationt rep)
static bvt extract(const bvt &a, std::size_t first, std::size_t last)
void lcnf(literalt l0, literalt l1)
literalt is_int_min(const bvt &op)
bvt cond_negate(const bvt &bv, const literalt cond)
bvt add_sub_no_overflow(const bvt &op0, const bvt &op1, bool subtract, representationt rep)
bvt divider(const bvt &op0, const bvt &op1, representationt rep)
literalt equal(const bvt &op0, const bvt &op1)
Bit-blasting ID_equal and use in other encodings.
virtual literalt lor(literalt a, literalt b)=0
void adder(bvt &sum, const bvt &op, literalt carry_in, literalt &carry_out)
bool is_constant(const bvt &bv)
literalt is_zero(const bvt &op)
bvt unsigned_multiplier_no_overflow(const bvt &op0, const bvt &op1)
#define forall_literals(it, bv)
virtual literalt limplies(literalt a, literalt b)=0
void l_set_to_true(literalt a)
bvt signed_multiplier_no_overflow(const bvt &op0, const bvt &op1)
virtual void set_equal(literalt a, literalt b)
asserts a==b in the propositional formula
virtual literalt land(literalt a, literalt b)=0
literalt lt_or_le(bool or_equal, const bvt &bv0, const bvt &bv1, representationt rep)
To provide a bitwise model of < or <=.
virtual literalt new_variable()=0
#define Forall_literals(it, bv)
literalt overflow_negate(const bvt &op)
void adder_no_overflow(bvt &sum, const bvt &op, bool subtract, representationt rep)
bvt concatenate(const bvt &a, const bvt &b) const
bvt signed_multiplier(const bvt &op0, const bvt &op1)
virtual void l_set_to(literalt a, bool value)
literalt rel(const bvt &bv0, irep_idt id, const bvt &bv1, representationt rep)
bvt negate(const bvt &op)
virtual literalt lxor(literalt a, literalt b)=0
literalt is_not_zero(const bvt &op)
static bvt extract_msb(const bvt &a, std::size_t n)
literalt full_adder(const literalt a, const literalt b, const literalt carry_in, literalt &carry_out)
bvt multiplier(const bvt &op0, const bvt &op1, representationt rep)
void signed_divider(const bvt &op0, const bvt &op1, bvt &res, bvt &rem)
void l_set_to_false(literalt a)
virtual bool cnf_handled_well() const
bvt absolute_value(const bvt &op)
bvt unsigned_multiplier(const bvt &op0, const bvt &op1)
literalt signed_less_than(const bvt &bv0, const bvt &bv1)
bvt select(literalt s, const bvt &a, const bvt &b)
If s is true, selects a otherwise selects b.
void set_equal(const bvt &a, const bvt &b)
literalt verilog_bv_has_x_or_z(const bvt &)
bvt verilog_bv_normal_bits(const bvt &)
void unsigned_divider(const bvt &op0, const bvt &op1, bvt &res, bvt &rem)
bvt incrementer(const bvt &op, literalt carry_in)
virtual literalt lequal(literalt a, literalt b)=0
bvt shift(const bvt &op, const shiftt shift, std::size_t distance)
literalt unsigned_less_than(const bvt &bv0, const bvt &bv1)
literalt const_literal(bool value)
bvt add(const bvt &op0, const bvt &op1)
literalt is_one(const bvt &op)
bvt cond_negate_no_overflow(const bvt &bv, const literalt cond)
static bvt extract_lsb(const bvt &a, std::size_t n)
virtual bool has_set_to() const
bvt negate_no_overflow(const bvt &op)
const std::string integer2binary(const mp_integer &n, std::size_t width)
literalt carry_out(const bvt &op0, const bvt &op1, literalt carry_in)
void cond_implies_equal(literalt cond, const bvt &a, const bvt &b)
literalt carry(literalt a, literalt b, literalt c)
literalt overflow_sub(const bvt &op0, const bvt &op1, representationt rep)
virtual literalt lselect(literalt a, literalt b, literalt c)=0
literalt overflow_add(const bvt &op0, const bvt &op1, representationt rep)
bvt add_sub(const bvt &op0, const bvt &op1, bool subtract)
std::vector< literalt > bvt
bvt build_constant(const mp_integer &i, std::size_t width)
bvt zeros(std::size_t new_size) const