cvc4-1.4
Main Page
Related Pages
Namespaces
Data Structures
Files
Data Structures
Data Structure Index
Class Hierarchy
Data Fields
Data Structure Index
A
|
B
|
C
|
D
|
E
|
F
|
G
|
H
|
I
|
K
|
L
|
M
|
N
|
O
|
P
|
Q
|
R
|
S
|
T
|
U
|
V
|
W
|
Z
A
G
SExprKeyword
(
CVC4
)
compressItes__option_t
(
CVC4::options
)
nnfQuant__option_t
(
CVC4::options
)
SExprType
(
CVC4
)
condenseFunctionValues__option_t
(
CVC4::options
)
o
AbstractValue
(
CVC4
)
GetAssertionsCommand
(
CVC4
)
SharedChannel
(
CVC4
)
Expr::const_iterator
(
CVC4
)
AbstractValueHashFunction
(
CVC4
)
GetAssignmentCommand
(
CVC4
)
SimplifyCommand
(
CVC4
)
continuedExecution__option_t
(
CVC4::options
)
out__option_t
(
CVC4::options
)
ArrayStoreAll
(
CVC4
)
GetInfoCommand
(
CVC4
)
SmtEngine
(
CVC4
)
cumulativeMillisecondLimit__option_t
(
CVC4::options
)
outputLanguage__option_t
(
CVC4::options
)
ArrayStoreAllHashFunction
(
CVC4
)
GetInstantiationsCommand
(
CVC4
)
SortConstructorType
(
CVC4
)
cumulativeResourceLimit__option_t
(
CVC4::options
)
p
ArrayType
(
CVC4
)
GetModelCommand
(
CVC4
)
SortType
(
CVC4
)
d
AscriptionType
(
CVC4
)
GetOptionCommand
(
CVC4
)
StatisticsBase::StatCmp
(
CVC4
)
parseOnly__option_t
(
CVC4::options
)
AscriptionTypeHashFunction
(
CVC4
)
GetProofCommand
(
CVC4
)
Statistics
(
CVC4
)
decisionMode__option_t
(
CVC4::options
)
pbRewrites__option_t
(
CVC4::options
)
AssertCommand
(
CVC4
)
GetUnsatCoreCommand
(
CVC4
)
StatisticsBase
(
CVC4
)
decisionRandomWeight__option_t
(
CVC4::options
)
pbRewriteThreshold__option_t
(
CVC4::options
)
B
GetValueCommand
(
CVC4
)
String
(
CVC4
)
decisionStopOnly__option_t
(
CVC4::options
)
perCallMillisecondLimit__option_t
(
CVC4::options
)
I
StringHashFunction
(
CVC4::strings
)
decisionThreshold__option_t
(
CVC4::options
)
perCallResourceLimit__option_t
(
CVC4::options
)
BitVector
(
CVC4
)
StringHashFunction
(
CVC4
)
decisionUseWeight__option_t
(
CVC4::options
)
ppAssertMaxSubSize__option_t
(
CVC4::options
)
BitVectorBitOf
(
CVC4
)
IllegalArgumentException
(
CVC4
)
StringType
(
CVC4
)
decisionWeightInternal__option_t
(
CVC4::options
)
prenexQuant__option_t
(
CVC4::options
)
BitVectorBitOfHashFunction
(
CVC4
)
Input
(
CVC4::parser
)
SubrangeBound
(
CVC4
)
defaultDagThresh__option_t
(
CVC4::options
)
preprocessOnly__option_t
(
CVC4::options
)
BitVectorExtract
(
CVC4
)
InputStream
(
CVC4::parser
)
SubrangeBounds
(
CVC4
)
defaultExprDepth__option_t
(
CVC4::options
)
preSkolemQuant__option_t
(
CVC4::options
)
BitVectorExtractHashFunction
(
CVC4
)
InputStreamException
(
CVC4::parser
)
SubrangeBoundsHashFunction
(
CVC4
)
dioRepeat__option_t
(
CVC4::options
)
printSuccess__option_t
(
CVC4::options
)
BitVectorHashFunction
(
CVC4
)
Integer
(
CVC4
)
SubrangeType
(
CVC4
)
dioSolverTurns__option_t
(
CVC4::options
)
produceAssignments__option_t
(
CVC4::options
)
BitVectorRepeat
(
CVC4
)
IntegerHashFunction
(
CVC4
)
SymbolTable
(
CVC4
)
doCutAllBounded__option_t
(
CVC4::options
)
produceModels__option_t
(
CVC4::options
)
BitVectorRotateLeft
(
CVC4
)
IntegerType
(
CVC4
)
SynchronizedSharedChannel
(
CVC4
)
doITESimp__option_t
(
CVC4::options
)
proof__option_t
(
CVC4::options
)
BitVectorRotateRight
(
CVC4
)
IntToBitVector
(
CVC4
)
T
doITESimpOnRepeat__option_t
(
CVC4::options
)
q
BitVectorSignExtend
(
CVC4
)
K
doStaticLearning__option_t
(
CVC4::options
)
BitVectorSize
(
CVC4
)
TesterType
(
CVC4
)
dtForceAssignment__option_t
(
CVC4::options
)
qcfMode__option_t
(
CVC4::options
)
BitVectorType
(
CVC4
)
KindHashFunction
(
CVC4::kind
)
Theorem
(
CVC3
)
dtRewriteErrorSel__option_t
(
CVC4::options
)
qcfTConstraint__option_t
(
CVC4::options
)
BitVectorZeroExtend
(
CVC4
)
L
TupleSelect
(
CVC4
)
dtStcInduction__option_t
(
CVC4::options
)
qcfWhenMode__option_t
(
CVC4::options
)
BooleanType
(
CVC4
)
TupleSelectHashFunction
(
CVC4
)
dumpInstantiations__option_t
(
CVC4::options
)
quantConflictFind__option_t
(
CVC4::options
)
BoolHashFunction
(
CVC4
)
LemmaInputChannel
(
CVC4
)
TupleType
(
CVC4
)
dumpModels__option_t
(
CVC4::options
)
quantRewriteRules__option_t
(
CVC4::options
)
C
LemmaOutputChannel
(
CVC4
)
TupleUpdate
(
CVC4
)
dumpProofs__option_t
(
CVC4::options
)
r
LogicException
(
CVC4
)
TupleUpdateHashFunction
(
CVC4
)
e
Cardinality
(
CVC4
)
LogicInfo
(
CVC4
)
Type
(
CVC3
)
recurseCbqi__option_t
(
CVC4::options
)
CardinalityBeth
(
CVC4
)
M
Type
(
CVC4
)
eagerInstQuant__option_t
(
CVC4::options
)
registerQuantBodyTerms__option_t
(
CVC4::options
)
CardinalityUnknown
(
CVC4
)
TypeCheckingException
(
CVC4
)
earlyExit__option_t
(
CVC4::options
)
relationalTriggers__option_t
(
CVC4::options
)
CDInsertHashMap
(
CVC4::context
)
MapPickler
(
CVC4::expr::pickle
)
TypeConstantHashFunction
(
CVC4
)
earlyTypeChecking__option_t
(
CVC4::options
)
relevantTriggers__option_t
(
CVC4::options
)
CDTrailHashMap
(
CVC4::context
)
ModalException
(
CVC4
)
TypeHashFunction
(
CVC4
)
err__option_t
(
CVC4::options
)
repeatSimp__option_t
(
CVC4::options
)
Chain
(
CVC4
)
N
U
expandDefinitions__option_t
(
CVC4::options
)
replayEarlyCloseDepths__option_t
(
CVC4::options
)
ChainHashFunction
(
CVC4
)
exportDioDecompositions__option_t
(
CVC4::options
)
replayFailureLemma__option_t
(
CVC4::options
)
CheckSatCommand
(
CVC4
)
NodeTemplate
(
CVC4
)
UninterpretedConstant
(
CVC4
)
f
replayFailurePenalty__option_t
(
CVC4::options
)
CLFlag
(
CVC3
)
O
UninterpretedConstantHashFunction
(
CVC4
)
replayFilename__option_t
(
CVC4::options
)
CLFlags
(
CVC3
)
UnrecognizedOptionException
(
CVC4
)
fallbackSequential__option_t
(
CVC4::options
)
replayLog__option_t
(
CVC4::options
)
Command
(
CVC4
)
OptionException
(
CVC4
)
UnsignedHashFunction
(
CVC4
)
filesystemAccess__option_t
(
CVC4::options
)
replayNumericFailurePenalty__option_t
(
CVC4::options
)
CommandFailure
(
CVC4
)
Options
(
CVC4
)
V
finiteModelFind__option_t
(
CVC4::options
)
replayRejectCutSize__option_t
(
CVC4::options
)
CommandPrintSuccess
(
CVC4
)
P
flipDecision__option_t
(
CVC4::options
)
replayStream__option_t
(
CVC4::options
)
CommandSequence
(
CVC4
)
ValidityChecker
(
CVC3
)
fmfBoundInt__option_t
(
CVC4::options
)
restrictedPivots__option_t
(
CVC4::options
)
CommandStatus
(
CVC4
)
PairHashFunction
(
CVC4
)
VariableTypeMap
(
CVC4
)
fmfBoundIntLazy__option_t
(
CVC4::options
)
revertArithModels__option_t
(
CVC4::options
)
CommandSuccess
(
CVC4
)
Parser
(
CVC4::parser
)
a
fmfFmcSimple__option_t
(
CVC4::options
)
rewriteApplyToConst__option_t
(
CVC4::options
)
CommandUnsupported
(
CVC4
)
ParserBuilder
(
CVC4::parser
)
fmfFreshDistConst__option_t
(
CVC4::options
)
rewriteDivk__option_t
(
CVC4::options
)
CommentCommand
(
CVC4
)
ParserEndOfFileException
(
CVC4::parser
)
abstractValues__option_t
(
CVC4::options
)
fmfInstEngine__option_t
(
CVC4::options
)
rrOneInstPerRound__option_t
(
CVC4::options
)
Configuration
(
CVC4
)
ParserException
(
CVC4::parser
)
aggressiveMiniscopeQuant__option_t
(
CVC4::options
)
fmfInstGen__option_t
(
CVC4::options
)
rrTurns__option_t
(
CVC4::options
)
ConstructorType
(
CVC4
)
Pickle
(
CVC4::expr::pickle
)
arithDioSolver__option_t
(
CVC4::options
)
fmfInstGenOneQuantPerRound__option_t
(
CVC4::options
)
s
D
Pickler
(
CVC4::expr::pickle
)
arithErrorSelectionRule__option_t
(
CVC4::options
)
fmfOneInstPerRound__option_t
(
CVC4::options
)
PicklingException
(
CVC4::expr::pickle
)
arithHeuristicPivots__option_t
(
CVC4::options
)
fmfOneQuantPerRound__option_t
(
CVC4::options
)
sat_refine_conflicts__option_t
(
CVC4::options
)
Datatype
(
CVC4
)
PopCommand
(
CVC4
)
arithMLTrick__option_t
(
CVC4::options
)
foPropQuant__option_t
(
CVC4::options
)
satClauseDecay__option_t
(
CVC4::options
)
DatatypeConstructor
(
CVC4
)
Predicate
(
CVC4
)
arithMLTrickSubstitutions__option_t
(
CVC4::options
)
forceLogic__option_t
(
CVC4::options
)
satRandomFreq__option_t
(
CVC4::options
)
DatatypeConstructorArg
(
CVC4
)
PredicateHashFunction
(
CVC4
)
arithPivotThreshold__option_t
(
CVC4::options
)
forceNoLimitCpuWhileDump__option_t
(
CVC4::options
)
satRandomSeed__option_t
(
CVC4::options
)
DatatypeConstructorArgIterator
(
CVC4
)
Proof
(
CVC3
)
arithPropagateMaxLength__option_t
(
CVC4::options
)
fullSaturateQuant__option_t
(
CVC4::options
)
satRestartFirst__option_t
(
CVC4::options
)
DatatypeConstructorIterator
(
CVC4
)
Proof
(
CVC4
)
arithPropagationMode__option_t
(
CVC4::options
)
h
satRestartInc__option_t
(
CVC4::options
)
DatatypeDeclarationCommand
(
CVC4
)
PropagateRuleCommand
(
CVC4
)
arithPropAsLemmaLength__option_t
(
CVC4::options
)
satVarDecay__option_t
(
CVC4::options
)
DatatypeHashFunction
(
CVC4
)
PushCommand
(
CVC4
)
arithRewriteEq__option_t
(
CVC4::options
)
hash
(
__gnu_cxx
)
segvSpin__option_t
(
CVC4::options
)
DatatypeResolutionException
(
CVC4
)
Q
arithSimplexCheckPeriod__option_t
(
CVC4::options
)
havePenalties__option_t
(
CVC4::options
)
semanticChecks__option_t
(
CVC4::options
)
DatatypeSelfType
(
CVC4
)
arithStandardCheckVarOrderPivots__option_t
(
CVC4::options
)
help__option_t
(
CVC4::options
)
setsEagerLemmas__option_t
(
CVC4::options
)
DatatypeType
(
CVC4
)
QueryCommand
(
CVC4
)
arithUnateLemmaMode__option_t
(
CVC4::options
)
i
setsPropagate__option_t
(
CVC4::options
)
DatatypeUnresolvedType
(
CVC4
)
QuitCommand
(
CVC4
)
arraysEagerIndexSplitting__option_t
(
CVC4::options
)
sharingFilterByLength__option_t
(
CVC4::options
)
DeclarationDefinitionCommand
(
CVC4
)
R
arraysEagerLemmas__option_t
(
CVC4::options
)
idlRewriteEq__option_t
(
CVC4::options
)
simpleIteLiftQuant__option_t
(
CVC4::options
)
DeclarationSequence
(
CVC4
)
arraysLazyRIntro1__option_t
(
CVC4::options
)
in__option_t
(
CVC4::options
)
simplificationMode__option_t
(
CVC4::options
)
DeclareFunctionCommand
(
CVC4
)
Rational
(
CVC4
)
arraysModelBased__option_t
(
CVC4::options
)
incrementalParallel__option_t
(
CVC4::options
)
simplifyWithCareEnabled__option_t
(
CVC4::options
)
DeclareTypeCommand
(
CVC4
)
RationalFromDoubleException
(
CVC4
)
arraysOptimizeLinear__option_t
(
CVC4::options
)
incrementalSolving__option_t
(
CVC4::options
)
skolemizeArguments__option_t
(
CVC4::options
)
DefineFunctionCommand
(
CVC4
)
RationalHashFunction
(
CVC4
)
axiomInstMode__option_t
(
CVC4::options
)
inputLanguage__option_t
(
CVC4::options
)
smartTriggers__option_t
(
CVC4::options
)
DefineNamedFunctionCommand
(
CVC4
)
RealType
(
CVC4
)
b
instFormatMode__option_t
(
CVC4::options
)
soiApproxMajorFailure__option_t
(
CVC4::options
)
DefineTypeCommand
(
CVC4
)
Record
(
CVC4
)
instMaxLevel__option_t
(
CVC4::options
)
soiApproxMajorFailurePen__option_t
(
CVC4::options
)
Divisible
(
CVC4
)
RecordHashFunction
(
CVC4
)
biasedITERemoval__option_t
(
CVC4::options
)
instWhenMode__option_t
(
CVC4::options
)
soiApproxMinorFailure__option_t
(
CVC4::options
)
DivisibleHashFunction
(
CVC4
)
RecordSelect
(
CVC4
)
binary_name__option_t
(
CVC4::options
)
interactive__option_t
(
CVC4::options
)
soiApproxMinorFailurePen__option_t
(
CVC4::options
)
E
RecordSelectHashFunction
(
CVC4
)
bitblastMode__option_t
(
CVC4::options
)
interactivePrompt__option_t
(
CVC4::options
)
soiQuickExplain__option_t
(
CVC4::options
)
RecordType
(
CVC4
)
bitvectorAig__option_t
(
CVC4::options
)
internalReps__option_t
(
CVC4::options
)
sortInference__option_t
(
CVC4::options
)
EchoCommand
(
CVC4
)
RecordUpdate
(
CVC4
)
bitvectorAigSimplifications__option_t
(
CVC4::options
)
StatisticsBase::iterator
(
CVC4
)
statistics__option_t
(
CVC4::options
)
EmptyCommand
(
CVC4
)
RecordUpdateHashFunction
(
CVC4
)
bitvectorAlgebraicBudget__option_t
(
CVC4::options
)
l
statsEveryQuery__option_t
(
CVC4::options
)
EmptySet
(
CVC4
)
RegExp
(
CVC4
)
bitvectorAlgebraicSolver__option_t
(
CVC4::options
)
statsHideZeros__option_t
(
CVC4::options
)
EmptySetHashFunction
(
CVC4
)
RegExpHashFunction
(
CVC4
)
bitvectorDivByZeroConst__option_t
(
CVC4::options
)
languageHelp__option_t
(
CVC4::options
)
strictParsing__option_t
(
CVC4::options
)
Exception
(
CVC4
)
Result
(
CVC4
)
bitvectorEqualitySlicer__option_t
(
CVC4::options
)
lemmaInputChannel__option_t
(
CVC4::options
)
stringCharCardinality__option_t
(
CVC4::options
)
ExpandDefinitionsCommand
(
CVC4
)
RewriteRuleCommand
(
CVC4
)
bitvectorEqualitySolver__option_t
(
CVC4::options
)
lemmaOutputChannel__option_t
(
CVC4::options
)
stringEIT__option_t
(
CVC4::options
)
Command::ExportTransformer
(
CVC4
)
S
bitvectorInequalitySolver__option_t
(
CVC4::options
)
lemmaRejectCutSize__option_t
(
CVC4::options
)
stringExp__option_t
(
CVC4::options
)
ExportUnsupportedException
(
CVC4
)
bitvectorPropagate__option_t
(
CVC4::options
)
literalMatchMode__option_t
(
CVC4::options
)
stringFMF__option_t
(
CVC4::options
)
Expr
(
CVC3
)
SatSolverFactory
(
CVC4::prop
)
bitvectorQuickXplain__option_t
(
CVC4::options
)
m
stringLB__option_t
(
CVC4::options
)
Expr
(
CVC4
)
ExprDag::Scope
(
CVC4::expr
)
bitvectorToBool__option_t
(
CVC4::options
)
stringOpt1__option_t
(
CVC4::options
)
ExprDag
(
CVC4::expr
)
ExprSetDepth::Scope
(
CVC4::expr
)
booleanTermConversionMode__option_t
(
CVC4::options
)
macrosQuant__option_t
(
CVC4::options
)
stringOpt2__option_t
(
CVC4::options
)
ExprHashFunction
(
CVC4
)
ExprPrintTypes::Scope
(
CVC4::expr
)
bvAbstraction__option_t
(
CVC4::options
)
maxApproxDepth__option_t
(
CVC4::options
)
t
ExprHashMap
(
CVC3
)
CommandPrintSuccess::Scope
(
CVC4
)
bvEagerExplanations__option_t
(
CVC4::options
)
maxCutsInContext__option_t
(
CVC4::options
)
ExprManager
(
CVC3
)
ExprSetLanguage::Scope
(
CVC4::expr
)
bvIntroducePow2__option_t
(
CVC4::options
)
maxReplayTree__option_t
(
CVC4::options
)
tearDownIncremental__option_t
(
CVC4::options
)
ExprManager
(
CVC4
)
ScopeException
(
CVC4
)
bvNumFunc__option_t
(
CVC4::options
)
mbqiMode__option_t
(
CVC4::options
)
theoryAlternates__option_t
(
CVC4::options
)
ExprManagerMapCollection
(
CVC4
)
SelectorType
(
CVC4
)
c
memoryMap__option_t
(
CVC4::options
)
theoryOfMode__option_t
(
CVC4::options
)
ExprMap
(
CVC3
)
SetBenchmarkLogicCommand
(
CVC4
)
minisatDumpDimacs__option_t
(
CVC4::options
)
thread_id__option_t
(
CVC4::options
)
ExprPrintTypes
(
CVC4::expr
)
SetBenchmarkStatusCommand
(
CVC4
)
cbqi__option_t
(
CVC4::options
)
minisatUseElim__option_t
(
CVC4::options
)
threadArgv__option_t
(
CVC4::options
)
ExprSetDepth
(
CVC4::expr
)
SetInfoCommand
(
CVC4
)
checkModels__option_t
(
CVC4::options
)
miniscopeQuant__option_t
(
CVC4::options
)
threads__option_t
(
CVC4::options
)
ExprSetLanguage
(
CVC4::expr
)
SetOptionCommand
(
CVC4
)
checkProofs__option_t
(
CVC4::options
)
miniscopeQuantFreeVar__option_t
(
CVC4::options
)
threadStackSize__option_t
(
CVC4::options
)
ExprStream
(
CVC4
)
SetType
(
CVC4
)
clauseSplit__option_t
(
CVC4::options
)
modelFormatMode__option_t
(
CVC4::options
)
trySolveIntStandardEffort__option_t
(
CVC4::options
)
Parser::ExprStream
(
CVC4::parser
)
SetUserAttributeCommand
(
CVC4
)
cnfQuant__option_t
(
CVC4::options
)
modelUninterpDtEnum__option_t
(
CVC4::options
)
typeChecking__option_t
(
CVC4::options
)
F
SExpr
(
CVC4
)
collectPivots__option_t
(
CVC4::options
)
n
u
FunctionType
(
CVC4
)
newProp__option_t
(
CVC4::options
)
ufssAbortCardinality__option_t
(
CVC4::options
)
A
|
B
|
C
|
D
|
E
|
F
|
G
|
H
|
I
|
K
|
L
|
M
|
N
|
O
|
P
|
Q
|
R
|
S
|
T
|
U
|
V
|
W
|
Z
Generated by
1.8.11