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

nodiscardprotected

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 )

nodiscardprotected

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 )

nodiscardprotected

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

literalt bv_utilst::sign_bit ( const bvt & op )

inlinestatic

Definition at line 138 of file bv_utils.h.

◆ sign_extension()

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

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

inlinestatic

Definition at line 187 of file bv_utils.h.

◆ zeros()

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:

solvers/flattening/bv_utils.h
solvers/flattening/bv_utils.cpp

Public Types

Public Member Functions

Static Public Member Functions

Protected Member Functions

Protected Attributes

Detailed Description

Member Enumeration Documentation

◆ representationt

◆ shiftt

Constructor & Destructor Documentation

◆ bv_utilst()

Member Function Documentation

◆ absolute_value()

◆ add()

◆ add_sub() [1/2]

◆ add_sub() [2/2]

◆ add_sub_no_overflow()

◆ adder()

◆ adder_no_overflow() [1/2]

◆ adder_no_overflow() [2/2]

◆ build_constant()

◆ carry()

◆ carry_out()

◆ concatenate()

◆ cond_implies_equal()

◆ cond_negate()

◆ cond_negate_no_overflow()

◆ dadda_tree()

◆ divider() [1/2]

◆ divider() [2/2]

◆ equal()

◆ extension()

◆ extract()

◆ extract_lsb()

◆ extract_msb()

◆ full_adder()

◆ inc()

◆ incrementer() [1/2]

◆ incrementer() [2/2]

◆ inverted()

◆ is_all_ones()

◆ is_constant()

◆ is_int_min()

◆ is_not_zero()

◆ is_one()

◆ is_zero()

◆ lt_or_le()

◆ multiplier()

◆ multiplier_no_overflow()

◆ negate()

◆ negate_no_overflow()

◆ overflow_add()

◆ overflow_negate()

◆ overflow_sub()

◆ popcount()

◆ rel()

◆ remainder()

◆ saturating_add_sub()

◆ select()

◆ set_equal()

◆ shift() [1/2]

◆ shift() [2/2]

◆ sign_bit()

◆ sign_extension()

◆ signed_divider()

◆ signed_less_than()

◆ signed_multiplier()

◆ signed_multiplier_no_overflow()

◆ sub()

◆ unsigned_divider()

◆ unsigned_less_than()

◆ unsigned_multiplier()

◆ unsigned_multiplier_no_overflow()

◆ verilog_bv_has_x_or_z()

◆ verilog_bv_normal_bits()

◆ wallace_tree()

◆ zero_extension()

◆ zeros()

Member Data Documentation

◆ prop