Use rustc_data_structures::fx::FxHashSet

Cargo.toml

@@ -16,6 +16,7 @@ rust-version = "1.84"
 [dependencies]
 bitflags = "^2.8"
 instant = { version = "0.1", features = ["wasm-bindgen"], optional = true }
+rustc_data_structures = "^0.1"
 
 [features]
 default = [

src/assign/rephase.rs

@@ -1,15 +1,15 @@
 use {
     super::AssignStack,
     crate::{types::*, var_vector::*},
-    std::collections::HashMap,
+    rustc_data_structures::fx::FxHashMap,
 };
 
 pub trait AssignRephaseIF {
     /// check usability of the saved best phase.
     /// return `true` if the current best phase got invalid.
     fn check_best_phase(&mut self, vi: VarId) -> bool;
-    fn best_phases_ref(&mut self, default_value: Option<bool>) -> HashMap<VarId, bool>;
-    fn override_rephasing_target(&mut self, assignment: &HashMap<VarId, bool>) -> usize;
+    fn best_phases_ref(&mut self, default_value: Option<bool>) -> FxHashMap<VarId, bool>;
+    fn override_rephasing_target(&mut self, assignment: &FxHashMap<VarId, bool>) -> usize;
     fn select_rephasing_target(&mut self);
     fn check_consistency_of_best_phases(&mut self);
 }
@@ -30,7 +30,7 @@ impl AssignRephaseIF for AssignStack {
         }
         false
     }
-    fn best_phases_ref(&mut self, default_value: Option<bool>) -> HashMap<VarId, bool> {
+    fn best_phases_ref(&mut self, default_value: Option<bool>) -> FxHashMap<VarId, bool> {
         VarRef::var_id_iter()
             .filter_map(|vi| {
                 if VarRef(vi).level() == self.root_level || VarRef(vi).is(FlagVar::ELIMINATED) {
@@ -47,9 +47,9 @@ impl AssignRephaseIF for AssignStack {
                     ))
                 }
             })
-            .collect::<HashMap<VarId, bool>>()
+            .collect::<FxHashMap<VarId, bool>>()
     }
