| andExpr(const std::vector< Expr > &children) | CVC3::ExprManager | [inline] |
| boolExpr() | CVC3::ExprManager | [inline] |
| checkType(const Expr &e) | CVC3::ExprManager | [private] |
| clear() | CVC3::ExprManager | |
| clearFlags() | CVC3::ExprManager | [inline] |
| computeType(const Expr &e) | CVC3::ExprManager | [private] |
| d_bool | CVC3::ExprManager | [private] |
| d_cm | CVC3::ExprManager | [private] |
| d_dagPrinting | CVC3::ExprManager | [private] |
| d_disableGC | CVC3::ExprManager | [private] |
| d_emptyVec | CVC3::ExprManager | [private] |
| d_exprSet | CVC3::ExprManager | [private] |
| d_false | CVC3::ExprManager | [private] |
| d_flagCounter | CVC3::ExprManager | [private] |
| d_indent | CVC3::ExprManager | [private] |
| d_indentTransient | CVC3::ExprManager | [private] |
| d_index | CVC3::ExprManager | [private] |
| d_inputLang | CVC3::ExprManager | [private] |
| d_inRebuild | CVC3::ExprManager | [private] |
| d_kindMap | CVC3::ExprManager | [private] |
| d_kindMapByName | CVC3::ExprManager | [private] |
| d_lineWidth | CVC3::ExprManager | [private] |
| d_mm | CVC3::ExprManager | [private] |
| d_mmFlag | CVC3::ExprManager | [private] |
| d_notifyObj | CVC3::ExprManager | [private] |
| d_nullExpr | CVC3::ExprManager | [private] |
| d_outputLang | CVC3::ExprManager | [private] |
| d_pointerHash | CVC3::ExprManager | [private] |
| d_postponed | CVC3::ExprManager | [private] |
| d_postponeGC | CVC3::ExprManager | [private] |
| d_prettyPrinter | CVC3::ExprManager | [private] |
| d_printDepth | CVC3::ExprManager | [private] |
| d_rebuildCache | CVC3::ExprManager | [private] |
| d_simpCacheTagCurrent | CVC3::ExprManager | [private] |
| d_tm | CVC3::ExprManager | [private] |
| d_true | CVC3::ExprManager | [private] |
| d_typeComputer | CVC3::ExprManager | [private] |
| d_typeKinds | CVC3::ExprManager | [private] |
| d_withIndentation | CVC3::ExprManager | [private] |
| dagPrinting() const | CVC3::ExprManager | [inline] |
| Expr class | CVC3::ExprManager | [friend] |
| ExprManager(ContextManager *cm, const CLFlags &flags) | CVC3::ExprManager | |
| ExprValue class | CVC3::ExprManager | [friend] |
| ExprValueSet typedef | CVC3::ExprManager | [private] |
| falseExpr() | CVC3::ExprManager | [inline] |
| gc(ExprValue *ev) | CVC3::ExprManager | |
| getCM() const | CVC3::ExprManager | [inline] |
| getCurrentContext() const | CVC3::ExprManager | [inline] |
| getEmptyVector() | CVC3::ExprManager | [inline] |
| getFlag() | CVC3::ExprManager | [inline, private] |
| getInputLang() const | CVC3::ExprManager | |
| getKind(const std::string &name) | CVC3::ExprManager | |
| getKindName(int kind) | CVC3::ExprManager | |
| getMM(size_t MMIndex) | CVC3::ExprManager | [inline] |
| getNullExpr() | CVC3::ExprManager | [inline] |
| getOutputLang() const | CVC3::ExprManager | |
| getPrinter() const | CVC3::ExprManager | [inline] |
| getSimpCacheTag() const | CVC3::ExprManager | [inline] |
| getTM() const | CVC3::ExprManager | [inline] |
| hash(const ExprValue *ev) const | CVC3::ExprManager | [inline, private] |
| hash(const Expr &e) const | CVC3::ExprManager | [inline] |
| HashEV class | CVC3::ExprManager | [friend] |
| incIndent(int n, bool permanent=false) | CVC3::ExprManager | |
| indent() const | CVC3::ExprManager | [inline] |
| indent(int n, bool permanent=false) | CVC3::ExprManager | |
| installExprValue(ExprValue *ev) | CVC3::ExprManager | [private] |
| invalidateSimpCache() | CVC3::ExprManager | [inline] |
| isActive() | CVC3::ExprManager | |
| isKindRegistered(int kind) | CVC3::ExprManager | [inline] |
| isTypeKind(int kind) | CVC3::ExprManager | [inline] |
| lastIndex() | CVC3::ExprManager | [inline] |
| lineWidth() const | CVC3::ExprManager | [inline] |
| newBoundVarExpr(const std::string &name, const std::string &uid) | CVC3::ExprManager | [inline] |
| newBoundVarExpr(const std::string &name, const std::string &uid, const Type &type) | CVC3::ExprManager | [inline] |
| newBoundVarExpr(const Type &type) | CVC3::ExprManager | [inline] |
| newClosureExpr(int kind, const std::vector< Expr > &vars, const Expr &body) | CVC3::ExprManager | [inline] |
| newExpr(ExprValue *ev) | CVC3::ExprManager | [inline] |
| newExprValue(ExprValue *ev) | CVC3::ExprManager | [private] |
| newKind(int kind, const std::string &name, bool isType=false) | CVC3::ExprManager | |
| newLeafExpr(const Op &op) | CVC3::ExprManager | [inline] |
| newRatExpr(const Rational &r) | CVC3::ExprManager | [inline] |
| newSkolemExpr(const Expr &e, int i) | CVC3::ExprManager | [inline] |
| newStringExpr(const std::string &s) | CVC3::ExprManager | [inline] |
| newSymbolExpr(const std::string &s, int kind) | CVC3::ExprManager | [inline] |
| newTheoremExpr(const Theorem &thm) | CVC3::ExprManager | [inline] |
| newVarExpr(const std::string &s) | CVC3::ExprManager | [inline] |
| nextFlag() | CVC3::ExprManager | [inline, private] |
| nextIndex() | CVC3::ExprManager | [inline] |
| Op class | CVC3::ExprManager | [friend] |
| orExpr(const std::vector< Expr > &children) | CVC3::ExprManager | [inline] |
| postponeGC() | CVC3::ExprManager | [inline] |
| printDepth() const | CVC3::ExprManager | [inline] |
| rebuild(const Expr &e) | CVC3::ExprManager | |
| rebuildRec(const Expr &e) | CVC3::ExprManager | [private] |
| registerPrettyPrinter(PrettyPrinter &printer) | CVC3::ExprManager | |
| registerSubclass(size_t sizeOfSubclass) | CVC3::ExprManager | |
| registerTypeComputer(TypeComputer *typeComputer) | CVC3::ExprManager | [inline] |
| restoreIndent() | CVC3::ExprManager | [inline] |
| resumeGC() | CVC3::ExprManager | |
| scopelevel() | CVC3::ExprManager | [inline] |
| setTM(TheoremManager *tm) | CVC3::ExprManager | [inline] |
| trueExpr() | CVC3::ExprManager | [inline] |
| Type class | CVC3::ExprManager | [friend] |
| unregisterPrettyPrinter() | CVC3::ExprManager | |
| withIndentation() const | CVC3::ExprManager | [inline] |
| ~ExprManager() | CVC3::ExprManager | |
