rustproof_libsmt/logics/
utils.rs

1//! Defines macros to build Logics on top of theories.
2
3#[macro_export]
4macro_rules! define_sorts_for_logic {
5    ($logic: ident, $($variant: ident -> $sort: ty),*) => {
6        #[derive(Clone, Debug)]
7        pub enum $logic {
8            $(
9                $variant($sort),
10            )*
11        }
12        
13        $(
14            impl Into<$logic> for $sort {
15                fn into(self) -> $logic {
16                    $logic::$variant(self)
17                }
18            }
19        )*
20
21            impl fmt::Display for $logic {
22                fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
23                    let s = match *self {
24                        $(
25                            $logic::$variant(ref op) => op.to_string(),
26                         )*
27                    };
28                    write!(f, "{}", s)
29                }
30            }
31    }
32}
33
34#[macro_export]
35macro_rules! define_fns_for_logic {
36    ($logic: ident, $($variant: ident -> $sort: ty),*) => {
37        #[derive(Clone, Debug)]
38        pub enum $logic {
39            $(
40                $variant($sort),
41            )*
42        }
43        
44        $(
45            impl Into<$logic> for $sort {
46                fn into(self) -> $logic {
47                    $logic::$variant(self)
48                }
49            }
50        )*
51
52            impl fmt::Display for $logic {
53                fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
54                    let s = match *self {
55                        $(
56                            $logic::$variant(ref op) => op.to_string(),
57                         )*
58                    };
59                    write!(f, "{}", s)
60                }
61            }
62
63        impl SMTNode for $logic {
64            fn is_var(&self) -> bool {
65                match *self {
66                    $(
67                        $logic::$variant(ref inner) => inner.is_var(),
68                    )*
69                }
70            }
71
72            fn is_const(&self) -> bool {
73                match *self {
74                    $(
75                        $logic::$variant(ref inner) => inner.is_const(),
76                    )*
77                }
78            }
79        }
80    }
81}
82
83#[macro_export]
84macro_rules! define_logic {
85    ($logic: ident, $op: ident, $sorts: ty, map { $($fv: pat => $rt: path),* }) => {
86        #[derive(Clone, Copy, Debug)]
87        pub struct $logic;
88
89        impl fmt::Display for $logic {
90            fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
91                write!(f, "{}", stringify!($logic))
92            }
93        }
94
95        impl Logic for $logic {
96            type Fns = $op;
97            type Sorts = $sorts;
98
99            fn free_var<T: AsRef<str>>(name: T, ty: $sorts) -> Self::Fns {
100                match ty {
101                    $(
102                        $fv => $rt(name.as_ref().to_owned()).into(),
103                    )*
104                    _ => unreachable!(),
105                }
106            }
107        }
108    }
109}
rustproof_libsmt/logics/utils.rs

rustproof_libsmt/logics/
utils.rs
