- _ -

• _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_producer.cpp , theorem_producer.cpp , common_theorem_producer.cpp , search_theorem_producer.cpp

- b -

• BASE_TRUST_LEVEL : decision_engine_caching.cpp , decision_engine_mbtf.cpp

- c -

• CACHE_SIZE : decision_engine_caching.cpp , decision_engine_mbtf.cpp
• CHECK : xchaff_utils.h
• CHECK_FULL : xchaff_utils.h
• CHECK_PROOFS : theorem_producer.h
• CHECK_SOUND : theorem_producer.h
• CLASS_NAME : array_theorem_producer.cpp , uf_theorem_producer.cpp , records_theorem_producer.cpp , quant_theorem_producer.cpp , arith_theorem_producer.cpp , arith_theorem_producer_old.cpp
• CVC_DLL : os.h

- d -

• DBG_PRINT : debug.h
• DBG_PRINT_MSG : debug.h
• DebugAssert : debug.h , hash_table.h

- f -

• FatalAssert : debug.h
• FLIPPED : xchaff_base.h
• followChaff : search_fast.cpp

- h -

• HASH_VALUE_ONE : theory_bitvector.cpp
• HASH_VALUE_ZERO : theory_bitvector.cpp

- i -

• IF_DEBUG : debug.h

- n -

• NULL_CLAUSE : xchaff_base.h

- p -

• PRIME : expr_value.h

- r -

• REG : expr_manager.cpp
• REG_TYPE : expr_manager.cpp

- s -

• STARTUP_LIT_POOL_SIZE : xchaff_dbase.h

- t -

• TEMPLATE_FAIL : minisat_global.h
• TRACE : debug.h
• TRACE_MSG : debug.h
• TURNOVER_RATE : decision_engine_mbtf.cpp , decision_engine_caching.cpp

- v -

• vals3 : circuit.cpp
• vals4 : circuit.cpp
• VERSION : main.cpp

---