#include <dag.h>

Public Member Functions
	DAGNode (std::shared_ptr< Sort > sort, NODE_KIND kind, std::string name, std::vector< std::shared_ptr< DAGNode > > children)

	DAGNode (std::shared_ptr< Sort > sort, NODE_KIND kind, std::string name)

	DAGNode (std::shared_ptr< Sort > sort, NODE_KIND kind)

	DAGNode (std::shared_ptr< Sort > sort)

	DAGNode ()

	DAGNode (const DAGNode &other)

	DAGNode (NODE_KIND kind, std::string name)

	DAGNode (NODE_KIND kind)

	DAGNode (std::shared_ptr< Sort > sort, const Integer &v)

	DAGNode (std::shared_ptr< Sort > sort, const Real &v)

	DAGNode (std::shared_ptr< Sort > sort, const double &v)

	DAGNode (std::shared_ptr< Sort > sort, const int &v)

	DAGNode (std::shared_ptr< Sort > sort, const bool &v)

	DAGNode (const std::string &n)

void	clear ()

bool	operator== (const DAGNode elem)

bool	operator!= (const DAGNode elem)

void	replace_children (const std::vector< std::shared_ptr< DAGNode > > &new_children)

void	setName (const std::string &n)

bool	isLeaf () const

bool	isInternal () const

bool	isNull () const

bool	isErr () const

bool	isUnknown () const

bool	isCBool () const

bool	isTrue () const

bool	isFalse () const

bool	isConst () const

bool	isNumeral () const

bool	isCInt () const

bool	isCReal () const

bool	isCBV () const

bool	isCFP () const

bool	isCRoundingMode () const

bool	isCStr () const

bool	isAttribute () const

bool	isAttributeParam () const

bool	isVBool () const

bool	isLiteral () const

bool	isVInt () const

bool	isVReal () const

bool	isVBV () const

bool	isVFP () const

bool	isVRoundingMode () const

bool	isVStr () const

bool	isTempVar () const

bool	isQuantVar () const

bool	isLetBindVar () const

bool	isPlaceholderVar () const

bool	isVReg () const

bool	isVar () const

bool	isVUF () const

bool	isUFName () const

bool	isMax () const

bool	isMin () const

bool	isArray () const

bool	isConstArray () const

bool	isAnd () const

bool	isOr () const

bool	isNot () const

bool	isImplies () const

bool	isXor () const

bool	isEqBool () const

bool	isEqOther () const

bool	isEq () const

bool	isDistinctBool () const

bool	isDistinctOther () const

bool	isDistinct () const

bool	isNeq () const

bool	isUFApplication () const

bool	isAdd () const

bool	isSub () const

bool	isMul () const

bool	isNeg () const

bool	isDivInt () const

bool	isDivReal () const

bool	isMod () const

bool	isAbs () const

bool	isCeil () const

bool	isFloor () const

bool	isRound () const

bool	isArithOp () const

bool	isIAnd () const

bool	isPow2 () const

bool	isPow () const

bool	isSqrt () const

bool	isSafeSqrt () const

bool	isRealNonlinearOp () const

bool	isExp () const

bool	isLog () const

bool	isLn () const

bool	isLb () const

bool	isLg () const

bool	isSin () const

bool	isCos () const

bool	isSec () const

bool	isCsc () const

bool	isTan () const

bool	isCot () const

bool	isAsin () const

bool	isAcos () const

bool	isAsec () const

bool	isAcsc () const

bool	isAtan () const

bool	isAcot () const

bool	isSinh () const

bool	isCosh () const

bool	isTanh () const

bool	isSech () const

bool	isCsch () const

bool	isCoth () const

bool	isAsinh () const

bool	isAcosh () const

bool	isAtanh () const

bool	isAsech () const

bool	isAcsch () const

bool	isAcoth () const

bool	isAtan2 () const

bool	isTranscendentalOp () const

bool	isLe () const

bool	isLt () const

bool	isGe () const

bool	isGt () const

bool	isArithTerm () const

bool	isArithComp () const

bool	isToReal () const

bool	isToInt () const

bool	isArithConv () const

bool	isInt () const

bool	isDivisible () const

bool	isPrime () const

bool	isEven () const

bool	isOdd () const

bool	isArithProp () const

bool	isPi () const

bool	isE () const

bool	isInfinity () const

bool	isPosInfinity () const

bool	isNegInfinity () const

bool	isNaN () const

bool	isEpsilon () const

bool	isPosEpsilon () const

bool	isNegEpsilon () const

bool	isGcd () const

