►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 | |