CVC3  2.4.1
Class List
Here are the classes, structs, unions and interfaces with brief descriptions:
Hash::_Identity
Hash::_Select1st
std::allocatorSTL class
CVC3::ArithException
CVC3::ArithProofRules
CVC3::ArithTheoremProducer
CVC3::ArithTheoremProducer3
CVC3::ArithTheoremProducerOld
CVC3::ArrayProofRules
CVC3::ArrayTheoremProducer
CVC3::Assumptions
std::auto_ptrSTL class
std::bad_allocSTL class
std::bad_castSTL class
std::bad_exceptionSTL class
std::bad_typeidSTL class
std::basic_fstreamSTL class
std::basic_ifstreamSTL class
std::basic_iosSTL class
std::basic_iostreamSTL class
std::basic_istreamSTL class
std::basic_istringstreamSTL class
std::basic_ofstreamSTL class
std::basic_ostreamSTL class
std::basic_ostringstreamSTL class
std::basic_stringSTL class
std::basic_stringstreamSTL class
std::bitsetSTL class
CVC3::BitvectorException
CVC3::BitvectorProofRules
CVC3::BitvectorTheoremProducerThis class implements proof rules for bitvector normalizers (concatenation normal form, bvplus normal form), bitblaster rules, other relevant rewrite rules for bv arithmetic and word-level operators
CVC3::TheoryArithNew::BoundInfo
Hash::hash_table::BucketNode
CVC3::BVConstExpr
CVC3::DecisionEngineCaching::CacheEntry
CVC3::DecisionEngineMBTF::CacheEntry
CClause
SAT::CD_CNF_Formula
CDatabase
CDatabaseStats
CVC3::CDFlags
CVC3::CDList
CVC3::CDMap
CVC3::CDMapData
CVC3::CDMapOrdered
CVC3::CDMapOrderedData
CVC3::CDO
CVC3::CDOmap
CVC3::CDOmapOrdered
CVC3::Circuit
SatSolver::Clause
CVC3::ClauseA class representing a CNF clause (a smart pointer)
SAT::Clause
MiniSat::Clause
CVC3::ClauseOwnerSame as class Clause, but when destroyed, marks the clause as deleted
CVC3::ClauseValue
CVC3::CLException
CVC3::CLFlag
CVC3::CLFlags
CLitPoolElement
SAT::CNF_Formula
SAT::CNF_Formula_Impl
SAT::CNF_Manager
CVC3::CNF_RulesAPI to the CNF proof rules
CVC3::CNF_TheoremProducer
SAT::CNF_Manager::CNFCallbackAbstract class for callbacks
CVC3::CommonProofRules
CVC3::CommonTheoremProducer
CVC3::CompactClause
CVC3::CompleteInstPreProcessor
std::complexSTL class
CVC3::SearchEngineFast::ConflictClauseManager
CVC3::ExprMap::const_iterator
CVC3::ExprHashMap::const_iterator
std::basic_string::const_iteratorSTL iterator class
std::string::const_iteratorSTL iterator class
std::wstring::const_iteratorSTL iterator class
std::deque::const_iteratorSTL iterator class
std::list::const_iteratorSTL iterator class
std::map::const_iteratorSTL iterator class
std::multimap::const_iteratorSTL iterator class
std::set::const_iteratorSTL iterator class
std::vector::const_iteratorSTL iterator class
std::multiset::const_iteratorSTL iterator class
Hash::hash_table::const_iterator
std::basic_string::const_reverse_iteratorSTL iterator class
std::string::const_reverse_iteratorSTL iterator class
std::wstring::const_reverse_iteratorSTL iterator class
std::deque::const_reverse_iteratorSTL iterator class
std::list::const_reverse_iteratorSTL iterator class
std::map::const_reverse_iteratorSTL iterator class
std::multimap::const_reverse_iteratorSTL iterator class
std::set::const_reverse_iteratorSTL iterator class
std::multiset::const_reverse_iteratorSTL iterator class
std::vector::const_reverse_iteratorSTL iterator class
CVC3::Context
CVC3::ContextManagerManager for multiple contexts. Also holds current context
CVC3::ContextMemoryManagerContextMemoryManager
CVC3::ContextNotifyObj
CVC3::ContextObj
CVC3::ContextObjChain
CVC3::TheoryCore::CoreNotifyObj
CVC3::CoreProofRules
CVC3::TheoryCore::CoreSatAPIInterface class for callbacks to SAT from Core
CVC3::CoreSatAPI_implBase
CVC3::CoreTheoremProducer
CSolver
CSolverParameters
CSolverStats
CVariable
CVC3::DatatypeProofRules
CVC3::DatatypeTheoremProducer
CVC3::DebugException
SAT::DPLLT::Decider
CVC3::DecisionEngine
CVC3::DecisionEngineCaching
CVC3::DecisionEngineDFSDecision Engine for use with the Search EngineAuthor: Clark Barrett
CVC3::DecisionEngineMBTF
std::dequeSTL class
MiniSat::Derivation
CVC3::TheoryArithOld::DifferenceLogicGraph
std::domain_errorSTL class
SAT::DPLLT
SAT::DPLLTBasic
SAT::DPLLTMiniSat
CVC3::dynTrig
CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo
CVC3::TheoryArithNew::EpsRational
CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational
CVC3::ExprManager::EqEVPrivate class for d_exprSet
CVC3::VariableManager::EqLV
CVC3::EvalException
std::exceptionSTL class
CVC3::Exception
CVC3::ExprData structure of expressions in CVC3
CVC3::ExprApply
CVC3::ExprApplyTmp
CVC3::TheoryArithNew::ExprBoundInfo
CVC3::ExprBoundVar
CVC3::ExprClosureA "closure" expression which binds variables used in the "body". Used by LAMBDA and quantifiers
CVC3::ExprHashMap
CVC3::ExprManager
CVC3::ExprManagerNotifyObjNotifies ExprManager before and after each pop()
CVC3::ExprMap
CVC3::ExprNode
CVC3::ExprNodeTmp
CVC3::ExprRational
CVC3::ExprSkolem
CVC3::ExprStreamPretty-printing output stream for Expr. READ THE DOCS BEFORE USING!
CVC3::ExprString
CVC3::ExprSymbol
CVC3::ExprTransform
CVC3::ExprValueThe base class for holding the actual data in expressions
CVC3::ExprVar
std::ios_base::failureSTL class
std::fdinbuf
std::fdistream
std::fdostream
std::fdoutbuf
CVC3::TheoryArith3::FreeConstData class for the strongest free constant in separation inqualities
CVC3::TheoryArithNew::FreeConst
CVC3::TheoryArithOld::FreeConstData class for the strongest free constant in separation inqualities
std::fstreamSTL class
CVC3::TheoryArithOld::GraphEdge
Hash::hash
Hash::hash< char * >
Hash::hash< char >
Hash::hash< const char * >
Hash::hash< CVC3::Expr >
Hash::hash< CVC3::Theorem >
Hash::hash< int >
Hash::hash< long >
Hash::hash< short >
Hash::hash< signed char >
Hash::hash< std::string >
Hash::hash< unsigned char >
Hash::hash< unsigned int >
Hash::hash< unsigned long >
Hash::hash< unsigned short >
Hash::hash_map
Hash::hash_set
Hash::hash_table
CVC3::ExprManager::HashEVPrivate class for d_exprSet
CVC3::VariableManager::HashLV
CVC3::ExprManager::HashStringPrivate class for hashing strings
CVC3::Translator::HashString
MiniSat::Heap
std::ifstreamSTL class
CVC3::TheoryArith3::IneqPrivate class for an inequality in the Fourier-Motzkin database
CVC3::TheoryArithNew::IneqPrivate class for an inequality in the Fourier-Motzkin database
CVC3::TheoryArithOld::IneqPrivate class for an inequality in the Fourier-Motzkin database
MiniSat::Inference
std::invalid_argumentSTL class
std::iosSTL class
std::ios_baseSTL class
std::istreamSTL class
std::istringstreamSTL class
CVC3::CDMapOrdered::iterator
CVC3::Assumptions::iteratorIterator for the Assumptions: points to class Theorem
CVC3::ExprMap::iterator
CVC3::CDMap::iterator
CVC3::ExprHashMap::iterator
std::basic_string::iteratorSTL iterator class
std::string::iteratorSTL iterator class
std::wstring::iteratorSTL iterator class
std::deque::iteratorSTL iterator class
std::list::iteratorSTL iterator class
std::map::iteratorSTL iterator class
std::multimap::iteratorSTL iterator class
std::set::iteratorSTL iterator class
std::multiset::iteratorSTL iterator class
std::vector::iteratorSTL iterator class
Hash::hash_table::iteratorInner classes
CVC3::Expr::iterator
lastToFirst_lt
MiniSat::lbool
std::length_errorSTL class
LFSCAssume
LFSCBoolRes
LFSCClausify
LFSCConvert
LFSCLem
LFSCLraAdd
LFSCLraAxiom
LFSCLraContra
LFSCLraMulC
LFSCLraPoly
LFSCLraSub
LFSCObj
LFSCPfLambda
LFSCPfLet
LFSCPfVar
LFSCPrinter
LFSCProof
LFSCProofExpr
LFSCProofGeneric
std::listSTL class
SatSolver::Lit
MiniSat::Lit
SAT::Lit
CVC3::Literal
CVC3::SearchSat::LitPriorityPairPair of Lit and priority of this Lit
std::logic_errorSTL class
CVC3::ltstr
std::mapSTL class
CVC3::MemoryManager
CVC3::MemoryManagerChunks
CVC3::MemoryManagerMalloc
CVC3::MemoryTracker
MonomialLess
std::multimapSTL class
std::multisetSTL class
CVC3::TheoryQuant::multTrigsInfo
NamedExprValueNamedExprValue
CVC3::NotifyList
Obj
std::ofstreamSTL class
CVC3::Op
CVC3::CDMapOrdered::orderedIterator
CVC3::CDMap::orderedIterator
std::ostreamSTL class
std::ostringstreamSTL class
std::out_of_rangeSTL class
std::overflow_errorSTL class
pair_int_equal
pair_int_hash_fun
CVC3::Parser
CVC3::ParserException
CVC3::ParserTemp
CVC3::PrettyPrinterAbstract API to a pretty-printer for Expr
CVC3::PrettyPrinterCoreImplementation of PrettyPrinter class
std::priority_queueSTL class
CVC3::Proof
CVC3::CDMap::iterator::Proxy
CVC3::CDMapOrdered::orderedIterator::Proxy
CVC3::ExprHashMap::iterator::Proxy
CVC3::CDMapOrdered::iterator::Proxy
CVC3::ExprMap::iterator::Proxy
CVC3::CDMap::orderedIterator::Proxy
CVC3::ExprMap::const_iterator::Proxy
CVC3::ExprHashMap::const_iterator::Proxy
CVC3::Assumptions::iterator::ProxyProxy class for postfix increment
CVC3::Expr::iterator::ProxyPostfix increment requires a Proxy object to hold the intermediate value for dereferencing
MiniSat::PushEntry
CVC3::QuantProofRules
CVC3::QuantTheoremProducer
std::queueSTL class
std::range_errorSTL class
CVC3::Rational
recCompleteInster
CVC3::RecordsProofRules
CVC3::RecordsTheoremProducer
reduceDB_lt
CVC3::SmartCDO::RefCDO
CVC3::SmartCDO::RefCDO::RefNotifyObj
RefPtr
CVC3::RegTheoremValue
CVC3::ResetException
CVC3::SearchSat::Restorer
std::string::reverse_iteratorSTL iterator class
std::basic_string::reverse_iteratorSTL iterator class
std::map::reverse_iteratorSTL iterator class
std::deque::reverse_iteratorSTL iterator class
std::list::reverse_iteratorSTL iterator class
std::multimap::reverse_iteratorSTL iterator class
std::set::reverse_iteratorSTL iterator class
std::multiset::reverse_iteratorSTL iterator class
std::vector::reverse_iteratorSTL iterator class
std::wstring::reverse_iteratorSTL iterator class
std::runtime_errorSTL class
CVC3::RWTheoremValue
SAT::SatProof
SAT::SatProofNode
SatSolver
CVC3::Scope
CVC3::ScopeWatcherA class which sets a boolean value to true when created, and resets to false when deleted
CVC3::SearchEngineAPI to to a generic proof search engine
CVC3::SearchEngineFastImplementation of a faster search engine, using newer techniques
CVC3::SearchEngineRulesAPI to the proof rules for the Search Engines
CVC3::SearchEngineTheoremProducer
CVC3::SearchImplBaseAPI to to a generic proof search engine (a.k.a. SAT solver)
MiniSat::SearchParams
CVC3::SearchSatSearch engine that connects to a generic SAT reasoning module
CVC3::SearchSatCNFCallback
CVC3::SearchSatCoreSatAPI
CVC3::SearchSatDecider
CVC3::SearchSatTheoryAPI
CVC3::SearchSimpleImplementation of the simple search engine
std::setSTL class
CVC3::SimulateProofRules
CVC3::SimulateTheoremProducer
CVC3::SmartCDOSmartCDO
CVC3::SmtlibException
MiniSat::Solver
MiniSat::SolverStats
CVC3::SoundException
CVC3::SearchImplBase::SplitterRepresentation of a DP-suggested splitter
std::stackSTL class
CVC3::StatCounter
CVC3::StatFlag
MiniSat::STATIC_ASSERTION_FAILURE< true >
CVC3::Statistics
std::stringSTL class
std::stringstreamSTL class
CVC3::StrPairLess
CVC3::TheoryUF::TCMapPair
CVC3::Theorem
CVC3::Theorem3Theorem3
CVC3::TheoremLess"Less" comparator for theorems by TheoremValue pointers
CVC3::TheoremManager
CVC3::TheoremProducer
CVC3::TheoremValue
CVC3::TheoryBase class for theories
SAT::DPLLT::TheoryAPI
CVC3::TheoryArithThis theory handles basic linear arithmetic
CVC3::TheoryArith3
CVC3::TheoryArithNew
CVC3::TheoryArithOld
CVC3::TheoryArrayThis theory handles arrays
CVC3::TheoryBitvectorTheory of bitvectors of known length \ (operations include: @,[i:j],[i],+,.,BVAND,BVNEG)
CVC3::TheoryCoreThis theory handles the built-in logical connectives plus equality. It also handles the registration and cooperation among all other theories
CVC3::TheoryDatatypeThis theory handles datatypes
CVC3::TheoryDatatypeLazyThis theory handles datatypes
CVC3::TheoryQuantThis theory handles quantifiers
CVC3::TheoryRecordsThis theory handles records
CVC3::TheorySimulate"Theory" of symbolic simulation
CVC3::TheoryUFThis theory handles uninterpreted functions
CVC3::Translator
TReturn
CVC3::Trigger
CVC3::TypeMS C++ specific settings
CVC3::TypecheckException
CVC3::TheoryQuant::TypeComp
CVC3::ExprManager::TypeComputerAbstract class for computing expr type
CVC3::TypeComputerCore
CVC3::UFProofRules
CVC3::UFTheoremProducer
std::underflow_errorSTL class
CVC3::Unsigned
CVC3::VCL::UserAssertionStructure to hold user assertions indexed by declaration order
std::valarraySTL class
CVC3::ValidityCheckerGeneric API for a validity checker
SAT::Var
SatSolver::Var
CVC3::Variable
CVC3::VariableManager
CVC3::VariableManagerNotifyObjNotifies VariableManager before and after each pop()
CVC3::VariableValue
SAT::CNF_Manager::VarinfoInformation kept for each CNF variable
MiniSat::VarOrder
MiniSat::VarOrder_lt
CVC3::TheoryArithOld::VarOrderGraph
CVC3::TheoryArithNew::VarOrderGraph
CVC3::TheoryArith3::VarOrderGraph
CVC3::VCCmd
CVC3::VCL
MiniSat::vec
std::vectorSTL class
std::wfstreamSTL class
std::wifstreamSTL class
std::wiosSTL class
std::wistreamSTL class
std::wistringstreamSTL class
std::wofstreamSTL class
std::wostreamSTL class
std::wostringstreamSTL class
std::wstringSTL class
std::wstringstreamSTL class
Xchaff