bool	isLcm () const

bool	isFact () const

bool	isBVNot () const

bool	isBVAnd () const

bool	isBVOr () const

bool	isBVXor () const

bool	isBVNand () const

bool	isBVNor () const

bool	isBVXnor () const

bool	isBVComp () const

bool	isBVNeg () const

bool	isBVAdd () const

bool	isBVSub () const

bool	isBVMul () const

bool	isBVUDiv () const

bool	isBVURem () const

bool	isBVSDiv () const

bool	isBVSRem () const

bool	isBVUMod () const

bool	isBVSMod () const

bool	isBVNegO () const

bool	isBVUAddO () const

bool	isBVSAddO () const

bool	isBVUMulO () const

bool	isBVSMulO () const

bool	isBVUDivO () const

bool	isBVSDivO () const

bool	isBVURemO () const

bool	isBVSRemO () const

bool	isBVUModO () const

bool	isBVSModO () const

bool	isBVShl () const

bool	isBVLSHR () const

bool	isBVASHR () const

bool	isBVConcat () const

bool	isBVExtract () const

bool	isBVRepeat () const

bool	isBVZeroExt () const

bool	isBVSignExt () const

bool	isBVRotLeft () const

bool	isBVRotRight () const

bool	isBVOp () const

bool	isBVUlt () const

bool	isBVUle () const

bool	isBVUgt () const

bool	isBVUge () const

bool	isBVSlt () const

bool	isBVSle () const

bool	isBVSgt () const

bool	isBVSge () const

bool	isBVTerm () const

bool	isBVCompOp () const

bool	isBvAtom () const

bool	isBVToNat () const

bool	isNatToBV () const

bool	isBVToInt () const

bool	isUBVToInt () const

bool	isSBVToInt () const

bool	isIntToBV () const

bool	isBVConv () const

bool	isFPAdd () const

bool	isFPSub () const

bool	isFPMul () const

bool	isFPDiv () const

bool	isFPAbs () const

bool	isFPNeg () const

bool	isFPRem () const

bool	isFPFMA () const

bool	isFPSqrt () const

bool	isFPRoundToIntegral () const

bool	isFPRoToInt () const

bool	isFPMin () const

bool	isFPMax () const

bool	isFPOp () const

bool	isFPLe () const

bool	isFPLt () const

bool	isFPGe () const

bool	isFPGt () const

bool	isFPEq () const

bool	isFPComp () const

bool	isFPToUBV () const

bool	isFPToSBV () const

bool	isFPToReal () const

bool	isToFP () const

bool	isToFPUnsigned () const

bool	isFPConv () const

bool	isFPIsNormal () const

bool	isFPIsSubnormal () const

bool	isFPIsZero () const

bool	isFPIsInf () const

bool	isFPIsNaN () const

bool	isFPIsNeg () const

bool	isFPIsPos () const

bool	isFPProp () const

bool	isSelect () const

bool	isStore () const

bool	isArrayOp () const

bool	isStrLen () const

bool	isStrConcat () const

bool	isStrSubstr () const

bool	isStrPrefixof () const

bool	isStrSuffixof () const

bool	isStrIndexof () const

bool	isStrCharat () const

bool	isStrUpdate () const

bool	isStrReplace () const

bool	isStrReplaceAll () const

bool	isStrToLower () const

bool	isStrToUpper () const

bool	isStrRev () const

bool	isStrSplit () const

bool	isStrSplitAt () const

bool	isStrSplitRest () const

bool	isStrNumSplits () const

bool	isStrSplitAtRe () const

bool	isStrSplitRestRe () const

bool	isStrNumSplitsRe () const

bool	isStrOp () const

bool	isStrLt () const

bool	isStrLe () const

bool	isStrGt () const

bool	isStrGe () const

bool	isStrEq () const

bool	isStrComp () const

bool	isStrInReg () const

bool	isStrContains () const

bool	isStrIsDigit () const

bool	isStrProp () const

bool	isStrFromInt () const

bool	isStrToInt () const

bool	isStrToReg () const

bool	isStrToCode () const

bool	isStrFromCode () const

bool	isStrConv () const

bool	isRegNone () const

bool	isRegAll () const

bool	isRegAllChar () const

bool	isRegConcat () const

bool	isRegUnion () const

bool	isRegInter () const

bool	isRegDiff () const

bool	isRegStar () const

bool	isRegPlus () const

bool	isRegOpt () const

bool	isRegRange () const

bool	isRegRepeat () const

bool	isRegLoop () const

bool	isRegComplement () const

