Dev 0.19

Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "splr"
-version = "0.17.3"
+version = "0.19.0-dev0"
 authors = ["Narazaki Shuji <[email protected]>"]
 description = "A modern CDCL SAT solver in Rust"
 edition = "2021"
@@ -11,7 +11,7 @@ homepage = "https://github.com/shnarazk/splr"
 keywords = ["SAT", "SAT-solver", "logic", "satisfiability"]
 categories = ["science", "mathematics"]
 default-run = "splr"
-rust-version = "1.65"
+rust-version = "1.84"
 
 [dependencies]
 bitflags = "^2.4"

flake.nix

@@ -1,6 +1,6 @@
 {
   description = "A modern SAT solver in Rust";
-  inputs.nixpkgs.url = github:NixOS/nixpkgs;
+  inputs.nixpkgs.url = "github:NixOS/nixpkgs";
   outputs = { self, nixpkgs }:
   {
     packages = builtins.listToAttrs

src/assign/mod.rs

@@ -1,5 +1,5 @@
-/// Module `assign` implements Boolean Constraint Propagation and decision var selection.
-/// This version can handle Chronological and Non Chronological Backtrack.
+// Module `assign` implements Boolean Constraint Propagation and decision var selection.
+// This version can handle Chronological and Non Chronological Backtrack.
 
 /// Ema
 mod ema;

src/assign/propagate.rs

@@ -765,7 +765,7 @@ impl AssignStack {
         assert_ne!(self.assigned(b0), Some(false));
         assert_ne!(self.assigned(b1), Some(false));
     }
-    ///
+    /// a specialized `propagate` to clean up the stack
     fn propagate_at_root_level(&mut self, cdb: &mut impl ClauseDBIF) -> MaybeInconsistent {
         let mut num_propagated = 0;
         while num_propagated < self.trail.len() {

src/assign/select.rs

@@ -1,4 +1,4 @@
-/// Decision var selection
+// Decision var selection
 
 #[cfg(feature = "rephase")]
 use super::property;

src/cdb/clause.rs

@@ -2,11 +2,49 @@ use {
     crate::{assign::AssignIF, types::*},
     std::{
         fmt,
+        num::NonZeroU32,
         ops::{Index, IndexMut, Range, RangeFrom},
         slice::Iter,
     },
 };
 
+/// Clause identifier, or clause index, starting with one.
+/// Note: ids are re-used after 'garbage collection'.
+#[derive(Clone, Copy, Eq, Hash, Ord, PartialEq, PartialOrd)]
+pub struct ClauseId {
+    /// a sequence number.
+    pub ordinal: NonZeroU32,
+}
+
+/// A representation of 'clause'
+#[derive(Clone, Debug, Eq, PartialEq, PartialOrd)]
+pub struct Clause {
+    /// The literals in a clause.
+    pub(super) lits: Vec<Lit>,
+    /// Flags (8 bits)
+    pub(crate) flags: FlagClause,
+    /// A static clause evaluation criterion like LBD, NDD, or something.
+    pub rank: u16,
+    /// A record of the rank at previos stage.
+    pub rank_old: u16,
+    /// the index from which `propagate` starts searching an un-falsified literal.
+    /// Since it's just a hint, we don't need u32 or usize.
+    pub(crate) search_from: u16,
+
+    #[cfg(any(feature = "boundary_check", feature = "clause_rewarding"))]
+    /// the number of conflicts at which this clause was used in `conflict_analyze`
+    timestamp: usize,
+
+    #[cfg(feature = "clause_rewarding")]
+    /// A dynamic clause evaluation criterion based on the number of references.
+    reward: f64,
+
+    #[cfg(feature = "boundary_check")]
+    pub birth: usize,
+    #[cfg(feature = "boundary_check")]
+    pub moved_at: Propagate,
+}
+
 impl Default for Clause {
     fn default() -> Clause {
         Clause {
@@ -257,4 +295,7 @@ impl Clause {
         self.rank = cnt;
         cnt as usize
     }
+    pub fn reverse_activity_sum(&self, asg: &impl AssignIF) -> f64 {
+        self.iter().map(|l| 1.0 - asg.activity(l.vi())).sum()
+    }
 }