switch to FXHash everywhere

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<TransitionSystem> {
     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.

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<V: Value> ValueSummary<V> {
         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<Guard> = a.iter().map(|e| e.guard).collect();
-        let b_guards: HashSet<Guard> = b.iter().map(|e| e.guard).collect();
-        let common_guards: HashSet<Guard> = a_guards.intersection(&b_guards).cloned().collect();
+        let a_guards: FxHashSet<Guard> = a.iter().map(|e| e.guard).collect();
+        let b_guards: FxHashSet<Guard> = b.iter().map(|e| e.guard).collect();
+        let common_guards: FxHashSet<Guard> = a_guards.intersection(&b_guards).cloned().collect();
 
         if !common_guards.is_empty() {
             // merge common guard entries
@@ -212,7 +212,7 @@ impl<V: Value> ValueSummary<V> {
 }
 
 fn coalesce_entries<V: Value>(entries: &mut Vec<Entry<V>>, 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();

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<String, ExprRef>,
+    symbols: FxHashMap<String, ExprRef>,
 }
 
 #[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 }
     }
 

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<ExprRef> = HashSet::from_iter(sys.states.iter().map(|s| s.symbol));
+        let is_state: FxHashSet<ExprRef> =
+            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());

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