libreda-logic 0.0.3

// SPDX-FileCopyrightText: 2022 Thomas Kramer <code@tkramer.ch>
//
// SPDX-License-Identifier: AGPL-3.0-or-later

//! Exact NPN (negation-permutation-negation) canonization of truth tables based on brute-force search.
//! Boolean functions can be categorized in equivalence classes such that members of a class can be
//! transformed into eachother by applying negations on the inputs, permuting the inputs and possibly negating the output.
//! Each NPN class has the same combinational complexity, i.e. its members share the same size-optimal implementation as a boolean network.

use crate::traits::NumInputs;

use super::bitflip_iter::{bitflips, BitFlippable};
use super::permutation_gray_code::{permutation_swaps, permutation_swaps_cyclic};
use super::permutation_iter::{permutations, Permutable};
use super::small_lut::{SmallStaticTruthTable, SmallTT, SmallTruthTable};
use super::{gray_code_flips, npn_transform::*};

/// Track input inversions, input permutations and output inversions of `SmallTruthTable`s.
/// This is used to find a transformation which leads a function to it's canonical form.
#[derive(Copy, Clone, Eq, PartialEq, PartialOrd, Ord)]
pub struct NPNTransformTracker {
    /// The truth-table. Result of applying `tf`.
    tt: SmallTruthTable,
    /// The transform which as lead to the truth-table.
    tf: NPNTransform,
}

impl NPNTransformTracker {
    /// Wrap the truth-table into a transform tracker.
    /// The transform tracker allows to apply input reordering, input negation and output negation to
    /// the truth-table while keeping track of the applied operations.
    pub fn new(tt: SmallTruthTable) -> Self {
        Self {
            tt,
            tf: NPNTransform::identity(tt.num_inputs()),
        }
    }

    /// Get the truth-table.
    /// It is the result of applying the `transform()` to the original truth-table.
    pub fn truth_table(&self) -> SmallTruthTable {
        self.tt
    }

    /// Get the transform which led to the `truth_table`.
    pub fn transform(&self) -> NPNTransform {
        self.tf
    }
}

impl InvertOutput for NPNTransformTracker {
    fn inverted_output(mut self) -> Self {
        self.invert_output();
        self
    }

    fn invert_output(&mut self) {
        self.tt.invert_output();
        self.tf.invert_output();
    }
}

impl BitFlippable for NPNTransformTracker {
    fn num_bits(&self) -> usize {
        self.tt.num_bits()
    }

    fn flip_bit(&mut self, bit_idx: usize) {
        self.tt.flip_bit(bit_idx);
        self.tf.flip_bit(bit_idx);
    }
}

impl Permutable for NPNTransformTracker {
    fn len(&self) -> usize {
        self.tt.len()
    }

    fn swap(&mut self, i: usize, j: usize) {
        self.tt.swap(i, j);
        self.tf.swap(i, j);
    }
}

/// Find the NPN-representative of the truth-table. I.e. the lexicographically smallest
/// truth-table which can be generated from `tt` by applying inversions at the inputs, permuting the inputs
/// and inverting the output.
///
/// # Example
///
/// ```
/// use libreda_logic::truth_table::canonization::exact_npn_canonization;
/// use libreda_logic::truth_table::small_lut::SmallTruthTable;
///
/// let tt1 = SmallTruthTable::new(|[a, b, c]| a & b ^ c);
/// let tt2 = SmallTruthTable::new(|[a, b, c]| !(c & !b ^ a));
///
/// assert_eq!(exact_npn_canonization(tt1), exact_npn_canonization(tt2));
/// ```
/// # Example - extracting the transform which leads to the canonical form.
///
/// Sometimes not only the canonical form of the truth-table is of interest but also
/// the transform which converts the original truth-table into its canonical form.
/// This can be used by wrapping the truth-table into a 'transform tracker':
///
/// ```
/// use libreda_logic::truth_table::canonization::{exact_npn_canonization, NPNTransformTracker};
/// use libreda_logic::truth_table::small_lut::SmallTruthTable;
///
/// let tt = SmallTruthTable::new(|[a, b, c]| a & b ^ c);
///
/// let tracker = NPNTransformTracker::new(tt);
///
/// // Perform canonization on the wrapped truth-table `tracker`!
/// exact_npn_canonization(tt);
/// let canonical_form = exact_npn_canonization(tracker);
///
/// let canonical_truth_table = canonical_form.truth_table();
///
/// let transform = canonical_form.transform();
/// let inverse_transform = transform.inverse();
///
/// assert_eq!(transform.apply(tt), canonical_truth_table);
/// assert_eq!(tt, inverse_transform.apply(canonical_truth_table));
///
/// ```
pub fn exact_npn_canonization<T>(tt: T) -> T
where
    T: Clone + BitFlippable + Permutable + InvertOutput + Ord,
{
    let mut state = tt.clone();
    let mut min = tt.clone();
    let n = tt.num_bits();

    // Swapping inputs is slower than inverting inputs which is slower than inverting the output.
    // Therefore, do the slowest operation in the outer loop and the fastest in the inner loop.

    // For all permutations...
    for swap in permutation_swaps_cyclic(n) {
        //let pre_flip = state.clone();
        // for all input flips...
        for flip_idx in gray_code_flips::gray_code_flips(n) {
            // for all output flips
            for _ in 0..2 {
                if state < min {
                    state.clone_into(&mut min);
                }
                state.invert_output();
            }
            state.flip_bit(flip_idx);
        }
        //debug_assert!(state == pre_flip, "state should be reverted");

        state.swap(swap.0, swap.1);
    }
    debug_assert!(state == tt, "state should be reverted to the initial state");

    min

    //// Neater but slower (requires clones):
    //// Iterate over all permutations of the inputs.
    //permutations(tt)
    //    // Find canonical form by inverting inputs and output.
    //    .map(exact_nn_canonization)
    //    // Find lexicographical smallest truth-table.
    //    .min()
    //    .unwrap() // There is always at least one lement in the iterator.

    //// TODO: Use this simpler alternative if it performs better. Benchmark says it's worse.
    // all_npn_equivalent_functions(tt)
    // // Find lexicographical smallest truth-table.
    // .min()
    // .unwrap()
}

