rustproof-libsmt 0.1.0

Rust bindings for z3 as utilized by RustProof.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26

//! Macro helpers for defining theories

#[macro_export]
macro_rules! impl_smt_node {
    ($fns: ty, define vars [$($variant: pat),*], define consts [$($c: pat),*]) => {
        impl SMTNode for $fns {
            fn is_var(&self) -> bool {
                match *self {
                $(
                    $variant => true,
                 )*
                    _ => false,
                }
            }

            fn is_const(&self) -> bool {
                match *self {
                $(
                    $c => true,
                )*
                    _ => false,
                }
            }
        }
    }
}