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

enum class bv_utilst::representationt
strong
Enumerator
SIGNED 
UNSIGNED 

Definition at line 29 of file bv_utils.h.

◆ shiftt

enum class bv_utilst::shiftt
strong
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: