#include <BVDirectEncoder.h>

Collaboration diagram for smtrat::BVDirectEncoder:

[legend]

Public Member Functions
const FormulaSetT &	encode (const FormulaT &_inputFormula)

const std::set< carl::Variable > &	introducedVariables () const

const carl::FastMap< BitVec, Variables >	bitvectorBlastings () const

	BVDirectEncoder ()

	~BVDirectEncoder ()

Private Types
typedef carl::Variable	Variable

typedef std::vector< Variable >	Variables

typedef FormulaT	Bit

typedef std::vector< Bit >	Bits

typedef carl::BVTerm	BitVecTerm

typedef carl::BVConstraint	BitVecConstr

typedef carl::BVVariable	BitVec

typedef FormulaT	Formula

Private Member Functions
const Bit	const0 ()

const Bit	const1 ()

void	boolAssert (const Formula &_formula)

Bits	encodeConstant (const carl::BVValue &_value)

Bits	encodeVariable (const BitVec &_variable)

Bits	encodeIte (const Bit &_condition, const Bits &_then, const Bits &_else)

Bits	encodeConcat (const Bits &_first, const Bits &_second)

Bits	encodeExtract (const Bits &_operand, std::size_t _highest, std::size_t _lowest)

Bits	encodeNot (const Bits &_operand)

Bits	encodeNeg (const Bits &_operand)

Bits	encodeAnd (const Bits &_first, const Bits &_second)

Bits	encodeOr (const Bits &_first, const Bits &_second)

Bits	encodeXor (const Bits &_first, const Bits &_second)

Bits	encodeNand (const Bits &_first, const Bits &_second)

Bits	encodeNor (const Bits &_first, const Bits &_second)

Bits	encodeXnor (const Bits &_first, const Bits &_second)

Bits	encodeAdd (const Bits &_first, const Bits &_second)

Bits	encodeSub (const Bits &_first, const Bits &_second)

Bits	encodeAdderNetwork (const Bits &_first, const Bits &_second, bool _carryInValue=false, bool _withCarryOut=false, bool _allowOverflow=true)

Bits	encodeMul (const Bits &_first, const Bits &_second)

Bits	encodeMultiplicationNetwork (const Bits &_first, const Bits &_second, bool _allowOverflow=true)

Bits	encodeDivU (const Bits &_first, const Bits &_second)

Bits	encodeDivisionNetwork (const Bits &_first, const Bits &_second, bool _returnRemainder=false)

Bits	encodeDivS (const Bits &_first, const Bits &_second)

Bits	encodeModU (const Bits &_first, const Bits &_second)

Bits	encodeModS1 (const Bits &_first, const Bits &_second)

Bits	encodeModS2 (const Bits &_first, const Bits &_second)

Bits	encodeComp (const Bits &_first, const Bits &_second)

Bits	encodeLshift (const Bits &_first, const Bits &_second)

Bits	encodeShiftNetwork (const Bits &_first, const Bits &_second, bool _left, bool _arithmetic=false)

Bits	encodeRshiftLogic (const Bits &_first, const Bits &_second)

Bits	encodeRshiftArith (const Bits &_first, const Bits &_second)

Bits	encodeLrotate (const Bits &_operand, std::size_t _index)

Bits	encodeRrotate (const Bits &_operand, std::size_t _index)

Bits	encodeExtU (const Bits &_operand, std::size_t _index)

Bits	encodeExtS (const Bits &_operand, std::size_t _index)

Bits	encodeRepeat (const Bits &_operand, std::size_t _index)

Bits	encodeTerm (const BitVecTerm &_term)

Bit	encodeConstraint (const BitVecConstr &_constraint)

Bit	encodeEq (const Bits &_lhs, const Bits &_rhs)

Bit	encodeNeq (const Bits &_lhs, const Bits &_rhs)

Bit	encodeUlt (const Bits &_lhs, const Bits &_rhs)

Bit	encodeUle (const Bits &_lhs, const Bits &_rhs)

Bit	encodeUgt (const Bits &_lhs, const Bits &_rhs)

Bit	encodeUge (const Bits &_lhs, const Bits &_rhs)

Bit	encodeSlt (const Bits &_lhs, const Bits &_rhs)

Bit	encodeSle (const Bits &_lhs, const Bits &_rhs)

Bit	encodeSgt (const Bits &_lhs, const Bits &_rhs)

Bit	encodeSge (const Bits &_lhs, const Bits &_rhs)

Bit	createBit (const FormulaT &_formula)

