Merge pull request #12 from JonasAlaif/fix-parsing-issues

smt-log-parser/src/parsers/mod.rs

@@ -13,6 +13,11 @@ pub mod z3;
 /// Trait for a generic SMT solver trace parser. Intended to support different
 /// solvers or log formats.
 pub trait LogParser: Default + Debug {
+    /// Can be used to allow for parsing entries across multiple lines.
+    fn is_line_start(&mut self, _first_byte: u8) -> bool {
+        true
+    }
+
     /// Process a single line of the log file. Return `true` if parsing should
     /// continue, or `false` if parsing should stop.
     fn process_line(&mut self, line: &str, line_no: usize) -> bool;
@@ -213,7 +218,16 @@ mod wrapper {
             while predicate(&self.parser, self.reader_state) {
                 buf.clear();
                 // Read line
-                let bytes_read = add_await([reader.read_line(&mut buf)]).unwrap();
+                let mut bytes_read = 0;
+
+                loop {
+                    bytes_read += add_await([reader.read_line(&mut buf)]).unwrap();
+                    let peek = add_await([reader.fill_buf()]).unwrap();
+                    // Stop reading if this is the end or we don't have a multiline.
+                    if peek.is_empty() || self.parser.is_line_start(peek[0]) {
+                        break;
+                    }
+                }
                 // Remove newline from end
                 if buf.ends_with('\n') {
                     buf.pop();

smt-log-parser/src/parsers/z3/inst_graph.rs

@@ -337,15 +337,9 @@ impl InstGraph {
         }
     }
 
-    fn fresh_line_nr(&self, line_nr: usize) -> bool {
-        self.inst_graph
-            .node_weights()
-            .all(|node| node.line_nr != line_nr)
-    }
-
     fn add_node(&mut self, node_data: NodeData) {
         let line_nr = node_data.line_nr;
-        if self.fresh_line_nr(line_nr) {
+        if !self.node_of_line_nr.contains_key(&line_nr) {
             let node = self.inst_graph.add_node(node_data);
             self.orig_graph.add_node(node_data);
             self.node_of_line_nr.insert(line_nr, node);

smt-log-parser/src/parsers/z3/mod.rs

@@ -10,12 +10,18 @@ pub mod z3parser;
 // pub mod dump;
 
 impl<T: Z3LogParser + Default> LogParser for T {
+    fn is_line_start(&mut self, first_byte: u8) -> bool {
+        first_byte == b'['
+    }
+
     fn process_line(&mut self, line: &str, line_no: usize) -> bool {
         // Much faster than `split_whitespace` or `split(' ')` since it works on
         // [u8] instead of [char] and so doesn't need to convert to UTF-8.
         let mut split = line.split_ascii_whitespace();
-        // println!("Processing {line:?} ({line_no})");
-        let parse = match split.next().unwrap() {
+        let Some(first) = split.next() else {
+            return true;
+        };
+        let parse = match first {
             // match the line case
             "[tool-version]" => self.version_info(split),
             "[mk-quant]" | "[mk-lambda]" => self.mk_quant(split),