Improved doc; conversion between Lut7 and u128; cleanup rustsat use; bump version number

Author: Coloquinte

Cargo.toml

@@ -1,12 +1,12 @@
 [package]
 name = "volute"
-version = "1.1.5"
+version = "1.1.6"
 edition = "2021"
 
 authors = ["Gabriel Gouvine <[email protected]>"]
 description = "Boolean functions implementation, represented as lookup tables (LUT) or sum-of-products (SOP)"
 license = "MIT OR Apache-2.0"
-keywords = ["boolean", "logic", "LUT", "lookup-table", "truth-table"]
+keywords = ["boolean-logic", "lookup-table", "truth-table"]
 repository = "https://github.com/Coloquinte/volute"
 homepage = "https://github.com/Coloquinte/volute"
 categories = ["mathematics", "algorithms"]

README.md

@@ -4,7 +4,7 @@
 
 <!-- cargo-rdme start -->
 
-Logic function manipulation using truth tables (LUTs) that represent the
+Logic function manipulation using truth tables (or lookup tables, `Luts`) that represent the
 value of the function for the 2<sup>n</sup> possible inputs.
 
 The crate implements optimized truth table datastructures, either arbitrary-size truth tables
@@ -19,32 +19,35 @@ API and documentation try to follow the same terminology as the C++ library
 
 # Examples
 
-Create a constant-one Lut with five variables.
-Check its hexadecimal value.
+Create a constant-one Lut with five variables and a constant-zero Lut with 4 variables.
 ```rust
-let lut = Lut::one(5);
-assert_eq!(lut.to_string(), "Lut5(ffffffff)");
+let lut5 = Lut::one(5);
+let lut4 = Lut::zero(4);
 ```
 
-Create a Lut4 (four variables) which is the logical and of the 1st and 3rd.
-Check its hexadecimal value.
+Create a Lut2 representing the first variable. Swap its inputs. Check the result.
+```rust
+let lut = Lut2::nth_var(0);
+assert_eq!(lut.swap(0, 1), Lut2::nth_var(1));
+```
+
+Perform the logical and between two Lut4. Check its hexadecimal value.
 ```rust
 let lut = Lut4::nth_var(0) & Lut4::nth_var(2);
 assert_eq!(lut.to_string(), "Lut4(a0a0)");
 ```
 
-Create a Lut6 (six variables) from its hexadecimal value
-Display its hexadecimal value.
+Create a Lut6 (6 variables) from its hexadecimal value. Display it.
 ```rust
 let lut = Lut6::from_hex_string("0123456789abcdef").unwrap();
 print!("{lut}");
 ```
 
-Create a random Lut6 (six variables).
-Display its hexadecimal value.
+Small Luts (3 to 7 variables) can be converted to the integer type of the same size.
 ```rust
-let lut = Lut6::random();
-print!("{lut}");
+let lut5: u32 = Lut5::random().into();
+let lut6: u64 = Lut6::random().into();
+let lut7: u128 = Lut7::random().into();
 ```
 
 Create the parity function on three variables, and check that in can be decomposed as a Xor.
@@ -55,32 +58,37 @@ assert_eq!(lut.top_decomposition(0), DecompositionType::Xor);
 assert_eq!(format!("{lut:b}"), "Lut3(10010110)");
 ```
 
-Create a Lut2 and swap its inputs.
-Check the result.
-```rust
-let lut = Lut2::nth_var(0);
-assert_eq!(lut.swap(0, 1), Lut2::nth_var(1));
-```
-
 ## Sum of products and Exclusive sum of products
 
 Volute provides Sum-of-Products (SOP) and Exclusive Sum-of-Products (ESOP)
-representations, including exact decomposition methods using a MILP solver
-or a SAT solver.
+representations.
+
+Create Sum of products and perform operations on them.
+```rust
+let var4 = Sop::nth_var(10, 4);
+let var2 = Sop::nth_var(10, 2);
+let var_and = var4 & var2;
+```
+
+Exact decomposition methods can be used with the features `optim-mip`  (using a MILP solver)
+or `optim-sat` (using a SAT solver).
 
  ```rust
