| ►Nbenchmax | |
| ►Nsettings | |
| CSlurmBackendSettings | Settings for the Slurm backend |
| CSSHBackendSettings | Settings for SSH backend |
| CBenchmarkSettings | Settings for benchmarks |
| CPresetSettings | |
| CCoreSettings | Core settings |
| COperationSettings | Operation settings |
| CSettings | Generic class to manage runtime settings |
| CToolSettings | Tool-related settings |
| ►Nslurm | |
| CArchiveProperties | All properties needed to archive log files |
| CSubmitfileProperties | All properties needed to create a submit file |
| CChunkedSubmitfileProperties | All properties needed to create a submit file |
| ►Nssh | |
| CNode | Specification of a compuation node for the SSH backend |
| CSSHConnection | A wrapper class that manages a single SSH connection as specified in a Node object (with all its channels) |
| CBackend | Base class for all backends |
| CCondorBackend | Backend for the HTCondor batch system |
| ►CRandomizationAdaptor | Provides iteration over a given std::vector in a pseudo-randomized order |
| Citerator | |
| CJobs | Represents a set of jobs, constructed as the cartesian product of a set of tools and a set of benchmarks |
| CLocalBackend | This backend simply runs files sequentially on the local machine |
| CSlurmBackend | Backend for the Slurm workload manager |
| CSSHBackend | |
| CBenchmarkSet | A set of benchmarks from some common base directory |
| CBenchmarkResult | Results for a single benchmark run |
| CCSVWriter | Writes results to a csv file |
| CDatabase | Dummy database that effectively disables storing to database. Set BENCHMAX_DATABASE to actually use a database |
| CDBAL | |
| CResults | Stores results for for whole benchmax run |
| CXMLWriter | Writes results to a xml file |
| CSettingsParser | Generic class to manage settings parsing using boost::program_options |
| CMathSAT | Tool wrapper for MathSAT for SMT-LIB |
| CMinisat | Tool wrapper for a Minisat solver |
| CMinisatp | Tool wrapper for the Minisatp solver for pseudo-Boolean problems |
| Csimple_parser | |
| CSMTRAT | Tool wrapper for SMT-RAT for SMT-LIB |
| CSMTRAT_Analyzer | Tool wrapper for SMT-RAT for SMT-LIB |
| CSMTRAT_OPB | Adapts the SMTRAT solver for OPB files |
| CTool | Base class for any tool |
| CZ3 | Tool wrapper for Z3 for SMT-LIB |
| Ncarl | |
| ►NMinisat | |
| CRegionAllocator | |
| CHeap | |
| CHash | |
| CEqual | |
| CDeepHash | |
| CDeepEqual | |
| ►CMap | |
| CPair | |
| ►COption | |
| COptionLt | |
| CIntRange | |
| CInt64Range | |
| CDoubleRange | |
| CDoubleOption | |
| CIntOption | |
| CStringOption | |
| CBoolOption | |
| CQueue | |
| CLit | |
| Clbool | |
| CClause | |
| CClauseAllocator | |
| COccLists | |
| ►CCMap | |
| CCRefHash | |
| CWatcher | [Minisat related code] |
| CLessThan_default | |
| Cvec | |
| COutOfMemoryException | |
| ►Nsmtrat | Class to create the formulas for axioms |
| ►Nanalyzer | |
| CProjector | |
| CSettingsCollins | |
| CSettingsHong | |
| CSettingsMcCallum | |
| CSettingsMcCallumPartial | |
| CSettingsLazard | |
| CSettingsBrown | |
| CDegreeCollector | |
| CAnalysisSettings | |
| CAnalyzerStatistics | |
| ►Ncad | |
| ►Ndebug | |
| CDotSubgraph | |
| CIDSanitizer | |
| CUnifiedData | |
| CTikzBasePrinter | |
| ►CTikzDAGPrinter | |
| CNode | |
| ►CTikzTreePrinter | |
| CUnifiedNode | |
| CTikzHistoryPrinter | |
| Nfull | |
| Nfull_ec | |
| ►Npreprocessor | |
| COrigins | |
| CAssignmentCollector | |
| CResultantRule | |
| CConstraintUpdate | |
| ►Nprojection | |
| Nbrown | Contains the implementation of Browns projection operator as specified in [3] after Theorem 3.1 |
| Ncollins | Contains the implementation of Collins projection operator as specified in [5] below Theorem 4 |
| Nhong | Contains the implementation of Hongs projection operator as specified in [15] in Section 2.2 |
| Nlazard | Contains the implementation of Lazards projection operator as specified in [Lauard1994] |
| Nmccallum | Contains the implementation of McCallums projection operator as specified in [23] |
| Nmccallum_partial | Contains the implementation of an optimized version McCallums projection operator |
| CReducta | Construct the set of reducta of the given polynomial |
| ►Nprojection_compare | |
| Clevel | |
| Cdegree | |
| Ctype | |
| CProjectionComparator_impl | |
| CProjectionComparator | |
| CProjectionComparator< ProjectionCompareStrategy::D > | |
| CProjectionComparator< ProjectionCompareStrategy::PD > | |
| CProjectionComparator< ProjectionCompareStrategy::SD > | |
| CProjectionComparator< ProjectionCompareStrategy::lD > | |
| CProjectionComparator< ProjectionCompareStrategy::LD > | |
| ►Nsample_compare | Contains comparison operators for samples and associated helpers |
| Clevel | |
| Csize | |
| Cabsvalue | |
| Ctype | |
| CSampleComparator_impl | |
| CSampleComparator | |
| CSampleComparator< Iterator, SampleCompareStrategy::Value > | |
| CSampleComparator< Iterator, SampleCompareStrategy::Type > | |
| CSampleComparator< Iterator, SampleCompareStrategy::T > | |
| CSampleComparator< Iterator, SampleCompareStrategy::TLSA > | |
| CSampleComparator< Iterator, SampleCompareStrategy::TSA > | |
| CSampleComparator< Iterator, SampleCompareStrategy::TS > | |
| CSampleComparator< Iterator, SampleCompareStrategy::LT > | |
| CSampleComparator< Iterator, SampleCompareStrategy::LTA > | |
| CSampleComparator< Iterator, SampleCompareStrategy::LTS > | |
| CSampleComparator< Iterator, SampleCompareStrategy::LTSA > | |
| CSampleComparator< Iterator, SampleCompareStrategy::LS > | |
| CSampleComparator< Iterator, SampleCompareStrategy::S > | |
| ►Nvariable_ordering | |
| CVariableMap | |
| Ctriangular_data | |
| CCAD | |
| CLiftingTree | |
| CSample | |
| CFullSampleComparator | |
| CFullSampleComparator< Iterator, FullSampleCompareStrategy::Value > | |
| CFullSampleComparator< Iterator, FullSampleCompareStrategy::Type > | |
| CFullSampleComparator< Iterator, FullSampleCompareStrategy::T > | |
| CSampleIteratorQueue | |
| CBaseProjection | |
| CPolynomialComparator | |
| CPolynomialLiftingQueue | |
| CProjection | |
| CModelBasedProjection | |
| ►CProjection< Incrementality::FULL, Backtracking::HIDE, Settings > | |
| CProjectionCandidateComparator | |
| CQueueEntry | |
| ►CProjection< Incrementality::FULL, BT, Settings > | |
| CProjectionCandidateComparator | |
| ►CPurgedPolynomials | |
| CPurgedLevel | |
| CQueueEntry | |
| CModelBasedProjection< Incrementality::NONE, Backtracking::ORDERED, Settings > | This class implements a projection that supports no incrementality and expects backtracking to be in order |
| CProjection< Incrementality::NONE, Backtracking::ORDERED, Settings > | This class implements a projection that supports no incrementality and expects backtracking to be in order |
| CProjection< Incrementality::NONE, Backtracking::UNORDERED, Settings > | This class implements a projection that supports no incrementality and allows backtracking to be out of order |
| ►CProjection< Incrementality::SIMPLE, BT, Settings > | |
| CPolynomialComparator | |
| CQueueEntry | |
| ►CProjectionGlobalInformation | |
| CECData | |
| ►CProjectionLevelInformation | |
| CEquationalConstraint | |
| CEquationalConstraints | |
| CLevelInfo | |
| ►CProjectionPolynomialInformation | |
| CPolyInfo | |
| CProjectionInformation | |
| CProjectionOperator | |
| CBaseSettings | |
| ►CCADConstraints | |
| CConstraintComparator | |
| CCADCore | |
| CCADCore< CoreHeuristic::BySample > | |
| CCADCore< CoreHeuristic::PreferProjection > | |
| CCADCore< CoreHeuristic::PreferSampling > | |
| CCADCore< CoreHeuristic::Interleave > | |
| CCADCore< CoreHeuristic::EnumerateAll > | |
| CCADPreprocessorSettings | |
| CCADPreprocessor | |
| CConflictGraph | Representation of a bipartite graph (C+S, E) of vertices C and S, representing the constraints and samples, respectively |
| CMISGeneration | |
| ►COrigin | This class represents one or more origins of some object |
| CBaseType | |
| CPreprocessorSettings | |
| CPreprocessor | |
| CIncrementalityMixin | Mixin that provides settings for incrementality and backtracking |
| CProjectionMixin | Mixin that provides settings for the projection operator |
| CSampleCompareMixin | Mixin that provides settings for the sample comparison |
| CProjectionOrderMixin | Mixin that provides settings for the projection order |
| CMISHeuristicMixin | Mixin that provides settings for MIS generation |
| ►Ncadcells | A framework for sample-based CAD algorithms |
| Nalgorithms | Various algorithms as well as helper functions for developing new algorithms |
| ►Ndatastructures | Main datastructures |
| ►Ndetail | |
| CPolyProperties | |
| CAssignmentProperties | |
| CTaggedIndexedRoot | |
| CDelineationInterval | An interval of a delineation |
| CDelineation | Represents the delineation of a set of polynomials (at a sample), that is |
| CBaseDerivation | A BaseDerivation has a level and a set of properties of this level, and an underlying derivation representing the lower levels |
| CDelineatedDerivation | A DelineatedDerivation is a BaseDerivation with a Delineation and an underlying SampledDerivation |
| CSampledDerivation | A SampledDerivation is a DelineatedDerivation with a sample and an DelineationInterval w.r.t |
| CDerivationRef | A reference to a derivation, which is either |
| CPolyRef | Refers to a polynomial |
| CPolyConstraint | |
| ►CPolyPool | A pool for polynomials |
| CElement | |
| Celement_less | |
| CProjections | Encapsulates all computations on polynomials |
| Cproperty_hash | |
| CPropertiesTContent | |
| CPropertiesTContent< T, true > | |
| CPropertiesTContent< T, false > | |
| CPropertiesT | Set of properties |
| CPropertiesT< T, Ts... > | |
| CCellRepresentation | Represents a cell |
| CCoveringRepresentation | Represents a covering over a cell |
| CIndexedRoot | Represents the i-th root of a multivariate polynomial at its main variable (given an appropriate sample) |
| CPiecewiseLinearInfo | |
| CCompoundMinMax | Represents the minimum function of the contained indexed root functions |
| CCompoundMaxMin | Represents the maximum function of the contained indexed root functions |
| CRootFunction | |
| CBound | Bound type of a SymbolicInterval |
| CSymbolicInterval | A symbolic interal whose bounds are defined by indexed root expressions |
| CCoveringDescription | Describes a covering of the real line by SymbolicIntervals (given an appropriate sample) |
| CIndexedRootRelation | A relation between two roots |
| CIndexedRootOrdering | Describes an ordering of IndexedRoots |
| Nhelper | |
| ►Noperators | Projection operators |
| ►Nproperties | Contains all properties that are stored in a derivation |
| Cpoly_sgn_inv | |
| Cpoly_irreducible_sgn_inv | |
| Cpoly_semi_sgn_inv | |
| Cpoly_irreducible_semi_sgn_inv | |
| Cpoly_ord_inv | |
| Cpoly_del | |
| Cpoly_proj_del | |
| Ccell_connected | |
| Cpoly_ord_inv_base | |
| Croot_ordering_holds | |
| ►Nrules | Implementation of derivation rules |
| Nfilter_util | |
| Nordering_util | |
| CDelineateSettings | |
| CMccallumSettings | |
| CMccallumSettingsComplete | |
| CMccallum | |
| CMccallumFilteredSettings | |
| CMccallumFiltered | |
| CMccallumPdel | |
| ►Nrepresentation | Heuristics for computing representations |
| ►Napproximation | |
| CApxSettings | |
| CCellApproximator | |
| CApxCriteria | |
| ►Nutil | |
| CIntervalCompare | |
| CPolyDelineation | Polynomial decomposition |
| CPolyDelineations | |
| Ccell | Note: If connected(i) holds, then the indexed root ordering must contain an ordering between the interval bounds |
| Ccovering | |
| Ccell< CellHeuristic::BIGGEST_CELL_APPROXIMATION > | |
| Ccell< CellHeuristic::BIGGEST_CELL > | |
| Ccell< CellHeuristic::BIGGEST_CELL_PDEL > | |
| Ccell< CellHeuristic::BIGGEST_CELL_FILTER > | |
| Ccell< CellHeuristic::BIGGEST_CELL_FILTER_ONLY_INDEPENDENT > | |
| Ccell< CellHeuristic::CHAIN_EQ > | |
| Ccell< CellHeuristic::LOWEST_DEGREE_BARRIERS_EQ > | |
| Ccell< CellHeuristic::LOWEST_DEGREE_BARRIERS > | |
| Ccell< CellHeuristic::LOWEST_DEGREE_BARRIERS_CACHE_GLOBAL > | |
| Ccell< CellHeuristic::LOWEST_DEGREE_BARRIERS_PDEL > | |
| Ccell< CellHeuristic::LOWEST_DEGREE_BARRIERS_FILTER > | |
| Ccell< CellHeuristic::LOWEST_DEGREE_BARRIERS_FILTER_ONLY_INDEPENDENT > | |
| Ccovering< CoveringHeuristic::BIGGEST_CELL_COVERING > | |
| Ccovering< CoveringHeuristic::LDB_COVERING > | |
| Ccovering< CoveringHeuristic::LDB_COVERING_CACHE > | |
| Ccovering< CoveringHeuristic::LDB_COVERING_CACHE_GLOBAL > | |
| Ccovering< CoveringHeuristic::BIGGEST_CELL_COVERING_PDEL > | |
| Ccovering< CoveringHeuristic::BIGGEST_CELL_COVERING_FILTER > | |
| Ccovering< CoveringHeuristic::BIGGEST_CELL_COVERING_FILTER_ONLY_INDEPENDENT > | |
| Ccovering< CoveringHeuristic::BIGGEST_CELL_COVERING_MIN_TDEG > | |
| Ccovering< CoveringHeuristic::CHAIN_COVERING > | |
| Ncompile_information | Compile time generated information about compiler and system version |
| ►Ncovering_ng | |
| ►Nformula | |
| ►Ncomplexity | |
| Nfeatures | |
| ►Nformula_ds | |
| Coverloaded | |
| CFormulaClassification | |
| CTRUE | |
| CFALSE | |
| CNOT | |
| CAND | |
| COR | |
| CIFF | |
| CXOR | |
| CBOOL | |
| CCONSTRAINT | |
| CFormula | |
| CFormulaGraph | |
| ►Npp | |
| CPolyInfo | |
| CGraphEvaluation | |
| ►Nvariables | |
| Nimpl | |
| Csampling | |
| Csampling< SamplingAlgorithm::LOWER_UPPER_BETWEEN_SAMPLING > | First checks lower bound and then upper bound, then checks between the cells if they are covered |
| Csampling< SamplingAlgorithm::LOWER_UPPER_BETWEEN_SAMPLING_AVOID_RAN > | First checks lower bound and then upper bound, then checks between the cells if they are covered (defers choosing interval endpoints as much as possible) |
| CIntervalCompare | Sorts interval by their lower bounds |
| CCoveringResult | |
| CParameterTree | |
| CVariableQuantification | |
| ►Nexecution | |
| CAssertion | |
| CSoftAssertion | |
| CObjective | |
| CExecutionState | |
| ►Nexpression | |
| ►Nsimplifier | |
| CBaseSimplifier | |
| CDuplicateSimplifier | |
| CMergeSimplifier | |
| CNegationSimplifier | |
| CSimplifierChainCaller | |
| CSimplifierChainCaller< 0 > | |
| CSimplifier | |
| CSingletonSimplifier | |
| CExpression | |
| CITEExpression | |
| CQuantifierExpression | |
| CUnaryExpression | |
| CBinaryExpression | |
| CNaryExpression | |
| CExpressionContent | |
| CExpressionTypeChecker | |
| CExpressionConverter | |
| CExpressionPool | |
| CExpressionVisitor | |
| CExpressionModifier | |
| ►Nfmplex | |
| CVariableIndex | |
| ►CFMplexElimination | |
| Ccmp_row | |
| ►CMatrix | |
| Ccol_iterator | |
| Ccol_view | |
| CColEntry | |
| Crow_iterator | |
| Crow_view | |
| CRowEntry | |
| CNode | |
| Ngroebner | |
| Nhelper | |
| ►Nicp | |
| CContractionCandidate | |
| CcontractionCandidateComp | |
| CContractionCandidateManager | |
| CHistoryNode | |
| CIcpVariable | |
| CicpVariableComp | |
| ►Ninternal | |
| ►CCoveringNGSettings | |
| Cformula_evaluation | |
| COpSettings | |
| COCSettings | |
| ►CSATSettings | |
| CMCSATSettings | |
| CNewCoveringSettings | |
| ►Nlra | |
| CVariable | |
| ►CBound | Stores a bound, which could be an upper "<= b" or a lower bound ">= b" for a bound value b |
| CInfo | Stores some additional information for a bound |
| CNumeric | |
| CTableauEntry | |
| ►CTableau | |
| CIterator | |
| CLearnedBound | |
| CTableauSettings1 | |
| CTableauSettings2 | |
| CTableauSettings3 | |
| CValue | |
| Nlve | |
| ►Nmaxsmt | Contains strategy implementations for max SMT computations |
| CMaxSMTBackend | |
| CMaxSMTBackend< Solver, MaxSMTStrategy::FU_MALIK_INCREMENTAL > | |
| CMaxSMTBackend< Solver, MaxSMTStrategy::LINEAR_SEARCH > | |
| CMaxSMTBackend< Solver, MaxSMTStrategy::MSU3 > | |
| ►Nmcsat | |
| ►Narithmetic | |
| CAssignmentFinder | |
| CAssignmentFinder_detail | |
| CAssignmentFinder_ctx | |
| CCovering | Semantics: The space is divided into a number of intervals: (-oo,a)[a,a](a,b)[b,b](b,oo) A bit is set if the constraints refutes the corresponding interval |
| CRootIndexer | |
| Nconstraint_type | |
| ►Nfm | A Fourier-Motzkin based backend |
| CBound | |
| CConflictGenerator | |
| CDefaultComparator | Does not order anything |
| CMaxSizeComparator | This heuristic chooses the explanation excluding the largest interval |
| CMinSizeComparator | This heuristic chooses the explanation excluding the smallest interval |
| CMinVarCountComparator | This heuristic tries to minimize the number of variables occuring in the explanation |
| CDefaultSettings | |
| CIgnoreCoreSettings | |
| CExplanation | |
| ►Nicp | |
| CDependencies | |
| CExplanation | |
| CQueueEntry | |
| CIntervalPropagation | |
| ►Nnlsat | |
| Nhelper | |
| CExplanation | |
| ►CExplanationGenerator | |
| CProjectionSettings | |
| ►Nonecell | |
| CBaseSettings | |
| CDefaultSettings | |
| CExplanation | |
| ►Nonecellcad | |
| ►Nlevelwise | |
| CSectionHeuristic1 | |
| CSectionHeuristic2 | |
| CSectionHeuristic3 | |
| CSectorHeuristic1 | |
| CSectorHeuristic2 | |
| CSectorHeuristic3 | |
| CExplanation | |
| CLevelwiseCAD | |
| ►Nrecursive | OneCell Explanation |
| CCoverNullification | |
| CDontCoverNullification | |
| CNoHeuristic | |
| CDegreeAscending | |
| CDegreeDescending | |
| CExplanation | |
| CRecursiveCAD | |
| CRealAlgebraicPoint | Represent a multidimensional point whose components are algebraic reals |
| CTagPoly | Tagged Polynomials |
| CSection | Represent a cell's (closed-interval-boundary) component along th k-th axis |
| CSector | Represent a cell's open-interval boundary object along one single axis by two irreducible, multivariate polynomials of level k |
| COneCellCAD | |
| ►Nsmtaf | |
| CAssignmentFinder | |
| CDefaultSettings | |
| CSMTModule | |
| CAssignmentFinder_SMT | |
| ►Nvariableordering | |
| ►Ndetail | |
| CFeatureCollector | This class manages features that are used to valuate variables on objects |
| CVariableIDs | |
| ►Nvs | |
| ►Nhelper | |
| CTestCandidate | |
| CExplanation | |
| CDefaultSettings | |
| CExplanationGenerator | |
| CSequentialAssignment | |
| CFastParallelExplanation | This explanation executes all given explanation in parallel processes and waits for the fastest explanation, returning the fastest delivered explanation, terminating all other parallel processes |
| CFullParallelExplanation | This explanation executes all given explanation parallel in multiple threads and waits until every single one has finished, returning the result of the first listed explanation |
| CParallelExplanation | |
| CSequentialExplanation | |
| CBookkeeping | Represent the trail, i.e |
| ►CClauseChain | An explanation is either a single clause or a chain of clauses, satisfying the following properties: |
| CLink | |
| CMCSATBackend | |
| CInformationGetter | |
| CTheoryLevel | |
| ►CMCSATMixin | |
| CVarMapping | |
| CVarProperties | |
| CBase | |
| CMCSATSettingsDefault | |
| CMCSATSettingsNL | |
| CMCSATSettingsFMICPVSNL | |
| CMCSATSettingsOC | |
| CMCSATSettingsOCNN | |
| CMCSATSettingsOCNNASC | |
| CMCSATSettingsOCNNDSC | |
| CMCSATSettingsOCLWH11 | |
| CMCSATSettingsOCLWH12 | |
| CMCSATSettingsOCLWH13 | |
| CMCSATSettingsOCLWH21 | |
| CMCSATSettingsOCLWH22 | |
| CMCSATSettingsOCLWH23 | |
| CMCSATSettingsOCLWH31 | |
| CMCSATSettingsOCLWH32 | |
| CMCSATSettingsOCLWH33 | |
| CMCSATSettingsFMICPVSOCLWH11 | |
| CMCSATSettingsFMICPVSOCLWH12 | |
| CMCSATSettingsFMICPVSOCLWH13 | |
| CMCSATSettingsFMICPVSOCNNASC | |
| CMCSATSettingsFMICPVSOCNNDSC | |
| CMCSATSettingsFMICPVSOCPARALLEL | |
| CMCSATSettingsOCPARALLEL | |
| CMCSATSettingsOCNew | |
| CMCSATSettingsFMICPVSOCNew | |
| CMCSATSettingsVSOCNew | |
| CMCSATSettingsFMOCNew | |
| CMCSATSettingsFMICPVSOCNewOC | |
| CMCSATSettingsFMVSOC | |
| CMCSATSettingsFMICPVSOC | |
| CMCSATSettingsFMICPOC | |
| CMCSATSettingsFMNL | |
| CMCSATSettingsVSNL | |
| CMCSATSettingsFMVSNL | |
| CMCSATSettingsICPNL | |
| CMCSAT_AF_NL | |
| CMCSAT_AF_OCNL | |
| CMCSAT_AF_FMOCNL | |
| CMCSAT_AF_FMICPOCNL | |
| CMCSAT_AF_FMICPVSOCNL | |
| CMCSAT_AF_FMVSOCNL | |
| CMCSAT_SMT_FMOCNL | |
| ►Nonecellcad | |
| ►Nrecursive | |
| CSection | Represent a cell's closed-interval-boundary object along one single axis by an irreducible, multivariate polynomial of level k |
| CSector | Represent a cell's open-interval boundary object along one single axis by two irreducible, multivariate polynomials of level k |
| Noptions_detail | |
| ►Nparseformula | |
| CFormulaCollector | |
| ►Nparser | |
| Narithmetic | |
| ►Nconversion | |
| CConverter | |
| CConverter< types::BVTerm > | |
| CConverter< Poly > | |
| CConverter< FormulaT > | |
| CVariantConverter | Converts variants to some type using the Converter class |
| CVariantVariantConverter | Converts variants to another variant type not using the Converter class |
| CVectorVariantConverter | Converts a vector of variants to a vector of some type using the Converter class |
| Ncore | |
| ►Ntypes | |
| CCoreTheory | Types of the core theory |
| CArithmeticTheory | Types of the arithmetic theory |
| CBitvectorTheory | Types of the theory of bitvectors |
| CUninterpretedTheory | Types of the theory of equalities and uninterpreted functions |
| Nuninterpreted | |
| CAttributeValueParser | |
| CAttributeParser | |
| CSkipper | |
| CIdentifierParser | |
| COutputWrapper | |
| CInstructionHandler | |
| CRationalPolicies | Specialization of qi::real_policies for a Rational |
| CNumeralParser | Parses numerals: (0 | [1-9][0-9]*) |
| CDecimalParser | Parses decimals: numeral.0*numeral |
| CHexadecimalParser | Parses hexadecimals: #x[0-9a-fA-F]+ |
| CBinaryParser | Parses binaries: #b[01]+ |
| CStringParser | Parses strings: ".+" with escape sequences \\" and \\\\ |
| CSimpleSymbolParser | Parses symbols: simple_symbol | quoted_symbol where |
| CSymbolParser | |
| CKeywordParser | Parses keywords: :simple_symbol |
| CSMTLIBParser | |
| CParserSettings | |
| CLogicParser | |
| ►CErrorHandler | |
| Cresult | |
| CScriptParser | |
| CSpecConstantParser | |
| CSExpressionParser | |
| CSortParser | |
| CQualifiedIdentifierParser | |
| CSortedVariableParser | |
| CTermParser | |
| CAbstractTheory | Base class for all theories |
| CToRealInstantiator | |
| CArithmeticTheory | Implements the theory of arithmetic, including LRA, LIA, NRA and NIA |
| CAttribute | Represents an Attribute |
| CBitvectorInstantiator | |
| CIndexedBitvectorInstantiator | |
| CUnaryBitvectorInstantiator | |
| CBinaryBitvectorInstantiator | |
| CBitvectorRelationInstantiator | |
| CSingleIndexBitvectorInstantiator | |
| CExtractBitvectorInstantiator | |
| CBitvectorConstantParser | |
| CBitvectorTheory | Implements the theory of bitvectors |
| CEncodingInstantiator | |
| CAtMostInstantiator | |
| CBooleanEncodingTheory | Implements the theory of bitvectors |
| CTheoryError | |
| CIdentifier | |
| CSExpressionSequence | |
| CCoreInstantiator | |
| CNaryCoreInstantiator | |
| CNotCoreInstantiator | |
| CImpliesCoreInstantiator | |
| CCoreTheory | Implements the core theory of the booleans |
| CFunctionInstantiator | |
| CIndexedFunctionInstantiator | |
| CInstantiator | |
| CUserFunctionInstantiator | |
| ►CParserState | |
| CExpressionScope | |
| CScriptScope | |
| ►CTheories | Combines all implemented theories and provides a single interface to interact with all theories at once |
| CConstantAdder | Helper functor for addConstants() method |
| CSimpleSortAdder | Helper functor for addSimpleSorts() method |
| CFixedWidthConstant | Represents a constant of a fixed width |
| CUninterpretedTheory | Implements the theory of equalities and uninterpreted functions |
| ►Nqe | |
| ►Ncad | |
| CCAD | |
| CCADSettings | |
| CCADElimination | |
| CProjection | |
| ►Ncoverings | |
| Nutil | |
| ►CDefaultSettings | |
| Cformula_evaluation | |
| ►Nfm | |
| CFourierMotzkinQE | |
| ►Nfmplex | |
| ►CFMplexQE | |
| Ccmp_row | |
| CNode | |
| ►Nutil | |
| CEquationSubstitution | |
| ►CMatrix | |
| Ccol_iterator | |
| Ccol_view | |
| CColEntry | |
| Crow_iterator | |
| Crow_view | |
| CRowEntry | |
| CSubquery | |
| CVariableIndex | |
| ►Nresource | |
| CLimiter | |
| ►Nsat | |
| ►Ndetail | |
| CClauseChecker | |
| ►Nsettings | |
| CCoreSettings | |
| CSolverSettings | |
| CModuleSettings | |
| CSettings | |
| ►Nstatistics | |
| CStatisticsSettings | |
| ►Nsubtropical | Implements data structures and encodings for the subtropical method |
| CMoment | Represents the normal vector component and the sign variable assigned to a variable in an original constraint |
| CVertex | Represents a term of an original constraint and assigns him a rating variable if a weak separator is searched |
| CSeparator | Represents the class of all original constraints with the same left hand side after a normalization |
| CEncoding | |
| ►Nunsatcore | Contains strategy implementations for unsat core computations |
| CUnsatCoreBackend | |
| CUnsatCoreBackend< Solver, UnsatCoreStrategy::ModelExclusion > | Implements an easy strategy to obtain an unsatisfiable core |
| ►Nvalidation | |
| CValidationCollector | |
| CValidationPoint | |
| CValidationPrinter | |
| CValidationSettings | |
| ►Nvb | |
| ►CVariable | Class for a variable |
| CboundPointerComp | Compares two pointers showing to bounds |
| CBound | Class for the bound of a variable |
| CVariableBounds | Class to manage the bounds of a variable |
| ►Nvs | |
| CCondition | |
| CunsignedTripleCmp | |
| CState | |
| CSubstitution | |
| CsubstitutionPointerEqual | |
| CsubstitutionPointerHash | |
| Cis_variant | States whether a given type is a boost::variant |
| CVariantMap | This class is a specialization of std::map where the keys are of arbitrary type and the values are of type boost::variant |
| CCMakeOptionPrinter | |
| CExecutor | |
| CPriorityQueue | |
| CDynamicPriorityQueue | |
| CSettingsComponents | |
| CSettingsParser | |
| CMaxSMT | |
| CBEModule | |
| CBESettings1 | |
| CBVDirectEncoder | |
| CBVModule | |
| CBVSettings1 | |
| ►CCNFerModule | |
| CSettingsType | |
| CCoCoAGBModule | |
| CCoCoAGBSettings1 | |
| CCoCoAGBSettings2 | |
| CCoveringNGModule | |
| ►CCoveringNGSettingsDefault | |
| Cformula_evaluation | |
| ►CBimap | Container that stores expensive to construct objects and allows the fast lookup with respect to two independent keys within the objects |
| CFirstCompare | Comparator that performs a heterogeneous lookup on the first key |
| CSecondCompare | Comparator that performs a heterogeneous lookup on the second key |
| ►CCSplitModule | |
| CExpansion | Represents the quotients and remainders of a variable in a positional notation to the basis Settings::expansionBase |
| CLAModule | Linear arithmetic module to call for the linearized formula |
| CLinearization | Represents the class of all original constraints with the same left hand side after a normalization |
| CPurification | Represents the substitution variables of a nonlinear monomial in a positional notation to the basis Settings::expansionBase |
| CCSplitSettings1 | |
| ►CCubeLIAModule | |
| CCubification | |
| CCubeLIASettings1 | |
| CCurryModule | |
| CCurrySettings1 | |
| CEMModule | |
| CEMSettings1 | |
| CESModule | |
| CESSettingsDefault | |
| CESSettingsLimitSubstitution | |
| CFPPModule | |
| CFPPSettings1Old | |
| CFPPSettings1 | |
| CFPPSettings2 | |
| CFPPSettings3 | |
| CFPPSettingsPBGroebner | |
| CFPPSettingsPB | |
| CFPPSettingsOptimization | |
| CGBModule | A solver module based on Groebner basis |
| CGBModuleState | A class to save the current state of a GBModule |
| CGBSettings5 | |
| CGBSettings3 | |
| CGBSettings1 | |
| CGBSettings4 | |
| CGBSettings6 | |
| CGBSettings41 | |
| CGBSettings51 | |
| CGBSettings51A | |
| CGBSettings61 | |
| CGBSettings61A | |
| CGBSettings43 | |
| CGBSettings63 | |
| CdecidePassingPolynomial | |
| CInequalitiesTable | Datastructure for the GBModule |
| CVariableRewriteRule | |
| CGBPPModule | |
| CGBPPSettings1 | |
| ►CForwardHyperGraph | This class implements a forward hypergraph |
| CEdge | Internal type of an edge |
| CCycleEnumerator | This class encapsulates an algorithm for enumerating all cycles |
| ►CICEModule | |
| CCoefficient | |
| CCycleCollector | |
| CEdgeProperty | |
| CICESettings1 | |
| ►CICPModule | |
| Ccomp | Typedefs: |
| CformulaPtrComp | |
| ClinearVariable | |
| Cweights | |
| CICPSettings1 | |
| CICPSettings2 | |
| CICPSettings3 | |
| CICPSettings4 | |
| CIncWidthModule | |
| CIncWidthSettings1 | |
| CIncWidthSettings2 | |
| CIncWidthSettings3 | |
| CBVAnnotation | |
| CAnnotatedBVTerm | |
| CBlastedPoly | |
| CBlastedConstr | |
| CConstrTree | |
| CElementWithOrigins | |
| CCollectionWithOrigins | |
| CIntBlastModule | |
| CIntBlastSettings1 | |
| CIntBlastSettings2 | |
| CPolyTree | |
| CPolyTreeContent | |
| CPolyTreePool | |
| CIntEqModule | A module which checks whether the equations contained in the received (linear integer) formula have a solution |
| CIntEqSettings1 | |
| ►CLRAModule | A module which performs the Simplex method on the linear part of it's received formula |
| CContext | Stores a formula, being part of the received formula of this module, and the position of this formula in the passed formula |
| ►CLRASettings1 | |
| CTableau_settings | |
| ►CLRASettings2 | |
| CTableau_settings | |
| ►CLRASettingsICP | |
| CTableau_settings | |
| CLVEModule | |
| CLVESettings1 | |
| CMCBModule | |
| CMCBSettings1 | |
| CNewCADModule | |
| CNewCADBaseSettings | |
| CNewCADSettingsNaive | |
| CNewCADSettingsNO | |
| CNewCADSettingsNU | |
| CNewCADSettingsSO | |
| CNewCADSettingsSU | |
| CNewCADSettingsFU | |
| CNewCADBaseProjectionSettings | |
| CNewCADSettingsCollins | |
| CNewCADSettingsHong | |
| CNewCADSettingsMcCallum | |
| CNewCADSettingsMcCallumPartial | |
| CNewCADSettingsLazard | |
| CNewCADSettingsBrown | |
| CNewCADBasePPSettings | |
| CNewCADSettingsPP | |
| CNewCADSettingsPPVE | |
| CNewCADSettingsPPRR | |
| CNewCADSettingsPPVERR | |
| CNewCADBaseSettingsLO | |
| CNewCADSettings_LOType | |
| CNewCADSettings_LOT | |
| CNewCADSettings_LOTLSA | |
| CNewCADSettings_LOTSA | |
| CNewCADSettings_LOTS | |
| CNewCADSettings_LOLT | |
| CNewCADSettings_LOLTA | |
| CNewCADSettings_LOLTS | |
| CNewCADSettings_LOLTSA | |
| CNewCADSettings_LOLS | |
| CNewCADSettings_LOS | |
| CNewCADBaseSettingsPO | |
| CNewCADSettings_POD | |
| CNewCADSettings_POPD | |
| CNewCADSettings_POSD | |
| CNewCADSettings_POlD | |
| CNewCADSettings_POLD | |
| CNewCADSettingsF1 | |
| CNewCADSettingsFO1 | |
| CNewCADSettingsFOS | |
| CNewCADSettingsInterleave | |
| CNewCADSettingsEQ_B | |
| CNewCADSettingsEQ_BD | |
| CNewCADSettingsEQ_R | |
| CNewCADSettingsEQ_RD | |
| CNewCADSettingsEQ_RI | |
| CNewCADSettingsEQ_RID | |
| CNewCADSettingsEQ_S | |
| CNewCADSettingsEQ_SD | |
| CNewCADSettingsEQ_BR | |
| CNewCADSettingsEQ_BRD | |
| CNewCADSettingsEQ_BRI | |
| CNewCADSettingsEQ_BRID | |
| CNewCADSettingsEQ_BS | |
| CNewCADSettingsEQ_BSD | |
| CNewCADSettingsEQ_SI | |
| CNewCADSettingsEQ_SID | |
| CNewCADSettingsEQ_BSI | |
| CNewCADSettingsEQ_BSID | |
| CNewCADSettingsFV | |
| CNewCADSettingsFOV | |
| CNewCADSettingsMISBase | |
| CNewCADSettingsMISTrivial | |
| CNewCADSettingsMISGreedy | |
| CNewCADSettingsMISGreedyPre | |
| CNewCADSettingsMISGreedyWeighted | |
| CNewCADSettingsMISExact | |
| CNewCADSettingsMISHybrid | |
| CNewCADSettingsEnumerateAll | |
| CBackend | |
| CSampledDerivationRefCompare | |
| CLevelWiseInformation | |
| CNewCoveringModule | |
| CNewCoveringSettings1 | |
| CNewCoveringSettings2 | |
| CNewCoveringSettings3 | |
| CNewCoveringSettings4 | |
| Csampling | |
| Cis_sample_outside | |
| Csampling< SamplingAlgorithm::LOWER_UPPER_BETWEEN_SAMPLING > | |
| Cis_sample_outside< IsSampleOutsideAlgorithm::DEFAULT > | |
| CNewGBPPModule | |
| CNewGBPPSettings1 | |
| CRationalCapsule | |
| CVariableCapsule | |
| CAxiomFactory | |
| CLOG | |
| CMonomialMappingByVariablePool | |
| CNRAILModule | |
| CNRAILSettings1 | |
| CNRAILSettings2 | |
| CNRAILSettings3 | |
| CNRAILSettings4 | |
| CNRAILSettings5 | |
| CNRAILSettings6 | |
| CNRAILSettings7 | |
| CNRAILSettings8 | |
| CNRAILSettings9 | |
| CNRAILSettings10 | |
| CNRAILSettings11 | |
| CNRAILSettings12 | |
| CNRAILSettings13 | |
| CNRAILSettings14 | |
| CNRAILSettings15 | |
| CNRAILSettings16 | |
| CNRAILSettings17 | |
| CNRAILSettings18 | |
| CNRAILSettings19 | |
| CNRAILSettings20 | |
| CNRAILSettings21 | |
| CNRAILSettings22 | |
| CNRAILSettings23 | |
| CNRAILSettings24 | |
| CNRAILSettings25 | |
| CPBGaussModule | |
| CPBGaussSettings1 | |
| CCardinalityEncoder | |
| CExactlyOneCommanderEncoder | |
| CLongFormulaEncoder | |
| CMixedSignEncoder | |
| CPseudoBoolEncoder | Base class for a PseudoBoolean Encoder |
| CPseudoBoolNormalizer | |
| CRNSEncoder | |
| CShortFormulaEncoder | |
| CTotalizerEncoder | TotalizerEncoder implements the Totalizer encoding as described in "Incremental Cardinality Constraints for MaxSAT" by Martins et al https://doi.org/10.1007/978-3-319-10428-7_39 |
| CTotalizerTree | |
| CPBPPModule | |
| CPBPPSettingsBase | |
| CPBPPSettingsLIAOnly | |
| CPBPPSettings1 | |
| CPBPPSettingsLIAOnlyWithNormalize | |
| CPBPPSettingsWithNormalize | |
| CPBPPSettingsCardinalityOnly20 | |
| CPBPPSettingsCardinalityOnly05 | |
| CPBPPSettingsFull20 | |
| CPBPPSettingsFull05 | |
| CPBPPSettingsCardinalityOnly20Normalize | |
| CPBPPSettingsCardinalityOnly05Normalize | |
| CPBPPSettingsWithRNS | |
| CPBPPSettingsWithCardConstr | |
| CPBPPSettingsWithMixedConstr | |
| CPBPPSettingsBasic | |
| CPBPPSettingsMaxSMT | |
| CPFEModule | |
| CPFESettings1 | |
| ►CPNFerModule | |
| CSettingsType | |
| CVarSchedulerMcsatBase | Base class for all MCSAT variable scheduler |
| CTheoryVarSchedulerStatic | Schedules theory variables statically |
| CVarSchedulerMcsatBooleanFirst | Variable scheduling that all decides Boolean variables first before deciding any theory variable |
| CVarSchedulerMcsatTheoryFirst | Variable scheduling that all decides theory variables first before deciding any Boolean variable |
| CVarSchedulerMcsatUnivariateConstraintsOnly | Decides only Constraints univariate in the current theory variable while the theory ordering is static |
| ►CVarSchedulerMcsatUnivariateClausesOnly | Decides only Constraints occuring in clauses that are univariate in the current theory variable while the theory ordering is static |
| CTheoryLevel | |
| CVarSchedulerMcsatActivityPreferTheory | Activity-based scheduler preferring initially theory variables |
| ►CSATModule | Implements a module performing DPLL style SAT checking |
| CAbstraction | Stores all information regarding a Boolean abstraction of a constraint |
| CClauseInformation | |
| CCNFInfos | |
| Clemma_lt | |
| CLiteralClauses | |
| ►CUnorderedClauseLookup | |
| CUnorderedClauseHasher | |
| CVarData | Stores information about a Minisat variable |
| CVarOrderLt | |
| CWatcherDeleted | [Minisat related code] |
| CSATSettings1 | |
| CSATSettings3 | |
| CSATSettingsStopAfterUnknown | |
| CSATSettingsMCSAT | |
| CSATSettingsMCSATDefault | |
| CSATSettingsMCSATOC | |
| CSATSettingsMCSATFMICPVSOC | |
| CSATSettingsMCSATFMICPOC | |
| CSATSettingsMCSATOCNew | |
| CSATSettingsMCSATFMICPVSOCNew | |
| CSATSettingsMCSATFMICPVSOCNewOC | |
| CSATSettingsMCSATFMICPVSOCLWH12 | |
| CSATSettingsMCSATNL | |
| CSATSettingsMCSATFMICPVSNL | |
| CSATSettingsMCSATVSOCNew | |
| CSATSettingsMCSATFMOCNew | |
| CVarSchedulerBase | Base class for variable schedulers |
| ►CVarSchedulerMinisat | Minisat's activity-based variable scheduling |
| CVarOrderLt | |
| CVarSchedulerFixedRandom | |
| CVarSchedulerRandom | Random scheduler |
| CVarSchedulerSMTTheoryGuided | Scheduler for SMT, implementing theory guided heuristics |
| CSplitSOSModule | |
| CSplitSOSSettings1 | |
| ►CSTropModule | |
| CLAModule | Linear arithmetic module to call for the linearized formula |
| CSeparatorGroup | Represents the class of all original constraints with the same left hand side after a normalization |
| CSTropSettings1 | Take conjunctions incrementally, construct linear formulas for LRA solver |
| CSTropSettings2 | |
| CSTropSettings3 | Transform to NNF then replace each constraint with its linear formula (equations become FALSE). Then let LRA solver solve |
| CSTropSettings3b | Transform to NNF then replace each constraint with its linear formula (equations become FALSE). Then let LRA solver solve |
| CSTropSettings2OutputOnly | |
| CSTropSettings3OutputOnly | |
| CSTropSettings3bOutputOnly | |
| CSymmetryModule | |
| CSymmetrySettings1 | |
| CVSModule | |
| CVSSettings1 | |
| CVSSettings234 | |
| ►COptimization | |
| CObjective | |
| CManager | Base class for solvers |
| CBranching | Stores all necessary information of an branch, which can be used to detect probable infinite loop of branchings |
| ►CModule | A base class for all kind of theory solving methods |
| CLemma | |
| CModuleStatistics | |
| CTheoryPropagation | |
| CFormulaWithOrigins | Stores a formula along with its origins |
| ►CModuleInput | The input formula a module has to consider for it's satisfiability check |
| CIteratorCompare | |
| CPModule | |
| CAbstractModuleFactory | |
| CModuleFactory | |
| CBackendLink | |
| CStrategyGraph | |
| CTask | |
| CBackendSynchronisation | |
| CThreadPool | |
| CAllModulesStrategy | |
| CBVPreprocessing | Strategy description |
| CBVSolver | Strategy description |
| CCoveringNG_Default | The most efficient CoveringNG strategy with preprocessing |
| CCoveringNG_GBDefault | |
| CCoveringNG_PPBooleanExploration | |
| CCoveringNG_PPBooleanExplorationOnlyBool | |
| CCoveringNG_PPBooleanExplorationWithBool | |
| CCoveringNG_PPBooleanOff | |
| CCoveringNG_PPBooleanPartialPropagationSotd | |
| CCoveringNG_PPBooleanPartialPropagationTdeg | |
| CCoveringNG_PPBooleanPropagation | |
| CCoveringNG_PPDefault | The most efficient CoveringNG strategy with preprocessing |
| CCoveringNG_PPFilterBoundsOnly | |
| CCoveringNG_PPFilterBoundsOnlyComplete | |
| CCoveringNG_PPFilterNoop | |
| CCoveringNG_PPGBDefault | |
| CCoveringNG_PPImplicantsLevelSize | |
| CCoveringNG_PPImplicantsLevelSotd | |
| CCoveringNG_PPImplicantsPickeringTotal | |
| CCoveringNG_PPImplicantsSizeOnly | |
| CCoveringNG_PPImplicantsSotd | |
| CCoveringNG_PPImplicantsSotdReverse | |
| CCoveringNG_PPImplicantsTdeg | |
| CCoveringNG_PPImplicantsVars | |
| CCoveringNG_PPImplicantsVarsVarorderSplitting | |
| CCoveringNG_PPInprocessingOn | |
| CCoveringNG_PPSTropDefault | The most efficient CoveringNG strategy with preprocessing and subtropical |
| CCoveringNG_PPVarorderPickering | |
| CCoveringNG_PPVarorderUnivariate | |
| CCSplitFull | |
| CCSplitOnly | |
| CDefault | The default SMT-RAT strategy |
| CDefaultTwo | The default SMT-RAT strategy |
| CFilter_BCAll | |
| CFilter_BCBc | |
| CFilter_BCBoundsOnly | |
| CFilter_BCDeg10 | |
| CFilter_BCDeg2 | |
| CFilter_BCDeg5 | |
| CFilter_BCIndep | |
| CFilter_BCIntersect | |
| CFilter_BCIrred | |
| CFilter_BCIrredIndep | |
| CFilter_BCNoop | |
| CFilter_BCRational | |
| CFilter_LDBBoundsOnly | |
| CFilter_LDBNoop | |
| CLIASolver | Strategy description |
| CLRASolver | Strategy description |
| CMAXSATBackendStrategy | This strategy is used as a artificial backend in the MaxSMT Module |
| CPBPPStrategy | |
| CMCSAT_FMICPOC | |
| CMCSAT_FMICPVSNL | |
| CMCSAT_FMICPVSOC | |
| CMCSAT_FMICPVSOCLWH11 | |
| CMCSAT_FMICPVSOCLWH12 | |
| CMCSAT_FMICPVSOCLWH13 | |
| CMCSAT_FMICPVSOCNew | |
| CMCSAT_FMICPVSOCNewOC | |
| CMCSAT_FMICPVSOCNNASC | |
| CMCSAT_FMICPVSOCNNDSC | |
| CMCSAT_FMICPVSOCPARALLEL | |
| CMCSAT_FMNL | |
| CMCSAT_FMOCNew | |
| CMCSAT_FMVSNL | |
| CMCSAT_FMVSOC | |
| CMCSAT_ICPNL | |
| CMCSAT_NL | |
| CMCSAT_OC | |
| CMCSAT_OCLWH11 | |
| CMCSAT_OCLWH12 | |
| CMCSAT_OCLWH13 | |
| CMCSAT_OCLWH21 | |
| CMCSAT_OCLWH22 | |
| CMCSAT_OCLWH23 | |
| CMCSAT_OCLWH31 | |
| CMCSAT_OCLWH32 | |
| CMCSAT_OCLWH33 | |
| CMCSAT_OCNew | |
| CMCSAT_OCNewBC | |
| CMCSAT_OCNewLDB | |
| CMCSAT_OCNewLDBCovering | |
| CMCSAT_OCNewLDBCoveringCache | |
| CMCSAT_OCNewLDBCoveringCacheGlobal | |
| CMCSAT_OCNN | |
| CMCSAT_OCNNASC | |
| CMCSAT_OCNNDSC | |
| CMCSAT_OCPARALLEL | |
| CMCSAT_PPDefault | |
| CMCSAT_PPNL | |
| CMCSAT_PPOC | |
| CMCSAT_PPOCNew | |
| CMCSAT_VSNL | |
| CMCSAT_VSOCNew | |
| CMIS_Exact | |
| CMIS_Greedy | |
| CMIS_Trivial | |
| CMIS_GreedyPre | |
| CMIS_GreedyWeighted | |
| CMIS_Hybrid | |
| CNewCAD_Brown | |
| CNewCAD_Collins | |
| CNewCAD_FOS | |
| CNewCAD_FU | |
| CNewCAD_FU_SC | |
| CNewCAD_FU_SI | |
| CNewCAD_FU_SInf | |
| CNewCAD_FU_SL | |
| CNewCAD_FU_SR | |
| CNewCAD_FU_SZ | |
| CNewCAD_Hong | |
| CNewCAD_LOLS | |
| CNewCAD_LOLT | |
| CNewCAD_LOLTA | |
| CNewCAD_LOLTS | |
| CNewCAD_LOLTSA | |
| CNewCAD_LOS | |
| CNewCAD_LOT | |
| CNewCAD_LOTLSA | |
| CNewCAD_LOTS | |
| CNewCAD_LOTSA | |
| CNewCAD_McCallum | |
| CNewCAD_McCallumPartial | |
| CNewCAD_Naive | |
| CNewCAD_NO | |
| CNewCAD_NU | |
| CNewCAD_Only | |
| CNewCAD_POD | |
| CNewCAD_POLD | |
| CNewCAD_POPD | |
| CNewCAD_POSD | |
| CNewCAD_PP | |
| CNewCAD_PPRR | |
| CNewCAD_PPVE | |
| CNewCAD_PPVERR | |
| CNewCAD_SAT | |
| CNewCAD_SO | |
| CNewCAD_SU | |
| CNewCADEQ_B | |
| CNewCADEQ_BD | |
| CNewCADEQ_BR | |
| CNewCADEQ_BRD | |
| CNewCADEQ_BRI | |
| CNewCADEQ_BRID | |
| CNewCADEQ_BS | |
| CNewCADEQ_BSD | |
| CNewCADEQ_BSI | |
| CNewCADEQ_BSID | |
| CNewCADEQ_R | |
| CNewCADEQ_RD | |
| CNewCADEQ_RI | |
| CNewCADEQ_RID | |
| CNewCADEQ_S | |
| CNewCADEQ_SD | |
| CNewCADEQ_SI | |
| CNewCADEQ_SID | |
| CNewCovering_Backtracking | |
| CNewCovering_FilterBoundsOnly | |
| CNewCovering_Incomplete | |
| CNewCovering_Incremental | |
| CNewCovering_IncrementalBacktracking | |
| CNewCovering_PPComplete | |
| CNewCovering_PPFilterBoundsOnly | |
| CNewCovering_PPFilterBoundsOnlyComplete | |
| CNewCovering_PPIncomplete | |
| CNewCovering_Vanilla | |
| CNIABB | Strategy description |
| CNIABlast | Strategy description |
| CNIASolver | Strategy description |
| CNRA_CAD | Strategy description |
| CNRA_ICPVSCAD | Strategy description |
| CNRA_LRAVSCAD | Strategy description |
| CNRA_VSCAD | Strategy description |
| CNRARefinement_Solver | Strategy description |
| CNRARefinement_Solver1 | Strategy description |
| CNRARefinement_Solver10 | Strategy description |
| CNRARefinement_Solver11 | Strategy description |
| CNRARefinement_Solver12 | Strategy description |
| CNRARefinement_Solver13 | Strategy description |
| CNRARefinement_Solver14 | Strategy description |
| CNRARefinement_Solver15 | Strategy description |
| CNRARefinement_Solver16 | Strategy description |
| CNRARefinement_Solver17 | Strategy description |
| CNRARefinement_Solver18 | Strategy description |
| CNRARefinement_Solver19 | Strategy description |
| CNRARefinement_Solver2 | Strategy description |
| CNRARefinement_Solver20 | Strategy description |
| CNRARefinement_Solver21 | Strategy description |
| CNRARefinement_Solver22 | Strategy description |
| CNRARefinement_Solver23 | Strategy description |
| CNRARefinement_Solver24 | Strategy description |
| CNRARefinement_Solver25 | Strategy description |
| CNRARefinement_Solver3 | Strategy description |
| CNRARefinement_Solver4 | Strategy description |
| CNRARefinement_Solver5 | Strategy description |
| CNRARefinement_Solver6 | Strategy description |
| CNRARefinement_Solver7 | Strategy description |
| CNRARefinement_Solver8 | Strategy description |
| CNRARefinement_Solver9 | Strategy description |
| CNRASolver | Strategy description |
| CNRASolverCov | Strategy description |
| COnlyCAD | |
| COnlyGB | |
| COnlySAT | A pure SAT solver |
| COnlySATPP | A pure SAT solver with preprocessing |
| COnlyVS | Strategy description |
| COptimizationPreprocessing | |
| COptimizationStrategy | A backend compatible with optimization |
| CPBPPStrategy2 | |
| CPBPPStrategyBasic | |
| CPBPPStrategyGauss | |
| CPBPPStrategyGroebner | |
| CPBPPStrategyLIAOnly | |
| CPBPPStrategyRNS | |
| CPBPPStrategyWithCardConstr | |
| CPBPPStrategyWithMixedConstr | |
| CPBPreprocessing | Strategy description |
| CPBPreprocessingGroebner | |
| CPreprocessingOne | Strategy description |
| CPreprocessingTwo | Strategy description |
| CPBPPStrategyGroe_Norm_PB_LIA | |
| CPBPPStrategyGroe_PB_LIA | |
| CPBPPStrategyLIA | |
| CPBPPStrategyLIA_ICP | |
| CPBPPStrategyLIA_VS | |
| CPBPPStrategyNorm_LIA | |
| CPBPPStrategyNorm_LIA_ICP | |
| CPBPPStrategyNorm_LIA_VS | |
| CPBPPStrategyNorm_PB_LIA | |
| CPBPPStrategyPB_LIA | |
| CRatIntBlast | Strategy description |
| CSMTCOMP | Strategy description |
| CSTrop_BackendsOnly | Strategy description |
| CSTrop_CADBackendsOnly | Strategy description |
| CSTrop_Formula | |
| CSTrop_FormulaAlt | |
| CSTrop_FormulaAltOutputOnly | |
| CSTrop_FormulaAltWCADBackends | |
| CSTrop_FormulaAltWCADBackendsFull | |
| CSTrop_FormulaOutputOnly | |
| CSTrop_FormulaWBackends | |
| CSTrop_FormulaWBackendsFull | |
| CSTrop_FormulaWCADBackends | |
| CSTrop_FormulaWCADBackendsFull | |
| CSTrop_FormulaWMCSAT | |
| CSTrop_Incremental | |
| CSTrop_IncrementalWBackends | |
| CSTrop_IncrementalWCADBackends | |
| CSTrop_MCSATOnly | |
| CSTrop_TransformationEQ | |
| CSTrop_TransformationEQOutputOnly | |
| CSTrop_TransformationEQWBackends | |
| CSTrop_TransformationEQWCADBackends | |
| CUnsatCore | |
| ►Nstd | STL namespace |
| Chash< std::vector< T > > | |
| Chash_combiner | |
| Chash< smtrat::expression::Expression > | |
| Chash< smtrat::expression::ITEExpression > | |
| Chash< smtrat::expression::QuantifierExpression > | |
| Chash< smtrat::expression::UnaryExpression > | |
| Chash< smtrat::expression::BinaryExpression > | |
| Chash< smtrat::expression::NaryExpression > | |
| Chash< const smtrat::expression::ExpressionContent * > | |
| Chash< smtrat::lra::Variable< T1, T2 > > | Implements std::hash for sort value |
| Chash< smtrat::vs::Substitution > | |
1.9.1