List of all items

Structs

• Context
• EqualityNotification
• Model
• NelsonOppenCombiner
• NelsonOppenStats
• Objective
• Optimizer
• ParetoPoint
• Proof
• Solver
• SolverConfig
• SolverStats
• TheoryId
• combination::conflict_resolution::ConflictAnalysis
• combination::conflict_resolution::ConflictClause
• combination::conflict_resolution::ConflictResolutionConfig
• combination::conflict_resolution::ConflictResolutionStats
• combination::conflict_resolution::ConflictResolver
• combination::conflict_resolution::Equality
• combination::conflict_resolution::ExplanationGenerator
• combination::conflict_resolution::Literal
• combination::conflict_resolution::MultiTheoryConflictAnalyzer
• combination::conflict_resolution::TheoryConflict
• combination::convexity::ConvexityConfig
• combination::convexity::ConvexityHandler
• combination::convexity::ConvexityStats
• combination::convexity::DisjunctiveReasoning
• combination::convexity::Equality
• combination::convexity::EqualityDisjunction
• combination::convexity::ModelBasedCombination
• combination::convexity::TheoryModel
• combination::coordinator::CoordinatorConfig
• combination::coordinator::CoordinatorStats
• combination::coordinator::EqualityProp
• combination::coordinator::SharedTerm
• combination::coordinator::TheoryCoordinator
• combination::equality_propagation::CongruenceData
• combination::equality_propagation::CongruenceKey
• combination::equality_propagation::EClassData
• combination::equality_propagation::EGraph
• combination::equality_propagation::EqualityPropStats
• combination::equality_propagation::EqualityPropagator
• combination::equality_propagation::EqualityWatch
• combination::equality_propagation::TheoryExplanation
• combination::equality_propagation::UnionFind
• combination::interface_eq::Equality
• combination::interface_eq::EqualityMinimizer
• combination::interface_eq::EqualityPriority
• combination::interface_eq::EqualityScheduler
• combination::interface_eq::InterfaceEClass
• combination::interface_eq::InterfaceEquality
• combination::interface_eq::InterfaceEqualityConfig
• combination::interface_eq::InterfaceEqualityManager
• combination::interface_eq::InterfaceEqualityStats
• combination::nelson_oppen::Equality
• combination::nelson_oppen::NelsonOppen
• combination::nelson_oppen::NelsonOppenConfig
• combination::nelson_oppen::NelsonOppenStats
• combination::nelson_oppen_advanced::AdvancedNelsonOppen
• combination::nelson_oppen_advanced::AdvancedNelsonOppenConfig
• combination::nelson_oppen_advanced::AdvancedNelsonOppenStats
• combination::nelson_oppen_advanced::CaseSplit
• combination::nelson_oppen_advanced::Disequality
• combination::nelson_oppen_advanced::Equality
• combination::nelson_oppen_advanced::EqualityPriority
• combination::nelson_oppen_advanced::ModelBasedCombination
• combination::nelson_oppen_advanced::PartitionRefinement
• combination::nelson_oppen_advanced::TermPartition
• combination::nelson_oppen_advanced::TheoryConflict
• combination::nelson_oppen_advanced::TheoryProperties
• combination::nelson_oppen_advanced::UnionFindWithExplanation
• combination::partition_refinement::Equality
• combination::partition_refinement::Partition
• combination::partition_refinement::PartitionComparator
• combination::partition_refinement::PartitionEnumerator
• combination::partition_refinement::PartitionRefinement
• combination::partition_refinement::PartitionRefinementConfig
• combination::partition_refinement::PartitionRefinementManager
• combination::partition_refinement::PartitionRefinementStats
• combination::propagation_opt::DependencyGraph
• combination::propagation_opt::IncrementalPropagator
• combination::propagation_opt::LazyPropagator
• combination::propagation_opt::Literal
• combination::propagation_opt::OptimizedPropagationEngine
• combination::propagation_opt::PropagationCache
• combination::propagation_opt::PropagationConfig
• combination::propagation_opt::PropagationEvent
• combination::propagation_opt::PropagationPriority
• combination::propagation_opt::PropagationStats
• combination::propagation_opt::PropagationTrail
• combination::propagation_opt::WatchList
• combination::shared_terms_advanced::AdvancedSharedTermsManager
• combination::shared_terms_advanced::EClass
• combination::shared_terms_advanced::EGraph
• combination::shared_terms_advanced::ENode
• combination::shared_terms_advanced::Equality
• combination::shared_terms_advanced::InterfaceTermMinimizer
• combination::shared_terms_advanced::SharedTermInfo
• combination::shared_terms_advanced::SharedTermsConfig
• combination::shared_terms_advanced::SharedTermsStats
• conflict::clause_learning::ClauseLearner
• conflict::clause_learning::ClauseLearningConfig
• conflict::clause_learning::ClauseLearningStats
• conflict::clause_learning::ClauseMinimizer
• conflict::clause_learning::ImplicationGraph
• conflict::clause_learning::ImplicationNode
• conflict::clause_learning::LearnedClause
• conflict::clause_learning::LearnedDatabase
• conflict::explanation_cache::CacheConfig
• conflict::explanation_cache::CacheStats
• conflict::explanation_cache::Explanation
• conflict::explanation_cache::ExplanationCache
• conflict::explanation_generator::Explanation
• conflict::explanation_generator::ExplanationConfig
• conflict::explanation_generator::ExplanationGenerator
• conflict::explanation_generator::ExplanationStats
• conflict::implication_graph::ImplicationGraph
• conflict::implication_graph::ImplicationGraphConfig
• conflict::implication_graph::ImplicationGraphStats
• conflict::implication_graph::ImplicationNode
• conflict::minimizer::ConflictMinimizer
• conflict::minimizer::MinimizerConfig
• conflict::minimizer::MinimizerStats
• conflict::recursive_minimizer::LitInfo
• conflict::recursive_minimizer::RecursiveMinConfig
• conflict::recursive_minimizer::RecursiveMinStats
• conflict::recursive_minimizer::RecursiveMinimizer
• conflict::relevancy::ImplicationEdge
• conflict::relevancy::RelevancyConfig
• conflict::relevancy::RelevancyStats
• conflict::relevancy::RelevancyTracker
• conflict::theory_explainer::ExplainerConfig
• conflict::theory_explainer::ExplainerStats
• conflict::theory_explainer::ProofStep
• conflict::theory_explainer::TheoryExplainer
• conflict::theory_explainer::TheoryExplanation
• conflict::uip_selection::ImplicationNode
• conflict::uip_selection::UipConfig
• conflict::uip_selection::UipSelector
• conflict::uip_selection::UipStats
• delayed_combination::DeferredEquality
• delayed_combination::DelayedCombination
• delayed_combination::DelayedCombinationConfig
• delayed_combination::DelayedCombinationStats
• delayed_combination::SharedTerm
• mbqi::Instantiation
• mbqi::MBQIStats
• mbqi::QuantifiedFormula
• mbqi::counterexample::CexStats
• mbqi::counterexample::CounterExample
• mbqi::counterexample::CounterExampleGenerator
• mbqi::finite_model::BoundedModelChecker
• mbqi::finite_model::DomainEnumerator
• mbqi::finite_model::FinderStats
• mbqi::finite_model::FiniteModel
• mbqi::finite_model::FiniteModelFinder
• mbqi::finite_model::SymmetryBreaker
• mbqi::finite_model::SymmetryStats
• mbqi::finite_model::UniverseSize
• mbqi::heuristics::InstantiationHeuristic
• mbqi::heuristics::MBQIHeuristics
• mbqi::heuristics::QuantifierQueue
• mbqi::instantiation::EngineStats
• mbqi::instantiation::InstantiationContext
• mbqi::instantiation::InstantiationEngine
• mbqi::instantiation::InstantiationPattern
• mbqi::instantiation::InstantiatorStats
• mbqi::instantiation::QuantifierInstantiator
• mbqi::integration::DefaultCallback
• mbqi::integration::MBQIIntegration
• mbqi::lazy_instantiation::EGraph
• mbqi::lazy_instantiation::LazyInstantiator
• mbqi::lazy_instantiation::LazyStats
• mbqi::lazy_instantiation::Match
• mbqi::lazy_instantiation::MatchingContext
• mbqi::lazy_instantiation::RelevanceTracker
• mbqi::lazy_instantiation::TermDatabase
• mbqi::model_completion::ArithmeticProjection
• mbqi::model_completion::CompletedModel
• mbqi::model_completion::CompletionStats
• mbqi::model_completion::FixerStats
• mbqi::model_completion::FunctionEntry
• mbqi::model_completion::FunctionInterpretation
• mbqi::model_completion::MacroDefinition
• mbqi::model_completion::MacroSolver
• mbqi::model_completion::MacroStats
• mbqi::model_completion::ModelCompleter
• mbqi::model_completion::ModelFixer
• mbqi::model_completion::ProjectionFunctionDef
• mbqi::model_completion::UninterpStats
• mbqi::model_completion::UninterpretedSortHandler
• mbqi::patterns::GeneratorStats
• mbqi::patterns::MultiMatch
• mbqi::patterns::MultiPatternCoordinator
• mbqi::patterns::Pattern
• mbqi::patterns::PatternGenerator
• mbqi::patterns::PatternMatch
• model::advanced_builder::AdvancedModelBuilder
• model::advanced_builder::ArrayValue
• model::advanced_builder::Model
• model::advanced_builder::ModelBuilderConfig
• model::advanced_builder::ModelBuilderStats
• model::advanced_builder::ModelValue
• model::builder::Model
• model::builder::ModelBuilder
• model::builder::ModelBuilderConfig
• model::builder::ModelBuilderStats
• model::completion::CompletionConfig
• model::completion::CompletionStats
• model::completion::ModelCompleter
• model::minimizer::Assignment
• model::minimizer::MinimizerConfig
• model::minimizer::MinimizerStats
• model::minimizer::ModelMinimizer
• propagation::backtrack_manager::Assignment
• propagation::backtrack_manager::BacktrackManager
• propagation::backtrack_manager::BacktrackStats
• propagation::backtrack_manager::BoundUpdate
• propagation::backtrack_manager::Checkpoint
• propagation::backtrack_manager::DecisionLevel
• propagation::backtrack_manager::TheoryReason
• propagation::pipeline::Propagation
• propagation::pipeline::PropagationConfig
• propagation::pipeline::PropagationPipeline
• propagation::pipeline::PropagationStats
• propagation::pipeline::PropagationWatcher
• propagation::priority_queue::PriorityQueueConfig
• propagation::priority_queue::PriorityQueueStats
• propagation::priority_queue::Propagation
• propagation::priority_queue::PropagationQueue
• propagation::theory_propagator::Explanation
• propagation::theory_propagator::PropagatorConfig
• propagation::theory_propagator::PropagatorManager
• propagation::theory_propagator::PropagatorStats
• propagation::watched_propagator::Watch
• propagation::watched_propagator::WatchedConfig
• propagation::watched_propagator::WatchedConstraint
• propagation::watched_propagator::WatchedPropagator
• propagation::watched_propagator::WatchedStats
• propagation_pipeline::PropagationConfig
• propagation_pipeline::PropagationItem
• propagation_pipeline::PropagationPipeline
• propagation_pipeline::PropagationStats
• shared_terms::Equality
• shared_terms::SharedTermsConfig
• shared_terms::SharedTermsManager
• shared_terms::SharedTermsStats