/// Find the NN-representative of the truth-table. I.e. the lexicographically smallest
/// truth-table which can be generated from `tt` by applying inversions at the inputs and at the output.
pub fn exact_nn_canonization<T>(tt: T) -> T
where
    T: Clone + BitFlippable + InvertOutput + Ord,
{
    let mut state = tt.clone();
    let mut min = tt.clone();
    let n = tt.num_bits();

    // for all input flips...
    for flip_idx in gray_code_flips::gray_code_flips(n) {
        // for all output flips
        for _ in 0..2 {
            if state < min {
                state.clone_into(&mut min);
            }
            // Inverting the output is cheap, therefore do it in the inner loop.
            state.invert_output();
        }
        state.flip_bit(flip_idx);
    }
    debug_assert!(state == tt, "state should be reverted to the initial state");

    min
    //bitflips(tt)
    //    // Find canonical form by inverting the output.
    //    .map(|tt| tt.clone().inverted_output().min(tt))
    //    .min()
    //    .unwrap()

    //// TODO: Use this simpler alternative if it performs better.
    //all_nn_equivalent_functions(tt)
    //    // Find lexicographical smallest truth-table.
    //    .min()
    //    .unwrap()
}

/// Iterate over the truth-tables of all functions which are in the same 'NN' class as `tt`.
/// I.e. all functions which can be derived from `tt` by inverting input and output bits.
pub fn all_nn_equivalent_functions<T>(tt: T) -> impl Iterator<Item = T>
where
    T: Clone + BitFlippable + InvertOutput + Ord,
{
    [tt.clone(), tt.inverted_output()]
        .into_iter()
        .flat_map(bitflips)
}

/// Iterate over the truth-tables of all functions which are in the same 'NPN' class as `tt`.
/// I.e. all functions which can be derived from `tt` by inverting input bits, permuting inputs and inverting the output.
pub fn all_npn_equivalent_functions<T>(tt: T) -> impl Iterator<Item = T>
where
    T: Clone + BitFlippable + InvertOutput + Permutable + Ord,
{
    all_nn_equivalent_functions(tt).flat_map(all_p_equivalent_functions)
}

#[test]
fn test_nn_canonization_3_inputs() {
    let tt1 = SmallTruthTable::new(|[a, b, c]| a & b | c);
    let tt2 = SmallTruthTable::new(|[a, b, c]| !(a & b | !c));

    assert_eq!(exact_nn_canonization(tt1), exact_nn_canonization(tt2));
}

#[test]
fn test_npn_canonization_2_inputs() {
    let tt1 = SmallTruthTable::new(|[a, b]| a & b);
    let tt2 = SmallTruthTable::new(|[a, b]| !(!b & a));

    assert_eq!(exact_npn_canonization(tt1), exact_npn_canonization(tt2));

    //let tt3 = SmallTruthTable::new(|[a, b]| a ^ b);
    //assert_ne!(exact_npn_canonization(tt1), exact_npn_canonization(tt3));
}

#[test]
fn test_npn_canonization_3_inputs() {
    let tt1 = SmallTruthTable::new(|[a, b, c]| a & b ^ c);
    let tt2 = SmallTruthTable::new(|[a, b, c]| !(c & !b ^ a));

    assert_eq!(exact_npn_canonization(tt1), exact_npn_canonization(tt2));
}

