| CVCL::_Hashtable_const_iterator< _Key, _Data > | |
| CVCL::_Hashtable_iterator< _Key, _Data > | |
| args | |
| 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::BoolVarExprValue | Boolean variables are treated as 0-ary predicates |
| CVCL::BVConstExpr | |
| CVCL::BVParameterExpr | |
| CVCL::BVPlusExpr | |
| CVCL::BVTypePredExpr | BVTypePredExpr |
| 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) |
| CVCL::ClauseOwner | Same as class Clause, but when destroyed, marks the clause as deleted |
| CVCL::ClauseValue | |
| CVCL::CLException | |
| CVCL::CLFlag | |
| CVCL::CLFlags | |
| CVCL::CNF | |
| CVCL::CommonProofRules | Commonly used proof rules (reflexivity, symmetry, transitivity, substitutivity, etc.) |
| CVCL::CommonTheoremProducer | |
| CVCL::CompactClause | |
| CVCL::Context | |
| CVCL::ContextManager | Manager for multiple contexts. Also holds current context |
| CVCL::ContextNotifyObj | |
| CVCL::ContextObj | |
| CVCL::ContextObjChain | |
| 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 |
| CVCL::DecisionEngineMBTF | |
| CVCL::DecisionEngineMBTF::CacheEntry | |
| CVCL::Dict< _Key, _Data > | |
| CVCL::Dict_Entry< _Key, _Data > | |
| CVCL::Dict_Ptr< _Key, _Data > | |
| 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::ExprCC | |
| CVCL::ExprClosure | A "closure" expression which binds variables used in the "body". Used by LAMBDA and quantifiers |
| CVCL::ExprGeneric | ExprGeneric |
| CVCL::ExprGrayShadow | Subclass of ExprValue for gray shadow expressions |
| 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::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::ExprRecord | Record literal: contains list of field names as an attribute |
| CVCL::ExprSkolem | |
| CVCL::ExprStream | Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING! |
| CVCL::ExprString | |
| 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 > | |
| CVCL::Literal | |
| CVCL::ltstr | |
| CVCL::MemoryManager | |
| CVCL::MemoryManagerChunks | |
| CVCL::MemoryManagerMalloc | |
| MonomialLess | |
| CVCL::NamedExprValue | NamedExprValue |
| CVCL::NotifyList | |
| CVCL::Op | |
| 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 | Implementation of the forward-declared internal class |
| CVCL::RecField | Record field access (select, update) |
| CVCL::RecordsProofRules | |
| CVCL::RecordsTheoremProducer | |
| CVCL::RefinedArithTheoremProducer | |
| CVCL::ReflexivityTheoremValue | A special subclass for reflexivity theorems: e = e and e <=> e |
| CVCL::RWTheoremValue | |
| 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 (a.k.a. SAT solver) |
| CVCL::SearchEngine::SearchNotifyObj | |
| CVCL::SearchEngine::Splitter | Representation of a DP-suggested splitter |
| 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::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 | |
| StrPairLess< T > | Comparison of string/Expr pairs for sorting |
| 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::TheoryDatatype | 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::TupleIndex | Tuple element access (select, update) |
| CVCL::Type | |
| CVCL::TypecheckException | |
| CVCL::UFProofRules | |
| CVCL::UFTheoremProducer | |
| CVCL::ValidityChecker | Generic API for a validity checker |
| 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 |
