improved doc + code quality

Cargo.toml

@@ -1,11 +1,26 @@
 [package]
 name = "pblib-rs"
+authors = ["Emmanuel Lonca <[email protected]>"]
+license = "LGPL-3.0-or-later"
 version = "0.1.0"
+description = "Rust safe bindings for pblib"
+categories = ["api-bindings", "encoding", "mathematics", "science"]
+keywords = ["cardinality", "PB", "constraints", "encoding", "SAT"]
+repository = "https://github.com/crillab/pblib-rs"
 edition = "2021"
 build = "build.rs"
 links = "libcpblib.a"
 
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 
+[lints.rust]
+missing_docs = "warn"
+
+[lints.clippy]
+pedantic = "warn"
+
 [build-dependencies]
 cc = { version = "1.0", features = ["parallel"] }
+
+[dev-dependencies]
+splr = { version = "0.17.1", features = ["incremental_solver"] }

README.md

@@ -2,7 +2,47 @@
 
 Rust safe bindings for pblib.
 
+The source code of pblib is taken from the fork maintained by Radomír Černoch [on Github](https://github.com/master-keying/pblib).
+This crate currently provides bindings to a partial set of the initial library functions.
+See the original documentation (that can be retrieved from the fork's README page) if you need more information on the encodings.
+
+The entry point of the API is the `PB2CNF` structure.
+You should begin by taking a look at its documentation is you want to use pblib-rs.
+
+## TL;DR
+
+Cardinality constraints:
+
+```rust
+use pblib_rs::PB2CNF;
+
+// we encode x1 + x2 + x3 >= 2
+let literals = vec![1, 2, 3];
+let pb2cnf = PB2CNF::new();
+// the threshold is 2 and the first variable not in use is 4
+let encoding = pb2cnf.encode_at_least_k(literals, 2, 4);
+println!("the encoding uses {} variables", encoding.next_free_var_id() - 4);
+println!("the encoding uses {} clauses", encoding.clauses().len());
+encoding.clauses().iter().enumerate().for_each(|(i,c)| println!("clause {i} is {:?}", c));
+```
+
+Pseudo-Boolean constraints:
+
+```rust
+use pblib_rs::PB2CNF;
+
+// we encode 8*x1 + 4*x2 + 2*x3 + 1*x4 >= 6
+let weights = vec![8, 4, 2, 1];
+let literals = vec![1, 2, 3, 4];
+let pb2cnf = PB2CNF::new();
+// the threshold is 6 and the first variable not in use is 5
+let encoding = pb2cnf.encode_geq(weights.clone(), literals, 6, 5);
+println!("the encoding uses {} variables", encoding.next_free_var_id() - 4);
+println!("the encoding uses {} clauses", encoding.clauses().len());
+encoding.clauses().iter().enumerate().for_each(|(i,c)| println!("clause {i} is {:?}", c));
+```
+
 ## License
 
 pblib-rs is developed at CRIL (Univ. Artois & CNRS).
-It is made available under the terms of the GNU GPLv3 license.
+It is made available under the terms of the GNU Lesser GPLv3 license.

build.rs

@@ -1,3 +1,7 @@
+//! # pblib-rs
+//!
+//! Rust safe bindings for pblib.
+
 use cc::Build;
 
 const PBLIB_DIR: &str = "pblib";
@@ -55,11 +59,11 @@ where
         .extra_warnings(true)
         .opt_level(3)
         .define("NDEBUG", "1");
-    flags.iter().for_each(|f| {
+    for f in flags {
         build.flag_if_supported(f);
-    });
-    build.includes(includes.iter().map(|i| i.as_ref()));
-    build.files(files.iter().map(|f| f.as_ref()));
+    }
+    build.includes(includes.iter().map(AsRef::as_ref));
+    build.files(files.iter().map(AsRef::as_ref));
     println!("cargo:rerun-if-changed=build.rs");
     build.compile(output);
 }
@@ -72,7 +76,7 @@ fn main() {
         &[MINISAT_DIR],
         MINISAT_FILES
             .iter()
-            .map(|f| format!("{}/{}", MINISAT_DIR, f))
+            .map(|f| format!("{MINISAT_DIR}/{f}"))
             .collect::<Vec<String>>()
             .as_slice(),
         "libminisat.a",
@@ -90,7 +94,7 @@ fn main() {
         &[PBLIB_DIR, MINISAT_DIR],
         PBLIB_FILES
             .iter()
-            .map(|f| format!("{}/{}", PBLIB_DIR, f))
+            .map(|f| format!("{PBLIB_DIR}/{f}"))
             .collect::<Vec<String>>()
             .as_slice(),
         "libpb.a",
@@ -101,5 +105,5 @@ fn main() {
         &[PBLIB_DIR],
         &["src/cpblib.cc"],
         "libcpblib.a",
-    )
+    );
 }

src/cpblib.rs

@@ -1,28 +1,107 @@
 use std::ffi::c_void;
 
+/// The entry point for the Rust bindings.
+///
+/// This structure is a wrapper around the underlying C structure that provides a safe interface to the pblib functions.
+/// It gives access to the functions dedicated to the encoding of cardinality and Pseudo-Boolean constraints.
+///
+/// # Encoding cardinality constraints
+///
+/// Cardinality constraints are encoded thanks to the [`encode_at_least_k`](Self::encode_at_least_k) and [`encode_at_most_k`](Self::encode_at_most_k) functions.
+/// They take as input the list of literals (in the DIMACS format) the constraints relies on, the bound, and the minimal variable index that can be used as an auxiliary variables must be given to the function.
+/// Auxiliary variables are often used in such encodings since they allow to use less clauses to encode the constraint.
+/// The preferred value for this parameter is in most cases the highest variable index in use plus 1.
+///
+/// The result of this function is an [`EncodingResult`] which gives both the clauses encoding the constraint (as a vector of DIMACS-encoded literals) and the new lowest variable index that is not in use.
+///
+/// ```
+/// use pblib_rs::PB2CNF;
+///
+/// // we encode x1 + x2 + x3 >= 2
+/// let literals = vec![1, 2, 3];
+/// let pb2cnf = PB2CNF::new();
+/// // the threshold is 2 and the first variable not in use is 4
+/// let encoding = pb2cnf.encode_at_least_k(literals, 2, 4);
+/// println!("the encoding uses {} variables", encoding.next_free_var_id() - 4);
+/// println!("the encoding uses {} clauses", encoding.clauses().len());
+/// encoding.clauses().iter().enumerate().for_each(|(i,c)| println!("clause {i} is {:?}", c));
+/// ```
+///
+/// # Encoding Pseudo-Boolean constraints
+///
+/// The difference between cardinality and Pseudo-Boolean constraints is than weights are applied to literals.
+/// Thus, the functions dedicated to this kind of constraints ([`encode_geq`](Self::encode_geq), [`encode_leq`](Self::encode_leq) and [`encode_both`](Self::encode_both)) takes a vector of weights as a supplementary parameter.
+/// The vectors of weights and literals must be of same lengths, since variable at index `i` has the weight at index `i`.
+///
+/// ```
+/// use pblib_rs::PB2CNF;
+///
+/// // we encode 8*x1 + 4*x2 + 2*x3 + 1*x4 >= 6
+/// let weights = vec![8, 4, 2, 1];
+/// let literals = vec![1, 2, 3, 4];
+/// let pb2cnf = PB2CNF::new();
+/// // the threshold is 6 and the first variable not in use is 5
+/// let encoding = pb2cnf.encode_geq(weights.clone(), literals, 6, 5);
+/// println!("the encoding uses {} variables", encoding.next_free_var_id() - 4);
+/// println!("the encoding uses {} clauses", encoding.clauses().len());
+/// encoding.clauses().iter().enumerate().for_each(|(i,c)| println!("clause {i} is {:?}", c));
+/// ```
+///
+/// # Note about the encodings
+///
+/// Contrary to pblib, pblib-rs does not allow the user to choose the encoding use for the constraint.
+/// The encoding used for the constraints are the default ones of the pblib.
+/// In particular, the encodings provided by this library are not intended to match the expected model count of the formula.
 #[repr(C)]
 pub struct PB2CNF(*mut c_void);
 
+/// The result of an encoding function.
+///
+/// This structure contains both the clauses generated to encode the constraint and the index of the next free variable id.
 pub struct EncodingResult {
     clauses: Vec<Vec<i32>>,
     next_free_var_id: i32,
 }
 
 impl EncodingResult {
+    /// Returns a reference to the clauses used to encode the constraint.
+    #[must_use]
     pub fn clauses(&self) -> &[Vec<i32>] {
         &self.clauses
     }
 
+    /// Returns the next free variable id.
+    ///
+    /// Encodings use auxiliary variables almost all the time.
+    /// Functions that encode constraints ask the first variable id they can use for these auxiliary variables.
+    /// In return, they tell the caller which is the lowest id that can be used after this encoding, that is, the highest auxiliary variable index plus 1.
+    #[must_use]
     pub fn next_free_var_id(&self) -> i32 {
         self.next_free_var_id
     }
 }
 
 impl PB2CNF {
+    /// Builds a new structure dedicated to the encoding of constraints.
+    #[must_use]
     pub fn new() -> Self {
         Self(unsafe { newPB2CNF() })
     }
 
+    /// Encodes an At-Most-k Pseudo-Boolean constraint.
+    ///
+    /// An At-Most-k constraint imposes that a weighted sum of literals is less than or equal to an integer value.
+    /// The vectors of weights and literals must be of same lengths, since variable at index `i` has the weight at index `i`.
+    ///
+    /// In addition to this vectors and the threshold, the minimal variable index that can be used as an auxiliary variables must be given to the function.
+    /// The preferred value for this parameter is in most cases the highest variable index in use plus 1.
+    ///
+    /// The result of this function is an [`EncodingResult`] which gives both the clauses encoding the constraint and the new lowest variable index that is not in use.
+    ///
+    /// # Panics
+    ///
+    /// In case the weights and literal vectors have not the same length, this function panics.
+    #[must_use]
     pub fn encode_leq(
         &self,
         weights: Vec<i64>,
@@ -43,10 +122,24 @@ impl PB2CNF {
             )
         };
         let result = decode_formula_data(formula_ptr);
-        unsafe { freePtr(formula_ptr as *mut _) };
+        unsafe { freePtr(formula_ptr.cast()) };
         result
     }
 
+    /// Encodes an At-Least-k Pseudo-Boolean constraint.
+    ///
+    /// An At-Least-k constraint imposes that a weighted sum of literals is greater than or equal to an integer value.
+    /// The vectors of weights and literals must be of same lengths, since variable at index `i` has the weight at index `i`.
+    ///
+    /// In addition to this vectors and the threshold, the minimal variable index that can be used as an auxiliary variables must be given to the function.
+    /// The preferred value for this parameter is in most cases the highest variable index in use plus 1.
+    ///
+    /// The result of this function is an [`EncodingResult`] which gives both the clauses encoding the constraint and the new lowest variable index that is not in use.
+    ///
+    /// # Panics
+    ///
+    /// In case the weights and literal vectors have not the same length, this function panics.
+    #[must_use]
     pub fn encode_geq(
         &self,
         weights: Vec<i64>,
@@ -67,16 +160,25 @@ impl PB2CNF {
             )
         };
         let result = decode_formula_data(formula_ptr);
-        unsafe { freePtr(formula_ptr as *mut _) };
+        unsafe { freePtr(formula_ptr.cast()) };
         result
     }
 