bool	isAtom () const

bool	isLet () const

bool	isLetChain () const

bool	isLetBindVarList () const

bool	isIte () const

bool	isFuncDec () const

bool	isFuncDef () const

bool	isFuncRec () const

bool	isFuncParam () const

bool	isFuncApplication () const

bool	isDtFunApplication () const

bool	isFuncRecApplication () const

size_t	getUseCount () const

void	incUseCount ()

void	decUseCount ()

std::string	getPureName () const

std::string	toString () const

std::shared_ptr< Sort >	getSort () const
	Get the sort of the node.

std::string	getName () const
	Get the name of the node.

std::string	rename (const std::string &new_name)
	Get the re-named name of the node.

NODE_KIND	getKind () const
	Get the kind of the node.

std::shared_ptr< Value >	getValue () const
	Get the value of the node.

void	setValue (std::shared_ptr< Value > v)
	Set the value of the node.

void	setValue (const Integer &v)

void	setValue (const Real &v)

void	setValue (const double &v)

void	setValue (const int &v)

void	setValue (const Interval &v)

size_t	getChildrenSize () const
	Get the number of children of the node.

std::vector< std::shared_ptr< DAGNode > >	getChildren () const
	Get the children of the node.

std::shared_ptr< DAGNode >	getChild (int i) const
	Get the child of the node.

std::shared_ptr< DAGNode >	getFuncBody () const
	Get the body of the function.

std::vector< std::shared_ptr< DAGNode > >	getFuncParams () const
	Get the parameters of the function.

size_t	getFuncParamsSize () const
	Get the number of parameters of the function.

std::shared_ptr< DAGNode >	getQuantBody () const
	Get the body of the quantifier.

std::vector< std::shared_ptr< DAGNode > >	getQuantVars () const
	Get the variables of the quantifier.

bool	isEquivalentTo (const std::shared_ptr< DAGNode > &other) const
	Check if the node is equivalent to another node.

bool	isEquivalentTo (const DAGNode &other) const
	Check if the node is equivalent to another node.

std::size_t	hashCode () const
	Get the hash code of the node.

void	updateFuncDef (std::shared_ptr< Sort > out_sort, std::shared_ptr< DAGNode > body, const std::vector< std::shared_ptr< DAGNode > > &params, bool is_rec=false)
	Update the function definition.

void	updateApplyFunc (std::shared_ptr< Sort > out_sort, std::shared_ptr< DAGNode > body, const std::vector< std::shared_ptr< DAGNode > > &params, bool is_rec=false)
	Update the function application.

Private Member Functions
bool	isEquivalentTo (const DAGNode &other, std::unordered_set< std::pair< const DAGNode , const DAGNode >, PairNodePtrHash, PairNodePtrEqual > &visited) const

Private Attributes
std::shared_ptr< Sort >	sort

NODE_KIND	kind

std::string	name

std::shared_ptr< Value >	value

std::vector< std::shared_ptr< DAGNode > >	children

std::string	children_hash

size_t	cached_hash_code

bool	hash_computed

size_t	_use_count

Detailed Description

Definition at line 74 of file dag.h.

Constructor & Destructor Documentation

◆ DAGNode() [1/14]

stabilizer::parser::DAGNode::DAGNode	(	std::shared_ptr< Sort >	sort,
		NODE_KIND	kind,
		std::string	name,
		std::vector< std::shared_ptr< DAGNode > >	children
	)

inline

Definition at line 89 of file dag.h.

References _use_count, cached_hash_code, children, children_hash, hash_computed, stabilizer::parser::TypeChecker::isInt(), stabilizer::parser::TypeChecker::isReal(), kind, name, stabilizer::parser::newValue(), stabilizer::parser::NT_CONST, and value.

◆ DAGNode() [2/14]

stabilizer::parser::DAGNode::DAGNode	(	std::shared_ptr< Sort >	sort,
		NODE_KIND	kind,
		std::string	name
	)

inline

Definition at line 118 of file dag.h.

References _use_count, cached_hash_code, children_hash, hash_computed, stabilizer::parser::TypeChecker::isInt(), stabilizer::parser::TypeChecker::isReal(), kind, name, stabilizer::parser::newValue(), stabilizer::parser::NT_CONST, and value.

◆ DAGNode() [3/14]

stabilizer::parser::DAGNode::DAGNode	(	std::shared_ptr< Sort >	sort,
		NODE_KIND	kind
	)

inline

Definition at line 135 of file dag.h.

References _use_count, cached_hash_code, children_hash, hash_computed, kind, stabilizer::parser::newValue(), stabilizer::parser::NT_CONST, and value.

