AxiomFactory.cpp File Reference

#include "AxiomFactory.h"
#include "../LOG.h"

Include dependency graph for AxiomFactory.cpp:

Go to the source code of this file.

Namespaces
	smtrat
	Class to create the formulas for axioms.

Functions
FormulaT	smtrat::createZeroOne (carl::Variable xVariable, carl::Variable yVariable, carl::Variable zVariable)
FormulaT	smtrat::createZeroTwo (carl::Variable xVariable, carl::Variable yVariable, carl::Variable zVariable)
FormulaT	smtrat::createZeroThree (carl::Variable xVariable, carl::Variable yVariable, carl::Variable zVariable)
FormulasT	smtrat::createZero (smtrat::VariableCapsule variableCapsule)
FormulaT	smtrat::createTangentPlaneNEQOne (carl::Variable xVariable, carl::Variable yVariable, carl::Variable zVariable, Rational aRational)
FormulaT	smtrat::createTangentPlaneNEQTwo (carl::Variable xVariable, carl::Variable yVariable, carl::Variable zVariable, Rational bRational)
FormulaT	smtrat::createTangentPlaneNEQThree (carl::Variable xVariable, carl::Variable yVariable, carl::Variable zVariable, Rational aRational, Rational bRational)
FormulaT	smtrat::createTangentPlaneNEQFour (carl::Variable xVariable, carl::Variable yVariable, carl::Variable zVariable, Rational aRational, Rational bRational)
FormulasT	smtrat::createTangentPlaneNEQ (VariableCapsule variableCapsule, RationalCapsule rationalCapsule)
FormulaT	smtrat::createTangentPlaneEQOne (carl::Variable xVariable, carl::Variable yVariable, carl::Variable zVariable, Rational aRational)
FormulaT	smtrat::createTangentPlaneEQTwo (carl::Variable xVariable, carl::Variable yVariable, carl::Variable zVariable, Rational aRational)
FormulasT	smtrat::createTangentPlaneEQ (VariableCapsule variableCapsule, RationalCapsule rationalCapsule)
const smtrat::VariableCapsule	smtrat::extractVariables (MonomialMapIterator monomialIterator)
Model	smtrat::createAbsoluteValuedModel (Model linearizedModel)
carl::Variable	smtrat::createAuxiliaryVariable (carl::Variable variable)
	create an auxiliary variable e.g. More...
FormulaT	smtrat::generateAbsFormula (carl::Variable variable, carl::Variable aux_variable)
	| x1 | = (and (=> (x1 >= 0) (y1 = x1)) (=> (x1 < 0) (y1 = -x1)) ) More...
FormulaT	smtrat::generateAbsFormula (carl::Variable variableLeft, carl::Variable variableRight, carl::Relation relation)
	| x1 | <= | x1 | = (and (=> (x1 >= 0) (y1 = x1)) (=> (x1 < 0) (y1 = -x1)) (=> (x2 >= 0) (y2 = x2)) (=> (x2 < 0) (y2 = -x2)) (y1 <= y2) ) More...
FormulaT	smtrat::createEquivalentToOriginalMonotonicityOne (smtrat::VariableCapsule variableCapsule, smtrat::VariableCapsule variableCapsuleInner)
FormulaT	smtrat::createEquivalentToOriginalMonotonicityTwo (smtrat::VariableCapsule variableCapsule, smtrat::VariableCapsule variableCapsuleInner)
FormulaT	smtrat::createEquivalentToOriginalMonotonicityThree (smtrat::VariableCapsule variableCapsule, smtrat::VariableCapsule variableCapsuleInner)
RationalCapsule	smtrat::extractRationalCapsule (VariableCapsule variableCapsule, Model linearizedModel)
FormulaT	smtrat::createOriginalMonotonicityOne (smtrat::VariableCapsule variableCapsule, smtrat::VariableCapsule variableCapsuleInner)
FormulaT	smtrat::createOriginalMonotonicityTwo (smtrat::VariableCapsule variableCapsule, smtrat::VariableCapsule variableCapsuleInner)
FormulaT	smtrat::createOriginalMonotonicityThree (smtrat::VariableCapsule variableCapsule, smtrat::VariableCapsule variableCapsuleInner)
FormulasT	smtrat::createMonotonicity (VariableCapsule variableCapsuleOuter, VariableCapsule variableCapsuleInner, Model absoluteValuedModel)
FormulaT	smtrat::createCongruence (smtrat::VariableCapsule variableCapsuleOuter, smtrat::VariableCapsule variableCapsuleInner)
FormulaT	smtrat::createICPGreaterOne (VariableCapsule variableCapsule, RationalCapsule rationalCapsule)
FormulaT	smtrat::createICPGreaterTwo (VariableCapsule variableCapsule, RationalCapsule rationalCapsule)
FormulasT	smtrat::createICPGreater (VariableCapsule variableCapsule, RationalCapsule rationalCapsule)
FormulaT	smtrat::createICPLess (VariableCapsule variableCapsule, RationalCapsule rationalCapsule)
bool	smtrat::abEqualcCheck (VariableCapsule variableCapsuleOuter, Model linearizedModel)
bool	smtrat::abGreatercCheck (RationalCapsule rationalCapsule)
bool	smtrat::abLesscCheck (RationalCapsule rationalCapsule)
RationalCapsule	smtrat::generateAbcPrimeForICP (RationalCapsule rationalCapsule, bool isGreater)
bool	smtrat::isAnyRationalIsZero (RationalCapsule rationalCapsule)