smt_scope/parsers/z3/
mod.rs

1use std::fmt::Debug;
2
3use super::{LogParser, LogParserHelper};
4use crate::{Error, FResult, Result};
5
6mod blame;
7mod bugs;
8pub mod cdcl;
9pub mod egraph;
10pub mod inst;
11pub mod inter_line;
12/// Original Z3 log parser. Works with Z3 v.4.12.1, should work with other versions
13/// as long as the log format is the same for the important line cases.
14/// Compare with the log files in the `logs/` folder to see if this is the case.
15pub mod parse;
16pub mod smt2;
17pub mod stack;
18pub mod synthetic;
19pub mod terms;
20// pub mod theory;
21mod z3parser;
22
23pub use z3parser::*;
24
25fn split_ascii_space(line: &str) -> impl Iterator<Item = &str> {
26    fn to_str(s: &[u8]) -> &str {
27        unsafe { core::str::from_utf8_unchecked(s) }
28    }
29    line.as_bytes().split(u8::is_ascii_whitespace).map(to_str)
30}
31
32impl<T: Z3LogParser + LogParserHelper> LogParser for T {
33    fn is_line_start(&mut self, first_byte: u8) -> bool {
34        first_byte == b'['
35    }
36
37    fn process_line(&mut self, line: &str, line_no: usize) -> FResult<bool> {
38        // Much faster than `split_whitespace` or `split(' ')` since it works on
39        // [u8] instead of [char] and so doesn't need to convert to UTF-8.
40        let mut split = split_ascii_space(line);
41        let Some(first) = split.next() else {
42            return Ok(true);
43        };
44        self.newline();
45        let parse = match first {
46            // match the line case
47            "[tool-version]" => self.version_info(split),
48            "[mk-quant]" => self.mk_quant(split),
49            "[mk-lambda]" => self.mk_lambda(split),
50            "[mk-var]" => self.mk_var(split),
51            "[mk-app]" => self.mk_app(split),
52            "[mk-proof]" => self.mk_proof(split),
53            "[attach-meaning]" => self.attach_meaning(split),
54            "[attach-var-names]" => self.attach_var_names(split),
55            "[attach-enode]" => self.attach_enode(split),
56            "[eq-expl]" => self.eq_expl(split),
57            "[new-match]" => self.new_match(split),
58            "[inst-discovered]" => self.inst_discovered(split),
59            "[instance]" => self.instance(split),
60            "[end-of-instance]" => self.end_of_instance(split),
61            "[decide-and-or]" => self.decide_and_or(split),
62            "[decide]" => self.decide(split),
63            "[assign]" => self.assign(split),
64            "[push]" => self.push(split),
65            "[pop]" => self.pop(split),
66            "[begin-check]" => self.begin_check(split),
67            "[query-done]" => self.query_done(split),
68            "[eof]" => return Ok(false),
69            "[resolve-process]" => self.resolve_process(split),
70            "[resolve-lit]" => self.resolve_lit(split),
71            "[conflict]" => self.conflict(split),
72            _ => Err(Error::UnknownLine(first.to_owned())),
73        };
74        match parse {
75            Ok(()) => Ok(true),
76            Err(err) => {
77                eprintln!("Error parsing line {line_no} ({err:?}): {line:?}");
78                // Fail in debug mode, we should never get here
79                debug_assert!(false, "Failed to parse a line!");
80                match err.as_fatal() {
81                    Some(err) => Err(err),
82                    None => Ok(true),
83                }
84            }
85        }
86    }
87
88    fn end_of_file(&mut self) {
89        self.eof();
90    }
91}
92
93const DEFAULT: Result<()> = Ok(());
94pub trait Z3LogParser {
95    fn newline(&mut self) {}
96
97    /* Methods to handle each line case of Z3 logs.
98     `l` is a line split with spaces as delimiters,
99     and `l0` is the raw line (used only when )
100    */
101    fn version_info<'a>(&mut self, l: impl Iterator<Item = &'a str>) -> Result<()>;
102    fn mk_quant<'a>(&mut self, l: impl Iterator<Item = &'a str>) -> Result<()>;
103    fn mk_lambda<'a>(&mut self, l: impl Iterator<Item = &'a str>) -> Result<()>;
104    fn mk_var<'a>(&mut self, l: impl Iterator<Item = &'a str>) -> Result<()>;
105    fn mk_app<'a>(&mut self, l: impl Iterator<Item = &'a str>) -> Result<()>;
106    fn mk_proof<'a>(&mut self, l: impl Iterator<Item = &'a str>) -> Result<()>;
107    fn attach_meaning<'a>(&mut self, l: impl Iterator<Item = &'a str>) -> Result<()>;
108    fn attach_var_names<'a>(&mut self, l: impl Iterator<Item = &'a str>) -> Result<()>;
109    fn attach_enode<'a>(&mut self, l: impl Iterator<Item = &'a str>) -> Result<()>;
110    fn eq_expl<'a>(&mut self, l: impl Iterator<Item = &'a str>) -> Result<()>;
111    fn new_match<'a>(&mut self, l: impl Iterator<Item = &'a str>) -> Result<()>;
112    fn inst_discovered<'a>(&mut self, l: impl Iterator<Item = &'a str>) -> Result<()>;
113    fn instance<'a>(&mut self, l: impl Iterator<Item = &'a str>) -> Result<()>;
114    fn end_of_instance<'a>(&mut self, l: impl Iterator<Item = &'a str>) -> Result<()>;
115    fn push<'a>(&mut self, _l: impl Iterator<Item = &'a str>) -> Result<()>;
116    fn pop<'a>(&mut self, _l: impl Iterator<Item = &'a str>) -> Result<()>;
117    fn eof(&mut self);
118
119    // unused in original parser
120    fn decide_and_or<'a>(&mut self, _l: impl Iterator<Item = &'a str>) -> Result<()> {
121        DEFAULT
122    }
123    fn decide<'a>(&mut self, _l: impl Iterator<Item = &'a str>) -> Result<()> {
124        DEFAULT
125    }
126    fn assign<'a>(&mut self, _l: impl Iterator<Item = &'a str>) -> Result<()> {
127        DEFAULT
128    }
129    fn begin_check<'a>(&mut self, _l: impl Iterator<Item = &'a str>) -> Result<()> {
130        DEFAULT
131    }
132    fn query_done<'a>(&mut self, _l: impl Iterator<Item = &'a str>) -> Result<()> {
133        DEFAULT
134    }
135    fn resolve_process<'a>(&mut self, _l: impl Iterator<Item = &'a str>) -> Result<()> {
136        DEFAULT
137    }
138    fn resolve_lit<'a>(&mut self, _l: impl Iterator<Item = &'a str>) -> Result<()> {
139        DEFAULT
140    }
141    fn conflict<'a>(&mut self, _l: impl Iterator<Item = &'a str>) -> Result<()> {
142        DEFAULT
143    }
144}
145
146/// Type of solver and version number
147#[derive(Debug, PartialEq, Default)]
148pub enum VersionInfo {
149    #[default]
150    None,
151    Present {
152        solver: String,
153        version: semver::Version,
154    },
155}
156impl VersionInfo {
157    pub fn solver(&self) -> Option<&str> {
158        match self {
159            VersionInfo::Present { solver, .. } => Some(solver),
160            VersionInfo::None => None,
161        }
162    }
163    pub fn version(&self) -> Option<&semver::Version> {
164        match self {
165            VersionInfo::Present { version, .. } => Some(version),
166            VersionInfo::None => None,
167        }
168    }
169    pub fn is_version(&self, major: u64, minor: u64, patch: u64) -> bool {
170        self.version()
171            .is_some_and(|v| v == &semver::Version::new(major, minor, patch))
172    }
173
174    pub fn is_version_minor(&self, major: u64, minor: u64) -> bool {
175        self.version().is_some_and(|v| {
176            &semver::Version::new(major, minor, 0) <= v
177                && v <= &semver::Version::new(major, minor, u64::MAX)
178        })
179    }
180
181    pub fn is_ge_version(&self, major: u64, minor: u64, patch: u64) -> bool {
182        self.version()
183            .is_some_and(|v| v >= &semver::Version::new(major, minor, patch))
184    }
185
186    pub fn is_le_version(&self, major: u64, minor: u64, patch: u64) -> bool {
187        self.version()
188            .is_some_and(|v| v <= &semver::Version::new(major, minor, patch))
189    }
190}
smt_scope/parsers/z3/mod.rs

smt_scope/parsers/z3/
mod.rs