+    /// Encodes both an At-Most-k and an At-Least-p Pseudo-Boolean constraints that refers to the same variables and weights.
+    ///
+    /// See [`encode_leq`](Self::encode_leq) and [`encode_geq`](Self::encode_geq) for more information on At-Most-k and At-Least-p constraints, the `first_aux_var` parameter and the return type.
+    /// A call to this function is intended to be more efficient in terms of encoding comparing to a call to [`encode_leq`](Self::encode_leq) and a call to [`encode_geq`](Self::encode_geq).
+    ///
+    /// # Panics
+    ///
+    /// In case the weights and literal vectors have not the same length, this function panics.
+    #[must_use]
     pub fn encode_both(
         &self,
         weights: Vec<i64>,
         literals: Vec<i32>,
-        leq: i64,
-        geq: i64,
+        less_or_eq: i64,
+        greater_or_eq: i64,
         first_aux_var: i32,
     ) -> EncodingResult {
         assert_len_eq(&weights, &literals);
@@ -87,16 +189,26 @@ impl PB2CNF {
                 weights.len().try_into().unwrap(),
                 literals.as_ptr(),
                 literals.len().try_into().unwrap(),
-                leq,
-                geq,
+                less_or_eq,
+                greater_or_eq,
                 first_aux_var,
             )
         };
         let result = decode_formula_data(formula_ptr);
