Loading...

Searching...

No Matches

bv_utilst Class Reference

#include <bv_utils.h>

+ Collaboration diagram for bv_utilst:

[フレーム]

[legend]

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 &)

bvt popcount (const bvt &bv)

Symbolic implementation of popcount (count of 1 bits in a bit vector) Based on the pop0 algorithm from Hacker's Delight.

Static Public Member Functions

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

static mp_integer from_constant (const bvt &bv)

Returns the unsigned integer value of the constant bitvector bv.

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

std::pair< bvt, literalt > adder (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.

bvt adder_no_overflow (const bvt &op0, const bvt &op1, bool subtract, representationt rep)

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

propt & prop

Detailed Description

Definition at line 23 of file bv_utils.h.

Member Enumeration Documentation

◆ representationt

enum class bv_utilst::representationt

strong

Enumerator
SIGNED
UNSIGNED

Definition at line 28 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 78 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 1045 of file bv_utils.cpp.

◆ add()

bvt bv_utilst::add ( const bvt & op0,

const bvt & op1

)

inline

Definition at line 71 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 349 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 361 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 340 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 309 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 522 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 487 of file bv_utils.cpp.

◆ build_constant()

bvt bv_utilst::build_constant ( const mp_integer & i,

std::size_t width

)

static

Definition at line 16 of file bv_utils.cpp.

◆ carry()

literalt bv_utilst::carry ( literalt a,

literalt b,

literalt c

)

Definition at line 242 of file bv_utils.cpp.

◆ carry_out()

literalt bv_utilst::carry_out ( const bvt & op0,

const bvt & op1,

literalt carry_in

)

Definition at line 325 of file bv_utils.cpp.

◆ concatenate()

bvt bv_utilst::concatenate ( const bvt & a,

const bvt & b

)

static

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

◆ cond_negate()

bvt bv_utilst::cond_negate ( const bvt & bv,

const literalt cond

)

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

◆ dadda_tree()

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

protected

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

◆ divider() [2/2]

bvt bv_utilst::divider ( const bvt & op0,

const bvt & op1,

representationt rep

)

inline

Definition at line 94 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: op0 Lhs bitvector to compare

op1 Rhs bitvector to compare

Returns: The literal that is true if and only if they are equal.

Definition at line 1397 of file bv_utils.cpp.

◆ extension()

bvt bv_utilst::extension ( const bvt & bv,

std::size_t new_size,

representationt rep

)

static

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

◆ extract_lsb()

bvt bv_utilst::extract_lsb ( const bvt & a,

std::size_t n

)

static

Definition at line 81 of file bv_utils.cpp.

◆ extract_msb()

bvt bv_utilst::extract_msb ( const bvt & a,

std::size_t n

)

static

Definition at line 69 of file bv_utils.cpp.

◆ from_constant()

mp_integer bv_utilst::from_constant ( const bvt & bv )

static

Returns the unsigned integer value of the constant bitvector bv.

This is the inverse of build_constant for non-negative values.

Precondition: all literals in bv are constant (see is_constant)

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

◆ inc()

bvt bv_utilst::inc ( const bvt & op )

inline

Definition at line 38 of file bv_utils.h.

◆ incrementer() [1/2]

void bv_utilst::incrementer ( bvt & op,

literalt carry_in,

literalt & carry_out

)

Definition at line 625 of file bv_utils.cpp.

◆ incrementer() [2/2]

bvt bv_utilst::incrementer ( const bvt & op,

literalt carry_in

)

Definition at line 640 of file bv_utils.cpp.

◆ inverted()

bvt bv_utilst::inverted ( const bvt & op )

static

Definition at line 648 of file bv_utils.cpp.

◆ is_all_ones()

literalt bv_utilst::is_all_ones ( const bvt & op )

inline

Definition at line 163 of file bv_utils.h.

◆ is_constant()

bool bv_utilst::is_constant ( const bvt & bv )

static

Definition at line 1673 of file bv_utils.cpp.

◆ is_int_min()

literalt bv_utilst::is_int_min ( const bvt & op )

inline

Definition at line 154 of file bv_utils.h.

◆ is_not_zero()

literalt bv_utilst::is_not_zero ( const bvt & op )

inline

Definition at line 151 of file bv_utils.h.

◆ is_one()

literalt bv_utilst::is_one ( const bvt & op )

Definition at line 37 of file bv_utils.cpp.

◆ is_zero()

literalt bv_utilst::is_zero ( const bvt & op )

inline

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

◆ multiplier()

bvt bv_utilst::multiplier ( const bvt & op0,

const bvt & op1,

representationt rep

)

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

◆ negate()

bvt bv_utilst::negate ( const bvt & op )

Definition at line 600 of file bv_utils.cpp.

◆ negate_no_overflow()

bvt bv_utilst::negate_no_overflow ( const bvt & op )

Definition at line 608 of file bv_utils.cpp.

◆ overflow_add()

literalt bv_utilst::overflow_add ( const bvt & op0,

const bvt & op1,

representationt rep

)

Definition at line 439 of file bv_utils.cpp.

◆ overflow_negate()

literalt bv_utilst::overflow_negate ( const bvt & op )

Definition at line 614 of file bv_utils.cpp.

◆ overflow_sub()

literalt bv_utilst::overflow_sub ( const bvt & op0,

const bvt & op1,

representationt rep

)

Definition at line 462 of file bv_utils.cpp.

◆ popcount()

bvt bv_utilst::popcount ( const bvt & bv )

Symbolic implementation of popcount (count of 1 bits in a bit vector) Based on the pop0 algorithm from Hacker's Delight.

Parameters: bv The bit vector to count 1s in

Returns: A bit vector representing the count

Definition at line 1741 of file bv_utils.cpp.

◆ rel()

literalt bv_utilst::rel ( const bvt & bv0,

irep_idt id,

const bvt & bv1,

representationt rep

)

Definition at line 1651 of file bv_utils.cpp.

◆ remainder()

bvt bv_utilst::remainder ( const bvt & op0,

const bvt & op1,

representationt rep

)

inline

Definition at line 101 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 370 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 107 of file bv_utils.cpp.

◆ set_equal()

void bv_utilst::set_equal ( const bvt & a,

const bvt & b

)

Definition at line 46 of file bv_utils.cpp.

◆ shift() [1/2]

bvt bv_utilst::shift ( const bvt & op,

const shiftt shift,

const bvt & distance

)

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

◆ sign_bit()

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

inlinestatic

Definition at line 143 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 187 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 1115 of file bv_utils.cpp.

◆ signed_less_than()

literalt bv_utilst::signed_less_than ( const bvt & bv0,

const bvt & bv1

)

Definition at line 1644 of file bv_utils.cpp.

◆ signed_multiplier()

bvt bv_utilst::signed_multiplier ( const bvt & op0,

const bvt & op1

)

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

◆ sub()

bvt bv_utilst::sub ( const bvt & op0,

const bvt & op1

)

inline

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

◆ unsigned_less_than()

literalt bv_utilst::unsigned_less_than ( const bvt & bv0,

const bvt & bv1

)

Definition at line 1637 of file bv_utils.cpp.

◆ unsigned_multiplier()

bvt bv_utilst::unsigned_multiplier ( const bvt & op0,

const bvt & op1

)

Definition at line 930 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 975 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 1707 of file bv_utils.cpp.

◆ verilog_bv_normal_bits()

bvt bv_utilst::verilog_bv_normal_bits ( const bvt & src )

static

Definition at line 1722 of file bv_utils.cpp.

◆ wallace_tree()

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

protected

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

◆ zeros()

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

inlinestatic

Definition at line 197 of file bv_utils.h.

Member Data Documentation

◆ prop

propt& bv_utilst::prop

protected

Definition at line 233 of file bv_utils.h.

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

/home/runner/work/cbmc/cbmc/src/solvers/flattening/bv_utils.h
/home/runner/work/cbmc/cbmc/src/solvers/flattening/bv_utils.cpp

bv_utilst
Generated by doxygen 1.9.8