Here is a list of all file members with links to the files they belong to:

- a -

• abs() : rational-gmp.cpp
• AND : kinds.h
• AND_R : kinds.h
• andExpr() : expr.h
• APPLY : kinds.h
• args : main.cpp
• ArithKinds : theory_arith.h
• ArithLang : theory_arith.h
• ARRAY : theory_array.h
• ARRAY_LITERAL : theory_array.h
• ArrayKinds : theory_array.h
• arrayLiteral() : theory_array.h
• arrayType() : theory_array.h
• ARROW : kinds.h
• ASSERT : kinds.h
• ASSERTIONS : kinds.h
• AST_LANG : lang.h

- b -

• BITVECTOR : theory_bitvector.h
• BOOL_VAR : kinds.h
• BOOLEAN : kinds.h
• BOOLEXTRACT : theory_bitvector.h
• BOUND_ID : kinds.h
• BOUND_VAR : kinds.h
• boundVarCount : theory.cpp
• BVAND : theory_bitvector.h
• BVCONST : theory_bitvector.h
• BVGE : theory_bitvector.h
• BVGT : theory_bitvector.h
• BVKinds : theory_bitvector.h
• BVLE : theory_bitvector.h
• BVLT : theory_bitvector.h
• BVMULT : theory_bitvector.h
• BVNAND : theory_bitvector.h
• BVNEG : theory_bitvector.h
• BVNOR : theory_bitvector.h
• BVOR : theory_bitvector.h
• BVPARAMOP : theory_bitvector.h
• BVPLUS : theory_bitvector.h
• BVSUB : theory_bitvector.h
• BVTOINT : theory_bitvector.h
• BVTYPEPRED : theory_bitvector.h
• BVUMINUS : theory_bitvector.h
• BVXNOR : theory_bitvector.h
• BVXOR : theory_bitvector.h

- c -

• CALL : kinds.h
• CareSet : preprocess.cpp
• CareSetPtr : preprocess.cpp
• ceil() : rational-gmp.cpp
• cf() : preprocess.cpp
• CHECK_TYPE : kinds.h
• checkAssump() : search_fast.cpp
• checkAssumpDebug() : search_fast.cpp
• checkInt() : rational-gmp.cpp
• checkRewriteType() : theory_core.cpp
• CHECKSAT : kinds.h
• CLFLAG_BOOL : command_line_flags.h
• CLFLAG_INT : command_line_flags.h
• CLFLAG_NULL : command_line_flags.h
• CLFLAG_STRING : command_line_flags.h
• CLFLAG_STRVEC : command_line_flags.h
• CLFlagType : command_line_flags.h
• compare() : theorem.cpp, expr.cpp
• compareByPtr() : theorem.cpp
• compareLits() : search_fast.cpp
• computeBVConst() : theory_bitvector.h
• computeNegBVConst() : theory_bitvector.h
• CONCAT : theory_bitvector.h
• COND : kinds.h
• CONST : kinds.h
• constantKids() : theory_bitvector.cpp, bitvector_theorem_producer.cpp
• CONSTDEF : kinds.h
• CONSTRUCTOR : theory_datatype.h
• CONTEXT : kinds.h
• CONTINUE : kinds.h
• COUNTEREXAMPLE : kinds.h

- d -

• DARK_SHADOW : theory_arith.h
• DATATYPE : theory_datatype.h
• DatatypeKinds : theory_datatype.h
• DBG : kinds.h
• debugError() : debug.cpp
• debugger : debug.cpp
• DEFUN : kinds.h
• DIFF_ONLY : theory_arith.h
• DIVIDE : theory_arith.h
• divideExpr() : theory_arith.h
• DUMP_ASSUMPTIONS : kinds.h
• DUMP_CLOSURE : kinds.h
• DUMP_CLOSURE_PROOF : kinds.h
• DUMP_PROOF : kinds.h
• DUMP_SIG : kinds.h
• DUMP_TCC : kinds.h
• DUMP_TCC_ASSUMPTIONS : kinds.h
• DUMP_TCC_PROOF : kinds.h

- e -

• ECHO : kinds.h
• ELSE : kinds.h
• endl() : expr_stream.cpp
• EQ : kinds.h
• equal_to() : hash.h
• EXISTS : kinds.h
• EXPR_APPLY : expr.h
• EXPR_BOOL_VAR : expr.h
• EXPR_BOUND_VAR : expr.h
• EXPR_CC : expr.h
• EXPR_CLOSURE : expr.h
• EXPR_NAMED : expr.h
• EXPR_NODE : expr.h
• EXPR_RATIONAL : expr.h
• EXPR_SKOLEM : expr.h
• EXPR_STRING : expr.h
• EXPR_UCONST : expr.h
• EXPR_VALUE : expr.h
• EXPR_VALUE_TYPE_LAST : expr.h
• ExprIndex : expr.h
• ExprValueType : expr.h
• EXTRACT : theory_bitvector.h