-        unsafe { freePtr(formula_ptr as *mut _) };
+        unsafe { freePtr(formula_ptr.cast()) };
         result
     }
 
+    /// Encodes an At-Most-k cardinality constraint.
+    ///
+    /// An At-Most-k cardinality constraint imposes that at most k literals in a vector are set to true.
+    ///
+    /// In addition to this vector and the threshold, the minimal variable index that can be used as an auxiliary variables must be given to the function.
+    /// The preferred value for this parameter is in most cases the highest variable index in use plus 1.
+    ///
+    /// The result of this function is an [`EncodingResult`] which gives both the clauses encoding the constraint and the new lowest variable index that is not in use.
+    #[must_use]
+    #[allow(clippy::missing_panics_doc)]
     pub fn encode_at_most_k(
         &self,
         literals: Vec<i32>,
@@ -113,10 +225,20 @@ impl PB2CNF {
             )
         };
         let result = decode_formula_data(formula_ptr);
-        unsafe { freePtr(formula_ptr as *mut _) };
+        unsafe { freePtr(formula_ptr.cast()) };
         result
     }
 
+    /// Encodes an At-Least-k cardinality constraint.
+    ///
+    /// An At-Least-k cardinality constraint imposes that at least k literals in a vector are set to true.
+    ///
+    /// In addition to this vector and the threshold, the minimal variable index that can be used as an auxiliary variables must be given to the function.
+    /// The preferred value for this parameter is in most cases the highest variable index in use plus 1.
+    ///
+    /// The result of this function is an [`EncodingResult`] which gives both the clauses encoding the constraint and the new lowest variable index that is not in use.
+    #[must_use]
+    #[allow(clippy::missing_panics_doc)]
     pub fn encode_at_least_k(
         &self,
         literals: Vec<i32>,
@@ -133,21 +255,22 @@ impl PB2CNF {
             )
         };
         let result = decode_formula_data(formula_ptr);
