cvc4-1.3
Main Page
Related Pages
Namespaces
Data Structures
Files
Data Structures
Data Structure Index
Class Hierarchy
Data Fields
Data Structures
Here are the data structures with brief descriptions:
[detail level
1
2
3
4
]
►
N
__gnu_cxx
C
hash
►
N
CVC3
C
CLFlag
C
CLFlags
C
Expr
Expr
class for
CVC3
compatibility layer
C
ExprHashMap
C
ExprManager
C
ExprMap
C
Proof
C
Theorem
C
Type
C
ValidityChecker
CVC3
API (compatibility layer for
CVC4
)
►
N
CVC4
►
N
context
C
CDInsertHashMap
C
CDTrailHashMap
►
N
expr
►
N
pickle
C
MapPickler
C
Pickle
C
Pickler
C
PicklingException
►
C
ExprDag
IOStream manipulator to print expressions as a dag (or not)
C
Scope
Set the dag state on the output stream for the current stack scope
►
C
ExprPrintTypes
IOStream manipulator to print type ascriptions or not
C
Scope
Set the print-types state on the output stream for the current stack scope
►
C
ExprSetDepth
IOStream manipulator to set the maximum depth of Exprs when pretty-printing
C
Scope
Set the expression depth on the output stream for the current stack scope
►
C
ExprSetLanguage
IOStream manipulator to set the output language for Exprs
C
Scope
Set a language on the output stream for the current stack scope
►
N
kind
C
KindHashFunction
►
N
language
►
N
options
C
abstractValues__option_t
C
aggressiveMiniscopeQuant__option_t
C
arithDioSolver__option_t
C
arithErrorSelectionRule__option_t
C
arithHeuristicPivots__option_t
C
arithMLTrick__option_t
C
arithMLTrickSubstitutions__option_t
C
arithPivotThreshold__option_t
C
arithPropagateMaxLength__option_t
C
arithPropagationMode__option_t
C
arithPropAsLemmaLength__option_t
C
arithRewriteEq__option_t
C
arithSimplexCheckPeriod__option_t
C
arithStandardCheckVarOrderPivots__option_t
C
arithUnateLemmaMode__option_t
C
arraysEagerIndexSplitting__option_t
C
arraysEagerLemmas__option_t
C
arraysLazyRIntro1__option_t
C
arraysModelBased__option_t
C
arraysOptimizeLinear__option_t
C
axiomInstMode__option_t
C
biasedITERemoval__option_t
C
binary_name__option_t
C
bitvectorCoreSolver__option_t
C
bitvectorEagerBitblast__option_t
C
bitvectorEagerFullcheck__option_t
C
bitvectorInequalitySolver__option_t
C
bitvectorShareLemmas__option_t
C
booleanTermConversionMode__option_t
C
bvEquality__option_t
C
bvPropagate__option_t
C
bvToBool__option_t
C
canIncludeFile__option_t
C
cbqi__option_t
C
checkModels__option_t
C
clauseSplit__option_t
C
cnfQuant__option_t
C
collectPivots__option_t
C
compressItes__option_t
C
condenseFunctionValues__option_t
C
cumulativeMillisecondLimit__option_t
C
cumulativeResourceLimit__option_t
C
decisionMode__option_t
C
decisionRandomWeight__option_t
C
decisionStopOnly__option_t
C
decisionThreshold__option_t
C
decisionUseWeight__option_t
C
decisionWeightInternal__option_t
C
defaultDagThresh__option_t
C
defaultExprDepth__option_t
C
doCutAllBounded__option_t
C
doITESimp__option_t
C
doITESimpOnRepeat__option_t
C
doStaticLearning__option_t
C
dtForceAssignment__option_t
C
dtRewriteErrorSel__option_t
C
dumpModels__option_t
C
eagerInstQuant__option_t
C
earlyExit__option_t
C
earlyTypeChecking__option_t
C
efficientEMatching__option_t
C
err__option_t
C
expandDefinitions__option_t
C
exportDioDecompositions__option_t
C
fallbackSequential__option_t
C
fancyFinal__option_t
C
finiteModelFind__option_t
C
flipDecision__option_t
C
fmfBoundInt__option_t
C
fmfFmcCoverSimplify__option_t
C
fmfFmcInterval__option_t
C
fmfFmcSimple__option_t
C
fmfFreshDistConst__option_t
C
fmfFullModelCheck__option_t
C
fmfInstEngine__option_t
C
fmfInstGen__option_t
C
fmfInstGenOneQuantPerRound__option_t
C
fmfModelBasedInst__option_t
C
fmfNewInstGen__option_t
C
fmfOneInstPerRound__option_t
C
fmfOneQuantPerRound__option_t
C
fmfRelevantDomain__option_t
C
foPropQuant__option_t
C
havePenalties__option_t
C
help__option_t
C
idlRewriteEq__option_t
C
in__option_t
C
incrementalParallel__option_t
C
incrementalSolving__option_t
C
inputLanguage__option_t
C
instWhenMode__option_t
C
interactive__option_t
C
internalReps__option_t
C
iteRemoveQuant__option_t
C
languageHelp__option_t
C
lemmaInputChannel__option_t
C
lemmaOutputChannel__option_t
C
literalMatchMode__option_t
C
macrosQuant__option_t
C
maxCutsInContext__option_t
C
memoryMap__option_t
C
minisatDumpDimacs__option_t
C
minisatUseElim__option_t
C
miniscopeQuant__option_t
C
miniscopeQuantFreeVar__option_t
C
modelFormatMode__option_t
C
modelUninterpDtEnum__option_t
C
newProp__option_t
C
out__option_t
C
outputLanguage__option_t
C
parseOnly__option_t
C
perCallMillisecondLimit__option_t
C
perCallResourceLimit__option_t
C
prenexQuant__option_t
C
preprocessOnly__option_t
C
preSkolemQuant__option_t
C
printSuccess__option_t
C
produceAssignments__option_t
C
produceModels__option_t
C
proof__option_t
C
recurseCbqi__option_t
C
registerQuantBodyTerms__option_t
C
relationalTriggers__option_t
C
relevantTriggers__option_t
C
repeatSimp__option_t
C
replayFilename__option_t
C
replayLog__option_t
C
replayStream__option_t
C
restrictedPivots__option_t
C
revertArithModels__option_t
C
rewriteApplyToConst__option_t
C
rewriteDivk__option_t
C
rewriteRulesAsAxioms__option_t
C
sat_refine_conflicts__option_t
C
satClauseDecay__option_t
C
satRandomFreq__option_t
C
satRandomSeed__option_t
C
satRestartFirst__option_t
C
satRestartInc__option_t
C
satVarDecay__option_t
C
segvSpin__option_t
C
semanticChecks__option_t
C
sharingFilterByLength__option_t
C
simpleIteLiftQuant__option_t
C
simplificationMode__option_t
C
simplifyWithCareEnabled__option_t
C
smartTriggers__option_t
C
soiQuickExplain__option_t
C
sortInference__option_t
C
statistics__option_t
C
strictParsing__option_t
C
stringCharCardinality__option_t
C
stringExp__option_t
C
stringFMF__option_t
C
stringLB__option_t
C
stringRegExpUnrollDepth__option_t
C
theoryAlternates__option_t
C
theoryOfMode__option_t
C
thread_id__option_t
C
threadArgv__option_t
C
threads__option_t
C
typeChecking__option_t
C
ufssAbortCardinality__option_t
C
ufssCliqueSplits__option_t
C
ufssColoringSat__option_t
C
ufssDiseqPropagation__option_t
C
ufssEagerSplits__option_t
C
ufssExplainedCliques__option_t
C
ufssFairness__option_t
C
ufssMinimalModel__option_t
C
ufssRegions__option_t
C
ufssSimpleCliques__option_t
C
ufssSmartSplits__option_t
C
ufssSymBreak__option_t
C
ufssTotality__option_t
C
ufssTotalityLazy__option_t
C
ufssTotalityLimited__option_t
C
ufssTotalitySymBreak__option_t
C
ufSymmetryBreaker__option_t
C
unconstrainedSimp__option_t
C
unsatCores__option_t
C
useFC__option_t
C
userPatternsQuant__option_t
C
useSOI__option_t
C
varElimQuant__option_t
C
verbosity__option_t
C
version__option_t
C
waitToJoin__option_t
C
zombieHuntThreshold__option_t
►
N
parser
C
Input
An input to be parsed
C
InputStream
Wrapper around an input stream
C
InputStreamException
►
C
Parser
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
C
ExprStream
An expression stream interface for a parser
C
ParserBuilder
A builder for input language parsers
C
ParserEndOfFileException
C
ParserException
►
N
prop
C
SatSolverFactory
►
N
strings
C
StringHashFunction
C
AbstractValue
C
AbstractValueHashFunction
Hash function for the
BitVector
constants
C
ArrayStoreAll
C
ArrayStoreAllHashFunction
Hash function for the
ArrayStoreAll
constants
C
ArrayType
Class encapsulating an array type
C
AscriptionType
A class used to parameterize a type ascription
C
AscriptionTypeHashFunction
A hash function for type ascription operators
C
AssertCommand
C
BitVector
C
BitVectorBitOf
The structure representing the extraction of one Boolean bit
C
BitVectorBitOfHashFunction
Hash function for the
BitVectorBitOf
objects
C
BitVectorExtract
The structure representing the extraction operation for bit-vectors
C
BitVectorExtractHashFunction
Hash function for the
BitVectorExtract
objects
C
BitVectorHashFunction
Hash function for the
BitVector
constants
C
BitVectorRepeat
C
BitVectorRotateLeft
C
BitVectorRotateRight
C
BitVectorSignExtend
C
BitVectorSize
C
BitVectorType
Class encapsulating the bit-vector type
C
BitVectorZeroExtend
C
BooleanType
Singleton class encapsulating the Boolean type
C
BoolHashFunction
C
Cardinality
A simple representation of a cardinality
C
CardinalityBeth
Representation for a Beth number, used only to construct
Cardinality
objects
C
CardinalityUnknown
Representation for an unknown cardinality
C
Chain
A class to represent a chained, built-in operator
C
ChainHashFunction
C
CheckSatCommand
►
C
Command
C
ExportTransformer
C
CommandFailure
►
C
CommandPrintSuccess
IOStream manipulator to print success messages or not
C
Scope
Set the print-success state on the output stream for the current stack scope
C
CommandSequence
C
CommandStatus
C
CommandSuccess
C
CommandUnsupported
C
CommentCommand
C
Configuration
Represents the (static) configuration of
CVC4
C
ConstructorType
Class encapsulating the constructor type
C
CVC4dumpstream
C
Datatype
The representation of an inductive datatype
C
DatatypeConstructor
A constructor for a
Datatype
C
DatatypeConstructorArg
A
Datatype
constructor argument (i.e., a
Datatype
field)
C
DatatypeDeclarationCommand
C
DatatypeHashFunction
A hash function for Datatypes
C
DatatypeResolutionException
An exception that is thrown when a datatype resolution fails
C
DatatypeSelfType
A holder type (used in calls to
DatatypeConstructor::addArg()
) to allow a
Datatype
to refer to itself
C
DatatypeType
Class encapsulating the datatype type
C
DatatypeUnresolvedType
An unresolved type (used in calls to
DatatypeConstructor::addArg()
) to allow a
Datatype
to refer to itself or to other mutually-recursive Datatypes
C
DeclarationDefinitionCommand
C
DeclarationSequence
C
DeclareFunctionCommand
C
DeclareTypeCommand
C
DefineFunctionCommand
C
DefineNamedFunctionCommand
This differs from
DefineFunctionCommand
only in that it instructs the
SmtEngine
to "remember" this function for later retrieval with getAssignment()
C
DefineTypeCommand
C
Divisible
The structure representing the divisibility-by-k predicate
C
DivisibleHashFunction
Hash function for the
Divisible
objects
C
DumpC
The dump class
C
EchoCommand
C
EmptyCommand
EmptyCommands are the residue of a command after the parser handles them (and there's nothing left to do)
C
Exception
C
ExpandDefinitionsCommand
C
ExportUnsupportedException
Exception
thrown in case of failure to export
►
C
Expr
Class encapsulating
CVC4
expressions and methods for constructing new expressions
C
const_iterator
Iterator type for the children of an
Expr
C
ExprHashFunction
C
ExprManager
C
ExprManagerMapCollection
C
ExprStream
A pure-virtual stream interface for expressions
C
FunctionType
Class encapsulating a function type
C
GetAssertionsCommand
C
GetAssignmentCommand
C
GetInfoCommand
C
GetModelCommand
C
GetOptionCommand
C
GetProofCommand
C
GetUnsatCoreCommand
C
GetValueCommand
C
IllegalArgumentException
C
Integer
C
IntegerHashFunction
C
IntegerType
Singleton class encapsulating the integer type
C
IntToBitVector
C
LemmaInputChannel
C
LemmaOutputChannel
This interface describes a mechanism for the propositional and theory engines to communicate with the "outside world" about new lemmas being discovered
C
LogicException
C
LogicInfo
A
LogicInfo
instance describes a collection of theory modules and some basic configuration about them
C
ModalException
C
NodeTemplate
C
OptionException
Class representing an option-parsing exception such as badly-typed or missing arguments, arguments out of bounds, etc
C
Options
C
PairHashFunction
C
PopCommand
C
Predicate
C
PredicateHashFunction
C
Proof
C
PropagateRuleCommand
C
PushCommand
C
QueryCommand
C
QuitCommand
C
Rational
A multi-precision rational constant
C
RationalHashFunction
C
RealType
Singleton class encapsulating the real type
C
Record
C
RecordHashFunction
C
RecordSelect
C
RecordSelectHashFunction
C
RecordType
Class encapsulating a record type
C
RecordUpdate
C
RecordUpdateHashFunction
C
RegExp
C
RegExpHashFunction
Hash function for the
RegExp
constants
C
Result
Three-valued SMT result, with optional explanation
C
RewriteRuleCommand
C
ScopeException
C
SelectorType
Class encapsulating the Selector type
C
SetBenchmarkLogicCommand
C
SetBenchmarkStatusCommand
C
SetInfoCommand
C
SetOptionCommand
C
SetUserAttributeCommand
The command when an attribute is set by a user
C
SExpr
A simple S-expression
C
SExprKeyword
C
SExprType
Class encapsulating a tuple type
C
SharedChannel
C
SimplifyCommand
C
SmtEngine
C
SortConstructorType
Class encapsulating a user-defined sort constructor
C
SortType
Class encapsulating a user-defined sort
C
Statistics
►
C
StatisticsBase
C
iterator
C
StatCmp
A helper class for comparing two statistics
C
String
C
StringHashFunction
C
StringType
Singleton class encapsulating the string type
C
SubrangeBound
Representation of a subrange bound
C
SubrangeBounds
C
SubrangeBoundsHashFunction
C
SubrangeType
Class encapsulating an integer subrange type
C
SymbolTable
A convenience class for handling scoped declarations
C
SynchronizedSharedChannel
C
TesterType
Class encapsulating the Tester type
C
TupleSelect
C
TupleSelectHashFunction
C
TupleType
Class encapsulating a tuple type
C
TupleUpdate
C
TupleUpdateHashFunction
C
Type
Class encapsulating
CVC4
expression types
C
TypeCheckingException
Exception
thrown in the case of type-checking errors
C
TypeConstantHashFunction
We hash the constants with their values
C
TypeHashFunction
Hash function for Types
C
UninterpretedConstant
C
UninterpretedConstantHashFunction
Hash function for the
BitVector
constants
C
UnrecognizedOptionException
Class representing an exception in option processing due to an unrecognized or unsupported option key
C
UnsignedHashFunction
C
VariableTypeMap
Generated by
1.8.7