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

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

nodiscardprotected

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 )

nodiscardprotected

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 )

nodiscardprotected

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:

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

◆ 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