smtlib 0.1.6

A high-level API for interacting with SMT solvers
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106

use std::{
    fs::{self, File},
    io::Write,
};

use smtlib_build_util::{
    itertools::Itertools,
    miette::{self, Context, IntoDiagnostic},
};
use smtlib_lowlevel::ast::{Logic, LogicAttribute};

fn logics() -> miette::Result<Vec<Logic>> {
    let mut logics = vec![];

    for p in fs::read_dir("./src/logics").into_diagnostic()? {
        let p = p.into_diagnostic()?;
        let p = p.path();
        if let Some("smt2") = p.extension().and_then(|c| c.to_str()) {
            let s = smtlib_build_util::read_to_string(&p)?;
            let l = Logic::parse(&s).with_context(|| format!("parsing {p:?}"))?;
            logics.push(l);
        }
    }

    Ok(logics)
}

fn main() -> miette::Result<()> {
    let out = smtlib_build_util::out_dir();

    let mut logic_file = File::create(out.join("logic.rs")).unwrap();

    writeln!(
        logic_file,
        "
        /// Logics allow specifictation of which (sub-)logic should be used by a
        /// solver.
        ///
        /// > [A more detailed description of logics can be found on the
        /// SMT-LIB website.](https://smtlib.cs.uiowa.edu/logics.shtml)
        ///
        /// ![This is a graph :)](https://smtlib.cs.uiowa.edu/Logics/logics.png)
        #[allow(nonstandard_style)]
        pub enum Logic {{
        "
    )
    .into_diagnostic()?;

    let logics = logics()?;

    for Logic(name, attrs) in &logics {
        let language = attrs
            .iter()
            .find_map(|a| match a {
                LogicAttribute::Theories(_) => None,
                LogicAttribute::Language(l) => Some(l.clone()),
                LogicAttribute::Extensions(_) => None,
                LogicAttribute::Values(_) => None,
                LogicAttribute::Notes(_) => None,
                LogicAttribute::Attribute(_) => None,
            })
            .unwrap();
        let language = language
            .trim()
            .trim_matches(|c| c == '"' || c == '“')
            .lines()
            .map(|l| format!("/// {l}"))
            .format("\n");

        writeln!(logic_file, "{language}").into_diagnostic()?;
        writeln!(logic_file, "{name},").into_diagnostic()?;
    }

    writeln!(
        logic_file,
        "
            /// A fallback variant in case the user wants to specify
            /// some logic which is not part of the predefined
            /// collection.
            Custom(String),
        }}"
    )
    .into_diagnostic()?;

    let display_impl = logics
        .iter()
        .map(|Logic(name, _)| format!("Self::{name} => \"{name}\".fmt(f),"))
        .format("\n");

    writeln!(
        logic_file,
        r#"
        impl std::fmt::Display for Logic {{
            fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {{
                match self {{
                    {display_impl}
                    Self::Custom(s) => s.fmt(f),
                }}
            }}
        }}
    "#
    )
    .into_diagnostic()?;

    Ok(())
}