z3rs 0.0.7

A pure-Rust port of the Z3 theorem prover, free of third-party and native dependencies
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19

//! # `nlsat` — Nonlinear arithmetic SAT, real closed fields
//!
//! **Port phase 5.** Ported from the Z3 C++ component(s) below.
//! See [`ROADMAP.md`](../../ROADMAP.md) for the porting plan and status.
//!
//! ## Upstream C++ components to port
//! - [~] `z3/src/nlsat` → [`icp`] (interval-propagation *refutation* half of nlsat)
//! - [ ] `z3/src/realclosure`
//!
//! ## Status: IN PROGRESS — sound nonlinear refutation via interval propagation

pub mod cad;
pub mod elim;
pub mod icp;
pub mod realclosure;
pub mod univariate;

pub use icp::{Constraint, Rel, refute};
pub use univariate::decide as decide_univariate;