Properly fix #63

axiom-profiler-GUI/src/screen/graphviz.rs

@@ -169,7 +169,7 @@ impl
         use NodeKind::*;
         fn get_name(parser: &Z3Parser, tidx: TermIdx) -> String {
             let owner = &parser[tidx];
-            let name = owner.kind.app_name();
+            let name = owner.app_name();
             let name = name.map(|n| &parser[n]).unwrap_or_default();
             if owner.child_ids.is_empty() {
                 name.to_string()

axiom-profiler-GUI/src/screen/inst_graph/display/node_info.rs

@@ -136,9 +136,10 @@ impl<'a, 'b> NodeInfo<'a, 'b> {
                 let pattern = pattern
                     .with_data(self.ctxt, &mut Some(qpat.quant))
                     .to_string();
-                let enode = matched.enode().with(self.ctxt).to_string();
+                let enode = matched.enode.with(self.ctxt).to_string();
                 let equalities = matched
-                    .equalities()
+                    .equalities
+                    .iter()
                     .map(|eq| eq.with(self.ctxt).to_string())
                     .collect();
                 (pattern, enode, equalities)

axiom-profiler-GUI/src/screen/inst_graph/search.rs

@@ -61,7 +61,7 @@ impl Graph {
             // TODO: display meaning in search?
             if let Some(_meaning) = parser.meaning(tidx) {}
             let term = &parser[tidx];
-            let Some(name) = term.kind.app_name() else {
+            let Some(name) = term.app_name() else {
                 if EXPECT_APP {
                     log::error!("ENode without name: {:?}", term);
                 }
@@ -99,8 +99,8 @@ impl Graph {
                         handle_enode(yt);
                     }
                     for blame in match_.pattern_matches() {
-                        handle_enode(blame.enode());
-                        for eq in blame.equalities() {
+                        handle_enode(blame.enode);
+                        for &eq in blame.equalities.iter() {
                             handle_eq(parser, eq, &mut handle_enode);
                         }
                     }

smt-log-parser/src/analysis/dependencies.rs

@@ -78,12 +78,12 @@ impl QuantifierAnalysis {
                 }
                 let direct_dep = &mut qinfo.direct_deps[i];
 
-                let created_by = parser[blame.enode()].blame.inst();
+                let created_by = parser[blame.enode].blame.inst();
                 let created_by =
                     created_by.and_then(|iidx| parser.get_inst(iidx).match_.kind.quant_idx());
                 *direct_dep.enode.entry(created_by).or_default() += 1;
 
-                for eq in blame.equalities() {
+                for &eq in blame.equalities.iter() {
                     let eq_parents = inst_graph.raw[eq].parents.insts.iter().copied();
                     let eq_parents =
                         eq_parents.filter_map(|iidx| parser.get_inst(iidx).match_.kind.quant_idx());

smt-log-parser/src/analysis/generalise.rs

@@ -27,7 +27,7 @@ impl SynthTerms {
         let larger_meaning = table.meaning(larger);
         if smaller_meaning.is_none()
             && larger_meaning.is_none()
-            && smaller_term.kind == larger_term.kind
+            && smaller_term.kind() == larger_term.kind()
             && smaller_term.child_ids.len() == larger_term.child_ids.len()
         {
             // TODO: remove this depth restriction
@@ -43,7 +43,7 @@ impl SynthTerms {
             else {
                 return Ok(None);
             };
-            self.new_synthetic(smaller_term.kind, child_ids).map(Some)
+            self.new_synthetic(smaller_term.kind(), child_ids).map(Some)
         } else {
             // If the meanings are some and equal, then the TermIdx should've
             // been equal?
@@ -128,7 +128,7 @@ impl SynthTerms {
             })
             .collect::<Result<_>>()?;
         let replaced = if found_smaller {
-            self.new_synthetic(larger_term.kind, child_ids)?
+            self.new_synthetic(larger_term.kind(), child_ids)?
         } else {
             larger.into()
         };
@@ -156,7 +156,7 @@ impl SynthTerms {
                     let larger_meaning = table.meaning(larger);
                     if !(smaller_meaning.is_none()
                         && larger_meaning.is_none()
-                        && threeway_eq(term_kind, &smaller_term.kind, &larger_term.kind)
+                        && threeway_eq(term_kind, &smaller_term.kind(), &larger_term.kind())
                         && threeway_eq(
                             gen_term.child_ids().len(),
                             smaller_term.child_ids.len(),

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

@@ -275,12 +275,13 @@ pub struct CollectedBlame {
 }
 
 impl CollectedBlame {
-    pub fn new(parser: &Z3Parser, blame: Blame<'_>) -> Self {
-        let enode = blame.enode();
+    pub fn new(parser: &Z3Parser, blame: &Blame) -> Self {
+        let enode = blame.enode;
         let owner = parser[enode].owner;
         let equalities = blame
-            .equalities()
-            .map(|eidx| {
+            .equalities
+            .iter()
+            .map(|&eidx| {
                 let (from, to) = parser.from_to(eidx);
                 let from = parser[from].owner;
                 let to = parser[to].owner;

smt-log-parser/src/analysis/graph/analysis/matching_loop/explain.rs

@@ -3,7 +3,7 @@ use petgraph::graph::NodeIndex;
 use crate::{
     analysis::analysis::matching_loop::{RecurrenceKind, SimpIdx},
     items::{
-        ENodeIdx, EqGivenUse, EqTransIdx, EqualityExpl, InstIdx, Term, TermIdx, TermKind,
+        ENodeIdx, EqGivenUse, EqTransIdx, EqualityExpl, InstIdx, TermIdx, TermKind,
         TransitiveExplSegmentKind,
     },
     parsers::z3::{
@@ -574,7 +574,7 @@ impl<'a> QVarParentCollector<'a> {
     }
     fn collect_term(&mut self, tidx: TermIdx) -> bool {
         let term = &self.parser[tidx];
-        match term.kind {
+        match term.kind() {
             TermKind::Var(_) => {
                 self.terms_with_qvars.insert(tidx);
                 true
@@ -653,43 +653,37 @@ impl TermSimplifier<'_> {
         }
 
         let must_pop = &mut false;
-        match term {
-            AnyTerm::Parsed(Term {
-                kind: TermKind::App(name),
-                ..
-            }) if {
-                self.stack.push(*name);
+        if let AnyTerm::Parsed(term) = term {
+            if let Some(name) = term.app_name() {
+                self.stack.push(name);
                 *must_pop = true;
                 let is_forbidden = self.forbidden_apps.contains(self.stack.as_slice());
-                !is_forbidden && !has_qvars
-            } =>
-            {
-                self.stack.pop();
-
-                let next = self.simplifications.len();
-                let new = self.parser.synth_terms.new_variable(next as u32)?;
-                let old = self.simplifications.insert(tidx.unwrap(), new);
-                // Should have returned early above if it was already contained.
-                assert!(old.is_none());
-                Ok(new)
-            }
-            _ => {
-                let mut child_ids = Vec::<SynthIdx>::new();
-                child_ids.try_reserve_exact(term.child_ids().len())?;
-                for i in 0..term.child_ids().len() {
-                    let child = self.parser[idx].child_ids()[i];
-                    let new = self.simplify_term(child)?;
-                    child_ids.push(new);
-                }
-                if *must_pop {
+                if !is_forbidden && !has_qvars {
                     self.stack.pop();
+
+                    let next = self.simplifications.len();
+                    let new = self.parser.synth_terms.new_variable(next as u32)?;
+                    let old = self.simplifications.insert(tidx.unwrap(), new);
+                    // Should have returned early above if it was already contained.
+                    assert!(old.is_none());
+                    return Ok(new);
                 }
-                let term = self.parser[idx].replace_child_ids(child_ids.into());
-                let term = term
-                    .map(|term| self.parser.synth_terms.insert(term))
-                    .transpose()?;
-                Ok(term.unwrap_or(idx))
             }
         }
+        let mut child_ids = Vec::<SynthIdx>::new();
+        child_ids.try_reserve_exact(term.child_ids().len())?;
+        for i in 0..term.child_ids().len() {
+            let child = self.parser[idx].child_ids()[i];
+            let new = self.simplify_term(child)?;
+            child_ids.push(new);
+        }
+        if *must_pop {
+            self.stack.pop();
+        }
+        let term = self.parser[idx].replace_child_ids(child_ids.into());
+        let term = term
+            .map(|term| self.parser.synth_terms.insert(term))
+            .transpose()?;
+        Ok(term.unwrap_or(idx))
     }
 }

smt-log-parser/src/analysis/graph/analysis/matching_loop/signature.rs

@@ -49,8 +49,8 @@ impl MlSignature {
         let parents: Box<[_]> = match_
             .pattern_matches()
             .map(|blame| {
-                let eq_len = blame.equalities().count();
-                let blame = blame.enode();
+                let eq_len = blame.equalities.len();
+                let blame = blame.enode;
                 let eblame = &parser[blame];
                 let Some(created_by) = eblame.blame.inst() else {
                     return (InstParent::Const(blame), eq_len);

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

@@ -110,10 +110,10 @@ impl RawInstGraph {
                 .enumerate()
             {
                 let pattern_term = i as u16;
-                self_.add_edge(blame.enode(), idx, EdgeKind::Blame { pattern_term });
-                for (i, eq) in blame.equalities().enumerate() {
+                self_.add_edge(blame.enode, idx, EdgeKind::Blame { pattern_term });
+                for (i, eq) in blame.equalities.iter().enumerate() {
                     self_.add_edge(
-                        eq,
+                        *eq,
                         idx,
                         EdgeKind::BlameEq {
                             pattern_term,

smt-log-parser/src/analysis/redundancy.rs

@@ -38,7 +38,7 @@ impl<'a> RedundancyAnalysis<'a> {
 #[derive(Debug, Default)]
 pub struct QuantRedundancy<'a> {
     pub duplicates: FxHashMap<Box<[Result<ENodeIdx, TermIdx>]>, Vec<InstIdx>>,
-    pub sub_duplicates: FxHashMap<Blame<'a>, u32>,
+    pub sub_duplicates: FxHashMap<&'a Blame, u32>,
 }
 
 impl<'a> QuantRedundancy<'a> {

smt-log-parser/src/bin/smt-scope/cmd/test.rs

@@ -49,8 +49,9 @@ fn run_file(path: PathBuf, timeout: f32, memory: bool) {
         #[cfg(feature = "mem_dbg")]
         result.mem_dbg(DbgFlags::default()).ok();
     }
+    let errors = result.errors();
     println!(
-        "[Parsing] {} after {} seconds (timeout {timeout:?})",
+        "[Parsing] {} after {} seconds (timeout {timeout:?}){errors}",
         if timeout.is_timeout() {
             "Timeout"
         } else {

smt-log-parser/src/display_with.rs

@@ -999,7 +999,7 @@ impl<'a> DisplayWithCtxt<DisplayCtxt<'a>, ()> for &'a EventKind {
         match *self {
             EventKind::NewConst(term_idx) => {
                 let term = &ctxt.parser[term_idx];
-                let name = &ctxt.parser[term.kind.app_name().unwrap()];
+                let name = &ctxt.parser[term.app_name().unwrap()];
                 if term.child_ids.is_empty() {
                     write!(f, "(declare-const {name} ?)")
                 } else {

smt-log-parser/src/error.rs

@@ -5,7 +5,7 @@ use lasso::LassoError;
 #[cfg(feature = "mem_dbg")]
 use mem_dbg::{MemDbg, MemSize};
 
-use crate::items::{BlameKind, ENodeIdx, Fingerprint, QuantIdx, TermId, TermIdx};
+use crate::items::{Blame, ENodeIdx, Fingerprint, QuantIdx, TermId, TermIdx};
 
 pub type Result<T> = std::result::Result<T, Error>;
 pub type FResult<T> = std::result::Result<T, FatalError>;
@@ -58,15 +58,15 @@ pub enum Error {
     NewMatchOnLambda(QuantIdx),
     UnknownPatternIdx(TermIdx),
     SubpatTooFewBlame(usize),
-    // Z3 BUG: https://github.com/viperproject/axiom-profiler-2/issues/63
-    SubpatUnknownBlame(String),
+    // Z3 ISSUE: https://github.com/viperproject/axiom-profiler-2/issues/63
+    SubpatNoBlame(Vec<TermIdx>),
 
     // Inst discovered
     /// theory-solving non-rewrite axiom should blame valid enodes
     NonRewriteAxiomInvalidEnode(TermIdx),
     /// theory-solving rewrite axiom should only have one term
     RewriteAxiomMultipleTerms1(TermIdx),
-    RewriteAxiomMultipleTerms2(Vec<BlameKind>),
+    RewriteAxiomMultipleTerms2(Vec<Blame>),
     UnknownInstMethod(String),
 
     // Instance
@@ -89,9 +89,6 @@ pub enum Error {
     PopConflictMismatch,
     InvalidFrameInteger(ParseIntError),
 
-    // Proof
-    ProvedVar(TermIdx),
-
     // CDCL
     NoConflict,
     BoolLiteral,
@@ -100,9 +97,6 @@ pub enum Error {
     UnknownJustification(String),
     MissingColonJustification,
 
-    // File IO
-    FileRead(std::io::Error),
-
     Allocation(TryReserveError),
     Lasso(LassoError),