A broken snapshot

src/assign/mod.rs

@@ -88,14 +88,14 @@ pub trait AssignIF:
 }
 
 /// Reasons of assignments
-#[derive(Clone, Copy, Debug, Eq, Ord, PartialEq, PartialOrd)]
+#[derive(Clone, Debug, Eq, Ord, PartialEq, PartialOrd)]
 pub enum AssignReason {
     /// Implication by binary clause
     BinaryLink(Lit),
     /// Assigned by decision
     Decision(DecisionLevel),
     /// Assigned by a non-binary clause.
-    Implication(ClauseId),
+    Implication(ClauseRef),
     /// None of the above.
     None,
 }

src/assign/propagate.rs

@@ -715,7 +715,7 @@ impl AssignStack {
         while num_propagated < self.trail.len() {
             num_propagated = self.trail.len();
             for ci in 1..cdb.len() {
-                let cid = ClauseId::from(ci);
+                let cid = ClauseRef::from(ci);
                 if cdb[cid].is_dead() {
                     continue;
                 }

src/cdb/activity.rs

@@ -1,18 +1,18 @@
 #![cfg(feature = "clause_rewarding")]
-use {super::ClauseId, crate::types::*, std::num::NonZeroU32};
+use {super::ClauseRef, crate::types::*, std::num::NonZeroU32};
 
 /// clause activity
 /// Note: vivifier has its own conflict analyzer, which never call reward functions.
 
-impl ActivityIF<ClauseId> for ClauseDB {
-    fn activity(&self, _cid: ClauseId) -> f64 {
+impl ActivityIF<ClauseRef> for ClauseDB {
+    fn activity(&self, _cid: ClauseRef) -> f64 {
         unreachable!()
     }
-    fn set_activity(&mut self, cid: ClauseId, val: f64) {
+    fn set_activity(&mut self, cid: ClauseRef, val: f64) {
         self[cid].reward = val;
     }
     #[inline]
-    fn reward_at_analysis(&mut self, cid: ClauseId) {
+    fn reward_at_analysis(&mut self, cid: ClauseRef) {
         self.clause[NonZeroU32::get(cid.ordinal) as usize].update_activity(
             self.tick,
             self.activity_decay,

src/cdb/binary.rs

@@ -7,7 +7,7 @@ use {
 };
 
 /// storage of binary links
-pub type BinaryLinkList = Vec<(Lit, ClauseId)>;
+pub type BinaryLinkList = Vec<(Lit, ClauseRef)>;
 
 impl Index<Lit> for Vec<BinaryLinkList> {
     type Output = BinaryLinkList;
@@ -34,10 +34,10 @@ impl IndexMut<Lit> for Vec<BinaryLinkList> {
     }
 }
 
-/// storage with mapper to `ClauseId` of binary links
+/// storage with mapper to `ClauseRef` of binary links
 #[derive(Clone, Debug, Default)]
 pub struct BinaryLinkDB {
-    hash: HashMap<(Lit, Lit), ClauseId>,
+    hash: HashMap<(Lit, Lit), ClauseRef>,
     list: Vec<BinaryLinkList>,
 }
 
@@ -53,12 +53,12 @@ impl Instantiate for BinaryLinkDB {
 }
 
 pub trait BinaryLinkIF {
-    /// add a mapping from a pair of Lit to a `ClauseId`
-    fn add(&mut self, lit0: Lit, lit1: Lit, cid: ClauseId);
+    /// add a mapping from a pair of Lit to a `ClauseRef`
+    fn add(&mut self, lit0: Lit, lit1: Lit, cid: ClauseRef);
     /// remove a pair of `Lit`s
     fn remove(&mut self, lit0: Lit, lit1: Lit) -> MaybeInconsistent;
-    /// return 'ClauseId` linked from a pair of `Lit`s
-    fn search(&self, lit0: Lit, lit1: Lit) -> Option<&ClauseId>;
+    /// return 'ClauseRef` linked from a pair of `Lit`s
+    fn search(&self, lit0: Lit, lit1: Lit) -> Option<&ClauseRef>;
     /// return the all links that include `Lit`.
     /// Note this is not a `watch_list`. The other literal has an opposite phase.
     fn connect_with(&self, lit: Lit) -> &BinaryLinkList;
@@ -69,7 +69,7 @@ pub trait BinaryLinkIF {
 }
 
 impl BinaryLinkIF for BinaryLinkDB {
-    fn add(&mut self, lit0: Lit, lit1: Lit, cid: ClauseId) {
+    fn add(&mut self, lit0: Lit, lit1: Lit, cid: ClauseRef) {
         let l0 = lit0.min(lit1);
         let l1 = lit0.max(lit1);
         self.hash.insert((l0, l1), cid);
@@ -84,7 +84,7 @@ impl BinaryLinkIF for BinaryLinkDB {
         self.list[lit1].delete_unstable(|p| p.0 == lit0);
         Ok(())
     }
-    fn search(&self, lit0: Lit, lit1: Lit) -> Option<&ClauseId> {
+    fn search(&self, lit0: Lit, lit1: Lit) -> Option<&ClauseRef> {
         let l0 = lit0.min(lit1);
         let l1 = lit0.max(lit1);
         self.hash.get(&(l0, l1))

src/cdb/cid.rs

@@ -1,53 +1,53 @@
 use {
-    super::ClauseId,
+    super::ClauseRef,
     std::{fmt, num::NonZeroU32},
 };
 
 /// API for Clause Id.
-pub trait ClauseIdIF {
+pub trait ClauseRefIF {
     /// return `true` if a given clause id is made from a `Lit`.
     fn is_lifted_lit(&self) -> bool;
 }
 
-impl Default for ClauseId {
+impl Default for ClauseRef {
     #[inline]
     /// return the default empty clause, used in a reason slot or no conflict path.
     fn default() -> Self {
-        ClauseId {
+        ClauseRef {
             ordinal: unsafe { NonZeroU32::new_unchecked(0x7FFF_FFFF) },
         }
     }
 }
 
-impl From<usize> for ClauseId {
+impl From<usize> for ClauseRef {
     #[inline]
-    fn from(u: usize) -> ClauseId {
-        ClauseId {
+    fn from(u: usize) -> ClauseRef {
+        ClauseRef {
             ordinal: unsafe { NonZeroU32::new_unchecked(u as u32) },
         }
     }
 }
 
-impl From<ClauseId> for usize {
+impl From<ClauseRef> for usize {
     #[inline]
-    fn from(cid: ClauseId) -> usize {
+    fn from(cid: ClauseRef) -> usize {
         NonZeroU32::get(cid.ordinal) as usize
     }
 }
 
-impl fmt::Debug for ClauseId {
+impl fmt::Debug for ClauseRef {
     fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
         write!(f, "{}C", self.ordinal)
     }
 }
 
-impl fmt::Display for ClauseId {
+impl fmt::Display for ClauseRef {
     fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
         write!(f, "{}C", self.ordinal)
     }
 }
 
-impl ClauseIdIF for ClauseId {
+impl ClauseRefIF for ClauseRef {
     /// return `true` if the clause is generated from a literal by Eliminator.
     fn is_lifted_lit(&self) -> bool {
         0 != 0x8000_0000 & NonZeroU32::get(self.ordinal)