cprover
Loading...
Searching...
No Matches
bv_utilst Class Reference

#include <bv_utils.h>

+ Collaboration diagram for bv_utilst:

Public Types

enum class  representationt { SIGNED , UNSIGNED }
 
enum class  shiftt {
  SHIFT_LEFT , SHIFT_LRIGHT , SHIFT_ARIGHT , ROTATE_LEFT ,
  ROTATE_RIGHT
}
 

Public Member Functions

 bv_utilst (propt &_prop)
 
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)
 
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 saturating_add_sub (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, 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.
 
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)
 
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)
 
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.
 
literalt verilog_bv_has_x_or_z (const bvt &)
 

Static Public Member Functions

static bvt build_constant (const mp_integer &i, std::size_t width)
 
static bvt inverted (const bvt &op)
 
static bvt shift (const bvt &op, const shiftt shift, std::size_t distance)
 
static literalt sign_bit (const bvt &op)
 
static bool is_constant (const bvt &bv)
 
static bvt extension (const bvt &bv, std::size_t new_size, representationt rep)
 
static bvt sign_extension (const bvt &bv, std::size_t new_size)
 
static bvt zero_extension (const bvt &bv, std::size_t new_size)
 
static bvt zeros (std::size_t new_size)
 
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)
 
static bvt concatenate (const bvt &a, const bvt &b)
 
static bvt verilog_bv_normal_bits (const bvt &)
 

Protected Member Functions

NODISCARD std::pair< bvt, literaltadder (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.
 
NODISCARD bvt adder_no_overflow (const bvt &op0, const bvt &op1, bool subtract, representationt rep)
 
NODISCARD bvt adder_no_overflow (const bvt &op0, const bvt &op1)
 
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)
 
bvt dadda_tree (const std::vector< bvt > &pps)
 

Protected Attributes

proptprop
 

Detailed Description

Definition at line 24 of file bv_utils.h.

Member Enumeration Documentation

◆ representationt

Enumerator
SIGNED 
UNSIGNED 

Definition at line 29 of file bv_utils.h.

◆ shiftt

Enumerator
SHIFT_LEFT 
SHIFT_LRIGHT 
SHIFT_ARIGHT 
ROTATE_LEFT 
ROTATE_RIGHT 

Definition at line 74 of file bv_utils.h.

Constructor & Destructor Documentation

◆ bv_utilst()

bv_utilst::bv_utilst ( propt _prop)
inlineexplicit

Definition at line 27 of file bv_utils.h.

Member Function Documentation

◆ absolute_value()

bvt bv_utilst::absolute_value ( const bvt op)

Definition at line 1033 of file bv_utils.cpp.

◆ add()

bvt bv_utilst::add ( const bvt op0,
const bvt op1 
)
inline

Definition at line 67 of file bv_utils.h.

◆ add_sub() [1/2]

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

Definition at line 336 of file bv_utils.cpp.

◆ add_sub() [2/2]

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

Definition at line 348 of file bv_utils.cpp.

◆ add_sub_no_overflow()

bvt bv_utilst::add_sub_no_overflow ( const bvt op0,
const bvt op1,
bool  subtract,
representationt  rep 
)

Definition at line 327 of file bv_utils.cpp.

◆ adder()

std::pair< bvt, literalt > bv_utilst::adder ( const bvt op0,
const bvt op1,
literalt  carry_in 
)
protected

Return the sum and carry-out when adding op0 and op1 under initial carry carry_in.

Definition at line 296 of file bv_utils.cpp.

◆ adder_no_overflow() [1/2]

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

Definition at line 510 of file bv_utils.cpp.

◆ adder_no_overflow() [2/2]

bvt bv_utilst::adder_no_overflow ( const bvt op0,
const bvt op1,
bool  subtract,
representationt  rep 
)
protected

Definition at line 475 of file bv_utils.cpp.

◆ build_constant()

bvt bv_utilst::build_constant ( const mp_integer i,
std::size_t  width 
)
static

Definition at line 13 of file bv_utils.cpp.

◆ carry()

literalt bv_utilst::carry ( literalt  a,
literalt  b,
literalt  c 
)

Definition at line 229 of file bv_utils.cpp.

◆ carry_out()

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

Definition at line 312 of file bv_utils.cpp.

◆ concatenate()

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

Definition at line 78 of file bv_utils.cpp.

◆ cond_implies_equal()

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

Definition at line 1589 of file bv_utils.cpp.

◆ cond_negate()

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

Definition at line 1020 of file bv_utils.cpp.

◆ cond_negate_no_overflow()

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

Definition at line 1039 of file bv_utils.cpp.

◆ dadda_tree()

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

Definition at line 691 of file bv_utils.cpp.

◆ divider() [1/2]

void bv_utilst::divider ( const bvt op0,
const bvt op1,
bvt res,
bvt rem,
representationt  rep 
)

Definition at line 1133 of file bv_utils.cpp.

◆ divider() [2/2]

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

Definition at line 90 of file bv_utils.h.

◆ equal()

literalt bv_utilst::equal ( const bvt op0,
const bvt op1 
)

Bit-blasting ID_equal and use in other encodings.

Parameters
op0Lhs bitvector to compare
op1Rhs bitvector to compare
Returns
The literal that is true if and only if they are equal.

Definition at line 1363 of file bv_utils.cpp.

◆ extension()

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

Definition at line 107 of file bv_utils.cpp.

◆ extract()

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

