smt_scope/formatter/
mod.rs

1mod defns;
2mod defns_const;
3mod deparse;
4mod error;
5mod parse;
6#[cfg(feature = "serde")]
7mod serde;
8
9pub use defns::*;
10pub use defns_const::*;
11pub use deparse::*;
12pub use error::*;
13use parse::*;
14
15macro_rules! unwrap {
16    ($e:expr) => {
17        match $e {
18            Ok(v) => v,
19            Err(e) => e.kind.const_error(true),
20        }
21    };
22}
23
24pub const QUANT_BIND: BindPowerPair = unwrap!(BindPowerPair::parse("-6,12")).1;
25
26pub const DEFAULT_FORMATTER: FormatterConst<'static> = unwrap!(FormatterConst::parse(
27    "$-8$${0}$$(#0..-1|4|8|4$(|, |))$$-4$"
28));
29// pub const DEFAULT: TermDisplayConst<'static> = unwrap!(TermDisplayConst::parse("/(?:.|\\n)*/", "$-8$${0}$$(#0..-1|4|8|4$(|, |))$$-4$"));
30
31pub const TRIGGER: TermDisplayConst<'static> = unwrap!(TermDisplayConst::parse(
32    "pattern",
33    "$-8${ $(#0..-1|4|8|4$, )$ }$-8$"
34));
35
36pub const UNARY_OP: TermDisplayConst<'static> = unwrap!(TermDisplayConst::parse(
37    "(/(?:not)/ _)",
38    "$-6$${0}$$[#0|-8,16]$$-16$"
39));
40pub const NEG: TermDisplayConst<'static> =
41    unwrap!(TermDisplayConst::parse("(- _)", "$-6$-$[#0|-8,16]$$-16$"));
42/// I'm not sure all of these are necessary since z3 generally breaks up terms,
43/// e.g. `(>= _ _)` into `(and (= _ _) (< _ _))`, or `(=> _ _)` into `(or (not _) _)`.
44pub const BINARY_OP: TermDisplayConst<'static> = unwrap!(TermDisplayConst::parse(
45    "/=|\\+|-|\\*|/|<|>|(?:and)|(?:or)|(?:<=)|(?:>=)|(?:=>)/",
46    "$10$$(#0..-1|9|-16|9$| ${0}$ |)$$10$"
47));
48pub const IF: TermDisplayConst<'static> = unwrap!(TermDisplayConst::parse(
49    "if",
50    "$-8$$[#0|9,-16]$ ? $[#1|4,4]$ : $[#2|4,4]$$-8$"
51));
52
53// pub const SLOT_TEST: TermDisplayConst<'static> = unwrap!(TermDisplayConst::parse("slot", "$-8$&$[#0|9,-16]$[$[#1|4,4]$]$-8$"));
54
55pub const S_EXPRESSION: FormatterConst<'static> =
56    unwrap!(FormatterConst::parse("$-1$(${0}$$(#0..-1|1$ | |)$)$-1$"));
57pub const S_EXPRESSION_LEAF: TermDisplayConst<'static> =
58    unwrap!(TermDisplayConst::parse("(/.*/)", "$-1$${0}$$-1$"));
59pub const S_EXPRESSION_PATTERN: TermDisplayConst<'static> = unwrap!(TermDisplayConst::parse(
60    "pattern",
61    "$-1$:pattern ($(#0..-1|1$| |)$)$-1$"
62));
63
64impl TermDisplayContext {
65    pub fn basic() -> Self {
66        let self_: Result<Self, _> = [TRIGGER, UNARY_OP, NEG, BINARY_OP, IF]
67            .into_iter()
68            .map(|td| TermDisplay::try_from(td).unwrap())
69            .collect();
70        self_.unwrap()
71    }
72
73    pub fn s_expression() -> Self {
74        let fallback = Formatter::try_from(S_EXPRESSION).unwrap();
75        let mut self_ = Self::new(fallback);
76
77        let leaf = TermDisplay::try_from(S_EXPRESSION_LEAF).unwrap();
78        self_.push(leaf).unwrap();
79        let pattern = TermDisplay::try_from(S_EXPRESSION_PATTERN).unwrap();
80        self_.push(pattern).unwrap();
81
82        self_
83    }
84}
85
86impl Default for Formatter {
87    fn default() -> Self {
88        static FMT: std::sync::OnceLock<Formatter> = std::sync::OnceLock::new();
89        FMT.get_or_init(|| Formatter::try_from(DEFAULT_FORMATTER).unwrap())
90            .clone()
91    }
92}
smt_scope/formatter/mod.rs

smt_scope/formatter/
mod.rs
