CVC3

Class List

Here are the classes, structs, unions and interfaces with brief descriptions:
Hash::_Identity< _Tp >
Hash::_Select1st< _Pair >
CVC3::ArithException
CVC3::ArithProofRules
CVC3::ArithTheoremProducer
CVC3::ArithTheoremProducer3
CVC3::ArithTheoremProducerOld
CVC3::ArrayProofRules
CVC3::ArrayTheoremProducer
CVC3::Assumptions
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< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey >::BucketNode
CVC3::BVConstExpr
CVC3::DecisionEngineCaching::CacheEntry
CVC3::DecisionEngineMBTF::CacheEntry
CClause
SAT::CD_CNF_Formula
CDatabase
CDatabaseStats
CVC3::CDFlags
CVC3::CDList< T >
CVC3::CDMap< Key, Data, HashFcn >
CVC3::CDMapData
CVC3::CDMapOrdered< Key, Data >
CVC3::CDMapOrderedData
CVC3::CDO< T >
CVC3::CDOmap< Key, Data, HashFcn >
CVC3::CDOmapOrdered< Key, Data >
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
CVC3::SearchEngineFast::ConflictClauseManager
CVC3::ExprMap< Data >::const_iterator
CVC3::ExprHashMap< Data >::const_iterator
Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey >::const_iterator
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
MiniSat::Derivation
CVC3::TheoryArithOld::DifferenceLogicGraph
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
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< Data >
CVC3::ExprManager
CVC3::ExprManagerNotifyObjNotifies ExprManager before and after each pop()
CVC3::ExprMap< Data >
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::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
CVC3::TheoryArithOld::GraphEdge
Hash::hash< _Key >
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< _Key, _Data, _HashFcn, _EqualKey >
Hash::hash_set< _Key, _HashFcn, _EqualKey >
Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey >
CVC3::ExprManager::HashEVPrivate class for d_exprSet
CVC3::VariableManager::HashLV
CVC3::ExprManager::HashStringPrivate class for hashing strings
CVC3::Translator::HashString
MiniSat::Heap< C >
CVC3::TheoryArith3::IneqPrivate class for an inequality in the Fourier-Motzkin database
CVC3::TheoryArithOld::IneqPrivate class for an inequality in the Fourier-Motzkin database
CVC3::TheoryArithNew::IneqPrivate class for an inequality in the Fourier-Motzkin database
MiniSat::Inference
CVC3::CDMapOrdered< Key, Data >::iterator
CVC3::Assumptions::iteratorIterator for the Assumptions: points to class Theorem
CVC3::ExprMap< Data >::iterator
CVC3::CDMap< Key, Data, HashFcn >::iterator
CVC3::ExprHashMap< Data >::iterator
CVC3::Expr::iterator
Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey >::iteratorInner classes
lastToFirst_lt
MiniSat::lbool
LFSCAssume
LFSCBoolRes
LFSCClausify
LFSCConvert
LFSCLem
LFSCLraAdd
LFSCLraAxiom
LFSCLraContra
LFSCLraMulC
LFSCLraPoly
LFSCLraSub
LFSCObj
LFSCPfLambda
LFSCPfLet
LFSCPfVar
LFSCPrinter
LFSCProof
LFSCProofExpr
LFSCProofGeneric
SatSolver::Lit
SAT::Lit
MiniSat::Lit
CVC3::Literal
CVC3::SearchSat::LitPriorityPairPair of Lit and priority of this Lit
CVC3::ltstr
CVC3::MemoryManager
CVC3::MemoryManagerChunks
CVC3::MemoryManagerMalloc
CVC3::MemoryTracker
MonomialLess
CVC3::TheoryQuant::multTrigsInfo
NamedExprValueNamedExprValue
CVC3::NotifyList
Obj
CVC3::Op
CVC3::CDMapOrdered< Key, Data >::orderedIterator
CVC3::CDMap< Key, Data, HashFcn >::orderedIterator
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
CVC3::Proof
CVC3::CDMapOrdered< Key, Data >::iterator::Proxy
CVC3::CDMapOrdered< Key, Data >::orderedIterator::Proxy
CVC3::ExprHashMap< Data >::iterator::Proxy
CVC3::ExprMap< Data >::const_iterator::Proxy
CVC3::CDMap< Key, Data, HashFcn >::iterator::Proxy
CVC3::CDMap< Key, Data, HashFcn >::orderedIterator::Proxy
CVC3::ExprHashMap< Data >::const_iterator::Proxy
CVC3::ExprMap< Data >::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
CVC3::Rational
recCompleteInster
CVC3::RecordsProofRules
CVC3::RecordsTheoremProducer
reduceDB_lt
CVC3::SmartCDO< T >::RefCDO< U >
CVC3::SmartCDO< T >::RefCDO< U >::RefNotifyObj
RefPtr< T >
CVC3::RegTheoremValue
CVC3::ResetException
CVC3::SearchSat::Restorer
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
CVC3::SimulateProofRules
CVC3::SimulateTheoremProducer
CVC3::SmartCDO< T >SmartCDO
CVC3::SmtlibException
MiniSat::Solver
MiniSat::SolverStats
CVC3::SoundException
CVC3::SearchImplBase::SplitterRepresentation of a DP-suggested splitter
CVC3::StatCounter
CVC3::StatFlag
MiniSat::STATIC_ASSERTION_FAILURE< true >
CVC3::Statistics
CVC3::StrPairLess< T >
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
unary_function
CVC3::Unsigned
CVC3::VCL::UserAssertionStructure to hold user assertions indexed by declaration order
CVC3::ValidityCheckerGeneric API for a validity checker
SatSolver::Var
SAT::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< T >
Xchaff