| CVCL::_Hashtable_const_iterator< _Key, _Data > | |
| CVCL::_Hashtable_iterator< _Key, _Data > | |
| CVCL::ArithException | |
| CVCL::ArithProofRules | |
| CVCL::ArithTheoremProducer | |
| CVCL::ArrayProofRules | |
| CVCL::ArrayTheoremProducer | |
| CVCL::Assumptions | |
| CVCL::Assumptions::iterator | Iterator for the Assumptions: points to class Theorem |
| CVCL::Assumptions::iterator::Proxy | Proxy class for postfix increment |
| CVCL::AssumptionsValue | |
| CVCL::AVHash | |
| CVCL::BitvectorException | |
| CVCL::BitvectorProofRules | |
| CVCL::BitvectorTheoremProducer | This 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 |
| CVCL::BVConstExpr | |
| CClause | |
| SAT::CD_CNF_Formula | |
| CDatabase | |
| CDatabaseStats | |
| CVCL::CDFlags | |
| CVCL::CDList< T > | |
| CVCL::CDMap< Key, Data, HashFcn > | |
| CVCL::CDMap< Key, Data, HashFcn >::iterator | |
| CVCL::CDMap< Key, Data, HashFcn >::iterator::Proxy | |
| CVCL::CDMap< Key, Data, HashFcn >::orderedIterator | |
| CVCL::CDMap< Key, Data, HashFcn >::orderedIterator::Proxy | |
| CVCL::CDMapData | |
| CVCL::CDMapOrdered< Key, Data > | |
| CVCL::CDMapOrdered< Key, Data >::iterator | |
| CVCL::CDMapOrdered< Key, Data >::iterator::Proxy | |
| CVCL::CDMapOrdered< Key, Data >::orderedIterator | |
| CVCL::CDMapOrdered< Key, Data >::orderedIterator::Proxy | |
| CVCL::CDMapOrderedData | |
| CVCL::CDO< T > | |
| CVCL::CDOmap< Key, Data, HashFcn > | |
| CVCL::CDOmapOrdered< Key, Data > | |
| CVCL::Circuit | |
| CVCL::Clause | A class representing a CNF clause (a smart pointer) |
| SAT::Clause | |
| CVCL::ClauseOwner | Same as class Clause, but when destroyed, marks the clause as deleted |
| CVCL::ClauseValue | |
| CVCL::CLException | |
| CVCL::CLFlag | |
| CVCL::CLFlags | |
| CLitPoolElement | |
| SAT::CNF_Formula | |
| SAT::CNF_Formula_Impl | |
| SAT::CNF_Manager | |
| SAT::CNF_Manager::Varinfo | Information kept for each CNF variable |
| CVCL::CNF_Rules | API to the CNF proof rules |
| CVCL::CNF_TheoremProducer | |
| CVCL::CommonProofRules | |
| CVCL::CommonTheoremProducer | |
| CVCL::CompactClause | |
| CVCL::Context | |
| CVCL::ContextManager | Manager for multiple contexts. Also holds current context |
| CVCL::ContextNotifyObj | |
| CVCL::ContextObj | |
| CVCL::ContextObjChain | |
| CVCL::CoreProofRules | |
| CVCL::CoreSatAPI_implBase | |
| CVCL::CoreTheoremProducer | |
| CSolver | |
| CSolverParameters | |
| CSolverStats | |
| CVariable | |
| CVCL::DatatypeProofRules | |
| CVCL::DatatypeTheoremProducer | |
| CVCL::Debug | The heart of the Bug Extermination Kingdom |
| CVCL::Debug::stringHash | Private hasher class for strings |
| CVCL::DebugCounter | Integer counter for debugging purposes |
| CVCL::DebugException | Our exception to throw |
| CVCL::DebugFlag | Boolean flag (can only be true or false) |
| CVCL::DebugTime | |
| CVCL::DebugTimer | Time counter |
| CVCL::DecisionEngine | |
| CVCL::DecisionEngineCaching | |
| CVCL::DecisionEngineCaching::CacheEntry | |
| CVCL::DecisionEngineDFS | Decision Engine for use with the Search Engine
Author: Clark Barrett |
| CVCL::DecisionEngineMBTF | |
| CVCL::DecisionEngineMBTF::CacheEntry | |
| CVCL::Dict< _Key, _Data > | |
| CVCL::Dict_Entry< _Key, _Data > | |
| CVCL::Dict_Ptr< _Key, _Data > | |
| SAT::DPLLT | |
| SAT::DPLLT::Decider | |
| SAT::DPLLT::TheoryAPI | |
| SAT::DPLLTBasic | |
| CVCL::EvalException | |
| CVCL::Exception | |
| CVCL::Expr | Data structure of expressions in CVC Lite |
| CVCL::Expr::iterator | |
| CVCL::Expr::iterator::Proxy | Postfix increment requires a Proxy object to hold the intermediate value for dereferencing |
| CVCL::ExprApply | |
| CVCL::ExprBoundVar | |
| CVCL::ExprClosure | A "closure" expression which binds variables used in the "body". Used by LAMBDA and quantifiers |
| CVCL::ExprHashMap< Data > | |
| CVCL::ExprHashMap< Data >::iterator | |
| CVCL::ExprHashMap< Data >::iterator::Proxy | |
| CVCL::ExprManager | |
| CVCL::ExprManager::EqEV | Private class for d_exprSet |
| CVCL::ExprManager::HashEV | Private classe for d_exprSet |
| CVCL::ExprManager::HashString | Private class for hashing strings |
| CVCL::ExprManager::TypeComputer | Abstract class for computing expr type |
| CVCL::ExprManagerNotifyObj | Notifies ExprManager before and after each pop() |
| CVCL::ExprMap< Data > | |
| CVCL::ExprMap< Data >::iterator | |
| CVCL::ExprMap< Data >::iterator::Proxy | |
| CVCL::ExprNode | |
| CVCL::ExprRational | |
| CVCL::ExprSkolem | |
| CVCL::ExprStream | Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING! |
| CVCL::ExprString | |
| CVCL::ExprSymbol | |
| CVCL::ExprTransform | |
| CVCL::ExprValue | The base class for holding the actual data in expressions |
| CVCL::ExprVar | |
| std::fdinbuf | |
| std::fdistream | |
| std::fdostream | |
| std::fdoutbuf | |
| endif::hash< CVCL::Expr > | |
| endif::hash< std::string > | |
| CVCL::Hash_Entry< _Key, _Data > | |
| CVCL::Hash_Ptr< _Key, _Data > | |
| CVCL::Hash_Table< _Key, _Data > | |
| SAT::Lit | |
| CVCL::Literal | |
| CVCL::ltstr | |
| CVCL::MemoryManager | |
| CVCL::MemoryManagerChunks | |
| CVCL::MemoryManagerMalloc | |
| MonomialLess | |
| NamedExprValue | NamedExprValue |
| CVCL::NotifyList | |
| CVCL::Op | |
| pair_int_equal | |
| pair_int_hash_fun | |
| CVCL::Parser | |
| CVCL::ParserException | |
| CVCL::ParserTemp | |
| CVCL::PrettyPrinter | Abstract API to a pretty-printer for Expr |
| CVCL::PrettyPrinterCore | Implementation of PrettyPrinter class |
| CVCL::Proof | |
| CVCL::QuantProofRules | |
| CVCL::QuantTheoremProducer | |
| CVCL::Rational | |
| CVCL::Rational::Impl | |
| CVCL::Rational::Impl | Implementation of the forward-declared internal class |
| CVCL::Rational::Impl | |
| CVCL::RecordsProofRules | |
| CVCL::RecordsTheoremProducer | |
| CVCL::RefinedArithTheoremProducer | |
| CVCL::ReflexivityTheoremValue | A special subclass for reflexivity theorems: e = e and e <=> e |
| CVCL::RWTheoremValue | |
| SatSolver | |
| SatSolver::Clause | |
| SatSolver::Lit | |
| SatSolver::Var | |
| CVCL::Scope | |
| CVCL::ScopeWatcher | A class which sets a boolean value to true when created, and resets to false when deleted |
| CVCL::SearchEngine | API to to a generic proof search engine |
| CVCL::SearchEngineFast | Implementation of a faster search engine, using newer techniques |
| CVCL::SearchEngineFast::ConflictClauseManager | |
| CVCL::SearchEngineRules | API to the proof rules for the Search Engines |
| CVCL::SearchEngineTheoremProducer | |
| CVCL::SearchImplBase | API to to a generic proof search engine (a.k.a. SAT solver) |
| CVCL::SearchImplBase::Splitter | Representation of a DP-suggested splitter |
| CVCL::SearchSat | Search engine that connects to a generic SAT reasoning module |
| CVCL::SearchSat::Restorer | |
| CVCL::SearchSatCoreSatAPI | |
| CVCL::SearchSatDecider | |
| CVCL::SearchSatTheoryAPI | |
| CVCL::SearchSimple | Implementation of the simple search engine |
| CVCL::SimulateProofRules | |
| CVCL::SimulateTheoremProducer | |
| CVCL::SmartCDO< T > | SmartCDO |
| CVCL::SmartCDO< T >::RefCDO< U > | |
| CVCL::SmartCDO< T >::RefCDO< U >::RefNotifyObj | |
| CVCL::SmtlibException | |
| CVCL::SoundException | |
| CVCL::StatCounter | |
| CVCL::StatFlag | |
| CVCL::Statistics | |
| CVCL::StrPairLess< T > | |
| CVCL::SVC_API_impl | |
| CVCL::SVC_API_impl::varinfo | |
| CVCL::Theorem | |
| CVCL::Theorem3 | Theorem3 |
| CVCL::TheoremLess | "Less" comparator for theorems by TheoremValue pointers |
| CVCL::TheoremManager | |
| CVCL::TheoremProducer | |
| CVCL::TheoremValue | |
| CVCL::Theory | Base class for theories |
| CVCL::TheoryArith | This theory handles basic linear arithmetic |
| CVCL::TheoryArith::FreeConst | Data class for the strongest free constant in separation inqualities |
| CVCL::TheoryArith::Ineq | Private class for an inequality in the Fourier-Motzkin database |
| CVCL::TheoryArith::VarOrderGraph | |
| CVCL::TheoryArray | This theory handles arrays |
| CVCL::TheoryBitvector | Theory of bitvectors of known length \ (operations include: @,[i:j],[i],+,.,BVAND,BVNEG) |
| CVCL::TheoryCore | This theory handles the built-in logical connectives plus equality. It also handles the registration and cooperation among all other theories |
| CVCL::TheoryCore::CoreNotifyObj | |
| CVCL::TheoryCore::CoreSatAPI | |
| TheoryCore::CoreSatAPI | Interface class for callbacks to SAT from Core |
| CVCL::TheoryDatatype | This theory handles datatypes |
| CVCL::TheoryDatatypeLazy | This theory handles datatypes |
| CVCL::TheoryQuant | This theory handles quantifiers |
| CVCL::TheoryQuant::TypeComp | |
| CVCL::TheoryRecords | This theory handles records |
| CVCL::TheorySimulate | "Theory" of symbolic simulation |
| CVCL::TheoryUF | This theory handles uninterpreted functions |
| CVCL::TheoryUF::TCMapPair | |
| CVCL::Translator | |
| CVCL::Type | |
| CVCL::TypecheckException | |
| CVCL::TypeComputerCore | |
| CVCL::UFProofRules | |
| CVCL::UFTheoremProducer | |
| CVCL::ValidityChecker | Generic API for a validity checker
|
| SAT::Var | |
| CVCL::Variable | |
| CVCL::VariableManager | |
| CVCL::VariableManager::EqLV | |
| CVCL::VariableManager::HashLV | |
| CVCL::VariableManagerNotifyObj | Notifies VariableManager before and after each pop() |
| CVCL::VariableValue | |
| CVCL::VCCmd | |
| CVCL::VCL | |
| CVCL::VCL::UserAssertion | Structure to hold user assertions indexed by declaration order |
| Xchaff | |
