- i -

• ICEModule() : smtrat::ICEModule< Settings >
• ICPModule() : smtrat::ICPModule< Settings >
• IcpVariable() : smtrat::icp::IcpVariable
• id() : smtrat::BackendLink , smtrat::icp::ContractionCandidate , smtrat::lra::Variable< T1, T2 > , smtrat::Module , smtrat::vs::Condition , smtrat::vs::State
• Identifier() : smtrat::parser::Identifier
• identifier() : smtrat::validation::ValidationPoint
• IdentifierParser() : smtrat::parser::IdentifierParser
• idLP() : smtrat::cad::CAD< Settings > , smtrat::qe::cad::CAD< Settings >
• idPL() : smtrat::cad::CAD< Settings > , smtrat::qe::cad::CAD< Settings >
• IDSanitizer() : smtrat::cad::debug::IDSanitizer
• imax() : Minisat::vec< T >
• impliedTseitinLiteral() : smtrat::mcsat::ClauseChain::Link
• implyDefiniteness() : smtrat::PFEModule< Settings >
• implyDefinitenessFromStrict() : smtrat::PFEModule< Settings >
• inConflictWith() : smtrat::lra::Variable< T1, T2 >
• increase() : Minisat::Heap< Comp >
• increaseActivity() : 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 >
• increaseIDCounter() : smtrat::VSModule< Settings >
• incrementActivity() : smtrat::icp::IcpVariable
• incrementReusagesAfterTargetDiameterReached() : smtrat::icp::ContractionCandidate
• incrementTseitinShadowOccurrences() : smtrat::SATModule< Settings >
• IncWidthModule() : smtrat::IncWidthModule< Settings >
• index() : Minisat::Map< K, D, H, E > , smtrat::fmplex::VariableIndex< Var > , smtrat::qe::util::VariableIndex , smtrat::vs::State
• indexed() : smtrat::cad::CADConstraints< BT >
• IndexedRoot() : smtrat::cadcells::datastructures::IndexedRoot
• inequalities() : smtrat::cad::CADPreprocessor
• InequalitiesTable() : smtrat::InequalitiesTable< Settings >
• infeasibleSubsets() : smtrat::Manager , smtrat::Module
• infimum() : smtrat::lra::Variable< T1, T2 > , smtrat::vb::Variable< T >
• Info() : smtrat::lra::Bound< T1, T2 >::Info
• info() : smtrat::parser::InstructionHandler
• inform() : smtrat::cadcells::representation::approximation::ApxCriteria , smtrat::Manager , smtrat::Module
• informBackends() : smtrat::Module
• informCore() : smtrat::BVModule< Settings > , smtrat::CoveringNGModule< Settings > , smtrat::CurryModule< Settings > , smtrat::FPPModule< Settings > , smtrat::ICPModule< Settings > , smtrat::IntBlastModule< Settings > , smtrat::LRAModule< Settings > , smtrat::Module , smtrat::NewCADModule< Settings > , smtrat::NewCoveringModule< Settings > , smtrat::NRAILModule< Settings > , smtrat::PBGaussModule< Settings > , smtrat::PBPPModule< Settings >
• informedConstraints() : smtrat::Module
• infty() : smtrat::cadcells::datastructures::Bound
• inHeap() : Minisat::Heap< Comp >
• init() : Minisat::OccLists< Idx, Vec, Deleted > , smtrat::Backend< Settings > , smtrat::BVModule< Settings > , smtrat::CurryModule< Settings > , smtrat::FPPModule< Settings > , smtrat::IntBlastModule< Settings > , smtrat::LRAModule< Settings > , smtrat::Module , smtrat::NewCADModule< Settings > , smtrat::NewCoveringModule< Settings > , smtrat::NRAILModule< Settings > , smtrat::PBGaussModule< Settings > , smtrat::PBPPModule< Settings >
• initConditionFlags() : smtrat::vs::State
• initialize() : smtrat::resource::Limiter
• initialLinearCheck() : smtrat::ICPModule< Settings >
• initIndex() : smtrat::vs::State
• initVariables() : smtrat::mcsat::MCSATBackend< Settings > , smtrat::mcsat::MCSATMixin< Settings >
• insert() : benchmax::DBAL , Minisat::CMap< T > , Minisat::Heap< Comp > , Minisat::Map< K, D, H, E > , Minisat::Queue< T > , smtrat::cad::PolynomialLiftingQueue< PolynomialGetter > , smtrat::cadcells::datastructures::BaseDerivation< Properties > , smtrat::cadcells::datastructures::DelineatedDerivation< Properties > , smtrat::cadcells::datastructures::PolyPool , smtrat::cadcells::datastructures::SampledDerivation< Properties > , smtrat::mcsat::MCSATMixin< Settings >::VarMapping , smtrat::SATModule< Settings >::UnorderedClauseLookup , smtrat::TheoryVarSchedulerStatic< vot > , 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 >
• insertIntoProjectionQueue() : smtrat::cad::Projection< Incrementality::FULL, Backtracking::HIDE, Settings > , smtrat::cad::Projection< Incrementality::FULL, BT, Settings >
• insertMonomialMapping() : smtrat::MonomialMappingByVariablePool
• insertPolynomial() : smtrat::cad::ModelBasedProjection< Incrementality::NONE, Backtracking::ORDERED, Settings > , smtrat::cad::Projection< Incrementality::NONE, Backtracking::ORDERED, Settings >
• insertPolynomialTo() : smtrat::cad::Projection< Incrementality::FULL, Backtracking::HIDE, Settings > , smtrat::cad::Projection< Incrementality::FULL, BT, Settings >
• InsertReceivedFormula() : smtrat::InequalitiesTable< Settings >
• insertRootSamples() : smtrat::cad::LiftingTree< Settings >
• insertTooHighDegreeStatesInRanking() : smtrat::VSModule< Settings >
• insertVarOrder() : smtrat::SATModule< Settings >
• instantiate() : smtrat::parser::AbstractTheory , smtrat::parser::ArithmeticTheory , smtrat::parser::BitvectorTheory , smtrat::parser::Instantiator< V, T > , smtrat::parser::Theories
• instantiateUserFunction() : smtrat::parser::Theories
• InstructionHandler() : smtrat::parser::InstructionHandler
• Int64Range() : Minisat::Int64Range
• IntBlastModule() : smtrat::IntBlastModule< Settings >
• integerFactorization() : smtrat::RNSEncoder
• IntEqModule() : smtrat::IntEqModule< Settings >
• interconnectVariables() : smtrat::PBPPModule< Settings >
• internalLeftBound() : smtrat::icp::IcpVariable
• internalRightBound() : smtrat::icp::IcpVariable
• internalVisit() : smtrat::expression::ExpressionModifier
• interrupt() : smtrat::SATModule< Settings >
• interval() : smtrat::icp::IcpVariable
• intervalBoundToFormula() : smtrat::ICPModule< Settings >
• intervalPosition() : smtrat::icp::IcpVariable
• IntervalPropagation() : smtrat::mcsat::icp::IntervalPropagation
• intervals() : smtrat::covering_ng::CoveringResult< PropertiesSet > , smtrat::icp::HistoryNode
• intervalsEmpty() : smtrat::ICPModule< Settings >
• IntOption() : Minisat::IntOption
• IntRange() : Minisat::IntRange
• introducedVariables() : smtrat::BVDirectEncoder
• involvesEquation() : smtrat::lra::Variable< T1, T2 >
• irand() : smtrat::SATModule< Settings >
• is_cmaxmin() : smtrat::cadcells::datastructures::RootFunction
• is_cminmax() : smtrat::cadcells::datastructures::RootFunction
• is_conflict() : smtrat::fmplex::FMplexElimination , smtrat::fmplex::Node , smtrat::qe::fmplex::FMplexQE , smtrat::qe::fmplex::Node
• is_consistent() : smtrat::cad::LiftingTree< Settings > , smtrat::cad::SampleIteratorQueue< Iterator, Comparator > , smtrat::mcsat::MCSATMixin< Settings >
• is_const() : smtrat::cadcells::datastructures::Projections
• is_constant() : smtrat::BlastedPoly , smtrat::BVAnnotation
• is_constraint_conjunction() : smtrat::ModuleInput
• is_disc_zero() : smtrat::cadcells::datastructures::Projections
• is_failed() : smtrat::covering_ng::CoveringResult< PropertiesSet >
• is_failed_projection() : smtrat::covering_ng::CoveringResult< PropertiesSet >
• is_finished() : smtrat::fmplex::Node , smtrat::qe::fmplex::Node
• is_global_conflict() : smtrat::fmplex::FMplexElimination
• is_infty() : smtrat::cadcells::datastructures::Bound
• is_integer() : smtrat::lra::Numeric , smtrat::lra::Variable< T1, T2 >
• is_integer_constraint_conjunction() : smtrat::ModuleInput
• is_ldcf_zero() : smtrat::cadcells::datastructures::Projections
• is_linear() : smtrat::icp::ContractionCandidate , smtrat::icp::IcpVariable
• is_minimizing() : smtrat::Module
• is_mode() : smtrat::execution::ExecutionState
• is_nary() : smtrat::expression::Expression
• is_negative() : smtrat::lra::Numeric
• is_null() : smtrat::cadcells::datastructures::DerivationRef< Properties >
• is_nullified() : smtrat::cadcells::datastructures::Projections
• is_only_propositional() : smtrat::ModuleInput
• is_outside() : smtrat::is_sample_outside< S > , smtrat::is_sample_outside< IsSampleOutsideAlgorithm::DEFAULT >
• is_parameter() : smtrat::covering_ng::CoveringResult< PropertiesSet >
• is_positive() : smtrat::lra::Numeric
• is_positive_combination() : smtrat::fmplex::FMplexElimination , smtrat::qe::fmplex::FMplexQE
• is_projective() : smtrat::cadcells::datastructures::IndexedRootOrdering
• is_real_constraint_conjunction() : smtrat::ModuleInput
• is_root() : smtrat::cadcells::datastructures::RootFunction , smtrat::mcsat::arithmetic::RootIndexer< RANT >
• is_sampled() : smtrat::cadcells::datastructures::DerivationRef< Properties >
• is_sat() : smtrat::covering_ng::CoveringResult< PropertiesSet >
• is_section() : smtrat::cadcells::datastructures::DelineationInterval , smtrat::cadcells::datastructures::SymbolicInterval
• is_sector() : smtrat::cadcells::datastructures::DelineationInterval
• is_strict() : smtrat::cadcells::datastructures::Bound
• is_suitable_for_splitting() : smtrat::qe::fmplex::Node
• is_trivial() : smtrat::fmplex::FMplexElimination , smtrat::qe::fmplex::FMplexQE
• is_univariate() : smtrat::mcsat::arithmetic::AssignmentFinder_detail
• is_unsat() : smtrat::covering_ng::CoveringResult< PropertiesSet >
• is_valid() : smtrat::cadcells::datastructures::CoveringRepresentation< P >
• is_weak() : smtrat::cadcells::datastructures::Bound
• is_zero() : smtrat::cadcells::datastructures::Projections , smtrat::ICEModule< Settings > , smtrat::lra::Numeric , smtrat::lra::Value< T >
• isActive() : smtrat::cad::Origin , smtrat::cad::ProjectionInformation , smtrat::icp::ContractionCandidate , smtrat::icp::IcpVariable , smtrat::lra::Bound< T1, T2 > , smtrat::lra::Tableau< Settings, T1, T2 > , smtrat::mcsat::MCSATBackend< Settings > , smtrat::vb::Bound< T >
• isAllCoefficientsEqual() : smtrat::PBPPModule< Settings >
• isAlreadyProcessed() : smtrat::mcsat::onecellcad::recursive::RecursiveCAD
• isAssignedTheoryVariable() : smtrat::mcsat::MCSATMixin< Settings >
• isBasic() : smtrat::lra::Variable< T1, T2 >
• isBinary() : smtrat::expression::Expression
• isBooleanDecisionFeasible() : smtrat::mcsat::MCSATMixin< Settings >
• isBound() : smtrat::cad::ProjectionLevelInformation::LevelInfo
• isComplementActive() : smtrat::lra::Bound< T1, T2 >
• isConflicting() : smtrat::lra::Tableau< Settings, T1, T2 > , smtrat::lra::Variable< T1, T2 > , smtrat::mcsat::ClauseChain::Link , smtrat::vb::VariableBounds< T >
• isConstraintLiteralConjunction() : smtrat::ModuleInput
• isDebugEnabled() : smtrat::LOG
• isDerived() : smtrat::icp::ContractionCandidate
• isEC() : smtrat::cad::ProjectionGlobalInformation
• isEvaluated() : smtrat::cad::ProjectionLevelInformation::LevelInfo
• isExternalUpdated() : smtrat::icp::IcpVariable
• isFailedCovering() : smtrat::LevelWiseInformation< Settings >
• isFeasible() : smtrat::mcsat::MCSATMixin< Settings >
• isFormulaUnivariate() : smtrat::mcsat::MCSATMixin< Settings >
• isFullCovering() : smtrat::LevelWiseInformation< Settings >
• isHighBoundInfty() : smtrat::onecellcad::recursive::Sector
• isIdValid() : smtrat::cad::CAD< Settings >
• isInconsistent() : smtrat::vs::State
• isInfeasible() : smtrat::mcsat::MCSATBackend< Settings >
• isInfinite() : smtrat::lra::Bound< T1, T2 > , smtrat::vb::Bound< T >
• isIntegerConstraintLiteralConjunction() : smtrat::ModuleInput
• isInternalBoundsSet() : smtrat::icp::IcpVariable
• isInternalUpdated() : smtrat::icp::IcpVariable
• isITE() : smtrat::expression::Expression
• isLeaf() : smtrat::TotalizerTree
• isLemmaLevel() : smtrat::Manager , smtrat::Module
• isLowBoundNegInfty() : smtrat::onecellcad::recursive::Sector
• isLowerBound() : smtrat::lra::Bound< T1, T2 > , smtrat::vb::Bound< T >
• isMainPointInsideCell() : smtrat::mcsat::onecellcad::OneCellCAD
• isNonRedundant() : smtrat::RNSEncoder
• isNull() : smtrat::MonomialMappingByVariablePool
• isolateLastVariableRoots() : smtrat::mcsat::onecellcad::OneCellCAD
• isOptional() : smtrat::mcsat::ClauseChain::Link
• isOriginal() : smtrat::icp::IcpVariable , smtrat::lra::Variable< T1, T2 >
• isPartialCovering() : smtrat::LevelWiseInformation< Settings >
• isPointRootOfPoly() : smtrat::mcsat::onecellcad::OneCellCAD
• isPreprocessor() : smtrat::Module , smtrat::PModule
• isProjectionDefinable() : smtrat::qe::cad::CADElimination
• isPropagating() : smtrat::mcsat::ClauseChain::Link
• isPurged() : smtrat::cad::BaseProjection< Settings > , smtrat::cad::Projection< Incrementality::FULL, Backtracking::HIDE, Settings > , smtrat::cad::Projection< Incrementality::FULL, BT, Settings >::PurgedPolynomials , smtrat::cad::ProjectionLevelInformation::LevelInfo
• isQuantifier() : smtrat::expression::Expression
• isQueueEntryActive() : smtrat::cad::Projection< Incrementality::FULL, Backtracking::HIDE, Settings >
• isRealConstraintLiteralConjunction() : smtrat::ModuleInput
• isRoot() : smtrat::cad::Sample , smtrat::vs::State
• isSatisfied() : smtrat::lra::Bound< T1, T2 >
• isSatisfiedBy() : smtrat::lra::Variable< T1, T2 >
• isSemiNegative() : smtrat::ICEModule< Settings >
• isSemiPositive() : smtrat::ICEModule< Settings >
• isSigned() : smtrat::BVAnnotation
• isSuitable() : smtrat::ICEModule< Settings > , smtrat::lra::Tableau< Settings, T1, T2 >
• isSuitableConflictDetection() : smtrat::lra::Tableau< Settings, T1, T2 >
• isSymbolFree() : smtrat::parser::ParserState
• isTheoryVar() : smtrat::mcsat::MCSATMixin< Settings >
• isTrivial() : smtrat::PBPPModule< Settings >
• isTseitinVar() : smtrat::mcsat::ClauseChain
• isType() : smtrat::expression::Expression
• isUnary() : smtrat::expression::Expression
• isUnassigned() : smtrat::lra::Bound< T1, T2 >
• isUnknownCovering() : smtrat::LevelWiseInformation< Settings >
• isUpperBound() : smtrat::lra::Bound< T1, T2 > , smtrat::vb::Bound< T >
• isVariableDeclared() : smtrat::parser::Theories
• isWeak() : smtrat::lra::Bound< T1, T2 >
• ITEExpression() : smtrat::expression::ITEExpression
• iterativeVariableRewriting() : smtrat::GBModule< Settings >
• iterator() : benchmax::RandomizationAdaptor< T >::iterator
• Iterator() : smtrat::lra::Tableau< Settings, T1, T2 >::Iterator