Correctly parse term names with spaces

smt-log-parser/design-docs/restrictions.md

@@ -6,4 +6,9 @@ If these restrictions are not satisfied these workarounds might fail and lines i
 
 The following restrictions apply to choosing names for `declare-fun` and `declare-const`:
 
-- The names `string`, `indent`, `compose`, `choice` and `cr` are forbidden ([#100](https://github.com/viperproject/axiom-profiler-2/issues/100)).
+- The names `string`, `indent`, `compose`, `choice` and `cr` are forbidden. Issue [#100](https://github.com/viperproject/axiom-profiler-2/issues/100).
+- Any names with spaces of which a non-first word ends with `#[0-9]*` (e.g. `(declare-const |x foo#1 #| Int)`). Examples which are fine are e.g. `|#3 x|` or `|(x #3)|`. Issue [#106](https://github.com/viperproject/axiom-profiler-2/issues/106).
+
+The following restrictions apply to choosing names for quantifiers (specified with `:qid`):
+
+- **(z3 <= v4.8.17)** Any names with spaces of which a non-first word contains digits only (e.g. `:qid |qname 10 2|`). Names with spaces where no non-first word can be parsed as a number are fine (e.g. `:qid |10 q50 3plus|`). Resolved with z3[#6081](https://github.com/Z3Prover/z3/issues/6081).

smt-log-parser/src/error.rs

@@ -51,6 +51,7 @@ pub enum Error {
     // Quantifier
     VarNamesListInconsistent, // attach var names
     VarNamesNoBar,
+    InvalidVarNum(ParseIntError),
     UnknownQuantifierIdx(TermIdx),
     NonNullLambdaName(String),
     InvalidQVarInteger(ParseIntError),

smt-log-parser/src/items/term.rs

@@ -68,12 +68,12 @@ impl TermId {
     pub fn parse(strings: &mut StringTable, value: &str) -> Result<Self> {
         let hash_idx = value.bytes().position(|b| b == b'#');
         let hash_idx = hash_idx.ok_or_else(|| Error::InvalidIdHash(value.to_string()))?;
-        let namespace = (hash_idx != 0).then(|| IString(strings.get_or_intern(&value[..hash_idx])));
-        let id = &value[hash_idx + 1..];
-        let id = match id {
+        let (namespace, id) = value.split_at(hash_idx);
+        let id = match &id[1..] {
             "" => None,
             id => Some(id.parse::<NonMaxU32>().map_err(Error::InvalidIdNumber)?),
         };
+        let namespace = (!namespace.is_empty()).then(|| IString(strings.get_or_intern(namespace)));
         Ok(Self { namespace, id })
     }
     pub fn order(&self) -> u32 {

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

@@ -1,3 +1,5 @@
+use std::borrow::Cow;
+
 #[cfg(feature = "mem_dbg")]
 use mem_dbg::{MemDbg, MemSize};
 
@@ -8,6 +10,96 @@ use crate::{
 
 use super::{terms::Terms, Z3Parser};
 
+// Z3 FIXED (v4.9.0+) https://github.com/Z3Prover/z3/issues/6081
+// This changes `null` to `<null>` and adds `|` around :qid with spaces.
+
+impl Z3Parser {
+    fn is_z3_6081_fixed(&self) -> bool {
+        self.version_info.is_ge_version(4, 9, 0)
+    }
+
+    pub(super) fn check_lambda_name(&self, lambda: &str) -> Result<()> {
+        let correct = if self.is_z3_6081_fixed() {
+            lambda == "<null>"
+        } else {
+            lambda == "null"
+        };
+        correct
+            .then_some(())
+            .ok_or_else(|| E::NonNullLambdaName(lambda.to_string()))
+    }
+
+    pub(super) fn parse_qid<'a>(
+        &self,
+        l: &mut impl Iterator<Item = &'a str>,
+    ) -> Result<(Cow<'a, str>, u32)> {
+        let mut qid = Cow::Borrowed(l.next().ok_or(E::UnexpectedNewline)?);
+        let mut num_vars = l.next().ok_or(E::UnexpectedNewline)?;
+        if self.is_z3_6081_fixed() {
+            if qid.starts_with('|') {
+                qid += " ";
+                qid += num_vars;
+                while !num_vars.ends_with('|') {
+                    num_vars = l.next().ok_or(E::UnexpectedNewline)?;
+                    qid += " ";
+                    qid += num_vars;
+                }
+                num_vars = l.next().ok_or(E::UnexpectedNewline)?;
+            }
+            let nvs = num_vars.parse::<u32>().map_err(E::InvalidVarNum)?;
+            return Ok((qid, nvs));
+        }
+
+        let mut nvs = num_vars.parse::<u32>();
+        if nvs.is_err() {
+            qid = Cow::Owned(format!("|{qid}"));
+        }
+        while nvs.is_err() {
+            qid += " ";
+            qid += num_vars;
+            num_vars = l.next().ok_or(E::UnexpectedNewline)?;
+            nvs = num_vars.parse::<u32>();
+        }
+        if matches!(qid, Cow::Owned(_)) {
+            qid += "|";
+        }
+        Ok((qid, nvs.unwrap()))
+    }
+}
+
+// Z3 BUG: https://github.com/viperproject/axiom-profiler-2/issues/106
+
+impl Z3Parser {
+    pub(super) fn parse_app_name<'a>(
+        &mut self,
+        l: &mut impl Iterator<Item = &'a str>,
+    ) -> Result<(Cow<'a, str>, Option<TermId>)> {
+        let mut name = Cow::Borrowed(l.next().ok_or(E::UnexpectedNewline)?);
+        let mut l = l.map(|id| (id, TermId::parse(&mut self.strings, id)));
+        let mut idp = l.next();
+
+        let post = |name: Cow<'a, str>| match name {
+            Cow::Borrowed(n) => Cow::Borrowed(n),
+            Cow::Owned(mut n) => {
+                n += "|";
+                Cow::Owned(n)
+            }
+        };
+        while let Some((ids, id)) = idp {
+            if let Ok(id) = id {
+                return Ok((post(name), Some(id)));
+            }
+            if let Cow::Borrowed(n) = name {
+                name = Cow::Owned(format!("|{n}"));
+            }
+            name += " ";
+            name += ids;
+            idp = l.next();
+        }
+        Ok((post(name), None))
+    }
+}
+
 // Z3 BUG: https://github.com/viperproject/axiom-profiler-2/issues/63
 
 impl Z3Parser {
@@ -191,8 +283,7 @@ pub(super) struct TermsBug {
 impl Terms {
     /// Normally one would use `app_terms.parse_existing_id`, but here we
     /// implement the workaround for `get_model`.
-    pub fn parse_app_child_id(&self, strings: &mut StringTable, id: &str) -> Result<TermIdx> {
-        let mut term_id = TermId::parse(strings, id)?;
+    pub fn parse_app_child_id(&self, mut term_id: TermId) -> Result<TermIdx> {
         if let Some(namespace) = self.bug.get_model {
             debug_assert!(term_id.namespace.is_none());
             term_id.namespace = Some(namespace);

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

@@ -73,10 +73,7 @@ impl Z3Parser {
         }
     }
 
-    fn map<'a, T>(
-        l: impl Iterator<Item = &'a str>,
-        f: impl FnMut(&'a str) -> Result<T>,
-    ) -> Result<BoxSlice<T>> {
+    fn map<T, U>(l: impl Iterator<Item = T>, f: impl FnMut(T) -> Result<U>) -> Result<BoxSlice<U>> {
         l.map(f).collect()
     }
     fn gobble_var_names_list<'a>(&mut self, l: impl Iterator<Item = &'a str>) -> Result<VarNames> {
@@ -231,14 +228,6 @@ impl Z3Parser {
         Ok(IString(self.strings.try_get_or_intern(s)?))
     }
 
-    fn expected_null_str(&self) -> &'static str {
-        if self.version_info.is_ge_version(4, 11, 0) {
-            "<null>"
-        } else {
-            "null"
-        }
-    }
-
     fn quant_or_lamda(
         &mut self,
         full_id: TermId,
@@ -389,17 +378,8 @@ impl Z3LogParser for Z3Parser {
 
     fn mk_quant<'a>(&mut self, mut l: impl Iterator<Item = &'a str>) -> Result<()> {
         let full_id = self.parse_new_full_id(l.next())?;
-        let mut quant_name = std::borrow::Cow::Borrowed(l.next().ok_or(E::UnexpectedNewline)?);
-        let mut num_vars_str = l.next().ok_or(E::UnexpectedNewline)?;
-        let mut num_vars = num_vars_str.parse::<u32>();
-        // 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().ok_or(E::UnexpectedNewline)?;
-            num_vars = num_vars_str.parse::<u32>();
-        }
+        let (quant_name, num_vars) = self.parse_qid(&mut l)?;
         let quant_name = QuantKind::parse(&mut self.strings, &quant_name);
-        let num_vars = num_vars.unwrap();
         let child_ids = Self::map(l, |id| self.parse_existing_app(id))?;
         assert!(!child_ids.is_empty());
         let child_id_names = || {
@@ -417,10 +397,8 @@ impl Z3LogParser for Z3Parser {
 
     fn mk_lambda<'a>(&mut self, mut l: impl Iterator<Item = &'a str>) -> Result<()> {
         let full_id = self.parse_new_full_id(l.next())?;
-        let lambda_name = l.next().ok_or(E::UnexpectedNewline)?;
-        if lambda_name != self.expected_null_str() {
-            return Err(E::NonNullLambdaName(lambda_name.to_string()));
-        }
+        let lambda = l.next().ok_or(E::UnexpectedNewline)?;
+        self.check_lambda_name(lambda)?;
         let num_vars = l.next().ok_or(E::UnexpectedNewline)?;
         let num_vars = num_vars.parse::<u32>().map_err(E::InvalidQVarInteger)?;
         let child_ids = Self::map(l, |id| self.parse_existing_proof(id))?;
@@ -446,12 +424,15 @@ impl Z3LogParser for Z3Parser {
     fn mk_app<'a>(&mut self, mut l: impl Iterator<Item = &'a str>) -> Result<()> {
         let id_str = l.next().ok_or(E::UnexpectedNewline)?;
         let mut id = TermId::parse(&mut self.strings, id_str)?;
-        let name = l.next().ok_or(E::UnexpectedNewline)?;
-        debug_assert!(name != "true" || id_str == "#1");
-        debug_assert!(name != "false" || id_str == "#2");
-        self.terms.check_get_model(&mut id, name, &mut self.strings);
-        let name = self.mk_string(name)?;
-        let child_ids = Self::map(l, |id| self.terms.parse_app_child_id(&mut self.strings, id))?;
+        let (name, child) = self.parse_app_name(&mut l)?;
+        debug_assert!(id_str != "#1" || name == "true");
+        debug_assert!(id_str != "#2" || name == "false");
+        self.terms
+            .check_get_model(&mut id, &name, &mut self.strings);
+        let name = self.mk_string(&name)?;
+        let child = child.into_iter().map(Ok);
+        let child_ids = child.chain(l.map(|id| TermId::parse(&mut self.strings, id)));
+        let child_ids = Self::map(child_ids, |id| self.terms.parse_app_child_id(id?))?;
         let term = Term {
             id,
             kind: TermKind::App(name),

smt-problems/handwritten/issue/106_spaces.smt2

@@ -0,0 +1,12 @@
+; https://github.com/viperproject/axiom-profiler-2/issues/106
+
+(push)(pop)
+(declare-fun |#1 f| (Int) Int)
+(declare-fun |(f #1)| (Int) Int)
+
+(assert (forall ((i Int))
+    (!  (> (|#1 f| i) (|(f #1)| i))
+        :pattern ((|#1 f| i) (|(f #1)| i)) :qid |21 q2 39i|
+    )))
+(assert (= (|#1 f| 0) (|(f #1)| 0)))
+(check-sat)