Add dedicated cache for variables

src/formulas/formula_cache/mod.rs

@@ -3,6 +3,7 @@ pub mod implication_cache;
 pub mod nary_formula_cache;
 pub mod not_cache;
 pub mod simple_cache;
+pub mod var_cache;
 
 pub mod formula_encoding;
 pub mod formula_factory_caches;

src/formulas/formula_cache/var_cache.rs

@@ -0,0 +1,63 @@
+use std::borrow::Cow;
+
+use dashmap::DashMap;
+
+use crate::collections::AppendOnlyVec;
+use crate::formulas::formula_cache::formula_encoding::Encoding;
+use crate::formulas::formula_cache::CACHE_INITIAL_CAPACITY;
+use crate::formulas::{FormulaType, LitType, VarType};
+
+use super::formula_encoding::FormulaEncoding;
+
+pub struct VariableCache {
+    vec: AppendOnlyVec<String>,
+    reverse_map: DashMap<String, FormulaEncoding>,
+}
+
+impl VariableCache {
+    pub fn new() -> Self {
+        Self { vec: AppendOnlyVec::new(), reverse_map: DashMap::with_capacity(CACHE_INITIAL_CAPACITY) }
+    }
+
+    #[allow(clippy::cast_possible_truncation)]
+    pub fn get(&self, index: FormulaEncoding) -> &str {
+        assert!(index.is_large_cache(), "VariableCache does not optimize for small formulas!");
+        &self.vec[index.index() as usize]
+    }
+
+    pub fn get_or_insert(&self, element: Cow<'_, str>) -> FormulaEncoding {
+        // first a fast check whether the element is already there.
+        if let Some(v) = self.reverse_map.get(element.as_ref()) {
+            return *v;
+        }
+
+        // If we need to add the element, we have to check again if the element
+        // is there, but in a more expensive thread-safe way.
+        let name = element.into_owned();
+        *self.reverse_map.entry(name.clone()).or_insert_with(|| {
+            let index = self.vec.push(name);
+            FormulaEncoding::encode(index as u64, FormulaType::Lit(LitType::Pos(VarType::FF)), true)
+        })
+    }
+
+    pub fn lookup(&self, element: &str) -> Option<FormulaEncoding> {
+        self.reverse_map.get(element).map(|v| *v)
+    }
+
+    pub fn shrink_to_fit(&self) {
+        self.reverse_map.shrink_to_fit();
+    }
+
+    pub fn len(&self) -> usize {
+        debug_assert_eq!(self.vec.len(), self.reverse_map.len());
+        self.vec.len()
+    }
+}
+
+impl std::ops::Index<FormulaEncoding> for VariableCache {
+    type Output = str;
+
+    fn index(&self, index: FormulaEncoding) -> &Self::Output {
+        self.get(index)
+    }
+}

src/formulas/formula_factory.rs

@@ -5,7 +5,7 @@
 //! and commutativity) are hold exactly once in memory.
 
 
-use std::borrow::Borrow;
+use std::borrow::{Borrow, Cow};
 use std::collections::{HashMap, HashSet};
 use std::str::FromStr;
 use std::sync::atomic::{AtomicUsize, Ordering};
@@ -30,7 +30,8 @@ use super::formula_cache::formula_encoding::{Encoding, FormulaEncoding, SmallFor
 use super::formula_cache::implication_cache::ImplicationCache;
 use super::formula_cache::nary_formula_cache::NaryFormulaCache;
 use super::formula_cache::not_cache::NotCache;
-use super::{Formula, FormulaType, LitType, VarType};
+use super::formula_cache::var_cache::VariableCache;
+use super::{Formula, FormulaType};
 
 const FF_ID_LENGTH: i32 = 4;
 
@@ -225,7 +226,7 @@ pub struct FormulaFactory {
     pub(crate) id: String,
     /// Configuration
     pub config: FormulaFactoryConfig,
-    pub(crate) variables: SimpleCache<String>,
+    pub(crate) variables: VariableCache,
     pub(crate) ands: NaryFormulaCache,
     pub(crate) ors: NaryFormulaCache,
     pub(crate) nots: NotCache,
@@ -289,7 +290,7 @@ impl FormulaFactory {
         Self {
             id: id.into(),
             config: FormulaFactoryConfig::new(),
-            variables: SimpleCache::new(),
+            variables: VariableCache::new(),
             ands: NaryFormulaCache::new(FormulaType::And),
             ors: NaryFormulaCache::new(FormulaType::Or),
             nots: NotCache::new(),
@@ -443,7 +444,7 @@ impl FormulaFactory {
     ///
     /// assert_eq!(var.name(&f).into_owned(), "MyVar");
     /// ```
-    pub fn var(&self, name: &str) -> Variable {
+    pub fn var<'a, S: Into<Cow<'a, str>>>(&self, name: S) -> Variable {
         Variable::try_from(self.variable(name)).unwrap()
     }
 
@@ -474,8 +475,8 @@ impl FormulaFactory {
     /// assert_eq!(formula.to_string(&f), "MyVar");
     /// assert_eq!(formula, EncodedFormula::from(f.var("MyVar")));
     /// ```
-    pub fn variable(&self, name: &str) -> EncodedFormula {
-        EncodedFormula::from(self.variables.get_or_insert(name.into(), FormulaType::Lit(LitType::Pos(VarType::FF))))
+    pub fn variable<'a, S: Into<Cow<'a, str>>>(&self, name: S) -> EncodedFormula {
+        EncodedFormula::from(self.variables.get_or_insert(name.into()))
     }
 
     /// Creates a new variable with the given name and returns the variable as a

src/solver/tests/maxsat_tests.rs

@@ -141,7 +141,7 @@ mod pure_maxsat_tests {
         assert_eq!(model.pos.len(), 1);
         assert!(model.contains_pos(f.var("y")));
         assert_eq!(model.neg.len(), 7);
-        for n in &["a", "b", "c", "d", "e", "x", "z"] {
+        for n in ["a", "b", "c", "d", "e", "x", "z"] {
             assert!(model.contains_neg(f.var(n)));
         }
     }