cprover
bv_utilst Class Reference

#include <bv_utils.h>

Collaboration diagram for bv_utilst:
[legend]

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

proptprop
 

Detailed Description

Definition at line 26 of file bv_utils.h.

Member Enumeration Documentation

◆ representationt

Enumerator
SIGNED 
UNSIGNED 

Definition at line 31 of file bv_utils.h.

◆ shiftt

enum bv_utilst::shiftt
strong
Enumerator
SHIFT_LEFT 
SHIFT_LRIGHT 
SHIFT_ARIGHT 
ROTATE_LEFT 
ROTATE_RIGHT 

Definition at line 71 of file bv_utils.h.

Constructor & Destructor Documentation

◆ bv_utilst()

bv_utilst::bv_utilst ( propt _prop)
inlineexplicit

Definition at line 29 of file bv_utils.h.

Member Function Documentation

◆ absolute_value()

bvt bv_utilst::absolute_value ( const bvt op)

◆ add()

◆ add_sub() [1/2]

bvt bv_utilst::add_sub ( const bvt op0,
const bvt op1,
bool  subtract 
)

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().

◆ add_sub() [2/2]

bvt bv_utilst::add_sub ( const bvt op0,
const bvt op1,
literalt  subtract 
)

Definition at line 354 of file bv_utils.cpp.

References adder(), carry_out(), inverted(), and select().

◆ add_sub_no_overflow()

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().

◆ adder()

void bv_utilst::adder ( bvt sum,
const bvt op,
literalt  carry_in,
literalt carry_out 
)
protected

Definition at line 297 of file bv_utils.cpp.

References carry_out(), and full_adder().

Referenced by add_sub(), and adder_no_overflow().

◆ adder_no_overflow() [1/2]

void bv_utilst::adder_no_overflow ( bvt sum,
const bvt op,
bool  subtract,
representationt  rep 
)
protected

◆ adder_no_overflow() [2/2]

void bv_utilst::adder_no_overflow ( bvt sum,
const bvt op 
)
protected

Definition at line 450 of file bv_utils.cpp.

References adder(), carry_out(), const_literal(), propt::l_set_to_false(), and prop.

◆ build_constant()

◆ carry()

◆ carry_out()

literalt bv_utilst::carry_out ( const bvt op0,
const bvt op1,
literalt  carry_in 
)

◆ concatenate()

bvt bv_utilst::concatenate ( const bvt a,
const bvt b 
) const

◆ cond_implies_equal()

void bv_utilst::cond_implies_equal ( literalt  cond,
const bvt a,
const bvt b 
)

◆ cond_negate()

bvt bv_utilst::cond_negate ( const bvt bv,
const literalt  cond 
)

◆ cond_negate_no_overflow()

bvt bv_utilst::cond_negate_no_overflow ( const bvt bv,
const literalt  cond 
)
protected

◆ divider() [1/2]

bvt bv_utilst::divider ( const bvt op0,
const bvt op1,
representationt  rep 
)
inline

◆ divider() [2/2]

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().

◆ equal()

◆ extension()

bvt bv_utilst::extension ( const bvt bv,
std::size_t  new_size,
representationt  rep 
)

◆ extract()

bvt bv_utilst::extract ( const bvt a,
std::size_t  first,
std::size_t  last 
)
static

◆ extract_lsb()

bvt bv_utilst::extract_lsb ( const bvt a,
std::size_t  n 
)
static

Definition at line 70 of file bv_utils.cpp.

◆ extract_msb()

bvt bv_utilst::extract_msb ( const bvt a,
std::size_t  n 
)
static

Definition at line 58 of file bv_utils.cpp.

Referenced by float_utilst::normalization_shift().

◆ full_adder()

literalt bv_utilst::full_adder ( const literalt  a,
const literalt  b,
const literalt  carry_in,
literalt carry_out 
)

◆ inc()

bvt bv_utilst::inc ( const bvt op)
inline

Definition at line 36 of file bv_utils.h.

References const_literal(), and incrementer().

Referenced by float_utilst::mul().

◆ incrementer() [1/2]

bvt bv_utilst::incrementer ( const bvt op,
literalt  carry_in 
)

Definition at line 572 of file bv_utils.cpp.

References carry_out().

Referenced by inc(), negate(), float_utilst::round_fraction(), and boolbvt::type_conversion().

◆ incrementer() [2/2]

void bv_utilst::incrementer ( bvt op,
literalt  carry_in,
literalt carry_out 
)

Definition at line 557 of file bv_utils.cpp.

References carry_out(), Forall_literals, propt::land(), propt::lxor(), and prop.

◆ inverted()

bvt bv_utilst::inverted ( const bvt op)

◆ is_all_ones()

literalt bv_utilst::is_all_ones ( const bvt op)
inline

Definition at line 156 of file bv_utils.h.

References propt::land(), and prop.

Referenced by float_utilst::exponent_all_ones().

◆ is_constant()

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().

◆ is_int_min()

literalt bv_utilst::is_int_min ( const bvt op)
inline

Definition at line 147 of file bv_utils.h.

References is_zero().

Referenced by overflow_sub().