Enums

• ObjectiveKind
• OptimizationResult
• ProofStep
• RestartStrategy
• SolverResult
• TheoryMode
• combination::conflict_resolution::Explanation
• combination::conflict_resolution::MinimizationAlgorithm
• combination::convexity::CaseSplitStrategy
• combination::convexity::ConvexityProperty
• combination::coordinator::SatResult
• combination::coordinator::TheoryId
• combination::equality_propagation::Explanation
• combination::interface_eq::GenerationStrategy
• combination::interface_eq::SchedulingPolicy
• combination::nelson_oppen::CombinationResult
• combination::nelson_oppen_advanced::CombinationResult
• combination::nelson_oppen_advanced::EqualityExplanation
• combination::propagation_opt::PropagationReason
• combination::shared_terms_advanced::EqualityExplanation
• conflict::recursive_minimizer::Reason
• conflict::theory_explainer::ExplanationType
• conflict::uip_selection::UipStrategy
• mbqi::InstantiationReason
• mbqi::MBQIResult
• mbqi::counterexample::RefinementStrategy
• mbqi::finite_model::CheckResult
• mbqi::finite_model::FinderError
• mbqi::finite_model::SymmetryStrategy
• mbqi::heuristics::InstantiationOrdering
• mbqi::heuristics::ResourceAllocation
• mbqi::heuristics::SelectionStrategy
• mbqi::heuristics::TriggerSelection
• mbqi::lazy_instantiation::LazyStrategy
• mbqi::model_completion::CompletionError
• mbqi::patterns::PatternType
• model::advanced_builder::Theory
• model::advanced_builder::Value
• model::builder::Value
• model::completion::CompletionStrategy
• model::minimizer::MinimizationStrategy
• propagation::backtrack_manager::ReasonClause
• propagation::backtrack_manager::UndoAction
• propagation::pipeline::PropagationLevel
• propagation::pipeline::PropagationReason
• propagation::pipeline::TheoryId
• propagation::priority_queue::PropagationType
• propagation::theory_propagator::PropagationResult
• propagation::watched_propagator::ConstraintData
• propagation::watched_propagator::WatchType
• propagation_pipeline::PropagationPriority
• propagation_pipeline::PropagationType

