| //! Invariant Extractor — Abstract Interpretation over SUBLEQ Memory States | |
| //! | |
| //! Derives loop invariants, pre/post conditions via symbolic execution | |
| //! and abstract domain analysis. Outputs predicates in SMT-LIB format. | |
| pub mod symbolic; | |
| pub mod abstract_domain; | |
| pub mod extractor; | |
| pub mod predicates; | |
| pub mod subleq_analysis; | |
| pub use symbolic::{SymbolicState, SymbolicValue}; | |
| pub use abstract_domain::{AbstractDomain, Interval}; | |
| pub use extractor::InvariantExtractor; | |
| pub use predicates::Predicate; | |
| pub use subleq_analysis::{SubleqPattern, PatternMatcher}; | |