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

- _ -

• _CVC3_TRUSTED_ : cnf_theorem_producer.cpp , uf_theorem_producer.cpp , simulate_theorem_producer.cpp , records_theorem_producer.cpp , quant_theorem_producer.cpp , datatype_theorem_producer.cpp , core_theorem_producer.cpp , bitvector_theorem_producer.cpp , array_theorem_producer.cpp , arith_theorem_producer_old.cpp , arith_theorem_producer3.cpp , arith_theorem_producer.cpp , theorem_producer.cpp , common_theorem_producer.cpp , search_theorem_producer.cpp , dpllt_minisat.cpp

- b -

• boundedModulo() : bitvector_theorem_producer.cpp
• boundVarCount : theory.cpp
• bvdump : theory_bitvector.cpp

- c -

• canGetHead() : theory_quant.cpp
• CHECK_PROOFS : theorem_producer.h
• CHECK_SOUND : theorem_producer.h
• CLASS_NAME : arith_theorem_producer.cpp , quant_theorem_producer.cpp , records_theorem_producer.cpp , arith_theorem_producer3.cpp , uf_theorem_producer.cpp , arith_theorem_producer_old.cpp , array_theorem_producer.cpp
• cmpExpr() : theory_quant.cpp
• collectVars() : search_theorem_producer.cpp
• compareLits() : search_fast.cpp
• constantKids() : theory_bitvector.cpp , bitvector_theorem_producer.cpp , theory_bitvector.cpp
• CVC_DLL : os.h

- d -

• DBG_PRINT : debug.h
• DBG_PRINT_MSG : debug.h
• debug_full : minisat_solver.cpp
• debug_skolem : vc_cmd.cpp
• debug_write : theory_array.cpp
• DebugAssert : debug.h , hash_table.h
• defer_theory_propagation : minisat_solver.cpp

- e -

• eager_explanation : minisat_solver.cpp
• exprScore() : theory_quant.cpp

- f -

• FatalAssert : debug.h
• findAtom() : theory_array.cpp , theory_bitvector.cpp
• findPolarity() : theory_quant.cpp
• findPolarityAtomic() : theory_quant.cpp
• flatAnds() : theory_quant.cpp
• followChaff : search_fast.cpp
• FOUND_FALSE : theory_quant.cpp

- g -

• generateSatProof() : dpllt_minisat.cpp
• getBoundVars() : theory_quant.cpp
• getLeft() : theory_quant.cpp
• getPartTriggers() : theory_quant.cpp
• getRight() : theory_quant.cpp
• getSubTrig() : theory_quant.cpp
• goodMultiTriggers() : theory_quant.cpp

- h -

• hasBoundVarRec() : theory_core.cpp
• HASH_VALUE_ONE : theory_bitvector.cpp
• HASH_VALUE_ZERO : theory_bitvector.cpp
• hasMoreBVs() : theory_quant.cpp

- i -

• IF_DEBUG : debug.h , search_fast.cpp , vcl.cpp , theory_core.cpp
• is_leaf() : search_theorem_producer.cpp
• isGoodFullTrigger() : theory_quant.cpp
• isGoodMultiTrigger() : theory_quant.cpp
• isGoodPartTrigger() : theory_quant.cpp
• isGoodSysPredTrigger() : theory_quant.cpp
• isGround() : theory_quant.cpp
• isIntx() : theory_quant.cpp
• isSimpleTrig() : theory_quant.cpp
• isSuperSimpleTrig() : theory_quant.cpp
• isSysPred() : theory_quant.cpp
• isUniterpFunc() : theory_quant.cpp

- k -

• keep_lazy_explanation : minisat_solver.cpp

- l -

• LIMIT : bryant.cpp
• locVar() : theory_quant.cpp

- m -

• main() : main.cpp
• MonomMap : arith_theorem_producer_old.cpp , arith_theorem_producer3.cpp , arith_theorem_producer.cpp

- n -

• null_expr : theory_quant.cpp

- p -

• parse_args() : main.cpp
• PRIME : expr_value.h
• printSatProof() : dpllt_minisat.cpp
• printUsage() : main.cpp
• processNode() : search_fast.cpp
• programName : main.cpp
• prop_lookahead : minisat_solver.cpp
• protocol : minisat_solver.cpp
• push_theory_clause : minisat_solver.cpp
• push_theory_implication : minisat_solver.cpp
• push_theory_propagation : minisat_solver.cpp

- r -

• recGetSubTerms() : theory_quant.cpp
• recursiveExprScore() : theory_quant.cpp
• recursiveGetBoundVars() : theory_quant.cpp
• recursiveGetPartTriggers() : theory_quant.cpp
• recursiveGetSubTrig() : theory_quant.cpp
• REG : expr_manager.cpp
• REG_TYPE : expr_manager.cpp
• registerKinds() : expr_manager.cpp

- s -

• SATAssignmentHook() : dpllt_basic.cpp
• SATDecisionHook() : dpllt_basic.cpp
• SATDeductionHook() : dpllt_basic.cpp
• SATDLevelHook() : dpllt_basic.cpp
• setRecursiveInUserAssumption() : search_sat.cpp
• sighandler() : main.cpp

- t -

• TEMPLATE_FAIL : minisat_global.h
• TheoremEq() : search_fast.cpp
• TRACE : debug.h
• TRACE_MSG : debug.h
• trigInitScore() : theory_quant.cpp

- u -

• usefulInMatch() : theory_quant.cpp

- v -

• vals3 : circuit.cpp
• vals4 : circuit.cpp
• vc : main.cpp
• vectorExpr2string() : theory_quant.cpp
• VERSION : main.cpp