- r -

• RandomizationAdaptor() : benchmax::RandomizationAdaptor< T >
• randomized() : benchmax::Jobs
• rAssignment() : smtrat::lra::Variable< T1, T2 >
• rating() : smtrat::subtropical::Vertex
• RatIntBlast() : smtrat::RatIntBlast
• RationalCapsule() : smtrat::RationalCapsule
• rbegin() : smtrat::ModuleInput
• rCannotBeSolved() : smtrat::vs::State
• rCannotBeSolvedLazy() : smtrat::vs::State
• rChildren() : smtrat::vs::State
• rConditions() : smtrat::vs::State
• rConflictSets() : smtrat::vs::State
• rConstraintToBound() : smtrat::lra::Tableau< Settings, T1, T2 >
• rContent() : smtrat::lra::Numeric , smtrat::lra::TableauEntry< T1, T2 >
• rDebugOutputChannel() : smtrat::Manager
• read_until() : benchmax::simple_parser
• read_until_whitespace() : benchmax::simple_parser
• read_until_whitespace_or() : benchmax::simple_parser
• real_roots() : smtrat::cadcells::datastructures::Projections
• real_roots_reducible() : smtrat::cadcells::datastructures::Projections
• RealAlgebraicPoint() : smtrat::mcsat::onecellcad::RealAlgebraicPoint< Number >
• reason() : smtrat::SATModule< Settings >
• reasons() : smtrat::cad::preprocessor::AssignmentCollector , smtrat::icp::HistoryNode
• reblastingNeeded() : smtrat::IntBlastModule< Settings >
• rebuild() : smtrat::VarSchedulerBase , smtrat::VarSchedulerMcsatActivityPreferTheory< vot > , smtrat::VarSchedulerMcsatBooleanFirst< vot > , smtrat::VarSchedulerMcsatTheoryFirst< TheoryScheduler > , smtrat::VarSchedulerMcsatUnivariateClausesOnly< TheoryScheduler, respectActivities > , smtrat::VarSchedulerMcsatUnivariateConstraintsOnly< lookahead, vot > , smtrat::VarSchedulerMinisat , smtrat::VarSchedulerRandom , smtrat::VarSchedulerSMTTheoryGuided< theory_conflict_guided_decision_heuristic >
• rebuildActivities() : smtrat::VarSchedulerBase , smtrat::VarSchedulerMcsatActivityPreferTheory< vot > , smtrat::VarSchedulerMcsatBooleanFirst< vot > , smtrat::VarSchedulerMcsatTheoryFirst< TheoryScheduler > , smtrat::VarSchedulerMcsatUnivariateClausesOnly< TheoryScheduler, respectActivities > , smtrat::VarSchedulerMcsatUnivariateConstraintsOnly< lookahead, vot > , smtrat::VarSchedulerMinisat , smtrat::VarSchedulerSMTTheoryGuided< theory_conflict_guided_decision_heuristic >
• rebuildOrderHeap() : smtrat::SATModule< Settings >
• rebuildTheoryVars() : smtrat::TheoryVarSchedulerStatic< vot > , smtrat::VarSchedulerBase , smtrat::VarSchedulerMcsatActivityPreferTheory< vot > , smtrat::VarSchedulerMcsatBooleanFirst< vot > , smtrat::VarSchedulerMcsatTheoryFirst< TheoryScheduler > , smtrat::VarSchedulerMcsatUnivariateClausesOnly< TheoryScheduler, respectActivities > , smtrat::VarSchedulerMcsatUnivariateConstraintsOnly< lookahead, vot >
• receivedFormulaChecked() : smtrat::Module
• receivedFormulasAsInfeasibleSubset() : smtrat::Module
• receivedVariable() : smtrat::Module
• recentlyAdded() : smtrat::vs::Condition
• recheckShrunkPolys() : smtrat::IntBlastModule< Settings >
• reconstructEqSystem() : smtrat::PBGaussModule< Settings >
• reduce() : smtrat::PBGaussModule< Settings >
• reduceDB() : smtrat::SATModule< Settings >
• reduceWRTGroebnerBasis() : smtrat::InequalitiesTable< Settings >
• reduceWRTVariableRewriteRules() : smtrat::InequalitiesTable< Settings >
• Reducta() : smtrat::cad::projection::Reducta< Poly >
• reference() : smtrat::cad::sample_compare::SampleComparator< Iterator, SampleCompareStrategy::Type >
• refineNonNull() : smtrat::mcsat::onecellcad::recursive::RecursiveCAD
• refineNull() : smtrat::mcsat::onecellcad::recursive::RecursiveCAD
• refreshConditions() : smtrat::vs::State
• refreshVariable() : smtrat::parser::AbstractTheory , smtrat::parser::BitvectorTheory
• RegionAllocator() : Minisat::RegionAllocator< T >
• register_hook() : smtrat::cad::CADPreprocessorSettings , smtrat::cad::PreprocessorSettings
• register_settings() : smtrat::cad::CADPreprocessorSettings , smtrat::cad::PreprocessorSettings
• registerFunction() : smtrat::parser::ParserState
• regular() : smtrat::parser::InstructionHandler
• rehash() : Minisat::Map< K, D, H, E >
• relation() : smtrat::ConstrTree
• reloc() : Minisat::ClauseAllocator , smtrat::SATModule< Settings >::LiteralClauses
• relocAll() : smtrat::SATModule< Settings >
• relocate() : Minisat::Clause
• relocateClauses() : smtrat::VarSchedulerBase , smtrat::VarSchedulerMcsatUnivariateClausesOnly< TheoryScheduler, respectActivities >
• relocation() : Minisat::Clause
• reloced() : Minisat::Clause
• remaining_constraints() : smtrat::qe::util::EquationSubstitution
• remaining_variables() : smtrat::qe::util::EquationSubstitution
• remapAndSetLraInfeasibleSubsets() : smtrat::ICPModule< Settings >
• remove() : Minisat::CMap< T > , Minisat::Map< K, D, H, E > , smtrat::cad::CADConstraints< BT > , smtrat::cad::preprocessor::Origins , smtrat::cad::Projection< Incrementality::FULL, BT, Settings >::PurgedPolynomials , smtrat::Manager , smtrat::Module , smtrat::PModule
• remove_annotated_name() : smtrat::UnsatCore< Solver, Strategy >
• remove_job_ids() : benchmax::SlurmBackend
• remove_lra_formula() : smtrat::STropModule< Settings >
• remove_objective() : smtrat::Optimization< Solver >
• remove_root() : smtrat::cadcells::datastructures::Delineation
• remove_roots_with_origin() : smtrat::cadcells::datastructures::Delineation
• remove_soft_formula() : smtrat::MaxSMT< Solver, Strategy >
• removeBound() : smtrat::lra::Tableau< Settings, T1, T2 > , smtrat::lra::Variable< T1, T2 > , smtrat::vb::VariableBounds< T >
• removeBoundRestrictionsFromICP() : smtrat::IntBlastModule< Settings >
• removeCandidateFromRelevant() : smtrat::ICPModule< Settings >
• removeClause() : smtrat::SATModule< Settings >
• removeConstraint() : smtrat::Backend< Settings > , smtrat::cad::CAD< Settings > , smtrat::cad::CADPreprocessor , smtrat::cad::Preprocessor , smtrat::LevelWiseInformation< Settings > , smtrat::NewCADModule< Settings > , smtrat::qe::cad::CAD< Settings >
• removeConstraintsFromReplacer() : smtrat::NewCADModule< Settings >
• removeConstraintsSAT() : smtrat::NewCoveringModule< Settings >
• removeConstraintsUNSAT() : smtrat::NewCoveringModule< Settings >
• removeCore() : smtrat::BVModule< Settings > , smtrat::CoveringNGModule< Settings > , smtrat::CSplitModule< Settings > , smtrat::CubeLIAModule< Settings > , smtrat::CurryModule< Settings > , smtrat::FPPModule< Settings > , smtrat::GBModule< Settings > , smtrat::ICEModule< Settings > , smtrat::ICPModule< Settings > , smtrat::IncWidthModule< Settings > , smtrat::IntBlastModule< Settings > , smtrat::IntEqModule< Settings > , smtrat::LRAModule< Settings > , smtrat::Module , smtrat::NewCADModule< Settings > , smtrat::NewCoveringModule< Settings > , smtrat::NRAILModule< Settings > , smtrat::PBGaussModule< Settings > , smtrat::PBPPModule< Settings > , smtrat::PFEModule< Settings > , smtrat::SATModule< Settings > , smtrat::STropModule< Settings > , smtrat::VSModule< Settings >
• removedConstraint() : smtrat::cad::LiftingTree< Settings >
• removeDerivation() : smtrat::LevelWiseInformation< Settings >
• removeDir() : benchmax::ssh::SSHConnection
• removedPolynomialsFromLevel() : smtrat::cad::LiftingTree< Settings >
• removeDuplicateColumns() : smtrat::cad::ConflictGraph
• removeEC() : smtrat::cad::ProjectionGlobalInformation
• removeECConstraint() : smtrat::cad::ProjectionInformation
• removeEntry() : smtrat::lra::Tableau< Settings, T1, T2 >
• removeEquality() : smtrat::cad::CADPreprocessor
• removeFactors() : smtrat::PFEModule< Settings >
• removeFiltered() : smtrat::cad::Origin
• removeFormula() : smtrat::BVSolver , smtrat::ICEModule< Settings >
• removeFormulaFromICP() : smtrat::IntBlastModule< Settings >
• removeFromICP() : smtrat::IncWidthModule< Settings >
• removeFromProjectionQueue() : smtrat::cad::Projection< Incrementality::FULL, BT, Settings >
• removeIf() : smtrat::PriorityQueue< T, Compare >
• removeInequality() : smtrat::InequalitiesTable< Settings >
• removeLiteralOrigin() : smtrat::SATModule< Settings >
• removeMin() : Minisat::Heap< Comp >
• removeNegative() : smtrat::SATModule< Settings >::LiteralClauses
• removeNextSample() : smtrat::cad::LiftingTree< Settings > , smtrat::cad::SampleIteratorQueue< Iterator, Comparator >
• removeOrigin() : smtrat::CollectionWithOrigins< Element, Origin > , smtrat::ElementWithOrigins< Element, Origin > , smtrat::icp::ContractionCandidate , smtrat::Module , smtrat::ModuleInput , smtrat::SATModule< Settings >::ClauseInformation
• removeOriginalConstraint() : smtrat::icp::IcpVariable
• removeOriginFromBV() : smtrat::IntBlastModule< Settings >
• removeOriginFromICP() : smtrat::IntBlastModule< Settings >
• removeOrigins() : smtrat::CollectionWithOrigins< Element, Origin > , smtrat::Module , smtrat::ModuleInput
• removePolynomial() : smtrat::cad::BaseProjection< Settings > , smtrat::cad::ModelBasedProjection< Incrementality::NONE, Backtracking::ORDERED, Settings > , smtrat::cad::Projection< Incrementality::FULL, Backtracking::HIDE, Settings > , smtrat::cad::Projection< Incrementality::FULL, BT, Settings > , smtrat::cad::Projection< Incrementality::NONE, Backtracking::ORDERED, Settings > , smtrat::cad::Projection< Incrementality::NONE, Backtracking::UNORDERED, Settings > , smtrat::cad::Projection< Incrementality::SIMPLE, BT, Settings > , smtrat::qe::cad::CAD< Settings > , smtrat::qe::cad::Projection< Settings >
• removePolynomialByIT() : smtrat::cad::Projection< Incrementality::FULL, BT, Settings >
• removePositive() : smtrat::SATModule< Settings >::LiteralClauses
• removePositiveCoeff() : smtrat::PseudoBoolNormalizer
• removeProjectionFactor() : smtrat::qe::cad::Projection< Settings >
• removePurgedFromEvaluated() : smtrat::cad::ProjectionLevelInformation::LevelInfo
• removeReceivedFormulaFromNewInequalities() : smtrat::GBModule< Settings >
• removeSatisfied() : smtrat::SATModule< Settings >
• removeSquares() : smtrat::PFEModule< Settings >
• removeSquaresFromStrict() : smtrat::PFEModule< Settings >
• removeStateFromRanking() : smtrat::VSModule< Settings >
• removeStatesFromRanking() : smtrat::vs::State , smtrat::VSModule< Settings >
• removeSubformulaFromPassedFormula() : smtrat::GBModule< Settings >
• removeTheoryPropagation() : smtrat::SATModule< Settings >
• removeUpperBoundOnMinimal() : smtrat::SATModule< Settings >
• rend() : smtrat::ModuleInput
• reorderTree() : smtrat::cad::debug::TikzTreePrinter
• replace() : benchmax::CSVWriter , benchmax::XMLWriter
• replacePlaceholders() : benchmax::DBAL
• res() : smtrat::cadcells::datastructures::Projections
• reserve() : smtrat::fmplex::Matrix , smtrat::qe::util::Matrix
• reset() : smtrat::cad::BaseProjection< Settings > , smtrat::cad::CAD< Settings > , smtrat::cad::CADConstraints< BT > , smtrat::cad::LiftingTree< Settings > , smtrat::cad::ModelBasedProjection< Incrementality::NONE, Backtracking::ORDERED, Settings > , smtrat::cad::Projection< Incrementality::FULL, Backtracking::HIDE, Settings > , smtrat::cad::Projection< Incrementality::FULL, BT, Settings >::PurgedPolynomials , smtrat::cad::Projection< Incrementality::FULL, BT, Settings > , smtrat::cad::Projection< Incrementality::NONE, Backtracking::ORDERED, Settings > , smtrat::cad::Projection< Incrementality::NONE, Backtracking::UNORDERED, Settings > , smtrat::cad::Projection< Incrementality::SIMPLE, BT, Settings > , smtrat::cad::ProjectionGlobalInformation , smtrat::cad::ProjectionInformation , smtrat::cad::ProjectionLevelInformation , smtrat::cad::ProjectionPolynomialInformation , smtrat::execution::ExecutionState , smtrat::Executor< Strategy > , smtrat::icp::HistoryNode , smtrat::IncWidthModule< Settings > , smtrat::Manager , smtrat::MaxSMT< Solver, Strategy > , smtrat::Optimization< Solver > , smtrat::parseformula::FormulaCollector , smtrat::parser::InstructionHandler , smtrat::parser::ParserState , smtrat::parser::SMTLIBParser , smtrat::qe::cad::CAD< Settings > , smtrat::qe::cad::Projection< Settings > , smtrat::resource::Limiter , smtrat::UnsatCore< Solver, Strategy >
• reset_answer() : smtrat::execution::ExecutionState
• reset_assertions() : smtrat::execution::ExecutionState
• resetAssertions() : smtrat::Executor< Strategy > , smtrat::parseformula::FormulaCollector , smtrat::parser::InstructionHandler , smtrat::parser::SMTLIBParser
• resetAssignment() : smtrat::lra::Tableau< Settings, T1, T2 >
• resetCached() : smtrat::cad::CADPreprocessor
• resetCannotBeSolvedLazyFlags() : smtrat::vs::State
• resetConflictSets() : smtrat::vs::State
• resetCurrentRangeSize() : smtrat::vs::State
• resetDerivationToConstraintMap() : smtrat::Backend< Settings >
• resetExpansions() : smtrat::CSplitModule< Settings >
• resetFullSamples() : smtrat::cad::LiftingTree< Settings >
• resetHistory() : smtrat::ICPModule< Settings >
• resetInfinityChild() : smtrat::vs::State
• resetNeqRepresentation() : smtrat::lra::Bound< T1, T2 >
• resetNumberOfPivotingSteps() : smtrat::lra::Tableau< Settings, T1, T2 >
• resetReusagesAfterTargetDiameterReached() : smtrat::icp::ContractionCandidate
• resetStoredData() : smtrat::Backend< Settings >
• resetTheta() : smtrat::lra::Tableau< Settings, T1, T2 >
• resetTimeout() : smtrat::resource::Limiter
• resetVariableAssignment() : smtrat::SATModule< Settings >
• resetWeights() : smtrat::icp::ContractionCandidate
• resizeBVTerm() : smtrat::IntBlastModule< Settings >
• resolve() : smtrat::cad::preprocessor::Origins , smtrat::mcsat::ClauseChain
• resolve_conflict() : smtrat::cad::Preprocessor
• resolveDependencies() : benchmax::Tool
• resolveSymbol() : smtrat::parser::AbstractTheory , smtrat::parser::BitvectorTheory , smtrat::parser::ParserState , smtrat::parser::Theories
• resolveVariable() : smtrat::parser::Theories
• restore() : benchmax::BenchmarkResult , smtrat::cad::PolynomialLiftingQueue< PolynomialGetter > , smtrat::cad::Projection< Incrementality::FULL, BT, Settings >::PurgedPolynomials
• restoreFormula() : smtrat::PBPPModule< Settings >
• restoreRemovedSamples() : smtrat::cad::LiftingTree< Settings >
• restrict_assignment() : smtrat::cadcells::datastructures::Projections
• restrict_base_assignment() : smtrat::cadcells::datastructures::Projections
• restrictEvaluatedToPurged() : smtrat::cad::ProjectionLevelInformation::LevelInfo
• restrictProjection() : smtrat::cad::Projection< Incrementality::FULL, Backtracking::HIDE, Settings >
• result() : smtrat::cad::CADPreprocessor , smtrat::cad::Preprocessor
• ResultantRule() : smtrat::cad::preprocessor::ResultantRule
• reusagesAfterTargetDiameterReached() : smtrat::icp::ContractionCandidate
• revert_valuation() : smtrat::covering_ng::formula::GraphEvaluation
• rewriteVariable() : smtrat::GBModule< Settings >
• rFactor() : smtrat::lra::Variable< T1, T2 >
• rFather() : smtrat::vs::State
• rFlag() : smtrat::vs::Condition
• rHasChildrenToInsert() : smtrat::vs::State
• rHasRecentlyAddedConditions() : smtrat::vs::State
• rhs() : smtrat::icp::ContractionCandidate
• rID() : smtrat::vs::State
• right() : Minisat::Heap< Comp > , smtrat::ConstrTree , smtrat::PolyTree , smtrat::TotalizerTree
• rInconsistent() : smtrat::vs::State
• rIntervals() : smtrat::icp::HistoryNode
• rLearnedLowerBounds() : smtrat::lra::Tableau< Settings, T1, T2 >
• rLearnedUpperBounds() : smtrat::lra::Tableau< Settings, T1, T2 >
• rLogic() : smtrat::Manager
• rLowerbounds() : smtrat::lra::Variable< T1, T2 >
• rLowerBoundsSize() : smtrat::lra::Variable< T1, T2 >
• rMarkedAsDeleted() : smtrat::vs::State
• rNewLearnedBounds() : smtrat::lra::Tableau< Settings, T1, T2 >
• RNSEncoder() : smtrat::RNSEncoder
• rnsTransformation() : smtrat::RNSEncoder
• root() : smtrat::cadcells::datastructures::RootFunction , smtrat::vs::State
• root_valuation() : smtrat::covering_ng::formula::GraphEvaluation
• RootFunction() : smtrat::cadcells::datastructures::RootFunction
• rootOf() : smtrat::cad::Sample
• roots() : smtrat::cadcells::datastructures::Delineation , smtrat::cadcells::datastructures::RootFunction
• rOrigin() : smtrat::icp::ContractionCandidate
• rOriginalConditions() : smtrat::vs::Substitution
• row() : smtrat::fmplex::Matrix::col_iterator , smtrat::qe::util::Matrix::col_iterator
• row_begin() : smtrat::fmplex::Matrix , smtrat::qe::util::Matrix
• row_end() : smtrat::fmplex::Matrix , smtrat::qe::util::Matrix
• row_end_idx() : smtrat::fmplex::Matrix , smtrat::qe::util::Matrix
• row_entries() : smtrat::fmplex::Matrix , smtrat::qe::util::Matrix
• row_iterator() : smtrat::fmplex::Matrix::row_iterator , smtrat::qe::util::Matrix::row_iterator
• row_size() : smtrat::fmplex::Matrix , smtrat::qe::util::Matrix
• row_start_idx() : smtrat::fmplex::Matrix , smtrat::qe::util::Matrix
• row_view() : smtrat::fmplex::Matrix::row_view , smtrat::qe::util::Matrix::row_view
• rowCorrect() : smtrat::lra::Tableau< Settings, T1, T2 >
• RowEntry() : smtrat::fmplex::Matrix::RowEntry , smtrat::qe::util::Matrix::RowEntry
• rowRefinement() : smtrat::lra::Tableau< Settings, T1, T2 >
• rows() : smtrat::lra::Tableau< Settings, T1, T2 >
• rowVar() : smtrat::lra::TableauEntry< T1, T2 >
• rPassedFormula() : smtrat::Module
• rPosition() : smtrat::lra::Variable< T1, T2 >
• rReasons() : smtrat::icp::HistoryNode
• rReceivedFormula() : smtrat::Module
• rRecentlyAdded() : smtrat::vs::Condition
• rSize() : smtrat::lra::Variable< T1, T2 >
• rStartEntry() : smtrat::lra::Variable< T1, T2 >
• rStateInfeasibleConstraints() : smtrat::icp::HistoryNode
• rStateInfeasibleVariables() : smtrat::icp::HistoryNode
• rSubResultCombination() : smtrat::vs::State
• rSubResultsSimplified() : smtrat::vs::State
• rSubstitution() : smtrat::vs::State
• rSubstitutionResults() : smtrat::vs::State
• rTakeSubResultCombAgain() : smtrat::vs::State
• rTooHighDegreeConditions() : smtrat::vs::State
• rType() : smtrat::vs::State , smtrat::vs::Substitution
• run() : benchmax::Backend , benchmax::CondorBackend , benchmax::SlurmBackend , benchmax::SSHBackend , smtrat::maxsmt::MaxSMTBackend< Solver, MaxSMTStrategy::FU_MALIK_INCREMENTAL > , smtrat::maxsmt::MaxSMTBackend< Solver, MaxSMTStrategy::LINEAR_SEARCH > , smtrat::maxsmt::MaxSMTBackend< Solver, MaxSMTStrategy::MSU3 > , smtrat::Task , smtrat::unsatcore::UnsatCoreBackend< Solver, UnsatCoreStrategy::ModelExclusion >
• run_job_async() : benchmax::SlurmBackend
• runAndWait() : benchmax::CondorBackend
• runBackends() : smtrat::Module , smtrat::PModule , smtrat::ThreadPool
• runBackendSolvers() : smtrat::VSModule< Settings >
• runInstructions() : smtrat::parser::InstructionHandler
• runTask() : smtrat::ThreadPool
• rUpperbounds() : smtrat::lra::Variable< T1, T2 >
• rUpperBoundsSize() : smtrat::lra::Variable< T1, T2 >
• rValuation() : smtrat::vs::Condition
• rVariableBounds() : smtrat::vs::State
• rVariableReasons() : smtrat::icp::HistoryNode
• RWA() : smtrat::icp::ContractionCandidate