From ad28a48b3b99e60ffca5f865c6f13725f04e19d7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jon=C3=A1=C5=A1=20Fiala?= <jonas.fiala@inf.ethz.ch>
Date: Wed, 30 Oct 2024 17:40:16 +0100
Subject: [PATCH] fmt and clippy

---
 axiom-profiler-GUI/src/results/node_info.rs   |  2 +-
 .../analysis/matching_loop/generalise.rs      |  2 +-
 .../graph/analysis/matching_loop/mod.rs       |  2 --
 .../graph/analysis/matching_loop/node.rs      |  2 +-
 .../graph/analysis/matching_loop/search.rs    | 24 ++++---------------
 .../graph/analysis/matching_loop/signature.rs | 11 ++-------
 .../src/analysis/graph/analysis/mod.rs        |  4 +++-
 .../src/analysis/graph/generalise.rs          |  4 ++--
 smt-log-parser/src/analysis/graph/raw.rs      |  1 -
 smt-log-parser/src/error.rs                   |  6 -----
 smt-log-parser/src/items/inst.rs              |  1 -
 smt-log-parser/src/mem_dbg/mod.rs             | 12 ++++++----
 smt-log-parser/src/parsers/z3/egraph.rs       |  4 ++--
 smt-log-parser/src/parsers/z3/stm2.rs         |  2 +-
 smt-log-parser/src/parsers/z3/synthetic.rs    |  6 ++---
 smt-log-parser/src/parsers/z3/terms.rs        |  2 +-
 smt-log-parser/src/parsers/z3/z3parser.rs     |  4 +---
 17 files changed, 30 insertions(+), 59 deletions(-)