◆ DAGNode() [4/14]

stabilizer::parser::DAGNode::DAGNode ( std::shared_ptr< Sort > sort )

inline

Definition at line 146 of file dag.h.

References _use_count, cached_hash_code, children_hash, hash_computed, kind, stabilizer::parser::newValue(), stabilizer::parser::NT_CONST, and value.

◆ DAGNode() [5/14]

stabilizer::parser::DAGNode::DAGNode ( )

inline

Definition at line 157 of file dag.h.

References children_hash.

std::shared_ptr< DAGNode > stabilizer::parser::DAGNode::getChild ( int i ) const

inline

Get the child of the node.

Parameters

i	The index of the child

Returns: The child of the node

Definition at line 987 of file dag.h.

References children.

Referenced by stabilizer::parser::dumpSMTLIB2_streaming(), getFuncParams(), getQuantVars(), isArithComp(), isBVCompOp(), isBVTerm(), isLiteral(), and isStrEq().

◆ getChildren()

std::vector< std::shared_ptr< DAGNode > > stabilizer::parser::DAGNode::getChildren ( ) const

inline

Get the children of the node.

Returns: The children of the node

Definition at line 977 of file dag.h.

References children.

Referenced by stabilizer::parser::dumpSMTLIB2_streaming().

◆ getChildrenSize()

size_t stabilizer::parser::DAGNode::getChildrenSize ( ) const

inline

Get the number of children of the node.

Returns: The number of children of the node

Definition at line 970 of file dag.h.

References children.

Referenced by stabilizer::parser::dumpSMTLIB2_streaming(), getFuncParams(), getFuncParamsSize(), getQuantVars(), and isStrEq().

◆ getFuncBody()

std::shared_ptr< DAGNode > stabilizer::parser::DAGNode::getFuncBody ( ) const

inline

Get the body of the function.

Returns: The body of the function

Definition at line 995 of file dag.h.

References children.

◆ getFuncParams()

std::vector< std::shared_ptr< DAGNode > > stabilizer::parser::DAGNode::getFuncParams ( ) const

inline

Get the parameters of the function.

Returns: The parameters of the function

Definition at line 1002 of file dag.h.

References getChild(), and getChildrenSize().

◆ getFuncParamsSize()

size_t stabilizer::parser::DAGNode::getFuncParamsSize ( ) const

inline

Get the number of parameters of the function.

Returns: The number of parameters of the function

Definition at line 1015 of file dag.h.

References getChildrenSize().

◆ getKind()

NODE_KIND stabilizer::parser::DAGNode::getKind ( ) const

inline

Get the kind of the node.

Returns: The kind of the node

Definition at line 939 of file dag.h.

References kind.

Referenced by stabilizer::parser::dumpSMTLIB2_streaming().

◆ getName()

std::string stabilizer::parser::DAGNode::getName ( ) const

inline

Get the name of the node.

Returns: The name of the node

Definition at line 921 of file dag.h.

References name.

Referenced by stabilizer::parser::dumpSMTLIB2_streaming().

◆ getPureName()

std::string stabilizer::parser::DAGNode::getPureName ( ) const

inline

Definition at line 900 of file dag.h.

References isLetBindVar(), name, and stabilizer::parser::PRESERVING_LET_BIND_VAR_SUFFIX.

Referenced by stabilizer::parser::dumpSMTLIB2_streaming(), and toString().

◆ getQuantBody()

std::shared_ptr< DAGNode > stabilizer::parser::DAGNode::getQuantBody ( ) const

inline

Get the body of the quantifier.

Returns: The body of the quantifier

Definition at line 1023 of file dag.h.

References children.

◆ getQuantVars()

std::vector< std::shared_ptr< DAGNode > > stabilizer::parser::DAGNode::getQuantVars ( ) const

inline

Get the variables of the quantifier.

Returns: The variables of the quantifier

Definition at line 1030 of file dag.h.

References getChild(), and getChildrenSize().

◆ getSort()

std::shared_ptr< Sort > stabilizer::parser::DAGNode::getSort ( ) const

inline

Get the sort of the node.

Returns: The sort of the node

Definition at line 915 of file dag.h.

References sort.

Referenced by stabilizer::parser::dumpSMTLIB2_streaming().

◆ getUseCount()

size_t stabilizer::parser::DAGNode::getUseCount ( ) const

inline

Definition at line 895 of file dag.h.

References _use_count.

◆ getValue()

