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