rust_formal_verification/algorithms/proof/mod.rs
1//! Algorithms for proving the safety of a finite state transition system.
2
3// ************************************************************************************************
4// rust submodule declaration, they get searched in their respective file names
5// ************************************************************************************************
6
7pub mod ic3_stateful_solver;
8pub mod ic3_stateless_solver;
9pub mod pdr;
10pub mod proof_result;
11
12// ************************************************************************************************
13// re-exports of structs in these modules to simplify paths for other imports
14// ************************************************************************************************
15
16pub use ic3_stateful_solver::IC3Stateful;
17pub use ic3_stateless_solver::IC3Stateless;
18pub use pdr::PDR;
19pub use proof_result::ProofResult;
20
21// ************************************************************************************************
22// use
23// ************************************************************************************************
24
25use crate::models::FiniteStateTransitionSystem;
26
27// ************************************************************************************************
28// Sat Solver trait
29// ************************************************************************************************
30
31pub trait FiniteStateTransitionSystemProver {
32 fn new(fin_state: &FiniteStateTransitionSystem) -> Self;
33 fn prove(&mut self) -> ProofResult;
34}