std::shared_ptr< Value > stabilizer::parser::DAGNode::getValue ( ) const

inline

Get the value of the node.

Returns: The value of the node

Definition at line 946 of file dag.h.

References value.

◆ hashCode()

std::size_t stabilizer::parser::DAGNode::hashCode ( ) const

inline

Get the hash code of the node.

Returns: The hash code of the node

Definition at line 1068 of file dag.h.

References cached_hash_code, children, children_hash, hash_computed, kind, name, and sort.

inline

Definition at line 455 of file dag.h.

References kind, stabilizer::parser::NT_CONST_ARRAY, stabilizer::parser::NT_PLACEHOLDER_VAR, stabilizer::parser::NT_VAR, and sort.

bool stabilizer::parser::DAGNode::isAtom ( ) const

inline

Definition at line 866 of file dag.h.

References isArithComp(), isArithProp(), isBVCompOp(), isFPComp(), isFPProp(), isStrComp(), isStrProp(), isUFApplication(), and sort.

◆ isAttribute()

bool stabilizer::parser::DAGNode::isAttribute ( ) const

inline

Definition at line 363 of file dag.h.

References kind, stabilizer::parser::NT_ATTRIBUTE, stabilizer::parser::NT_NO_PATTERN, stabilizer::parser::NT_PATTERN, and stabilizer::parser::NT_WEIGHT.

bool stabilizer::parser::DAGNode::isBvAtom ( ) const

inline

Definition at line 688 of file dag.h.

References isBVCompOp().

bool stabilizer::parser::DAGNode::isBVNeg ( ) const

inline

Definition at line 624 of file dag.h.

References kind, and stabilizer::parser::NT_BV_NEG.

bool stabilizer::parser::DAGNode::isBVSAddO ( ) const

inline

Definition at line 637 of file dag.h.

References kind, and stabilizer::parser::NT_BV_SADDO.

◆ isBVSDiv()

bool stabilizer::parser::DAGNode::isBVSDiv ( ) const

inline

Definition at line 630 of file dag.h.

References kind, and stabilizer::parser::NT_BV_SDIV.

Referenced by isBVOp().

bool stabilizer::parser::DAGNode::isBVSModO ( ) const

inline

Definition at line 645 of file dag.h.

References kind, and stabilizer::parser::NT_BV_SMODO.

◆ isBVSMulO()

bool stabilizer::parser::DAGNode::isBVSMulO ( ) const

inline

Definition at line 639 of file dag.h.

References kind, and stabilizer::parser::NT_BV_SMULO.

◆ isBVSRem()

bool stabilizer::parser::DAGNode::isBVSRem ( ) const

inline

Definition at line 631 of file dag.h.

References kind, and stabilizer::parser::NT_BV_SREM.

Referenced by isBVOp().

bool stabilizer::parser::DAGNode::isBVUAddO ( ) const

inline

Definition at line 636 of file dag.h.

References kind, and stabilizer::parser::NT_BV_UADDO.

◆ isBVUDiv()

bool stabilizer::parser::DAGNode::isBVUDiv ( ) const

inline

Definition at line 628 of file dag.h.

References kind, and stabilizer::parser::NT_BV_UDIV.

Referenced by isBVOp().

bool stabilizer::parser::DAGNode::isBVUMod ( ) const

inline

Definition at line 632 of file dag.h.

References kind, and stabilizer::parser::NT_BV_UMOD.

◆ isBVUModO()

bool stabilizer::parser::DAGNode::isBVUModO ( ) const

inline

Definition at line 644 of file dag.h.

References kind, and stabilizer::parser::NT_BV_UMODO.

◆ isBVUMulO()

bool stabilizer::parser::DAGNode::isBVUMulO ( ) const

inline

Definition at line 638 of file dag.h.

References kind, and stabilizer::parser::NT_BV_UMULO.

◆ isBVURem()

bool stabilizer::parser::DAGNode::isBVURem ( ) const

inline

Definition at line 629 of file dag.h.

References kind, and stabilizer::parser::NT_BV_UREM.

Referenced by isBVOp().

bool stabilizer::parser::DAGNode::isCFP ( ) const

inline

Definition at line 360 of file dag.h.

References isConst(), and sort.

◆ isCInt()

bool stabilizer::parser::DAGNode::isCInt ( ) const

inline

Definition at line 353 of file dag.h.

References isConst(), and sort.

Referenced by isArithTerm(), and isNumeral().

◆ isConst()

bool stabilizer::parser::DAGNode::isConst ( ) const

inline

inline

Definition at line 887 of file dag.h.

