19 for(std::size_t i=0; i<width; i++)
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++)
136#define OPTIMAL_FULL_ADDER
144 #ifdef OPTIMAL_FULL_ADDER
157 else if(
b.is_constant())
236 a.is_constant() +
b.is_constant() +
c.is_constant();
295std::pair<bvt, literalt>
301 result.first.reserve(op0.size());
304 for(std::size_t i = 0; i < op0.size(); i++)
321 for(std::size_t i=0; i<op0.size(); i++)
503 "representation has either value signed or unsigned");
506 return std::move(result.first);
517 std::size_t d=1, width=op.size();
526 for(std::size_t i=0; i<width; i++)
539 result.resize(src.size());
545 for(std::size_t i=0; i<src.size(); i++)
559 l=(
dist<src.size()-i?src[i+
dist]:src[src.size()-1]);
570 l=src[(src.size()+i-(
dist%src.size()))%src.size()];
575 l=src[(i+(
dist%src.size()))%src.size()];
650 else if(
pps.size()==2)
664 INVARIANT(
a.size() ==
b.size(),
"groups should be of equal size");
665 INVARIANT(
a.size() ==
c.size(),
"groups should be of equal size");
674 if(
bit + 1 <
a.size())
678 new_pps.push_back(std::move(s));
679 new_pps.push_back(std::move(t));
695 using columnt = std::list<literalt>;
696 std::vector<columnt>
columns(
pps.front().size());
697 for(
const auto &
pp :
pps)
700 for(std::size_t i = 0; i <
pp.size(); ++i)
708 for(std::size_t d = 2; d <
pps.front().size(); d = (d * 3) / 2)
717 else if(
col_it->size() == d + 1)
724 *std::next(
col_it->begin()),
740 *std::next(
col_it->begin()),
741 *std::next(std::next(
col_it->begin())),
753 a.reserve(
pps.front().size());
754 b.reserve(
pps.front().size());
766 a.push_back(
col.front());
770 a.push_back(
col.front());
771 b.push_back(
col.back());
926 std::vector<bvt>
pps;
927 pps.reserve(op0.size());
929 for(std::size_t
bit=0;
bit<op0.size();
bit++)
936 pp.reserve(op0.size());
938 for(std::size_t idx =
bit; idx < op0.size(); idx++)
945 return zeros(op0.size());
950#elif defined(DADDA_TREE)
955 for(
auto it = std::next(
pps.begin()); it !=
pps.end(); ++it)
977 for(std::size_t i=0; i<
product.size(); i++)
980 for(std::size_t
sum=0;
sum<op0.size();
sum++)
987 for(std::size_t idx=0; idx<
sum; idx++)
990 for(std::size_t idx=
sum; idx<
product.size(); idx++)
995 for(std::size_t idx=op1.size()-
sum; idx<op1.size(); idx++)
1004 if(op0.empty() || op1.empty())
1025 result.resize(bv.size());
1027 for(std::size_t i=0; i<bv.size(); i++)
1050 if(op0.empty() || op1.empty())
1104 if(op0.empty() || op1.empty())
1114 for(std::size_t i=0; i<
_op0.size(); i++)
1117 for(std::size_t i=0; i<
_op1.size(); i++)
1126 for(std::size_t i=0; i<
res.size(); i++)
1129 for(std::size_t i=0; i<
res.size(); i++)
1157 std::size_t width=op0.size();
1164 for(std::size_t i=0; i<op1.size(); i++)
1183 for(std::size_t i=
one_pos; i<rem.size(); i++)
1229#ifdef COMPACT_EQUAL_CONST
1235void bv_utilst::equal_const_register(
const bvt &var)
1250 std::size_t size = var.size();
1260 constant.pop_back();
1271 return entry->second;
1277 constant.pop_back();
1283 std::pair<var_constant_pairt, literalt>(index, compare));
1298literalt bv_utilst::equal_const(
const bvt &var,
const bvt &constant)
1300 std::size_t size = constant.size();
1320 std::size_t
split = size - 1;
1337 for(std::size_t i = 0; i <=
split; ++i)
1346 "lower size plus upper size should equal the total size");
1349 "lower size plus upper size should equal the total size");
1367 #ifdef COMPACT_EQUAL_CONST
1381 for(std::size_t i=0; i<op0.size(); i++)
1392#define COMPACT_LT_OR_LE
1409#ifdef COMPACT_LT_OR_LE
1419 if(
top0.is_false() &&
top1.is_true())
1421 else if(
top0.is_true() &&
top1.is_false())
1425 bv0.size() >= 2,
"signed bitvectors should have at least two bits");
1432 else if(
top0.is_true())
1434 else if(
top1.is_false())
1436 else if(
top1.is_true())
1448#ifdef INCLUDE_REDUNDANT_CLAUSES
1486 for(i = start; i > 0; i--)
1493#ifdef INCLUDE_REDUNDANT_CLAUSES
1498 for(i = start; i > 0; i--)
1526 "representation has either value signed or unsigned");
1541#ifdef COMPACT_LT_OR_LE
1598 for(std::size_t i=0; i<
a.size(); i++)
1618 for(std::size_t i=0; i<src.size(); i++)
1633 for(std::size_t i=0; i<src.size(); i++)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
static bvt inverted(const bvt &op)
literalt signed_less_than(const bvt &bv0, const bvt &bv1)
static bool is_constant(const bvt &bv)
NODISCARD std::pair< bvt, literalt > adder(const bvt &op0, const bvt &op1, literalt carry_in)
Return the sum and carry-out when adding op0 and op1 under initial carry carry_in.
bvt wallace_tree(const std::vector< bvt > &pps)
literalt is_not_zero(const bvt &op)
static bvt verilog_bv_normal_bits(const bvt &)
literalt is_int_min(const bvt &op)
static bvt extract_msb(const bvt &a, std::size_t n)
void set_equal(const bvt &a, const bvt &b)
static literalt sign_bit(const bvt &op)
bvt multiplier_no_overflow(const bvt &op0, const bvt &op1, representationt rep)
bvt add_sub_no_overflow(const bvt &op0, const bvt &op1, bool subtract, representationt rep)
bvt add(const bvt &op0, const bvt &op1)
bvt absolute_value(const bvt &op)
bvt select(literalt s, const bvt &a, const bvt &b)
If s is true, selects a otherwise selects b.
static bvt build_constant(const mp_integer &i, std::size_t width)
void signed_divider(const bvt &op0, const bvt &op1, bvt &res, bvt &rem)
literalt is_zero(const bvt &op)
literalt equal(const bvt &op0, const bvt &op1)
Bit-blasting ID_equal and use in other encodings.
bvt signed_multiplier(const bvt &op0, const bvt &op1)
literalt overflow_add(const bvt &op0, const bvt &op1, representationt rep)
literalt is_one(const bvt &op)
bvt cond_negate_no_overflow(const bvt &bv, const literalt cond)
literalt overflow_sub(const bvt &op0, const bvt &op1, representationt rep)
void cond_implies_equal(literalt cond, const bvt &a, const bvt &b)
literalt unsigned_less_than(const bvt &bv0, const bvt &bv1)
bvt signed_multiplier_no_overflow(const bvt &op0, const bvt &op1)
bvt incrementer(const bvt &op, literalt carry_in)
bvt add_sub(const bvt &op0, const bvt &op1, bool subtract)
static bvt shift(const bvt &op, const shiftt shift, std::size_t distance)
literalt lt_or_le(bool or_equal, const bvt &bv0, const bvt &bv1, representationt rep)
literalt overflow_negate(const bvt &op)
static bvt concatenate(const bvt &a, const bvt &b)
literalt full_adder(const literalt a, const literalt b, const literalt carry_in, literalt &carry_out)
bvt negate_no_overflow(const bvt &op)
static bvt extract(const bvt &a, std::size_t first, std::size_t last)
bvt unsigned_multiplier(const bvt &op0, const bvt &op1)
bvt divider(const bvt &op0, const bvt &op1, representationt rep)
void unsigned_divider(const bvt &op0, const bvt &op1, bvt &res, bvt &rem)
bvt multiplier(const bvt &op0, const bvt &op1, representationt rep)
bvt cond_negate(const bvt &bv, const literalt cond)
bvt dadda_tree(const std::vector< bvt > &pps)
literalt carry_out(const bvt &op0, const bvt &op1, literalt carry_in)
bvt negate(const bvt &op)
static bvt extension(const bvt &bv, std::size_t new_size, representationt rep)
static bvt extract_lsb(const bvt &a, std::size_t n)
literalt verilog_bv_has_x_or_z(const bvt &)
literalt carry(literalt a, literalt b, literalt c)
bvt unsigned_multiplier_no_overflow(const bvt &op0, const bvt &op1)
static bvt zeros(std::size_t new_size)
literalt rel(const bvt &bv0, irep_idt id, const bvt &bv1, representationt rep)
NODISCARD bvt adder_no_overflow(const bvt &op0, const bvt &op1, bool subtract, representationt rep)
bvt saturating_add_sub(const bvt &op0, const bvt &op1, bool subtract, representationt rep)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
void l_set_to_true(literalt a)
virtual literalt land(literalt a, literalt b)=0
virtual literalt limplies(literalt a, literalt b)=0
virtual literalt lselect(literalt a, literalt b, literalt c)=0
virtual bool cnf_handled_well() const
virtual void l_set_to(literalt a, bool value)
virtual literalt lxor(literalt a, literalt b)=0
void lcnf(literalt l0, literalt l1)
virtual void set_equal(literalt a, literalt b)
asserts a==b in the propositional formula
virtual bvt new_variables(std::size_t width)
generates a bitvector of given width with new variables
virtual literalt new_variable()=0
virtual literalt lequal(literalt a, literalt b)=0
virtual literalt lor(literalt a, literalt b)=0
void l_set_to_false(literalt a)
virtual bool has_set_to() const
bool is_false(const literalt &l)
bool is_true(const literalt &l)
std::vector< literalt > bvt
literalt const_literal(bool value)
const std::string integer2binary(const mp_integer &n, std::size_t width)
#define CHECK_RETURN(CONDITION)
#define UNREACHABLE
This should be used to mark dead code.
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
#define POSTCONDITION(CONDITION)