Add enode blame asserted

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

@@ -180,8 +180,8 @@ impl
         match *self {
             Instantiation(inst) => match &parser[parser[inst].match_].kind {
                 MatchKind::TheorySolving { axiom_id, .. } => {
-                    let namespace = &parser[axiom_id.namespace];
-                    let id = axiom_id.id.map(|id| format!("[{id}]")).unwrap_or_default();
+                    let (namespace, id) = axiom_id.to_string_components(&parser.strings);
+                    let id = id.map(|id| format!("[{id}]")).unwrap_or_default();
                     format!("{namespace}{id}")
                 }
                 MatchKind::MBQI { quant, .. }

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

@@ -232,7 +232,7 @@ impl<'a, 'b> NodeInfo<'a, 'b> {
             .node
             .kind()
             .inst()
-            .and_then(|i| self.ctxt.parser[i].z3_generation)
+            .and_then(|i| self.ctxt.parser[i].kind.z3_generation())
         {
             extra_info.push(("z3 gen", z3gen.to_string()));
         }

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

@@ -65,7 +65,7 @@ impl QuantifierAnalysis {
                 }
                 let direct_dep = &mut qinfo.direct_deps[i];
 
-                let created_by = parser[blame.enode()].created_by;
+                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;

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

@@ -334,7 +334,7 @@ impl MlExplainer {
 
     fn add_enode(&mut self, parser: &Z3Parser, enode: ENodeIdx, result_enode: NodeIndex) -> bool {
         let enode_data = &parser[enode];
-        let created_by = enode_data.created_by;
+        let created_by = enode_data.blame.inst();
         let created_by = created_by.and_then(|cb| self.instantiations.get(&cb));
         if let Some(created_by) = created_by {
             self.graph
@@ -375,7 +375,7 @@ impl MlExplainer {
                 let eq_expl = &self.equalities().given[eq];
                 match eq_expl {
                     &EqualityExpl::Literal { eq, .. } => {
-                        let created_by = self.parser[eq].created_by;
+                        let created_by = self.parser[eq].blame.inst();
                         let created_by =
                             created_by.and_then(|iidx| self.explainer.instantiations.get(&iidx));
                         if let Some(created_by) = created_by {

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

@@ -52,7 +52,7 @@ impl MlSignature {
                 let eq_len = blame.equalities().count();
                 let blame = blame.enode();
                 let eblame = &parser[blame];
-                let Some(created_by) = eblame.created_by else {
+                let Some(created_by) = eblame.blame.inst() else {
                     return (InstParent::Const(blame), eq_len);
                 };
                 match parser[parser[created_by].match_].kind.quant_idx() {

smt-log-parser/src/display_with.rs

@@ -486,10 +486,8 @@ impl DisplayWithCtxt<DisplayCtxt<'_>, ()> for &MatchKind {
                 quant.fmt_with(f, ctxt, data)
             }
             MatchKind::TheorySolving { axiom_id, .. } => {
-                write!(f, "[TheorySolving] {}#", &ctxt.parser[axiom_id.namespace])?;
-                if let Some(id) = axiom_id.id {
-                    write!(f, "{id}")?;
-                }
+                write!(f, "[TheorySolving] ")?;
+                axiom_id.fmt_with(f, ctxt, data)?;
                 Ok(())
             }
             MatchKind::Axiom { axiom, .. } => {
@@ -617,9 +615,13 @@ impl<'a: 'b, 'b> DisplayWithCtxt<DisplayCtxt<'b>, ()> for &'a TermId {
         ctxt: &DisplayCtxt<'b>,
         _data: &mut (),
     ) -> fmt::Result {
-        let namespace = &ctxt.parser[self.namespace];
-        let id = self.id.map(|id| id.to_string()).unwrap_or_default();
-        write!(f, "{namespace}#{id}")
+        let (namespace, id) = self.to_string_components(&ctxt.parser.strings);
+        write!(f, "{namespace}#")?;
+        if let Some(id) = id {
+            write!(f, "{id}")
+        } else {
+            Ok(())
+        }
     }
 }
 

smt-log-parser/src/error.rs

@@ -37,7 +37,7 @@ pub enum Error {
     InvalidVersion(semver::Error),
 
     // Id parsing
-    InvalidIdNumber(ParseIntError),
+    InvalidIdNumber(nonmax::ParseIntError),
     InvalidIdHash(String),
     UnknownId(TermId),
 
@@ -85,6 +85,9 @@ pub enum Error {
     PopConflictMismatch,
     InvalidFrameInteger(ParseIntError),
 
+    // Proof
+    ProvedVar(TermIdx),
+
     // CDCL
     NoConflict,
     BoolLiteral,

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

@@ -3,22 +3,44 @@ use mem_dbg::{MemDbg, MemSize};
 
 use crate::{FxHashMap, NonMaxU32};
 
-use super::{ENodeIdx, EqGivenIdx, EqTransIdx, InstIdx, StackIdx, TermIdx};
+use super::{ENodeIdx, EqGivenIdx, EqTransIdx, InstIdx, ProofIdx, StackIdx, TermIdx};
 
 #[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
 #[derive(Debug)]
 pub struct ENode {
     pub frame: StackIdx,
-    pub created_by: Option<InstIdx>,
+    pub blame: ENodeBlame,
     pub owner: TermIdx,
-    pub z3_generation: Option<NonMaxU32>,
+    pub z3_generation: NonMaxU32,
 
     pub(crate) equalities: Vec<Equality>,
     /// This will never contain a `TransitiveExpl::to` pointing to itself. It
     /// may contain `TransitiveExpl::given_len` of 0, but only when
     /// `get_simple_path` fails but `can_mismatch` is true.
     pub(crate) transitive: FxHashMap<ENodeIdx, EqTransIdx>,
-    pub(crate) self_transitive: Option<EqTransIdx>,
+}
+
+#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
+#[cfg_attr(feature = "mem_dbg", copy_type)]
+#[derive(Debug, Clone, Copy)]
+pub enum ENodeBlame {
+    /// The `ENode` was created by an instantiation.
+    Inst(InstIdx),
+    /// The `ENode` was created by a proof step.
+    Proof(ProofIdx),
+    /// The `ENode` represents either `#1` or `#2`.
+    BoolConst,
+    /// We don't know why the `ENode` was created.
+    Unknown,
+}
+
+impl ENodeBlame {
+    pub fn inst(self) -> Option<InstIdx> {
+        match self {
+            Self::Inst(inst) => Some(inst),
+            _ => None,
+        }
+    }
 }
 
 #[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]

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

@@ -215,16 +215,43 @@ impl fmt::Display for Fingerprint {
 #[derive(Debug, Clone)]
 pub struct Instantiation {
     pub match_: MatchIdx,
-    pub fingerprint: Fingerprint,
+    pub kind: InstantiationKind,
     pub proof_id: InstProofLink,
-    pub z3_generation: Option<NonMaxU32>,
     /// The enodes that were yielded by the instantiation along with the
     /// generalised terms for them (`MaybeSynthIdx::Parsed` if the yielded term
     /// doesn't contain any quantified variables)
     pub yields_terms: BoxSlice<ENodeIdx>,
     pub frame: StackIdx,
 }
 
+#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
+#[cfg_attr(feature = "mem_dbg", copy_type)]
+#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
+#[derive(Debug, Clone, Copy)]
+pub enum InstantiationKind {
+    Axiom,
+    NonAxiom {
+        fingerprint: Fingerprint,
+        z3_generation: NonMaxU32,
+    },
+}
+
+impl InstantiationKind {
+    pub fn fingerprint(&self) -> Fingerprint {
+        match self {
+            Self::NonAxiom { fingerprint, .. } => *fingerprint,
+            _ => Fingerprint(0),
+        }
+    }
+
+    pub fn z3_generation(&self) -> Option<NonMaxU32> {
+        match self {
+            Self::NonAxiom { z3_generation, .. } => Some(*z3_generation),
+            _ => None,
+        }
+    }
+}
+
 /// A Z3 instantiation.
 #[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
 #[cfg_attr(feature = "mem_dbg", copy_type)]

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

@@ -58,7 +58,7 @@ impl TermKind {
 #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 #[derive(Debug, Clone, Copy, Default, Hash, PartialEq, Eq)]
 pub struct TermId {
-    pub namespace: IString,
+    pub namespace: Option<IString>,
     pub id: Option<NonMaxU32>,
 }
 impl TermId {
@@ -68,21 +68,29 @@ 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 = IString(strings.get_or_intern(&value[..hash_idx]));
+        let namespace = (hash_idx != 0).then(|| IString(strings.get_or_intern(&value[..hash_idx])));
         let id = &value[hash_idx + 1..];
         let id = match id {
             "" => None,
-            id => Some(NonMaxU32::new(id.parse::<u32>().map_err(Error::InvalidIdNumber)?).unwrap()),
+            id => Some(id.parse::<NonMaxU32>().map_err(Error::InvalidIdNumber)?),
         };
         Ok(Self { namespace, id })
     }
     pub fn order(&self) -> u32 {
         self.id.map(|id| id.get() + 1).unwrap_or_default()
     }
+
+    pub fn to_string_components<'a>(
+        &self,
+        strings: &'a StringTable,
+    ) -> (&'a str, Option<NonMaxU32>) {
+        let namespace = self.namespace.map(|ns| &strings[*ns]).unwrap_or_default();
+        (namespace, self.id)
+    }
     pub fn to_string(&self, strings: &StringTable) -> String {
-        let namespace = &strings[*self.namespace];
-        let id = self.id.map(|id| id.to_string()).unwrap_or_default();
-        format!("{}#{}", namespace, id)
+        let (namespace, id) = self.to_string_components(strings);
+        let id = id.map(|id| id.to_string()).unwrap_or_default();
+        format!("{namespace}#{id}")
     }
 }
 
@@ -93,25 +101,27 @@ impl TermId {
 #[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
 #[derive(Debug)]
 pub struct TermIdToIdxMap<K: Copy> {
-    empty_string: IString,
     empty_namespace: Vec<Option<K>>,
     namespace_map: FxHashMap<IString, Vec<Option<K>>>,
 }
-impl<K: Copy> TermIdToIdxMap<K> {
-    pub fn new(strings: &mut StringTable) -> Self {
+
+impl<K: Copy> Default for TermIdToIdxMap<K> {
+    fn default() -> Self {
         Self {
-            empty_string: IString(strings.get_or_intern_static("")),
             empty_namespace: Vec::new(),
             namespace_map: FxHashMap::default(),
         }
     }
-    fn get_vec_mut(&mut self, namespace: IString) -> Result<&mut Vec<Option<K>>> {
-        if self.empty_string == namespace {
-            // Special handling of common case for empty namespace
-            Ok(&mut self.empty_namespace)
-        } else {
+}
+
+impl<K: Copy> TermIdToIdxMap<K> {
+    fn get_vec_mut(&mut self, namespace: Option<IString>) -> Result<&mut Vec<Option<K>>> {
+        if let Some(namespace) = namespace {
             self.namespace_map.try_reserve(1)?;
             Ok(self.namespace_map.entry(namespace).or_default())
+        } else {
+            // Special handling of common case for empty namespace
+            Ok(&mut self.empty_namespace)
         }
     }
     pub fn register_term(&mut self, id: TermId, idx: K) -> Result<()> {
@@ -128,11 +138,11 @@ impl<K: Copy> TermIdToIdxMap<K> {
         vec[id_idx].replace(idx);
         Ok(())
     }
-    fn get_vec(&self, namespace: IString) -> Option<&Vec<Option<K>>> {
-        if self.empty_string == namespace {
-            Some(&self.empty_namespace)
-        } else {
+    fn get_vec(&self, namespace: Option<IString>) -> Option<&Vec<Option<K>>> {
+        if let Some(namespace) = namespace {
             self.namespace_map.get(&namespace)
+        } else {
+            Some(&self.empty_namespace)
         }
     }
     pub fn get_term(&self, id: &TermId) -> Option<K> {