References kind, and stabilizer::parser::NT_DT_FUN_APPLY.

◆ isE()

bool stabilizer::parser::DAGNode::isE ( ) const

inline

Definition at line 590 of file dag.h.

References kind, and stabilizer::parser::NT_CONST_E.

bool stabilizer::parser::DAGNode::isEquivalentTo ( const DAGNode & other ) const

inline

Check if the node is equivalent to another node.

Parameters

other The other node

Returns: True if the node is equivalent to the other node, false otherwise

Definition at line 1055 of file dag.h.

References isEquivalentTo().

◆ isEquivalentTo() [2/3]

bool stabilizer::parser::DAGNode::isEquivalentTo	(	const DAGNode &	other,
		std::unordered_set< std::pair< const DAGNode , const DAGNode >, PairNodePtrHash, PairNodePtrEqual > &	visited
	)		const

inlineprivate

Definition at line 1127 of file dag.h.

References children, children_hash, isEquivalentTo(), kind, name, and sort.

◆ isEquivalentTo() [3/3]

bool stabilizer::parser::DAGNode::isEquivalentTo ( const std::shared_ptr< DAGNode > & other ) const

inline

Check if the node is equivalent to another node.

Parameters

other The other node

Returns: True if the node is equivalent to the other node, false otherwise

Definition at line 1045 of file dag.h.

References isEquivalentTo().

Referenced by isEquivalentTo(), isEquivalentTo(), and isEquivalentTo().

bool stabilizer::parser::DAGNode::isFact ( ) const

inline

Definition at line 613 of file dag.h.

References kind, and stabilizer::parser::NT_FACT.

inline

Definition at line 707 of file dag.h.

References kind, and stabilizer::parser::NT_FP_NEG.

Referenced by isFPOp().

bool stabilizer::parser::DAGNode::isImplies ( ) const

inline

Definition at line 467 of file dag.h.

References kind, and stabilizer::parser::NT_IMPLIES.

◆ isInfinity()

bool stabilizer::parser::DAGNode::isInfinity ( ) const

inline

Definition at line 591 of file dag.h.

References kind, stabilizer::parser::NT_INFINITY, stabilizer::parser::NT_NEG_INFINITY, and stabilizer::parser::NT_POS_INFINITY.

◆ isInt()

bool stabilizer::parser::DAGNode::isInt ( ) const

inline

Definition at line 579 of file dag.h.

References kind, and stabilizer::parser::NT_IS_INT.

Referenced by isArithProp().

bool stabilizer::parser::DAGNode::isLcm ( ) const

inline

Definition at line 612 of file dag.h.

References kind, and stabilizer::parser::NT_LCM.

◆ isLe()

bool stabilizer::parser::DAGNode::isLe ( ) const

inline

Definition at line 556 of file dag.h.

References kind, and stabilizer::parser::NT_LE.

Referenced by isArithComp().

◆ isLeaf()

bool stabilizer::parser::DAGNode::isLeaf ( ) const

inline

Definition at line 318 of file dag.h.

References children.

◆ isLet()

bool stabilizer::parser::DAGNode::isLet ( ) const

inline

Definition at line 872 of file dag.h.

References kind, and stabilizer::parser::NT_LET.

◆ isLetBindVar()

bool stabilizer::parser::DAGNode::isLetBindVar ( ) const

inline

Definition at line 427 of file dag.h.

References kind, and stabilizer::parser::NT_LET_BIND_VAR.

Referenced by getPureName(), and isVar().

◆ isLetBindVarList()

bool stabilizer::parser::DAGNode::isLetBindVarList ( ) const

inline

Definition at line 874 of file dag.h.

References kind, and stabilizer::parser::NT_LET_BIND_VAR_LIST.

◆ isLetChain()

bool stabilizer::parser::DAGNode::isLetChain ( ) const

inline

Definition at line 873 of file dag.h.

References kind, and stabilizer::parser::NT_LET_CHAIN.

◆ isLg()

bool stabilizer::parser::DAGNode::isLg ( ) const

inline

Definition at line 520 of file dag.h.

References kind, and stabilizer::parser::NT_LG.

Referenced by isTranscendentalOp().

bool stabilizer::parser::DAGNode::isNaN ( ) const

inline

Definition at line 598 of file dag.h.

References kind, and stabilizer::parser::NT_NAN.

◆ isNatToBV()

bool stabilizer::parser::DAGNode::isNatToBV ( ) const

inline

Definition at line 692 of file dag.h.

References kind, and stabilizer::parser::NT_NAT_TO_BV.

