Crate volute 

Logic function manipulation using truth tables (or lookup tables) that represent the value of the function for the 2ⁿ possible inputs.

The crate implements optimized truth table datastructures, either arbitrary-size truth tables (Lut), or more efficient fixed-size truth tables (Lut2 to Lut16). They provide logical operators and utility functions for analysis, canonization and decomposition. Some support is available for other standard representation, such as Sum-of-Products (SOP) and Exclusive Sum-of-Products (ESOP).

Volute is used by the logic optimization and analysis library Quaigh. When applicable, API and documentation try to follow the same terminology as the C++ library Kitty.

Examples

Create a constant-one Lut with five variables and a constant-zero Lut with 4 variables.

let lut5 = Lut::one(5);
let lut4 = Lut::zero(4);

Create a Lut2 representing the first variable. Swap its inputs. Check the result.

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.

let lut = Lut4::nth_var(0) & Lut4::nth_var(2);
assert_eq!(lut.to_string(), "Lut4(a0a0)");

Create a Lut6 (6 variables) from its hexadecimal value. Display it.

let lut = Lut6::from_hex_string("0123456789abcdef").unwrap();
print!("{lut}");

Small Luts (3 to 7 variables) can be converted to the integer type of the same size.

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. Check its value in binary.

let lut = Lut::parity(3);
assert_eq!(lut.top_decomposition(0), DecompositionType::Xor);
assert_eq!(format!("{lut:b}"), "Lut3(10010110)");

Sum of products and Exclusive sum of products

Volute provides Sum-of-Products (SOP) and Exclusive Sum-of-Products (ESOP) representations.

Create Sum of products and perform operations on them.

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).

let lut = Lut::threshold(4, 3);
let esop = sop::optim::optimize_esop_mip(&[lut], 1, 2);

Canonical representation

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).

let lut = Lut4::threshold(3);
let (canonical, flips) = lut.n_canonization();
let (canonical, perm) = lut.p_canonization();
let (canonical, perm, flips) = lut.npn_canonization();
assert_eq!(lut.permute(&perm).flip_n(flips), canonical);

Modules

sop

Sum-of-Products representations

Structs

Lut

Arbitrary-size truth table, representing a N-input boolean function with 2^N bits, one for each input combination

StaticLut

Fixed-size truth table representing a N-input boolean function with 2^N bits; more compact than Lut when the size is known

Enums

DecompositionType

Basic boolean function families to describe decompositions

ParseLutError

An error that can be returned when parsing a Lut

Type Aliases

Lut0

0-input Lut

Lut1

1-input Lut

Lut2

2-input Lut

Lut3

3-input Lut

Lut4

4-input Lut

Lut5

5-input Lut

Lut6

6-input Lut

Lut7

7-input Lut

Lut8

8-input Lut

Lut9

9-input Lut

Lut10

10-input Lut

Lut11

11-input Lut

Lut12

12-input Lut

Lut13

13-input Lut

Lut14

14-input Lut

Lut15

15-input Lut

Lut16

16-input Lut