/// Find the P-representative of the truth-table. I.e. the lexicographically smallest
/// truth-table which can be generated from `tt` by permuting the inputs.
pub fn exact_p_canonization<T>(tt: T) -> T
where
    T: Permutable + Ord + Clone,
{
    let mut state = tt.clone();
    let mut min = tt.clone();
    let n = tt.len();

    // For all permutations...
    for swap in permutation_swaps(n) {
        state.swap(swap.0, swap.1);
        if state < min {
            state.clone_into(&mut min);
        }
    }

    min
    //permutations(tt)
    //    // Find the lexicographical smallest truth-table.
    //    .min()
    //    .unwrap() // There's always an element in this iterator.
}

/// Iterate over the truth-tables of all functions which are in the same 'P' class as `tt`.
/// I.e. all functions which can be derived from `tt` by permuting the inputs.
pub fn all_p_equivalent_functions<T>(tt: T) -> impl Iterator<Item = T>
where
    T: Clone + Permutable,
{
    permutations(tt)
}

impl Permutable for SmallTruthTable {
    fn len(&self) -> usize {
        self.num_inputs()
    }

    fn swap(&mut self, i: usize, j: usize) {
        *self = self.swap_inputs(i, j);
    }
}

impl BitFlippable for SmallTruthTable {
    fn num_bits(&self) -> usize {
        self.num_inputs()
    }

    fn flip_bit(&mut self, bit_idx: usize) {
        *self = self.invert_input(bit_idx)
    }
}

impl InvertOutput for SmallTruthTable {
    fn inverted_output(mut self) -> Self {
        self.invert_output();
        self
    }

    fn invert_output(&mut self) {
        *self = <Self as SmallTT>::invert(*self);
    }
}

impl<const N: usize> Permutable for SmallStaticTruthTable<N> {
    fn len(&self) -> usize {
        self.num_inputs()
    }

    fn swap(&mut self, i: usize, j: usize) {
        *self = self.swap_inputs(i, j);
    }
}

impl<const N: usize> BitFlippable for SmallStaticTruthTable<N> {
    fn num_bits(&self) -> usize {
        self.num_inputs()
    }

    fn flip_bit(&mut self, bit_idx: usize) {
        *self = self.invert_input(bit_idx)
    }
}

impl<const N: usize> InvertOutput for SmallStaticTruthTable<N> {
    fn inverted_output(mut self) -> Self {
        self.invert_output();
        self
    }

    fn invert_output(&mut self) {
        *self = <Self as SmallTT>::invert(*self);
    }
}
#[test]
fn test_p_canonization_2_inputs() {
    let tt1 = SmallTruthTable::new(|[a, b]| !a & b);
    let tt2 = SmallTruthTable::new(|[a, b]| a & !b);

    assert_eq!(exact_p_canonization(tt1), exact_p_canonization(tt2));
}

#[test]
fn test_p_canonization_6_inputs() {
    let tt1 = SmallTruthTable::new(|[a, b, c, d, e, f]| a & b & !c | d ^ e ^ f);
    let tt2 = SmallTruthTable::new(|[f, b, c, e, d, a]| a & b & !c | d ^ e ^ f);

    assert_eq!(exact_p_canonization(tt1), exact_p_canonization(tt2));
}

#[test]
fn test_npn_canonization_get_transform() {
    let tt = SmallTruthTable::new(|[a, b, c]| a & b ^ c);

    let tracker = NPNTransformTracker::new(tt);

    // Perform canonization on the wrapped truth-table `tracker`!
    exact_npn_canonization(tt);
    let canonical_form = exact_npn_canonization(tracker);

    let canonical_truth_table = canonical_form.truth_table();

    let transform = canonical_form.transform();
    let inverse_transform = transform.inverse();

    assert_eq!(transform.apply(tt), canonical_truth_table);
    assert_eq!(tt, inverse_transform.apply(canonical_truth_table));
}

#[test]
fn test_generate_3_input_npn_classes() {
    use std::collections::HashSet;

    let all_functions = (0..(1 << 8)).map(|i| SmallTruthTable::from_table(i, 3));

    let canonized = all_functions.map(exact_npn_canonization);
    let npn_classes: HashSet<_> = canonized.collect();

    assert_eq!(
        npn_classes.len(),
        14,
        "there must be 14 different NPN classes of 3-input Boolean functions"
    );
}

#[test]
fn test_generate_4_input_npn_classes() {
    use std::collections::HashSet;

    let all_functions = (0..(1 << 16)).map(|i| SmallTruthTable::from_table(i, 4));

    let canonized = all_functions.map(exact_npn_canonization);
    let npn_classes: HashSet<_> = canonized.collect();

    assert_eq!(
        npn_classes.len(),
        222,
        "there must be 222 different NPN classes of 4-input Boolean functions"
    );
}