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 &)
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 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 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 1035 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 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 351 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 330 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 299 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 512 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 477 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 232 of file bv_utils.cpp.

carry_out()

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

Definition at line 315 of file bv_utils.cpp.

concatenate()

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

static

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

cond_negate()

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

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

dadda_tree()

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

protected

Definition at line 693 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 1140 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 1370 of file bv_utils.cpp.

extension()

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

static

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

extract_lsb()

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

static

Definition at line 71 of file bv_utils.cpp.

extract_msb()

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

static

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

incrementer() [2/2]

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

Definition at line 630 of file bv_utils.cpp.

inverted()

bvt bv_utilst::inverted ( const bvt &  op )

static

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

multiplier()

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

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

negate()

bvt bv_utilst::negate

(

const bvt &

op

)

Definition at line 590 of file bv_utils.cpp.

negate_no_overflow()

bvt bv_utilst::negate_no_overflow

(

const bvt &

op

)

Definition at line 598 of file bv_utils.cpp.

overflow_add()

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

Definition at line 429 of file bv_utils.cpp.

overflow_negate()

literalt bv_utilst::overflow_negate

(

const bvt &

op

)

Definition at line 604 of file bv_utils.cpp.

overflow_sub()

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

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

rel()

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

Definition at line 1613 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 360 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 97 of file bv_utils.cpp.

set_equal()

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

Definition at line 36 of file bv_utils.cpp.

shift() [1/2]

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

Definition at line 517 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 538 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 1105 of file bv_utils.cpp.

signed_less_than()

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

Definition at line 1606 of file bv_utils.cpp.

signed_multiplier()

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

Definition at line 1004 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 1048 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 1158 of file bv_utils.cpp.

unsigned_less_than()

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

Definition at line 1599 of file bv_utils.cpp.

unsigned_multiplier()

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

Definition at line 920 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 965 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 1669 of file bv_utils.cpp.

verilog_bv_normal_bits()

bvt bv_utilst::verilog_bv_normal_bits ( const bvt &  src )

static

Definition at line 1684 of file bv_utils.cpp.

wallace_tree()

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

protected

Definition at line 646 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 228 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