warp_types_pdr/
lib.rs

1//! Phase-typed Property-Directed Reachability (IC3).
2//!
3//! Proves unbounded safety properties or finds concrete counterexamples
4//! by maintaining an inductive frame sequence. Unlike bounded model checking
5//! (which only proves safety up to a depth bound), PDR can prove that a
6//! property holds at *all* depths by finding an inductive invariant.
7//!
8//! # PDR Phase Machine
9//!
10//! ```text
11//! with_session(|session| {
12//!   // session: PdrSession<'s, Init>
13//!   let modeled = session.build_model();   // → Modeled
14//!   // Internally: strengthen → propagate → converge (or counterexample)
15//!   //   → check_safe()            → Safe     (inductive invariant found)
16//!   //   → check_counterexample()  → CounterexampleFound (trace found)
17//!   //   → check_exhausted()       → Exhausted (frame budget exceeded)
18//! })
19//! ```
20//!
21//! # Built on warp-types-sat and warp-types-bmc
22//!
23//! Uses the CDCL SAT solver from `warp-types-sat` as the decision oracle
24//! (multiple queries per frame: consecution, predecessor, generalization).
25//! Shares the `TransitionSystem` model type from `warp-types-bmc`.
26
27pub mod checker;
28pub mod cube;
29pub mod frames;
30pub mod phase;
31pub mod session;
32
33pub use checker::{check, PdrResult};
34pub use cube::Cube;
35pub use frames::{Frame, FrameSequence};
36pub use phase::{CounterexampleFound, Exhausted, Init, Modeled, Phase, Safe};
37pub use session::{with_session, PdrSession};
warp_types_pdr/lib.rs

warp_types_pdr/
lib.rs