Definition at line 40 of file bv_utils.cpp.

◆ extract_lsb()

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

Definition at line 68 of file bv_utils.cpp.

◆ extract_msb()

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

Definition at line 56 of file bv_utils.cpp.

◆ full_adder()

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

Definition at line 138 of file bv_utils.cpp.

◆ inc()

bvt bv_utilst::inc ( const bvt op)
inline

Definition at line 34 of file bv_utils.h.

◆ incrementer() [1/2]

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

Definition at line 613 of file bv_utils.cpp.

◆ incrementer() [2/2]

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

Definition at line 628 of file bv_utils.cpp.

◆ inverted()

bvt bv_utilst::inverted ( const bvt op)
static

Definition at line 636 of file bv_utils.cpp.

◆ is_all_ones()

literalt bv_utilst::is_all_ones ( const bvt op)
inline

Definition at line 159 of file bv_utils.h.

◆ is_constant()

bool bv_utilst::is_constant ( const bvt bv)
static

Definition at line 1578 of file bv_utils.cpp.

◆ is_int_min()

literalt bv_utilst::is_int_min ( const bvt op)
inline

Definition at line 150 of file bv_utils.h.

◆ is_not_zero()

literalt bv_utilst::is_not_zero ( const bvt op)
inline

Definition at line 147 of file bv_utils.h.

◆ is_one()

literalt bv_utilst::is_one ( const bvt op)

Definition at line 24 of file bv_utils.cpp.

◆ is_zero()

literalt bv_utilst::is_zero ( const bvt op)
inline

Definition at line 144 of file bv_utils.h.

◆ lt_or_le()

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

Definition at line 1398 of file bv_utils.cpp.

◆ multiplier()

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

Definition at line 1068 of file bv_utils.cpp.

◆ multiplier_no_overflow()

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

Definition at line 1082 of file bv_utils.cpp.

◆ negate()

bvt bv_utilst::negate ( const bvt op)

Definition at line 588 of file bv_utils.cpp.

◆ negate_no_overflow()

bvt bv_utilst::negate_no_overflow ( const bvt op)

Definition at line 596 of file bv_utils.cpp.

◆ overflow_add()

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

Definition at line 426 of file bv_utils.cpp.

◆ overflow_negate()

literalt bv_utilst::overflow_negate ( const bvt op)

Definition at line 602 of file bv_utils.cpp.

◆ overflow_sub()

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

Definition at line 450 of file bv_utils.cpp.

◆ rel()

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

Definition at line 1556 of file bv_utils.cpp.

◆ remainder()

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

Definition at line 97 of file bv_utils.h.

◆ saturating_add_sub()

bvt bv_utilst::saturating_add_sub ( const bvt op0,
const bvt op1,
bool  subtract,
representationt  rep 
)

Definition at line 357 of file bv_utils.cpp.

◆ select()

bvt bv_utilst::select ( literalt  s,
const bvt a,
const bvt b 
)

If s is true, selects a otherwise selects b.

Definition at line 94 of file bv_utils.cpp.

◆ set_equal()

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

Definition at line 33 of file bv_utils.cpp.

◆ shift() [1/2]

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

Definition at line 515 of file bv_utils.cpp.

◆ shift() [2/2]

bvt bv_utilst::shift ( const bvt op,
const shiftt  shift,
std::size_t  distance 
)
static

Definition at line 536 of file bv_utils.cpp.

◆ sign_bit()

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

Definition at line 139 of file bv_utils.h.

◆ sign_extension()

static bvt bv_utilst::sign_extension ( const bvt bv,
std::size_t  new_size 
)
inlinestatic

Definition at line 183 of file bv_utils.h.

◆ signed_divider()

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

Definition at line 1098 of file bv_utils.cpp.

◆ signed_less_than()

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

Definition at line 1549 of file bv_utils.cpp.

◆ signed_multiplier()

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

Definition at line 1002 of file bv_utils.cpp.

◆ signed_multiplier_no_overflow()

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

Definition at line 1046 of file bv_utils.cpp.

◆ sub()

bvt bv_utilst::sub ( const bvt op0,
const bvt op1 
)
inline

Definition at line 68 of file bv_utils.h.

◆ unsigned_divider()

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

Definition at line 1151 of file bv_utils.cpp.

◆ unsigned_less_than()

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

Definition at line 1537 of file bv_utils.cpp.

◆ unsigned_multiplier()

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

Definition at line 918 of file bv_utils.cpp.

◆ unsigned_multiplier_no_overflow()

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

Definition at line 963 of file bv_utils.cpp.

◆ verilog_bv_has_x_or_z()

literalt bv_utilst::verilog_bv_has_x_or_z ( const bvt src)

Definition at line 1612 of file bv_utils.cpp.

◆ verilog_bv_normal_bits()

bvt bv_utilst::verilog_bv_normal_bits ( const bvt src)
static

Definition at line 1627 of file bv_utils.cpp.

◆ wallace_tree()

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

Definition at line 644 of file bv_utils.cpp.

◆ zero_extension()

static bvt bv_utilst::zero_extension ( const bvt bv,
std::size_t  new_size 
)
inlinestatic

Definition at line 188 of file bv_utils.h.

◆ zeros()

static bvt bv_utilst::zeros ( std::size_t  new_size)
inlinestatic

Definition at line 193 of file bv_utils.h.

Member Data Documentation

◆ prop

propt& bv_utilst::prop
protected

Definition at line 223 of file bv_utils.h.


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