diff --git a/axiom-profiler-GUI/src/results/node_info.rs b/axiom-profiler-GUI/src/results/node_info.rs
index 854d6a94..87486a64 100644
--- a/axiom-profiler-GUI/src/results/node_info.rs
+++ b/axiom-profiler-GUI/src/results/node_info.rs
@@ -190,7 +190,7 @@ impl<'a, 'b> NodeInfo<'a, 'b> {
         {
             extra_info.push(("z3 gen", z3gen.to_string()));
         }
-        if let Some(frame) = self.node.frame(&self.ctxt.parser) {
+        if let Some(frame) = self.node.frame(self.ctxt.parser) {
             let frame = &self.ctxt.parser[frame];
             extra_info.push(("Frame", frame.active.to_string()));
         }
diff --git a/smt-log-parser/src/analysis/graph/analysis/matching_loop/generalise.rs b/smt-log-parser/src/analysis/graph/analysis/matching_loop/generalise.rs
index e05a325e..1b520cc3 100644
--- a/smt-log-parser/src/analysis/graph/analysis/matching_loop/generalise.rs
+++ b/smt-log-parser/src/analysis/graph/analysis/matching_loop/generalise.rs
@@ -1,7 +1,7 @@
 use petgraph::graph::NodeIndex;
 
 use crate::{
-    analysis::{raw::NodeKind, visible::VisibleInstGraph, InstGraph, VisibleNodeIndex},
+    analysis::{raw::NodeKind, InstGraph},
     items::{ENodeIdx, EqTransIdx, QuantIdx, TermIdx},
     FxHashMap, Graph, Z3Parser,
 };
diff --git a/smt-log-parser/src/analysis/graph/analysis/matching_loop/mod.rs b/smt-log-parser/src/analysis/graph/analysis/matching_loop/mod.rs
index b581832c..7be3d2bb 100644
--- a/smt-log-parser/src/analysis/graph/analysis/matching_loop/mod.rs
+++ b/smt-log-parser/src/analysis/graph/analysis/matching_loop/mod.rs
@@ -3,9 +3,7 @@ mod node;
 mod search;
 mod signature;
 
-pub use generalise::*;
 pub use node::*;
-pub use search::*;
 pub use signature::*;
 
 pub const MIN_MATCHING_LOOP_LENGTH: usize = 3;
diff --git a/smt-log-parser/src/analysis/graph/analysis/matching_loop/node.rs b/smt-log-parser/src/analysis/graph/analysis/matching_loop/node.rs
index b9b93348..3086a868 100644
--- a/smt-log-parser/src/analysis/graph/analysis/matching_loop/node.rs
+++ b/smt-log-parser/src/analysis/graph/analysis/matching_loop/node.rs
@@ -3,7 +3,7 @@ use fxhash::FxHashSet;
 use crate::{
     items::{QuantIdx, TermIdx},
     parsers::z3::synthetic::MaybeSynthIdx,
-    FxHashMap, Z3Parser,
+    Z3Parser,
 };
 
 pub(super) struct MlEquality {
diff --git a/smt-log-parser/src/analysis/graph/analysis/matching_loop/search.rs b/smt-log-parser/src/analysis/graph/analysis/matching_loop/search.rs
index 40a0ce25..56d0a686 100644
--- a/smt-log-parser/src/analysis/graph/analysis/matching_loop/search.rs
+++ b/smt-log-parser/src/analysis/graph/analysis/matching_loop/search.rs
@@ -1,22 +1,14 @@
-#[cfg(feature = "mem_dbg")]
-use mem_dbg::{MemDbg, MemSize};
-
-use fxhash::FxHashSet;
 use petgraph::visit::{Dfs, Reversed};
 
 use crate::{
     analysis::{
-        raw::{IndexesInstGraph, NodeKind},
-        visible::VisibleEdge,
-        InstGraph, LogInfo, RawNodeIndex,
+        analysis::MlEndNodes, raw::NodeKind, visible::VisibleEdge, InstGraph, RawNodeIndex,
     },
-    display_with::{DisplayCtxt, DisplayWithCtxt},
-    formatter::TermDisplayContext,
-    items::{ENodeIdx, InstIdx, Instantiation, Match, QuantIdx, TermIdx, TimeRange},
-    FxHashMap, Z3Parser,
+    items::{InstIdx, TermIdx, TimeRange},
+    Z3Parser,
 };
 
-use super::{MLGraphNode, MlSignature, MIN_MATCHING_LOOP_LENGTH};
+use super::{MLGraphNode, MIN_MATCHING_LOOP_LENGTH};
 
 impl InstGraph {
     pub fn search_matching_loops(&mut self, parser: &mut Z3Parser) -> usize {
@@ -90,13 +82,7 @@ impl InstGraph {
     /// Per each quantifier, finds the nodes that are part paths of length at
     /// least `MIN_MATCHING_LOOP_LENGTH`. Additionally, returns a list of the
     /// endpoints of these paths.
-    fn find_long_paths_per_quant(
-        &mut self,
-        parser: &Z3Parser,
-    ) -> (
-        Vec<(MlSignature, Vec<(usize, RawNodeIndex)>)>,
-        Vec<RawNodeIndex>,
-    ) {
+    fn find_long_paths_per_quant(&mut self, parser: &Z3Parser) -> (MlEndNodes, Vec<RawNodeIndex>) {
         let signatures = Self::collect_ml_signatures(parser);
         // Collect all signatures instantiated at least `MIN_MATCHING_LOOP_LENGTH` times
         let mut signatures: Vec<_> = signatures
diff --git a/smt-log-parser/src/analysis/graph/analysis/matching_loop/signature.rs b/smt-log-parser/src/analysis/graph/analysis/matching_loop/signature.rs
index ebb95897..9132208c 100644
--- a/smt-log-parser/src/analysis/graph/analysis/matching_loop/signature.rs
+++ b/smt-log-parser/src/analysis/graph/analysis/matching_loop/signature.rs
@@ -2,22 +2,15 @@
 use mem_dbg::{MemDbg, MemSize};
 
 use fxhash::FxHashSet;
-use petgraph::visit::{Dfs, Reversed};
 
 use crate::{
-    analysis::{
-        raw::{IndexesInstGraph, NodeKind},
-        visible::VisibleEdge,
-        InstGraph, LogInfo, RawNodeIndex,
-    },
+    analysis::InstGraph,
     display_with::{DisplayCtxt, DisplayWithCtxt},
     formatter::TermDisplayContext,
-    items::{ENodeIdx, InstIdx, Instantiation, Match, QuantIdx, TermIdx},
+    items::{ENodeIdx, InstIdx, Instantiation, QuantIdx, TermIdx},
     FxHashMap, Z3Parser,
 };
 
-use super::{MLGraphNode, MIN_MATCHING_LOOP_LENGTH};
-
 #[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
 #[derive(Clone, Debug, PartialEq, Eq, Hash, PartialOrd, Ord)]
 pub struct MlSignature {
diff --git a/smt-log-parser/src/analysis/graph/analysis/mod.rs b/smt-log-parser/src/analysis/graph/analysis/mod.rs
index c5974423..a86f7b0a 100644
--- a/smt-log-parser/src/analysis/graph/analysis/mod.rs
+++ b/smt-log-parser/src/analysis/graph/analysis/mod.rs
@@ -21,6 +21,8 @@ use self::{
 
 use super::{raw::Node, InstGraph, RawNodeIndex};
 
+pub type MlEndNodes = Vec<(MlSignature, Vec<(usize, RawNodeIndex)>)>;
+
 #[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
 #[derive(Debug, Default)]
 pub struct Analysis {
@@ -32,7 +34,7 @@ pub struct Analysis {
     pub fwd_depth_min: Vec<RawNodeIndex>,
     // // Most to least
     // pub(super) max_depth: Vec<RawNodeIndex>,
-    pub matching_loop_end_nodes: Option<Vec<(MlSignature, Vec<(usize, RawNodeIndex)>)>>,
+    pub matching_loop_end_nodes: Option<MlEndNodes>,
     pub matching_loop_graphs: Vec<Graph<MLGraphNode, ()>>,
 }
 
diff --git a/smt-log-parser/src/analysis/graph/generalise.rs b/smt-log-parser/src/analysis/graph/generalise.rs
index 5c8642b9..3d04d086 100644
--- a/smt-log-parser/src/analysis/graph/generalise.rs
+++ b/smt-log-parser/src/analysis/graph/generalise.rs
@@ -1,10 +1,10 @@
 use crate::{
-    items::{Meaning, SynthTermIdx, Term, TermIdx, TermKind},
+    items::{TermIdx, TermKind},
     parsers::z3::{
         synthetic::{MaybeSynthIdx, MaybeSynthTerm, SynthTermKind, SynthTerms},
         terms::Terms,
     },
-    IString, Result, StringTable,
+    Result,
 };
 
 impl SynthTerms {
diff --git a/smt-log-parser/src/analysis/graph/raw.rs b/smt-log-parser/src/analysis/graph/raw.rs
index c7f9f72a..37e029cc 100644
--- a/smt-log-parser/src/analysis/graph/raw.rs
+++ b/smt-log-parser/src/analysis/graph/raw.rs
@@ -18,7 +18,6 @@ use crate::{
         ENodeIdx, EqGivenIdx, EqTransIdx, EqualityExpl, GraphIdx, InstIdx, StackIdx,
         TransitiveExplSegmentKind,
     },
-    parsers::z3::synthetic::MaybeSynthIdx,
     DiGraph, FxHashMap, NonMaxU32, Result, Z3Parser,
 };
 
diff --git a/smt-log-parser/src/error.rs b/smt-log-parser/src/error.rs
index 95d4a5c6..0ce4e65d 100644
--- a/smt-log-parser/src/error.rs
+++ b/smt-log-parser/src/error.rs
@@ -24,12 +24,6 @@ impl<T, U> Either<T, U> {
             Self::Right(u) => Err(u),
         }
     }
-    pub fn as_result(&self) -> std::result::Result<&T, &U> {
-        match self {
-            Self::Left(t) => Ok(t),
-            Self::Right(u) => Err(u),
-        }
-    }
 }
 
 #[derive(Debug)]
diff --git a/smt-log-parser/src/items/inst.rs b/smt-log-parser/src/items/inst.rs
index e6bbefef..39117b5e 100644
--- a/smt-log-parser/src/items/inst.rs
+++ b/smt-log-parser/src/items/inst.rs
@@ -1,7 +1,6 @@
 #[cfg(feature = "mem_dbg")]
 use mem_dbg::{MemDbg, MemSize};
 
-use crate::error::Either;
 use crate::{Error, Result};
 use std::fmt;
 use std::ops::Index;
diff --git a/smt-log-parser/src/mem_dbg/mod.rs b/smt-log-parser/src/mem_dbg/mod.rs
index e5c1b1cc..ea6cc4f0 100644
--- a/smt-log-parser/src/mem_dbg/mod.rs
+++ b/smt-log-parser/src/mem_dbg/mod.rs
@@ -125,8 +125,10 @@ impl<K, V> FromIterator<V> for TiVec<K, V> {
         Self(typed_index_collections::TiVec::from_iter(iter))
     }
 }
-impl<K, V> TiVec<K, V> {
-    pub fn into_iter(self) -> std::vec::IntoIter<V> {
+impl<K, V> std::iter::IntoIterator for TiVec<K, V> {
+    type Item = <Self::IntoIter as std::iter::IntoIterator>::Item;
+    type IntoIter = std::vec::IntoIter<V>;
+    fn into_iter(self) -> Self::IntoIter {
         self.0.into_iter()
     }
 }
@@ -144,8 +146,10 @@ impl<K: Eq + std::hash::Hash, V> FromIterator<(K, V)> for FxHashMap<K, V> {
         Self(fxhash::FxHashMap::from_iter(iter))
     }
 }
-impl<K, V> FxHashMap<K, V> {
-    pub fn into_iter(self) -> std::collections::hash_map::IntoIter<K, V> {
+impl<K, V> std::iter::IntoIterator for FxHashMap<K, V> {
+    type Item = <Self::IntoIter as std::iter::IntoIterator>::Item;
+    type IntoIter = std::collections::hash_map::IntoIter<K, V>;
+    fn into_iter(self) -> Self::IntoIter {
         self.0.into_iter()
     }
 }
diff --git a/smt-log-parser/src/parsers/z3/egraph.rs b/smt-log-parser/src/parsers/z3/egraph.rs
index 05994138..992a614f 100644
--- a/smt-log-parser/src/parsers/z3/egraph.rs
+++ b/smt-log-parser/src/parsers/z3/egraph.rs
@@ -10,8 +10,8 @@ use petgraph::{
 
 use crate::{
     items::{
-        ENode, ENodeIdx, EqGivenIdx, EqTransIdx, Equality, EqualityExpl, InstIdx, StackIdx,
-        TermIdx, TransitiveExpl, TransitiveExplSegment, TransitiveExplSegmentKind,
+        ENode, ENodeIdx, EqGivenIdx, EqTransIdx, Equality, EqualityExpl, InstIdx, TermIdx,
+        TransitiveExpl, TransitiveExplSegment, TransitiveExplSegmentKind,
     },
     BoxSlice, Error, FxHashMap, NonMaxU32, Result, TiVec,
 };
diff --git a/smt-log-parser/src/parsers/z3/stm2.rs b/smt-log-parser/src/parsers/z3/stm2.rs
index 603fb4b2..7b691032 100644
--- a/smt-log-parser/src/parsers/z3/stm2.rs
+++ b/smt-log-parser/src/parsers/z3/stm2.rs
@@ -10,7 +10,7 @@ use super::terms::Terms;
 
 /// Taken from `ast_smt_pp.cpp` of z3. These are not user defined and cannot be
 /// used as triggers.
-pub const M_PREDEF_NAMES: &'static [&'static str] = &[
+pub const M_PREDEF_NAMES: &[&str] = &[
     "=", ">=", "<=", "+", "-", "*", ">", "<", "!=", "or", "and", "implies", "not", "iff", "xor",
     "true", "false", "forall", "exists", "let", "flet", // Extended with the following.
     "pi", "euler", "pattern", "to_int", "to_real",
diff --git a/smt-log-parser/src/parsers/z3/synthetic.rs b/smt-log-parser/src/parsers/z3/synthetic.rs
index 47502170..87330784 100644
--- a/smt-log-parser/src/parsers/z3/synthetic.rs
+++ b/smt-log-parser/src/parsers/z3/synthetic.rs
@@ -1,15 +1,13 @@
-use std::{collections::hash_map::Entry, mem::ManuallyDrop, ops::Index};
+use std::{collections::hash_map::Entry, ops::Index};
 
 #[cfg(feature = "mem_dbg")]
 use mem_dbg::{MemDbg, MemSize};
 
 use crate::{
-    items::{QuantIdx, Quantifier, SynthTermIdx, Term, TermIdx, TermKind},
+    items::{SynthTermIdx, Term, TermIdx, TermKind},
     FxHashMap, IString, Result, TiVec,
 };
 
-use super::terms::Terms;
-
 // #[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
 // #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 // #[derive(Debug, PartialEq, Eq, Hash, Clone, Copy)]
diff --git a/smt-log-parser/src/parsers/z3/terms.rs b/smt-log-parser/src/parsers/z3/terms.rs
index ee3de3ad..1aaddacc 100644
--- a/smt-log-parser/src/parsers/z3/terms.rs
+++ b/smt-log-parser/src/parsers/z3/terms.rs
@@ -6,7 +6,7 @@ use crate::{
     error::Either,
     items::{
         InstProofLink, Instantiation, Meaning, ProofIdx, ProofStep, ProofStepKind, QuantIdx, Term,
-        TermId, TermIdToIdxMap, TermIdx, TermKind,
+        TermId, TermIdToIdxMap, TermIdx,
     },
     Error, FxHashMap, Result, StringTable, TiVec,
 };
diff --git a/smt-log-parser/src/parsers/z3/z3parser.rs b/smt-log-parser/src/parsers/z3/z3parser.rs
index 48800fee..11791f58 100644
--- a/smt-log-parser/src/parsers/z3/z3parser.rs
+++ b/smt-log-parser/src/parsers/z3/z3parser.rs
@@ -3,8 +3,6 @@ use mem_dbg::{MemDbg, MemSize};
 use typed_index_collections::TiSlice;
 
 use crate::{
-    display_with::{DisplayCtxt, DisplayWithCtxt},
-    formatter::TermDisplayContext,
     items::*,
     parsers::z3::{VersionInfo, Z3LogParser},
     Error, IString, Result, StringTable, TiVec,
@@ -15,7 +13,7 @@ use super::{
     inst::Insts,
     stack::Stack,
     stm2::EventLog,
-    synthetic::{MaybeSynthIdx, MaybeSynthTerm, SynthTerm, SynthTerms},
+    synthetic::{SynthTerm, SynthTerms},
     terms::Terms,
 };