Expand description
§oxiz-nlsat
Non-linear arithmetic solver for OxiZ using Cylindrical Algebraic Decomposition (CAD).
This crate implements the NLSAT algorithm for solving non-linear real arithmetic (QF_NRA) and non-linear integer arithmetic (QF_NIA) problems.
§Reference
Z3’s nlsat/ directory (~180k lines), particularly nlsat_solver.cpp.
§Key Components
- Polynomial Constraints: Representation of non-linear constraints
- Variable Ordering: Strategies for CAD variable ordering
- Interval Sets: Representation of solution intervals
- Explanation: Conflict explanation for CDCL integration
Re-exports§
pub use assumptions::AssumptionManager;pub use assumptions::Scope;pub use asymmetric_literal_addition::AlaConfig;pub use asymmetric_literal_addition::AlaEngine;pub use asymmetric_literal_addition::AlaStats;pub use bce::BceConfig;pub use bce::BceEngine;pub use bce::BceStats;pub use bound_propagation::BoundPropagator;pub use bound_propagation::Interval;pub use bve::BveConfig;pub use bve::BveEngine;pub use bve::BveStats;pub use cad::CadCell;pub use cad::CadConfig;pub use cad::CadDecomposer;pub use cad::CadError;pub use cad::CadLifter;pub use cad::CadPoint;pub use cad::CadProjection;pub use cad::ProjectionSet;pub use cad::SampleStrategy;pub use cad::SturmSequence;pub use cad_optimization::CadOptConfig;pub use cad_optimization::CadOptStats;pub use cad_optimization::CadOrderingAnalyzer;pub use cad_optimization::HongProjection;pub use cad_optimization::OrderingHeuristic;pub use cad_optimization::PartialCadBuilder;pub use cad_optimization::ProjectionConflict;pub use cad_optimization::SampleCache;pub use chrono_bt::BacktrackDecision;pub use chrono_bt::ChronoBacktracker;pub use chrono_bt::ChronoConfig;pub use chrono_bt::ChronoStats;pub use chrono_bt::ConflictAnalysisResult;pub use clause_tiers::ClauseTier;pub use clause_tiers::ClauseTierConfig;pub use clause_tiers::ClauseTierManager;pub use clause_tiers::ClauseTierStats;pub use discriminant::DiscriminantAnalyzer;pub use discriminant::DiscriminantSign;pub use discriminant::DiscriminantStats;pub use discriminant::RootInfo;pub use eval_cache::CachedSign;pub use eval_cache::EvalCache;pub use eval_cache::EvalCacheConfig;pub use eval_cache::EvalCacheStats;pub use eval_cache::SignPattern;pub use grobner_preprocess::GroebnerConfig;pub use grobner_preprocess::GroebnerPreprocessor;pub use grobner_preprocess::GroebnerStats;pub use grobner_preprocess::PreprocessResult;pub use incremental_cad::CacheStats;pub use incremental_cad::CadSnapshot;pub use incremental_cad::IncrementalCad;pub use inprocessing::InprocessConfig;pub use inprocessing::InprocessStats;pub use inprocessing::Inprocessor;pub use lookahead::LookaheadConfig;pub use lookahead::LookaheadEngine;pub use lookahead::LookaheadResult;pub use lookahead::LookaheadStats;pub use maxsat::MaxSatConfig;pub use maxsat::MaxSatResult;pub use maxsat::MaxSatSolver;pub use maxsat::MaxSatStats;pub use maxsat::SoftConstraint;pub use monotonicity::MonotonicityAnalyzer;pub use monotonicity::MonotonicityDirection;pub use monotonicity::MonotonicityInfo;pub use monotonicity::MonotonicityStats;pub use nia::BranchingStrategy;pub use nia::NiaConfig;pub use nia::NiaSolver;pub use nia::NiaStats;pub use nia::VarType;pub use portfolio::PortfolioConfig;pub use portfolio::PortfolioResult;pub use portfolio::PortfolioSolver;pub use portfolio::PortfolioStats;pub use proof::CadOperation;pub use proof::Proof;pub use proof::ProofBuilder;pub use proof::ProofError;pub use proof::ProofId;pub use proof::ProofMetadata;pub use proof::ProofRule;pub use proof::ProofStats;pub use proof::ProofStep;pub use proof::TheoryExplanation;pub use restart::RestartManager;pub use restart::RestartStrategy;pub use root_hints::PolynomialRootHints;pub use root_hints::RootHint;pub use root_hints::RootHintsCache;pub use root_hints::RootHintsConfig;pub use root_hints::RootHintsStats;pub use solver::NlsatSolver;pub use structure_analyzer::ProblemClass;pub use structure_analyzer::SolverStrategy;pub use structure_analyzer::StructureAnalyzer;pub use structure_analyzer::StructureStats;pub use subsumption::SubsumptionChecker;pub use subsumption::SubsumptionConfig;pub use subsumption::SubsumptionStats;pub use symmetry::Permutation;pub use symmetry::SymmetryDetector;pub use symmetry::SymmetryGroup;pub use symmetry::SymmetryStats;pub use theory_conflict::ConflictInfo;pub use theory_conflict::ConflictPatterns;pub use theory_conflict::TheoryConflictConfig;pub use theory_conflict::TheoryConflictStats;pub use theory_conflict::TheoryConflictTracker;pub use var_order::OrderingAnalyzer;pub use var_order::OrderingStats;pub use var_order::OrderingStrategy;pub use var_order::VariableOrdering;pub use vivification::VivificationConfig;pub use vivification::VivificationStats;pub use vivification::Vivifier;pub use watched_literals::WatchEntry;pub use watched_literals::WatchStats;pub use watched_literals::WatchedLiterals;pub use watched_literals::WatchedPropagator;
Modules§
- assignment
- Variable assignment for NLSAT.
- assumptions
- Assumption-based incremental solving.
- asymmetric_
literal_ addition - Asymmetric Literal Addition (ALA) for clause strengthening.
- bce
- Blocked Clause Elimination (BCE)
- bound_
propagation - Bound propagation for polynomial constraints.
- bve
- Bounded Variable Elimination (BVE)
- cad
- Cylindrical Algebraic Decomposition (CAD) for NLSAT.
- cad_
optimization - Advanced CAD Optimization Techniques.
- chrono_
bt - Chronological backtracking support.
- clause
- Clause representation for NLSAT.
- clause_
tiers - Clause Tier System
- discriminant
- Discriminant analysis for polynomial root counting.
- eval_
cache - Advanced polynomial evaluation cache and sign pattern memoization.
- evaluator
- Polynomial constraint evaluator for NLSAT.
- explain
- Conflict explanation for NLSAT.
- grobner_
preprocess - Gröbner Basis Preprocessing for NLSAT.
- incremental_
cad - Incremental CAD for efficient updates and backtracking.
- inprocessing
- Inprocessing techniques for clause database optimization.
- interval_
set - Interval sets for NLSAT.
- lemma
- Theory lemma interface for NLSAT.
- lookahead
- Lookahead decision heuristics for SAT solving.
- maxsat
- Core-guided MaxSAT optimization for NLSAT.
- monotonicity
- Polynomial monotonicity analysis for improved bound propagation.
- nia
- Non-linear Integer Arithmetic (NIA) solver.
- portfolio
- Portfolio-based parallel solving for NLSAT.
- proof
- Proof generation for NLSAT solver.
- restart
- Restart strategies for the NLSAT solver.
- root_
hints - Root approximation hints cache for faster root isolation.
- simplify
- Simplification of polynomials and constraints.
- solver
- NLSAT solver implementation.
- structure_
analyzer - Problem structure analyzer for NLSAT.
- subsumption
- Clause Subsumption
- symmetry
- Symmetry detection and breaking for polynomial constraints.
- theory_
conflict - Theory conflict tracking for improved decision heuristics.
- types
- Type definitions for NLSAT.
- var_
order - Variable ordering strategies for NLSAT.
- vivification
- Vivification for clause strengthening.
- watched_
literals - Two-watched literal scheme for efficient unit propagation.