cvc4-1.4
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)   decisionThreshold__option_t (CVC4::options)   perCallResourceLimit__option_t (CVC4::options)   
BitVector (CVC4)   StringHashFunction (CVC4::strings)   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 (CVC4)   arithPropagateMaxLength__option_t (CVC4::options)   fullSaturateQuant__option_t (CVC4::options)   satRestartFirst__option_t (CVC4::options)   
DatatypeConstructorIterator (CVC4)   Proof (CVC3)   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 (CVC4)   SatSolverFactory (CVC4::prop)   bitvectorQuickXplain__option_t (CVC4::options)   
  m  
stringLB__option_t (CVC4::options)   
Expr (CVC3)   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)   ExprSetLanguage::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 (CVC4)   ExprPrintTypes::Scope (CVC4::expr)   bvIntroducePow2__option_t (CVC4::options)   maxReplayTree__option_t (CVC4::options)   tearDownIncremental__option_t (CVC4::options)   
ExprManager (CVC3)   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)   
Parser::ExprStream (CVC4::parser)   SetType (CVC4)   clauseSplit__option_t (CVC4::options)   modelFormatMode__option_t (CVC4::options)   trySolveIntStandardEffort__option_t (CVC4::options)   
ExprStream (CVC4)   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