rustproof_libsmt/theories/
utils.rs

1//! Macro helpers for defining theories
2
3#[macro_export]
4macro_rules! impl_smt_node {
5    ($fns: ty, define vars [$($variant: pat),*], define consts [$($c: pat),*]) => {
6        impl SMTNode for $fns {
7            fn is_var(&self) -> bool {
8                match *self {
9                $(
10                    $variant => true,
11                 )*
12                    _ => false,
13                }
14            }
15
16            fn is_const(&self) -> bool {
17                match *self {
18                $(
19                    $c => true,
20                )*
21                    _ => false,
22                }
23            }
24        }
25    }
26}