From 5ef2533ad30d8259904b50d182d055ee3e7d94d0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jon=C3=A1=C5=A1=20Fiala?= <jonas.fiala@inf.ethz.ch>
Date: Mon, 18 Dec 2023 20:06:51 +0100
Subject: [PATCH] Bodge to parse quantifier names with spaces

---
 smt-log-parser/src/items.rs               |  2 +-
 smt-log-parser/src/parsers/z3/z3parser.rs | 13 +++++++++++--
 smt-log-parser/tests/parse_logs.rs        |  4 ++--
 3 files changed, 14 insertions(+), 5 deletions(-)

diff --git a/smt-log-parser/src/items.rs b/smt-log-parser/src/items.rs
index dd52a2da..59ba4f5d 100644
--- a/smt-log-parser/src/items.rs
+++ b/smt-log-parser/src/items.rs
@@ -128,7 +128,7 @@ impl QuantKind {
                 name: name.to_string(),
                 id,
             })
-            .unwrap_or_else(|| Self::NamedQuant(name.to_string()))
+            .unwrap_or_else(|| Self::NamedQuant(value.to_string()))
     }
     pub fn is_discovered(&self) -> bool {
         matches!(self, Self::Other(_))
diff --git a/smt-log-parser/src/parsers/z3/z3parser.rs b/smt-log-parser/src/parsers/z3/z3parser.rs
index ff554b93..dc2813ac 100644
--- a/smt-log-parser/src/parsers/z3/z3parser.rs
+++ b/smt-log-parser/src/parsers/z3/z3parser.rs
@@ -167,8 +167,17 @@ impl Z3LogParser for Z3Parser {
 
     fn mk_quant<'a>(&mut self, mut l: impl Iterator<Item = &'a str>) -> Option<()> {
         let full_id = l.next().and_then(TermIdCow::parse)?;
-        let quant_name = l.next().map(QuantKind::parse)?;
-        let num_vars = l.next()?.parse().ok()?;
+        let mut quant_name = std::borrow::Cow::Borrowed(l.next()?);
+        let mut num_vars_str = l.next()?;
+        let mut num_vars = num_vars_str.parse::<usize>();
+        // The name may contain spaces... TODO: PR to add quotes around name when logging in z3
+        while num_vars.is_err() {
+            quant_name = std::borrow::Cow::Owned(format!("{quant_name} {num_vars_str}"));
+            num_vars_str = l.next()?;
+            num_vars = num_vars_str.parse::<usize>();
+        }
+        let quant_name = QuantKind::parse(&*quant_name);
+        let num_vars = num_vars.unwrap();
         let children = self.gobble_children(l)?;
         assert!(!children.is_empty());
         let qidx = self.quantifiers.next_key();
diff --git a/smt-log-parser/tests/parse_logs.rs b/smt-log-parser/tests/parse_logs.rs
index dc6add15..49ea0558 100644
--- a/smt-log-parser/tests/parse_logs.rs
+++ b/smt-log-parser/tests/parse_logs.rs
@@ -11,8 +11,8 @@ fn parse_all_logs() {
         let filename = log.unwrap().path();
         println!("Parsing {}", filename.display());
         let (metadata, parser) = Z3Parser::from_file(filename).unwrap();
-        // Gives 20 millis per MB (or 20 secs per GB)
-        let to = Duration::from_millis(500 + (metadata.len() / 50_000));
+        // Gives 50 millis per MB (or 50 secs per GB)
+        let to = Duration::from_millis(500 + (metadata.len() / 20_000));
         let (timeout, _result) = parser.process_all_timeout(to);
         assert!(timeout.is_none());
     }