cprover
bv_utilst Class Reference

#include <bv_utils.h>

+ Collaboration diagram for bv_utilst:

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)

Definition at line 775 of file bv_utils.cpp.

◆ add()

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

Definition at line 64 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 339 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 354 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 328 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 297 of file bv_utils.cpp.

◆ adder_no_overflow() [1/2]

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

Definition at line 416 of file bv_utils.cpp.

◆ adder_no_overflow() [2/2]

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

Definition at line 451 of file bv_utils.cpp.

◆ build_constant()

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

Definition at line 15 of file bv_utils.cpp.

◆ carry()

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

Definition at line 231 of file bv_utils.cpp.

◆ carry_out()

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

Definition at line 313 of file bv_utils.cpp.

◆ concatenate()

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

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

◆ cond_negate()

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

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

◆ divider() [1/2]

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

Definition at line 87 of file bv_utils.h.

◆ divider() [2/2]

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

Definition at line 875 of file bv_utils.cpp.

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

◆ extension()

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

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

◆ 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.

◆ full_adder()

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.

◆ inc()

bvt bv_utilst::inc ( const bvt op)
inline

Definition at line 36 of file bv_utils.h.

◆ incrementer() [1/2]

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

Definition at line 573 of file bv_utils.cpp.

◆ incrementer() [2/2]

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

Definition at line 558 of file bv_utils.cpp.

◆ inverted()

bvt bv_utilst::inverted ( const bvt op)

Definition at line 581 of file bv_utils.cpp.

◆ is_all_ones()

literalt bv_utilst::is_all_ones ( const bvt op)
inline

Definition at line 156 of file bv_utils.h.

◆ is_constant()

bool bv_utilst::is_constant ( const bvt bv)

Definition at line 1312 of file bv_utils.cpp.

◆ is_int_min()

literalt bv_utilst::is_int_min ( const bvt op)
inline

Definition at line 147 of file bv_utils.h.

◆ is_not_zero()

literalt bv_utilst::is_not_zero ( const bvt op)
inline

Definition at line 144 of file bv_utils.h.

◆ is_one()

literalt bv_utilst::is_one ( const bvt op)

Definition at line 26 of file bv_utils.cpp.

◆ is_zero()

literalt bv_utilst::is_zero ( const bvt op)
inline

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

◆ multiplier()

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

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

◆ negate()

bvt bv_utilst::negate ( const bvt op)

Definition at line 533 of file bv_utils.cpp.

◆ negate_no_overflow()

bvt bv_utilst::negate_no_overflow ( const bvt op)

Definition at line 541 of file bv_utils.cpp.

◆ overflow_add()

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

Definition at line 367 of file bv_utils.cpp.

◆ overflow_negate()

literalt bv_utilst::overflow_negate ( const bvt op)

Definition at line 547 of file bv_utils.cpp.

◆ overflow_sub()

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

Definition at line 391 of file bv_utils.cpp.

◆ rel()

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

Definition at line 1290 of file bv_utils.cpp.

◆ remainder()

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

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

◆ set_equal()

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

Definition at line 35 of file bv_utils.cpp.

◆ shift() [1/2]

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

Definition at line 481 of file bv_utils.cpp.

◆ shift() [2/2]

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

Definition at line 460 of file bv_utils.cpp.

◆ sign_bit()

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

Definition at line 136 of file bv_utils.h.

◆ sign_extension()

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

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

◆ signed_less_than()

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

Definition at line 1283 of file bv_utils.cpp.

◆ signed_multiplier()

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

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

◆ sub()

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

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

◆ unsigned_less_than()

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

Definition at line 1271 of file bv_utils.cpp.

◆ unsigned_multiplier()

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

Definition at line 635 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 705 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 1344 of file bv_utils.cpp.

◆ verilog_bv_normal_bits()

bvt bv_utilst::verilog_bv_normal_bits ( const bvt src)

Definition at line 1359 of file bv_utils.cpp.

◆ wallace_tree()

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

Definition at line 589 of file bv_utils.cpp.

◆ zero_extension()

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

Definition at line 184 of file bv_utils.h.

◆ zeros()

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

Definition at line 189 of file bv_utils.h.

Member Data Documentation

◆ prop

propt& bv_utilst::prop
protected

Definition at line 221 of file bv_utils.h.


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