-        unsafe { freePtr(formula_ptr as *mut _) };
+        unsafe { freePtr(formula_ptr.cast()) };
         result
     }
 }
 
 fn decode_formula_data(formula_ptr: *mut i32) -> EncodingResult {
-    let data_len = unsafe { std::slice::from_raw_parts(formula_ptr, 1) }[0] as usize;
+    let data_len =
+        usize::try_from(unsafe { std::slice::from_raw_parts(formula_ptr, 1) }[0]).unwrap();
     let data = unsafe { std::slice::from_raw_parts(formula_ptr, data_len) };
     let next_free_var_id = data[1];
-    let mut clauses = Vec::with_capacity(data[0] as usize);
+    let mut clauses = Vec::with_capacity(usize::try_from(data[0]).unwrap());
     let mut i = 2;
     while i < data_len {
-        let len = data[i] as usize;
+        let len = usize::try_from(data[i]).unwrap();
         clauses.push(data[i + 1..i + 1 + len].into());
-        i += len + 1
+        i += len + 1;
     }
     EncodingResult {
         clauses,
@@ -156,13 +279,13 @@ fn decode_formula_data(formula_ptr: *mut i32) -> EncodingResult {
 }
 
 fn assert_len_eq(weights: &[i64], literals: &[i32]) {
-    if weights.len() != literals.len() {
-        panic!(
-            "weights len ({}) and literals len ({}) must be equal",
-            weights.len(),
-            literals.len()
-        );
-    }
+    assert_eq!(
+        weights.len(),
+        literals.len(),
+        "weights len ({}) and literals len ({}) must be equal",
+        weights.len(),
+        literals.len()
+    );
 }
 
 impl Default for PB2CNF {
@@ -298,7 +421,7 @@ mod tests {
         let weights = vec![1];
         let literals = vec![1, 2];
         let pb2cnf = PB2CNF::new();
-        pb2cnf.encode_leq(weights, literals, 1, 3);
+        let _ = pb2cnf.encode_leq(weights, literals, 1, 3);
     }
 
     fn check_models(