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. 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)
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. 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	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. More...
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 bv_utilst::representationt

strong

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

add()

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

inline

Definition at line 66 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 337 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 349 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()

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 297 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 511 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 476 of file bv_utils.cpp.

build_constant()

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

static

Definition at line 14 of file bv_utils.cpp.

carry()

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

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

static

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

cond_negate()

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

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

dadda_tree()

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

protected

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

divider() [2/2]

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

inline

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

extension()

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

static

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

extract_lsb()

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

static

Definition at line 69 of file bv_utils.cpp.

extract_msb()

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

static

Definition at line 57 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 139 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 614 of file bv_utils.cpp.

incrementer() [2/2]

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

Definition at line 629 of file bv_utils.cpp.

inverted()

bvt bv_utilst::inverted ( const bvt &  op )

static

Definition at line 637 of file bv_utils.cpp.

is_all_ones()

literalt bv_utilst::is_all_ones ( const bvt &  op )

inline

Definition at line 158 of file bv_utils.h.

is_constant()

bool bv_utilst::is_constant ( const bvt &  bv )

static

Definition at line 1584 of file bv_utils.cpp.

is_int_min()

literalt bv_utilst::is_int_min ( const bvt &  op )

inline

Definition at line 149 of file bv_utils.h.

is_not_zero()

literalt bv_utilst::is_not_zero ( const bvt &  op )

inline

Definition at line 146 of file bv_utils.h.

is_one()

literalt bv_utilst::is_one

(

const bvt &

op

)

Definition at line 25 of file bv_utils.cpp.

is_zero()

literalt bv_utilst::is_zero ( const bvt &  op )

inline

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

multiplier()

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

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

negate()

bvt bv_utilst::negate

(

const bvt &

op

)

Definition at line 589 of file bv_utils.cpp.

negate_no_overflow()

bvt bv_utilst::negate_no_overflow

(

const bvt &

op

)

Definition at line 597 of file bv_utils.cpp.

overflow_add()

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

Definition at line 427 of file bv_utils.cpp.

overflow_negate()

literalt bv_utilst::overflow_negate

(

const bvt &

op

)

Definition at line 603 of file bv_utils.cpp.

overflow_sub()

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

Definition at line 451 of file bv_utils.cpp.

rel()

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

Definition at line 1562 of file bv_utils.cpp.

remainder()

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

inline

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

set_equal()

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

Definition at line 34 of file bv_utils.cpp.

shift() [1/2]

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

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

sign_bit()

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

inlinestatic

Definition at line 138 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 182 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 1104 of file bv_utils.cpp.

signed_less_than()

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

Definition at line 1555 of file bv_utils.cpp.

signed_multiplier()

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

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

sub()

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

inline

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

unsigned_less_than()

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

Definition at line 1543 of file bv_utils.cpp.

unsigned_multiplier()

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

Definition at line 919 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 964 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 1618 of file bv_utils.cpp.

verilog_bv_normal_bits()

bvt bv_utilst::verilog_bv_normal_bits ( const bvt &  src )

static

Definition at line 1633 of file bv_utils.cpp.

wallace_tree()

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

protected

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

zeros()

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

inlinestatic

Definition at line 192 of file bv_utils.h.

Member Data Documentation

prop

propt& bv_utilst::prop

protected

Definition at line 222 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