cprover
|
#include <bv_utils.h>
Public Types | |
enum | representationt { representationt::SIGNED, representationt::UNSIGNED } |
enum | shiftt { shiftt::SHIFT_LEFT, shiftt::SHIFT_LRIGHT, shiftt::SHIFT_ARIGHT, shiftt::ROTATE_LEFT, shiftt::ROTATE_RIGHT } |
Public Member Functions | |
bv_utilst (propt &_prop) | |
bvt | build_constant (const mp_integer &i, std::size_t width) |
bvt | incrementer (const bvt &op, literalt carry_in) |
bvt | inc (const bvt &op) |
void | incrementer (bvt &op, literalt carry_in, literalt &carry_out) |
bvt | negate (const bvt &op) |
bvt | negate_no_overflow (const bvt &op) |
bvt | absolute_value (const bvt &op) |
literalt | overflow_negate (const bvt &op) |
bvt | inverted (const bvt &op) |
literalt | full_adder (const literalt a, const literalt b, const literalt carry_in, literalt &carry_out) |
literalt | carry (literalt a, literalt b, literalt c) |
bvt | add_sub (const bvt &op0, const bvt &op1, bool subtract) |
bvt | add_sub (const bvt &op0, const bvt &op1, literalt subtract) |
bvt | add_sub_no_overflow (const bvt &op0, const bvt &op1, bool subtract, representationt rep) |
bvt | add (const bvt &op0, const bvt &op1) |
bvt | sub (const bvt &op0, const bvt &op1) |
literalt | overflow_add (const bvt &op0, const bvt &op1, representationt rep) |
literalt | overflow_sub (const bvt &op0, const bvt &op1, representationt rep) |
literalt | carry_out (const bvt &op0, const bvt &op1, literalt carry_in) |
bvt | shift (const bvt &op, const shiftt shift, std::size_t distance) |
bvt | shift (const bvt &op, const shiftt shift, const bvt &distance) |
bvt | unsigned_multiplier (const bvt &op0, const bvt &op1) |
bvt | signed_multiplier (const bvt &op0, const bvt &op1) |
bvt | multiplier (const bvt &op0, const bvt &op1, representationt rep) |
bvt | multiplier_no_overflow (const bvt &op0, const bvt &op1, representationt rep) |
bvt | divider (const bvt &op0, const bvt &op1, representationt rep) |
bvt | remainder (const bvt &op0, const bvt &op1, representationt rep) |
void | divider (const bvt &op0, const bvt &op1, bvt &res, bvt &rem, representationt rep) |
void | signed_divider (const bvt &op0, const bvt &op1, bvt &res, bvt &rem) |
void | unsigned_divider (const bvt &op0, const bvt &op1, bvt &res, bvt &rem) |
literalt | equal (const bvt &op0, const bvt &op1) |
Bit-blasting ID_equal and use in other encodings. More... | |
literalt | is_zero (const bvt &op) |
literalt | is_not_zero (const bvt &op) |
literalt | is_int_min (const bvt &op) |
literalt | is_one (const bvt &op) |
literalt | is_all_ones (const bvt &op) |
literalt | lt_or_le (bool or_equal, const bvt &bv0, const bvt &bv1, representationt rep) |
To provide a bitwise model of < or <=. More... | |
literalt | rel (const bvt &bv0, irep_idt id, const bvt &bv1, representationt rep) |
literalt | unsigned_less_than (const bvt &bv0, const bvt &bv1) |
literalt | signed_less_than (const bvt &bv0, const bvt &bv1) |
bool | is_constant (const bvt &bv) |
bvt | extension (const bvt &bv, std::size_t new_size, representationt rep) |
bvt | sign_extension (const bvt &bv, std::size_t new_size) |
bvt | zero_extension (const bvt &bv, std::size_t new_size) |
bvt | zeros (std::size_t new_size) const |
void | set_equal (const bvt &a, const bvt &b) |
void | cond_implies_equal (literalt cond, const bvt &a, const bvt &b) |
bvt | cond_negate (const bvt &bv, const literalt cond) |
bvt | select (literalt s, const bvt &a, const bvt &b) |
If s is true, selects a otherwise selects b. More... | |
bvt | concatenate (const bvt &a, const bvt &b) const |
literalt | verilog_bv_has_x_or_z (const bvt &) |
bvt | verilog_bv_normal_bits (const bvt &) |
Static Public Member Functions | |
static literalt | sign_bit (const bvt &op) |
static bvt | extract (const bvt &a, std::size_t first, std::size_t last) |
static bvt | extract_msb (const bvt &a, std::size_t n) |
static bvt | extract_lsb (const bvt &a, std::size_t n) |
Protected Member Functions | |
void | adder (bvt &sum, const bvt &op, literalt carry_in, literalt &carry_out) |
void | adder_no_overflow (bvt &sum, const bvt &op, bool subtract, representationt rep) |
void | adder_no_overflow (bvt &sum, const bvt &op) |
bvt | unsigned_multiplier_no_overflow (const bvt &op0, const bvt &op1) |
bvt | signed_multiplier_no_overflow (const bvt &op0, const bvt &op1) |
bvt | cond_negate_no_overflow (const bvt &bv, const literalt cond) |
bvt | wallace_tree (const std::vector< bvt > &pps) |
Protected Attributes | |
propt & | prop |
Definition at line 26 of file bv_utils.h.
|
strong |
Enumerator | |
---|---|
SIGNED | |
UNSIGNED |
Definition at line 31 of file bv_utils.h.
|
strong |
Enumerator | |
---|---|
SHIFT_LEFT | |
SHIFT_LRIGHT | |
SHIFT_ARIGHT | |
ROTATE_LEFT | |
ROTATE_RIGHT |
Definition at line 71 of file bv_utils.h.
|
inlineexplicit |
Definition at line 29 of file bv_utils.h.
Definition at line 773 of file bv_utils.cpp.
References cond_negate().
Referenced by float_utilst::add_sub(), boolbvt::convert_abs(), and float_utilst::from_signed_integer().
Definition at line 64 of file bv_utils.h.
References add_sub().
Referenced by float_utilst::add_bias(), float_utilst::add_sub(), bv_pointerst::convert_pointer_type(), float_utilst::div(), float_utilst::mul(), float_approximationt::normalization_shift(), float_utilst::normalization_shift(), bv_pointerst::offset_arithmetic(), overflow_add(), boolbvt::type_conversion(), unsigned_multiplier(), and wallace_tree().
Definition at line 339 of file bv_utils.cpp.
References adder(), carry_out(), const_literal(), and inverted().
Referenced by add(), float_utilst::add_sub(), boolbvt::convert_add_sub(), and sub().
Definition at line 354 of file bv_utils.cpp.
References adder(), carry_out(), inverted(), and select().
bvt bv_utilst::add_sub_no_overflow | ( | const bvt & | op0, |
const bvt & | op1, | ||
bool | subtract, | ||
representationt | rep | ||
) |
Definition at line 328 of file bv_utils.cpp.
References adder_no_overflow().
Referenced by boolbvt::convert_add_sub().
|
protected |
Definition at line 297 of file bv_utils.cpp.
References carry_out(), and full_adder().
Referenced by add_sub(), and adder_no_overflow().
|
protected |
Definition at line 416 of file bv_utils.cpp.
References adder(), carry(), carry_out(), const_literal(), inverted(), propt::l_set_to(), propt::l_set_to_false(), propt::land(), propt::lequal(), propt::lxor(), prop, SIGNED, and UNSIGNED.
Referenced by add_sub_no_overflow(), unsigned_divider(), and unsigned_multiplier_no_overflow().
Definition at line 450 of file bv_utils.cpp.
References adder(), carry_out(), const_literal(), propt::l_set_to_false(), and prop.
bvt bv_utilst::build_constant | ( | const mp_integer & | i, |
std::size_t | width | ||
) |
Definition at line 15 of file bv_utils.cpp.
References const_literal(), and integer2binary().
Referenced by float_utilst::add_bias(), float_utilst::add_sub(), float_utilst::build_constant(), bv_pointerst::convert_bitvector(), boolbvt::convert_bitvector(), boolbvt::convert_constant(), boolbvt::convert_overflow(), bv_pointerst::convert_pointer_type(), boolbvt::convert_power(), boolbvt::convert_update_rec(), float_utilst::denormalization_shift(), float_utilst::div(), bv_pointerst::do_postponed(), float_utilst::from_signed_integer(), float_utilst::from_unsigned_integer(), float_approximationt::normalization_shift(), float_utilst::normalization_shift(), bv_pointerst::offset_arithmetic(), float_utilst::round_exponent(), float_utilst::set_rounding_mode(), float_utilst::sub_bias(), float_utilst::to_integer(), boolbvt::type_conversion(), and float_utilst::unpack().
Definition at line 231 of file bv_utils.cpp.
References propt::cnf_handled_well(), propt::has_set_to(), literalt::is_constant(), propt::land(), propt::lcnf(), propt::lor(), propt::new_variable(), and prop.
Referenced by adder_no_overflow(), carry_out(), full_adder(), lt_or_le(), and wallace_tree().
Definition at line 313 of file bv_utils.cpp.
References carry().
Referenced by add_sub(), adder(), adder_no_overflow(), full_adder(), incrementer(), lt_or_le(), negate(), overflow_add(), overflow_sub(), and unsigned_less_than().
Definition at line 80 of file bv_utils.cpp.
Referenced by float_utilst::add_sub(), float_utilst::conversion(), float_utilst::denormalization_shift(), and float_utilst::round_fraction().
Definition at line 1312 of file bv_utils.cpp.
References propt::cnf_handled_well(), equal(), propt::lcnf(), propt::limplies(), and prop.
Referenced by float_approximationt::normalization_shift(), and float_utilst::normalization_shift().
Definition at line 760 of file bv_utils.cpp.
References propt::lselect(), negate(), and prop.
Referenced by absolute_value(), cond_negate_no_overflow(), signed_multiplier(), and float_utilst::to_integer().
Definition at line 779 of file bv_utils.cpp.
References cond_negate(), propt::l_set_to(), propt::limplies(), overflow_negate(), and prop.
Referenced by signed_multiplier_no_overflow().
|
inline |
Definition at line 87 of file bv_utils.h.
Referenced by bv_refinementt::check_SAT(), bv_pointerst::convert_bitvector(), boolbvt::convert_div(), boolbvt::convert_mod(), and remainder().
void bv_utilst::divider | ( | const bvt & | op0, |
const bvt & | op1, | ||
bvt & | res, | ||
bvt & | rem, | ||
representationt | rep | ||
) |
Definition at line 873 of file bv_utils.cpp.
References propt::has_set_to(), prop, SIGNED, signed_divider(), UNSIGNED, and unsigned_divider().
Bit-blasting ID_equal and use in other encodings.
Bit:vectors | for the two things to compare. |
Definition at line 1108 of file bv_utils.cpp.
References is_constant(), propt::land(), propt::lequal(), and prop.
Referenced by equalityt::add_equality_constraints(), bv_refinementt::check_SAT(), cond_implies_equal(), boolbvt::convert_case(), boolbvt::convert_cond(), boolbvt::convert_constraint_select_one(), boolbvt::convert_equality(), bv_refinementt::convert_mult(), boolbvt::convert_power(), boolbvt::convert_update_rec(), boolbvt::convert_verilog_case_equality(), bv_pointerst::do_postponed(), lt_or_le(), rel(), float_utilst::relation(), float_utilst::set_rounding_mode(), and unsigned_divider().
bvt bv_utilst::extension | ( | const bvt & | bv, |
std::size_t | new_size, | ||
representationt | rep | ||
) |
Definition at line 109 of file bv_utils.cpp.
References const_literal(), and SIGNED.
Referenced by boolbvt::convert_overflow(), bv_pointerst::convert_pointer_type(), bv_pointerst::offset_arithmetic(), sign_extension(), and zero_extension().
Definition at line 42 of file bv_utils.cpp.
Referenced by float_utilst::fraction_rounding_decision(), float_utilst::get_exponent(), float_utilst::get_fraction(), float_utilst::round_fraction(), and float_utilst::sticky_right_shift().
Definition at line 70 of file bv_utils.cpp.
Definition at line 58 of file bv_utils.cpp.
Referenced by float_utilst::normalization_shift().
literalt bv_utilst::full_adder | ( | const literalt | a, |
const literalt | b, | ||
const literalt | carry_in, | ||
literalt & | carry_out | ||
) |
Definition at line 140 of file bv_utils.cpp.
References carry(), carry_out(), propt::cnf_handled_well(), propt::has_set_to(), literalt::is_constant(), literalt::is_true(), propt::land(), propt::lcnf(), propt::lequal(), propt::lor(), propt::lxor(), propt::new_variable(), and prop.
Referenced by adder().
Definition at line 36 of file bv_utils.h.
References const_literal(), and incrementer().
Referenced by float_utilst::mul().
Definition at line 572 of file bv_utils.cpp.
References carry_out().
Referenced by inc(), negate(), float_utilst::round_fraction(), and boolbvt::type_conversion().
Definition at line 557 of file bv_utils.cpp.
References carry_out(), Forall_literals, propt::land(), propt::lxor(), and prop.
Definition at line 580 of file bv_utils.cpp.
References Forall_literals.
Referenced by add_sub(), adder_no_overflow(), boolbvt::convert_bitwise(), lt_or_le(), negate(), overflow_sub(), float_utilst::round_exponent(), and unsigned_less_than().
Definition at line 156 of file bv_utils.h.
References propt::land(), and prop.
Referenced by float_utilst::exponent_all_ones().
bool bv_utilst::is_constant | ( | const bvt & | bv | ) |
Definition at line 1303 of file bv_utils.cpp.
References forall_literals.
Referenced by equal(), unsigned_multiplier(), and unsigned_multiplier_no_overflow().
Definition at line 144 of file bv_utils.h.
References propt::lor(), and prop.
Referenced by float_utilst::div(), and unsigned_divider().
Definition at line 26 of file bv_utils.cpp.
References is_zero(), propt::land(), and prop.
Referenced by bv_refinementt::convert_mult().
Definition at line 141 of file bv_utils.h.
References propt::lor(), and prop.
Referenced by bv_refinementt::convert_mult(), boolbvt::convert_not(), float_utilst::denormalization_shift(), float_utilst::exponent_all_zeros(), float_utilst::fraction_all_zeros(), is_int_min(), is_one(), float_utilst::is_zero(), float_approximationt::normalization_shift(), float_utilst::normalization_shift(), float_utilst::round_exponent(), boolbvt::type_conversion(), and float_utilst::unpack().
literalt bv_utilst::lt_or_le | ( | bool | or_equal, |
const bvt & | bv0, | ||
const bvt & | bv1, | ||
representationt | rep | ||
) |
To provide a bitwise model of < or <=.
Definition at line 1147 of file bv_utils.cpp.
References carry(), carry_out(), propt::cnf_handled_well(), const_literal(), equal(), Forall_literals, propt::has_set_to(), inverted(), propt::l_set_to_true(), propt::lcnf(), propt::lequal(), propt::lor(), propt::lxor(), propt::new_variable(), prop, SIGNED, and UNSIGNED.
Referenced by rel(), signed_less_than(), unsigned_divider(), and unsigned_less_than().
bvt bv_utilst::multiplier | ( | const bvt & | op0, |
const bvt & | op1, | ||
representationt | rep | ||
) |
Definition at line 810 of file bv_utils.cpp.
References SIGNED, signed_multiplier(), UNREACHABLE, UNSIGNED, and unsigned_multiplier().
Referenced by bv_refinementt::check_SAT(), boolbvt::convert_mult(), and boolbvt::convert_overflow().
bvt bv_utilst::multiplier_no_overflow | ( | const bvt & | op0, |
const bvt & | op1, | ||
representationt | rep | ||
) |
Definition at line 823 of file bv_utils.cpp.
References SIGNED, signed_multiplier_no_overflow(), UNREACHABLE, UNSIGNED, and unsigned_multiplier_no_overflow().
Referenced by boolbvt::convert_mult().
Definition at line 532 of file bv_utils.cpp.
References carry_out(), const_literal(), incrementer(), and inverted().
Referenced by cond_negate(), boolbvt::convert_unary_minus(), negate_no_overflow(), overflow_sub(), and signed_divider().
Definition at line 540 of file bv_utils.cpp.
References propt::l_set_to(), negate(), overflow_negate(), and prop.
Referenced by boolbvt::convert_unary_minus().
literalt bv_utilst::overflow_add | ( | const bvt & | op0, |
const bvt & | op1, | ||
representationt | rep | ||
) |
Definition at line 367 of file bv_utils.cpp.
References add(), carry_out(), const_literal(), propt::land(), propt::lequal(), propt::lxor(), prop, SIGNED, UNREACHABLE, and UNSIGNED.
Referenced by boolbvt::convert_overflow(), and overflow_sub().
Definition at line 546 of file bv_utils.cpp.
References propt::land(), propt::lor(), prop, and zeros().
Referenced by cond_negate_no_overflow(), boolbvt::convert_overflow(), boolbvt::convert_unary_minus(), and negate_no_overflow().
literalt bv_utilst::overflow_sub | ( | const bvt & | op0, |
const bvt & | op1, | ||
representationt | rep | ||
) |
Definition at line 391 of file bv_utils.cpp.
References carry_out(), const_literal(), inverted(), is_int_min(), propt::lselect(), negate(), overflow_add(), prop, SIGNED, UNREACHABLE, and UNSIGNED.
Referenced by boolbvt::convert_overflow().
literalt bv_utilst::rel | ( | const bvt & | bv0, |
irep_idt | id, | ||
const bvt & | bv1, | ||
representationt | rep | ||
) |
Definition at line 1281 of file bv_utils.cpp.
References equal(), lt_or_le(), and UNREACHABLE.
Referenced by boolbvt::convert_bv_rel(), boolbvt::convert_overflow(), and bv_pointerst::convert_rest().
|
inline |
Definition at line 94 of file bv_utils.h.
References divider().
Referenced by bv_refinementt::check_SAT().
If s is true, selects a otherwise selects b.
Definition at line 96 of file bv_utils.cpp.
References propt::lselect(), and prop.
Referenced by add_sub(), float_utilst::add_sub(), bv_pointerst::convert_address_of_rec(), boolbvt::convert_if(), boolbvt::convert_power(), float_utilst::denormalization_shift(), float_utilst::div(), float_utilst::normalization_shift(), float_utilst::round_exponent(), float_utilst::sticky_right_shift(), and float_utilst::unpack().
Definition at line 35 of file bv_utils.cpp.
References prop, and propt::set_equal().
Referenced by bv_refinementt::check_SAT().
Definition at line 480 of file bv_utils.cpp.
References const_literal(), ROTATE_LEFT, ROTATE_RIGHT, SHIFT_ARIGHT, SHIFT_LEFT, SHIFT_LRIGHT, and UNREACHABLE.
Referenced by boolbvt::convert_overflow(), boolbvt::convert_power(), boolbvt::convert_shift(), float_utilst::denormalization_shift(), float_approximationt::normalization_shift(), float_utilst::normalization_shift(), shift(), float_utilst::sticky_right_shift(), float_utilst::to_integer(), and unsigned_divider().
Definition at line 459 of file bv_utils.cpp.
References const_literal(), propt::lselect(), prop, and shift().
Definition at line 136 of file bv_utils.h.
Definition at line 179 of file bv_utils.h.
References extension(), and SIGNED.
Referenced by float_utilst::add_sub(), float_utilst::conversion(), bv_pointerst::convert_bitvector(), boolbvt::convert_div(), boolbvt::convert_mult(), float_utilst::denormalization_shift(), float_utilst::div(), float_utilst::mul(), float_utilst::normalization_shift(), float_utilst::rounder(), and float_utilst::subtract_exponents().
Definition at line 838 of file bv_utils.cpp.
References propt::lselect(), propt::lxor(), negate(), prop, and unsigned_divider().
Referenced by divider().
Definition at line 1274 of file bv_utils.cpp.
References lt_or_le(), and SIGNED.
Referenced by float_utilst::round_exponent().
Definition at line 742 of file bv_utils.cpp.
References cond_negate(), propt::lxor(), prop, and unsigned_multiplier().
Referenced by boolbvt::convert_mult(), and multiplier().
Definition at line 788 of file bv_utils.cpp.
References cond_negate_no_overflow(), propt::l_set_to(), propt::lxor(), prop, and unsigned_multiplier_no_overflow().
Referenced by multiplier_no_overflow().
Definition at line 65 of file bv_utils.h.
References add_sub().
Referenced by bv_pointerst::convert_bitvector(), float_utilst::denormalization_shift(), float_utilst::div(), float_utilst::normalization_shift(), float_utilst::sub_bias(), float_utilst::subtract_exponents(), and float_utilst::to_integer().
Definition at line 892 of file bv_utils.cpp.
References adder_no_overflow(), const_literal(), equal(), literalt::is_false(), is_not_zero(), literalt::is_true(), propt::l_set_to_true(), propt::limplies(), propt::lor(), lt_or_le(), propt::new_variable(), prop, shift(), UNSIGNED, and unsigned_multiplier_no_overflow().
Referenced by float_utilst::div(), divider(), and signed_divider().
Definition at line 1262 of file bv_utils.cpp.
References carry_out(), const_literal(), inverted(), and lt_or_le().
Referenced by float_utilst::relation().
Definition at line 633 of file bv_utils.cpp.
References add(), const_literal(), is_constant(), propt::land(), prop, wallace_tree(), and zeros().
Referenced by float_utilst::mul(), multiplier(), bv_pointerst::offset_arithmetic(), and signed_multiplier().
Definition at line 703 of file bv_utils.cpp.
References adder_no_overflow(), const_literal(), is_constant(), propt::l_set_to_false(), propt::land(), and prop.
Referenced by multiplier_no_overflow(), signed_multiplier_no_overflow(), and unsigned_divider().
Definition at line 1335 of file bv_utils.cpp.
References propt::lor(), and prop.
Referenced by boolbvt::convert_not().
Definition at line 1350 of file bv_utils.cpp.
Referenced by boolbvt::convert_not().
Definition at line 588 of file bv_utils.cpp.
References add(), carry(), const_literal(), propt::lxor(), and prop.
Referenced by unsigned_multiplier().
Definition at line 184 of file bv_utils.h.
References extension(), and UNSIGNED.
Referenced by float_utilst::add_sub(), bv_pointerst::convert_bitvector(), bv_pointerst::convert_pointer_type(), float_utilst::div(), float_utilst::mul(), bv_pointerst::offset_arithmetic(), float_utilst::round_fraction(), and boolbvt::type_conversion().
|
inline |
Definition at line 189 of file bv_utils.h.
References const_literal().
Referenced by float_utilst::add_sub(), float_utilst::conversion(), float_utilst::denormalization_shift(), float_utilst::div(), float_utilst::normalization_shift(), overflow_negate(), float_utilst::round_exponent(), float_utilst::round_fraction(), and unsigned_multiplier().
|
protected |
Definition at line 221 of file bv_utils.h.
Referenced by adder_no_overflow(), carry(), cond_implies_equal(), cond_negate(), cond_negate_no_overflow(), divider(), equal(), full_adder(), incrementer(), is_all_ones(), is_not_zero(), is_one(), is_zero(), lt_or_le(), negate_no_overflow(), overflow_add(), overflow_negate(), overflow_sub(), select(), set_equal(), shift(), signed_divider(), signed_multiplier(), signed_multiplier_no_overflow(), unsigned_divider(), unsigned_multiplier(), unsigned_multiplier_no_overflow(), verilog_bv_has_x_or_z(), and wallace_tree().