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

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 23 of file bv_utils.h.

Member Enumeration Documentation

◆ representationt

Enumerator
SIGNED 
UNSIGNED 

Definition at line 28 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 68 of file bv_utils.h.

Constructor & Destructor Documentation

◆ bv_utilst()

bv_utilst::bv_utilst ( propt _prop)
inlineexplicit

Definition at line 26 of file bv_utils.h.

Member Function Documentation

◆ absolute_value()

bvt bv_utilst::absolute_value ( const bvt op)

Definition at line 771 of file bv_utils.cpp.

◆ add()

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

Definition at line 61 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 335 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 350 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 324 of file bv_utils.cpp.

◆ adder()

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

Definition at line 293 of file bv_utils.cpp.

◆ adder_no_overflow() [1/2]

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

Definition at line 447 of file bv_utils.cpp.

◆ adder_no_overflow() [2/2]

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

Definition at line 412 of file bv_utils.cpp.

◆ build_constant()

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

Definition at line 11 of file bv_utils.cpp.

◆ carry()

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

Definition at line 227 of file bv_utils.cpp.

◆ carry_out()

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

Definition at line 309 of file bv_utils.cpp.

◆ concatenate()

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

Definition at line 76 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 1312 of file bv_utils.cpp.

◆ cond_negate()

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

Definition at line 758 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 777 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 871 of file bv_utils.cpp.

◆ divider() [2/2]

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

Definition at line 84 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 1103 of file bv_utils.cpp.

◆ extension()

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

Definition at line 105 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 38 of file bv_utils.cpp.

◆ extract_lsb()

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

Definition at line 66 of file bv_utils.cpp.

◆ extract_msb()

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

Definition at line 54 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 136 of file bv_utils.cpp.

◆ inc()

bvt bv_utilst::inc ( const bvt op)
inline

Definition at line 33 of file bv_utils.h.

◆ incrementer() [1/2]

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

Definition at line 554 of file bv_utils.cpp.

◆ incrementer() [2/2]

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

Definition at line 569 of file bv_utils.cpp.

◆ inverted()

bvt bv_utilst::inverted ( const bvt op)
static

Definition at line 577 of file bv_utils.cpp.

◆ is_all_ones()

literalt bv_utilst::is_all_ones ( const bvt op)
inline

Definition at line 153 of file bv_utils.h.

◆ is_constant()

bool bv_utilst::is_constant ( const bvt bv)
static

Definition at line 1301 of file bv_utils.cpp.

◆ is_int_min()

literalt bv_utilst::is_int_min ( const bvt op)
inline

Definition at line 144 of file bv_utils.h.

◆ is_not_zero()

literalt bv_utilst::is_not_zero ( const bvt op)
inline

Definition at line 141 of file bv_utils.h.

◆ is_one()

literalt bv_utilst::is_one ( const bvt op)

Definition at line 22 of file bv_utils.cpp.

◆ is_zero()

literalt bv_utilst::is_zero ( const bvt op)
inline

Definition at line 138 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 
)

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 1142 of file bv_utils.cpp.

◆ multiplier()

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

Definition at line 806 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 820 of file bv_utils.cpp.

◆ negate()

bvt bv_utilst::negate ( const bvt op)

Definition at line 529 of file bv_utils.cpp.

◆ negate_no_overflow()

bvt bv_utilst::negate_no_overflow ( const bvt op)

Definition at line 537 of file bv_utils.cpp.

◆ overflow_add()

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

Definition at line 363 of file bv_utils.cpp.

◆ overflow_negate()

literalt bv_utilst::overflow_negate ( const bvt op)

Definition at line 543 of file bv_utils.cpp.

◆ overflow_sub()

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

Definition at line 387 of file bv_utils.cpp.

◆ rel()

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

Definition at line 1279 of file bv_utils.cpp.

◆ remainder()

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

Definition at line 91 of file bv_utils.h.

◆ 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 92 of file bv_utils.cpp.

◆ set_equal()

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

Definition at line 31 of file bv_utils.cpp.

◆ shift() [1/2]

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

Definition at line 456 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 477 of file bv_utils.cpp.

◆ sign_bit()

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

Definition at line 133 of file bv_utils.h.

◆ sign_extension()

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

Definition at line 177 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 836 of file bv_utils.cpp.

◆ signed_less_than()

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

Definition at line 1272 of file bv_utils.cpp.

◆ signed_multiplier()

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

Definition at line 740 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 784 of file bv_utils.cpp.

◆ sub()

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

Definition at line 62 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 889 of file bv_utils.cpp.

◆ unsigned_less_than()

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

Definition at line 1260 of file bv_utils.cpp.

◆ unsigned_multiplier()

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

Definition at line 631 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 701 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 1335 of file bv_utils.cpp.

◆ verilog_bv_normal_bits()

bvt bv_utilst::verilog_bv_normal_bits ( const bvt src)
static

Definition at line 1350 of file bv_utils.cpp.

◆ wallace_tree()

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

Definition at line 585 of file bv_utils.cpp.

◆ zero_extension()

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

Definition at line 182 of file bv_utils.h.

◆ zeros()

bvt bv_utilst::zeros ( std::size_t  new_size) const
inline

Definition at line 187 of file bv_utils.h.

Member Data Documentation

◆ prop

propt& bv_utilst::prop
protected

Definition at line 219 of file bv_utils.h.


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