Attachment 238171 Details for Bug 353401 – Input file for dot

Input file for dot

classCVC3_1_1Assumptions_1_1iterator_1_1Proxy__coll__graph.dot (text/plain), 32.72 KB, created by Jerry James on 2007-10-25 22:58:18 UTC

(hide)

Description:

Filename:

MIME Type:

Creator: Jerry James

Created: 2007-10-25 22:58:18 UTC

Size: 32.72 KB

patch

obsolete

>digraph G
>{
>  edge [fontname="FreeSans.ttf",fontsize=10,labelfontname="FreeSans.ttf",labelfontsize=10];
>  node [fontname="FreeSans.ttf",fontsize=10,shape=record];
>  Node1 [label="{CVC3::Assumptions::iterator::Proxy\n|- d_t\l|+ Proxy()\l+ operator *()\l}",height=0.2,width=0.4,color="black", fillcolor="grey75", style="filled" fontcolor="black"];
>  Node2 -> Node1 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="d_t",arrowtail="open",fontname="FreeSans.ttf"];
>  Node2 [label="{CVC3::Theorem\n|+ d_thm\l+ d_expr\l- @2\l|+ printDebug()\l+ Theorem()\l+ Theorem()\l+ operator=()\l+ ~Theorem()\l+ withProof()\l+ withAssumptions()\l+ isNull()\l+ isRewrite()\l+ isAssump()\l+ isRefl()\l+ getExpr()\l+ getLHS()\l+ getRHS()\l+ getLeafAssumptions()\l+ getAssumptionsRef()\l+ getProof()\l+ getScope()\l+ getQuantLevel()\l+ setQuantLevel()\l+ hash()\l+ toString()\l+ printx()\l+ printxnodag()\l+ pprintx()\l+ pprintxnodag()\l+ print()\l+ print()\l+ isFlagged()\l+ clearAllFlags()\l+ setFlag()\l+ setExpandFlag()\l+ getExpandFlag()\l+ setLitFlag()\l+ getLitFlag()\l+ isAbsLiteral()\l+ refutes()\l+ proves()\l+ matches()\l+ setCachedValue()\l+ getCachedValue()\l+ TheoremEq()\l- Theorem()\l- Theorem()\l- Theorem()\l- Theorem()\l- recursivePrint()\l- getAssumptionsRec()\l- exprValue()\l- thm()\l* isFlagged()\l* clearAllFlags()\l* setFlag()\l* setExpandFlag()\l* getExpandFlag()\l* setLitFlag()\l* getLitFlag()\l* isAbsLiteral()\l* refutes()\l* proves()\l* matches()\l* setCachedValue()\l* getCachedValue()\l}",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$classCVC3_1_1Theorem.html"];
>  Node3 -> Node2 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="d_expr",arrowtail="open",fontname="FreeSans.ttf"];
>  Node3 [label="{CVC3::ExprValue\n|# d_kind\l# d_em\l# s_charHash\l# s_intHash\l- d_index\l- d_refcount\l- d_hash\l- d_find\l- d_type\l- d_notifyList\l- d_simpCache\l- d_simpCacheTag\l- d_dynamicFlags\l- d_flag\l|+ ExprValue()\l+ ~ExprValue()\l+ getKind()\l+ operator new()\l+ operator delete()\l+ operator delete()\l+ getMMIndex()\l+ operator==()\l+ getExprValue()\l+ isString()\l+ isRational()\l+ isVar()\l+ isApply()\l+ isSymbol()\l+ isClosure()\l+ isTheorem()\l+ getKids()\l+ arity()\l+ getSig()\l+ getRep()\l+ setSig()\l+ setRep()\l+ getUid()\l+ getString()\l+ getRational()\l+ getName()\l+ getVar()\l+ getOp()\l+ getVars()\l+ getBody()\l+ getExistential()\l+ getBoundIndex()\l+ getFields()\l+ getField()\l+ getTupleIndex()\l+ getTheorem()\l# getMM()\l# rebuild()\l# rebuild()\l# computeHash()\l# copy()\l# pointerHash()\l# hash()\l# hash()\l- setIndex()\l- incRefcount()\l- decRefcount()\l- hash()\l}",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$classCVC3_1_1ExprValue.html",tooltip="The base class for holding the actual data in expressions."];
>  Node4 -> Node3 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="s_intHash",arrowtail="open",fontname="FreeSans.ttf"];
>  Node4 [label="{Hash::hash\< long int \>\n||}",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$structHash_1_1hash.html"];
>  Node5 -> Node4 [dir=back,color="orange",fontsize=10,style="dashed",label="\< long int \>",fontname="FreeSans.ttf"];
>  Node5 [label="{Hash::hash\< _Key \>\n||}",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$structHash_1_1hash.html"];
>  Node6 -> Node3 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="s_charHash",arrowtail="open",fontname="FreeSans.ttf"];
>  Node6 [label="{Hash::hash\< char * \>\n||+ operator()()\l}",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$structHash_1_1hash_3_01char_01_5_01_4.html"];
>  Node7 -> Node3 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="d_notifyList",arrowtail="open",fontname="FreeSans.ttf"];
>  Node7 [label="{CVC3::NotifyList\n|- d_tlist\l- d_elist\l|+ NotifyList()\l+ size()\l+ add()\l+ getTheory()\l+ getExpr()\l}",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$classCVC3_1_1NotifyList.html"];
>  Node8 -> Node7 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="d_tlist",arrowtail="open",fontname="FreeSans.ttf"];
>  Node8 [label="{CVC3::CDList\< Theory * \>\n|- d_list\l- d_size\l|+ CDList()\l+ ~CDList()\l+ size()\l+ empty()\l+ push_back()\l+ pop_back()\l+ operator[]()\l+ at()\l+ back()\l+ begin()\l+ end()\l- makeCopy()\l- restoreData()\l- setNull()\l- CDList()\l}",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$classCVC3_1_1CDList.html"];
>  Node9 -> Node8 [dir=back,color="midnightblue",fontsize=10,style="solid",arrowtail="empty",fontname="FreeSans.ttf"];
>  Node9 [label="{CVC3::ContextObj\n|- d_scope\l- d_restore\l|+ ContextObj()\l+ ~ContextObj()\l+ level()\l+ isCurrent()\l+ makeCurrent()\l+ operator new()\l+ operator delete()\l+ operator new()\l+ operator delete()\l+ operator delete()\l# ContextObj()\l# operator=()\l# makeCopy()\l# restoreData()\l# getRestore()\l# setNull()\l# getCMM()\l- update()\l}",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$classCVC3_1_1ContextObj.html"];
>  Node10 -> Node9 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="d_restore",arrowtail="open",fontname="FreeSans.ttf"];
>  Node10 [label="{CVC3::ContextObjChain\n|- d_restoreChainNext\l- d_restoreChainPrev\l- d_restore\l- d_data\l- d_master\l|+ ~ContextObjChain()\l+ operator new()\l+ operator delete()\l+ operator delete()\l+ operator new()\l+ operator delete()\l- ContextObjChain()\l- restore()\l}",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$classCVC3_1_1ContextObjChain.html"];
>  Node10 -> Node10 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="d_restoreChainPrev\nd_restore\nd_restoreChainNext",arrowtail="open",fontname="FreeSans.ttf"];
>  Node9 -> Node10 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="d_data\nd_master",arrowtail="open",fontname="FreeSans.ttf"];
>  Node11 -> Node9 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="d_scope",arrowtail="open",fontname="FreeSans.ttf"];
>  Node11 [label="{CVC3::Scope\n|- d_context\l- d_cmm\l- d_prevScope\l- d_level\l- d_restoreChain\l|+ Scope()\l+ ~Scope()\l+ prevScope()\l+ level()\l+ isCurrent()\l+ topScope()\l+ getContext()\l+ getCMM()\l+ operator new()\l+ operator delete()\l+ operator delete()\l+ restore()\l+ finalize()\l+ check()\l- addToChain()\l}",height=0.2,width=0.4,color="red", fillcolor="white", style="filled",URL="$classCVC3_1_1Scope.html"];
>  Node10 -> Node11 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="d_restoreChain",arrowtail="open",fontname="FreeSans.ttf"];
>  Node11 -> Node11 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="d_prevScope",arrowtail="open",fontname="FreeSans.ttf"];
>  Node12 -> Node11 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="d_context",arrowtail="open",fontname="FreeSans.ttf"];
>  Node12 [label="{CVC3::Context\n|- d_cm\l- d_name\l- d_id\l- d_topScope\l- d_bottomScope\l- d_notifyObjList\l- d_cmmStack\l|+ Context()\l+ ~Context()\l+ getCM()\l+ name()\l+ id()\l+ topScope()\l+ bottomScope()\l+ level()\l+ push()\l+ pop()\l+ popto()\l+ addNotifyObj()\l+ deleteNotifyObj()\l+ getMemory()\l}",height=0.2,width=0.4,color="red", fillcolor="white", style="filled",URL="$classCVC3_1_1Context.html"];
>  Node11 -> Node12 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="d_bottomScope\nd_topScope",arrowtail="open",fontname="FreeSans.ttf"];
>  Node13 -> Node12 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="d_name",arrowtail="open",fontname="FreeSans.ttf"];
>  Node13 [label="{std::string\n||}",height=0.2,width=0.4,color="grey75", fillcolor="white", style="filled",tooltip="STL class."];
>  Node14 -> Node13 [dir=back,color="midnightblue",fontsize=10,style="solid",arrowtail="empty",fontname="FreeSans.ttf"];
>  Node14 [label="{std::basic_string\< char \>\n||}",height=0.2,width=0.4,color="grey75", fillcolor="white", style="filled"];
>  Node15 -> Node12 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="d_cm",arrowtail="open",fontname="FreeSans.ttf"];
>  Node15 [label="{CVC3::ContextManager\n|- d_curContext\l- d_contexts\l|+ ContextManager()\l+ ~ContextManager()\l+ push()\l+ pop()\l+ popto()\l+ scopeLevel()\l+ createContext()\l+ getCurrentContext()\l+ switchContext()\l+ getMemory()\l}",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$classCVC3_1_1ContextManager.html",tooltip="Manager for multiple contexts. Also holds current context."];
>  Node12 -> Node15 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="d_curContext",arrowtail="open",fontname="FreeSans.ttf"];
>  Node16 -> Node15 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="d_contexts",arrowtail="open",fontname="FreeSans.ttf"];
>  Node16 [label="{std::vector\< Context * \>\n||}",height=0.2,width=0.4,color="grey75", fillcolor="white", style="filled"];
>  Node17 -> Node16 [dir=back,color="orange",fontsize=10,style="dashed",label="\< Context * \>",fontname="FreeSans.ttf"];
>  Node17 [label="{std::vector\< T \>\n||}",height=0.2,width=0.4,color="grey75", fillcolor="white", style="filled",tooltip="STL class."];
>  Node18 -> Node8 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="d_list",arrowtail="open",fontname="FreeSans.ttf"];
>  Node18 [label="{std::deque\< Theory * \>\n||}",height=0.2,width=0.4,color="grey75", fillcolor="white", style="filled"];
>  Node19 -> Node8 [dir=back,color="orange",fontsize=10,style="dashed",label="\< Theory * \>",fontname="FreeSans.ttf"];
>  Node19 [label="{CVC3::CDList\< T \>\n|- d_list\l- d_size\l|+ CDList()\l+ ~CDList()\l+ size()\l+ empty()\l+ push_back()\l+ pop_back()\l+ operator[]()\l+ at()\l+ back()\l+ begin()\l+ end()\l- makeCopy()\l- restoreData()\l- setNull()\l- CDList()\l}",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$classCVC3_1_1CDList.html"];
>  Node9 -> Node19 [dir=back,color="midnightblue",fontsize=10,style="solid",arrowtail="empty",fontname="FreeSans.ttf"];
>  Node20 -> Node7 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="d_elist",arrowtail="open",fontname="FreeSans.ttf"];
>  Node20 [label="{CVC3::CDList\< Expr \>\n|- d_list\l- d_size\l|+ CDList()\l+ ~CDList()\l+ size()\l+ empty()\l+ push_back()\l+ pop_back()\l+ operator[]()\l+ at()\l+ back()\l+ begin()\l+ end()\l- makeCopy()\l- restoreData()\l- setNull()\l- CDList()\l}",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$classCVC3_1_1CDList.html"];
>  Node9 -> Node20 [dir=back,color="midnightblue",fontsize=10,style="solid",arrowtail="empty",fontname="FreeSans.ttf"];
>  Node21 -> Node20 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="d_list",arrowtail="open",fontname="FreeSans.ttf"];
>  Node21 [label="{std::deque\< Expr \>\n||}",height=0.2,width=0.4,color="grey75", fillcolor="white", style="filled"];
>  Node19 -> Node20 [dir=back,color="orange",fontsize=10,style="dashed",label="\< Expr \>",fontname="FreeSans.ttf"];
>  Node22 -> Node3 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="d_dynamicFlags",arrowtail="open",fontname="FreeSans.ttf"];
>  Node22 [label="{CVC3::CDFlags\n|- d_flags\l|+ CDFlags()\l+ ~CDFlags()\l+ set()\l+ clear()\l+ get()\l- makeCopy()\l- restoreData()\l- setNull()\l- update()\l- CDFlags()\l- operator=()\l}",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$classCVC3_1_1CDFlags.html"];
>  Node9 -> Node22 [dir=back,color="midnightblue",fontsize=10,style="solid",arrowtail="empty",fontname="FreeSans.ttf"];
>  Node2 -> Node3 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="d_simpCache",arrowtail="open",fontname="FreeSans.ttf"];
>  Node23 -> Node3 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="d_find",arrowtail="open",fontname="FreeSans.ttf"];
>  Node23 [label="{CVC3::CDO\< Theorem \>\n|- d_data\l|+ CDO()\l+ CDO()\l+ operator=()\l+ ~CDO()\l+ set()\l+ get()\l+ operator Theorem()\l- makeCopy()\l- restoreData()\l- setNull()\l- CDO()\l- operator=()\l}",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$classCVC3_1_1CDO.html"];
>  Node9 -> Node23 [dir=back,color="midnightblue",fontsize=10,style="solid",arrowtail="empty",fontname="FreeSans.ttf"];
>  Node2 -> Node23 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="d_data",arrowtail="open",fontname="FreeSans.ttf"];
>  Node24 -> Node23 [dir=back,color="orange",fontsize=10,style="dashed",label="\< Theorem \>",fontname="FreeSans.ttf"];
>  Node24 [label="{CVC3::CDO\< T \>\n|- d_data\l|+ CDO()\l+ CDO()\l+ ~CDO()\l+ set()\l+ get()\l+ operator T()\l+ operator=()\l- makeCopy()\l- restoreData()\l- setNull()\l- CDO()\l- operator=()\l}",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$classCVC3_1_1CDO.html"];
>  Node9 -> Node24 [dir=back,color="midnightblue",fontsize=10,style="solid",arrowtail="empty",fontname="FreeSans.ttf"];
>  Node25 -> Node24 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="d_data",arrowtail="open",fontname="FreeSans.ttf"];
>  Node25 [label="{T\n||}",height=0.2,width=0.4,color="grey75", fillcolor="white", style="filled"];
>  Node26 -> Node3 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="d_type",arrowtail="open",fontname="FreeSans.ttf"];
>  Node26 [label="{CVC3::Type\n|- d_expr\l|+ Type()\l+ Type()\l+ Type()\l+ Type()\l+ getExpr()\l+ arity()\l+ operator[]()\l+ isNull()\l+ isBool()\l+ isSubtype()\l+ isFunction()\l+ funType()\l+ toString()\l+ typeBool()\l+ anyType()\l+ funType()\l}",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$classCVC3_1_1Type.html"];
>  Node27 -> Node26 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="d_expr",arrowtail="open",fontname="FreeSans.ttf"];
>  Node27 [label="{CVC3::Expr\n|- d_expr\l- s_null\l|+ Expr()\l+ Expr()\l+ operator=()\l+ Expr()\l+ Expr()\l+ Expr()\l+ Expr()\l+ Expr()\l+ ~Expr()\l+ eqExpr()\l+ notExpr()\l+ negate()\l+ andExpr()\l+ orExpr()\l+ iteExpr()\l+ iffExpr()\l+ impExpr()\l+ skolemExpr()\l+ rebuild()\l+ substExpr()\l+ substExpr()\l+ operator!()\l+ operator &&()\l+ operator\|\|()\l+ hash()\l+ isFalse()\l+ isTrue()\l+ isBoolConst()\l+ isVar()\l+ isBoundVar()\l+ isString()\l+ isClosure()\l+ isQuantifier()\l+ isLambda()\l+ isApply()\l+ isSymbol()\l+ isTheorem()\l+ isType()\l+ getExprValue()\l+ isTerm()\l+ isAtomic()\l+ isAtomicFormula()\l+ isAbsAtomicFormula()\l+ isLiteral()\l+ isAbsLiteral()\l+ isBoolConnective()\l+ isPropAtom()\l+ isPropLiteral()\l+ isEq()\l+ isNot()\l+ isAnd()\l+ isOr()\l+ isITE()\l+ isIff()\l+ isImpl()\l+ isXor()\l+ isForall()\l+ isExists()\l+ isRational()\l+ isSkolem()\l+ getName()\l+ getUid()\l+ getString()\l+ getVars()\l+ getExistential()\l+ getBoundIndex()\l+ getBody()\l+ getRational()\l+ getTheorem()\l+ getEM()\l+ getKids()\l+ getKind()\l+ getIndex()\l+ hasLastIndex()\l+ mkOp()\l+ getOp()\l+ getOpExpr()\l+ getOpKind()\l+ arity()\l+ operator[]()\l+ unnegate()\l+ begin()\l+ end()\l+ isNull()\l+ isInitialized()\l+ getMMIndex()\l+ hasFind()\l+ getFind()\l+ getFindLevel()\l+ getNotify()\l+ getType()\l+ lookupType()\l+ validSimpCache()\l+ getSimpCache()\l+ isValidType()\l+ validIsAtomicFlag()\l+ getIsAtomicFlag()\l+ isRewriteNormal()\l+ isFinite()\l+ isWellFounded()\l+ computeTransClosure()\l+ containsBoundVar()\l+ isImpliedLiteral()\l+ isUserAssumption()\l+ inUserAssumption()\l+ isIntAssumption()\l+ isJustified()\l+ isTranslated()\l+ isUserRegisteredAtom()\l+ isRegisteredAtom()\l+ isSelected()\l+ isStoredPredicate()\l+ getFlag()\l+ setFlag()\l+ clearFlags()\l+ toString()\l+ toString()\l+ print()\l+ print()\l+ printnodag()\l+ pprint()\l+ pprintnodag()\l+ print()\l+ printAST()\l+ indent()\l+ setFind()\l+ addToNotify()\l+ setType()\l+ setSimpCache()\l+ setValidType()\l+ setIsAtomicFlag()\l+ setRewriteNormal()\l+ clearRewriteNormal()\l+ setFinite()\l+ setWellFounded()\l+ setComputeTransClosure()\l+ setContainsBoundVar()\l+ setImpliedLiteral()\l+ setUserAssumption()\l+ setInUserAssumption()\l+ setIntAssumption()\l+ setJustified()\l+ setTranslated()\l+ setUserRegisteredAtom()\l+ setRegisteredAtom()\l+ setSelected()\l+ setStoredPredicate()\l+ subExprOf()\l+ hasSig()\l+ hasRep()\l+ getSig()\l+ getRep()\l+ setSig()\l+ setRep()\l+ hash()\l- Expr()\l- recursiveSubst()\l}",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$classCVC3_1_1Expr.html",tooltip="Data structure of expressions in CVC3."];
>  Node3 -> Node27 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="d_expr",arrowtail="open",fontname="FreeSans.ttf"];
>  Node27 -> Node27 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="s_null",arrowtail="open",fontname="FreeSans.ttf"];
>  Node28 -> Node3 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="d_em",arrowtail="open",fontname="FreeSans.ttf"];
>  Node28 [label="{CVC3::ExprManager\n|- d_cm\l- d_tm\l- d_notifyObj\l- d_index\l- d_flagCounter\l- d_kindMap\l- d_typeKinds\l- d_kindMapByName\l- d_prettyPrinter\l- d_printDepth\l- d_withIndentation\l- d_indent\l- d_indentTransient\l- d_lineWidth\l- d_inputLang\l- d_outputLang\l- d_dagPrinting\l- d_mmFlag\l- d_exprSet\l- d_mm\l- d_pointerHash\l- d_bool\l- d_false\l- d_true\l- d_emptyVec\l- d_nullExpr\l- d_simpCacheTagCurrent\l- d_disableGC\l- d_postponeGC\l- d_postponed\l- d_rebuildCache\l- d_typeComputer\l|+ ExprManager()\l+ ~ExprManager()\l+ clear()\l+ isActive()\l+ gc()\l+ postponeGC()\l+ resumeGC()\l+ rebuild()\l+ nextIndex()\l+ lastIndex()\l+ clearFlags()\l+ boolExpr()\l+ falseExpr()\l+ trueExpr()\l+ getEmptyVector()\l+ getNullExpr()\l+ newExpr()\l+ newLeafExpr()\l+ newStringExpr()\l+ newRatExpr()\l+ newSkolemExpr()\l+ newVarExpr()\l+ newSymbolExpr()\l+ newBoundVarExpr()\l+ newBoundVarExpr()\l+ newBoundVarExpr()\l+ newClosureExpr()\l+ newTheoremExpr()\l+ andExpr()\l+ orExpr()\l+ hash()\l+ getCM()\l+ getCurrentContext()\l+ scopelevel()\l+ setTM()\l+ getTM()\l+ getMM()\l+ getSimpCacheTag()\l+ invalidateSimpCache()\l+ registerTypeComputer()\l+ printDepth()\l+ withIndentation()\l+ lineWidth()\l+ indent()\l+ indent()\l+ incIndent()\l+ restoreIndent()\l+ getInputLang()\l+ getOutputLang()\l+ dagPrinting()\l+ getPrinter()\l+ newKind()\l+ registerPrettyPrinter()\l+ unregisterPrettyPrinter()\l+ isKindRegistered()\l+ isTypeKind()\l+ getKindName()\l+ getKind()\l+ registerSubclass()\l- hash()\l- installExprValue()\l- rebuildRec()\l- newExprValue()\l- getFlag()\l- nextFlag()\l- computeType()\l- checkType()\l}",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$classCVC3_1_1ExprManager.html"];
>  Node29 -> Node28 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="d_mm",arrowtail="open",fontname="FreeSans.ttf"];
>  Node29 [label="{std::vector\< MemoryManager * \>\n||}",height=0.2,width=0.4,color="grey75", fillcolor="white", style="filled"];
>  Node17 -> Node29 [dir=back,color="orange",fontsize=10,style="dashed",label="\< MemoryManager * \>",fontname="FreeSans.ttf"];
>  Node30 -> Node28 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="d_prettyPrinter",arrowtail="open",fontname="FreeSans.ttf"];
>  Node30 [label="{CVC3::PrettyPrinter\n||+ PrettyPrinter()\l+ ~PrettyPrinter()\l+ print()\l}",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$classCVC3_1_1PrettyPrinter.html",tooltip="Abstract API to a pretty-printer for Expr."];
>  Node31 -> Node28 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="d_typeComputer",arrowtail="open",fontname="FreeSans.ttf"];
>  Node31 [label="{CVC3::ExprManager::TypeComputer\n||+ TypeComputer()\l+ ~TypeComputer()\l+ computeType()\l+ checkType()\l}",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$classCVC3_1_1ExprManager_1_1TypeComputer.html",tooltip="Abstract class for computing expr type."];
>  Node32 -> Node28 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="d_rebuildCache",arrowtail="open",fontname="FreeSans.ttf"];
>  Node32 [label="{CVC3::ExprHashMap\< Expr \>\n|- d_map\l|+ ExprHashMap()\l+ ExprHashMap()\l+ ExprHashMap()\l+ empty()\l+ size()\l+ count()\l+ operator[]()\l+ clear()\l+ insert()\l+ insert()\l+ erase()\l+ erase()\l+ begin()\l+ end()\l+ find()\l}",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$classCVC3_1_1ExprHashMap.html"];
>  Node33 -> Node32 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="d_map",arrowtail="open",fontname="FreeSans.ttf"];
>  Node33 [label="{Hash::hash_map\< _Key, _Data, _HashFcn, _EqualKey \>\n|# d_table\l|+ hash_map()\l+ hash_map()\l+ hash_map()\l+ hash_map()\l+ hash_map()\l+ operator=()\l+ swap()\l+ clear()\l+ find()\l+ find()\l+ operator[]()\l+ insert()\l+ erase()\l+ contains()\l+ count()\l+ empty()\l+ size()\l+ bucket_count()\l+ load_factor()\l+ begin()\l+ begin()\l+ end()\l+ end()\l}",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$classHash_1_1hash__map.html"];
>  Node34 -> Node33 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="d_table",arrowtail="open",fontname="FreeSans.ttf"];
>  Node34 [label="{Hash::hash_table\< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey \>\n|# d_hash\l# d_equal\l# d_extractKey\l# d_size\l# d_data\l|+ hash_table()\l+ hash_table()\l+ hash_table()\l+ hash_table()\l+ hash_table()\l+ ~hash_table()\l+ operator=()\l+ assignTable()\l+ swap()\l+ init()\l+ clear()\l+ find()\l+ find()\l+ insert()\l+ find_or_insert()\l+ erase()\l+ contains()\l+ count()\l+ empty()\l+ size()\l+ bucket_count()\l+ load_factor()\l+ begin()\l+ begin()\l+ end()\l+ end()\l# hash()\l# equal()\l# extractKey()\l# getBucketIndex()\l# getBucketByKey()\l# getBucketByKey()\l# getBucketByIndex()\l# getBucketByIndex()\l# resize()\l}",height=0.2,width=0.4,color="red", fillcolor="white", style="filled",URL="$classHash_1_1hash__table.html"];
>  Node17 -> Node34 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="d_data",arrowtail="open",fontname="FreeSans.ttf"];
>  Node35 -> Node32 [dir=back,color="orange",fontsize=10,style="dashed",label="\< Expr \>",fontname="FreeSans.ttf"];
>  Node35 [label="{CVC3::ExprHashMap\< Data \>\n|- d_map\l|+ ExprHashMap()\l+ ExprHashMap()\l+ ExprHashMap()\l+ empty()\l+ size()\l+ count()\l+ operator[]()\l+ clear()\l+ insert()\l+ erase()\l+ insert()\l+ erase()\l+ begin()\l+ end()\l+ find()\l}",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$classCVC3_1_1ExprHashMap.html"];
>  Node33 -> Node35 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="d_map",arrowtail="open",fontname="FreeSans.ttf"];
>  Node36 -> Node28 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="d_emptyVec",arrowtail="open",fontname="FreeSans.ttf"];
>  Node36 [label="{std::vector\< Expr \>\n||}",height=0.2,width=0.4,color="grey75", fillcolor="white", style="filled"];
>  Node17 -> Node36 [dir=back,color="orange",fontsize=10,style="dashed",label="\< Expr \>",fontname="FreeSans.ttf"];
>  Node37 -> Node28 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="d_exprSet",arrowtail="open",fontname="FreeSans.ttf"];
>  Node37 [label="{Hash::hash_set\< _Key, _HashFcn, _EqualKey \>\n|# d_table\l|+ hash_set()\l+ hash_set()\l+ hash_set()\l+ hash_set()\l+ hash_set()\l+ operator=()\l+ swap()\l+ clear()\l+ find()\l+ find()\l+ insert()\l+ erase()\l+ contains()\l+ count()\l+ empty()\l+ size()\l+ bucket_count()\l+ load_factor()\l+ begin()\l+ begin()\l+ end()\l+ end()\l}",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$classHash_1_1hash__set.html"];
>  Node34 -> Node37 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="d_table",arrowtail="open",fontname="FreeSans.ttf"];
>  Node27 -> Node28 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="d_nullExpr\nd_false\nd_bool\nd_true",arrowtail="open",fontname="FreeSans.ttf"];
>  Node38 -> Node28 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="d_tm",arrowtail="open",fontname="FreeSans.ttf"];
>  Node38 [label="{CVC3::TheoremManager\n|- d_cm\l- d_em\l- d_flags\l- d_mm\l- d_rwmm\l- d_withProof\l- d_withAssump\l- d_flag\l- d_active\l- d_rules\l- d_reflFlags\l- d_cachedValues\l- d_expandFlags\l- d_litFlags\l|+ TheoremManager()\l+ ~TheoremManager()\l+ clear()\l+ isActive()\l+ getCM()\l+ getEM()\l+ getFlags()\l+ getMM()\l+ getRWMM()\l+ getRules()\l+ getFlag()\l+ clearAllFlags()\l+ withProof()\l+ withAssumptions()\l+ setFlag()\l+ isFlagged()\l+ setCachedValue()\l+ getCachedValue()\l+ setExpandFlag()\l+ getExpandFlag()\l+ setLitFlag()\l+ getLitFlag()\l- createProofRules()\l}",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$classCVC3_1_1TheoremManager.html"];
>  Node39 -> Node38 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="d_flags",arrowtail="open",fontname="FreeSans.ttf"];
>  Node39 [label="{CVC3::CLFlags\n|- d_map\l|+ addFlag()\l+ countFlags()\l+ countFlags()\l+ getFlag()\l+ operator[]()\l+ setFlag()\l+ setFlag()\l+ setFlag()\l+ setFlag()\l+ setFlag()\l+ setFlag()\l+ setFlag()\l- getFlag0()\l}",height=0.2,width=0.4,color="red", fillcolor="white", style="filled",URL="$classCVC3_1_1CLFlags.html"];
>  Node40 -> Node38 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="d_cachedValues",arrowtail="open",fontname="FreeSans.ttf"];
>  Node40 [label="{Hash::hash_map\< long, int \>\n|# d_table\l|+ hash_map()\l+ hash_map()\l+ hash_map()\l+ hash_map()\l+ hash_map()\l+ operator=()\l+ swap()\l+ clear()\l+ find()\l+ find()\l+ operator[]()\l+ insert()\l+ erase()\l+ contains()\l+ count()\l+ empty()\l+ size()\l+ bucket_count()\l+ load_factor()\l+ begin()\l+ begin()\l+ end()\l+ end()\l}",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$classHash_1_1hash__map.html"];
>  Node34 -> Node40 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="d_table",arrowtail="open",fontname="FreeSans.ttf"];
>  Node33 -> Node40 [dir=back,color="orange",fontsize=10,style="dashed",label="\< long, int \>",fontname="FreeSans.ttf"];
>  Node41 -> Node38 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="d_rules",arrowtail="open",fontname="FreeSans.ttf"];
>  Node41 [label="{CVC3::CommonProofRules\n||+ ~CommonProofRules()\l+ queryTCC()\l+ implIntro3()\l+ assumpRule()\l+ reflexivityRule()\l+ rewriteReflexivity()\l+ symmetryRule()\l+ rewriteUsingSymmetry()\l+ transitivityRule()\l+ substitutivityRule()\l+ substitutivityRule()\l+ substitutivityRule()\l+ substitutivityRule()\l+ substitutivityRule()\l+ contradictionRule()\l+ excludedMiddle()\l+ iffTrue()\l+ iffNotFalse()\l+ iffTrueElim()\l+ iffFalseElim()\l+ iffContrapositive()\l+ notNotElim()\l+ iffMP()\l+ implMP()\l+ andElim()\l+ andIntro()\l+ andIntro()\l+ implIntro()\l+ implContrapositive()\l+ notToIff()\l+ xorToIff()\l+ rewriteIff()\l+ rewriteAnd()\l+ rewriteOr()\l+ rewriteNotTrue()\l+ rewriteNotFalse()\l+ rewriteNotNot()\l+ rewriteNotForall()\l+ rewriteNotExists()\l+ skolemize()\l+ skolemizeRewrite()\l+ skolemizeRewriteVar()\l+ varIntroRule()\l+ skolemize()\l+ varIntroSkolem()\l+ trueTheorem()\l+ rewriteAnd()\l+ rewriteOr()\l+ getSkolemAxioms()\l+ clearSkolemAxioms()\l+ ackermann()\l}",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$classCVC3_1_1CommonProofRules.html"];
>  Node42 -> Node38 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="d_litFlags\nd_reflFlags\nd_expandFlags",arrowtail="open",fontname="FreeSans.ttf"];
>  Node42 [label="{Hash::hash_map\< long, bool \>\n|# d_table\l|+ hash_map()\l+ hash_map()\l+ hash_map()\l+ hash_map()\l+ hash_map()\l+ operator=()\l+ swap()\l+ clear()\l+ find()\l+ find()\l+ operator[]()\l+ insert()\l+ erase()\l+ contains()\l+ count()\l+ empty()\l+ size()\l+ bucket_count()\l+ load_factor()\l+ begin()\l+ begin()\l+ end()\l+ end()\l}",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$classHash_1_1hash__map.html"];
>  Node34 -> Node42 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="d_table",arrowtail="open",fontname="FreeSans.ttf"];
>  Node33 -> Node42 [dir=back,color="orange",fontsize=10,style="dashed",label="\< long, bool \>",fontname="FreeSans.ttf"];
>  Node15 -> Node38 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="d_cm",arrowtail="open",fontname="FreeSans.ttf"];
>  Node43 -> Node38 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="d_rwmm\nd_mm",arrowtail="open",fontname="FreeSans.ttf"];
>  Node43 [label="{CVC3::MemoryManager\n||+ ~MemoryManager()\l+ newData()\l+ deleteData()\l}",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$classCVC3_1_1MemoryManager.html"];
>  Node28 -> Node38 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="d_em",arrowtail="open",fontname="FreeSans.ttf"];
>  Node44 -> Node28 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="d_kindMapByName",arrowtail="open",fontname="FreeSans.ttf"];
>  Node44 [label="{Hash::hash_map\< std::string, int, HashString \>\n|# d_table\l|+ hash_map()\l+ hash_map()\l+ hash_map()\l+ hash_map()\l+ hash_map()\l+ operator=()\l+ swap()\l+ clear()\l+ find()\l+ find()\l+ operator[]()\l+ insert()\l+ erase()\l+ contains()\l+ count()\l+ empty()\l+ size()\l+ bucket_count()\l+ load_factor()\l+ begin()\l+ begin()\l+ end()\l+ end()\l}",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$classHash_1_1hash__map.html"];
>  Node34 -> Node44 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="d_table",arrowtail="open",fontname="FreeSans.ttf"];
>  Node33 -> Node44 [dir=back,color="orange",fontsize=10,style="dashed",label="\< std::string, int, HashString \>",fontname="FreeSans.ttf"];
>  Node45 -> Node28 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="d_kindMap",arrowtail="open",fontname="FreeSans.ttf"];
>  Node45 [label="{Hash::hash_map\< int, std::string \>\n|# d_table\l|+ hash_map()\l+ hash_map()\l+ hash_map()\l+ hash_map()\l+ hash_map()\l+ operator=()\l+ swap()\l+ clear()\l+ find()\l+ find()\l+ operator[]()\l+ insert()\l+ erase()\l+ contains()\l+ count()\l+ empty()\l+ size()\l+ bucket_count()\l+ load_factor()\l+ begin()\l+ begin()\l+ end()\l+ end()\l}",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$classHash_1_1hash__map.html"];
>  Node34 -> Node45 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="d_table",arrowtail="open",fontname="FreeSans.ttf"];
>  Node33 -> Node45 [dir=back,color="orange",fontsize=10,style="dashed",label="\< int, std::string \>",fontname="FreeSans.ttf"];
>  Node46 -> Node28 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="d_pointerHash",arrowtail="open",fontname="FreeSans.ttf"];
>  Node46 [label="{Hash::hash\< void * \>\n||}",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$structHash_1_1hash.html"];
>  Node5 -> Node46 [dir=back,color="orange",fontsize=10,style="dashed",label="\< void * \>",fontname="FreeSans.ttf"];
>  Node13 -> Node28 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="d_mmFlag\nd_outputLang\nd_inputLang",arrowtail="open",fontname="FreeSans.ttf"];
>  Node47 -> Node28 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="d_notifyObj",arrowtail="open",fontname="FreeSans.ttf"];
>  Node47 [label="{CVC3::ExprManagerNotifyObj\n|- d_em\l|+ ExprManagerNotifyObj()\l+ notifyPre()\l+ notify()\l}",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$classCVC3_1_1ExprManagerNotifyObj.html",tooltip="Notifies ExprManager before and after each pop()."];
>  Node48 -> Node47 [dir=back,color="midnightblue",fontsize=10,style="solid",arrowtail="empty",fontname="FreeSans.ttf"];
>  Node48 [label="{CVC3::ContextNotifyObj\n|# d_context\l|+ ContextNotifyObj()\l+ ~ContextNotifyObj()\l+ notifyPre()\l+ notify()\l}",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$classCVC3_1_1ContextNotifyObj.html"];
>  Node12 -> Node48 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="d_context",arrowtail="open",fontname="FreeSans.ttf"];
>  Node28 -> Node47 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="d_em",arrowtail="open",fontname="FreeSans.ttf"];
>  Node15 -> Node28 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="d_cm",arrowtail="open",fontname="FreeSans.ttf"];
>  Node49 -> Node28 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="d_postponed",arrowtail="open",fontname="FreeSans.ttf"];
>  Node49 [label="{std::vector\< ExprValue * \>\n||}",height=0.2,width=0.4,color="grey75", fillcolor="white", style="filled"];
>  Node17 -> Node49 [dir=back,color="orange",fontsize=10,style="dashed",label="\< ExprValue * \>",fontname="FreeSans.ttf"];
>  Node50 -> Node28 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="d_typeKinds",arrowtail="open",fontname="FreeSans.ttf"];
>  Node50 [label="{Hash::hash_set\< int \>\n|# d_table\l|+ hash_set()\l+ hash_set()\l+ hash_set()\l+ hash_set()\l+ hash_set()\l+ operator=()\l+ swap()\l+ clear()\l+ find()\l+ find()\l+ insert()\l+ erase()\l+ contains()\l+ count()\l+ empty()\l+ size()\l+ bucket_count()\l+ load_factor()\l+ begin()\l+ begin()\l+ end()\l+ end()\l}",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$classHash_1_1hash__set.html"];
>  Node34 -> Node50 [dir=back,color="darkorchid3",fontsize=10,style="dashed",label="d_table",arrowtail="open",fontname="FreeSans.ttf"];
>  Node37 -> Node50 [dir=back,color="orange",fontsize=10,style="dashed",label="\< int \>",fontname="FreeSans.ttf"];
>}

Actions: View

Attachments on bug 353401: 238171