Handle strange equality blaming in v4.12.3 and onwards and increase t…

…imeout

smt-log-parser/src/display_with.rs

@@ -147,8 +147,10 @@ mod private {
     }
 }
 use private::*;
+// lower inside higher needs brackets around the lower
 const NO_BIND: u8 = 0;
 const QUANT_BIND: u8 = 3;
+const TERNARY_BIND: u8 = 7;
 const INFIX_BIND: u8 = 15;
 const PREFIX_BIND: u8 = 31;
 
@@ -190,10 +192,10 @@ impl DisplayWithCtxt<DisplayCtxt<'_>, ()> for QuantIdx {
         if let Some(term) = quant.term {
             term.fmt_with(f, ctxt, data)
         } else {
-            let QuantKind::Other(name) = &quant.kind else {
+            let QuantKind::Other(name) = quant.kind else {
                 panic!()
             };
-            write!(f, "{}", ctxt.parser.strings.resolve(name))
+            write!(f, "{}", &ctxt.parser.strings[name])
         }
     }
 }
@@ -214,7 +216,7 @@ impl DisplayWithCtxt<DisplayCtxt<'_>, ()> for &MatchKind {
                 write!(
                     f,
                     "[TheorySolving] {}#",
-                    ctxt.parser.strings.resolve(&axiom_id.namespace)
+                    &ctxt.parser.strings[axiom_id.namespace],
                 )?;
                 if let Some(id) = axiom_id.id {
                     write!(f, "{id}")?;
@@ -243,7 +245,7 @@ impl<'a: 'b, 'b> DisplayWithCtxt<DisplayCtxt<'b>, DisplayData<'b>> for &'a Term
     ) -> fmt::Result {
         data.with_children(&self.child_ids, |data| {
             if ctxt.display_term_ids {
-                let namespace = ctxt.parser.strings.resolve(&self.id.namespace);
+                let namespace = &ctxt.parser.strings[self.id.namespace];
                 let id = self.id.id.map(|id| id.to_string()).unwrap_or_default();
                 write!(f, "[{namespace}#{id}]")?;
             }
@@ -275,12 +277,13 @@ impl<'a, 'b> DisplayWithCtxt<DisplayCtxt<'b>, DisplayData<'b>> for &'a TermKind
     }
 }
 
-enum ProofOrAppKind {
-    Unary,
-    Inline,
+enum ProofOrAppKind<'a> {
+    Unary(&'a str),
+    Inline(&'a str),
+    Ternary(&'a str, &'a str),
     Pattern,
-    OtherApp,
-    Proof,
+    OtherApp(&'a str),
+    Proof(&'a str),
 }
 impl<'a, 'b> DisplayWithCtxt<DisplayCtxt<'b>, DisplayData<'b>> for &'a ProofOrApp {
     fn fmt_with(
@@ -291,38 +294,39 @@ impl<'a, 'b> DisplayWithCtxt<DisplayCtxt<'b>, DisplayData<'b>> for &'a ProofOrAp
     ) -> fmt::Result {
         let math = ctxt.use_mathematical_symbols;
         use ProofOrAppKind::*;
-        let name = ctxt.parser.strings.resolve(&self.name);
-        let (name, kind) = match name {
-            name if self.is_proof => (name, Proof),
-            "not" => (if math { "¬" } else { "!" }, Unary),
-            "-" if data.children().len() == 1 => ("-", Unary),
+        let name = &ctxt.parser.strings[self.name];
+        let kind = match name {
+            name if self.is_proof => Proof(name),
+            "not" => Unary(if math { "¬" } else { "!" }),
+            "-" if data.children().len() == 1 => Unary("-"),
 
-            "and" => (if math { "∧" } else { "&&" }, Inline),
-            "or" => (if math { "∨" } else { "||" }, Inline),
-            "<=" => (if math { "≤" } else { "<=" }, Inline),
-            ">=" => (if math { "≥" } else { ">=" }, Inline),
-            op @ ("=" | "+" | "-" | "*" | "/" | "<" | ">") => (op, Inline),
+            "and" => Inline(if math { "∧" } else { "&&" }),
+            "or" => Inline(if math { "∨" } else { "||" }),
+            "<=" => Inline(if math { "≤" } else { "<=" }),
+            ">=" => Inline(if math { "≥" } else { ">=" }),
+            op @ ("=" | "+" | "-" | "*" | "/" | "<" | ">") => Inline(op),
 
-            "pattern" => ("pattern", Pattern),
+            "if" => Ternary("?", ":"),
 
-            name => (name, OtherApp),
+            "pattern" => Pattern,
+
+            name => OtherApp(name),
         };
         match kind {
-            Unary => data.with_bind_power(PREFIX_BIND, |data, bind_power| {
+            Unary(op) => data.with_bind_power(PREFIX_BIND, |data, bind_power| {
                 assert!(bind_power <= PREFIX_BIND);
                 assert_eq!(data.children().len(), 1);
                 let child = data.children()[0];
-                let child = &ctxt.parser[child];
-                write!(f, "{name}{}", child.with_data(ctxt, data))
+                write!(f, "{op}{}", ctxt.parser[child].with_data(ctxt, data))
             }),
-            Inline => data.with_bind_power(INFIX_BIND, |data, bind_power| {
+            Inline(op) => data.with_bind_power(INFIX_BIND, |data, bind_power| {
                 let need_brackets = bind_power >= INFIX_BIND;
                 if need_brackets {
                     write!(f, "(")?;
                 }
                 for (idx, child) in data.children().iter().enumerate() {
                     if idx != 0 {
-                        write!(f, " {name} ")?;
+                        write!(f, " {op} ")?;
                     }
                     write!(f, "{}", ctxt.parser[*child].with_data(ctxt, data))?;
                 }
@@ -331,6 +335,35 @@ impl<'a, 'b> DisplayWithCtxt<DisplayCtxt<'b>, DisplayData<'b>> for &'a ProofOrAp
                 }
                 Ok(())
             }),
+            Ternary(op1, op2) => data.with_bind_power(TERNARY_BIND, |data, bind_power| {
+                let need_brackets = bind_power >= TERNARY_BIND;
+                if need_brackets {
+                    write!(f, "(")?;
+                }
+                assert_eq!(data.children().len(), 3);
+                let cond = data.children()[0];
+                write!(
+                    f,
+                    "{} {op1}",
+                    ctxt.parser[cond].with_data(ctxt, data)
+                )?;
+                let then = data.children()[1];
+                write!(
+                    f,
+                    " {} {op2}",
+                    ctxt.parser[then].with_data(ctxt, data)
+                )?;
+                let else_ = data.children()[2];
+                write!(
+                    f,
+                    " {}",
+                    ctxt.parser[else_].with_data(ctxt, data)
+                )?;
+                if need_brackets {
+                    write!(f, ")")?;
+                }
+                Ok(())
+            }),
             Pattern => data.with_bind_power(NO_BIND, |data, _| {
                 // BIND_POWER is highest
                 write!(f, "{{")?;
@@ -342,7 +375,7 @@ impl<'a, 'b> DisplayWithCtxt<DisplayCtxt<'b>, DisplayData<'b>> for &'a ProofOrAp
                 }
                 write!(f, "}}")
             }),
-            OtherApp | Proof => data.with_bind_power(NO_BIND, |data, _| {
+            OtherApp(name) | Proof(name) => data.with_bind_power(NO_BIND, |data, _| {
                 // BIND_POWER is highest
                 write!(f, "{name}")?;
                 if data.children().is_empty() {
@@ -368,8 +401,8 @@ impl<'a> DisplayWithCtxt<DisplayCtxt<'a>, DisplayData<'a>> for &'a Meaning {
         ctxt: &DisplayCtxt<'a>,
         _data: &mut DisplayData<'a>,
     ) -> fmt::Result {
-        let theory = ctxt.parser.strings.resolve(&self.theory);
-        let value = ctxt.parser.strings.resolve(&self.value);
+        let theory = &ctxt.parser.strings[self.theory];
+        let value = &ctxt.parser.strings[self.value];
         match theory {
             "arith" | "bv" => write!(f, "{value}"),
             theory => write!(f, "/{theory} {value}\\"),
@@ -434,12 +467,12 @@ impl<'a> DisplayWithCtxt<DisplayCtxt<'a>, DisplayData<'a>> for &'a QuantKind {
         }
         if ctxt.display_quantifier_name {
             write!(f, "\"")?;
-            match self {
-                QuantKind::Other(kind) => write!(f, "{}", ctxt.parser.strings.resolve(kind))?,
+            match *self {
+                QuantKind::Other(kind) => write!(f, "{}", &ctxt.parser.strings[kind])?,
                 QuantKind::Lambda => write!(f, "<null>")?,
-                QuantKind::NamedQuant(name) => write!(f, "{}", ctxt.parser.strings.resolve(name))?,
+                QuantKind::NamedQuant(name) => write!(f, "{}", &ctxt.parser.strings[name])?,
                 QuantKind::UnnamedQuant { name, id } => {
-                    write!(f, "{}!{id}", ctxt.parser.strings.resolve(name))?
+                    write!(f, "{}!{id}", &ctxt.parser.strings[name])?
                 }
             };
             write!(f, "\" ")?;

smt-log-parser/src/items.rs

@@ -79,6 +79,12 @@ impl TermKind {
             _ => None,
         }
     }
+    pub fn app_name(&self) -> Option<IString> {
+        match self {
+            Self::ProofOrApp(ProofOrApp { is_proof: false, name }) => Some(*name),
+            _ => None,
+        }
+    }
 }
 
 #[derive(Debug, Serialize, Deserialize, PartialEq, Eq)]
@@ -145,18 +151,18 @@ pub enum VarNames {
 impl VarNames {
     pub fn get_name<'a>(strings: &'a StringTable, this: &Option<Self>, idx: usize) -> Cow<'a, str> {
         match this {
-            Some(Self::NameAndType(names)) => Cow::Borrowed(strings.resolve(&names[idx].0)),
+            Some(Self::NameAndType(names)) => Cow::Borrowed(&strings[names[idx].0]),
             None | Some(Self::TypeOnly(_)) => Cow::Owned(format!("qvar_{idx}")),
         }
     }
     pub fn get_type(strings: &StringTable, this: &Option<Self>, idx: usize) -> String {
         this.as_ref()
             .map(|this| {
                 let ty = match this {
-                    Self::TypeOnly(names) => &names[idx],
-                    Self::NameAndType(names) => &names[idx].1,
+                    Self::TypeOnly(names) => names[idx],
+                    Self::NameAndType(names) => names[idx].1,
                 };
-                format!(": {}", strings.resolve(ty))
+                format!(": {}", &strings[ty])
             })
             .unwrap_or_default()
     }

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

@@ -19,14 +19,14 @@ impl EGraph {
         z3_generation: Option<u32>,
         stack: &Stack,
     ) -> ENodeIdx {
-        if created_by.is_none() && z3_generation.is_some() {
-            // TODO: why does this happen sometimes?
-            // debug_assert_eq!(
-            //     z3_generation.unwrap(),
-            //     0,
-            //     "enode with no creator has non-zero generation"
-            // );
-        }
+        // TODO: why does this happen sometimes?
+        // if created_by.is_none() && z3_generation.is_some() {
+        //     debug_assert_eq!(
+        //         z3_generation.unwrap(),
+        //         0,
+        //         "enode with no creator has non-zero generation"
+        //     );
+        // }
         let enode = self.enodes.push_and_get_key(ENode {
             frame: stack.active_frame(),
             created_by,
@@ -54,6 +54,10 @@ impl EGraph {
         }
     }
 
+    pub fn get_owner(&self, enode: ENodeIdx) -> TermIdx {
+        self.enodes[enode].owner
+    }
+
     pub fn new_equality(&mut self, from: ENodeIdx, expl: EqualityExpl, stack: &Stack) {
         let enode = &mut self.enodes[from];
         let to = expl.to();
@@ -98,20 +102,30 @@ impl EGraph {
         path
     }
 
-    pub fn get_equalities<'a: 'b, 'b>(&'a self, from: ENodeIdx, to: ENodeIdx, stack: &'b Stack) -> impl Iterator<Item = &'a EqualityExpl> + 'b {
-        let from = self.path_to_root(from, stack, 0);
-        let to = self.path_to_root(to, stack, 0);
-        assert_eq!(from[0], to[0]);
+    #[must_use]
+    pub fn get_equalities<'a: 'b, 'b>(&'a self, from: ENodeIdx, to: ENodeIdx, stack: &'b Stack, can_mismatch: impl Fn() -> bool) -> Option<impl Iterator<Item = &'a EqualityExpl> + 'b> {
+        let f_path = self.path_to_root(from, stack, 0);
+        let t_path = self.path_to_root(to, stack, 0);
         let mut shared = 1;
-        while shared < from.len() && shared < to.len() && from[shared] == to[shared] {
+        if f_path[0] != t_path[0] {
+            // Root may not always be the same from v4.12.3 onwards if `to` is an `ite` expression. See:
+            // https://github.com/Z3Prover/z3/commit/faf14012ba18d21c1fcddbdc321ac127f019fa03#diff-0a9ec50ded668e51578edc67ecfe32380336b9cbf12c5d297e2d3759a7a39847R2417-R2419
+            if !can_mismatch() {
+                return None;
+            }
+            // Return an empty iterator if the roots are different.
+            shared = f_path.len().max(t_path.len());
+        }
+        while shared < f_path.len() && shared < t_path.len() && f_path[shared] == t_path[shared] {
             shared += 1;
         }
-        let all = from.into_iter().skip(shared).rev().chain(to.into_iter().skip(shared));
-        all.map(|idx| &self.enodes[idx].get_equality(stack).unwrap().expl)
+        let all = f_path.into_iter().skip(shared).rev().chain(t_path.into_iter().skip(shared));
+        Some(all.map(|idx| &self.enodes[idx].get_equality(stack).unwrap().expl))
     }
 
-    pub fn blame_equalities(&self, from: ENodeIdx, to: ENodeIdx, stack: &Stack, blamed: &mut Vec<BlameKind>) {
-        for eq in self.get_equalities(from, to, stack) {
+    #[must_use]
+    pub fn blame_equalities(&self, from: ENodeIdx, to: ENodeIdx, stack: &Stack, blamed: &mut Vec<BlameKind>, can_mismatch: impl Fn() -> bool) -> Option<()> {
+        for eq in self.get_equalities(from, to, stack, can_mismatch)? {
             // TODO: figure out if this is all the blames we need.
             match eq {
                 EqualityExpl::Root { .. } => unreachable!(),
@@ -120,14 +134,16 @@ impl EGraph {
                 }
                 EqualityExpl::Congruence { arg_eqs, .. } => {
                     for (from, to) in arg_eqs.iter() {
-                        self.blame_equalities(*from, *to, stack, blamed);
+                        fn cannot_mismatch() -> bool { false }
+                        self.blame_equalities(*from, *to, stack, blamed, cannot_mismatch)?;
                     }
                 }
                 EqualityExpl::Theory { .. } => (),
                 EqualityExpl::Axiom { .. } => (),
                 EqualityExpl::Unknown { .. } => (),
             }
         }
+        Some(())
     }
 }
 

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

@@ -50,14 +50,17 @@ impl Z3Parser {
     pub fn version_info(&self) -> Option<&VersionInfo> {
         self.version_info.as_ref()
     }
-    pub fn is_version(&self, version: semver::Version) -> bool {
-        self.version_info.as_ref().is_some_and(|v| v.version == version)
+    pub fn is_version(&self, major: u64, minor: u64, patch: u64) -> bool {
+        self.version_info.as_ref().is_some_and(|v| v.version == semver::Version::new(major, minor, patch))
+    }
+    pub fn is_ge_version(&self, major: u64, minor: u64, patch: u64) -> bool {
+        self.version_info.as_ref().is_some_and(|v| v.version >= semver::Version::new(major, minor, patch))
     }
 
     pub fn parse_existing_enode(&mut self, id: &str) -> Option<ENodeIdx> {
         let idx = self.terms.parse_existing_id(&mut self.strings, id)?;
         let enode = self.egraph.get_enode(idx, &self.stack);
-        if self.is_version(semver::Version::new(4, 12, 2)) && enode.is_none() {
+        if self.is_version(4, 12, 2) && enode.is_none() {
             // Very rarely in version 4.12.2, an `[attach-enode]` is not emitted. Create it here.
             // TODO: log somewhere when this happens.
             self.egraph.new_enode(None, idx, None, &self.stack);
@@ -293,8 +296,7 @@ impl Z3LogParser for Z3Parser {
     fn attach_enode<'a>(&mut self, mut l: impl Iterator<Item = &'a str>) -> Option<()> {
         let idx = self.terms.parse_existing_id(&mut self.strings, l.next()?);
         let Some(idx) = idx else {
-            const Z3_4_8_7: semver::Version = semver::Version::new(4, 8, 7);
-            if self.is_version(Z3_4_8_7) {
+            if self.is_version(4, 8, 7) {
                 // Z3 4.8.7 seems to have a bug where it can emit a non-existent term id here.
                 return Some(());
             } else {
@@ -404,7 +406,10 @@ impl Z3LogParser for Z3Parser {
                 let second_term = l.next()?.strip_suffix(')')?;
                 let from = self.parse_existing_enode(first_term)?;
                 let to = self.parse_existing_enode(second_term)?;
-                self.egraph.blame_equalities(from, to, &self.stack, &mut blamed);
+                // See comment in `EGraph::get_equalities`
+                let can_mismatch = || self.is_ge_version(4, 12, 3) &&
+                    self.terms[self.egraph.get_owner(to)].kind.app_name().is_some_and(|app| &self.strings[app] == "if");
+                self.egraph.blame_equalities(from, to, &self.stack, &mut blamed, can_mismatch)?;
             } else {
                 let term = self.parse_existing_enode(word)?;
                 blamed.push(BlameKind::Term { term })

smt-log-parser/tests/parse_logs.rs

@@ -14,8 +14,8 @@ fn parse_all_logs() {
             let (metadata, mut parser) = Z3Parser::from_file(&filename).unwrap();
             let file_size = metadata.len();
 
-            // Gives 50 millis per MB (or 50 secs per GB)
-            let timeout = Duration::from_millis(500 + (file_size / 20_000));
+            // Gives 100 millis per MB (or 100 secs per GB)
+            let timeout = Duration::from_millis(500 + (file_size / 10_000));
             println!(
                 "Parsing {} ({} MB) with timeout of {timeout:?}",
                 filename.display(),