- a -

• Abort() : xchaff_utils.cpp , xchaff_utils.h
• ajr_debug_print() : Util.cpp , Util.h

- b -

• boundedModulo() : bitvector_theorem_producer.cpp

- c -

• canGetHead() : theory_quant.cpp
• cmpExpr() : theory_quant.cpp
• compare_var_stat() : xchaff_solver.cpp
• compareLits() : search_fast.cpp
• constantKids() : theory_bitvector.cpp , bitvector_theorem_producer.cpp , theory_bitvector.cpp
• contains() : theory_core.cpp
• containsRec() : theory_core.cpp

- e -

• exprScore() : theory_quant.cpp

- f -

• findAtom() : theory_array.cpp , theory_bitvector.cpp
• findPolarity() : theory_quant.cpp
• findPolarityAtomic() : theory_quant.cpp
• flatAnds() : theory_quant.cpp

- g -

• generateSatProof() : dpllt_minisat.cpp
• get_knd_order() : Util.cpp , Util.h
• get_knd_result() : Util.cpp , Util.h
• get_normalized() : Util.cpp , Util.h
• get_not() : Util.cpp , Util.h
• getBoundVars() : theory_quant.cpp
• getLeft() : theory_quant.cpp
• getPartTriggers() : theory_quant.cpp
• getRat() : Util.h , Util.cpp
• getRight() : theory_quant.cpp
• getSubTrig() : theory_quant.cpp
• goodMultiTriggers() : theory_quant.cpp

- h -

• hasBoundVarRec() : theory_core.cpp
• hasMoreBVs() : theory_quant.cpp

- i -

• is_comparison() : Util.cpp , Util.h
• is_eq_kind() : Util.h , Util.cpp
• is_opposite() : Util.cpp , Util.h
• is_smt_kind() : Util.h , Util.cpp
• isFlat() : Util.cpp , Util.h
• 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 -

• kind_to_str() : Util.cpp , Util.h

- l -

• locVar() : theory_quant.cpp

- m -

• main() : main.cpp
• make_flatten_expr() : Util.cpp , Util.h
• make_flatten_expr_h() : Util.cpp

- p -

• parse_args() : main.cpp
• print_mpq() : Util.cpp , Util.h
• print_rational() : Util.cpp , Util.h
• print_rational_divide() : Util.h , Util.cpp
• printSatProof() : dpllt_minisat.cpp
• printUsage() : main.cpp
• processNode() : search_fast.cpp

- r -

• recGetSubTerms() : theory_quant.cpp
• recursiveExprScore() : theory_quant.cpp
• recursiveGetBoundVars() : theory_quant.cpp
• recursiveGetPartTriggers() : theory_quant.cpp
• recursiveGetSubTrig() : theory_quant.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 -

• TheoremEq() : search_fast.cpp
• trigInitScore() : theory_quant.cpp

- u -

• usefulInMatch() : theory_quant.cpp

- v -

• vectorExpr2string() : theory_quant.cpp

- w -

• Warning() : xchaff_utils.cpp , xchaff_utils.h