Traits

• TheoryCombination
• combination::coordinator::TheorySolver
• combination::nelson_oppen_advanced::TheorySolver
• mbqi::integration::SolverCallback
• mbqi::model_completion::ProjectionFunction
• propagation::theory_propagator::TheoryPropagator

Macros

• completion_error
• finder_error
• instantiation
• mbqi_debug
• mbqi_time
• mbqi_trace
• quantifier

Functions

• mbqi::macros::utils::free_vars
• mbqi::macros::utils::is_ground
• mbqi::macros::utils::substitute
• mbqi::macros::utils::term_depth
• mbqi::macros::utils::term_size

Type Aliases

• combination::conflict_resolution::DecisionLevel
• combination::conflict_resolution::TermId
• combination::conflict_resolution::TheoryId
• combination::convexity::DecisionLevel
• combination::convexity::TermId
• combination::convexity::TheoryId
• combination::coordinator::TermId
• combination::equality_propagation::EClassId
• combination::interface_eq::DecisionLevel
• combination::interface_eq::TermId
• combination::interface_eq::TheoryId
• combination::nelson_oppen::TermId
• combination::nelson_oppen::TheoryId
• combination::nelson_oppen_advanced::DecisionLevel
• combination::nelson_oppen_advanced::TermId
• combination::nelson_oppen_advanced::TheoryId
• combination::partition_refinement::ClassId
• combination::partition_refinement::DecisionLevel
• combination::partition_refinement::TermId
• combination::partition_refinement::TheoryId
• combination::propagation_opt::ClauseId
• combination::propagation_opt::DecisionLevel
• combination::propagation_opt::TermId
• combination::propagation_opt::TheoryId
• combination::propagation_opt::Timestamp
• combination::shared_terms_advanced::DecisionLevel
• combination::shared_terms_advanced::EClassId
• combination::shared_terms_advanced::TermId
• combination::shared_terms_advanced::TheoryId
• conflict::clause_learning::ClauseId
• conflict::explanation_cache::CacheKey
• conflict::explanation_generator::TheoryId
• conflict::implication_graph::Level
• conflict::implication_graph::Var
• conflict::recursive_minimizer::ClauseId
• conflict::recursive_minimizer::Level
• conflict::recursive_minimizer::Lit
• conflict::relevancy::ClauseId
• conflict::relevancy::Lit
• conflict::uip_selection::Level
• delayed_combination::TheoryId
• model::advanced_builder::TermId
• model::builder::SortId
• model::builder::VarId
• propagation::pipeline::TermId
• propagation::priority_queue::Priority
• propagation::priority_queue::PropagationId
• propagation::theory_propagator::TheoryId
• propagation::watched_propagator::ConstraintId
• shared_terms::TheoryId