oxiz_nlsat/
lib.rs

1//! # oxiz-nlsat
2//!
3//! Non-linear arithmetic solver for OxiZ using Cylindrical Algebraic Decomposition (CAD).
4//!
5//! This crate implements the NLSAT algorithm for solving non-linear real arithmetic
6//! (QF_NRA) and non-linear integer arithmetic (QF_NIA) problems.
7//!
8//! ## Reference
9//!
10//! Z3's `nlsat/` directory (~180k lines), particularly `nlsat_solver.cpp`.
11//!
12//! ## Key Components
13//!
14//! - **Polynomial Constraints**: Representation of non-linear constraints
15//! - **Variable Ordering**: Strategies for CAD variable ordering
16//! - **Interval Sets**: Representation of solution intervals
17//! - **Explanation**: Conflict explanation for CDCL integration
18
19pub mod assignment;
20pub mod assumptions;
21pub mod asymmetric_literal_addition;
22pub mod bce;
23pub mod bound_propagation;
24pub mod bve;
25pub mod cad;
26pub mod cad_optimization;
27pub mod chrono_bt;
28pub mod clause;
29pub mod clause_tiers;
30pub mod discriminant;
31pub mod eval_cache;
32pub mod evaluator;
33pub mod explain;
34pub mod grobner_preprocess;
35pub mod incremental_cad;
36pub mod inprocessing;
37pub mod interval_set;
38pub mod lemma;
39pub mod lookahead;
40pub mod maxsat;
41pub mod monotonicity;
42pub mod nia;
43pub mod portfolio;
44pub mod proof;
45pub mod restart;
46pub mod root_hints;
47pub mod simplify;
48pub mod solver;
49pub mod structure_analyzer;
50pub mod subsumption;
51pub mod symmetry;
52pub mod theory_conflict;
53pub mod types;
54pub mod var_order;
55pub mod vivification;
56pub mod watched_literals;
57
58// Re-exports
59pub use assumptions::{AssumptionManager, Scope};
60pub use asymmetric_literal_addition::{AlaConfig, AlaEngine, AlaStats};
61pub use bce::{BceConfig, BceEngine, BceStats};
62pub use bound_propagation::{BoundPropagator, Interval};
63pub use bve::{BveConfig, BveEngine, BveStats};
64pub use cad::{
65    CadCell, CadConfig, CadDecomposer, CadError, CadLifter, CadPoint, CadProjection, ProjectionSet,
66    SampleStrategy, SturmSequence,
67};
68pub use cad_optimization::{
69    CadOptConfig, CadOptStats, CadOrderingAnalyzer, HongProjection, OrderingHeuristic,
70    PartialCadBuilder, ProjectionConflict, SampleCache,
71};
72pub use chrono_bt::{
73    BacktrackDecision, ChronoBacktracker, ChronoConfig, ChronoStats, ConflictAnalysisResult,
74};
75pub use clause_tiers::{ClauseTier, ClauseTierConfig, ClauseTierManager, ClauseTierStats};
76// TODO: Re-export cutting planes from oxiz-math after API updates
77// pub use oxiz_math::lp::cutting_planes::{Cut, CutType, CuttingPlaneConfig, CuttingPlaneGenerator, CuttingPlaneStats};
78pub use discriminant::{DiscriminantAnalyzer, DiscriminantSign, DiscriminantStats, RootInfo};
79pub use eval_cache::{CachedSign, EvalCache, EvalCacheConfig, EvalCacheStats, SignPattern};
80pub use grobner_preprocess::{
81    GroebnerConfig, GroebnerPreprocessor, GroebnerStats, PreprocessResult,
82};
83pub use incremental_cad::{CacheStats, CadSnapshot, IncrementalCad};
84pub use inprocessing::{InprocessConfig, InprocessStats, Inprocessor};
85pub use lookahead::{LookaheadConfig, LookaheadEngine, LookaheadResult, LookaheadStats};
86pub use maxsat::{MaxSatConfig, MaxSatResult, MaxSatSolver, MaxSatStats, SoftConstraint};
87pub use monotonicity::{
88    MonotonicityAnalyzer, MonotonicityDirection, MonotonicityInfo, MonotonicityStats,
89};
90pub use nia::{BranchingStrategy, NiaConfig, NiaSolver, NiaStats, VarType};
91pub use portfolio::{PortfolioConfig, PortfolioResult, PortfolioSolver, PortfolioStats};
92pub use proof::{
93    CadOperation, Proof, ProofBuilder, ProofError, ProofId, ProofMetadata, ProofRule, ProofStats,
94    ProofStep, TheoryExplanation,
95};
96pub use restart::{RestartManager, RestartStrategy};
97pub use root_hints::{
98    PolynomialRootHints, RootHint, RootHintsCache, RootHintsConfig, RootHintsStats,
99};
100pub use solver::NlsatSolver;
101pub use structure_analyzer::{ProblemClass, SolverStrategy, StructureAnalyzer, StructureStats};
102pub use subsumption::{SubsumptionChecker, SubsumptionConfig, SubsumptionStats};
103pub use symmetry::{Permutation, SymmetryDetector, SymmetryGroup, SymmetryStats};
104pub use theory_conflict::{
105    ConflictInfo, ConflictPatterns, TheoryConflictConfig, TheoryConflictStats,
106    TheoryConflictTracker,
107};
108pub use var_order::{OrderingAnalyzer, OrderingStats, OrderingStrategy, VariableOrdering};
109pub use vivification::{VivificationConfig, VivificationStats, Vivifier};
110pub use watched_literals::{WatchEntry, WatchStats, WatchedLiterals, WatchedPropagator};
oxiz_nlsat/lib.rs

oxiz_nlsat/
lib.rs
