19 for(std::size_t i=0; i<width; i++)
29 tmp.erase(tmp.begin(), tmp.begin()+1);
36 for(std::size_t i=0; i<a.size(); i++)
48 result.resize(last+1);
50 result.erase(result.begin(), result.begin()+first);
62 result.erase(result.begin(), result.begin()+(result.size()-n));
82 result.resize(a.size()+b.size());
84 for(std::size_t i=0; i<a.size(); i++)
87 for(std::size_t i=0; i<b.size(); i++)
88 result[i+a.size()]=b[i];
100 result.resize(a.size());
101 for(std::size_t i=0; i<result.size(); i++)
109 std::size_t new_size,
112 std::size_t old_size=bv.size();
116 result.resize(new_size);
122 for(std::size_t i=old_size; i<new_size; i++)
123 result[i]=extend_with;
136 #define OPTIMAL_FULL_ADDER
144 #ifdef OPTIMAL_FULL_ADDER
149 int constantProp = -1;
155 constantProp = (a.
is_true()) ? 1 : 0;
161 constantProp = (b.
is_true()) ? 1 : 0;
167 constantProp = (carry_in.
is_true()) ? 1 : 0;
173 if(constantProp == 1)
179 else if(constantProp == 0)
218 #endif // OPTIMAL_FULL_ADDER
227 #define COMPACT_CARRY
235 const auto const_count =
282 #endif // COMPACT_CARRY
305 for(std::size_t i=0; i<sum.size(); i++)
320 for(std::size_t i=0; i<op0.size(); i++)
354 const bvt op1_sign_applied=
373 literalt old_sign=op0[op0.size()-1];
398 literalt op0_is_negative=op0[op0.size()-1];
427 literalt old_sign=sum[sum.size()-1];
429 prop.
lequal(sum[sum.size()-1], tmp_op[tmp_op.size()-1]);
442 "representation has either value signed or unsigned");
460 std::size_t d=1, width=op.size();
463 for(std::size_t stage=0; stage<dist.size(); stage++)
469 for(std::size_t i=0; i<width; i++)
470 result[i]=
prop.
lselect(dist[stage], tmp[i], result[i]);
482 result.resize(src.size());
488 for(std::size_t i=0; i<src.size(); i++)
502 l=(dist<src.size()-i?src[i+dist]:src[src.size()-1]);
513 l=src[(src.size()+i-(dist%src.size()))%src.size()];
518 l=src[(i+(dist%src.size()))%src.size()];
563 for(
auto &literal : bv)
582 for(
auto &literal : result)
593 else if(pps.size()==2)
594 return add(pps[0], pps[1]);
597 std::vector<bvt> new_pps;
598 std::size_t no_full_adders=pps.size()/3;
601 for(std::size_t i=0; i<no_full_adders; i++)
603 const bvt &a=pps[i*3+0],
607 INVARIANT(a.size() == b.size(),
"groups should be of equal size");
608 INVARIANT(a.size() == c.size(),
"groups should be of equal size");
610 bvt s(a.size()), t(a.size());
612 for(std::size_t bit=0; bit<a.size(); bit++)
617 carry(a[bit-1], b[bit-1], c[bit-1]);
620 new_pps.push_back(s);
621 new_pps.push_back(t);
625 for(std::size_t i=no_full_adders*3; i<pps.size(); i++)
626 new_pps.push_back(pps[i]);
636 bvt op0=_op0, op1=_op1;
642 product.resize(op0.size());
644 for(std::size_t i=0; i<product.size(); i++)
647 for(std::size_t sum=0; sum<op0.size(); sum++)
652 tmpop.reserve(op0.size());
654 for(std::size_t idx=0; idx<sum; idx++)
657 for(std::size_t idx=sum; idx<op0.size(); idx++)
658 tmpop.push_back(
prop.
land(op1[idx-sum], op0[sum]));
660 product=
add(product, tmpop);
670 bvt op0=_op0, op1=_op1;
675 std::vector<bvt> pps;
676 pps.reserve(op0.size());
678 for(std::size_t bit=0; bit<op0.size(); bit++)
683 pp.reserve(op0.size());
686 for(std::size_t idx=0; idx<bit; idx++)
689 for(std::size_t idx=bit; idx<op0.size(); idx++)
690 pp.push_back(
prop.
land(op1[idx-bit], op0[bit]));
696 return zeros(op0.size());
707 bvt _op0=op0, _op1=op1;
715 product.resize(_op0.size());
717 for(std::size_t i=0; i<product.size(); i++)
720 for(std::size_t sum=0; sum<op0.size(); sum++)
725 tmpop.reserve(product.size());
727 for(std::size_t idx=0; idx<sum; idx++)
730 for(std::size_t idx=sum; idx<product.size(); idx++)
731 tmpop.push_back(
prop.
land(op1[idx-sum], op0[sum]));
735 for(std::size_t idx=op1.size()-sum; idx<op1.size(); idx++)
744 if(op0.empty() || op1.empty())
765 result.resize(bv.size());
767 for(std::size_t i=0; i<bv.size(); i++)
790 if(op0.empty() || op1.empty())
844 if(op0.empty() || op1.empty())
847 bvt _op0(op0), _op1(op1);
849 literalt sign_0=_op0[_op0.size()-1];
850 literalt sign_1=_op1[_op1.size()-1];
854 for(std::size_t i=0; i<_op0.size(); i++)
857 for(std::size_t i=0; i<_op1.size(); i++)
866 for(std::size_t i=0; i<res.size(); i++)
867 res[i]=
prop.
lselect(result_sign, neg_res[i], res[i]);
869 for(std::size_t i=0; i<res.size(); i++)
897 std::size_t width=op0.size();
902 std::size_t one_count=0, non_const_count=0, one_pos=0;
904 for(std::size_t i=0; i<op1.size(); i++)
916 if(non_const_count==0 && one_count==1 && one_pos!=0)
919 res=
shift(op0, LRIGHT, one_pos);
923 for(std::size_t i=one_pos; i<rem.size(); i++)
942 for(std::size_t i=0; i<width; i++)
977 #ifdef COMPACT_EQUAL_CONST
983 void bv_utilst::equal_const_register(
const bvt &var)
986 equal_const_registered.insert(var);
998 std::size_t size = var.size();
1008 constant.pop_back();
1013 var_constant_pairt index(var, constant);
1015 equal_const_cachet::iterator entry = equal_const_cache.find(index);
1017 if(entry != equal_const_cache.end())
1019 return entry->second;
1025 constant.pop_back();
1027 literalt rec = equal_const_rec(var, constant);
1030 equal_const_cache.insert(
1031 std::pair<var_constant_pairt, literalt>(index, compare));
1046 literalt bv_utilst::equal_const(
const bvt &var,
const bvt &constant)
1048 std::size_t size = constant.size();
1066 literalt top_bit = constant[size - 1];
1068 std::size_t split = size - 1;
1069 var_upper.push_back(var[size - 1]);
1070 constant_upper.push_back(constant[size - 1]);
1072 for(split = size - 2; split != 0; --split)
1074 if(constant[split] != top_bit)
1080 var_upper.push_back(var[split]);
1081 constant_upper.push_back(constant[split]);
1085 for(std::size_t i = 0; i <= split; ++i)
1087 var_lower.push_back(var[i]);
1088 constant_lower.push_back(constant[i]);
1093 var_upper.size() + var_lower.size() == size,
1094 "lower size plus upper size should equal the total size");
1096 constant_upper.size() + constant_lower.size() == size,
1097 "lower size plus upper size should equal the total size");
1099 literalt top_comparison = equal_const_rec(var_upper, constant_upper);
1100 literalt bottom_comparison = equal_const_rec(var_lower, constant_lower);
1102 return prop.
land(top_comparison, bottom_comparison);
1115 #ifdef COMPACT_EQUAL_CONST
1119 equal_const_registered.find(op1) != equal_const_registered.end())
1120 return equal_const(op1, op0);
1122 equal_const_registered.find(op0) != equal_const_registered.end())
1123 return equal_const(op0, op1);
1127 equal_bv.resize(op0.size());
1129 for(std::size_t i=0; i<op0.size(); i++)
1159 top1=bv1[bv1.size()-1];
1161 #ifdef COMPACT_LT_OR_LE
1169 compareBelow.resize(bv0.size());
1170 for(
auto &literal : compareBelow)
1177 bv0.size() >= 2,
"signed bitvectors should have at least two bits");
1178 start = compareBelow.size() - 2;
1180 literalt firstComp=compareBelow[start];
1183 #ifdef INCLUDE_REDUNDANT_CLAUSES
1191 prop.
lcnf(!top0, !top1, firstComp);
1193 #ifdef INCLUDE_REDUNDANT_CLAUSES
1194 prop.
lcnf(top0, !top1, !firstComp);
1195 prop.
lcnf(!top0, top1, !firstComp);
1201 start = compareBelow.size() - 1;
1211 prop.
lcnf(!compareBelow[i], bv0[i], !bv1[i], result);
1212 prop.
lcnf(!compareBelow[i], !bv0[i], bv1[i], !result);
1219 for(i = start; i > 0; i--)
1221 prop.
lcnf(!compareBelow[i], !bv0[i], !bv1[i], compareBelow[i-1]);
1222 prop.
lcnf(!compareBelow[i], bv0[i], bv1[i], compareBelow[i-1]);
1226 #ifdef INCLUDE_REDUNDANT_CLAUSES
1231 for(i = start; i > 0; i--)
1233 prop.
lcnf(compareBelow[i], !compareBelow[i-1]);
1234 prop.
lcnf(!compareBelow[i], bv0[i], !bv1[i], !compareBelow[i-1]);
1235 prop.
lcnf(!compareBelow[i], !bv0[i], bv1[i], !compareBelow[i-1]);
1240 prop.
lcnf(!compareBelow[0], !bv0[0], !bv1[0], (or_equal)?result:!result);
1241 prop.
lcnf(!compareBelow[0], bv0[0], bv1[0], (or_equal)?result:!result);
1259 "representation has either value signed or unsigned");
1274 #ifdef COMPACT_LT_OR_LE
1275 return lt_or_le(
false, op0, op1, UNSIGNED);
1296 return equal(bv0, bv1);
1297 else if(
id==ID_notequal)
1298 return !
equal(bv0, bv1);
1300 return lt_or_le(
true, bv0, bv1, rep);
1302 return lt_or_le(
false, bv0, bv1, rep);
1304 return lt_or_le(
true, bv1, bv0, rep);
1306 return lt_or_le(
false, bv1, bv0, rep);
1313 for(
const auto &literal : bv)
1315 if(!literal.is_constant())
1331 for(std::size_t i=0; i<a.size(); i++)
1348 odd_bits.reserve(src.size()/2);
1351 for(std::size_t i=0; i<src.size(); i++)
1354 odd_bits.push_back(src[i]);
1363 even_bits.reserve(src.size()/2);
1366 for(std::size_t i=0; i<src.size(); i++)
1369 even_bits.push_back(src[i]);