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            real: "Real";
52            slash: "/";
53            to_real: "to_real";
54            array: "Array";
55            select: "select";
56            store: "store";
57            let_: "let";
58            forall: "forall";
59            exists: "exists";
60            match_: "match";
61            und: "_";
62            bit_vec: "BitVec";
63            concat: "concat";
64            extract: "extract";
65            bvnot: "bvnot";
66            bvor: "bvor";
67            bvand: "bvand";
68            bvnand: "bvnand";
69            bvxor: "bvxor";
70            bvxnor: "bvxnor";
71            bvneg: "bvneg";
72            bvadd: "bvadd";
73            bvsub: "bvsub";
74            bvmul: "bvmul";
75            bvudiv: "bvudiv";
76            bvurem: "bvurem";
77            bvsdiv: "bvsdiv";
78            bvsmod: "bvsmod";
79            bvsrem: "bvsrem";
80            bvshl: "bvshl";
81            bvlshr: "bvlshr";
82            bvashr: "bvashr";
83            bvule: "bvule";
84            bvult: "bvult";
85            bvuge: "bvuge";
86            bvugt: "bvugt";
87            bvsle: "bvsle";
88            bvslt: "bvslt";
89            bvsge: "bvsge";
90            bvsgt: "bvsgt";
91            bvcomp: "bvcomp";
92        }
93    };
94}
95
96macro_rules! define_known_atoms {
97    ( $( $id:ident : $atom:expr ; )* ) => {
98        #[non_exhaustive]
99        pub struct KnownAtoms {
100            $(
101                #[doc = "The atom: `"]
102                #[doc = $atom]
103                #[doc = "`"]
104                pub $id: SExpr,
105            )*
106        }
107
108        impl KnownAtoms {
109            pub(crate) fn new(arena: &Arena) -> Self {
110                KnownAtoms {
111                    $( $id: arena.atom($atom), )*
112                }
113            }
114        }
115    };
116}
117
118for_each_known_atom!(define_known_atoms);
easy_smt/known_atoms.rs

easy_smt/
known_atoms.rs
