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