Data Structures

Here are the data structures with brief descriptions:

[detail level 1234]

►N__gnu_cxx
Chash
►NCVC3
CCLFlag
CCLFlags
CExpr	Expr class for CVC3 compatibility layer
CExprHashMap
CExprManager
CExprMap
CProof
CTheorem
CType
CValidityChecker	CVC3 API (compatibility layer for CVC4)
►NCVC4
►Ncontext
CCDInsertHashMap
CCDTrailHashMap
►Nexpr
►Npickle
CMapPickler
CPickle
CPickler
CPicklingException
►CExprDag	IOStream manipulator to print expressions as a dag (or not)
CScope	Set the dag state on the output stream for the current stack scope
►CExprPrintTypes	IOStream manipulator to print type ascriptions or not
CScope	Set the print-types state on the output stream for the current stack scope
►CExprSetDepth	IOStream manipulator to set the maximum depth of Exprs when pretty-printing
CScope	Set the expression depth on the output stream for the current stack scope
►CExprSetLanguage	IOStream manipulator to set the output language for Exprs
CScope	Set a language on the output stream for the current stack scope
►Nkind
CKindHashFunction
►Nlanguage
►Noptions
CabstractValues__option_t
CaggressiveMiniscopeQuant__option_t
CarithDioSolver__option_t
CarithErrorSelectionRule__option_t
CarithHeuristicPivots__option_t
CarithMLTrick__option_t
CarithMLTrickSubstitutions__option_t
CarithPivotThreshold__option_t
CarithPropagateMaxLength__option_t
CarithPropagationMode__option_t
CarithPropAsLemmaLength__option_t
CarithRewriteEq__option_t
CarithSimplexCheckPeriod__option_t
CarithStandardCheckVarOrderPivots__option_t
CarithUnateLemmaMode__option_t
CarraysEagerIndexSplitting__option_t
CarraysEagerLemmas__option_t
CarraysLazyRIntro1__option_t
CarraysModelBased__option_t
CarraysOptimizeLinear__option_t
CaxiomInstMode__option_t
CbiasedITERemoval__option_t
Cbinary_name__option_t
CbitblastMode__option_t
CbitvectorAig__option_t
CbitvectorAigSimplifications__option_t
CbitvectorAlgebraicBudget__option_t
CbitvectorAlgebraicSolver__option_t
CbitvectorDivByZeroConst__option_t
CbitvectorEqualitySlicer__option_t
CbitvectorEqualitySolver__option_t
CbitvectorInequalitySolver__option_t
CbitvectorPropagate__option_t
CbitvectorQuickXplain__option_t
CbitvectorToBool__option_t
CbooleanTermConversionMode__option_t
CbvAbstraction__option_t
CbvEagerExplanations__option_t
CbvIntroducePow2__option_t
CbvNumFunc__option_t
Ccbqi__option_t
CcheckModels__option_t
CcheckProofs__option_t
CclauseSplit__option_t
CcnfQuant__option_t
CcollectPivots__option_t
CcompressItes__option_t
CcondenseFunctionValues__option_t
CcontinuedExecution__option_t
CcumulativeMillisecondLimit__option_t
CcumulativeResourceLimit__option_t
CdecisionMode__option_t
CdecisionRandomWeight__option_t
CdecisionStopOnly__option_t
CdecisionThreshold__option_t
CdecisionUseWeight__option_t
CdecisionWeightInternal__option_t
CdefaultDagThresh__option_t
CdefaultExprDepth__option_t
CdioRepeat__option_t
CdioSolverTurns__option_t
CdoCutAllBounded__option_t
CdoITESimp__option_t
CdoITESimpOnRepeat__option_t
CdoStaticLearning__option_t
CdtForceAssignment__option_t
CdtRewriteErrorSel__option_t
CdtStcInduction__option_t
CdumpInstantiations__option_t
CdumpModels__option_t
CdumpProofs__option_t
CeagerInstQuant__option_t
CearlyExit__option_t
CearlyTypeChecking__option_t
Cerr__option_t
CexpandDefinitions__option_t
CexportDioDecompositions__option_t
CfallbackSequential__option_t
CfilesystemAccess__option_t
CfiniteModelFind__option_t
CflipDecision__option_t
CfmfBoundInt__option_t
CfmfBoundIntLazy__option_t
CfmfFmcSimple__option_t
CfmfFreshDistConst__option_t
CfmfInstEngine__option_t
CfmfInstGen__option_t
CfmfInstGenOneQuantPerRound__option_t
CfmfOneInstPerRound__option_t
CfmfOneQuantPerRound__option_t
CfoPropQuant__option_t
CforceLogic__option_t
CforceNoLimitCpuWhileDump__option_t
CfullSaturateQuant__option_t
ChavePenalties__option_t
Chelp__option_t
CidlRewriteEq__option_t
Cin__option_t
CincrementalParallel__option_t
CincrementalSolving__option_t
CinputLanguage__option_t
CinstFormatMode__option_t
CinstMaxLevel__option_t
CinstWhenMode__option_t
Cinteractive__option_t
CinteractivePrompt__option_t
CinternalReps__option_t
ClanguageHelp__option_t
ClemmaInputChannel__option_t
ClemmaOutputChannel__option_t
ClemmaRejectCutSize__option_t
CliteralMatchMode__option_t
CmacrosQuant__option_t
CmaxApproxDepth__option_t
CmaxCutsInContext__option_t
CmaxReplayTree__option_t
CmbqiMode__option_t
CmemoryMap__option_t
CminisatDumpDimacs__option_t
CminisatUseElim__option_t
CminiscopeQuant__option_t
CminiscopeQuantFreeVar__option_t
CmodelFormatMode__option_t
CmodelUninterpDtEnum__option_t
CnewProp__option_t
CnnfQuant__option_t
Cout__option_t
CoutputLanguage__option_t
CparseOnly__option_t
CpbRewrites__option_t
CpbRewriteThreshold__option_t
CperCallMillisecondLimit__option_t
CperCallResourceLimit__option_t
CppAssertMaxSubSize__option_t
CprenexQuant__option_t
CpreprocessOnly__option_t
CpreSkolemQuant__option_t
CprintSuccess__option_t
CproduceAssignments__option_t
CproduceModels__option_t
Cproof__option_t
CqcfMode__option_t
CqcfTConstraint__option_t
CqcfWhenMode__option_t
CquantConflictFind__option_t
CquantRewriteRules__option_t
CrecurseCbqi__option_t
CregisterQuantBodyTerms__option_t
CrelationalTriggers__option_t
CrelevantTriggers__option_t
CrepeatSimp__option_t
CreplayEarlyCloseDepths__option_t
CreplayFailureLemma__option_t
CreplayFailurePenalty__option_t
CreplayFilename__option_t
CreplayLog__option_t
CreplayNumericFailurePenalty__option_t
CreplayRejectCutSize__option_t
CreplayStream__option_t
CrestrictedPivots__option_t
CrevertArithModels__option_t
CrewriteApplyToConst__option_t
CrewriteDivk__option_t
CrrOneInstPerRound__option_t
CrrTurns__option_t
Csat_refine_conflicts__option_t
CsatClauseDecay__option_t
CsatRandomFreq__option_t
CsatRandomSeed__option_t
CsatRestartFirst__option_t
CsatRestartInc__option_t
CsatVarDecay__option_t
CsegvSpin__option_t
CsemanticChecks__option_t
CsetsEagerLemmas__option_t
CsetsPropagate__option_t
CsharingFilterByLength__option_t
CsimpleIteLiftQuant__option_t
CsimplificationMode__option_t
CsimplifyWithCareEnabled__option_t
CskolemizeArguments__option_t
CsmartTriggers__option_t
CsoiApproxMajorFailure__option_t
CsoiApproxMajorFailurePen__option_t
CsoiApproxMinorFailure__option_t
CsoiApproxMinorFailurePen__option_t
CsoiQuickExplain__option_t
CsortInference__option_t
Cstatistics__option_t
CstatsEveryQuery__option_t
CstatsHideZeros__option_t
CstrictParsing__option_t
CstringCharCardinality__option_t
CstringEIT__option_t
CstringExp__option_t
CstringFMF__option_t
CstringLB__option_t
CstringOpt1__option_t
CstringOpt2__option_t
CtearDownIncremental__option_t
CtheoryAlternates__option_t
CtheoryOfMode__option_t
Cthread_id__option_t
CthreadArgv__option_t
Cthreads__option_t
CthreadStackSize__option_t
CtrySolveIntStandardEffort__option_t
CtypeChecking__option_t
CufssAbortCardinality__option_t
CufssCliqueSplits__option_t
CufssDiseqPropagation__option_t
CufssEagerSplits__option_t
CufssExplainedCliques__option_t
CufssFairness__option_t
CufssMinimalModel__option_t
CufssRegions__option_t
CufssSimpleCliques__option_t
CufssSymBreak__option_t
CufssTotality__option_t
CufssTotalityLimited__option_t
CufssTotalitySymBreak__option_t
CufSymmetryBreaker__option_t
CunconstrainedSimp__option_t
CunsatCores__option_t
CuseApprox__option_t
CuseFC__option_t
CuserPatternsQuant__option_t
CuseSOI__option_t
CvarElimQuant__option_t
Cverbosity__option_t
Cversion__option_t
CwaitToJoin__option_t
CzombieHuntThreshold__option_t
►Nparser
CInput	An input to be parsed
CInputStream	Wrapper around an input stream
CInputStreamException
►CParser	This class encapsulates all of the state of a parser, including the name of the file, line number and column information, and in-scope declarations
CExprStream	An expression stream interface for a parser
CParserBuilder	A builder for input language parsers
CParserEndOfFileException
CParserException
►Nprop
CSatSolverFactory
►Nstrings
CStringHashFunction
CAbstractValue
CAbstractValueHashFunction	Hash function for the BitVector constants
CArrayStoreAll
CArrayStoreAllHashFunction	Hash function for the ArrayStoreAll constants
CArrayType	Class encapsulating an array type
CAscriptionType	A class used to parameterize a type ascription
CAscriptionTypeHashFunction	A hash function for type ascription operators
CAssertCommand
CBitVector
CBitVectorBitOf	The structure representing the extraction of one Boolean bit
CBitVectorBitOfHashFunction	Hash function for the BitVectorBitOf objects
CBitVectorExtract	The structure representing the extraction operation for bit-vectors
CBitVectorExtractHashFunction	Hash function for the BitVectorExtract objects
CBitVectorHashFunction	Hash function for the BitVector constants
CBitVectorRepeat
CBitVectorRotateLeft
CBitVectorRotateRight
CBitVectorSignExtend
CBitVectorSize
CBitVectorType	Class encapsulating the bit-vector type
CBitVectorZeroExtend
CBooleanType	Singleton class encapsulating the Boolean type
CBoolHashFunction
CCardinality	A simple representation of a cardinality
CCardinalityBeth	Representation for a Beth number, used only to construct Cardinality objects
CCardinalityUnknown	Representation for an unknown cardinality
CChain	A class to represent a chained, built-in operator
CChainHashFunction
CCheckSatCommand
►CCommand
CExportTransformer
CCommandFailure
►CCommandPrintSuccess	IOStream manipulator to print success messages or not
CScope	Set the print-success state on the output stream for the current stack scope
CCommandSequence
CCommandStatus
CCommandSuccess
CCommandUnsupported
CCommentCommand
CConfiguration	Represents the (static) configuration of CVC4
CConstructorType	Class encapsulating the constructor type
CDatatype	The representation of an inductive datatype
CDatatypeConstructor	A constructor for a Datatype
CDatatypeConstructorArg	A Datatype constructor argument (i.e., a Datatype field)
CDatatypeConstructorArgIterator
CDatatypeConstructorIterator
CDatatypeDeclarationCommand
CDatatypeHashFunction	A hash function for Datatypes
CDatatypeResolutionException	An exception that is thrown when a datatype resolution fails
CDatatypeSelfType	A holder type (used in calls to DatatypeConstructor::addArg()) to allow a Datatype to refer to itself
CDatatypeType	Class encapsulating the datatype type
CDatatypeUnresolvedType	An unresolved type (used in calls to DatatypeConstructor::addArg()) to allow a Datatype to refer to itself or to other mutually-recursive Datatypes
CDeclarationDefinitionCommand
CDeclarationSequence
CDeclareFunctionCommand
CDeclareTypeCommand
CDefineFunctionCommand
CDefineNamedFunctionCommand	This differs from DefineFunctionCommand only in that it instructs the SmtEngine to "remember" this function for later retrieval with getAssignment()
CDefineTypeCommand
CDivisible	The structure representing the divisibility-by-k predicate
CDivisibleHashFunction	Hash function for the Divisible objects
CEchoCommand
CEmptyCommand	EmptyCommands are the residue of a command after the parser handles them (and there's nothing left to do)
CEmptySet
CEmptySetHashFunction
CException
CExpandDefinitionsCommand
CExportUnsupportedException	Exception thrown in case of failure to export
►CExpr	Class encapsulating CVC4 expressions and methods for constructing new expressions
Cconst_iterator	Iterator type for the children of an Expr
CExprHashFunction
CExprManager
CExprManagerMapCollection
CExprStream	A pure-virtual stream interface for expressions
CFunctionType	Class encapsulating a function type
CGetAssertionsCommand
CGetAssignmentCommand
CGetInfoCommand
CGetInstantiationsCommand
CGetModelCommand
CGetOptionCommand
CGetProofCommand
CGetUnsatCoreCommand
CGetValueCommand
CIllegalArgumentException
CInteger
CIntegerHashFunction
CIntegerType	Singleton class encapsulating the integer type
CIntToBitVector
CLemmaInputChannel
CLemmaOutputChannel	This interface describes a mechanism for the propositional and theory engines to communicate with the "outside world" about new lemmas being discovered
CLogicException
CLogicInfo	A LogicInfo instance describes a collection of theory modules and some basic configuration about them
CModalException
CNodeTemplate
COptionException	Class representing an option-parsing exception such as badly-typed or missing arguments, arguments out of bounds, etc
COptions
CPairHashFunction
CPopCommand
CPredicate
CPredicateHashFunction
CProof
CPropagateRuleCommand
CPushCommand
CQueryCommand
CQuitCommand
CRational	A multi-precision rational constant
CRationalFromDoubleException
CRationalHashFunction
CRealType	Singleton class encapsulating the real type
CRecord
CRecordHashFunction
CRecordSelect
CRecordSelectHashFunction
CRecordType	Class encapsulating a record type
CRecordUpdate
CRecordUpdateHashFunction
CRegExp
CRegExpHashFunction	Hash function for the RegExp constants
CResult	Three-valued SMT result, with optional explanation
CRewriteRuleCommand
CScopeException
CSelectorType	Class encapsulating the Selector type
CSetBenchmarkLogicCommand
CSetBenchmarkStatusCommand
CSetInfoCommand
CSetOptionCommand
CSetType	Class encapsulating an set type
CSetUserAttributeCommand	The command when an attribute is set by a user
CSExpr	A simple S-expression
CSExprKeyword
CSExprType	Class encapsulating a tuple type
CSharedChannel
CSimplifyCommand
CSmtEngine
CSortConstructorType	Class encapsulating a user-defined sort constructor
CSortType	Class encapsulating a user-defined sort
CStatistics
►CStatisticsBase
Citerator
CStatCmp	A helper class for comparing two statistics
CString
CStringHashFunction
CStringType	Singleton class encapsulating the string type
CSubrangeBound	Representation of a subrange bound
CSubrangeBounds
CSubrangeBoundsHashFunction
CSubrangeType	Class encapsulating an integer subrange type
CSymbolTable	A convenience class for handling scoped declarations
CSynchronizedSharedChannel
CTesterType	Class encapsulating the Tester type
CTupleSelect
CTupleSelectHashFunction
CTupleType	Class encapsulating a tuple type
CTupleUpdate
CTupleUpdateHashFunction
CType	Class encapsulating CVC4 expression types
CTypeCheckingException	Exception thrown in the case of type-checking errors
CTypeConstantHashFunction	We hash the constants with their values
CTypeHashFunction	Hash function for Types
CUninterpretedConstant
CUninterpretedConstantHashFunction	Hash function for the BitVector constants
CUnrecognizedOptionException	Class representing an exception in option processing due to an unrecognized or unsupported option key
CUnsignedHashFunction
CVariableTypeMap