warp_types_smt/
phase.rs

1//! SMT solver phase markers.
2//!
3//! Zero-sized types encoding the SMT solving workflow. Sealed —
4//! external crates cannot forge phases or create invalid transitions.
5//!
6//! # Phase machine
7//!
8//! ```text
9//!   Init
10//!     → declare_sort(), declare_fun()   stays Init (accumulates declarations)
11//!     → finish_declarations()           → Declared
12//!   Declared
13//!     → assert_formula()                stays Declared (accumulates assertions)
14//!     → finish_assertions()             → Asserted
15//!   Asserted
16//!     → check_sat()                     → SmtResult
17//!       → Sat                             terminal: satisfiable model exists
18//!       → Unsat                           terminal: no model exists
19//!       → Unknown                         terminal: solver budget exhausted
20//! ```
21
22// ============================================================================
23// Sealed trait
24// ============================================================================
25
26pub(crate) mod sealed {
27    pub(crate) struct SealToken;
28
29    #[allow(private_interfaces)]
30    pub trait Sealed {
31        #[doc(hidden)]
32        fn _sealed() -> SealToken;
33    }
34}
35
36// ============================================================================
37// Phase trait + markers
38// ============================================================================
39
40/// Marker trait for SMT phases. Sealed.
41pub trait Phase: sealed::Sealed + 'static {
42    /// Human-readable phase name.
43    const NAME: &'static str;
44}
45
46/// Initial state — declare sorts and function symbols.
47#[derive(Debug)]
48pub struct Init;
49
50/// Declarations finalized — assert formulas.
51#[derive(Debug)]
52pub struct Declared;
53
54/// Assertions finalized — ready to solve.
55#[derive(Debug)]
56pub struct Asserted;
57
58/// Satisfiable — a model exists.
59/// Terminal phase.
60#[derive(Debug)]
61pub struct Sat;
62
63/// Unsatisfiable — no model exists.
64/// Terminal phase.
65#[derive(Debug)]
66pub struct Unsat;
67
68/// Solver budget exhausted without conclusive result.
69/// Terminal phase.
70#[derive(Debug)]
71pub struct Unknown;
72
73// ============================================================================
74// Sealed + Phase impls
75// ============================================================================
76
77macro_rules! impl_phase {
78    ($ty:ty, $name:literal) => {
79        #[allow(private_interfaces)]
80        impl sealed::Sealed for $ty {
81            fn _sealed() -> sealed::SealToken {
82                sealed::SealToken
83            }
84        }
85        impl Phase for $ty {
86            const NAME: &'static str = $name;
87        }
88    };
89}
90
91impl_phase!(Init, "init");
92impl_phase!(Declared, "declared");
93impl_phase!(Asserted, "asserted");
94impl_phase!(Sat, "sat");
95impl_phase!(Unsat, "unsat");
96impl_phase!(Unknown, "unknown");
warp_types_smt/phase.rs

warp_types_smt/
phase.rs
