Here is a list of all class members with links to the classes they belong to:
- d -
- d_abInstCount
: CVC3::TheoryQuant
- d_active
: CVC3::TheoremManager
- d_activity
: MiniSat::Clause
, MiniSat::Solver
- d_added
: CVC3::VariableValue
- d_addInequalities_str
: LFSCObj
- d_all_good
: CVC3::CompleteInstPreProcessor
- d_all_index
: recCompleteInster
- d_all_multTrigsInfo
: CVC3::TheoryQuant
- d_allIndex
: CVC3::CompleteInstPreProcessor
- d_allInstCount
: CVC3::TheoryQuant
- d_allInstCount2
: CVC3::TheoryQuant
- d_allInsts
: CVC3::TheoryQuant
- d_allmap_trigs
: CVC3::TheoryQuant
- d_allout
: CVC3::TheoryQuant
- d_alltrig_list
: CVC3::TheoryQuant
- d_analyze_redundant
: MiniSat::Solver
- d_analyze_seen
: MiniSat::Solver
- d_analyze_stack
: MiniSat::Solver
- d_and_final_s
: LFSCObj
- d_and_mid_s
: LFSCObj
- d_andE_str
: LFSCObj
- d_ante
: CVC3::VariableValue
- d_anteIdx
: CVC3::VariableValue
- d_applicationsInModel
: CVC3::TheoryArray
, CVC3::TheoryUF
- d_applyCNFRulesCache
: CVC3::SearchImplBase
- d_arithUsed
: CVC3::Translator
- d_arrayConvertMap
: CVC3::Translator
- d_arrayIndic
: CVC3::TheoryQuant
- d_arrayTrigs
: CVC3::TheoryQuant
- d_arrayType
: CVC3::Translator
- d_assertions
: SAT::DPLLTBasic
- d_assertionsStack
: SAT::DPLLTBasic
- d_assigns
: MiniSat::Solver
- d_assm
: LFSCAssume
- d_assump
: CVC3::VariableValue
, CVC3::RegTheoremValue
, CVC3::RWTheoremValue
- d_assump_map
: LFSCObj
- d_assump_str
: LFSCObj
- d_assumptions
: CVC3::SearchImplBase
- d_ax
: CVC3::Translator
- d_basic_subst_op0_str
: LFSCObj
- d_basic_subst_op1_str
: LFSCObj
- d_basic_subst_op_str
: LFSCObj
- d_basicModelVars
: CVC3::TheoryCore
- d_batchedAssertions
: CVC3::VCL
- d_batchedAssertionsIdx
: CVC3::VCL
- d_bb_index
: CVC3::TheoryBitvector
- d_beginningOfLine
: CVC3::ExprStream
- d_benchName
: CVC3::Translator
- d_berkminFlag
: CVC3::SearchEngineFast
- d_bestByExpr
: CVC3::DecisionEngine
- d_bindGlobalHistory
: CVC3::TheoryQuant
- d_bindGlobalThmHistory
: CVC3::TheoryQuant
- d_bindHistory
: CVC3::TheoryQuant
- d_bitblast
: CVC3::TheoryBitvector
- d_bitvecCache
: CVC3::TheoryBitvector
- d_body
: CVC3::ExprClosure
, LFSCPfLet
, recCompleteInster
- d_bool
: CVC3::ExprManager
- d_bool_res_str
: LFSCObj
- d_booleanRWFlag
: CVC3::TheoryBitvector
- d_boolExtractCacheFlag
: CVC3::TheoryBitvector
- d_bottomLevel
: CVC3::DecisionEngineCaching
, CVC3::DecisionEngineMBTF
- d_bottomScope
: SAT::CNF_Manager
, CVC3::Context
, CVC3::SearchImplBase
, CVC3::SearchSat
- d_boundVarMap
: CVC3::TheoryCore
- d_boundVarStack
: CVC3::TheoryCore
- d_budgetLimit
: CVC3::ExprTransform
- d_buff
: recCompleteInster
- d_buffer
: CVC3::TheoryArith3
, CVC3::TheoryArithNew
- d_buffer_0
: CVC3::TheoryArithOld
- d_buffer_1
: CVC3::TheoryArithOld
- d_buffer_2
: CVC3::TheoryArithOld
- d_buffer_3
: CVC3::TheoryArithOld
- d_bufferIdx
: CVC3::TheoryArith3
, CVC3::TheoryArithNew
- d_bufferIdx_0
: CVC3::TheoryArithOld
- d_bufferIdx_1
: CVC3::TheoryArithOld
- d_bufferIdx_2
: CVC3::TheoryArithOld
- d_bufferIdx_3
: CVC3::TheoryArithOld
- d_bufferThres
: CVC3::TheoryArith3
, CVC3::TheoryArithNew
, CVC3::TheoryArithOld
- d_bv32Flag
: CVC3::TheoryBitvector
- d_bvAssertDiseq
: CVC3::TheoryBitvector
- d_bvAssertEq
: CVC3::TheoryBitvector
- d_bvBitBlastDiseq
: CVC3::TheoryBitvector
- d_bvBitBlastEq
: CVC3::TheoryBitvector
- d_bvconst
: CVC3::BVConstExpr
- d_bvConstExprIndex
: CVC3::TheoryBitvector
- d_bvDelayDiseq
: CVC3::TheoryBitvector
- d_bvDelayEq
: CVC3::TheoryBitvector
- d_bvDelayTypePreds
: CVC3::TheoryBitvector
- d_bvOne
: CVC3::TheoryBitvector
, CVC3::BitvectorTheoremProducer
- d_bvParameterExprIndex
: CVC3::TheoryBitvector
- d_bvPlusCarryCacheLeftBV
: CVC3::TheoryBitvector
- d_bvPlusCarryCacheRightBV
: CVC3::TheoryBitvector
- d_bvPlusExprIndex
: CVC3::TheoryBitvector
- d_bvs
: recCompleteInster
- d_bvTypePredExprIndex
: CVC3::TheoryBitvector
- d_bvTypePreds
: CVC3::TheoryBitvector
- d_bvZero
: CVC3::TheoryBitvector
, CVC3::BitvectorTheoremProducer
- d_c
: TReturn
- d_cache
: CVC3::TheoryArith3::VarOrderGraph
, CVC3::TheoryArithNew::VarOrderGraph
, CVC3::TheoryArithOld::VarOrderGraph
, CVC3::DecisionEngineCaching
, CVC3::DecisionEngineMBTF
- d_cachedValue
: CVC3::TheoremValue
- d_cachedValues
: CVC3::TheoremManager
- d_cacheTheorem
: CVC3::TheoryQuant
- d_cacheThmPos
: CVC3::TheoryQuant
- d_calledFromParser
: CVC3::VCCmd
- d_callThisRound
: CVC3::TheoryQuant
- d_canon_invert_divide_str
: LFSCObj
- d_canon_mult_str
: LFSCObj
- d_canon_plus_str
: LFSCObj
- d_category
: CVC3::Translator
- d_cdmap
: CVC3::CDOmap< Key, Data, HashFcn >
, CVC3::CDOmapOrdered< Key, Data >
- d_cdo
: CVC3::SmartCDO< T >::RefCDO< U >
- d_checkProofs
: CVC3::TheoremProducer
- d_children
: CVC3::ExprNode
, CVC3::ExprNodeTmp
, LFSCBoolRes
, LFSCLraAdd
, LFSCLraSub
- d_chunkList
: CVC3::MemoryManagerChunks
, CVC3::ContextMemoryManager
- d_chunkSize
: CVC3::MemoryManagerChunks
- d_chunkSizeBytes
: CVC3::MemoryManagerChunks
- d_circuitPropCount
: CVC3::SearchEngineFast
- d_circuits
: CVC3::SearchEngineFast
- d_circuitsByExpr
: CVC3::SearchEngineFast
- d_cla_decay
: MiniSat::Solver
- d_cla_inc
: MiniSat::Solver
- d_clause
: CVC3::Clause
, CVC3::ClauseOwner
, CVC3::CompactClause
- d_clauseID
: MiniSat::PushEntry
- d_clauseIDCounter
: MiniSat::Solver
- d_clauseIdNext
: SAT::CNF_Manager
- d_clauselit
: CVC3::TheoremValue
- d_clauses
: CVC3::SearchEngineFast
, MiniSat::Derivation
, MiniSat::Solver
- d_clausesQueryEnd
: CVC3::SearchEngineFast
- d_clausesQueryStart
: CVC3::SearchEngineFast
- d_cm
: CVC3::Context
, SAT::DPLLTBasic
, CVC3::ExprManager
, CVC3::TheoremManager
, CVC3::TheoryCore
, CVC3::VariableManager
, CVC3::VCL
, CVC3::SearchSatTheoryAPI
- d_cmm
: CVC3::Scope
- d_cmmStack
: CVC3::Context
- d_cnf
: SAT::DPLLTBasic
- d_cnf_add_unit_str
: LFSCObj
- d_cnf_convert_str
: LFSCObj
- d_CNF_str
: LFSCObj
- d_cnfCache
: CVC3::SearchImplBase
- d_cnfCallback
: SAT::CNF_Manager
, CVC3::SearchSat
- d_CNFITE_str
: LFSCObj
- d_cnfManager
: CVC3::SearchSat
- d_cnfOption
: CVC3::SearchImplBase
- d_cnfStack
: SAT::DPLLTBasic
- d_cnfVars
: SAT::CNF_Manager
, CVC3::SearchImplBase
- d_col
: CVC3::ExprStream
, LFSCBoolRes
- d_combineAssump
: CVC3::Translator
- d_common_pf_rules
: LFSCPrinter
- d_commonRules
: SAT::CNF_Manager
, CVC3::ExprTransform
, CVC3::SearchEngine
, CVC3::Theory
, CVC3::SearchEngineTheoremProducer
- d_conflict
: MiniSat::Solver
- d_conflictClauseCount
: CVC3::SearchEngineFast
- d_conflictClauseManager
: CVC3::SearchEngineFast
- d_conflictClauses
: CVC3::SearchEngineFast
- d_conflictClauseStack
: CVC3::SearchEngineFast
- d_conflictCount
: CVC3::SearchEngineFast
- d_conflictTheorem
: CVC3::SearchEngineFast
- d_const
: CVC3::TheoryArith3::Ineq
, CVC3::TheoryArithNew::Ineq
, CVC3::TheoryArithOld::Ineq
- d_const_predicate_str
: LFSCObj
- d_constructorMap
: CVC3::TheoryDatatype
- d_context
: CVC3::CDMap< Key, Data, HashFcn >
, CVC3::CDMapOrdered< Key, Data >
, CVC3::Scope
, CVC3::ContextNotifyObj
- d_contextCache
: CVC3::TheoryQuant
- d_contextMap
: CVC3::TheoryQuant
- d_contexts
: CVC3::ContextManager
- d_contextTerms
: CVC3::TheoryQuant
- d_convertArith
: CVC3::Translator
- d_convertArray
: CVC3::Translator
- d_convertToBV
: CVC3::Translator
- d_convertToDiff
: CVC3::Translator
- d_core
: CVC3::ExprTransform
, CVC3::SearchEngine
, CVC3::DecisionEngine
, CVC3::CoreTheoremProducer
, CVC3::PrettyPrinterCore
, CVC3::TypeComputerCore
- d_coreSatAPI
: CVC3::SearchSat
, CVC3::TheoryCore
- d_coreSatAPI_implBase
: CVC3::SearchImplBase
- d_count
: CVC3::VariableValue
- d_counter
: CVC3::StatCounter
- d_counters
: CVC3::Statistics
- d_countLeft
: CVC3::TheoryArith3
, CVC3::TheoryArithNew
, CVC3::TheoryArithOld
- d_countPrev
: CVC3::VariableValue
- d_countRight
: CVC3::TheoryArith3
, CVC3::TheoryArithNew
, CVC3::TheoryArithOld
- d_createProof
: SAT::DPLLTMiniSat
- d_curContext
: CVC3::ContextManager
- d_curMaxExprScore
: CVC3::TheoryQuant
- d_currDepth
: CVC3::ExprStream
- d_current
: SAT::CNF_Formula
- d_currentRecursiveSimplifier
: CVC3::TheoryCore
- d_cycle_conflict_str
: LFSCObj
- d_dag
: CVC3::ExprStream
- d_dagBuilt
: CVC3::ExprStream
- d_dagMap
: CVC3::ExprStream
- d_dagPrinting
: CVC3::ExprManager
- d_dagPtr
: CVC3::ExprStream
- d_dagStack
: CVC3::ExprStream
- d_data
: CVC3::CDOmap< Key, Data, HashFcn >
, CVC3::CDOmapOrdered< Key, Data >
, CVC3::CDO< T >
, CVC3::CLFlag
, CVC3::ContextObjChain
, Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey >
, CVC3::Parser
, CVC3::SmartCDO< T >
, MiniSat::Clause
- d_dataSize
: CVC3::MemoryManagerChunks
- d_datatypes
: CVC3::TheoryDatatype
- d_decider
: SAT::DPLLT
, CVC3::SearchSat
, MiniSat::Solver
- d_decisionEngine
: CVC3::SearchEngineFast
, CVC3::SearchSimple
- d_default_params
: MiniSat::Solver
- d_delay
: CVC3::SmartCDO< T >::RefCDO< U >
- d_deleted
: CVC3::ClauseValue
, CVC3::VariableManager
- d_depth
: CVC3::ExprStream
- d_derivation
: MiniSat::Solver
- d_dir
: CVC3::ClauseValue
- d_disableGC
: CVC3::ExprManager
, CVC3::VariableManager
- d_diseq
: CVC3::TheoryArith3
, CVC3::TheoryArithNew
, CVC3::TheoryArithOld
- d_diseqIdx
: CVC3::TheoryArith3
, CVC3::TheoryArithNew
, CVC3::TheoryArithOld
- d_display
: CVC3::CLFlag
- d_dpllt
: CVC3::SearchSat
- d_dplltReady
: CVC3::SearchSat
- d_dpSplitters
: CVC3::SearchImplBase
- d_dump
: CVC3::Translator
, CVC3::VCL
- d_dumpExprs
: CVC3::Translator
- d_dumpFileOpen
: CVC3::Translator
- d_dynamicFlags
: CVC3::ExprValue
- d_e
: CVC3::Expr::iterator::Proxy
, LFSCProofExpr
- d_edges
: CVC3::TheoryArith3::VarOrderGraph
, CVC3::TheoryArithNew::VarOrderGraph
, CVC3::TheoryArithOld::VarOrderGraph
- d_elementType
: CVC3::Translator
- d_elist
: CVC3::NotifyList
- d_em
: CVC3::ExprManager::HashEV
, CVC3::ExprManagerNotifyObj
, CVC3::ExprStream
, CVC3::ExprValue
, CVC3::TheoremManager
, CVC3::TheoremProducer
, CVC3::Theory
, CVC3::Translator
, CVC3::VCL
- d_emptyClause
: MiniSat::Derivation
- d_emptyVec
: CVC3::ExprManager
- d_endChunk
: CVC3::MemoryManagerChunks
, CVC3::ContextMemoryManager
- d_endChunkStack
: CVC3::ContextMemoryManager
- d_enqueueCNFCache
: CVC3::SearchImplBase
- d_eq
: CVC3::TheoryBitvector
- d_eq_index
: CVC3::TheoryBitvector
- d_eq_list
: CVC3::TheoryQuant
- d_eq_pos
: CVC3::TheoryQuant
- d_eq_symm_str
: LFSCObj
- d_eq_trans_str
: LFSCObj
- d_eqNext
: CVC3::ExprValue
- d_eqPending
: CVC3::TheoryBitvector
- d_eqs
: CVC3::TheoryQuant
- d_eqs_pos
: CVC3::TheoryQuant
- d_eqsUpdate
: CVC3::TheoryQuant
- d_equal
: Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey >
- d_equalities
: CVC3::Translator
- d_expand
: CVC3::TheoremValue
- d_expandFlags
: CVC3::TheoremManager
- d_expensive_ccmin
: MiniSat::Solver
- d_expr
: CVC3::Expr
, CVC3::Op
, CVC3::Theorem
, CVC3::Type
, CVC3::VariableValue
, CVC3::DecisionEngineCaching::CacheEntry
, CVC3::DecisionEngineMBTF::CacheEntry
- d_expr_pol
: CVC3::CompleteInstPreProcessor
- d_expResult
: CVC3::Translator
- d_exprLastUpdatedPos
: CVC3::TheoryQuant
- d_exprs
: recCompleteInster
- d_exprSet
: CVC3::ExprManager
- d_exprTrans
: CVC3::TheoryCore
- d_extractKey
: Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey >
- d_factQueue
: CVC3::SearchEngineFast
- d_facts
: CVC3::TheoryDatatype
- d_false
: CVC3::ExprManager
- d_find
: CVC3::ExprValue
- d_first
: CVC3::CDMap< Key, Data, HashFcn >
, CVC3::CDMapOrdered< Key, Data >
- d_flag
: CVC3::ScopeWatcher
, CVC3::ExprValue
, CVC3::StatFlag
, CVC3::TheoremManager
, CVC3::TheoremValue
- d_flagCounter
: CVC3::ExprManager
- d_flags
: CVC3::CDFlags
, SAT::CNF_Manager
, CVC3::Statistics
, CVC3::TheoremManager
, CVC3::TheoryCore
, CVC3::VCL
, CVC3::CNF_TheoremProducer
- d_flip_inequality_str
: LFSCObj
- d_formula
: SAT::CNF_Formula_Impl
, SAT::CD_CNF_Formula
- d_formulas
: LFSCObj
- d_formulas_printed
: LFSCObj
- d_freeConstDB
: CVC3::TheoryArith3
, CVC3::TheoryArithNew
, CVC3::TheoryArithOld
- d_freeList
: CVC3::MemoryManagerChunks
- d_fullTrigs
: CVC3::TheoryQuant
- d_funApplications
: CVC3::TheoryUF
- d_funApplicationsIdx
: CVC3::TheoryUF
- d_gBindQueue
: CVC3::TheoryQuant
- d_getConstantStack
: CVC3::TheoryDatatype
- d_gfactLimit
: CVC3::TheoryQuant
- d_globals
: CVC3::TheoryCore
- d_gnd_cache
: CVC3::CompleteInstPreProcessor
- d_goal
: CVC3::SearchSimple
- d_graph
: CVC3::TheoryArith3
, CVC3::TheoryArithNew
, CVC3::TheoryArithOld
- d_grayShadowThres
: CVC3::TheoryArithOld
- d_gUnivQueue
: CVC3::TheoryQuant
- d_hash
: CVC3::ExprValue
, Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey >
- d_hash_table
: Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey >::iterator
, Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey >::const_iterator
- d_hasMoreBVs
: CVC3::TheoryQuant
- d_hasRt
: TReturn
- d_hasTriggers
: CVC3::TheoryQuant
- d_height
: CVC3::DecisionEngineCaching
, CVC3::DecisionEngineMBTF
- d_help
: CVC3::CLFlag
- d_hole
: CVC3::TheoremProducer
- d_id
: CVC3::Context
, MiniSat::Clause
- d_idCounter
: CVC3::ExprStream
- d_idx
: CVC3::ExprSkolem
, CVC3::VCL::UserAssertion
- d_idxUserAssump
: CVC3::SearchSat
- d_if_lift_rule_str
: LFSCObj
- d_iff_false_elim_str
: LFSCObj
- d_iff_false_str
: LFSCObj
- d_iff_mp_str
: LFSCObj
- d_iff_not_false_str
: LFSCObj
- d_iff_s
: LFSCObj
- d_iff_symm_str
: LFSCObj
- d_iff_trans_str
: LFSCObj
- d_iff_true_elim_str
: LFSCObj
- d_iff_true_str
: LFSCObj
- d_ifLiftOption
: CVC3::SearchImplBase
- d_ignoreCnfVarsOption
: CVC3::SearchImplBase
- d_imp_mp_str
: LFSCObj
- d_imp_s
: LFSCObj
- d_impl_mp_str
: LFSCObj
- d_impliedLiterals
: CVC3::TheoryCore
- d_impliedLiteralsIdx
: CVC3::TheoryCore
- d_implyEqualities_str
: LFSCObj
- d_implyNegatedInequality_str
: LFSCObj
- d_implyWeakerInequality_str
: LFSCObj
- d_implyWeakerInequalityDiffLogic_str
: LFSCObj
- d_inAddFact
: CVC3::TheoryCore
- d_inCheckSAT
: CVC3::SearchEngineFast
- d_inCheckSat
: CVC3::SearchSat
, CVC3::TheoryArray
- d_inCheckSATCore
: CVC3::TheoryCore
- d_incomplete
: CVC3::TheoryCore
- d_inconsistent
: CVC3::TheoryCore
- d_incThm
: CVC3::TheoryCore
- d_indent
: CVC3::ExprManager
, CVC3::ExprStream
- d_indentLast
: CVC3::ExprStream
- d_indentReg
: CVC3::ExprStream
- d_indentStack
: CVC3::ExprStream
- d_indentTransient
: CVC3::ExprManager
- d_index
: SAT::Var
, SAT::Lit
, CVC3::ExprManager
, CVC3::ExprValue
, CVC3::TheoryArray
, CVC3::DecisionEngineCaching
, CVC3::DecisionEngineMBTF
- d_index1
: CVC3::TheoryBitvector
- d_index2
: CVC3::TheoryBitvector
- d_indexChunkList
: CVC3::ContextMemoryManager
- d_indexChunkListStack
: CVC3::ContextMemoryManager
- d_indexExpr
: CVC3::TheoryQuant
- d_indexScore
: CVC3::TheoryQuant
- d_indexType
: CVC3::Translator
- d_inEnd
: CVC3::TheoryQuant
- d_ineq
: CVC3::TheoryArith3::Ineq
, CVC3::TheoryArithNew::Ineq
, CVC3::TheoryArithOld::Ineq
- d_inequalitiesLeftDB
: CVC3::TheoryArith3
, CVC3::TheoryArithNew
, CVC3::TheoryArithOld
- d_inequalitiesRightDB
: CVC3::TheoryArith3
, CVC3::TheoryArithNew
, CVC3::TheoryArithOld
- d_inferences
: MiniSat::Derivation
- d_inGC
: CVC3::ExprManager
- d_initMaxScore
: CVC3::TheoryQuant
- d_inMap
: CVC3::CDOmap< Key, Data, HashFcn >
, CVC3::CDOmapOrdered< Key, Data >
- d_inModelCreation
: CVC3::TheoryArith3
, CVC3::TheoryArithNew
, CVC3::TheoryArithOld
- d_inPP
: CVC3::TheoryCore
- d_inputClauses
: MiniSat::Derivation
- d_inputLang
: CVC3::ExprManager
- d_inRegisterAtom
: CVC3::TheoryCore
- d_inSearch
: MiniSat::Solver
- d_instCount
: CVC3::TheoryQuant
- d_instHistory
: CVC3::TheoryQuant
- d_instHistoryGlobal
: CVC3::TheoryQuant
- d_insts
: CVC3::TheoryQuant
- d_instThisRound
: CVC3::TheoryQuant
- d_int_const_eq_str
: LFSCObj
- d_intAssumptions
: CVC3::SearchSat
- d_intConstUsed
: CVC3::Translator
- d_intIntArray
: CVC3::Translator
- d_intIntRealArray
: CVC3::Translator
- d_intRealArray
: CVC3::Translator
- d_intType
: CVC3::TheoryArith
- d_intUsed
: CVC3::Translator
- d_inUpdate
: CVC3::TheoryCore
- d_is_macro_def
: CVC3::CompleteInstPreProcessor
- d_isAssump
: CVC3::TheoremValue
- d_isSubst
: CVC3::TheoremValue
- d_isTh
: LFSCPfLet
- d_it
: CVC3::Assumptions::iterator
, CVC3::CDMap< Key, Data, HashFcn >::iterator
, CVC3::CDMap< Key, Data, HashFcn >::orderedIterator
, CVC3::CDMapOrdered< Key, Data >::iterator
, CVC3::CDMapOrdered< Key, Data >::orderedIterator
, CVC3::Expr::iterator
, CVC3::ExprMap< Data >::const_iterator
, CVC3::ExprMap< Data >::iterator
, CVC3::ExprHashMap< Data >::const_iterator
, CVC3::ExprHashMap< Data >::iterator
- d_ite_s
: LFSCObj
- d_iteLiftArith
: CVC3::Translator
- d_iteMap
: SAT::CNF_Manager
- d_key
: CVC3::CDOmap< Key, Data, HashFcn >
, CVC3::CDOmapOrdered< Key, Data >
- d_kind
: CVC3::Op
, CVC3::ExprValue
- d_kindMap
: CVC3::ExprManager
- d_kindMapByName
: CVC3::ExprManager
- d_kinds
: CVC3::TheoryArith
- d_L
: TReturn
- d_L_used
: TReturn
- d_labels
: CVC3::TheoryDatatype
- d_lang
: CVC3::ExprStream
- d_langUsed
: CVC3::Translator
- d_lastArrayPos
: CVC3::TheoryQuant
- d_lastCheck
: CVC3::SearchSat
- d_lastClosure
: CVC3::VCL
- d_lastConflictClause
: CVC3::SearchEngineFast
- d_lastConflictScope
: CVC3::SearchEngineFast
- d_lastCounterExample
: CVC3::SearchImplBase
- d_lastDagSize
: CVC3::ExprStream
- d_lastEqsUpdatePos
: CVC3::TheoryQuant
- d_lastPartLevel
: CVC3::TheoryQuant
- d_lastPartPredsPos
: CVC3::TheoryQuant
- d_lastPartTermsPos
: CVC3::TheoryQuant
- d_lastPredsPos
: CVC3::TheoryQuant
- d_lastQuery
: CVC3::VCL
- d_lastQueryTCC
: CVC3::VCL
- d_lastRegisteredVar
: CVC3::SearchSat
- d_lastTermsPos
: CVC3::TheoryQuant
- d_lastUsefulGtermsPos
: CVC3::TheoryQuant
- d_lastValid
: CVC3::SearchImplBase
, CVC3::SearchSat
- d_learned_clause_str
: LFSCObj
- d_learnts
: MiniSat::Solver
- d_left
: SAT::SatProofNode
- d_lemmas
: CVC3::SearchSat
- d_lemmasNext
: CVC3::SearchSat
- d_lessThan_To_LE_rhs_rwr_str
: LFSCObj
- d_letPf
: LFSCPfLet
- d_letPfRpl
: LFSCPfLet
- d_level
: CVC3::Scope
, MiniSat::Solver
- d_lfsc_pf
: TReturn
- d_lhs
: CVC3::RWTheoremValue
- d_liftReadIte
: CVC3::TheoryArray
- d_lineWidth
: CVC3::ExprManager
, CVC3::ExprStream
- d_list
: CVC3::CDList< T >
- d_lit
: CVC3::SearchImplBase::Splitter
, CVC3::SearchSat::LitPriorityPair
, SAT::SatProofNode
- d_literals
: CVC3::ClauseValue
, CVC3::SearchEngineFast
- d_literalSet
: CVC3::SearchEngineFast
- d_litFlags
: CVC3::TheoremManager
- d_lits
: CVC3::Circuit
, SAT::Clause
, SAT::CNF_Formula_Impl
- d_litsAlive
: CVC3::SearchEngineFast
- d_litsByScores
: CVC3::SearchEngineFast
- d_litsMaxScorePos
: CVC3::SearchEngineFast
- d_litSortCount
: CVC3::SearchEngineFast
- d_macro_def
: CVC3::CompleteInstPreProcessor
- d_macro_lhs
: CVC3::CompleteInstPreProcessor
- d_macro_quant
: CVC3::CompleteInstPreProcessor
- d_manual_triggers
: CVC3::ExprClosure
- d_map
: CVC3::CDMap< Key, Data, HashFcn >
, CVC3::CDMapOrdered< Key, Data >
, CVC3::CLFlags
, CVC3::ExprMap< Data >
, CVC3::ExprHashMap< Data >
, CVC3::VCCmd
- d_master
: CVC3::ContextObjChain
- d_maxIL
: CVC3::TheoryQuant
- d_maxILReached
: CVC3::TheoryQuant
- d_maxInst
: CVC3::TheoryQuant
- d_maxLength
: CVC3::TheoryBitvector
- d_maxNaiveCall
: CVC3::TheoryQuant
- d_maxQuantInst
: CVC3::TheoryQuant
- d_minimizeClauses
: SAT::CNF_Manager
- d_minisat_proof_str
: LFSCObj
- d_minus_to_plus_str
: LFSCObj
- d_mm
: CVC3::ExprManager
, CVC3::TheoremManager
, CVC3::VariableManager
- d_mmFlag
: CVC3::ExprManager
- d_MMIndex
: CVC3::BVConstExpr
- d_mng
: SAT::DPLLTBasic
- d_mngStack
: SAT::DPLLTBasic
- d_modified
: CVC3::CLFlag
- d_msg
: CVC3::Exception
- d_mtrigs_bvorder
: CVC3::TheoryQuant
- d_mtrigs_inst
: CVC3::TheoryQuant
- d_mult_eqn_str
: LFSCObj
- d_mult_ineqn_str
: LFSCObj
- d_multitrigs_maps
: CVC3::TheoryQuant
- d_multTriggers
: CVC3::TheoryQuant
- d_multTrigs
: CVC3::TheoryQuant
- d_mybvs
: CVC3::TheoryQuant
- d_n
: CVC3::Rational
, CVC3::Unsigned
- d_name
: CVC3::Context
, CVC3::ExprVar
, CVC3::ExprSymbol
, CVC3::ExprBoundVar
, CVC3::SearchEngineFast
, CVC3::SearchSat
, CVC3::SearchSimple
, CVC3::Theory
- d_name_of_cur_ctxt
: CVC3::VCCmd
- d_neg
: CVC3::VariableValue
- d_negAdded
: CVC3::VariableValue
- d_negated_inequality_str
: LFSCObj
- d_negative
: CVC3::Literal
- d_negCount
: CVC3::VariableValue
- d_negCountPrev
: CVC3::VariableValue
- d_negScore
: CVC3::VariableValue
- d_negwp
: CVC3::VariableValue
- d_newDagMap
: CVC3::ExprStream
- d_newPPCache
: CVC3::ExprTransform
- d_next
: CVC3::CDOmap< Key, Data, HashFcn >
, CVC3::CDOmapOrdered< Key, Data >
, Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey >::BucketNode
- d_nextFree
: CVC3::MemoryManagerChunks
, CVC3::ContextMemoryManager
- d_nextFreeStack
: CVC3::ContextMemoryManager
- d_nextIdx
: CVC3::VCL
- d_nextImpliedLiteral
: CVC3::SearchSat
- d_nodag
: CVC3::ExprStream
- d_node
: Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey >::iterator
, Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey >::const_iterator
- d_nodes
: SAT::SatProof
- d_nonLiterals
: CVC3::SearchEngineFast
, CVC3::SearchSimple
- d_nonLiteralsSaved
: CVC3::SearchEngineFast
- d_nonlitQueryEnd
: CVC3::SearchEngineFast
- d_nonlitQueryStart
: CVC3::SearchEngineFast
- d_not_not_elim_str
: LFSCObj
- d_not_to_iff_str
: LFSCObj
- d_notifyEq
: CVC3::TheoryCore
- d_notifyList
: CVC3::ExprValue
- d_notifyObj
: CVC3::ExprManager
, CVC3::SmartCDO< T >::RefCDO< U >
, CVC3::TheoryCore
, CVC3::VariableManager
- d_notifyObjList
: CVC3::Context
- d_nullExpr
: CVC3::ExprManager
, SAT::CNF_Manager
- d_numVars
: SAT::CNF_Formula_Impl
, SAT::CD_CNF_Formula
- d_offset_multi_trig
: CVC3::TheoryQuant
- d_ok
: MiniSat::PushEntry
, MiniSat::Solver
- d_op
: LFSCLraPoly
, LFSCLraAxiom
, LFSCLraMulC
, LFSCLraContra
- d_op1
: LFSCLraAdd
, LFSCLraSub
- d_op2
: LFSCLraAdd
, LFSCLraSub
- d_opExpr
: CVC3::ExprApplyTmp
, CVC3::ExprApply
- d_optimized_subst_op_str
: LFSCObj
- d_or_final_s
: LFSCObj
- d_or_mid_s
: LFSCObj
- d_order
: MiniSat::Solver
- d_origFormulaOption
: CVC3::SearchImplBase
- d_os
: CVC3::ExprStream
, CVC3::Statistics
- d_osdump
: CVC3::Translator
- d_osdumpFile
: CVC3::Translator
- d_outputLang
: CVC3::ExprManager
- d_pair
: CVC3::ExprHashMap< Data >::const_iterator::Proxy
, CVC3::CDMap< Key, Data, HashFcn >::iterator::Proxy
, CVC3::CDMap< Key, Data, HashFcn >::orderedIterator::Proxy
, CVC3::CDMapOrdered< Key, Data >::iterator::Proxy
, CVC3::CDMapOrdered< Key, Data >::orderedIterator::Proxy
, CVC3::ExprMap< Data >::const_iterator::Proxy
, CVC3::ExprMap< Data >::iterator::Proxy
, CVC3::ExprHashMap< Data >::iterator::Proxy
- d_parent_list
: CVC3::TheoryQuant
- d_parseCache
: CVC3::TheoryCore
- d_parseCacheOther
: CVC3::TheoryCore
- d_parseCacheTop
: CVC3::TheoryCore
- d_parser
: CVC3::VCCmd
- d_partCalled
: CVC3::TheoryQuant
- d_partTriggers
: CVC3::TheoryQuant
- d_partTrigs
: CVC3::TheoryQuant
- d_pathLenghtThres
: CVC3::TheoryArithOld::DifferenceLogicGraph
- d_pending
: CVC3::ExprManager
- d_pendingClauses
: MiniSat::Solver
- d_pendingLemmas
: CVC3::SearchSat
- d_pendingLemmasNext
: CVC3::SearchSat
- d_pendingLemmasSize
: CVC3::SearchSat
- d_pendingScopes
: CVC3::SearchSat
- d_pf
: LFSCLraPoly
, LFSCClausify
, LFSCAssume
, LFSCLraMulC
, LFSCLraContra
, LFSCProofGeneric
- d_pf_expr
: LFSCObj
- d_pfOp
: CVC3::TheoremProducer
- d_plus_predicate_str
: LFSCObj
- d_pn
: LFSCObj
- d_pn_form
: LFSCObj
- d_pointerHash
: CVC3::ExprManager
- d_popLemmas
: MiniSat::Solver
- d_popRequests
: MiniSat::Solver
- d_postponed
: CVC3::ExprManager
- d_postponeGC
: CVC3::ExprManager
, CVC3::VariableManager
- d_predicates
: CVC3::TheoryCore
- d_prettyPrinter
: CVC3::ExprManager
- d_prev
: CVC3::CDOmap< Key, Data, HashFcn >
, CVC3::CDOmapOrdered< Key, Data >
- d_prevAStackSize
: SAT::DPLLTBasic
- d_prevScope
: CVC3::Scope
- d_prevStackSize
: SAT::DPLLTBasic
- d_print_map
: LFSCPrinter
- d_print_visited_map
: LFSCPrinter
- d_printDepth
: CVC3::ExprManager
- d_printer
: CVC3::TheoryCore
- d_printStats
: SAT::DPLLTBasic
, SAT::DPLLTMiniSat
- d_priority
: CVC3::SearchSat::LitPriorityPair
- d_prioritySet
: CVC3::SearchSat
- d_prioritySetBottomEntries
: CVC3::SearchSat
- d_prioritySetBottomEntriesSize
: CVC3::SearchSat
- d_prioritySetBottomEntriesSizeStack
: CVC3::SearchSat
- d_prioritySetEntries
: CVC3::SearchSat
- d_prioritySetEntriesSize
: CVC3::SearchSat
- d_prioritySetStart
: CVC3::SearchSat
- d_processIndex
: CVC3::TheoryDatatypeLazy
- d_processQueue
: CVC3::TheoryDatatypeLazy
- d_processQueueKind
: CVC3::TheoryDatatypeLazy
- d_proof
: SAT::DPLLTMiniSat
, CVC3::Proof
, SAT::SatProofNode
, CVC3::TheoremValue
- d_provesY
: TReturn
- d_pushes
: MiniSat::Solver
- d_pushID
: MiniSat::Clause
- d_pushIDs
: MiniSat::Solver
- d_pushLevel
: SAT::DPLLTBasic
- d_pushNegCache
: CVC3::TheoryBitvector
, CVC3::ExprTransform
- d_pv
: LFSCPfLet
- d_pvRpl
: LFSCPfLet
- d_qhead
: MiniSat::Solver
, MiniSat::PushEntry
- d_quant
: CVC3::ExprSkolem
- d_quant_equiv_map
: CVC3::CompleteInstPreProcessor
- d_quant_rules
: CVC3::CompleteInstPreProcessor
- d_quantLevel
: CVC3::TheoremValue
- d_queue
: CVC3::TheoryCore
- d_queueSE
: CVC3::TheoryCore
- d_r
: LFSCLraMulC
, CVC3::TheoryArith3::FreeConst
, CVC3::ExprRational
, CVC3::TheoryArithNew::FreeConst
, CVC3::TheoryArithOld::FreeConst
, LFSCLraAxiom
- d_rank
: CVC3::DecisionEngineCaching::CacheEntry
, CVC3::DecisionEngineMBTF::CacheEntry
- d_rawUnivs
: CVC3::TheoryQuant
- d_rawUnivsSavedPos
: CVC3::TheoryQuant
- d_reach
: CVC3::TheoryDatatype
- d_reads
: CVC3::TheoryArray
- d_ready
: SAT::DPLLTBasic
- d_readyPrev
: SAT::DPLLTBasic
- d_real2int
: CVC3::Translator
- d_real_shadow_eq_str
: LFSCObj
- d_real_shadow_str
: LFSCObj
- d_realType
: CVC3::TheoryArith
- d_realUsed
: CVC3::Translator
- d_reason
: SAT::Clause
, MiniSat::Solver
- d_rebuildCache
: CVC3::ExprManager
- d_ref
: CVC3::SmartCDO< T >::RefCDO< U >::RefNotifyObj
- d_refcount
: CVC3::ClauseValue
, CVC3::ExprValue
, CVC3::TheoremValue
- d_refCount
: CVC3::SmartCDO< T >::RefCDO< U >
- d_refcount
: CVC3::VariableValue
- d_refcountOwner
: CVC3::ClauseValue
- d_refl_str
: LFSCObj
- d_reflFlags
: CVC3::TheoremManager
- d_registeredVars
: MiniSat::Solver
- d_removedClauses
: MiniSat::Derivation
- d_renameThms
: CVC3::TheoryArray
- d_rep
: CVC3::ExprNode
- d_replaceITECache
: CVC3::SearchImplBase
- d_replaceSymbols
: CVC3::Translator
- d_resourceLimit
: CVC3::TheoryCore
- d_restore
: CVC3::ContextObjChain
, CVC3::ContextObj
- d_restoreChain
: CVC3::Scope
- d_restoreChainNext
: CVC3::ContextObjChain
- d_restoreChainPrev
: CVC3::ContextObjChain
- d_restorePoints
: CVC3::SearchEngineFast::ConflictClauseManager
- d_restorer
: CVC3::SearchSat
- d_result
: recCompleteInster
- d_rewrite_and_str
: LFSCObj
- d_rewrite_eq_refl_str
: LFSCObj
- d_rewrite_eq_symm_str
: LFSCObj
- d_rewrite_iff_str
: LFSCObj
- d_rewrite_iff_symm_str
: LFSCObj
- d_rewrite_implies_str
: LFSCObj
- d_rewrite_ite_same_str
: LFSCObj
- d_rewrite_not_false_str
: LFSCObj
- d_rewrite_not_not_str
: LFSCObj
- d_rewrite_not_true_str
: LFSCObj
- d_rewrite_or_str
: LFSCObj
- d_rhs
: CVC3::TheoryArithNew::Ineq
, CVC3::TheoryArithOld::Ineq
, CVC3::RWTheoremValue
, CVC3::TheoryArith3::Ineq
- d_right
: SAT::SatProofNode
- d_right_minus_left_str
: LFSCObj
- d_root
: SAT::SatProof
- d_rootLevel
: MiniSat::Solver
- d_rules
: CVC3::ExprTransform
, CVC3::SearchEngine
, CVC3::TheoremManager
, CVC3::TheoryArithNew
, CVC3::TheoryArithOld
, CVC3::TheoryArray
, CVC3::TheoryCore
, CVC3::TheoryDatatype
, CVC3::TheoryQuant
, CVC3::TheoryRecords
, CVC3::TheorySimulate
, CVC3::TheoryUF
, CVC3::VariableManager
, LFSCObj
, CVC3::TheoryArith3
, CVC3::TheoryBitvector
, SAT::CNF_Manager
- d_rwmm
: CVC3::TheoremManager
- d_same_head_expr
: CVC3::TheoryQuant
- d_sat
: CVC3::ClauseValue
- d_satisfied
: SAT::Clause
- d_savedCache
: CVC3::TheoryQuant
- d_savedMap
: CVC3::TheoryQuant
- d_savedTerms
: CVC3::TheoryQuant
- d_savedTermsPos
: CVC3::TheoryQuant
- d_scope
: CVC3::ClauseValue
, CVC3::ContextObj
, CVC3::VariableValue
- d_scopeLevel
: CVC3::TheoremValue
- d_score
: CVC3::VariableValue
- d_se
: CVC3::SearchEngineFast::ConflictClauseManager
, CVC3::VCL
, CVC3::CoreSatAPI_implBase
, CVC3::DecisionEngine
- d_selectorMap
: CVC3::TheoryDatatype
- d_sharedIdx1
: CVC3::TheoryArray
, CVC3::TheoryUF
- d_sharedIdx2
: CVC3::TheoryUF
, CVC3::TheoryArray
- d_sharedSubterms
: CVC3::TheoryBitvector
, CVC3::TheoryArray
- d_sharedSubtermsList
: CVC3::TheoryArray
, CVC3::TheoryBitvector
- d_sharedTerms
: CVC3::TheoryArithNew
, CVC3::TheoryArith3
, CVC3::TheoryArithOld
- d_sharedTermsList
: CVC3::TheoryArithOld
- d_sharedTermsMap
: CVC3::TheoryUF
- d_sharedVars
: CVC3::TheoryArithOld
, CVC3::TheoryArith3
, CVC3::TheoryArithNew
- d_sig
: CVC3::ExprNode
- d_simpCache
: CVC3::ExprValue
- d_simpCacheTag
: CVC3::ExprValue
- d_simpCacheTagCurrent
: CVC3::ExprManager
- d_simpDB_assigns
: MiniSat::Solver
- d_simpDB_props
: MiniSat::Solver
- d_simplifiedModelVars
: CVC3::TheoryCore
- d_simplifiedThm
: CVC3::SearchSimple
, CVC3::SearchEngineFast
- d_simplifiedThmQueue
: CVC3::TheoryQuant
- d_simplifyInPlace
: CVC3::TheoryCore
- d_simpRD_learnts
: MiniSat::Solver
- d_size
: CVC3::ExprValue
, Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey >
, CVC3::CDList< T >
- d_size_learnt
: MiniSat::Clause
- d_skolem_axioms
: CVC3::CommonTheoremProducer
- d_skolemized_thms
: CVC3::CommonTheoremProducer
- d_skolemVars
: CVC3::CommonTheoremProducer
- d_smartClauses
: CVC3::CNF_TheoremProducer
- d_smartSplits
: CVC3::TheoryDatatype
- d_solver
: CVC3::TheoryCore
- d_solvers
: SAT::DPLLTMiniSat
- d_source
: CVC3::Translator
- d_splitSign
: CVC3::TheoryArithOld
- d_splitterAsserted
: CVC3::TheoryDatatype
- d_splitterCount
: CVC3::SearchEngineFast
, CVC3::DecisionEngine
- d_splitters
: CVC3::DecisionEngine
, CVC3::TheoryDatatype
- d_splittersIndex
: CVC3::TheoryDatatype
- d_ss
: CVC3::SearchSatCNFCallback
, CVC3::SearchSatTheoryAPI
, CVC3::SearchSat::Restorer
, CVC3::SearchSatCoreSatAPI
, CVC3::SearchSatDecider
- d_stackLevel
: CVC3::VCL
- d_start
: MiniSat::Inference
- d_startLevel
: CVC3::DecisionEngineCaching
, CVC3::DecisionEngineMBTF
- d_statistics
: CVC3::TheoryCore
, SAT::CNF_Manager
, CVC3::VCL
- d_stats
: MiniSat::Solver
- d_status
: CVC3::Translator
- d_steps
: MiniSat::Inference
- d_str
: LFSCProofGeneric
, CVC3::ExprString
- d_strict
: CVC3::TheoryArithNew::FreeConst
, CVC3::TheoryArith3::FreeConst
, CVC3::TheoryArithOld::FreeConst
- d_subTermsMap
: CVC3::TheoryQuant
- d_t
: CVC3::Assumptions::iterator::Proxy
- d_table
: Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >
, Hash::hash_set< _Key, _HashFcn, _EqualKey >
- d_tcc
: CVC3::VCL::UserAssertion
- d_tccCache
: CVC3::TheoryCore
- d_tempBinds
: CVC3::TheoryQuant
- d_terms
: LFSCObj
, CVC3::TheoryCore
- d_termTheorems
: CVC3::TheoryCore
- d_testerMap
: CVC3::TheoryDatatype
- d_th_trans
: LFSCConvert
- d_th_trans_lam
: LFSCConvert
- d_th_trans_map
: LFSCConvert
- d_thead
: MiniSat::PushEntry
, MiniSat::Solver
- d_theorem
: MiniSat::Clause
, SAT::SatProofNode
- d_theorems
: CVC3::SearchSat
- d_theories
: CVC3::TheoryCore
, CVC3::VCL
- d_theoryAPI
: CVC3::SearchSat
, SAT::DPLLT
, MiniSat::Solver
- d_theoryArith
: CVC3::ExprTransform
, CVC3::Translator
, CVC3::ArithTheoremProducer3
, CVC3::VCL
, CVC3::ArithTheoremProducerOld
, CVC3::ArithTheoremProducer
- d_theoryArray
: CVC3::ArrayTheoremProducer
, CVC3::Translator
, CVC3::VCL
- d_theoryBitvector
: CVC3::Translator
, CVC3::VCL
, CVC3::BitvectorTheoremProducer
- d_theoryCore
: CVC3::CompleteInstPreProcessor
, CVC3::VCL
, CVC3::Theory
, CVC3::TheoryCore::CoreNotifyObj
, CVC3::Translator
- d_theoryDatatype
: CVC3::VCL
, CVC3::Translator
, CVC3::DatatypeTheoremProducer
- d_theoryExplanations
: MiniSat::Solver
- d_theoryMap
: CVC3::TheoryCore
- d_theoryQuant
: CVC3::Translator
, CVC3::QuantTheoremProducer
, CVC3::VCL
- d_theoryRecords
: CVC3::VCL
, CVC3::Translator
, CVC3::RecordsTheoremProducer
- d_theorySimulate
: CVC3::VCL
, CVC3::Translator
- d_theoryUF
: CVC3::Translator
, CVC3::UFTheoremProducer
, CVC3::VCL
- d_theoryUsed
: CVC3::Theory
- d_thm
: CVC3::VariableValue
, CVC3::TheoremValue
, CVC3::Theorem
, CVC3::Circuit
, CVC3::Theorem3
, CVC3::ClauseValue
, CVC3::VCL::UserAssertion
- d_thmCount
: CVC3::TheoryQuant
- d_timeBase
: CVC3::TheoryCore
- d_timeLimit
: CVC3::TheoryCore
- d_tlist
: CVC3::NotifyList
- d_tm
: CVC3::TheoremProducer
, CVC3::VCL
, CVC3::TheoremValue
, CVC3::ExprManager
, CVC3::TheoryCore
- d_tmpFile
: CVC3::Translator
- d_topLevel
: CVC3::DecisionEngineMBTF
, CVC3::DecisionEngineCaching
- d_topLevelLock
: CVC3::DecisionEngineMBTF
, CVC3::DecisionEngineCaching
- d_topScope
: CVC3::Context
- d_totalInstCount
: CVC3::TheoryQuant
- d_totalThmCount
: CVC3::TheoryQuant
- d_tp
: CVC3::CLFlag
- d_trail
: MiniSat::Solver
- d_trail_lim
: MiniSat::Solver
- d_trail_pos
: MiniSat::Solver
, lastToFirst_lt
- d_trailSize
: MiniSat::PushEntry
- d_trans2_found
: CVC3::TheoryQuant
- d_trans2_num
: CVC3::TheoryQuant
- d_trans_back
: CVC3::TheoryQuant
- d_trans_forw
: CVC3::TheoryQuant
- d_trans_found
: CVC3::TheoryQuant
- d_trans_num
: CVC3::TheoryQuant
- d_transClosureMap
: CVC3::TheoryUF
- d_translate
: CVC3::Translator
, CVC3::TheoryQuant
- d_translateQueueFlags
: SAT::CNF_Manager
- d_translateQueueThms
: SAT::CNF_Manager
- d_translateQueueVars
: SAT::CNF_Manager
- d_translator
: CVC3::TheoryCore
, CVC3::VCL
- d_transThm
: CVC3::TheoryQuant
- d_trash
: CVC3::CDMapOrdered< Key, Data >
, CVC3::CDMap< Key, Data, HashFcn >
- d_true
: CVC3::ExprManager
- d_trueInstCount
: CVC3::TheoryQuant
- d_trust
: CVC3::DecisionEngineCaching::CacheEntry
, CVC3::DecisionEngineMBTF::CacheEntry
- d_trusted
: LFSCObj
- d_type
: LFSCAssume
, CVC3::ExprValue
- d_typeComplete
: CVC3::TheoryDatatypeLazy
- d_typeComputer
: CVC3::ExprManager
, CVC3::TheoryCore
- d_typeExprMap
: CVC3::TheoryQuant
- d_typeFound
: CVC3::QuantTheoremProducer
- d_typeKinds
: CVC3::ExprManager
- d_UFIDL_ok
: CVC3::Translator
- d_uid
: CVC3::ExprBoundVar
, CVC3::ParserTemp
- d_uminus_to_mult_str
: LFSCObj
- d_unit
: SAT::Clause
- d_unitClauses
: MiniSat::Derivation
- d_unitConflictClauses
: CVC3::SearchEngineFast
- d_unitPropCount
: CVC3::SearchEngineFast
- d_univs
: CVC3::TheoryQuant
- d_univsContextPos
: CVC3::TheoryQuant
- d_univsPartSavedPos
: CVC3::TheoryQuant
- d_univsPosFull
: CVC3::TheoryQuant
- d_univsQueue
: CVC3::TheoryQuant
- d_univsSavedPos
: CVC3::TheoryQuant
- d_unknown
: CVC3::Translator
- d_unreportedLits
: CVC3::SearchEngineFast
- d_unreportedLitsHandled
: CVC3::SearchEngineFast
- d_update_data
: CVC3::TheoryCore
- d_update_thms
: CVC3::TheoryCore
- d_useCompleteInst
: CVC3::TheoryQuant
- d_useEnqueueFact
: CVC3::SearchEngineFast
- d_useEqu
: CVC3::TheoryQuant
- d_useExprScore
: CVC3::TheoryQuant
- d_usefulGterms
: CVC3::TheoryQuant
- d_useFullTrig
: CVC3::TheoryQuant
- d_useGFact
: CVC3::TheoryQuant
- d_useInstAll
: CVC3::TheoryQuant
- d_useInstGCache
: CVC3::TheoryQuant
- d_useInstLCache
: CVC3::TheoryQuant
- d_useInstThmCache
: CVC3::TheoryQuant
- d_useInstTrue
: CVC3::TheoryQuant
- d_useLazyInst
: CVC3::TheoryQuant
- d_useManTrig
: CVC3::TheoryQuant
- d_useMult
: CVC3::TheoryQuant
- d_useMultTrig
: CVC3::TheoryQuant
- d_useNaiveInst
: CVC3::TheoryQuant
- d_useNew
: CVC3::TheoryQuant
- d_useNewEqu
: CVC3::TheoryQuant
- d_usePart
: CVC3::TheoryQuant
- d_usePartTrig
: CVC3::TheoryQuant
- d_usePolarity
: CVC3::TheoryQuant
- d_usePullVar
: CVC3::TheoryQuant
- d_user_assumptions
: LFSCPrinter
- d_userAssertions
: CVC3::VCL
- d_userAssumptions
: CVC3::SearchSat
- d_useSemMatch
: CVC3::TheoryQuant
- d_useTrans
: CVC3::TheoryQuant
- d_useTrans2
: CVC3::TheoryQuant
- d_useTrigLoop
: CVC3::TheoryQuant
- d_val
: CVC3::Variable
, CVC3::VariableValue
- d_value
: Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey >::BucketNode
- d_var
: LFSCBoolRes
, LFSCLem
, CVC3::Literal
, LFSCClausify
, LFSCAssume
, LFSCLraPoly
- d_var_decay
: MiniSat::Solver
- d_var_inc
: MiniSat::Solver
- d_var_intro_str
: LFSCObj
- d_varAssignments
: CVC3::TheoryCore
- d_varInfo
: SAT::CNF_Manager
- d_varModelMap
: CVC3::TheoryCore
- d_vars
: CVC3::SearchSat
, CVC3::ExprClosure
, CVC3::TheoryCore
- d_varSet
: CVC3::VariableManager
- d_varsUndoList
: CVC3::SearchSat
- d_varsUndoListSize
: CVC3::SearchSat
- d_vc
: CVC3::VCCmd
, SAT::CNF_Manager
- d_vector
: CVC3::Assumptions
- d_visited
: CVC3::DecisionEngine
- d_vm
: CVC3::SearchImplBase
, CVC3::VariableValue
, CVC3::VariableManagerNotifyObj
- d_watches
: MiniSat::Solver
- d_withAssump
: CVC3::TheoremManager
- d_withIndentation
: CVC3::ExprManager
- d_withProof
: CVC3::TheoremManager
- d_wp
: CVC3::ClauseValue
, CVC3::VariableValue
- d_zeroVar
: CVC3::Translator
- dagFlag()
: CVC3::ExprStream
- dagPrinting()
: CVC3::ExprManager
- darkGrayShadow2ab()
: CVC3::ArithProofRules
, CVC3::ArithTheoremProducerOld
, CVC3::ArithTheoremProducer3
, CVC3::ArithTheoremProducer
- darkGrayShadow2ba()
: CVC3::ArithTheoremProducer3
, CVC3::ArithProofRules
, CVC3::ArithTheoremProducerOld
, CVC3::ArithTheoremProducer
- darkShadow()
: CVC3::TheoryArith
, CVC3::ArithTheoremProducer
, CVC3::ArithTheoremProducerOld
, CVC3::ArithTheoremProducer3
- Data
: Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey >
- data
: MiniSat::vec< T >
- data_const_iter
: Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey >
- data_iter
: Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey >
- data_type
: Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >
- dataType()
: CVC3::VCL
, CVC3::TheoryDatatype
, CVC3::ValidityChecker
, CVC3::VCL
, CVC3::TheoryDatatype
, CVC3::ValidityChecker
, CVC3::VCL
- datatypeConsExpr()
: CVC3::ValidityChecker
, CVC3::TheoryDatatype
, CVC3::VCL
- datatypeSelExpr()
: CVC3::ValidityChecker
, CVC3::VCL
, CVC3::TheoryDatatype
- datatypeTestExpr()
: CVC3::ValidityChecker
, CVC3::VCL
, CVC3::TheoryDatatype
- DatatypeTheoremProducer()
: CVC3::DatatypeTheoremProducer
- Datum
: MiniSat::vec< T >
- db_simpl
: MiniSat::SolverStats
- debug()
: CVC3::TheoryQuant
, MiniSat::SolverStats
- debug_conv
: LFSCObj
- debug_str
: LFSCProofGeneric
- debug_var
: LFSCObj
- decide_next_branch()
: CSolver
- Decider()
: SAT::DPLLT::Decider
- decider()
: SAT::DPLLT
- Decision()
: MiniSat::Clause
- decision_strategy
: CSolverParameters
- DecisionEngine
: CVC3::SearchImplBase
, CVC3::DecisionEngine
- DecisionEngineCaching()
: CVC3::DecisionEngineCaching
- DecisionEngineDFS()
: CVC3::DecisionEngineDFS
- DecisionEngineMBTF()
: CVC3::DecisionEngineMBTF
- decisionLevel()
: MiniSat::Solver
- decisions
: MiniSat::SolverStats
- decompose()
: CVC3::DatatypeProofRules
, CVC3::DatatypeTheoremProducer
- decRefcount()
: CVC3::ExprValue
- deduce()
: CSolver
- defaultDivideExpr
: CVC3::TheoryQuant
- defaultMinusExpr
: CVC3::TheoryQuant
- defaultMultExpr
: CVC3::TheoryQuant
- defaultPlusExpr
: CVC3::TheoryQuant
- defaultPowExpr
: CVC3::TheoryQuant
- defaultReadExpr
: CVC3::TheoryQuant
- defaultWriteExpr
: CVC3::TheoryQuant
- define_skolem_vars()
: LFSCObj
- del_clauses
: MiniSat::SolverStats
- del_lemmas
: MiniSat::SolverStats
- delete_unrelevant_clauses()
: CSolver
- DeleteClause()
: SatSolver
- deleted()
: CVC3::Clause
- deleteData()
: CVC3::MemoryManagerMalloc
, CVC3::MemoryManager
, CVC3::MemoryManagerChunks
, CVC3::ContextMemoryManager
- deleteLast()
: SAT::CD_CNF_Formula
, SAT::CNF_Formula_Impl
- deleteNotifyObj()
: CVC3::Context
- deleteParser()
: CVC3::Parser
- delNewTrigs()
: CVC3::TheoryQuant
- DependenciesMap
: CVC3::TheoryArithNew
- dependenciesMap
: CVC3::TheoryArithNew
- depth()
: CVC3::ExprStream
- Derivation()
: MiniSat::Derivation
- deriveClosure()
: CVC3::VCL
- deriveGomoryCut()
: CVC3::TheoryArithNew
- deriveTheorem()
: CVC3::Variable
, CVC3::Literal
- deriveThmRec()
: CVC3::Variable
- destroy()
: CVC3::VCL
- detail_dump_cl()
: CDatabase
- dfs()
: CVC3::TheoryArithNew::VarOrderGraph
, CVC3::TheoryArithOld::VarOrderGraph
, CVC3::TheoryArith3::VarOrderGraph
, CVC3::TheoryArithOld::VarOrderGraph
- diff_logic_size
: CVC3::TheoryArithOld
- DifferenceLogicGraph()
: CVC3::TheoryArithOld::DifferenceLogicGraph
- diffLogicGraph
: CVC3::TheoryArithOld
- diffLogicOnly
: CVC3::TheoryArithOld
- dir()
: CVC3::Clause
- direction()
: CLitPoolElement
- DisableClauseDeletion()
: Xchaff
, SatSolver
- diseqSplitAlready
: CVC3::TheoryArithOld
- diseqToIneq()
: CVC3::ArithTheoremProducer
, CVC3::ArithProofRules
, CVC3::ArithTheoremProducer3
, CVC3::ArithTheoremProducerOld
- display()
: CVC3::CLFlag
- distinctExpr()
: CVC3::ValidityChecker
, CVC3::VCL
- distributive_rule()
: CVC3::BitvectorTheoremProducer
, CVC3::BitvectorProofRules
- divideEqnNonConst()
: CVC3::ArithTheoremProducer
, CVC3::ArithTheoremProducerOld
, CVC3::ArithTheoremProducer3
, CVC3::ArithProofRules
- divideExpr()
: CVC3::ValidityChecker
, CVC3::VCL
- dlevel()
: CSolver
, CVariable
- do_bso()
: LFSCConvert
- doackermann()
: CVC3::ExprTransform
- dobryant()
: CVC3::ExprTransform
- done
: CVC3::ParserTemp
, CVC3::Parser
- dontBuffer
: CVC3::TheoryArithOld
- doPops()
: MiniSat::Solver
- doSolve()
: CVC3::TheoryArith3
, CVC3::TheoryArithNew
, CVC3::TheoryArithOld
- DPLLT()
: SAT::DPLLT
- DPLLTBasic()
: SAT::DPLLTBasic
- DPLLTMiniSat()
: SAT::DPLLTMiniSat
- dummyTheorem()
: CVC3::ArithTheoremProducerOld
, CVC3::DatatypeProofRules
, CVC3::ArithTheoremProducer3
, CVC3::ArithTheoremProducer
, CVC3::CoreTheoremProducer
, CVC3::DatatypeTheoremProducer
, CVC3::ArithProofRules
, CVC3::CoreProofRules
- dump()
: CSolver
, CLitPoolElement
, CVC3::Translator
, CClause
, CVariable
, CDatabase
- dump_assignment_stack()
: CSolver
- dumpAssertion()
: CVC3::Translator
- dumpQuery()
: CVC3::Translator
- dumpQueryResult()
: CVC3::Translator
- DynamicFlagsEnum
: CVC3::Expr
- dynTrig()
: CVC3::dynTrig