Referenced by isBVConv().

◆ isNeg()

bool stabilizer::parser::DAGNode::isNeg ( ) const

inline

Definition at line 493 of file dag.h.

References kind, and stabilizer::parser::NT_NEG.

Referenced by isArithOp().

◆ isNegEpsilon()

bool stabilizer::parser::DAGNode::isNegEpsilon ( ) const

inline

Definition at line 605 of file dag.h.

References kind, and stabilizer::parser::NT_NEG_EPSILON.

◆ isNegInfinity()

bool stabilizer::parser::DAGNode::isNegInfinity ( ) const

inline

Definition at line 597 of file dag.h.

References kind, and stabilizer::parser::NT_NEG_INFINITY.

◆ isNeq()

bool stabilizer::parser::DAGNode::isNeq ( ) const

inline

Definition at line 484 of file dag.h.

References isDistinct().

◆ isNot()

bool stabilizer::parser::DAGNode::isNot ( ) const

inline

Definition at line 466 of file dag.h.

References kind, and stabilizer::parser::NT_NOT.

Referenced by isLiteral().

◆ isNull()

bool stabilizer::parser::DAGNode::isNull ( ) const

inline

Definition at line 322 of file dag.h.

References kind, and stabilizer::parser::NT_NULL.

◆ isNumeral()

bool stabilizer::parser::DAGNode::isNumeral ( ) const

inline

Definition at line 352 of file dag.h.

References isCInt(), and isCReal().

◆ isOdd()

bool stabilizer::parser::DAGNode::isOdd ( ) const

inline

Definition at line 583 of file dag.h.

References kind, and stabilizer::parser::NT_IS_ODD.

Referenced by isArithProp().

◆ isOr()

bool stabilizer::parser::DAGNode::isOr ( ) const

inline

Definition at line 465 of file dag.h.

References kind, and stabilizer::parser::NT_OR.

◆ isPi()

bool stabilizer::parser::DAGNode::isPi ( ) const

inline

Definition at line 589 of file dag.h.

References kind, and stabilizer::parser::NT_CONST_PI.

◆ isPlaceholderVar()

bool stabilizer::parser::DAGNode::isPlaceholderVar ( ) const

inline

Definition at line 428 of file dag.h.

References kind, and stabilizer::parser::NT_PLACEHOLDER_VAR.

Referenced by isVar().

◆ isPosEpsilon()

bool stabilizer::parser::DAGNode::isPosEpsilon ( ) const

inline

Definition at line 604 of file dag.h.

References kind, and stabilizer::parser::NT_POS_EPSILON.

bool stabilizer::parser::DAGNode::isTrue ( ) const

inline

Definition at line 336 of file dag.h.

References kind, stabilizer::parser::NT_CONST_TRUE, and sort.

◆ isUBVToInt()

bool stabilizer::parser::DAGNode::isUBVToInt ( ) const

inline

Definition at line 694 of file dag.h.

References kind, and stabilizer::parser::NT_UBV_TO_INT.

◆ isUFApplication()

bool stabilizer::parser::DAGNode::isUFApplication ( ) const

inline

Definition at line 487 of file dag.h.

References kind, and stabilizer::parser::NT_UF_APPLY.

Referenced by isArithTerm(), isArrayOp(), isAtom(), isBVTerm(), isFPOp(), and isStrOp().

◆ isUFName()

bool stabilizer::parser::DAGNode::isUFName ( ) const

inline

Definition at line 448 of file dag.h.

References kind, and stabilizer::parser::NT_UF_NAME.

bool stabilizer::parser::DAGNode::isVUF ( ) const

inline

Definition at line 445 of file dag.h.

References kind, stabilizer::parser::NT_VAR, and sort.

◆ isXor()

bool stabilizer::parser::DAGNode::isXor ( ) const

inline

Definition at line 468 of file dag.h.

References kind, and stabilizer::parser::NT_XOR.

◆ operator!=()

bool stabilizer::parser::DAGNode::operator!= ( const DAGNode elem )

inline

Definition at line 306 of file dag.h.

References children_hash, kind, name, and sort.

◆ operator==()

bool stabilizer::parser::DAGNode::operator== ( const DAGNode elem )

inline

Definition at line 302 of file dag.h.

References children_hash, kind, name, and sort.

◆ rename()

std::string stabilizer::parser::DAGNode::rename ( const std::string & new_name )

inline

Get the re-named name of the node.

Returns: The re-named name of the node

Set the value of the node.

Parameters

v	The value to set

Definition at line 953 of file dag.h.

References value.