◆ is_not_zero()

literalt bv_utilst::is_not_zero ( const bvt op)
inline

Definition at line 144 of file bv_utils.h.

References propt::lor(), and prop.

Referenced by float_utilst::div(), and unsigned_divider().

◆ is_one()

literalt bv_utilst::is_one ( const bvt op)

Definition at line 26 of file bv_utils.cpp.

References is_zero(), propt::land(), and prop.

Referenced by bv_refinementt::convert_mult().

◆ is_zero()

◆ lt_or_le()

literalt bv_utilst::lt_or_le ( bool  or_equal,
const bvt bv0,
const bvt bv1,
representationt  rep 
)

To provide a bitwise model of < or <=.

parameters: bvts for each input and whether they are signed and whether
a model of < or <= is required.
Returns
A literalt that models the value of the comparison.

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().

◆ multiplier()

bvt bv_utilst::multiplier ( const bvt op0,
const bvt op1,
representationt  rep 
)

◆ multiplier_no_overflow()

bvt bv_utilst::multiplier_no_overflow ( const bvt op0,
const bvt op1,
representationt  rep 
)

◆ negate()

bvt bv_utilst::negate ( const bvt op)

◆ negate_no_overflow()

bvt bv_utilst::negate_no_overflow ( const bvt op)

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().

◆ overflow_add()

literalt bv_utilst::overflow_add ( const bvt op0,
const bvt op1,
representationt  rep 
)

◆ overflow_negate()

literalt bv_utilst::overflow_negate ( const bvt op)

◆ overflow_sub()

literalt bv_utilst::overflow_sub ( const bvt op0,
const bvt op1,
representationt  rep 
)

◆ rel()

literalt bv_utilst::rel ( const bvt bv0,
irep_idt  id,
const bvt bv1,
representationt  rep 
)

◆ remainder()

bvt bv_utilst::remainder ( const bvt op0,
const bvt op1,
representationt  rep 
)
inline

Definition at line 94 of file bv_utils.h.

References divider().

Referenced by bv_refinementt::check_SAT().

◆ select()

◆ set_equal()

void bv_utilst::set_equal ( const bvt a,
const bvt b 
)

Definition at line 35 of file bv_utils.cpp.

References prop, and propt::set_equal().

Referenced by bv_refinementt::check_SAT().

◆ shift() [1/2]

◆ shift() [2/2]

bvt bv_utilst::shift ( const bvt op,
const shiftt  shift,
const bvt distance 
)

Definition at line 459 of file bv_utils.cpp.

References const_literal(), propt::lselect(), prop, and shift().

◆ sign_bit()

static literalt bv_utilst::sign_bit ( const bvt op)
inlinestatic

Definition at line 136 of file bv_utils.h.

◆ sign_extension()

◆ signed_divider()

void bv_utilst::signed_divider ( const bvt op0,
const bvt op1,
bvt res,
bvt rem 
)

Definition at line 838 of file bv_utils.cpp.

References propt::lselect(), propt::lxor(), negate(), prop, and unsigned_divider().

Referenced by divider().

◆ signed_less_than()

literalt bv_utilst::signed_less_than ( const bvt bv0,
const bvt bv1 
)

Definition at line 1274 of file bv_utils.cpp.

References lt_or_le(), and SIGNED.

Referenced by float_utilst::round_exponent().

◆ signed_multiplier()

bvt bv_utilst::signed_multiplier ( const bvt op0,
const bvt op1 
)

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().

◆ signed_multiplier_no_overflow()

bvt bv_utilst::signed_multiplier_no_overflow ( const bvt op0,
const bvt op1 
)
protected

◆ sub()

◆ unsigned_divider()

◆ unsigned_less_than()

literalt bv_utilst::unsigned_less_than ( const bvt bv0,
const bvt bv1 
)

Definition at line 1262 of file bv_utils.cpp.

References carry_out(), const_literal(), inverted(), and lt_or_le().

Referenced by float_utilst::relation().

◆ unsigned_multiplier()

bvt bv_utilst::unsigned_multiplier ( const bvt op0,
const bvt op1 
)

◆ unsigned_multiplier_no_overflow()

bvt bv_utilst::unsigned_multiplier_no_overflow ( const bvt op0,
const bvt op1 
)
protected

◆ verilog_bv_has_x_or_z()

literalt bv_utilst::verilog_bv_has_x_or_z ( const bvt src)

Definition at line 1335 of file bv_utils.cpp.

References propt::lor(), and prop.

Referenced by boolbvt::convert_not().

◆ verilog_bv_normal_bits()

bvt bv_utilst::verilog_bv_normal_bits ( const bvt src)

Definition at line 1350 of file bv_utils.cpp.

Referenced by boolbvt::convert_not().

◆ wallace_tree()

bvt bv_utilst::wallace_tree ( const std::vector< bvt > &  pps)
protected

Definition at line 588 of file bv_utils.cpp.

References add(), carry(), const_literal(), propt::lxor(), and prop.

Referenced by unsigned_multiplier().

◆ zero_extension()

◆ zeros()

Member Data Documentation

◆ prop


The documentation for this class was generated from the following files: