veri_engine_lib/
lib.rs

1use easy_smt::SExpr;
2
3pub mod annotations;
4pub mod interp;
5pub mod solver;
6pub mod termname;
7pub mod type_inference;
8pub mod verify;
9
10pub const REG_WIDTH: usize = 64;
11
12// Use a distinct with as the maximum width any value should have within type inference
13pub const MAX_WIDTH: usize = 2 * REG_WIDTH;
14
15pub const FLAGS_WIDTH: usize = 4;
16
17pub const WIDTHS: [usize; 4] = [8, 16, 32, 64];
18
19// Closure arguments: SMT context, arguments to the term, lhs, rhs
20type CustomCondition = dyn Fn(&easy_smt::Context, Vec<SExpr>, SExpr, SExpr) -> SExpr;
21
22// Closure arguments: SMT context, arguments to the term
23type CustomAssumption = dyn Fn(&easy_smt::Context, Vec<SExpr>) -> SExpr;
24
25pub struct Config {
26    pub term: String,
27    pub names: Option<Vec<String>>,
28    pub distinct_check: bool,
29
30    pub custom_verification_condition: Option<Box<CustomCondition>>,
31    pub custom_assumptions: Option<Box<CustomAssumption>>,
32}
33
34impl Config {
35    pub fn with_term_and_name(term: &str, name: &str) -> Self {
36        Config {
37            term: term.to_string(),
38            distinct_check: true,
39            custom_verification_condition: None,
40            custom_assumptions: None,
41            names: Some(vec![name.to_string()]),
42        }
43    }
44}
veri_engine_lib/lib.rs

veri_engine_lib/
lib.rs
