diff --git a/smt-log-parser/design-docs/restrictions.md b/smt-log-parser/design-docs/restrictions.md index eed0806d..cd8ff556 100644 --- a/smt-log-parser/design-docs/restrictions.md +++ b/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). diff --git a/smt-log-parser/src/error.rs b/smt-log-parser/src/error.rs index a8376e46..5d5518c1 100644 --- a/smt-log-parser/src/error.rs +++ b/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), diff --git a/smt-log-parser/src/items/term.rs b/smt-log-parser/src/items/term.rs index f1e4ac97..db4c653e 100644 --- a/smt-log-parser/src/items/term.rs +++ b/smt-log-parser/src/items/term.rs @@ -68,12 +68,12 @@ impl TermId { pub fn parse(strings: &mut StringTable, value: &str) -> Result { 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::().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 { diff --git a/smt-log-parser/src/parsers/z3/bugs.rs b/smt-log-parser/src/parsers/z3/bugs.rs index 1a22689b..f8b5a414 100644 --- a/smt-log-parser/src/parsers/z3/bugs.rs +++ b/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 `` 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 == "" + } 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, + ) -> 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.ends_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::().map_err(E::InvalidVarNum)?; + return Ok((qid, nvs)); + } + + let mut nvs = num_vars.parse::(); + 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::(); + } + 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, + ) -> Result<(Cow<'a, str>, Option)> { + 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 { - let mut term_id = TermId::parse(strings, id)?; + pub fn parse_app_child_id(&self, mut term_id: TermId) -> Result { if let Some(namespace) = self.bug.get_model { debug_assert!(term_id.namespace.is_none()); term_id.namespace = Some(namespace); diff --git a/smt-log-parser/src/parsers/z3/parse.rs b/smt-log-parser/src/parsers/z3/parse.rs index fb3f322a..0ad7dbf6 100644 --- a/smt-log-parser/src/parsers/z3/parse.rs +++ b/smt-log-parser/src/parsers/z3/parse.rs @@ -73,10 +73,7 @@ impl Z3Parser { } } - fn map<'a, T>( - l: impl Iterator, - f: impl FnMut(&'a str) -> Result, - ) -> Result> { + fn map(l: impl Iterator, f: impl FnMut(T) -> Result) -> Result> { l.map(f).collect() } fn gobble_var_names_list<'a>(&mut self, l: impl Iterator) -> Result { @@ -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) { - "" - } 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) -> 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::(); - // 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::(); - } + 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) -> 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::().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) -> 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), diff --git a/smt-problems/handwritten/issue/106_spaces.smt2 b/smt-problems/handwritten/issue/106_spaces.smt2 new file mode 100644 index 00000000..47fbb069 --- /dev/null +++ b/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)