Clean up opt code

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

@@ -51,18 +51,13 @@ impl Terms {
                 // if meanings or kinds don't match up, need to generalize
                 let (_, _, children) = stack.last_mut()?;
                 let meaning = self.try_find_meaning(strings, &next);
-                let tidx = self.new_synthetic_term(
-                    TermKind::Generalised,
-                    next.into_boxed_slice(),
-                    meaning,
-                );
+                let tidx = self.new_synthetic_term(TermKind::Generalised, next.into(), meaning);
                 children.push(tidx);
             }
 
             let (mut deref, mut meaning, mut children) = stack.pop().unwrap();
             while deref[0].child_ids.len() == children.len() {
-                let tidx =
-                    self.new_synthetic_term(deref[0].kind, children.into_boxed_slice(), meaning);
+                let tidx = self.new_synthetic_term(deref[0].kind, children.into(), meaning);
                 let Some((new_deref, new_meaning, new_children)) = stack.pop() else {
                     return Some(tidx);
                 };
@@ -81,9 +76,11 @@ impl Terms {
             }
             TermKind::Generalised => pattern,
             _ => {
-                let children = Vec::from(self[pattern].child_ids.clone())
-                    .into_iter()
-                    .map(|c| self.generalise_pattern(_strings, c))
+                let children = self[pattern]
+                    .child_ids
+                    .clone()
+                    .iter()
+                    .map(|&c| self.generalise_pattern(_strings, c))
                     .collect();
                 self.new_synthetic_term(
                     self[pattern].kind,

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

@@ -8,7 +8,7 @@ use super::{ENodeIdx, EqGivenIdx, EqTransIdx, InstIdx, StackIdx, TermIdx};
 #[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
 #[derive(Debug)]
 pub struct ENode {
-    pub frame: StackIdx,
+    pub frame: Option<StackIdx>,
     pub created_by: Option<InstIdx>,
     pub owner: TermIdx,
     pub z3_generation: Option<NonMaxU32>,
@@ -24,7 +24,7 @@ pub struct ENode {
 #[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
 #[derive(Debug)]
 pub struct Equality {
-    pub(crate) _frame: StackIdx,
+    pub(crate) _frame: Option<StackIdx>,
     pub to: ENodeIdx,
     pub expl: EqGivenIdx,
 }

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

@@ -1,29 +1,11 @@
 #[cfg(feature = "mem_dbg")]
 use mem_dbg::{MemDbg, MemSize};
 
-use crate::{BoxSlice, Error, NonMaxU32, Result};
+use crate::{error::Either, BoxSlice, Error, NonMaxU32, Result};
 use std::fmt;
 use std::ops::Index;
 
-use super::{ENodeIdx, EqTransIdx, MatchIdx, QuantIdx, TermId, TermIdx};
-
-/// A Z3 instantiation.
-#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
-#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
-#[derive(Debug, Clone)]
-pub struct Instantiation {
-    pub match_: MatchIdx,
-    pub fingerprint: Fingerprint,
-    pub proof_id: Option<Either<TermIdx, TermId>>,
-    pub z3_generation: Option<u32>,
-    pub yields_terms: Box<[ENodeIdx]>,
-}
-
-impl Instantiation {
-    pub fn get_resulting_term(&self) -> Option<TermIdx> {
-        self.proof_id.as_ref()?.as_result().ok().copied()
-    }
-}
+use super::{ENodeIdx, EqTransIdx, MatchIdx, QuantIdx, StackIdx, TermId, TermIdx};
 
 #[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
 #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
@@ -209,31 +191,17 @@ impl fmt::Display for Fingerprint {
 pub struct Instantiation {
     pub match_: MatchIdx,
     pub fingerprint: Fingerprint,
-    pub proof_id: InstProofLink,
+    pub proof_id: Option<Either<TermIdx, TermId>>,
     pub z3_generation: Option<NonMaxU32>,
-    pub frame: StackIdx,
+    pub frame: Option<StackIdx>,
     /// 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>,
 }
 
-/// A Z3 instantiation.
-#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
-#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
-#[derive(Debug, Clone, Copy)]
-pub enum InstProofLink {
-    /// Axiom instantiations (i.e. those with `.fingerprint.is_zero()`) point to
-    /// a term regardless of whether proofs are enabled. These terms seem to
-    /// generally be an equality.
-    IsAxiom(TermIdx),
-    /// When proofs are enabled (i.e. if z3 was run with `proof=true`) non-axiom
-    /// instantiations will include a pointer to the instantiation proof step.
-    HasProof(ProofIdx),
-    /// When proofs are disabled, non-axiom instantiations have no link to the
-    /// fact (i.e. their body) that was instantiated. However, we use a hack to
-    /// try and find the proof term nevertheless: the `[mk-app]` immediately
-    /// preceding the `[instantiation]` line is generally the term we just
-    /// proved.
-    ProofsDisabled(Option<TermIdx>),
+impl Instantiation {
+    pub fn get_resulting_term(&self) -> Option<TermIdx> {
+        self.proof_id.as_ref()?.as_result().ok().copied()
+    }
 }

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

@@ -1,9 +1,11 @@
+mod enode;
 mod equality;
 mod idx;
 mod instantiation;
 mod proof;
 mod term;
 
+pub use enode::*;
 pub use equality::*;
 pub use idx::*;
 pub use instantiation::*;

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

@@ -10,8 +10,8 @@ use petgraph::{
 
 use crate::{
     items::{
-        ENodeIdx, EqGivenIdx, EqTransIdx, EqualityExpl, InstIdx, StackIdx, TermIdx, TransitiveExpl,
-        TransitiveExplSegment, TransitiveExplSegmentKind,
+        ENode, ENodeIdx, EqGivenIdx, EqTransIdx, Equality, EqualityExpl, InstIdx, TermIdx,
+        TransitiveExpl, TransitiveExplSegment, TransitiveExplSegmentKind,
     },
     BoxSlice, Error, FxHashMap, NonMaxU32, Result, TiVec,
 };
@@ -372,22 +372,6 @@ impl std::ops::Index<ENodeIdx> for EGraph {
     }
 }
 
-#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
-#[derive(Debug)]
-pub struct ENode {
-    frame: Option<StackIdx>,
-    pub created_by: Option<InstIdx>,
-    pub owner: TermIdx,
-    pub z3_generation: Option<u32>,
-
-    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.
-    transitive: FxHashMap<ENodeIdx, EqTransIdx>,
-    self_transitive: Option<EqTransIdx>,
-}
-
 impl ENode {
     pub fn get_equality(&self, _stack: &Stack) -> Option<&Equality> {
         // TODO: why are we allowed to use equalities from popped stack frames?
@@ -396,14 +380,6 @@ impl ENode {
     }
 }
 
-#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
-#[derive(Debug)]
-pub struct Equality {
-    _frame: Option<StackIdx>,
-    pub to: ENodeIdx,
-    pub expl: EqGivenIdx,
-}
-
 #[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
 #[derive(Debug, Default)]
 pub struct Equalities {

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

@@ -1,6 +1,6 @@
 use std::fmt::Debug;
 
-use super::LogParser;
+use super::{LogParser, LogParserHelper};
 use crate::{Error, FResult, Result};
 
 pub mod egraph;
@@ -13,7 +13,7 @@ pub mod terms;
 /// Compare with the log files in the `logs/` folder to see if this is the case.
 pub mod z3parser;
 
-impl<T: Z3LogParser + Default> LogParser for T {
+impl<T: Z3LogParser + LogParserHelper> LogParser for T {
     fn is_line_start(&mut self, first_byte: u8) -> bool {
         first_byte == b'['
     }

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

@@ -8,7 +8,7 @@ use crate::{
         Meaning, ProofIdx, ProofStep, QuantIdx, Term, TermAndMeaning, TermId, TermIdToIdxMap,
         TermIdx, TermKind,
     },
-    Error, FxHashMap, Result, StringTable, TiVec,
+    BoxSlice, Error, FxHashMap, Result, StringTable, TiVec,
 };
 
 pub trait HasTermId {
@@ -136,7 +136,7 @@ impl Terms {
     pub(crate) fn new_synthetic_term(
         &mut self,
         kind: TermKind,
-        child_ids: Box<[TermIdx]>,
+        child_ids: BoxSlice<TermIdx>,
         meaning: Option<Meaning>,
     ) -> TermIdx {
         let term = Term {

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

@@ -8,13 +8,7 @@ use crate::{
     BoxSlice, Error, IString, NonMaxU32, Result, StringTable, TiVec,
 };
 
-use super::{
-    egraph::{EGraph, ENode},
-    inst::Insts,
-    stack::Stack,
-    stm2::EventLog,
-    terms::Terms,
-};
+use super::{egraph::EGraph, inst::Insts, stack::Stack, stm2::EventLog, terms::Terms};
 
 /// A parser for Z3 log files. Use one of the various `Z3Parser::from_*` methods
 /// to construct this parser.
@@ -699,6 +693,7 @@ impl Z3LogParser for Z3Parser {
             .get_match(fingerprint)
             .ok_or(Error::UnknownFingerprint(fingerprint))?;
         let inst = Instantiation {
+            frame: self.stack.active_frame(),
             match_,
             fingerprint,
             proof_id,

smt-log-parser/tests/parse_logs.rs

@@ -66,7 +66,7 @@ fn parse_all_logs() {
                 (parse_limit <= s.bytes_read as u64).then_some(())
             });
             let elapsed = now.elapsed();
-            let mut parser = parser.take_parser();
+            let parser = parser.take_parser();
 
             max_parse_ovhd = f64::max(
                 max_parse_ovhd,
@@ -98,8 +98,15 @@ fn parse_all_logs() {
                 mem_limit / mb,
             );
             ALLOCATOR.set_limit(mem_limit as usize).unwrap();
-            let inst_graph = InstGraph::new(parser.parser()).unwrap();
+
+            let now = Instant::now();
+            let inst_graph = InstGraph::new(&parser).unwrap();
             let elapsed = now.elapsed();
+            assert!(
+                elapsed < timeout,
+                "Constructing inst graph took longer than timeout"
+            );
+
             max_analysis_ovhd = f64::max(
                 max_analysis_ovhd,
                 (ALLOCATOR.allocated() as u64 - middle_alloc) as f64 / parse_bytes as f64,
@@ -116,7 +123,6 @@ fn parse_all_logs() {
             println!();
             println!("===");
 
-            assert!(elapsed_ml < timeout, "ML search took longer than timeout");
             assert!(
                 mem_size as u64 <= parse_bytes * 2 / 3,
                 "Analysis takes up more memory than 2/3 * file size!"