Bits	createBits (std::size_t _n)

Variable	createVariable ()

Variables	createVariables (std::size_t _n)

Bits	createBits (const Bits &_original)

Bits	createBits (const Variables &_variables)

Bit	boolNot (const Bit &_operand)

Bit	boolImplies (const Bit &_first, const Bit &_second)

Bit	boolAnd (const Bit &_first, const Bit &_second)

Bit	boolAnd (const Bits &_operands)

Bit	boolOr (const Bit &_first, const Bit &_second)

Bit	boolOr (const Bits &_operands)

Bit	boolXor (const Bit &_first, const Bit &_second)

Bit	boolIff (const Bit &_first, const Bit &_second)

Bit	boolIte (const Bit &_condition, const Bit &_then, const Bit &_else)

FormulaT	encodeBVConstraints (const FormulaT _original)

Private Attributes
std::set< Variable >	mIntroducedVariables

carl::FastMap< BitVec, Variables >	mBitVecBits

carl::FastMap< BitVecTerm, Bits >	mTermBits

carl::FastMap< BitVecConstr, Bit >	mConstraintBits

carl::FastMap< BitVecTerm, FormulaSetT >	mTermEncodings

carl::FastMap< BitVecConstr, FormulaSetT >	mConstraintEncodings

FormulaSetT	mCurrentEncodings

std::optional< BitVecConstr >	mCurrentConstraint

std::optional< BitVecTerm >	mCurrentTerm

Detailed Description

Definition at line 40 of file BVDirectEncoder.h.

Member Typedef Documentation

◆ Bit

typedef FormulaT smtrat::BVDirectEncoder::Bit

private

Definition at line 44 of file BVDirectEncoder.h.

◆ Bits

typedef std::vector<Bit> smtrat::BVDirectEncoder::Bits

private

Definition at line 45 of file BVDirectEncoder.h.

◆ BitVec

typedef carl::BVVariable smtrat::BVDirectEncoder::BitVec

private

Definition at line 48 of file BVDirectEncoder.h.

◆ BitVecConstr

typedef carl::BVConstraint smtrat::BVDirectEncoder::BitVecConstr

private

Definition at line 47 of file BVDirectEncoder.h.

◆ BitVecTerm

typedef carl::BVTerm smtrat::BVDirectEncoder::BitVecTerm

private

Definition at line 46 of file BVDirectEncoder.h.

◆ Formula

typedef FormulaT smtrat::BVDirectEncoder::Formula

private

Definition at line 49 of file BVDirectEncoder.h.

◆ Variable

typedef carl::Variable smtrat::BVDirectEncoder::Variable

private

Definition at line 42 of file BVDirectEncoder.h.

◆ Variables

typedef std::vector<Variable> smtrat::BVDirectEncoder::Variables

private

Definition at line 43 of file BVDirectEncoder.h.

Constructor & Destructor Documentation

◆ BVDirectEncoder()

smtrat::BVDirectEncoder::BVDirectEncoder ( )

inline

Definition at line 996 of file BVDirectEncoder.h.

◆ ~BVDirectEncoder()

smtrat::BVDirectEncoder::~BVDirectEncoder ( )

inline

Definition at line 1003 of file BVDirectEncoder.h.

Member Function Documentation

◆ bitvectorBlastings()

const carl::FastMap<BitVec, Variables> smtrat::BVDirectEncoder::bitvectorBlastings ( ) const

inline

Definition at line 991 of file BVDirectEncoder.h.

◆ boolAnd() [1/2]

Bit smtrat::BVDirectEncoder::boolAnd	(	const Bit &	_first,
		const Bit &	_second
	)

inlineprivate

Definition at line 932 of file BVDirectEncoder.h.

Here is the caller graph for this function:

◆ boolAnd() [2/2]

Bit smtrat::BVDirectEncoder::boolAnd ( const Bits & _operands )

inlineprivate

Definition at line 936 of file BVDirectEncoder.h.

◆ boolAssert()

void smtrat::BVDirectEncoder::boolAssert ( const Formula & _formula )

inlineprivate

Definition at line 97 of file BVDirectEncoder.h.

Here is the caller graph for this function:

◆ boolIff()

Bit smtrat::BVDirectEncoder::boolIff	(	const Bit &	_first,
		const Bit &	_second
	)

inlineprivate

Definition at line 952 of file BVDirectEncoder.h.

Here is the caller graph for this function:

◆ boolImplies()

