rapx/verify/smt_check/mod.rs
1//! SMT checking package for the staged verifier.
2//!
3//! The package is split into:
4//!
5//! - `common`: the shared SMT entry point, query/result types, and term model.
6//! - one SP-specific module per safety property family, such as `align`.
7//!
8//! SP-specific modules should only lower verifier properties into common SMT
9//! obligations. They should not construct independent solver APIs.
10
11mod alias;
12mod align;
13mod alive;
14mod allocated;
15mod common;
16mod deref;
17mod in_bound;
18mod init;
19mod non_null;
20mod non_overlap;
21mod non_volatile;
22mod typed;
23mod valid_num;
24mod valid_ptr;
25
26pub use common::{SmtCheckResult, SmtChecker, SmtObligation, SmtQuery};