z3rs 0.0.8

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
26

//! # `sat` — propositional SAT core
//!
//! **Port phase 4.** Ported from `z3/src/sat` (Z3 4.17.0, MIT).
//! See [`ROADMAP.md`](../../ROADMAP.md) for the porting plan and status.
//!
//! ## Ported so far
//! - [x] literal/variable encoding (`sat_types`) → [`literal`]
//! - [x] a correct DPLL solver with unit propagation → [`solver`]
//! - [x] Tseitin CNF encoding of a Boolean AST formula (`goal2sat` core) → [`tseitin`]
//! - [x] DIMACS CNF parsing → [`dimacs`]
//! - [ ] CDCL: watched literals, clause learning, restarts, in-processing
//! - [ ] `sat_smt` bridge, DRAT proofs
//!
//! ## Status: IN PROGRESS

pub mod dimacs;
pub mod drat;
pub mod literal;
pub mod solver;
pub mod tseitin;

pub use dimacs::{DimacsError, parse as parse_dimacs};
pub use drat::{check as check_drat, check_text as check_drat_text};
pub use literal::{Lit, Var};
pub use solver::{SatResult, Solver};
pub use tseitin::{check_skeleton, encode, encode_tracking};