Crate warp_types_smt 

Phase-typed SMT solver for QF_EUF (Quantifier-Free Equality with Uninterpreted Functions).

Encodes the SMT workflow in Rust’s type system following the typestate pattern from warp_types. Phase transitions consume the old state and produce the new — invalid transitions are compile errors.

SMT Phase Machine

with_session(|session| {
  // session: SmtSession<'s, Init>
  let (session, s) = session.declare_sort("S");
  let (session, f) = session.declare_fun("f", &[s], s);
  let (session, a) = session.var("a", s);
  let (session, b) = session.var("b", s);
  let declared = session.finish_declarations();
  // declared: SmtSession<'s, Declared>
  let asserted = declared
      .assert_formula(SmtFormula::Eq(a, b))
      .finish_assertions();
  // asserted: SmtSession<'s, Asserted>
  asserted.check_sat()
})

Built on warp-types-sat

Uses the CDCL SAT solver from warp-types-sat as the Boolean backbone. The EUF congruence closure engine implements TheorySolver, integrating via the DPLL(T) protocol: check after BCP fixpoint, lazy explanation during conflict analysis, backtrackable union-find.

Re-exports

pub use euf::EufSolver;

pub use formula::AtomId;

pub use formula::AtomMap;

pub use formula::SmtFormula;

pub use phase::Asserted;

pub use phase::Declared;

pub use phase::Init;

pub use phase::Phase;

pub use phase::Sat;

pub use phase::Unknown;

pub use phase::Unsat;

pub use session::with_session;

pub use session::SmtSession;

pub use solver::SmtResult;

pub use term::FuncDecl;

pub use term::FuncId;

pub use term::Sort;

pub use term::SortId;

pub use term::TermArena;

pub use term::TermId;

pub use term::TermKind;

Modules

euf

Congruence closure engine for QF_EUF.

formula

SMT formula representation and Boolean abstraction.

phase

SMT solver phase markers.

session

SMT session with lifetime-branded phase tracking.

solver

Top-level SMT solver: wires formula abstraction, EUF theory, and SAT together.

term

Term representation for QF_EUF.