- f -

• FALSE : kinds.h
• falseExpr() : expr.h
• fatalError() : debug.cpp
• fileToSMTLIBIdentifier() : vcl.cpp
• findExpr() : assumptions_value.cpp
• findExprs() : assumptions_value.cpp
• floor() : rational-gmp.cpp
• FORALL : kinds.h
• FORGET : kinds.h
• funType() : expr.cpp

- g -

• gcd() : rational-native.cpp, rational-gmp.cpp
• GE : theory_arith.h
• geExpr() : theory_arith.h
• GET_CHILD : kinds.h
• GET_TYPE : kinds.h
• getLanguage() : lang.h
• getOp() : expr_op.h
• GRAY_SHADOW : theory_arith.h
• GT : theory_arith.h
• gtExpr() : theory_arith.h

- h -

• hash() : hash.h
• HASH_TABLE_GROW_FACTOR : hash.h
• HASH_TABLE_GROW_THRESHOLD : hash.h
• HASH_TABLE_SIZE : hash.h
• HashUpdateIntData() : hash.h
• HELP : kinds.h
• HEXBVCONST : theory_bitvector.h
• hf() : preprocess.cpp

- i -

• ID : kinds.h
• IF : kinds.h
• IF_DEBUG() : theory_core.cpp, search_fast.cpp, main.cpp, context.cpp
• IFF : kinds.h
• IFF_R : kinds.h
• IFTHEN : kinds.h
• IMPLIES : kinds.h
• INCLUDE : kinds.h
• InputLanguage : lang.h
• insert() : hash.h
• INT : theory_arith.h
• int2string() : debug.h
• INTDIV : theory_arith.h
• INTTOBV : theory_bitvector.h
• IS_INTEGER : theory_arith.h
• isArray() : theory_array.h
• isArrayLiteral() : theory_array.h
• isDarkShadow() : theory_arith.h
• isDivide() : theory_arith.h
• isGE() : theory_arith.h
• isGT() : theory_arith.h
• isIneq() : theory_arith.h
• isInt() : theory_arith.h
• isIntPred() : theory_arith.h
• isLE() : theory_arith.h
• isLeafKind() : kinds.h
• isLT() : theory_arith.h
• isMinus() : theory_arith.h
• isMult() : theory_arith.h
• isPlus() : theory_arith.h
• isRational() : theory_arith.h
• isRead() : theory_array.h
• isReal() : theory_arith.h
• isTrivialExpr() : expr_stream.cpp
• isUMinus() : theory_arith.h
• isWrite() : theory_array.h
• ITE : kinds.h
• ITE_R : kinds.h

- k -

• Kind : kinds.h

- l -

• LAMBDA : kinds.h
• LAST_KIND : kinds.h
• lcm() : rational-native.cpp, rational-gmp.cpp
• LE : theory_arith.h
• leExpr() : theory_arith.h
• LEFTSHIFT : theory_bitvector.h
• LET : kinds.h
• LETDECL : kinds.h
• LETDECLS : kinds.h
• LINEAR : theory_arith.h
• LISP_LANG : lang.h
• LT : theory_arith.h
• ltExpr() : theory_arith.h

- m -

• main() : main.cpp
• merge() : theorem.cpp, theorem.h
• mergeVectors() : assumptions_value.cpp
• mf() : preprocess.cpp
• MINUS : theory_arith.h
• minusExpr() : theory_arith.h
• MOD : theory_arith.h
• mod() : rational-gmp.cpp
• MonomMap : arith_theorem_producer.cpp
• mult() : rational-native.cpp
• MULT : theory_arith.h
• multExpr() : theory_arith.h

- n -

• NEGINF : theory_arith.h
• NEQ : kinds.h
• newApplyExpr() : expr.h
• newBoolVarExpr() : expr.h
• newBoundVarExpr() : expr.h
• newClosureExpr() : expr.h
• newExpr() : expr.h
• newNamedExpr() : expr.h
• newRatExpr() : expr.h
• newRational() : rational.h
• newSkolemExpr() : expr.h
• newStringExpr() : expr.h
• newVarExpr() : expr.h
• nodag() : expr_stream.cpp
• NONLINEAR : theory_arith.h
• NOT : kinds.h
• NOT_USED : theory_arith.h
• NULL_KIND : kinds.h

- o -

