new file: src/types/bsvr.rs

src/types/bsvr.rs

@@ -0,0 +1,40 @@
+//! Bounded static Var ref
+
+use crate::{types::*, var_vector::*};
+
+/// Bounded Static Var Ref
+pub struct BSVR {
+    pub var: &'static Var,
+    pub vi: VarId,
+    pub possitive: bool,
+}
+
+impl Default for BSVR {
+    fn default() -> Self {
+        BSVR {
+            var: VarRef(0).get_reference(),
+            vi: 0,
+            possitive: true,
+        }
+    }
+}
+
+impl BSVR {
+    pub fn new(vi: VarId, possitive: bool) -> Self {
+        BSVR {
+            var: VarRef(vi).get_reference(),
+            vi,
+            possitive,
+        }
+    }
+    #[inline]
+    pub fn lit_assigned(&self) -> Option<bool> {
+        match self.var.assign {
+            Some(b) if !self.possitive => Some(!b),
+            ob => ob,
+        }
+    }
+    pub fn as_lit(&self) -> Lit {
+        Lit::from((self.vi, self.possitive))
+    }
+}

src/types/mod.rs

@@ -1,6 +1,8 @@
 //! Module `types' provides various building blocks, including
 //! some common traits.
 
+/// Bounded static Var ref
+pub mod bsvr;
 /// methods on clause
 pub mod clause;
 /// methods on CNF file

src/var_vector.rs

@@ -4,6 +4,7 @@ use crate::{types::*, vam::VarActivityManager};
 pub static mut VAR_VECTOR: Vec<Var> = Vec::new();
 
 pub trait VarRefIF {
+    fn get_reference(&self) -> &'static Var;
     fn assign(&self) -> Option<bool>;
     fn set_assign(&self, value: Option<bool>);
     fn level(&self) -> DecisionLevel;
@@ -109,6 +110,9 @@ impl VarRef {
 }
 
 impl VarRefIF for VarRef {
+    fn get_reference(&self) -> &'static Var {
+        unsafe { &VAR_VECTOR.get_unchecked(self.0) }
+    }
     #[inline]
     fn assign(&self) -> Option<bool> {
         unsafe { VAR_VECTOR.get_unchecked(self.0).assign }