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

oxiz_solver/
lib.rs
