Dev 0.17.1 (#224)

* README.md: about 'incremental_solver' configuration (#213)
* no_IO is incompatible with Splr executables (#223)

.github/workflows/rust.yml

@@ -9,7 +9,9 @@ jobs:
     - uses: actions/checkout@v1
     - name: Prepare
       run: rustup update
-    - name: Build
+    - name: Build executables
       run: cargo build --verbose
+    - name: Build library
+      run: cargo build --lib --verbose
     - name: Run tests
       run: cargo test --verbose

Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "splr"
-version = "0.17.0"
+version = "0.17.1-RC1"
 authors = ["Narazaki Shuji <shujinarazaki@protonmail.com>"]
 description = "A modern CDCL SAT solver in Rust"
 edition = "2021"
@@ -14,7 +14,7 @@ default-run = "splr"
 rust-version = "1.65"
 
 [dependencies]
-bitflags = "^1.3"
+bitflags = "^2.3"
 
 [features]
 default = [

ChangeLog.md

@@ -1,3 +1,7 @@
+## 0.17.1, 2023-07-xx
+
+- fix compilation errors with feature 'no_IO'
+
 ## 0.17.0, 2023-01-30
 
 - (Breaking change) `Certificate::try_from` returns `Ok` values even if a given vector

README.md

@@ -37,6 +37,13 @@ Two executables will be installed:
 
 Alternatively, Nix users can use `nix build`.
 
+### About `no_std` environment and feature `no_IO`
+
+If you want to build a library for `no_std` environment,
+or if you want to compile with feature `no_IO`,
+you have to run `cargo build --lib --features no_IO`.
+They are incompatible with `cargo install`.
+
 ## Usage
 
 Splr is a standalone program, taking a CNF file. The result will be saved to a file, which format is
@@ -223,7 +230,24 @@ fn main() {
 }
 ```
 
-### All solutions SAT solver
+### All solutions SAT solver as an application of 'incremental_solver' feature
+
+The following example requires 'incremental_solver' feature. You need the following dependeny:
+
+```toml
+splr = { version = "^0.17", features = ["incremental_solver"] }
+```
+Under this configuration, module `splr` provides some more functions:
+
+- `splr::Solver::reset(&mut self)`
+- `splr::Solver::add_var(&mut self)` // increments the last variable number
+- `splr::Solver::add_clause(&mut self, vec: AsRef<[i32]>) -> Result<&mut Solver, SolverError>`
+
+You have to call `reset` before calling `add_var`, `add_clause`, and `solve` again.
+By this, splr forgets everything about the previous formula, especially non-equivalent transformations by pre/inter-processors like clause subsumbtion.
+So technically splr is not an incremental solver.
+
+'add_clause' will emit an error if `vec` is invalid.
 
 ```rust
 use splr::*;
@@ -419,4 +443,4 @@ file, You can obtain one at http://mozilla.org/MPL/2.0/.
 
 ---
 
-2020-2022, Narazaki Shuji
+2020-2023, Narazaki Shuji

src/bin/dmcr.rs

@@ -1,4 +1,5 @@
-// DIMACS Model Checker in Rust
+#![cfg(not(feature = "no_IO"))]
+// A simple DIMACS Model Checker in Rust, which can't be compiled with feature 'no_IO'
 #![allow(unused_imports)]
 use {
     splr::{Config, SatSolverIF, Solver, ValidateIF},

src/bin/splr.rs

@@ -1,4 +1,5 @@
-// SAT solver for Propositional Logic in Rust
+#![cfg(not(feature = "no_IO"))]
+/// SAT solver for Propositional Logic in Rust, which can't be compiled with feature 'no_IO'
 use {
     splr::{
         assign, cdb,

src/cdb/unsat_certificate.rs

@@ -1,16 +1,37 @@
+use crate::types::*;
 #[cfg(not(feature = "no_IO"))]
-use {
-    crate::types::*,
-    std::{
-        fs::File,
-        io::{BufWriter, Write},
-        ops::Neg,
-        path::PathBuf,
-    },
+use std::{
+    fs::File,
+    io::{BufWriter, Write},
+    ops::Neg,
+    path::PathBuf,
 };
 
+#[cfg(feature = "no_IO")]
+#[derive(Debug, Default)]
+pub struct CertificationStore();
+
+#[cfg(feature = "no_IO")]
+impl Instantiate for CertificationStore {
+    fn instantiate(_config: &Config, _cnf: &CNFDescription) -> Self {
+        CertificationStore()
+    }
+}
+
+#[cfg(feature = "no_IO")]
+impl CertificationStore {
+    pub fn is_active(&self) -> bool {
+        false
+    }
+    pub fn add_clause(&mut self, _clause: &[Lit]) {}
+    pub fn delete_clause(&mut self, _vec: &[Lit]) {}
+    pub fn close(&mut self) {}
+}
+
+#[cfg(not(feature = "no_IO"))]
 const DUMP_INTERVAL: usize = 4096 * 16;
 
+#[cfg(not(feature = "no_IO"))]
 /// Struct for saving UNSAT certification
 #[derive(Debug, Default)]
 pub struct CertificationStore {
@@ -26,6 +47,7 @@ impl Clone for CertificationStore {
     }
 }
 
+#[cfg(not(feature = "no_IO"))]
 impl Instantiate for CertificationStore {
     fn instantiate(config: &Config, _cnf: &CNFDescription) -> Self {
         #[cfg(not(feature = "no_IO"))]
@@ -43,13 +65,11 @@ impl Instantiate for CertificationStore {
     }
 }
 
+#[cfg(not(feature = "no_IO"))]
 impl CertificationStore {
     pub fn is_active(&self) -> bool {
         self.buffer.is_some()
     }
-    #[cfg(feature = "no_IO")]
-    pub fn add_clause(&mut self, _clause: &[Lit]) {}
-    #[cfg(not(feature = "no_IO"))]
     pub fn add_clause(&mut self, clause: &[Lit]) {
         self.queue.push(clause.len() as i32);
         for l in clause.iter() {
@@ -59,9 +79,6 @@ impl CertificationStore {
             self.dump_to_file();
         }
     }
-    #[cfg(feature = "no_IO")]
-    pub fn delete_clause(&mut self, _vec: &[Lit]) {}
-    #[cfg(not(feature = "no_IO"))]
     pub fn delete_clause(&mut self, clause: &[Lit]) {
         self.queue.push((clause.len() as i32).neg());
         for l in clause.iter() {
@@ -71,9 +88,6 @@ impl CertificationStore {
             self.dump_to_file();
         }
     }
-    #[cfg(feature = "no_IO")]
-    pub fn close(&mut self) {}
-    #[cfg(not(feature = "no_IO"))]
     pub fn close(&mut self) {
         if self.buffer.is_none() {
             return;
@@ -87,6 +101,7 @@ impl CertificationStore {
     }
 }
 
+#[cfg(not(feature = "no_IO"))]
 impl CertificationStore {
     fn dump_to_file(&mut self) {
         let mut index = 0;

src/types.rs

@@ -398,22 +398,17 @@ impl fmt::Display for SolverError {
 pub type MaybeInconsistent = Result<(), SolverError>;
 
 /// CNF locator
-#[derive(Clone, Debug)]
+#[derive(Clone, Debug, Default)]
 pub enum CNFIndicator {
     /// not specified
+    #[default]
     Void,
     /// from a file
     File(String),
     /// embedded directly
     LitVec(usize),
 }
 
-impl Default for CNFIndicator {
-    fn default() -> Self {
-        CNFIndicator::Void
-    }
-}
-
 impl fmt::Display for CNFIndicator {
     fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
         match self {
@@ -570,6 +565,7 @@ pub trait FlagIF {
 
 bitflags! {
     /// Misc flags used by [`Clause`](`crate::cdb::Clause`).
+    #[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord)]
     pub struct FlagClause: u8 {
         /// a clause is a generated clause by conflict analysis and is removable.
         const LEARNT       = 0b0000_0001;
@@ -586,6 +582,7 @@ bitflags! {
 
 bitflags! {
     /// Misc flags used by [`Var`](`crate::assign::Var`).
+    #[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord)]
     pub struct FlagVar: u8 {
         /// * the previous assigned value of a Var.
         const PHASE        = 0b0000_0001;