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

Generated on Wed Nov 18 16:14:45 2009 for CVC3 by  doxygen 1.5.2