CVC3
CVC3::Expr Member List

This is the complete list of members for CVC3::Expr, including all inherited members.

::CInterface classCVC3::Exprfriend
addToNotify(Theory *i, const Expr &e) const CVC3::Expr
andExpr(const Expr &right) const CVC3::Exprinline
arity() const CVC3::Exprinline
begin() const CVC3::Exprinline
clearFlags() const CVC3::Exprinline
clearRewriteNormal() const CVC3::Exprinline
compare(const Expr &e1, const Expr &e2)CVC3::Exprfriend
COMPUTE_TRANS_CLOSURE enum valueCVC3::Exprprivate
computeTransClosure() const CVC3::Exprinline
CONTAINS_BOUND_VAR enum valueCVC3::Exprprivate
containsBoundVar() const CVC3::Exprinline
containsTermITE() const CVC3::Expr
d_exprCVC3::Exprprivate
DynamicFlagsEnum enum nameCVC3::Exprprivate
end() const CVC3::Exprinline
eqExpr(const Expr &right) const CVC3::Exprinline
Expr(ExprValue *expr)CVC3::Exprinlineprivate
Expr()CVC3::Exprinline
Expr(const Expr &e)CVC3::Exprinline
Expr(const Op &op, const Expr &child)CVC3::Exprinline
Expr(const Op &op, const Expr &child0, const Expr &child1)CVC3::Exprinline
Expr(const Op &op, const Expr &child0, const Expr &child1, const Expr &child2)CVC3::Exprinline
Expr(const Op &op, const Expr &child0, const Expr &child1, const Expr &child2, const Expr &child3)CVC3::Exprinline
Expr(const Op &op, const std::vector< Expr > &children, ExprManager *em=NULL)CVC3::Exprinline
ExprClosure classCVC3::Exprfriend
ExprHasher classCVC3::Exprfriend
ExprManager classCVC3::Exprfriend
ExprNode classCVC3::Exprfriend
ExprValue classCVC3::Exprfriend
getBody() const CVC3::Exprinline
getBoundIndex() const CVC3::Exprinline
getEM() const CVC3::Exprinline
getEqNext() const CVC3::Exprinline
getExistential() const CVC3::Exprinline
getExprValue() const CVC3::Exprinline
getFind() const CVC3::Exprinline
getFindLevel() const CVC3::Exprinline
getFlag() const CVC3::Exprinline
getIndex() const CVC3::Exprinline
getIsAtomicFlag() const CVC3::Exprinline
getKids() const CVC3::Exprinline
getKind() const CVC3::Exprinline
getMMIndex() const CVC3::Exprinline
getName() const CVC3::Exprinline
getNotify() const CVC3::Exprinline
getOp() const CVC3::Exprinline
getOpExpr() const CVC3::Exprinline
getOpKind() const CVC3::Exprinline
getRational() const CVC3::Exprinline
getRep() const CVC3::Exprinline
getSig() const CVC3::Exprinline
getSimpCache() const CVC3::Exprinline
getSize() const CVC3::Exprinline
getString() const CVC3::Exprinline
getTerminalsConstFlag() const CVC3::Exprinline
getTheorem() const CVC3::Exprinline
getTriggers() const CVC3::Exprinline
getType() const CVC3::Exprinline
getUid() const CVC3::Exprinline
getVars() const CVC3::Exprinline
hasFind() const CVC3::Exprinline
hash(const Expr &e)CVC3::Exprinlinestatic
hash() const CVC3::Exprinline
hasLastIndex() const CVC3::Exprinline
hasRep() const CVC3::Exprinline
hasSig() const CVC3::Exprinline
iffExpr(const Expr &right) const CVC3::Exprinline
impExpr(const Expr &right) const CVC3::Exprinline
IMPLIED_LITERAL enum valueCVC3::Exprprivate
IN_USER_ASSUMPTION enum valueCVC3::Exprprivate
indent(int n, bool permanent=false)CVC3::Expr
inUserAssumption() const CVC3::Exprinline
IS_ATOMIC enum valueCVC3::Exprprivate
IS_FINITE enum valueCVC3::Exprprivate
IS_INT_ASSUMPTION enum valueCVC3::Exprprivate
IS_JUSTIFIED enum valueCVC3::Exprprivate
IS_REGISTERED_ATOM enum valueCVC3::Exprprivate
IS_SELECTED enum valueCVC3::Exprprivate
IS_STORED_PREDICATE enum valueCVC3::Exprprivate
IS_TRANSLATED enum valueCVC3::Exprprivate
IS_USER_ASSUMPTION enum valueCVC3::Exprprivate
IS_USER_REGISTERED_ATOM enum valueCVC3::Exprprivate
isAbsAtomicFormula() const CVC3::Exprinline
isAbsLiteral() const CVC3::Exprinline
isAnd() const CVC3::Exprinline
isApply() const CVC3::Exprinline
isAtomic() const CVC3::Expr
isAtomicFormula() const CVC3::Expr
isBoolConnective() const CVC3::Exprinline
isBoolConst() const CVC3::Exprinline
isBoundVar() const CVC3::Exprinline
isClosure() const CVC3::Exprinline
isConstant() const CVC3::Exprinline
isEq() const CVC3::Exprinline
isExists() const CVC3::Exprinline
isFalse() const CVC3::Exprinline
isFinite() const CVC3::Exprinline
isForall() const CVC3::Exprinline
isIff() const CVC3::Exprinline
isImpl() const CVC3::Exprinline
isImpliedLiteral() const CVC3::Exprinline
isInitialized() const CVC3::Exprinline
isIntAssumption() const CVC3::Exprinline
isITE() const CVC3::Exprinline
isJustified() const CVC3::Exprinline
isLambda() const CVC3::Exprinline
isLiteral() const CVC3::Exprinline
isNot() const CVC3::Exprinline
isNull() const CVC3::Exprinline
isOr() const CVC3::Exprinline
isPropAtom() const CVC3::Exprinline
isPropLiteral() const CVC3::Exprinline
isQuantifier() const CVC3::Exprinline
isRational() const CVC3::Exprinline
isRawList() const CVC3::Exprinline
isRegisteredAtom() const CVC3::Exprinline
isRewriteNormal() const CVC3::Exprinline
isSelected() const CVC3::Exprinline
isSkolem() const CVC3::Exprinline
isStoredPredicate() const CVC3::Exprinline
isString() const CVC3::Exprinline
isSymbol() const CVC3::Exprinline
isTerm() const CVC3::Exprinline
isTheorem() const CVC3::Exprinline
isTranslated() const CVC3::Exprinline
isTrue() const CVC3::Exprinline
isType() const CVC3::Exprinline
isUserAssumption() const CVC3::Exprinline
isUserRegisteredAtom() const CVC3::Exprinline
isValidType() const CVC3::Exprinline
isVar() const CVC3::Exprinline
isWellFounded() const CVC3::Exprinline
isXor() const CVC3::Exprinline
iteExpr(const Expr &thenpart, const Expr &elsepart) const CVC3::Exprinline
lookupType() const CVC3::Exprinline
mkOp() const CVC3::Exprinline
negate() const CVC3::Exprinline
NOT_ARRAY_NORMALIZED enum valueCVC3::Exprprivate
notArrayNormalized() const CVC3::Exprinline
notExpr() const CVC3::Exprinline
Op classCVC3::Exprfriend
operator!() const CVC3::Exprinline
operator!=(const Expr &e1, const Expr &e2)CVC3::Exprfriend
operator&&(const Expr &right) const CVC3::Exprinline
operator<(const Expr &e1, const Expr &e2)CVC3::Exprfriend
operator<<(std::ostream &os, const Expr &e)CVC3::Exprfriend
operator<=(const Expr &e1, const Expr &e2)CVC3::Exprfriend
operator=(const Expr &e)CVC3::Exprinline
operator==(const Expr &e1, const Expr &e2)CVC3::Exprfriend
operator>(const Expr &e1, const Expr &e2)CVC3::Exprfriend
operator>=(const Expr &e1, const Expr &e2)CVC3::Exprfriend
operator[](int i) const CVC3::Exprinline
operator||(const Expr &right) const CVC3::Exprinline
orExpr(const Expr &right) const CVC3::Exprinline
pprint() const CVC3::Expr
pprintnodag() const CVC3::Expr
print(InputLanguage lang, bool dagify=true) const CVC3::Expr
print() const CVC3::Exprinline
print(ExprStream &os) const CVC3::Expr
printAST(ExprStream &os) const CVC3::Expr
printnodag() const CVC3::Expr
rebuild(ExprManager *em) const CVC3::Exprinline
recursiveQuantSubst(const ExprHashMap< Expr > &subst, ExprHashMap< Expr > &visited) const CVC3::Exprprivate
recursiveSubst(const ExprHashMap< Expr > &subst, ExprHashMap< Expr > &visited) const CVC3::Exprprivate
REWRITE_NORMAL enum valueCVC3::Exprprivate
s_nullCVC3::Exprprivatestatic
setComputeTransClosure() const CVC3::Exprinline
setContainsBoundVar() const CVC3::Exprinline
setEqNext(const Theorem &e) const CVC3::Exprinline
setFind(const Theorem &e) const CVC3::Exprinline
setFinite() const CVC3::Exprinline
setFlag() const CVC3::Exprinline
setImpliedLiteral() const CVC3::Exprinline
setIntAssumption() const CVC3::Exprinline
setInUserAssumption(int scope=-1) const CVC3::Exprinline
setIsAtomicFlag(bool value) const CVC3::Exprinline
setJustified() const CVC3::Exprinline
setMultiTrigger(const std::vector< Expr > &multiTrigger) const CVC3::Exprinline
setNotArrayNormalized() const CVC3::Exprinline
setRegisteredAtom() const CVC3::Exprinline
setRep(const Theorem &e) const CVC3::Exprinline
setRewriteNormal() const CVC3::Exprinline
setSelected() const CVC3::Exprinline
setSig(const Theorem &e) const CVC3::Exprinline
setSimpCache(const Theorem &e) const CVC3::Exprinline
setStoredPredicate() const CVC3::Exprinline
setTerminalsConstFlag(bool value) const CVC3::Exprinline
setTranslated(int scope=-1) const CVC3::Exprinline
setTrigger(const Expr &trigger) const CVC3::Exprinline
setTriggers(const std::vector< std::vector< Expr > > &triggers) const CVC3::Exprinline
setTriggers(const std::vector< Expr > &triggers) const CVC3::Exprinline
setType(const Type &t) const CVC3::Exprinline
setUserAssumption(int scope=-1) const CVC3::Exprinline
setUserRegisteredAtom() const CVC3::Exprinline
setUsesCC() const CVC3::Exprinline
setValidType() const CVC3::Exprinline
setWellFounded() const CVC3::Exprinline
skolemExpr(int i) const CVC3::Exprinline
StaticFlagsEnum enum nameCVC3::Exprprivate
subExprOf(const Expr &e) const CVC3::Expr
substExpr(const std::vector< Expr > &oldTerms, const std::vector< Expr > &newTerms) const CVC3::Expr
substExpr(const ExprHashMap< Expr > &oldToNew) const CVC3::Expr
substExprQuant(const std::vector< Expr > &oldTerms, const std::vector< Expr > &newTerms) const CVC3::Expr
substExprQuant(const ExprHashMap< Expr > &oldToNew) const CVC3::Expr
substTriggers(const ExprHashMap< Expr > &subst, ExprHashMap< Expr > &visited) const CVC3::Exprprivate
TERMINALS_CONST enum valueCVC3::Exprprivate
Theorem classCVC3::Exprfriend
toString() const CVC3::Expr
toString(InputLanguage lang) const CVC3::Expr
typeCard() const CVC3::Exprinline
typeEnumerateFinite(Unsigned n) const CVC3::Exprinline
typeSizeFinite() const CVC3::Exprinline
unnegate() const CVC3::Exprinline
USES_CC enum valueCVC3::Exprprivate
usesCC() const CVC3::Exprinline
VALID_IS_ATOMIC enum valueCVC3::Exprprivate
VALID_TERMINALS_CONST enum valueCVC3::Exprprivate
VALID_TYPE enum valueCVC3::Exprprivate
validIsAtomicFlag() const CVC3::Exprinline
validSimpCache() const CVC3::Exprinline
validTerminalsConstFlag() const CVC3::Exprinline
WELL_FOUNDED enum valueCVC3::Exprprivate
xorExpr(const Expr &right) const CVC3::Exprinline
~Expr()CVC3::Exprinline