-let lut = Lut::parity(6);
-let sop = sop::optim::optimize_esop_mip(&[lut], 1, 2);
+let lut = Lut::threshold(6, 5);
+let esop = sop::optim::optimize_esop_mip(&[lut], 1, 2);
 ```
 
 ## Canonical representation
 
-For boolean optimization, Luts can be represented by a canonical
-representation, that is identical up to variable complementation (N),
-input permutation (P), or both (NPN).
+For boolean optimization, Luts have several canonical forms that allow to only store
+optimizations for a small subset of Luts.
+Methods are available to find the smallest Lut that is identical up to variable
+complementation (N), input permutation (P), or both (NPN).
 
- ```rust
-let lut = Lut6::parity();
+```rust
+let lut = Lut4::threshold(3);
+let (canonical, flips) = lut.n_canonization();
+let (canonical, perm) = lut.p_canonization();
 let (canonical, perm, flips) = lut.npn_canonization();
 ```
 

src/lib.rs

@@ -1,7 +1,7 @@
 #![warn(missing_docs)]
 #![cfg_attr(docsrs, feature(doc_cfg))]
 
-//! Logic function manipulation using truth tables (LUTs) that represent the
+//! Logic function manipulation using truth tables (or lookup tables, `Luts`) that represent the
 //! value of the function for the 2<sup>n</sup> possible inputs.
 //!
 //! The crate implements optimized truth table datastructures, either arbitrary-size truth tables
@@ -16,39 +16,46 @@
 //!
 //! # Examples
 //!
-//! Create a constant-one Lut with five variables.
-//! Check its hexadecimal value.
+//! Create a constant-one Lut with five variables and a constant-zero Lut with 4 variables.
 //! ```
 //! # use volute::Lut;
-//! let lut = Lut::one(5);
-//! assert_eq!(lut.to_string(), "Lut5(ffffffff)");
+//! let lut5 = Lut::one(5);
+//! let lut4 = Lut::zero(4);
 //! ```
 //!
-//! Create a Lut4 (four variables) which is the logical and of the 1st and 3rd.
-//! Check its hexadecimal value.
+//! Create a Lut2 representing the first variable. Swap its inputs. Check the result.
+//! ```
+//! # use volute::Lut2;
+//! let lut = Lut2::nth_var(0);
+//! assert_eq!(lut.swap(0, 1), Lut2::nth_var(1));
+//! ```
+//!
+//! Perform the logical and between two Lut4. Check its hexadecimal value.
 //! ```
 //! # use volute::Lut4;
 //! let lut = Lut4::nth_var(0) & Lut4::nth_var(2);
 //! assert_eq!(lut.to_string(), "Lut4(a0a0)");
 //! ```
 //!
-//! Create a Lut6 (six variables) from its hexadecimal value
-//! Display its hexadecimal value.
+//! Create a Lut6 (6 variables) from its hexadecimal value. Display it.
 //! ```
 //! # use volute::Lut6;
 //! # use std::fmt::Display;
 //! let lut = Lut6::from_hex_string("0123456789abcdef").unwrap();
 //! print!("{lut}");
 //! ```
 //!
-//! Create a random Lut6 (six variables).
-//! Display its hexadecimal value.
+//! Small Luts (3 to 7 variables) can be converted to the integer type of the same size.
 //! ```
+//! # use volute::Lut5;
 //! # use volute::Lut6;
+//! # use volute::Lut7;
 //! # #[cfg(feature = "rand")]
-//! let lut = Lut6::random();
+//! let lut5: u32 = Lut5::random().into();
 //! # #[cfg(feature = "rand")]
-//! print!("{lut}");
+//! let lut6: u64 = Lut6::random().into();
+//! # #[cfg(feature = "rand")]
+//! let lut7: u128 = Lut7::random().into();
 //! ```
 //!
 //! Create the parity function on three variables, and check that in can be decomposed as a Xor.
