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	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
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
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 833 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 335 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 350 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 324 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 293 of file bv_utils.cpp.

adder_no_overflow() [1/2]

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

protected

Definition at line 517 of file bv_utils.cpp.

adder_no_overflow() [2/2]

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

protected

Definition at line 482 of file bv_utils.cpp.

build_constant()

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

static

Definition at line 11 of file bv_utils.cpp.

carry()

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

Definition at line 227 of file bv_utils.cpp.

carry_out()

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

Definition at line 309 of file bv_utils.cpp.

concatenate()

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

static

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

cond_negate()

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

Definition at line 820 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 839 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 933 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 1165 of file bv_utils.cpp.

extension()

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

static

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

extract_lsb()

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

static

Definition at line 66 of file bv_utils.cpp.

extract_msb()

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

static

Definition at line 54 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 136 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 624 of file bv_utils.cpp.

incrementer() [2/2]

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

Definition at line 639 of file bv_utils.cpp.

inverted()

bvt bv_utilst::inverted ( const bvt &  op )

static

Definition at line 647 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 1359 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 22 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 1200 of file bv_utils.cpp.

multiplier()

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

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

negate()

bvt bv_utilst::negate

(

const bvt &

op

)

Definition at line 599 of file bv_utils.cpp.

negate_no_overflow()

bvt bv_utilst::negate_no_overflow

(

const bvt &

op

)

Definition at line 607 of file bv_utils.cpp.

overflow_add()

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

Definition at line 433 of file bv_utils.cpp.

overflow_negate()

literalt bv_utilst::overflow_negate

(

const bvt &

op

)

Definition at line 613 of file bv_utils.cpp.

overflow_sub()

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

Definition at line 457 of file bv_utils.cpp.

rel()

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

Definition at line 1337 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 363 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 92 of file bv_utils.cpp.

set_equal()

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

Definition at line 31 of file bv_utils.cpp.

shift() [1/2]

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

Definition at line 526 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 547 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 898 of file bv_utils.cpp.

signed_less_than()

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

Definition at line 1330 of file bv_utils.cpp.

signed_multiplier()

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

Definition at line 802 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 846 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 951 of file bv_utils.cpp.

unsigned_less_than()

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

Definition at line 1318 of file bv_utils.cpp.

unsigned_multiplier()

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

Definition at line 701 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 763 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 1393 of file bv_utils.cpp.

verilog_bv_normal_bits()

bvt bv_utilst::verilog_bv_normal_bits ( const bvt &  src )

static

Definition at line 1408 of file bv_utils.cpp.

wallace_tree()

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

protected

Definition at line 655 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-documentation/cbmc-documentation/src/solvers/flattening/bv_utils.h
• /home/runner/work/cbmc-documentation/cbmc-documentation/src/solvers/flattening/bv_utils.cpp