Bit smtrat::BVDirectEncoder::boolImplies	(	const Bit &	_first,
		const Bit &	_second
	)

inlineprivate

Definition at line 928 of file BVDirectEncoder.h.

Here is the caller graph for this function:

◆ boolIte()

Bit smtrat::BVDirectEncoder::boolIte	(	const Bit &	_condition,
		const Bit &	_then,
		const Bit &	_else
	)

inlineprivate

Definition at line 956 of file BVDirectEncoder.h.

Here is the caller graph for this function:

◆ boolNot()

Bit smtrat::BVDirectEncoder::boolNot ( const Bit & _operand )

inlineprivate

Definition at line 924 of file BVDirectEncoder.h.

Here is the caller graph for this function:

◆ boolOr() [1/2]

Bit smtrat::BVDirectEncoder::boolOr	(	const Bit &	_first,
		const Bit &	_second
	)

inlineprivate

Definition at line 940 of file BVDirectEncoder.h.

Here is the caller graph for this function:

◆ boolOr() [2/2]

Bit smtrat::BVDirectEncoder::boolOr ( const Bits & _operands )

inlineprivate

Definition at line 944 of file BVDirectEncoder.h.

◆ boolXor()

Bit smtrat::BVDirectEncoder::boolXor	(	const Bit &	_first,
		const Bit &	_second
	)

inlineprivate

Definition at line 948 of file BVDirectEncoder.h.

Here is the caller graph for this function:

◆ const0()

const Bit smtrat::BVDirectEncoder::const0 ( )

inlineprivate

Definition at line 83 of file BVDirectEncoder.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ const1()

const Bit smtrat::BVDirectEncoder::const1 ( )

inlineprivate

Definition at line 90 of file BVDirectEncoder.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ createBit()

Bit smtrat::BVDirectEncoder::createBit ( const FormulaT & _formula )

inlineprivate

Definition at line 872 of file BVDirectEncoder.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ createBits() [1/3]

Bits smtrat::BVDirectEncoder::createBits ( const Bits & _original )

inlineprivate

Definition at line 905 of file BVDirectEncoder.h.

Here is the call graph for this function:

◆ createBits() [2/3]

Bits smtrat::BVDirectEncoder::createBits ( const Variables & _variables )

inlineprivate

Definition at line 916 of file BVDirectEncoder.h.

Here is the call graph for this function:

◆ createBits() [3/3]

Bits smtrat::BVDirectEncoder::createBits ( std::size_t _n )

inlineprivate

Definition at line 883 of file BVDirectEncoder.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ createVariable()

Variable smtrat::BVDirectEncoder::createVariable ( )

inlineprivate

Definition at line 888 of file BVDirectEncoder.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ createVariables()

Variables smtrat::BVDirectEncoder::createVariables ( std::size_t _n )

inlineprivate

Definition at line 897 of file BVDirectEncoder.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ encode()

const FormulaSetT& smtrat::BVDirectEncoder::encode ( const FormulaT & _inputFormula )

inline

Definition at line 972 of file BVDirectEncoder.h.

Here is the call graph for this function:

◆ encodeAdd()

Bits smtrat::BVDirectEncoder::encodeAdd	(	const Bits &	_first,
		const Bits &	_second
	)

inlineprivate

Definition at line 251 of file BVDirectEncoder.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ encodeAdderNetwork()

Bits smtrat::BVDirectEncoder::encodeAdderNetwork	(	const Bits &	_first,
		const Bits &	_second,
		bool	_carryInValue = `false`,
		bool	_withCarryOut = `false`,
		bool	_allowOverflow = `true`
	)

inlineprivate

Definition at line 261 of file BVDirectEncoder.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ encodeAnd()

Bits smtrat::BVDirectEncoder::encodeAnd	(	const Bits &	_first,
		const Bits &	_second
	)

inlineprivate

Definition at line 197 of file BVDirectEncoder.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ encodeBVConstraints()

FormulaT smtrat::BVDirectEncoder::encodeBVConstraints ( const FormulaT _original )

inlineprivate

Definition at line 960 of file BVDirectEncoder.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ encodeComp()

Bits smtrat::BVDirectEncoder::encodeComp	(	const Bits &	_first,
		const Bits &	_second
	)

inlineprivate

Definition at line 469 of file BVDirectEncoder.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ encodeConcat()

Bits smtrat::BVDirectEncoder::encodeConcat	(	const Bits &	_first,
		const Bits &	_second
	)

inlineprivate

Definition at line 153 of file BVDirectEncoder.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ encodeConstant()

