oxiz_solver/
lib.rs

1//! OxiZ Solver - Main CDCL(T) SMT Solver
2//!
3//! This crate provides the main solver API that orchestrates:
4//! - SAT core (CDCL)
5//! - Theory solvers (EUF, LRA, LIA, BV)
6//! - Tactic framework
7//! - Parallel portfolio solving
8
9#![allow(clippy::collapsible_if)]
10#![allow(clippy::only_used_in_recursion)]
11#![allow(clippy::for_kv_map)]
12#![allow(clippy::too_many_arguments)]
13//!
14//! # Examples
15//!
16//! ## Basic Boolean Satisfiability
17//!
18//! ```
19//! use oxiz_solver::{Solver, SolverResult};
20//! use oxiz_core::ast::TermManager;
21//!
22//! let mut solver = Solver::new();
23//! let mut tm = TermManager::new();
24//!
25//! // Create boolean variables
26//! let p = tm.mk_var("p", tm.sorts.bool_sort);
27//! let q = tm.mk_var("q", tm.sorts.bool_sort);
28//!
29//! // Assert p AND q
30//! let formula = tm.mk_and(vec![p, q]);
31//! solver.assert(formula, &mut tm);
32//!
33//! // Check satisfiability
34//! match solver.check(&mut tm) {
35//!     SolverResult::Sat => println!("Satisfiable!"),
36//!     SolverResult::Unsat => println!("Unsatisfiable!"),
37//!     SolverResult::Unknown => println!("Unknown"),
38//! }
39//! ```
40//!
41//! ## Integer Arithmetic
42//!
43//! ```
44//! use oxiz_solver::{Solver, SolverResult};
45//! use oxiz_core::ast::TermManager;
46//! use num_bigint::BigInt;
47//!
48//! let mut solver = Solver::new();
49//! let mut tm = TermManager::new();
50//!
51//! solver.set_logic("QF_LIA");
52//!
53//! // Create integer variable
54//! let x = tm.mk_var("x", tm.sorts.int_sort);
55//!
56//! // Assert: x >= 5 AND x <= 10
57//! let five = tm.mk_int(BigInt::from(5));
58//! let ten = tm.mk_int(BigInt::from(10));
59//! solver.assert(tm.mk_ge(x, five), &mut tm);
60//! solver.assert(tm.mk_le(x, ten), &mut tm);
61//!
62//! // Should be satisfiable
63//! assert_eq!(solver.check(&mut tm), SolverResult::Sat);
64//! ```
65//!
66//! ## Incremental Solving with Push/Pop
67//!
68//! ```
69//! use oxiz_solver::{Solver, SolverResult};
70//! use oxiz_core::ast::TermManager;
71//!
72//! let mut solver = Solver::new();
73//! let mut tm = TermManager::new();
74//!
75//! let p = tm.mk_var("p", tm.sorts.bool_sort);
76//! solver.assert(p, &mut tm);
77//!
78//! // Push a new scope
79//! solver.push();
80//! let q = tm.mk_var("q", tm.sorts.bool_sort);
81//! solver.assert(q, &mut tm);
82//! assert_eq!(solver.check(&mut tm), SolverResult::Sat);
83//!
84//! // Pop back to previous scope
85//! solver.pop();
86//! assert_eq!(solver.check(&mut tm), SolverResult::Sat);
87//! ```
88
89#![cfg_attr(not(feature = "std"), no_std)]
90#![forbid(unsafe_code)]
91#![warn(missing_docs)]
92
93#[cfg(not(feature = "std"))]
94extern crate alloc;
95
96mod prelude;
97
98mod context;
99mod nelson_oppen;
100mod optimization;
101pub mod resource_limits;
102mod simplify;
103#[cfg(feature = "std")]
104pub mod skolemization;
105mod solver;
106
107pub use context::Context;
108pub use nelson_oppen::{NelsonOppenCombiner, NelsonOppenStats, TheoryId};
109pub use optimization::{Objective, ObjectiveKind, OptimizationResult, Optimizer, ParetoPoint};
110#[cfg(feature = "std")]
111pub use oxiz_proof::replay::VerificationResult;
112pub use solver::{Model, Proof, ProofStep, Solver, SolverConfig, SolverResult, TheoryMode};
113
114// Re-export types from oxiz-sat
115pub use oxiz_sat::{RestartStrategy, SolverStats};
116
117// Re-export theory combination types from oxiz-theories
118pub use oxiz_theories::{EqualityNotification, TheoryCombination};
119
120// Phase 2 enhancements
121pub mod combination;
122pub mod conflict;
123pub mod delayed_combination;
124pub mod model;
125pub mod propagation;
126pub mod propagation_pipeline;
127pub mod shared_terms;
128
129// MBQI module (Model-Based Quantifier Instantiation)
130pub mod mbqi;
131
132// Z3 API compatibility layer (std-only)
133#[cfg(feature = "std")]
134pub mod z3_compat;
oxiz_solver/lib.rs

oxiz_solver/
lib.rs
