diff --git a/patronus/src/btor2/parse.rs b/patronus/src/btor2/parse.rs index a2172a6..8142ee9 100644 --- a/patronus/src/btor2/parse.rs +++ b/patronus/src/btor2/parse.rs @@ -10,7 +10,6 @@ use fuzzy_matcher::FuzzyMatcher; use rustc_hash::{FxHashMap, FxHashSet}; use smallvec::SmallVec; use std::borrow::Cow; -use std::collections::HashMap; pub fn parse_str(ctx: &mut Context, input: &str, name: Option<&str>) -> Option { match Parser::new(ctx).parse(input.as_bytes(), name) { @@ -824,7 +823,7 @@ fn include_name(name: &str) -> bool { /// Instead it creates nodes that just point to the state and carry its name. This function searches /// for these nodes and tries to rename the states. fn improve_state_names(ctx: &mut Context, sys: &mut TransitionSystem) { - let mut renames = HashMap::new(); + let mut renames = FxHashMap::default(); for state in sys.states.iter() { // since the alias signal refers to the same expression as the state symbol, // it will generate a signal info with the better name @@ -974,12 +973,9 @@ const OTHER_OPS: [&str; 17] = [ ]; lazy_static! { - static ref UNARY_OPS_SET: std::collections::HashSet<&'static str> = - std::collections::HashSet::from(UNARY_OPS); - static ref BINARY_OPS_SET: std::collections::HashSet<&'static str> = - std::collections::HashSet::from(BINARY_OPS); - static ref OTHER_OPS_SET: std::collections::HashSet<&'static str> = - std::collections::HashSet::from(OTHER_OPS); + static ref UNARY_OPS_SET: FxHashSet<&'static str> = FxHashSet::from_iter(UNARY_OPS); + static ref BINARY_OPS_SET: FxHashSet<&'static str> = FxHashSet::from_iter(BINARY_OPS); + static ref OTHER_OPS_SET: FxHashSet<&'static str> = FxHashSet::from_iter(OTHER_OPS); } /// Indicated success or failure. Errors and data is not returned, but rather added to the context. diff --git a/patronus/src/dse/value_summary.rs b/patronus/src/dse/value_summary.rs index 653becb..b269c26 100644 --- a/patronus/src/dse/value_summary.rs +++ b/patronus/src/dse/value_summary.rs @@ -4,7 +4,7 @@ use crate::expr::*; use boolean_expression::{BDDFunc, BDD}; -use std::collections::{HashMap, HashSet}; +use rustc_hash::{FxBuildHasher, FxHashMap, FxHashSet}; use std::hash::Hash; #[derive(Debug, Clone)] @@ -130,9 +130,9 @@ impl ValueSummary { let mut out = Vec::with_capacity(a.len() + b.len()); // first we check to see if any guards are the same, then we do not need to apply the cross product - let a_guards: HashSet = a.iter().map(|e| e.guard).collect(); - let b_guards: HashSet = b.iter().map(|e| e.guard).collect(); - let common_guards: HashSet = a_guards.intersection(&b_guards).cloned().collect(); + let a_guards: FxHashSet = a.iter().map(|e| e.guard).collect(); + let b_guards: FxHashSet = b.iter().map(|e| e.guard).collect(); + let common_guards: FxHashSet = a_guards.intersection(&b_guards).cloned().collect(); if !common_guards.is_empty() { // merge common guard entries @@ -212,7 +212,7 @@ impl ValueSummary { } fn coalesce_entries(entries: &mut Vec>, gc: &mut GuardCtx) { - let mut by_value = HashMap::with_capacity(entries.len()); + let mut by_value = FxHashMap::with_capacity_and_hasher(entries.len(), FxBuildHasher); let mut delete_list = vec![]; for ii in 0..entries.len() { let entry = entries[ii].clone(); diff --git a/patronus/src/expr/parse.rs b/patronus/src/expr/parse.rs index 1e5a2f2..13f6c29 100644 --- a/patronus/src/expr/parse.rs +++ b/patronus/src/expr/parse.rs @@ -5,7 +5,7 @@ use crate::expr::{Context, ExprRef, TypeCheck, WidthInt}; use baa::BitVecValue; use regex::{Captures, Match, Regex, RegexSet}; -use std::collections::HashMap; +use rustc_hash::FxHashMap; pub fn parse_expr(ctx: &mut Context, inp: &str) -> ExprRef { let mut parser = Parser::new(ctx, inp); @@ -18,7 +18,7 @@ pub fn parse_expr(ctx: &mut Context, inp: &str) -> ExprRef { struct Parser<'a> { ctx: &'a mut Context, inp: &'a str, - symbols: HashMap, + symbols: FxHashMap, } #[derive(Debug, Copy, Clone)] @@ -36,7 +36,7 @@ enum ArgTpe { impl<'a> Parser<'a> { fn new(ctx: &'a mut Context, inp: &'a str) -> Self { let inp = inp.trim(); - let symbols = HashMap::new(); + let symbols = FxHashMap::default(); Self { ctx, inp, symbols } } diff --git a/patronus/src/mc/smt.rs b/patronus/src/mc/smt.rs index f1c3a33..965bdff 100644 --- a/patronus/src/mc/smt.rs +++ b/patronus/src/mc/smt.rs @@ -12,7 +12,6 @@ use crate::system::{State, TransitionSystem}; use baa::*; use easy_smt as smt; use rustc_hash::FxHashSet; -use std::collections::HashSet; #[derive(Debug, Clone, Copy)] pub struct SmtSolverCmd { @@ -346,7 +345,8 @@ impl UnrollSmtEncoding { let mut signals = vec![None; signals_map_len]; let mut signal_order = Vec::with_capacity(ser_info.signal_order.len()); - let is_state: HashSet = HashSet::from_iter(sys.states.iter().map(|s| s.symbol)); + let is_state: FxHashSet = + FxHashSet::from_iter(sys.states.iter().map(|s| s.symbol)); // we skip states in our signal order since they are not calculated directly in the update function let input_set = FxHashSet::from_iter(sys.inputs.iter().cloned()); diff --git a/patronus/src/system/transform.rs b/patronus/src/system/transform.rs index 8829664..4a3505e 100644 --- a/patronus/src/system/transform.rs +++ b/patronus/src/system/transform.rs @@ -6,14 +6,14 @@ use super::TransitionSystem; use crate::btor2::{DEFAULT_INPUT_PREFIX, DEFAULT_STATE_PREFIX}; use crate::expr::*; -use std::collections::HashMap; +use rustc_hash::FxHashMap; /** Remove any inputs named `_input_[...]` and replace their use with a literal zero. * This essentially gets rid of all undefined value modelling by yosys. */ pub fn replace_anonymous_inputs_with_zero(ctx: &mut Context, sys: &mut TransitionSystem) { // find and remove inputs - let mut replace_map = HashMap::new(); + let mut replace_map = FxHashMap::default(); sys.inputs.retain(|&input| { let name = ctx.get_symbol_name(input).unwrap(); if name.starts_with(DEFAULT_INPUT_PREFIX) || name.starts_with(DEFAULT_STATE_PREFIX) {