Bits smtrat::BVDirectEncoder::encodeConstant ( const carl::BVValue & _value )

inlineprivate

Definition at line 115 of file BVDirectEncoder.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ encodeConstraint()

Bit smtrat::BVDirectEncoder::encodeConstraint ( const BitVecConstr & _constraint )

inlineprivate

Definition at line 713 of file BVDirectEncoder.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ encodeDivisionNetwork()

Bits smtrat::BVDirectEncoder::encodeDivisionNetwork	(	const Bits &	_first,
		const Bits &	_second,
		bool	_returnRemainder = `false`
	)

inlineprivate

TODO: Create a direct encoding of this instead of an equation to a constant.

Definition at line 339 of file BVDirectEncoder.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ encodeDivS()

Bits smtrat::BVDirectEncoder::encodeDivS	(	const Bits &	_first,
		const Bits &	_second
	)

inlineprivate

Definition at line 374 of file BVDirectEncoder.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ encodeDivU()

Bits smtrat::BVDirectEncoder::encodeDivU	(	const Bits &	_first,
		const Bits &	_second
	)

inlineprivate

Definition at line 334 of file BVDirectEncoder.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ encodeEq()

Bit smtrat::BVDirectEncoder::encodeEq	(	const Bits &	_lhs,
		const Bits &	_rhs
	)

inlineprivate

Definition at line 783 of file BVDirectEncoder.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ encodeExtract()

Bits smtrat::BVDirectEncoder::encodeExtract	(	const Bits &	_operand,
		std::size_t	_highest,
		std::size_t	_lowest
	)

inlineprivate

Definition at line 160 of file BVDirectEncoder.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ encodeExtS()

Bits smtrat::BVDirectEncoder::encodeExtS	(	const Bits &	_operand,
		std::size_t	_index
	)

inlineprivate

Definition at line 580 of file BVDirectEncoder.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ encodeExtU()

Bits smtrat::BVDirectEncoder::encodeExtU	(	const Bits &	_operand,
		std::size_t	_index
	)

inlineprivate

Definition at line 571 of file BVDirectEncoder.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ encodeIte()

Bits smtrat::BVDirectEncoder::encodeIte	(	const Bit &	_condition,
		const Bits &	_then,
		const Bits &	_else
	)

inlineprivate

Definition at line 143 of file BVDirectEncoder.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ encodeLrotate()

Bits smtrat::BVDirectEncoder::encodeLrotate	(	const Bits &	_operand,
		std::size_t	_index
	)

inlineprivate

Definition at line 549 of file BVDirectEncoder.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ encodeLshift()

Bits smtrat::BVDirectEncoder::encodeLshift	(	const Bits &	_first,
		const Bits &	_second
	)

inlineprivate

Definition at line 476 of file BVDirectEncoder.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ encodeModS1()

Bits smtrat::BVDirectEncoder::encodeModS1	(	const Bits &	_first,
		const Bits &	_second
	)

inlineprivate

Definition at line 405 of file BVDirectEncoder.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ encodeModS2()

Bits smtrat::BVDirectEncoder::encodeModS2	(	const Bits &	_first,
		const Bits &	_second
	)

inlineprivate

Definition at line 431 of file BVDirectEncoder.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ encodeModU()

Bits smtrat::BVDirectEncoder::encodeModU	(	const Bits &	_first,
		const Bits &	_second
	)

inlineprivate

Definition at line 400 of file BVDirectEncoder.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ encodeMul()

Bits smtrat::BVDirectEncoder::encodeMul	(	const Bits &	_first,
		const Bits &	_second
	)

inlineprivate

Definition at line 297 of file BVDirectEncoder.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ encodeMultiplicationNetwork()

Bits smtrat::BVDirectEncoder::encodeMultiplicationNetwork	(	const Bits &	_first,
		const Bits &	_second,
		bool	_allowOverflow = `true`
	)

inlineprivate

Definition at line 302 of file BVDirectEncoder.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ encodeNand()

Bits smtrat::BVDirectEncoder::encodeNand	(	const Bits &	_first,
		const Bits &	_second
	)

inlineprivate

Definition at line 224 of file BVDirectEncoder.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ encodeNeg()

Bits smtrat::BVDirectEncoder::encodeNeg ( const Bits & _operand )

inlineprivate

Definition at line 174 of file BVDirectEncoder.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ encodeNeq()

Bit smtrat::BVDirectEncoder::encodeNeq	(	const Bits &	_lhs,
		const Bits &	_rhs
	)