@@ -61,37 +68,43 @@
 //! assert_eq!(format!("{lut:b}"), "Lut3(10010110)");
 //! ```
 //!
-//! Create a Lut2 and swap its inputs.
-//! Check the result.
-//! ```
-//! # use volute::Lut2;
-//! let lut = Lut2::nth_var(0);
-//! assert_eq!(lut.swap(0, 1), Lut2::nth_var(1));
-//! ```
-//!
 //! ## Sum of products and Exclusive sum of products
 //!
 //! Volute provides Sum-of-Products (SOP) and Exclusive Sum-of-Products (ESOP)
-//! representations, including exact decomposition methods using a MILP solver
-//! or a SAT solver.
+//! representations.
+//!
+//! Create Sum of products and perform operations on them.
+//! ```
+//! # use volute::sop::Cube;
+//! # use volute::sop::Sop;
+//! let var4 = Sop::nth_var(10, 4);
+//! let var2 = Sop::nth_var(10, 2);
+//! let var_and = var4 & var2;
+//! ```
+//!
+//! Exact decomposition methods can be used with the features `optim-mip`  (using a MILP solver)
+//! or `optim-sat` (using a SAT solver).
 //!
 //!  ```
 //! # use volute::Lut;
 //! # use volute::sop;
-//! let lut = Lut::parity(6);
+//! let lut = Lut::threshold(6, 5);
 //! # #[cfg(feature = "optim-mip")]
-//! let sop = sop::optim::optimize_esop_mip(&[lut], 1, 2);
+//! let esop = sop::optim::optimize_esop_mip(&[lut], 1, 2);
 //! ```
 //!
 //! ## Canonical representation
 //!
-//! For boolean optimization, Luts can be represented by a canonical
-//! representation, that is identical up to variable complementation (N),
-//! input permutation (P), or both (NPN).
+//! For boolean optimization, Luts have several canonical forms that allow to only store
+//! optimizations for a small subset of Luts.
+//! Methods are available to find the smallest Lut that is identical up to variable
+//! complementation (N), input permutation (P), or both (NPN).
 //!
-//!  ```
-//! # use volute::Lut6;
-//! let lut = Lut6::parity();
+//! ```
+//! # use volute::Lut4;
+//! let lut = Lut4::threshold(3);
+//! let (canonical, flips) = lut.n_canonization();
+//! let (canonical, perm) = lut.p_canonization();
 //! let (canonical, perm, flips) = lut.npn_canonization();
 //! ```
 //!

src/sop/optim/sat.rs

@@ -3,7 +3,6 @@
 use std::cmp::max;
 use std::iter::zip;
 
-use rustsat::instances::ManageVars;
 use rustsat::instances::SatInstance;
 use rustsat::solvers::Solve;
 use rustsat::solvers::SolverResult;
@@ -81,7 +80,7 @@ impl<'a> SopModeler<'a> {
     fn build_variables(&mut self, n: usize) -> Vec<Lit> {
         let mut ret = Vec::new();
         for _ in 0..n {
-            ret.push(self.instance.var_manager().new_var().pos_lit());
+            ret.push(self.instance.new_var().pos_lit());
         }
         ret
     }
@@ -91,7 +90,7 @@ impl<'a> SopModeler<'a> {
         for _ in 0..n {
             let mut fn_vars = Vec::new();
             for _ in self.functions {
-                fn_vars.push(self.instance.var_manager().new_var().pos_lit());
+                fn_vars.push(self.instance.new_var().pos_lit());
             }
             ret.push(fn_vars);
         }
@@ -217,7 +216,7 @@ impl<'a> SopModeler<'a> {
             ));
         }
         let mut solver = rustsat_kissat::Kissat::default();
