CVC3::Expr Member List

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

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

Generated on Thu Oct 15 22:18:17 2009 for CVC3 by  doxygen 1.5.8