inlineprivate

Definition at line 795 of file BVDirectEncoder.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ encodeNor()

Bits smtrat::BVDirectEncoder::encodeNor	(	const Bits &	_first,
		const Bits &	_second
	)

inlineprivate

Definition at line 233 of file BVDirectEncoder.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ encodeNot()

Bits smtrat::BVDirectEncoder::encodeNot ( const Bits & _operand )

inlineprivate

Definition at line 165 of file BVDirectEncoder.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ encodeOr()

Bits smtrat::BVDirectEncoder::encodeOr	(	const Bits &	_first,
		const Bits &	_second
	)

inlineprivate

Definition at line 206 of file BVDirectEncoder.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ encodeRepeat()

Bits smtrat::BVDirectEncoder::encodeRepeat	(	const Bits &	_operand,
		std::size_t	_index
	)

inlineprivate

Definition at line 589 of file BVDirectEncoder.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ encodeRrotate()

Bits smtrat::BVDirectEncoder::encodeRrotate	(	const Bits &	_operand,
		std::size_t	_index
	)

inlineprivate

Definition at line 561 of file BVDirectEncoder.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ encodeRshiftArith()

Bits smtrat::BVDirectEncoder::encodeRshiftArith	(	const Bits &	_first,
		const Bits &	_second
	)

inlineprivate

Definition at line 544 of file BVDirectEncoder.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ encodeRshiftLogic()

Bits smtrat::BVDirectEncoder::encodeRshiftLogic	(	const Bits &	_first,
		const Bits &	_second
	)

inlineprivate

Definition at line 539 of file BVDirectEncoder.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ encodeSge()

Bit smtrat::BVDirectEncoder::encodeSge	(	const Bits &	_lhs,
		const Bits &	_rhs
	)

inlineprivate

Definition at line 867 of file BVDirectEncoder.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ encodeSgt()

Bit smtrat::BVDirectEncoder::encodeSgt	(	const Bits &	_lhs,
		const Bits &	_rhs
	)

inlineprivate

Definition at line 862 of file BVDirectEncoder.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ encodeShiftNetwork()

Bits smtrat::BVDirectEncoder::encodeShiftNetwork	(	const Bits &	_first,
		const Bits &	_second,
		bool	_left,
		bool	_arithmetic = `false`
	)

inlineprivate

Definition at line 481 of file BVDirectEncoder.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ encodeSle()

Bit smtrat::BVDirectEncoder::encodeSle	(	const Bits &	_lhs,
		const Bits &	_rhs
	)

inlineprivate

Definition at line 843 of file BVDirectEncoder.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ encodeSlt()

Bit smtrat::BVDirectEncoder::encodeSlt	(	const Bits &	_lhs,
		const Bits &	_rhs
	)

inlineprivate

Definition at line 824 of file BVDirectEncoder.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ encodeSub()

Bits smtrat::BVDirectEncoder::encodeSub	(	const Bits &	_first,
		const Bits &	_second
	)

inlineprivate

Definition at line 256 of file BVDirectEncoder.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ encodeTerm()

Bits smtrat::BVDirectEncoder::encodeTerm ( const BitVecTerm & _term )

inlineprivate

Definition at line 599 of file BVDirectEncoder.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ encodeUge()

Bit smtrat::BVDirectEncoder::encodeUge	(	const Bits &	_lhs,
		const Bits &	_rhs
	)

inlineprivate

Definition at line 818 of file BVDirectEncoder.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ encodeUgt()

Bit smtrat::BVDirectEncoder::encodeUgt	(	const Bits &	_lhs,
		const Bits &	_rhs
	)

inlineprivate

Definition at line 813 of file BVDirectEncoder.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ encodeUle()

Bit smtrat::BVDirectEncoder::encodeUle	(	const Bits &	_lhs,
		const Bits &	_rhs
	)

inlineprivate

Definition at line 805 of file BVDirectEncoder.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ encodeUlt()

Bit smtrat::BVDirectEncoder::encodeUlt	(	const Bits &	_lhs,
		const Bits &	_rhs
	)

inlineprivate

Definition at line 800 of file BVDirectEncoder.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ encodeVariable()

Bits smtrat::BVDirectEncoder::encodeVariable ( const BitVec & _variable )

inlineprivate

Definition at line 125 of file BVDirectEncoder.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ encodeXnor()

Bits smtrat::BVDirectEncoder::encodeXnor	(	const Bits &	_first,
		const Bits &	_second
	)

inlineprivate

