cvc4-1.3
Class Hierarchy
This inheritance list is sorted roughly, but not completely, alphabetically:
[detail level 1234]
 CCVC4::AbstractValue
 CCVC4::AbstractValueHashFunctionHash 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::ArrayStoreAllHashFunctionHash function for the ArrayStoreAll constants
 CCVC4::AscriptionTypeA class used to parameterize a type ascription
 CCVC4::AscriptionTypeHashFunctionA hash function for type ascription operators
 CCVC4::options::axiomInstMode__option_t
 CCVC4::options::biasedITERemoval__option_t
 CCVC4::options::binary_name__option_t
 CCVC4::BitVector
 CCVC4::BitVectorBitOfThe structure representing the extraction of one Boolean bit
 CCVC4::BitVectorBitOfHashFunctionHash function for the BitVectorBitOf objects
 CCVC4::options::bitvectorCoreSolver__option_t
 CCVC4::options::bitvectorEagerBitblast__option_t
 CCVC4::options::bitvectorEagerFullcheck__option_t
 CCVC4::BitVectorExtractThe structure representing the extraction operation for bit-vectors
 CCVC4::BitVectorExtractHashFunctionHash function for the BitVectorExtract objects
 CCVC4::BitVectorHashFunctionHash function for the BitVector constants
 CCVC4::options::bitvectorInequalitySolver__option_t
 CCVC4::BitVectorRepeat
 CCVC4::BitVectorRotateLeft
 CCVC4::BitVectorRotateRight
 CCVC4::options::bitvectorShareLemmas__option_t
 CCVC4::BitVectorSignExtend
 CCVC4::BitVectorSize
 CCVC4::BitVectorZeroExtend
 CCVC4::options::booleanTermConversionMode__option_t
 CCVC4::BoolHashFunction
 CCVC4::options::bvEquality__option_t
 CCVC4::options::bvPropagate__option_t
 CCVC4::options::bvToBool__option_t
 CCVC4::options::canIncludeFile__option_t
 CCVC4::CardinalityA simple representation of a cardinality
 CCVC4::CardinalityBethRepresentation for a Beth number, used only to construct Cardinality objects
 CCVC4::CardinalityUnknownRepresentation for an unknown cardinality
 CCVC4::options::cbqi__option_t
 CCVC4::context::CDInsertHashMap< Key, Data, HashFcn >
 CCVC4::context::CDTrailHashMap< Key, Data, HashFcn >
 CCVC4::ChainA class to represent a chained, built-in operator
 CCVC4::ChainHashFunction
 CCVC4::options::checkModels__option_t
 CCVC4::options::clauseSplit__option_t
 CCVC3::CLFlag
 CCVC3::CLFlags
 CCVC4::options::cnfQuant__option_t
 CCVC4::options::collectPivots__option_t
 CCVC4::Command
 CCVC4::CommandPrintSuccessIOStream manipulator to print success messages or not
 CCVC4::CommandStatus
 CCVC4::options::compressItes__option_t
 CCVC4::options::condenseFunctionValues__option_t
 CCVC4::ConfigurationRepresents the (static) configuration of CVC4
 CCVC4::options::cumulativeMillisecondLimit__option_t
 CCVC4::options::cumulativeResourceLimit__option_t
 CCVC4::CVC4dumpstream
 CCVC4::DatatypeThe representation of an inductive datatype
 CCVC4::DatatypeConstructorA constructor for a Datatype
 CCVC4::DatatypeConstructorArgA Datatype constructor argument (i.e., a Datatype field)
 CCVC4::DatatypeHashFunctionA hash function for Datatypes
 CCVC4::DatatypeSelfTypeA holder type (used in calls to DatatypeConstructor::addArg()) to allow a Datatype to refer to itself
 CCVC4::DatatypeUnresolvedTypeAn 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::DivisibleThe structure representing the divisibility-by-k predicate
 CCVC4::DivisibleHashFunctionHash 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::DumpCThe dump class
 CCVC4::options::dumpModels__option_t
 CCVC4::options::eagerInstQuant__option_t
 CCVC4::options::earlyExit__option_t
 CCVC4::options::earlyTypeChecking__option_t
 CCVC4::options::efficientEMatching__option_t
 CCVC4::options::err__option_t
 Cstd::exceptionSTL class
 CCVC4::options::expandDefinitions__option_t
 CCVC4::options::exportDioDecompositions__option_t
 CCVC4::Command::ExportTransformer
 CCVC4::ExprClass encapsulating CVC4 expressions and methods for constructing new expressions
 CCVC4::expr::ExprDagIOStream manipulator to print expressions as a dag (or not)
 CCVC4::ExprHashFunction
 CCVC4::ExprManager
 CCVC4::ExprManagerMapCollection
 CCVC4::expr::ExprPrintTypesIOStream manipulator to print type ascriptions or not
 CCVC4::expr::ExprSetDepthIOStream manipulator to set the maximum depth of Exprs when pretty-printing
 CCVC4::expr::ExprSetLanguageIOStream manipulator to set the output language for Exprs
 CCVC4::ExprStreamA pure-virtual stream interface for expressions
 CCVC4::options::fallbackSequential__option_t
 CCVC4::options::fancyFinal__option_t
 CCVC4::options::finiteModelFind__option_t
 CCVC4::options::flipDecision__option_t
 CCVC4::options::fmfBoundInt__option_t
 CCVC4::options::fmfFmcCoverSimplify__option_t
 CCVC4::options::fmfFmcInterval__option_t
 CCVC4::options::fmfFmcSimple__option_t
 CCVC4::options::fmfFreshDistConst__option_t
 CCVC4::options::fmfFullModelCheck__option_t
 CCVC4::options::fmfInstEngine__option_t
 CCVC4::options::fmfInstGen__option_t
 CCVC4::options::fmfInstGenOneQuantPerRound__option_t
 CCVC4::options::fmfModelBasedInst__option_t
 CCVC4::options::fmfNewInstGen__option_t
 CCVC4::options::fmfOneInstPerRound__option_t
 CCVC4::options::fmfOneQuantPerRound__option_t
 CCVC4::options::fmfRelevantDomain__option_t
 CCVC4::options::foPropQuant__option_t
 C__gnu_cxx::hash< Key >
 Chash_map
 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::InputAn input to be parsed
 CCVC4::options::inputLanguage__option_t
 CCVC4::parser::InputStreamWrapper around an input stream
 CCVC4::options::instWhenMode__option_t
 CCVC4::Integer
 CCVC4::IntegerHashFunction
 CCVC4::options::interactive__option_t
 CCVC4::options::internalReps__option_t
 CCVC4::IntToBitVector
 Citerator
 CCVC4::options::iteRemoveQuant__option_t
 CCVC4::kind::KindHashFunction
 CCVC4::options::languageHelp__option_t
 CCVC4::LemmaInputChannel
 CCVC4::options::lemmaInputChannel__option_t
 CCVC4::LemmaOutputChannelThis 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::literalMatchMode__option_t
 CCVC4::LogicInfoA 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
 CCVC4::options::maxCutsInContext__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::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::ParserThis 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::ParserBuilderA builder for input language parsers
 CCVC4::options::perCallMillisecondLimit__option_t
 CCVC4::options::perCallResourceLimit__option_t
 CCVC4::expr::pickle::Pickle
 CCVC4::expr::pickle::Pickler
 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
 CCVC3::Proof
 CCVC4::Proof
 CCVC4::options::proof__option_t
 CCVC4::RationalA 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::RegExpHashFunctionHash 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::replayFilename__option_t
 CCVC4::options::replayLog__option_t
 CCVC4::options::replayStream__option_t
 CCVC4::options::restrictedPivots__option_t
 CCVC4::ResultThree-valued SMT result, with optional explanation
 CCVC4::options::revertArithModels__option_t
 CCVC4::options::rewriteApplyToConst__option_t
 CCVC4::options::rewriteDivk__option_t
 CCVC4::options::rewriteRulesAsAxioms__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::ScopeSet the dag state on the output stream for the current stack scope
 CCVC4::expr::ExprSetLanguage::ScopeSet a language on the output stream for the current stack scope
 CCVC4::expr::ExprSetDepth::ScopeSet the expression depth on the output stream for the current stack scope
 CCVC4::expr::ExprPrintTypes::ScopeSet the print-types state on the output stream for the current stack scope
 CCVC4::CommandPrintSuccess::ScopeSet the print-success state on the output stream for the current stack scope
 CCVC4::options::segvSpin__option_t
 CCVC4::options::semanticChecks__option_t
 CCVC4::SExprA simple S-expression
 CCVC4::SExprKeyword
 CCVC4::SharedChannel< T >
 CCVC4::options::sharingFilterByLength__option_t
 CCVC4::options::simpleIteLiftQuant__option_t
 CCVC4::options::simplificationMode__option_t
 CCVC4::options::simplifyWithCareEnabled__option_t
 CCVC4::options::smartTriggers__option_t
 CCVC4::SmtEngine
 CCVC4::options::soiQuickExplain__option_t
 CCVC4::options::sortInference__option_t
 CCVC4::StatisticsBase::StatCmpA helper class for comparing two statistics
 CCVC4::options::statistics__option_t
 CCVC4::StatisticsBase
 CCVC4::options::strictParsing__option_t
 CCVC4::String
 CCVC4::options::stringCharCardinality__option_t
 CCVC4::options::stringExp__option_t
 CCVC4::options::stringFMF__option_t
 CCVC4::StringHashFunction
 CCVC4::strings::StringHashFunction
 CCVC4::options::stringLB__option_t
 CCVC4::options::stringRegExpUnrollDepth__option_t
 CCVC4::SubrangeBoundRepresentation of a subrange bound
 CCVC4::SubrangeBounds
 CCVC4::SubrangeBoundsHashFunction
 CCVC4::SymbolTableA convenience class for handling scoped declarations
 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::TupleSelect
 CCVC4::TupleSelectHashFunction
 CCVC4::TupleUpdate
 CCVC4::TupleUpdateHashFunction
 CCVC4::TypeClass encapsulating CVC4 expression types
 CCVC4::options::typeChecking__option_t
 CCVC4::TypeConstantHashFunctionWe hash the constants with their values
 CCVC4::TypeHashFunctionHash function for Types
 CCVC4::options::ufssAbortCardinality__option_t
 CCVC4::options::ufssCliqueSplits__option_t
 CCVC4::options::ufssColoringSat__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::ufssSmartSplits__option_t
 CCVC4::options::ufssSymBreak__option_t
 CCVC4::options::ufssTotality__option_t
 CCVC4::options::ufssTotalityLazy__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::UninterpretedConstantHashFunctionHash function for the BitVector constants
 CCVC4::options::unsatCores__option_t
 CCVC4::UnsignedHashFunction< T >
 CCVC4::options::useFC__option_t
 CCVC4::options::userPatternsQuant__option_t
 CCVC4::options::useSOI__option_t
 CCVC3::ValidityCheckerCVC3 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