• OLD_ARROW : kinds.h
• operator *() : theory_arith.h, rational-gmp.cpp
• operator!() : variable.h
• operator!=() : type.h, statistics.h, expr.h, debug.h, assumptions.h, rational-gmp.cpp, debug.cpp
• operator%() : rational-gmp.cpp
• operator+() : assumptions_value.cpp, theory_arith.h, rational-gmp.cpp, debug.cpp
• operator-() : assumptions_value.cpp, theory_arith.h, rational-gmp.cpp, debug.cpp
• operator/() : theory_arith.h, rational-gmp.cpp
• operator<() : theorem.h, expr.h, rational-gmp.cpp, debug.cpp
• operator<<() : dictionary.h, theory_arith.cpp, assumptions_value.cpp, variable.cpp, clause.cpp, variable.h, type.h, statistics.h, proof.h, exception.h, debug.h, rational-gmp.cpp, expr_stream.cpp, expr.cpp, debug.cpp
• operator<=() : theorem.h, expr.h, rational-gmp.cpp, debug.cpp
• operator==() : type.h, statistics.h, proof.h, expr.h, debug.h, assumptions.h, rational-gmp.cpp, debug.cpp
• operator>() : theorem.h, expr.h, rational-gmp.cpp, debug.cpp
• operator>=() : theorem.h, expr.h, rational-gmp.cpp, debug.cpp
• OPTION : kinds.h
• OR : kinds.h
• orExpr() : expr.h

- p -

• parse_args() : main.cpp
• parserTemp : parser.h
• PF_APPLY : kinds.h
• PF_HOLE : kinds.h
• PLUS : theory_arith.h
• plus() : rational-native.cpp
• plusExpr() : theory_arith.h
• POP : kinds.h
• pop() : expr_stream.cpp
• POP_SCOPE : kinds.h
• popdag() : expr_stream.cpp
• popSave() : expr_stream.cpp
• POPTO : kinds.h
• POPTO_SCOPE : kinds.h
• POSINF : theory_arith.h
• POW : theory_arith.h
• pow() : rational.h
• powExpr() : theory_arith.h
• PRESENTATION_LANG : lang.h
• PRINT : kinds.h
• printLit() : clause.cpp
• printRational() : rational.h
• printUsage() : main.cpp
• processNode() : search_fast.cpp
• programName : main.cpp
• PUSH : kinds.h
• push() : expr_stream.cpp
• PUSH_SCOPE : kinds.h
• pushdag() : expr_stream.cpp
• pushRestore() : expr_stream.cpp

- q -

• QUERY : kinds.h
• Queue : preprocess.cpp
• QueuePtr : preprocess.cpp

- r -

• RATIONAL_EXPR : kinds.h
• RAW_LIST : kinds.h
• READ : theory_array.h
• read() : theory_array.h
• REAL : theory_arith.h
• RECORD : theory_records.h
• RECORD_SELECT : theory_records.h
• RECORD_TYPE : theory_records.h
• RECORD_UPDATE : theory_records.h
• RecordKinds : theory_records.h
• recursiveSubst() : expr.cpp
• registerKinds() : expr_manager.cpp
• reset() : expr_stream.cpp
• RESTART : kinds.h
• RIGHTSHIFT : theory_bitvector.h

- s -

• SELECTOR : theory_datatype.h
• sighandler() : main.cpp
• SIMULATE : kinds.h
• SKOLEM_VAR : kinds.h
• SMTLIB_LANG : lang.h
• sort2() : vcl.cpp
• space() : expr_stream.cpp
• Str_To_Expr : vcl.h
• STRING_EXPR : kinds.h
• strPair() : vcl.cpp
• subExprRec() : expr.cpp
• SUBRANGE : theory_arith.h
• substExpr() : expr.cpp
• SUBSTITUTE : kinds.h
• SUBTYPE : kinds.h

- t -

• Table : preprocess.cpp
• TCC : kinds.h
• TERMS_ONLY : theory_arith.h
• TESTER : theory_datatype.h
• TheoremEq() : assumptions_value.cpp, search_fast.cpp
• TheoremMap : search_theorem_producer.h
• THISTYPE : theory_datatype.h
• TRACE : kinds.h
• TRANS_CLOSURE : theory_uf.h
• TRANSFORM : kinds.h
• TRUE : kinds.h
• trueExpr() : expr.h
• TUPLE : theory_records.h
• TUPLE_SELECT : theory_records.h
• TUPLE_TYPE : theory_records.h
• TUPLE_UPDATE : theory_records.h
• TYPE : kinds.h
• TYPEDECL : kinds.h
• TYPEDEF : kinds.h

- u -

• UCONST : kinds.h
• UFKinds : theory_uf.h
• uminus() : rational-native.cpp
• UMINUS : theory_arith.h
• uminusExpr() : theory_arith.h
• UNTRACE : kinds.h
• update_queue() : preprocess.cpp

- v -

• VARDECL : kinds.h
• VARDECLS : kinds.h
• VARLIST : kinds.h
• VARSHIFT : theory_bitvector.h
• vc : main.cpp
• version : main.cpp
• void_pointer : hash.h
• void_ptr : dictionary.h

- w -

• WHERE : kinds.h
• WRITE : theory_array.h
• write() : theory_array.h

- x -

• XOR : kinds.h

---