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
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109

//! Defines macros to build Logics on top of theories.

#[macro_export]
macro_rules! define_sorts_for_logic {
    ($logic: ident, $($variant: ident -> $sort: ty),*) => {
        #[derive(Clone, Debug)]
        pub enum $logic {
            $(
                $variant($sort),
            )*
        }
        
        $(
            impl Into<$logic> for $sort {
                fn into(self) -> $logic {
                    $logic::$variant(self)
                }
            }
        )*

            impl fmt::Display for $logic {
                fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
                    let s = match *self {
                        $(
                            $logic::$variant(ref op) => op.to_string(),
                         )*
                    };
                    write!(f, "{}", s)
                }
            }
    }
}

#[macro_export]
macro_rules! define_fns_for_logic {
    ($logic: ident, $($variant: ident -> $sort: ty),*) => {
        #[derive(Clone, Debug)]
        pub enum $logic {
            $(
                $variant($sort),
            )*
        }
        
        $(
            impl Into<$logic> for $sort {
                fn into(self) -> $logic {
                    $logic::$variant(self)
                }
            }
        )*

            impl fmt::Display for $logic {
                fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
                    let s = match *self {
                        $(
                            $logic::$variant(ref op) => op.to_string(),
                         )*
                    };
                    write!(f, "{}", s)
                }
            }

        impl SMTNode for $logic {
            fn is_var(&self) -> bool {
                match *self {
                    $(
                        $logic::$variant(ref inner) => inner.is_var(),
                    )*
                }
            }

            fn is_const(&self) -> bool {
                match *self {
                    $(
                        $logic::$variant(ref inner) => inner.is_const(),
                    )*
                }
            }
        }
    }
}

#[macro_export]
macro_rules! define_logic {
    ($logic: ident, $op: ident, $sorts: ty, map { $($fv: pat => $rt: path),* }) => {
        #[derive(Clone, Copy, Debug)]
        pub struct $logic;

        impl fmt::Display for $logic {
            fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
                write!(f, "{}", stringify!($logic))
            }
        }

        impl Logic for $logic {
            type Fns = $op;
            type Sorts = $sorts;

            fn free_var<T: AsRef<str>>(name: T, ty: $sorts) -> Self::Fns {
                match ty {
                    $(
                        $fv => $rt(name.as_ref().to_owned()).into(),
                    )*
                    _ => unreachable!(),
                }
            }
        }
    }
}