◆ toString()

std::string stabilizer::parser::DAGNode::toString ( ) const

inline

Definition at line 907 of file dag.h.

References getPureName().

◆ updateApplyFunc()

void stabilizer::parser::DAGNode::updateApplyFunc	(	std::shared_ptr< Sort >	out_sort,
		std::shared_ptr< DAGNode >	body,
		const std::vector< std::shared_ptr< DAGNode > > &	params,
		bool	is_rec = `false`
	)

Update the function application.

Note: This function is only used to update the function application.

Parameters

out_sort	The output sort
body	The body of the function
params	The parameters of the function
is_rec	True when updating a recursive function application

Definition at line 57 of file dag.cpp.

References children, condAssert, kind, stabilizer::parser::NT_FUNC_APPLY, stabilizer::parser::NT_FUNC_REC_APPLY, and sort.

◆ updateFuncDef()

void stabilizer::parser::DAGNode::updateFuncDef	(	std::shared_ptr< Sort >	out_sort,
		std::shared_ptr< DAGNode >	body,
		const std::vector< std::shared_ptr< DAGNode > > &	params,
		bool	is_rec = `false`
	)

Update the function definition.

Note: This function is only used to update the function definition.

Parameters

out_sort	The output sort
body	The body of the function
params	The parameters of the function
is_rec	True when updating a recursive function definition

private

Definition at line 77 of file dag.h.

Referenced by DAGNode(), getSort(), hashCode(), isArithTerm(), isArray(), isArrayOp(), isAtom(), isBVTerm(), isCBool(), isCBV(), isCFP(), isCInt(), isCReal(), isCRoundingMode(), isCStr(), isEquivalentTo(), isFalse(), isFPOp(), isStrOp(), isTrue(), isVBool(), isVBV(), isVFP(), isVInt(), isVReal(), isVReg(), isVRoundingMode(), isVStr(), isVUF(), operator!=(), operator==(), updateApplyFunc(), and updateFuncDef().

◆ value

std::shared_ptr<Value> stabilizer::parser::DAGNode::value

private

Definition at line 80 of file dag.h.

Referenced by DAGNode(), DAGNode(), DAGNode(), DAGNode(), DAGNode(), DAGNode(), DAGNode(), getValue(), setValue(), setValue(), setValue(), setValue(), setValue(), and setValue().

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

src/parser/dag.h
src/parser/dag.cpp

Public Member Functions

Private Member Functions

Private Attributes

Detailed Description

Constructor & Destructor Documentation

◆ DAGNode() [1/14]

◆ DAGNode() [2/14]

◆ DAGNode() [3/14]

◆ DAGNode() [4/14]

◆ DAGNode() [5/14]

◆ DAGNode() [6/14]

◆ DAGNode() [7/14]

◆ DAGNode() [8/14]

◆ DAGNode() [9/14]

◆ DAGNode() [10/14]

◆ DAGNode() [11/14]

◆ DAGNode() [12/14]

◆ DAGNode() [13/14]

◆ DAGNode() [14/14]

Member Function Documentation

◆ clear()

◆ decUseCount()

◆ getChild()

◆ getChildren()

◆ getChildrenSize()

◆ getFuncBody()

◆ getFuncParams()

◆ getFuncParamsSize()

◆ getKind()

◆ getName()

◆ getPureName()

◆ getQuantBody()

◆ getQuantVars()

◆ getSort()

◆ getUseCount()

◆ getValue()

◆ hashCode()

◆ incUseCount()

◆ isAbs()

◆ isAcos()

◆ isAcosh()

◆ isAcot()

◆ isAcoth()

◆ isAcsc()

◆ isAcsch()

◆ isAdd()

◆ isAnd()

◆ isArithComp()

◆ isArithConv()

◆ isArithOp()

◆ isArithProp()

◆ isArithTerm()

◆ isArray()

◆ isArrayOp()

◆ isAsec()

◆ isAsech()

◆ isAsin()

◆ isAsinh()

◆ isAtan()

◆ isAtan2()

◆ isAtanh()

◆ isAtom()

◆ isAttribute()

◆ isAttributeParam()

◆ isBVAdd()

◆ isBVAnd()

◆ isBVASHR()

◆ isBvAtom()

◆ isBVComp()

◆ isBVCompOp()

◆ isBVConcat()

◆ isBVConv()

◆ isBVExtract()

◆ isBVLSHR()

◆ isBVMul()

◆ isBVNand()

◆ isBVNeg()

◆ isBVNegO()

◆ isBVNor()

◆ isBVNot()