Properly fix issue #63 (#103)

smt-log-parser/src/analysis/graph/analysis/mod.rs

@@ -101,15 +101,15 @@ impl Analysis {
 }
 
 impl InstGraph {
-    pub fn initialise_first(&mut self, parser: &Z3Parser) {
+    pub fn initialise_first(&mut self, parser: &Z3Parser, n: usize) {
         self.initialise_collect(ProofInitialiser::<false>, parser);
         self.initialise_collect(ProofInitialiser::<true>, parser);
         self.initialise_cdcl(parser);
 
-        self.initialise_default(parser);
+        self.initialise_default(parser, n);
     }
 
-    pub fn initialise_default(&mut self, parser: &Z3Parser) {
+    pub fn initialise_default(&mut self, parser: &Z3Parser, n: usize) {
         let mut reach = BwdReachableAnalysis::<ReachNonDisabled>::default();
         self.analysis.reach = self.topo_analysis(&mut reach);
 
@@ -121,16 +121,16 @@ impl InstGraph {
         self.initialise_transfer(NextInstsInit::<true>, parser);
         self.initialise_transfer(NextInstsInit::<false>, parser);
 
-        self.analyse();
+        self.analyse(n);
     }
 
-    pub fn analyse(&mut self) {
+    pub fn analyse(&mut self, n: usize) {
         self.analysis.cost.sorted_to = 0;
         self.analysis.children.sorted_to = 0;
         self.analysis.fwd_depth_min.sorted_to = 0;
-        self.analysis.first_n_cost(&self.raw, 10000);
-        self.analysis.first_n_children(&self.raw, 10000);
-        self.analysis.first_n_fwd_depth_min(&self.raw, 10000);
+        self.analysis.first_n_cost(&self.raw, n);
+        self.analysis.first_n_children(&self.raw, n);
+        self.analysis.first_n_fwd_depth_min(&self.raw, n);
     }
 }
 

smt-log-parser/src/analysis/graph/disable.rs

@@ -16,7 +16,7 @@ impl InstGraph {
     ) {
         let (_, disabled_changed) = self.raw.reset_disabled_to_raw(f);
         if disabled_changed {
-            self.initialise_default(parser);
+            self.initialise_default(parser, super::DEFAULT_N);
         }
     }
 

smt-log-parser/src/analysis/graph/mod.rs

@@ -16,6 +16,8 @@ pub mod visible;
 pub use raw::{RawEdgeIndex, RawNodeIndex};
 pub use visible::{VisibleEdgeIndex, VisibleNodeIndex};
 
+const DEFAULT_N: usize = 10000;
+
 #[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
 #[derive(Debug)]
 pub struct InstGraph {
@@ -26,6 +28,13 @@ pub struct InstGraph {
 
 impl InstGraph {
     pub fn new(parser: &Z3Parser) -> Result<Self> {
+        Self::new_with_analysis(parser, DEFAULT_N)
+    }
+    pub fn new_lite(parser: &Z3Parser) -> Result<Self> {
+        Self::new_with_analysis(parser, 0)
+    }
+
+    fn new_with_analysis(parser: &Z3Parser, n: usize) -> Result<Self> {
         let mut raw = RawInstGraph::new(parser)?;
         let subgraphs = raw.partition()?;
         let analysis = Analysis::new(subgraphs.in_subgraphs())?;
@@ -34,7 +43,7 @@ impl InstGraph {
             subgraphs,
             analysis,
         };
-        self_.initialise_first(parser);
+        self_.initialise_first(parser, n);
         Ok(self_)
     }
 

smt-log-parser/src/error.rs

@@ -56,8 +56,9 @@ pub enum Error {
     InvalidQVarInteger(ParseIntError),
     NewMatchOnLambda(QuantIdx),
     UnknownPatternIdx(TermIdx),
-    SubpatTooManyBlame(TermId),
     SubpatTooFewBlame(usize),
+    // Z3 BUG: https://github.com/viperproject/axiom-profiler-2/issues/63
+    SubpatUnknownBlame(String),
 
     // Inst discovered
     /// theory-solving non-rewrite axiom should blame valid enodes

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

@@ -32,6 +32,7 @@ impl Match {
             .flat_map(|(idx, blame)| matches!(blame, BlameKind::Term { .. }).then(|| idx))
             .chain([self.blamed.len()]);
         let mut last = terms.next().unwrap_or_default();
+        debug_assert_eq!(last, 0);
         terms.map(move |idx| {
             let slice = &self.blamed[last..idx];
             last = idx;
@@ -136,10 +137,9 @@ impl MatchKind {
 #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
 pub enum BlameKind {
     Term { term: ENodeIdx },
-    // See https://github.com/viperproject/axiom-profiler-2/issues/63
-    // sometimes we need to ignore a blamed term.
-    IgnoredTerm { term: ENodeIdx },
     Equality { eq: EqTransIdx },
+    // Z3 BUG: https://github.com/viperproject/axiom-profiler-2/issues/63
+    TermBug { term: ENodeIdx },
 }
 impl BlameKind {
     pub(crate) fn term(&self) -> Option<&ENodeIdx> {
@@ -151,7 +151,7 @@ impl BlameKind {
     pub(crate) fn equality(&self) -> Option<core::result::Result<&EqTransIdx, &ENodeIdx>> {
         match self {
             Self::Equality { eq } => Some(Ok(eq)),
-            Self::IgnoredTerm { term } => Some(Err(term)),
+            Self::TermBug { term } => Some(Err(term)),
             _ => None,
         }
     }

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

@@ -0,0 +1,185 @@
+#[cfg(feature = "mem_dbg")]
+use mem_dbg::{MemDbg, MemSize};
+
+use crate::{
+    items::{BlameKind, ENodeIdx, Term, TermId, TermIdx},
+    Error as E, FxHashSet, IString, Result, StringTable,
+};
+
+use super::{terms::Terms, Z3Parser};
+
+// Z3 BUG: https://github.com/viperproject/axiom-profiler-2/issues/63
+
+impl Z3Parser {
+    pub(super) fn can_blame_match_subpat(&self, blame: ENodeIdx, subpat: TermIdx) -> bool {
+        self[self[blame].owner].kind == self[subpat].kind
+    }
+
+    /// Fixes the blame vector which may be incorrect due the Z3 BUG.
+    pub(super) fn fix_blamed(&self, blamed: &mut [BlameKind], pattern: &Term) -> Result<()> {
+        debug_assert!(!pattern.child_ids.is_empty());
+        let mut b_roots = blamed.iter().filter_map(|b| b.term());
+        let mut no_bug = true;
+        for (i, subpat) in pattern.child_ids.iter().enumerate() {
+            let Some(root) = b_roots.next() else {
+                return Err(E::SubpatTooFewBlame(pattern.child_ids.len() - i));
+            };
+            no_bug &= self.can_blame_match_subpat(*root, *subpat);
+        }
+        let too_many = b_roots.next().is_some();
+        if no_bug && !too_many {
+            debug_assert!(blamed[0].term().is_some());
+            return Ok(());
+        }
+        let mut root_count = pattern.child_ids.len() + too_many as usize + b_roots.count();
+        debug_assert!(root_count >= pattern.child_ids.len());
+        self.disable_obvious_blamed_bugs(blamed, pattern, &mut root_count);
+
+        let b = blamed.iter().enumerate();
+        let b_roots: Vec<_> = b
+            .filter_map(|(i, b)| Some(i).zip(b.term().copied()))
+            .collect();
+        debug_assert_eq!(b_roots.len(), root_count);
+
+        let mut valid_rotation = None;
+        let mut skipped = Vec::new();
+        for offset in 0..b_roots.len() {
+            if !self.can_blame_match_subpat(b_roots[offset].1, pattern.child_ids[0]) {
+                continue;
+            }
+            let can_skip = b_roots.len() - pattern.child_ids.len();
+            let idx = |i| b_roots[(offset + i) % b_roots.len()];
+            let mut ok = true;
+            'outer: for (i, &sp) in pattern.child_ids.iter().enumerate().skip(1) {
+                while !self.can_blame_match_subpat(idx(skipped.len() + i).1, sp) {
+                    if skipped.len() == can_skip {
+                        ok = false;
+                        break 'outer;
+                    }
+                    skipped.push(skipped.len() + i);
+                }
+            }
+            if ok {
+                valid_rotation.replace(offset);
+                let mut skip = |i| {
+                    let i = idx(i).0;
+                    let b = &mut blamed[i];
+                    let term = *b.term().unwrap();
+                    *b = BlameKind::TermBug { term };
+                    root_count -= 1;
+                };
+                for &i in &skipped {
+                    skip(i);
+                }
+                for i in 0..(can_skip - skipped.len()) {
+                    skip(skipped.len() + pattern.child_ids.len() + i);
+                }
+                debug_assert_eq!(root_count, pattern.child_ids.len());
+                break;
+                // To error on ambiguous replace the above block with:
+                // let old = valid_rotation.replace(offset);
+                // if let Some(old) = old {
+                //     return Err(E::SubpatAmbiguousBlame(old, offset));
+                // }
+            }
+            skipped.clear();
+        }
+
+        let Some(rotation) = valid_rotation else {
+            let name = |t: TermIdx| &self[self[t].kind.app_name().unwrap()];
+            let blamed = blamed.iter().filter_map(|b| match *b {
+                BlameKind::Term { term } => Some((true, term)),
+                BlameKind::Equality { .. } => None,
+                BlameKind::TermBug { term } => Some((false, term)),
+            });
+            let blamed = blamed.map(|(r, t)| format!("{r} {}", name(self[t].owner)));
+            let pattern = pattern.child_ids.iter().copied();
+            let s = format!(
+                "Blamed: [{}] | Subpats: [{}]",
+                blamed.collect::<Vec<_>>().join(", "),
+                pattern.map(name).collect::<Vec<_>>().join(", "),
+            );
+            return Err(E::SubpatUnknownBlame(s));
+        };
+        let rotation = b_roots[rotation].0;
+        blamed.rotate_left(rotation);
+        debug_assert!(blamed[0].term().is_some());
+        Ok(())
+    }
+
+    fn disable_obvious_blamed_bugs(
+        &self,
+        blamed: &mut [BlameKind],
+        pattern: &Term,
+        root_count: &mut usize,
+    ) {
+        if pattern.child_ids.len() == *root_count {
+            return;
+        }
+        let roots = pattern
+            .child_ids
+            .iter()
+            .map(|&sp| self[sp].kind.app_name().unwrap())
+            .collect::<FxHashSet<_>>();
+        for b in blamed.iter_mut() {
+            let BlameKind::Term { term } = *b else {
+                continue;
+            };
+            let root = self[self[term].owner].kind.app_name().unwrap();
+            if roots.contains(&root) {
+                continue;
+            }
+            *b = BlameKind::TermBug { term };
+            *root_count -= 1;
+        }
+    }
+}
+
+// Z3 BUG: https://github.com/viperproject/axiom-profiler-2/issues/100
+
+#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
+#[derive(Debug, Default)]
+pub(super) struct TermsBug {
+    /// Solve bug by switching to an artificial namespace after a "string" mk_app.
+    get_model: Option<IString>,
+    get_model_idx: u32,
+}
+
+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)?;
+        if let Some(namespace) = self.bug.get_model {
+            debug_assert!(term_id.namespace.is_none());
+            term_id.namespace = Some(namespace);
+        }
+        self.get_app_term_bug(term_id)
+    }
+
+    pub fn check_get_model(&mut self, id: &mut TermId, name: &str, strings: &mut StringTable) {
+        let bug = &mut self.bug;
+        let get_model = bug.get_model.take();
+        if id.namespace.is_some() {
+            return;
+        }
+        // See https://github.com/Z3Prover/z3/blob/z3-4.13.4/src/ast/format.cpp#L45-L52
+        let Some(get_model) = get_model else {
+            // Is a mk_app line with this term the start of a get-model command?
+            if name == "string" {
+                let namespace = format!("get-model-{}", bug.get_model_idx);
+                bug.get_model_idx += 1;
+                bug.get_model = Some(IString(strings.get_or_intern(namespace)));
+                id.namespace = bug.get_model;
+            }
+            return;
+        };
+        match name {
+            "string" | "cr" | "compose" | "indent" | "choice" => {
+                bug.get_model = Some(get_model);
+                id.namespace = Some(get_model);
+            }
+            _ => (),
+        }
+    }
+}

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

@@ -190,12 +190,12 @@ impl EGraph {
         to: ENodeIdx,
         stack: &Stack,
         can_mismatch: impl Fn(&EGraph) -> bool,
-    ) -> Result<Option<EqTransIdx>> {
+    ) -> Result<core::result::Result<EqTransIdx, ENodeIdx>> {
         if from == to {
-            Ok(None)
+            Ok(Err(from))
         } else {
             self.construct_trans_equality(from, to, stack, can_mismatch)
-                .map(Some)
+                .map(Ok)
         }
     }
 
@@ -402,7 +402,7 @@ impl EGraph {
                 let mut use_ = Vec::new();
                 use_.try_reserve_exact(arg_eqs.len())?;
                 for (from, to) in args {
-                    let Some(trans) = self.new_trans_equality(from, to, stack, |_| false)? else {
+                    let Ok(trans) = self.new_trans_equality(from, to, stack, |_| false)? else {
                         continue;
                     };
                     use_.push(trans);

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

@@ -3,6 +3,7 @@ use std::fmt::Debug;
 use super::{LogParser, LogParserHelper};
 use crate::{Error, FResult, Result};
 
+mod bugs;
 pub mod egraph;
 pub mod inst;
 pub mod inter_line;