-    fn override_rephasing_target(&mut self, assignment: &HashMap<VarId, bool>) -> usize {
+    fn override_rephasing_target(&mut self, assignment: &FxHashMap<VarId, bool>) -> usize {
         let mut num_flipped = 0;
         for (vi, b) in assignment.iter() {
             if self.best_phases.get(vi).is_none_or(|(p, _)| *p != *b) {

src/assign/stack.rs

@@ -6,7 +6,10 @@ use {
 };
 
 #[cfg(any(feature = "best_phases_tracking", feature = "rephase"))]
-use std::collections::HashMap;
+use {
+    rustc_data_structures::fx::{FxHashMap, FxHasher},
+    std::{collections::HashMap, hash::BuildHasherDefault},
+};
 
 #[cfg(feature = "trail_saving")]
 use super::TrailSavingIF;
@@ -37,7 +40,7 @@ pub struct AssignStack {
     pub(super) bp_divergence_ema: Ema,
 
     #[cfg(feature = "best_phases_tracking")]
-    pub(super) best_phases: HashMap<VarId, (bool, AssignReason)>,
+    pub(super) best_phases: FxHashMap<VarId, (bool, AssignReason)>,
     #[cfg(feature = "rephase")]
     pub(super) phase_age: usize,
 
@@ -92,7 +95,8 @@ impl Default for AssignStack {
             bp_divergence_ema: Ema::new(10),
 
             #[cfg(feature = "best_phases_tracking")]
-            best_phases: HashMap::new(),
+            best_phases:
+                HashMap::<VarId, (bool, AssignReason), BuildHasherDefault<FxHasher>>::default(),
             #[cfg(feature = "rephase")]
             phase_age: 0,
 

src/cdb/binary.rs

@@ -1,8 +1,10 @@
 use {
     super::ClauseId,
     crate::types::*,
+    rustc_data_structures::fx::{FxHashMap, FxHasher},
     std::{
         collections::HashMap,
+        hash::BuildHasherDefault,
         ops::{Index, IndexMut},
     },
 };
@@ -38,15 +40,15 @@ impl IndexMut<Lit> for Vec<BinaryLinkList> {
 /// storage with mapper to `ClauseId` of binary links
 #[derive(Clone, Debug, Default)]
 pub struct BinaryLinkDB {
-    hash: HashMap<(Lit, Lit), ClauseId>,
+    hash: FxHashMap<(Lit, Lit), ClauseId>,
     list: Vec<BinaryLinkList>,
 }
 
 impl Instantiate for BinaryLinkDB {
     fn instantiate(_conf: &Config, cnf: &CNFDescription) -> Self {
         let num_lit = 2 * (cnf.num_of_variables + 1);
         BinaryLinkDB {
-            hash: HashMap::new(),
+            hash: HashMap::<(Lit, Lit), ClauseId, BuildHasherDefault<FxHasher>>::default(),
             list: vec![Vec::new(); num_lit],
         }
     }

src/cdb/sls.rs

@@ -2,7 +2,8 @@
 use {
     super::{Clause, ClauseDB, VarId},
     crate::types::*,
-    std::collections::HashMap,
+    rustc_data_structures::fx::{FxHashMap, FxHasher},
+    std::{collections::HashMap, hash::BuildHasherDefault},
 };
 
 pub trait StochasticLocalSearchIF {
@@ -12,15 +13,15 @@ pub trait StochasticLocalSearchIF {
     /// This would be a better criteria that can be used in CDCL solvers.
     fn stochastic_local_search(
         &mut self,
-        start: &mut HashMap<VarId, bool>,
+        start: &mut FxHashMap<VarId, bool>,
         limit: usize,
     ) -> (usize, usize);
 }
 
 impl StochasticLocalSearchIF for ClauseDB {
     fn stochastic_local_search(
         &mut self,
-        assignment: &mut HashMap<VarId, bool>,
+        assignment: &mut FxHashMap<VarId, bool>,
         limit: usize,
     ) -> (usize, usize) {
         let mut returns: (usize, usize) = (0, 0);
@@ -30,7 +31,8 @@ impl StochasticLocalSearchIF for ClauseDB {
             let mut unsat_clauses = 0;
             // let mut level: DecisionLevel = 0;
             // CONSIDER: counting only given (permanent) clauses.
-            let mut flip_target: HashMap<VarId, usize> = HashMap::new();
+            let mut flip_target: FxHashMap<VarId, usize> =
+                HashMap::<VarId, usize, BuildHasherDefault<FxHasher>>::default();
             let mut target_clause: Option<&Clause> = None;
             for c in self.clause.iter().skip(1).filter(|c| !c.is_dead()) {
                 // let mut cls_lvl: DecisionLevel = 0;
@@ -86,8 +88,8 @@ impl StochasticLocalSearchIF for ClauseDB {
 impl Clause {
     fn is_falsified(
         &self,
-        assignment: &HashMap<VarId, bool>,
-        flip_target: &mut HashMap<VarId, usize>,
+        assignment: &FxHashMap<VarId, bool>,
+        flip_target: &mut FxHashMap<VarId, usize>,
     ) -> bool {
         let mut num_sat = 0;
         let mut sat_vi = 0;

src/cdb/watch_cache.rs

@@ -2,7 +2,7 @@ use {
     super::ClauseId,
     crate::types::*,
     std::{
-        collections::HashMap,
+        //        collections::HashMap,
         ops::{Index, IndexMut},
     },
 };
@@ -44,30 +44,30 @@ impl WatchCacheIF for WatchCacheList {
     }
 }
 
-impl Index<Lit> for Vec<HashMap<Lit, ClauseId>> {
-    type Output = HashMap<Lit, ClauseId>;
-    #[inline]
-    fn index(&self, l: Lit) -> &Self::Output {
-        #[cfg(feature = "unsafe_access")]
-        unsafe {
-            self.get_unchecked(usize::from(l))
-        }
-        #[cfg(not(feature = "unsafe_access"))]
-        &self[usize::from(l)]
-    }
-}
+// impl Index<Lit> for Vec<HashMap<Lit, ClauseId>> {
+//     type Output = HashMap<Lit, ClauseId>;
+//     #[inline]
+//     fn index(&self, l: Lit) -> &Self::Output {
+//         #[cfg(feature = "unsafe_access")]
+//         unsafe {
+//             self.get_unchecked(usize::from(l))
+//         }
+//         #[cfg(not(feature = "unsafe_access"))]
+//         &self[usize::from(l)]
+//     }
+// }
 
-impl IndexMut<Lit> for Vec<HashMap<Lit, ClauseId>> {
-    #[inline]
-    fn index_mut(&mut self, l: Lit) -> &mut Self::Output {
-        #[cfg(feature = "unsafe_access")]
-        unsafe {
-            self.get_unchecked_mut(usize::from(l))
-        }
-        #[cfg(not(feature = "unsafe_access"))]
-        &mut self[usize::from(l)]
-    }
-}
+// impl IndexMut<Lit> for Vec<HashMap<Lit, ClauseId>> {
+//     #[inline]
+//     fn index_mut(&mut self, l: Lit) -> &mut Self::Output {
+//         #[cfg(feature = "unsafe_access")]
+//         unsafe {
+//             self.get_unchecked_mut(usize::from(l))
+//         }
+//         #[cfg(not(feature = "unsafe_access"))]
+//         &mut self[usize::from(l)]
+//     }
+// }
 
 impl Index<Lit> for Vec<WatchCache> {
     type Output = WatchCache;

src/cnf/mod.rs

@@ -1,10 +1,12 @@
 // pub mod cnf;
 // pub use self::cnf::*;
-use std::{
-    collections::HashSet,
-    fs::File,
-    io::{BufRead, BufReader},
-    path::Path,
+use {
+    rustc_data_structures::fx::FxHashSet,
+    std::{
+        fs::File,
+        io::{BufRead, BufReader},
+        path::Path,
+    },
 };
 
 const TOO_MANY_CLAUSES: usize = 100_000;
@@ -26,9 +28,9 @@ pub enum CNFOperationError {
 #[derive(Debug, Default, Eq, PartialEq)]
 pub struct CNF {
     num_vars: u32,
-    assign: HashSet<i32>,
+    assign: FxHashSet<i32>,
     clauses: Vec<Clause>,
-    cls_map: HashSet<Vec<i32>>,
+    cls_map: FxHashSet<Vec<i32>>,
     no_check_uniqueness: bool,
 }
 
@@ -43,7 +45,7 @@ impl std::fmt::Display for CNF {
     }
 }
 
-pub trait CnfIf: Sized {
+pub trait CnfIF: Sized {
     type Error;
     // Add a `Clause` and returns:
     // - `Some(self)`: if add it successfully
@@ -57,7 +59,7 @@ pub trait CnfIf: Sized {
     fn dump_to_string(&self) -> String;
 }
 
-impl CnfIf for CNF {
+impl CnfIF for CNF {
     type Error = CNFOperationError;
     fn add_clause<C: AsRef<Clause>>(&mut self, clause: C) -> Result<&mut CNF, Self::Error> {
         let c = clause.as_ref().clone();

src/vam.rs

@@ -156,12 +156,12 @@ impl VarIdHeap {
 }
 // Decision var selection
 
-use std::collections::HashMap;
+use rustc_data_structures::fx::FxHashMap;
 
 /// API for var selection, depending on an internal heap.
 pub trait VarSelectIF {
     /// give rewards to vars selected by SLS
-    fn reward_by_sls(assignment: &HashMap<VarId, bool>) -> usize;
+    fn reward_by_sls(assignment: &FxHashMap<VarId, bool>) -> usize;
     /// select a new decision variable.
     fn select_decision_literal(asg: &mut AssignStack) -> Lit;
     /// update the internal heap on var order.
@@ -171,7 +171,7 @@ pub trait VarSelectIF {
 }
 
 impl VarSelectIF for VarActivityManager {
-    fn reward_by_sls(assignment: &HashMap<VarId, bool>) -> usize {
+    fn reward_by_sls(assignment: &FxHashMap<VarId, bool>) -> usize {
         unsafe {
             let mut num_flipped = 0;
             for (vi, b) in assignment.iter() {