17 for(std::size_t
i=0;
i<width;
i++)
34 for(std::size_t
i=0;
i<
a.size();
i++)
46 result.resize(
last+1);
48 result.erase(result.begin(), result.begin()+first);
60 result.erase(result.begin(), result.begin()+(result.size()-
n));
80 result.resize(
a.size()+
b.size());
82 for(std::size_t
i=0;
i<
a.size();
i++)
85 for(std::size_t
i=0;
i<
b.size();
i++)
86 result[
i+
a.size()]=
b[
i];
98 result.resize(
a.size());
99 for(std::size_t
i=0;
i<result.size();
i++)
134#define OPTIMAL_FULL_ADDER
142 #ifdef OPTIMAL_FULL_ADDER
155 else if(
b.is_constant())
234 a.is_constant() +
b.is_constant() +
c.is_constant();
303 for(std::size_t
i=0;
i<
sum.size();
i++)
318 for(std::size_t
i=0;
i<op0.size();
i++)
440 "representation has either value signed or unsigned");
458 std::size_t d=1, width=op.size();
467 for(std::size_t
i=0;
i<width;
i++)
480 result.resize(src.size());
486 for(std::size_t
i=0;
i<src.size();
i++)
500 l=(
dist<src.size()-
i?src[
i+
dist]:src[src.size()-1]);
511 l=src[(src.size()+
i-(
dist%src.size()))%src.size()];
516 l=src[(
i+(
dist%src.size()))%src.size()];
591 else if(
pps.size()==2)
605 INVARIANT(
a.size() ==
b.size(),
"groups should be of equal size");
606 INVARIANT(
a.size() ==
c.size(),
"groups should be of equal size");
608 bvt s(
a.size()), t(
a.size());
645 for(std::size_t
sum=0;
sum<op0.size();
sum++)
650 tmpop.reserve(op0.size());
652 for(std::size_t idx=0; idx<
sum; idx++)
655 for(std::size_t idx=
sum; idx<op0.size(); idx++)
673 std::vector<bvt>
pps;
674 pps.reserve(op0.size());
676 for(std::size_t
bit=0;
bit<op0.size();
bit++)
681 pp.reserve(op0.size());
684 for(std::size_t idx=0; idx<
bit; idx++)
687 for(std::size_t idx=
bit; idx<op0.size(); idx++)
694 return zeros(op0.size());
718 for(std::size_t
sum=0;
sum<op0.size();
sum++)
725 for(std::size_t idx=0; idx<
sum; idx++)
728 for(std::size_t idx=
sum; idx<
product.size(); idx++)
733 for(std::size_t idx=op1.size()-
sum; idx<op1.size(); idx++)
742 if(op0.empty() || op1.empty())
763 result.resize(bv.size());
765 for(std::size_t
i=0;
i<bv.size();
i++)
788 if(op0.empty() || op1.empty())
842 if(op0.empty() || op1.empty())
852 for(std::size_t
i=0;
i<
_op0.size();
i++)
855 for(std::size_t
i=0;
i<
_op1.size();
i++)
864 for(std::size_t
i=0;
i<
res.size();
i++)
867 for(std::size_t
i=0;
i<
res.size();
i++)
895 std::size_t width=op0.size();
902 for(std::size_t
i=0;
i<op1.size();
i++)
969#ifdef COMPACT_EQUAL_CONST
975void bv_utilst::equal_const_register(
const bvt &var)
990 std::size_t size = var.size();
1000 constant.pop_back();
1011 return entry->second;
1017 constant.pop_back();
1023 std::pair<var_constant_pairt, literalt>(index, compare));
1038literalt bv_utilst::equal_const(
const bvt &var,
const bvt &constant)
1040 std::size_t size = constant.size();
1060 std::size_t
split = size - 1;
1077 for(std::size_t
i = 0;
i <=
split; ++
i)
1086 "lower size plus upper size should equal the total size");
1089 "lower size plus upper size should equal the total size");
1107 #ifdef COMPACT_EQUAL_CONST
1121 for(std::size_t
i=0;
i<op0.size();
i++)
1153#ifdef COMPACT_LT_OR_LE
1167 bv0.size() >= 2,
"signed bitvectors should have at least two bits");
1173#ifdef INCLUDE_REDUNDANT_CLAUSES
1183#ifdef INCLUDE_REDUNDANT_CLAUSES
1216#ifdef INCLUDE_REDUNDANT_CLAUSES
1249 "representation has either value signed or unsigned");
1264#ifdef COMPACT_LT_OR_LE
1321 for(std::size_t
i=0;
i<
a.size();
i++)
1341 for(std::size_t
i=0;
i<src.size();
i++)
1356 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)
void adder_no_overflow(bvt &sum, const bvt &op, bool subtract, representationt rep)
static bool is_constant(const bvt &bv)
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)
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)
void adder(bvt &sum, const bvt &op, literalt carry_in, literalt &carry_out)
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)
To provide a bitwise model of < or <=.
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)
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)
literalt rel(const bvt &bv0, irep_idt id, const bvt &bv1, representationt rep)
bvt zeros(std::size_t new_size) const
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
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)