fmt and clippy

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()));
         }

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,
 };

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;

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 {

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

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 {

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, ()>>,
 }
 

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 {

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,
 };
 

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)]

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;

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()
     }
 }

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,
 };

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",

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)]

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,
 };

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,
 };