| ►NCVC3 | |
| CArithException | |
| CArithProofRules | |
| CArithTheoremProducer | |
| CArithTheoremProducer3 | |
| CArithTheoremProducerOld | |
| CArrayProofRules | |
| CArrayTheoremProducer | |
| ►CAssumptions | |
| ►Citerator | Iterator for the Assumptions: points to class Theorem |
| CProxy | Proxy class for postfix increment |
| CBitvectorException | |
| CBitvectorProofRules | |
| CBitvectorTheoremProducer | 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 |
| CBVConstExpr | An expression subclass for bitvector constants |
| CCDFlags | |
| CCDList | |
| ►CCDMap | |
| ►Citerator | |
| CProxy | |
| ►CorderedIterator | |
| CProxy | |
| CCDMapData | |
| ►CCDMapOrdered | |
| ►Citerator | |
| CProxy | |
| ►CorderedIterator | |
| CProxy | |
| CCDMapOrderedData | |
| CCDO | |
| CCDOmap | |
| CCDOmapOrdered | |
| CCircuit | |
| CClause | A class representing a CNF clause (a smart pointer) |
| CClauseOwner | Same as class Clause, but when destroyed, marks the clause as deleted |
| CClauseValue | |
| CCLException | |
| CCLFlag | |
| CCLFlags | |
| CCNF_Rules | API to the CNF proof rules |
| CCNF_TheoremProducer | |
| CCommonProofRules | |
| CCommonTheoremProducer | |
| CCompactClause | |
| CCompleteInstPreProcessor | |
| CContext | |
| CContextManager | Manager for multiple contexts. Also holds current context |
| CContextMemoryManager | ContextMemoryManager |
| CContextNotifyObj | |
| CContextObj | |
| CContextObjChain | |
| CCoreProofRules | |
| CCoreSatAPI_implBase | |
| CCoreTheoremProducer | |
| CDatatypeProofRules | |
| CDatatypeTheoremProducer | |
| CDebugException | |
| CDecisionEngine | |
| ►CDecisionEngineCaching | |
| CCacheEntry | |
| CDecisionEngineDFS | Decision Engine for use with the Search EngineAuthor: Clark Barrett |
| ►CDecisionEngineMBTF | |
| CCacheEntry | |
| CdynTrig | |
| CEvalException | |
| CException | |
| ►CExpr | Data structure of expressions in CVC3 |
| ►Citerator | |
| CProxy | Postfix increment requires a Proxy object to hold the intermediate value for dereferencing |
| CExprApply | |
| CExprApplyTmp | |
| CExprBoundVar | |
| CExprClosure | A "closure" expression which binds variables used in the "body". Used by LAMBDA and quantifiers |
| ►CExprHashMap | |
| ►Cconst_iterator | |
| CProxy | |
| ►Citerator | |
| CProxy | |
| ►CExprManager | Expression Manager |
| CEqEV | Private class for d_exprSet |
| CHashEV | Private class for d_exprSet |
| CHashString | Private class for hashing strings |
| CTypeComputer | Abstract class for computing expr type |
| CExprManagerNotifyObj | Notifies ExprManager before and after each pop() |
| ►CExprMap | |
| ►Cconst_iterator | |
| CProxy | |
| ►Citerator | |
| CProxy | |
| CExprNode | |
| CExprNodeTmp | |
| CExprRational | |
| CExprSkolem | |
| CExprStream | Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING! |
| CExprString | |
| CExprSymbol | |
| CExprTransform | |
| CExprValue | The base class for holding the actual data in expressions |
| CExprVar | |
| CLiteral | |
| Cltstr | |
| CMemoryManager | |
| CMemoryManagerChunks | |
| CMemoryManagerMalloc | |
| CMemoryTracker | |
| CNotifyList | |
| COp | |
| CParser | |
| CParserException | |
| CParserTemp | |
| CPrettyPrinter | Abstract API to a pretty-printer for Expr |
| CPrettyPrinterCore | Implementation of PrettyPrinter class |
| CProof | |
| CQuantProofRules | |
| CQuantTheoremProducer | |
| CRational | |
| CRecordsProofRules | |
| CRecordsTheoremProducer | |
| CRegTheoremValue | |
| CResetException | |
| CRWTheoremValue | |
| CScope | |
| CScopeWatcher | A class which sets a boolean value to true when created, and resets to false when deleted |
| CSearchEngine | API to to a generic proof search engine |
| ►CSearchEngineFast | Implementation of a faster search engine, using newer techniques |
| CConflictClauseManager | |
| CSearchEngineRules | API to the proof rules for the Search Engines |
| CSearchEngineTheoremProducer | |
| ►CSearchImplBase | API to to a generic proof search engine (a.k.a. SAT solver) |
| CSplitter | Representation of a DP-suggested splitter |
| ►CSearchSat | Search engine that connects to a generic SAT reasoning module |
| CLitPriorityPair | Pair of Lit and priority of this Lit |
| CRestorer | |
| CSearchSatCNFCallback | |
| CSearchSatCoreSatAPI | |
| CSearchSatDecider | |
| CSearchSatTheoryAPI | |
| CSearchSimple | Implementation of the simple search engine |
| CSimulateProofRules | |
| CSimulateTheoremProducer | |
| ►CSmartCDO | SmartCDO |
| ►CRefCDO | |
| CRefNotifyObj | |
| CSmtlibException | |
| CSoundException | |
| CStatCounter | |
| CStatFlag | |
| CStatistics | |
| CStrPairLess | |
| CTheorem | |
| CTheorem3 | Theorem3 |
| CTheoremLess | "Less" comparator for theorems by TheoremValue pointers |
| CTheoremManager | |
| CTheoremProducer | |
| CTheoremValue | |
| CTheory | Base class for theories |
| CTheoryArith | This theory handles basic linear arithmetic |
| ►CTheoryArith3 | |
| CFreeConst | Data class for the strongest free constant in separation inqualities |
| CIneq | Private class for an inequality in the Fourier-Motzkin database |
| CVarOrderGraph | |
| ►CTheoryArithNew | |
| CBoundInfo | |
| CEpsRational | |
| CExprBoundInfo | |
| CFreeConst | |
| CIneq | Private class for an inequality in the Fourier-Motzkin database |
| CVarOrderGraph | |
| ►CTheoryArithOld | |
| ►CDifferenceLogicGraph | |
| CEdgeInfo | |
| CEpsRational | |
| CFreeConst | Data class for the strongest free constant in separation inqualities |
| CGraphEdge | |
| CIneq | Private class for an inequality in the Fourier-Motzkin database |
| CVarOrderGraph | |
| CTheoryArray | This theory handles arrays |
| CTheoryBitvector | Theory of bitvectors of known length \ (operations include: @,[i:j],[i],+,.,BVAND,BVNEG) |
| ►CTheoryCore | This theory handles the built-in logical connectives plus equality. It also handles the registration and cooperation among all other theories |
| CCoreNotifyObj | |
| CCoreSatAPI | Interface class for callbacks to SAT from Core |
| CTheoryDatatype | This theory handles datatypes |
| CTheoryDatatypeLazy | This theory handles datatypes |
| ►CTheoryQuant | This theory handles quantifiers |
| CmultTrigsInfo | |
| CTypeComp | |
| CTheoryRecords | This theory handles records |
| CTheorySimulate | "Theory" of symbolic simulation |
| ►CTheoryUF | This theory handles uninterpreted functions |
| CTCMapPair | |
| ►CTranslator | |
| CHashString | |
| CTrigger | |
| CType | MS C++ specific settings |
| CTypecheckException | |
| CTypeComputerCore | |
| CUFProofRules | |
| CUFTheoremProducer | |
| CUnsigned | |
| CValidityChecker | Generic API for a validity checker |
| CVariable | |
| ►CVariableManager | |
| CEqLV | |
| CHashLV | |
| CVariableManagerNotifyObj | Notifies VariableManager before and after each pop() |
| CVariableValue | |
| CVCCmd | |
| ►CVCL | |
| CUserAssertion | Structure to hold user assertions indexed by declaration order |
| ►NHash | |
| C_Identity | |
| C_Select1st | |
| Chash | |
| Chash< char * > | |
| Chash< char > | |
| Chash< const char * > | |
| Chash< CVC3::Expr > | |
| Chash< CVC3::Theorem > | |
| Chash< int > | |
| Chash< long > | |
| Chash< short > | |
| Chash< signed char > | |
| Chash< std::string > | |
| Chash< unsigned char > | |
| Chash< unsigned int > | |
| Chash< unsigned long > | |
| Chash< unsigned short > | |
| Chash_map | |
| Chash_set | |
| ►Chash_table | |
| CBucketNode | |
| Cconst_iterator | |
| Citerator | Inner classes |
| ►NMiniSat | |
| CClause | |
| CDerivation | |
| CHeap | |
| CInference | |
| Clbool | |
| CLit | |
| CPushEntry | |
| CSearchParams | |
| CSolver | |
| CSolverStats | |
| CSTATIC_ASSERTION_FAILURE | |
| CSTATIC_ASSERTION_FAILURE< true > | |
| CVarOrder | |
| CVarOrder_lt | |
| Cvec | |
| ►NSAT | |
| CCD_CNF_Formula | |
| CClause | |
| CCNF_Formula | |
| CCNF_Formula_Impl | |
| ►CCNF_Manager | |
| CCNFCallback | Abstract class for callbacks |
| CVarinfo | Information kept for each CNF variable |
| ►CDPLLT | |
| CDecider | |
| CTheoryAPI | |
| CDPLLTBasic | |
| CDPLLTMiniSat | |
| CLit | |
| CSatProof | |
| CSatProofNode | |
| CVar | |
| ►Nstd | STL namespace |
| Cfdinbuf | |
| Cfdistream | |
| Cfdostream | |
| Cfdoutbuf | |
| CCClause | |
| CCDatabase | |
| CCDatabaseStats | |
| CCLitPoolElement | |
| CCSolver | |
| CCSolverParameters | |
| CCSolverStats | |
| CCVariable | |
| ClastToFirst_lt | |
| CLFSCAssume | |
| CLFSCBoolRes | |
| CLFSCClausify | |
| CLFSCConvert | |
| CLFSCLem | |
| CLFSCLraAdd | |
| CLFSCLraAxiom | |
| CLFSCLraContra | |
| CLFSCLraMulC | |
| CLFSCLraPoly | |
| CLFSCLraSub | |
| CLFSCObj | |
| CLFSCPfLambda | |
| CLFSCPfLet | |
| CLFSCPfVar | |
| CLFSCPrinter | |
| CLFSCProof | |
| CLFSCProofExpr | |
| CLFSCProofGeneric | |
| CMonomialLess | |
| CNamedExprValue | NamedExprValue |
| CObj | |
| Cpair_int_equal | |
| Cpair_int_hash_fun | |
| CrecCompleteInster | |
| CreduceDB_lt | |
| CRefPtr | |
| ►CSatSolver | |
| CClause | |
| CLit | |
| CVar | |
| CTReturn | |
| CXchaff | |
