easy_smt/
known_atoms.rs

1use crate::{sexpr::Arena, SExpr};
2
3macro_rules! for_each_known_atom {
4    ( $mac:ident ) => {
5        $mac! {
6            check_sat: "check-sat";
7            check_sat_assuming: "check-sat-assuming";
8            unsat: "unsat";
9            sat: "sat";
10            unknown: "unknown";
11            declare_const: "declare-const";
12            declare_datatype: "declare-datatype";
13            declare_datatypes: "declare-datatypes";
14            par: "par";
15            declare_sort: "declare-sort";
16            declare_fun: "declare-fun";
17            define_fun: "define-fun";
18            assert: "assert";
19            get_model: "get-model";
20            get_value: "get-value";
21            get_unsat_core: "get-unsat-core";
22            set_logic: "set-logic";
23            set_option: "set-option";
24            exit: "exit";
25            push: "push";
26            pop: "pop";
27            bool: "Bool";
28            bang: "!";
29            success: "success";
30            t: "true";
31            f: "false";
32            not: "not";
33            imp: "=>";
34            and: "and";
35            or: "or";
36            xor: "xor";
37            eq: "=";
38            distinct: "distinct";
39            ite: "ite";
40            int: "Int";
41            minus: "-";
42            plus: "+";
43            times: "*";
44            div: "div";
45            modulo: "mod";
46            rem: "rem";
47            lte: "<=";
48            lt: "<";
49            gte: ">=";
50            gt: ">";
51            array: "Array";
52            select: "select";
53            store: "store";
54            let_: "let";
55            forall: "forall";
56            exists: "exists";
57            match_: "match";
58            und: "_";
59            bit_vec: "BitVec";
60            concat: "concat";
61            extract: "extract";
62            bvnot: "bvnot";
63            bvor: "bvor";
64            bvand: "bvand";
65            bvnand: "bvnand";
66            bvxor: "bvxor";
67            bvxnor: "bvxnor";
68            bvneg: "bvneg";
69            bvadd: "bvadd";
70            bvsub: "bvsub";
71            bvmul: "bvmul";
72            bvudiv: "bvudiv";
73            bvurem: "bvurem";
74            bvsdiv: "bvsdiv";
75            bvsmod: "bvsmod";
76            bvsrem: "bvsrem";
77            bvshl: "bvshl";
78            bvlshr: "bvlshr";
79            bvashr: "bvashr";
80            bvule: "bvule";
81            bvult: "bvult";
82            bvuge: "bvuge";
83            bvugt: "bvugt";
84            bvsle: "bvsle";
85            bvslt: "bvslt";
86            bvsge: "bvsge";
87            bvsgt: "bvsgt";
88            bvcomp: "bvcomp";
89        }
90    };
91}
92
93macro_rules! define_known_atoms {
94    ( $( $id:ident : $atom:expr ; )* ) => {
95        #[non_exhaustive]
96        pub struct KnownAtoms {
97            $(
98                #[doc = "The atom: `"]
99                #[doc = $atom]
100                #[doc = "`"]
101                pub $id: SExpr,
102            )*
103        }
104
105        impl KnownAtoms {
106            pub(crate) fn new(arena: &Arena) -> Self {
107                KnownAtoms {
108                    $( $id: arena.atom($atom), )*
109                }
110            }
111        }
112    };
113}
114
115for_each_known_atom!(define_known_atoms);
easy_smt/known_atoms.rs

easy_smt/
known_atoms.rs
