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#![allow(unused_variables)]
14#![allow(dead_code)]
15//!
16//! # Examples
17//!
18//! ## Basic Boolean Satisfiability
19//!
20//! ```
21//! use oxiz_solver::{Solver, SolverResult};
22//! use oxiz_core::ast::TermManager;
23//!
24//! let mut solver = Solver::new();
25//! let mut tm = TermManager::new();
26//!
27//! // Create boolean variables
28//! let p = tm.mk_var("p", tm.sorts.bool_sort);
29//! let q = tm.mk_var("q", tm.sorts.bool_sort);
30//!
31//! // Assert p AND q
32//! let formula = tm.mk_and(vec![p, q]);
33//! solver.assert(formula, &mut tm);
34//!
35//! // Check satisfiability
36//! match solver.check(&mut tm) {
37//!     SolverResult::Sat => println!("Satisfiable!"),
38//!     SolverResult::Unsat => println!("Unsatisfiable!"),
39//!     SolverResult::Unknown => println!("Unknown"),
40//! }
41//! ```
42//!
43//! ## Integer Arithmetic
44//!
45//! ```
46//! use oxiz_solver::{Solver, SolverResult};
47//! use oxiz_core::ast::TermManager;
48//! use num_bigint::BigInt;
49//!
50//! let mut solver = Solver::new();
51//! let mut tm = TermManager::new();
52//!
53//! solver.set_logic("QF_LIA");
54//!
55//! // Create integer variable
56//! let x = tm.mk_var("x", tm.sorts.int_sort);
57//!
58//! // Assert: x >= 5 AND x <= 10
59//! let five = tm.mk_int(BigInt::from(5));
60//! let ten = tm.mk_int(BigInt::from(10));
61//! solver.assert(tm.mk_ge(x, five), &mut tm);
62//! solver.assert(tm.mk_le(x, ten), &mut tm);
63//!
64//! // Should be satisfiable
65//! assert_eq!(solver.check(&mut tm), SolverResult::Sat);
66//! ```
67//!
68//! ## Incremental Solving with Push/Pop
69//!
70//! ```
71//! use oxiz_solver::{Solver, SolverResult};
72//! use oxiz_core::ast::TermManager;
73//!
74//! let mut solver = Solver::new();
75//! let mut tm = TermManager::new();
76//!
77//! let p = tm.mk_var("p", tm.sorts.bool_sort);
78//! solver.assert(p, &mut tm);
79//!
80//! // Push a new scope
81//! solver.push();
82//! let q = tm.mk_var("q", tm.sorts.bool_sort);
83//! solver.assert(q, &mut tm);
84//! assert_eq!(solver.check(&mut tm), SolverResult::Sat);
85//!
86//! // Pop back to previous scope
87//! solver.pop();
88//! assert_eq!(solver.check(&mut tm), SolverResult::Sat);
89//! ```
90
91#![forbid(unsafe_code)]
92#![warn(missing_docs)]
93
94mod context;
95mod nelson_oppen;
96mod optimization;
97mod simplify;
98mod solver;
99
100pub use context::Context;
101pub use nelson_oppen::{NelsonOppenCombiner, NelsonOppenStats, TheoryId};
102pub use optimization::{Objective, ObjectiveKind, OptimizationResult, Optimizer, ParetoPoint};
103pub use solver::{Model, Proof, ProofStep, Solver, SolverConfig, SolverResult, TheoryMode};
104
105// Re-export types from oxiz-sat
106pub use oxiz_sat::{RestartStrategy, SolverStats};
107
108// Re-export theory combination types from oxiz-theories
109pub use oxiz_theories::{EqualityNotification, TheoryCombination};
110
111// Phase 2 enhancements
112pub mod combination;
113pub mod conflict;
114pub mod delayed_combination;
115pub mod model;
116pub mod propagation;
117pub mod propagation_pipeline;
118pub mod shared_terms;
119
120// MBQI module (Model-Based Quantifier Instantiation)
121pub mod mbqi;
oxiz_solver/lib.rs

oxiz_solver/
lib.rs