-        solver.add_cnf(inst.clone().as_cnf().0).unwrap();
+        solver.add_cnf(inst.into_cnf().0).unwrap();
         if solver.solve().unwrap() == SolverResult::Sat {
             let sol = solver.solution(self.max_var()).unwrap();
             Some(sol)
@@ -368,7 +367,7 @@ impl<'a> EsopModeler<'a> {
     fn build_variables(&mut self, n: usize) -> Vec<Lit> {
         let mut ret = Vec::new();
         for _ in 0..n {
-            ret.push(self.instance.var_manager().new_var().pos_lit());
+            ret.push(self.instance.new_var().pos_lit());
         }
         ret
     }
@@ -378,7 +377,7 @@ impl<'a> EsopModeler<'a> {
         for _ in 0..n {
             let mut fn_vars = Vec::new();
             for _ in self.functions {
-                fn_vars.push(self.instance.var_manager().new_var().pos_lit());
+                fn_vars.push(self.instance.new_var().pos_lit());
             }
             ret.push(fn_vars);
         }
@@ -424,7 +423,7 @@ impl<'a> EsopModeler<'a> {
         let mut xor_val = vars[0];
         for i in 1..vars.len() {
             let v = vars[i];
-            let next_val = self.instance.var_manager().new_var().pos_lit();
+            let next_val = self.instance.new_var().pos_lit();
             self.instance.add_ternary(!xor_val, !next_val, !v);
             self.instance.add_ternary(!xor_val, next_val, v);
             self.instance.add_ternary(xor_val, !next_val, v);
@@ -508,7 +507,7 @@ impl<'a> EsopModeler<'a> {
             ));
         }
         let mut solver = rustsat_kissat::Kissat::default();
-        solver.add_cnf(inst.clone().as_cnf().0).unwrap();
+        solver.add_cnf(inst.into_cnf().0).unwrap();
         if solver.solve().unwrap() == SolverResult::Sat {
             let sol = solver.solution(self.max_var()).unwrap();
             Some(sol)

src/static_lut.rs

@@ -660,6 +660,12 @@ impl From<u64> for Lut6 {
     }
 }
 
+impl From<u128> for Lut7 {
+    fn from(table: u128) -> Lut7 {
+        Lut7::from_blocks(&[(table & 0xffff_ffff_ffff_ffff) as u64, (table >> 64) as u64])
+    }
+}
+
 impl From<Lut3> for u8 {
     fn from(lut: Lut3) -> u8 {
         (lut.table[0] & !VAR_MASK[3]) as u8
@@ -684,6 +690,12 @@ impl From<Lut6> for u64 {
     }
 }
 
+impl From<Lut7> for u128 {
+    fn from(lut: Lut7) -> u128 {
+        lut.table[0] as u128 + ((lut.table[1] as u128) << 64)
+    }
+}
+
 #[cfg(test)]
 mod tests {
     use crate::{Lut0, Lut1, Lut2, Lut3, Lut4, Lut5, Lut6, Lut7};
@@ -791,18 +803,27 @@ mod tests {
         for _ in 0..10 {
             let lut = Lut3::random();
             assert_eq!(lut, Lut3::from(u8::from(lut)));
+            assert_eq!(lut.to_hex_string(), format!("{:02x}", u8::from(lut)));
         }
         for _ in 0..10 {
             let lut = Lut4::random();
             assert_eq!(lut, Lut4::from(u16::from(lut)));
+            assert_eq!(lut.to_hex_string(), format!("{:04x}", u16::from(lut)));
         }
         for _ in 0..10 {
             let lut = Lut5::random();
             assert_eq!(lut, Lut5::from(u32::from(lut)));
+            assert_eq!(lut.to_hex_string(), format!("{:08x}", u32::from(lut)));
         }
         for _ in 0..10 {
             let lut = Lut6::random();
             assert_eq!(lut, Lut6::from(u64::from(lut)));
+            assert_eq!(lut.to_hex_string(), format!("{:016x}", u64::from(lut)));
+        }
+        for _ in 0..10 {
+            let lut = Lut7::random();
+            assert_eq!(lut, Lut7::from(u128::from(lut)));
+            assert_eq!(lut.to_hex_string(), format!("{:032x}", u128::from(lut)));
         }
     }