z3rs 0.0.3

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
20
21
22
23
24
25

//! # `smt` — core SMT engine
//!
//! **Port phase 5.** Ported from `z3/src/smt` (Z3 4.17.0, MIT).
//! See [`ROADMAP.md`](../../ROADMAP.md) for the porting plan and status.
//!
//! ## Ported so far
//! - [x] congruence closure for equality + uninterpreted functions → [`euf`]
//! - [x] a lazy DPLL(T) loop deciding QF_UF → [`solver`]
//! - [ ] online theory propagation, minimized explanations, more theories
//!   (arith/bv/arrays), quantifier instantiation
//!
//! ## Status: IN PROGRESS

pub mod arith;
pub mod bv;
pub mod euf;
pub mod solver;

pub use arith::{
    Assignment, Constraint, LinExpr, OptOutcome, Rel, SolveOutcome, feasible, feasible_with_diseqs,
    model, model_with_diseqs, model_with_diseqs_budgeted, optimize as arith_optimize, project,
};
pub use bv::{check_bv, check_bv_model};
pub use euf::Egraph;
pub use solver::{Model, SmtResult, Value, ast_to_lin, check, check_model, linear_constraints};