smtrat::PseudoBoolNormalizer Class Reference

#include <PseudoBoolNormalizer.h>

Collaboration diagram for smtrat::PseudoBoolNormalizer:

Public Member Functions
std::pair< std::optional< FormulaT >, ConstraintT >	normalize (const ConstraintT &constraint)
	Modifies the constraint in-place and returns an additional boolean formula. More...
std::map< carl::Variable, carl::Variable > &	substitutedVariables ()
	returns all variable substitutions done by this normalizer instance. More...
ConstraintT	trim (const ConstraintT &constraint)

Private Member Functions
std::pair< std::optional< FormulaT >, ConstraintT >	removePositiveCoeff (const ConstraintT &constraint)
ConstraintT	gcd (const ConstraintT &constraint)
ConstraintT	normalizeLessConstraint (const ConstraintT &constraint)
bool	trimmable (const ConstraintT &constraint)

Private Attributes
std::map< carl::Variable, carl::Variable >	mVariablesCache

Detailed Description

Definition at line 7 of file PseudoBoolNormalizer.h.

Member Function Documentation

gcd()

ConstraintT smtrat::PseudoBoolNormalizer::gcd ( const ConstraintT &  constraint )

private

Definition at line 106 of file PseudoBoolNormalizer.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

normalize()

std::pair< std::optional< FormulaT >, ConstraintT > smtrat::PseudoBoolNormalizer::normalize

(

const ConstraintT &

constraint

)

Modifies the constraint in-place and returns an additional boolean formula.

Consider -4x <= 2

This is equivalent to -4*(1 - not x) <= 2 iff. -4 + 4 not x <= 2 iff 4 not x <= 6 Since we can not represent this negation in the constraint itself we add a variable y and get y <-> not x and 4 y <= 6

In this particular case we can later on remove y again since the constraint is trivially satisfied.

Definition at line 7 of file PseudoBoolNormalizer.cpp.

Here is the call graph for this function:

normalizeLessConstraint()

ConstraintT smtrat::PseudoBoolNormalizer::normalizeLessConstraint ( const ConstraintT &  constraint )

private

Definition at line 131 of file PseudoBoolNormalizer.cpp.

Here is the caller graph for this function:

removePositiveCoeff()

std::pair< std::optional< FormulaT >, ConstraintT > smtrat::PseudoBoolNormalizer::removePositiveCoeff ( const ConstraintT &  constraint )

private

Definition at line 73 of file PseudoBoolNormalizer.cpp.

Here is the caller graph for this function:

substitutedVariables()

std::map<carl::Variable, carl::Variable>& smtrat::PseudoBoolNormalizer::substitutedVariables ( )

inline

returns all variable substitutions done by this normalizer instance.

An entry {x: y} correlates to the boolean expression y <-> not x

Useful if all occurences of the substituted variable should be substituted as well or in general when the correlation is needed.

Definition at line 30 of file PseudoBoolNormalizer.h.

trim()

ConstraintT smtrat::PseudoBoolNormalizer::trim

(

const ConstraintT &

constraint

)

Definition at line 53 of file PseudoBoolNormalizer.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

trimmable()

bool smtrat::PseudoBoolNormalizer::trimmable ( const ConstraintT &  constraint )

private

Definition at line 41 of file PseudoBoolNormalizer.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

Field Documentation

mVariablesCache

std::map<carl::Variable, carl::Variable> smtrat::PseudoBoolNormalizer::mVariablesCache

private

Definition at line 36 of file PseudoBoolNormalizer.h.

---

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

• smtrat-modules/PBPPModule/Encoders/PseudoBoolNormalizer.h
• smtrat-modules/PBPPModule/Encoders/PseudoBoolNormalizer.cpp