Definition at line 242 of file BVDirectEncoder.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ encodeXor()

Bits smtrat::BVDirectEncoder::encodeXor	(	const Bits &	_first,
		const Bits &	_second
	)

inlineprivate

Definition at line 215 of file BVDirectEncoder.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ introducedVariables()

const std::set<carl::Variable>& smtrat::BVDirectEncoder::introducedVariables ( ) const

inline

Definition at line 986 of file BVDirectEncoder.h.

Field Documentation

◆ mBitVecBits

carl::FastMap<BitVec, Variables> smtrat::BVDirectEncoder::mBitVecBits

private

Definition at line 57 of file BVDirectEncoder.h.

◆ mConstraintBits

carl::FastMap<BitVecConstr, Bit> smtrat::BVDirectEncoder::mConstraintBits

private

Definition at line 61 of file BVDirectEncoder.h.

◆ mConstraintEncodings

carl::FastMap<BitVecConstr, FormulaSetT> smtrat::BVDirectEncoder::mConstraintEncodings

private

Definition at line 69 of file BVDirectEncoder.h.

◆ mCurrentConstraint

std::optional<BitVecConstr> smtrat::BVDirectEncoder::mCurrentConstraint

private

Definition at line 75 of file BVDirectEncoder.h.

◆ mCurrentEncodings

FormulaSetT smtrat::BVDirectEncoder::mCurrentEncodings

private

Definition at line 72 of file BVDirectEncoder.h.

◆ mCurrentTerm

std::optional<BitVecTerm> smtrat::BVDirectEncoder::mCurrentTerm

private

Definition at line 76 of file BVDirectEncoder.h.

◆ mIntroducedVariables

std::set<Variable> smtrat::BVDirectEncoder::mIntroducedVariables

private

Definition at line 53 of file BVDirectEncoder.h.

◆ mTermBits

carl::FastMap<BitVecTerm, Bits> smtrat::BVDirectEncoder::mTermBits

private

Definition at line 59 of file BVDirectEncoder.h.

◆ mTermEncodings

carl::FastMap<BitVecTerm, FormulaSetT> smtrat::BVDirectEncoder::mTermEncodings

private

Definition at line 67 of file BVDirectEncoder.h.

The documentation for this class was generated from the following file:

smtrat-modules/BVModule/BVDirectEncoder.h

Public Member Functions

Private Types

Private Member Functions

Private Attributes

Detailed Description

Member Typedef Documentation

◆ Bit

◆ Bits

◆ BitVec

◆ BitVecConstr

◆ BitVecTerm

◆ Formula

◆ Variable

◆ Variables

Constructor & Destructor Documentation

◆ BVDirectEncoder()

◆ ~BVDirectEncoder()

Member Function Documentation

◆ bitvectorBlastings()

◆ boolAnd() [1/2]

◆ boolAnd() [2/2]

◆ boolAssert()

◆ boolIff()

◆ boolImplies()

◆ boolIte()

◆ boolNot()

◆ boolOr() [1/2]

◆ boolOr() [2/2]

◆ boolXor()

◆ const0()

◆ const1()

◆ createBit()

◆ createBits() [1/3]

◆ createBits() [2/3]

◆ createBits() [3/3]

◆ createVariable()

◆ createVariables()

◆ encode()

◆ encodeAdd()

◆ encodeAdderNetwork()

◆ encodeAnd()

◆ encodeBVConstraints()

◆ encodeComp()

◆ encodeConcat()

◆ encodeConstant()

◆ encodeConstraint()

◆ encodeDivisionNetwork()

◆ encodeDivS()

◆ encodeDivU()

◆ encodeEq()

◆ encodeExtract()

◆ encodeExtS()

◆ encodeExtU()

◆ encodeIte()

◆ encodeLrotate()

◆ encodeLshift()

◆ encodeModS1()

◆ encodeModS2()

◆ encodeModU()

◆ encodeMul()

◆ encodeMultiplicationNetwork()

◆ encodeNand()

◆ encodeNeg()

◆ encodeNeq()

◆ encodeNor()

◆ encodeNot()

◆ encodeOr()

◆ encodeRepeat()

◆ encodeRrotate()

◆ encodeRshiftArith()

◆ encodeRshiftLogic()

◆ encodeSge()

◆ encodeSgt()

◆ encodeShiftNetwork()

◆ encodeSle()

◆ encodeSlt()

◆ encodeSub()

◆ encodeTerm()

◆ encodeUge()

◆ encodeUgt()