libreda-logic 0.0.3

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

//! And-inverter (AIG) graph data structures.

use crate::{
    helpers::sort2,
    network::*,
    networks::generic_network::*,
    truth_table::small_lut::{truth_table_library, SmallTruthTable},
};

use super::SimplifyResult;

/// And-inverter graph.
///
/// A logic network consisting of three-input majority nodes.
///
/// # Examples
/// ```
/// use libreda_logic::traits::*;
/// use libreda_logic::network::*;
/// use libreda_logic::networks::aig::*;
///
/// // Create an empty network.
/// let mut aig = Aig::new();
///
/// // Create two inputs.
/// let a = aig.create_primary_input();
/// let b = aig.create_primary_input();
///
/// // Create the boolean AND of the two inputs.
/// let a_and_b = aig.create_and(a, b);
/// ```
pub type Aig = LogicNetwork<AigNode>;

/// Identifier for nodes in the and-inverter graph.
pub type AigNodeId = NodeId;

/// Node in the and-inverter graph.
#[derive(Clone, Copy, Debug, Hash, PartialEq, PartialOrd, Eq, Ord)]
pub struct AigNode {
    pub(super) a: AigNodeId,
    pub(super) b: AigNodeId,
    /// Number of nodes which reference to this node.
    num_references: usize,
}

impl AigNode {
    /// Create a new 2-input AND node.
    fn new([a, b]: [AigNodeId; 2]) -> Self {
        Self {
            a,
            b,
            num_references: 0,
        }
    }

    /// Get the child node IDs as an array.
    fn to_array(self) -> [AigNodeId; 2] {
        [self.a, self.b]
    }

    /// Get an array of mutable references to the node inputs.
    fn to_array_mut(&mut self) -> [&mut AigNodeId; 2] {
        [&mut self.a, &mut self.b]
    }
}

impl NetworkNode for AigNode {
    type NodeId = AigNodeId;

    fn num_inputs(&self) -> usize {
        2
    }

    fn get_input(&self, i: usize) -> Self::NodeId {
        match i {
            0 => self.a,
            1 => self.b,
            _ => panic!("index out of bounds"),
        }
    }

    fn function(&self) -> SmallTruthTable {
        truth_table_library::and2()
    }

    fn normalized(self) -> SimplifyResult<Self, Self::NodeId> {
        Aig::simplify_node(self)
    }
}

impl MutNetworkNode for AigNode {
    fn set_input(&mut self, i: usize, signal: Self::NodeId) {
        let input = match i {
            0 => &mut self.a,
            1 => &mut self.b,
            _ => panic!("index out of bounds"),
        };

        *input = signal;
    }
}

impl NetworkNodeWithReferenceCount for AigNode {
    fn num_references(&self) -> usize {
        self.num_references
    }
}

impl MutNetworkNodeWithReferenceCount for AigNode {
    fn reference(&mut self) {
        self.num_references += 1;
    }

    fn dereference(&mut self) {
        self.num_references -= 1;
    }
}

impl IntoIterator for AigNode {
    type Item = AigNodeId;

    type IntoIter = std::array::IntoIter<AigNodeId, 2>;

    fn into_iter(self) -> Self::IntoIter {
        // Sanity check: inputs must be sorted.
        debug_assert_eq!(
            self.to_array(),
            sort2(self.to_array()),
            "inputs must be sorted"
        );

        self.to_array().into_iter()
    }
}

impl Aig {
    /// Simplify the node without making changes to the graph.
    ///
    /// Either returns the ID of an existing node which is equivalent to the given node,
    /// or returns a node with simplified input, or returns the unmodified node.
    fn simplify_node(node: AigNode) -> SimplifyResult<AigNode, NodeId> {
        SimplifyResult::new_node(node)
            // Use majority rule
            .and_then(Self::simplify_node_by_majority)
            .and_then(Self::simplify_constants)
            .map_unsimplified(Self::normalize_node_by_commutativity) // TODO: Is this necessary? Might be done in simplify_node_with_hashtable
    }

    /// Sort the inputs of the node.
    /// Use the rule `AND(x, y) == AND(y, x)``.
    fn normalize_node_by_commutativity(node: AigNode) -> AigNode {
        let [a, b] = sort2(node.to_array());
        AigNode { a, b, ..node }
    }

    /// Simplify if both operands are equal.
    fn simplify_node_by_majority(node: AigNode) -> SimplifyResult<AigNode, NodeId> {
        let [a, b] = [node.a, node.b];
        match [a, b] {
            // And(x, x) => x
            [x, y] if x == y => SimplifyResult::new_id(x),
            // And(x, x') => false
            [x, y] if x == y.invert() => SimplifyResult::new_id(AigNodeId::zero()),
            _ => SimplifyResult::new_node(node),
        }
    }

    /// Simplify `And(x, 0) = 0` and `And(x, 1) = x`.
    fn simplify_constants(node: AigNode) -> SimplifyResult<AigNode, NodeId> {
        let [a, b] = node.to_array();
        match [a, b] {
            [x, _] | [_, x] if x.is_zero() => SimplifyResult::new_id(AigNodeId::zero()),
            [x, y] | [y, x] if x.is_one() => SimplifyResult::new_id(y),
            _ => SimplifyResult::new_node(node),
        }
    }
}

impl HomogeneousNetwork for Aig {
    const NUM_NODE_INPUTS: usize = 2;

    fn function(&self) -> Self::NodeFunction {
        crate::truth_table::small_lut::truth_table_library::and2()
    }
}

impl SubstituteInNode for Aig {
    fn substitute_in_node(
        &mut self,
        node: Self::NodeId,
        old_signal: Self::Signal,
        new_signal: Self::Signal,
    ) {
        if let Some(n) = self.get_logic_node_mut(node) {
            // Replace the each occurrence of the old signal with the new signal.
            n.to_array_mut()
                .into_iter()
                .filter(|input| **input == old_signal)
                .for_each(|input| *input = new_signal);
        }
    }
}

impl UnaryOp for Aig {
    fn create_not(&mut self, signal: Self::Signal) -> Self::Signal {
        signal.invert()
    }
}

impl BinaryOp for Aig {
    fn create_and(&mut self, a: Self::Signal, b: Self::Signal) -> Self::Signal {
        let node = AigNode::new([a, b]);
        // TODO: doing double the work. Normalization is already called by `create_node`
        match Self::simplify_node(node) {
            SimplifyResult::Node(n, invert) => self.create_node(n).invert_if(invert),
            SimplifyResult::Simplified(s, invert) => s.invert_if(invert),
        }
    }

    fn create_or(&mut self, a: Self::Signal, b: Self::Signal) -> Self::Signal {
        self.create_and(a.invert(), b.invert()).invert()
    }

    fn create_nand(&mut self, a: Self::Signal, b: Self::Signal) -> Self::Signal {
        self.create_and(a, b).invert()
    }

    fn create_nor(&mut self, a: Self::Signal, b: Self::Signal) -> Self::Signal {
        self.create_or(a, b).invert()
    }

    fn create_xor(&mut self, a: Self::Signal, b: Self::Signal) -> Self::Signal {
        let x = self.create_and(a, b.invert());
        let y = self.create_and(a.invert(), b);
        self.create_or(x, y)
    }
}

impl TernaryOp for Aig {}

#[test]
fn test_aig_create_constants() {
    let aig = Aig::new();

    let zero = aig.get_constant(false);
    let one = aig.get_constant(true);

    assert!(zero.is_constant());
    assert!(one.is_constant());

    assert!(zero.is_zero());

    assert_ne!(zero, one);
    assert_eq!(zero.invert(), one);
}

#[test]
fn test_aig_create_primary_inputs() {
    let mut aig = Aig::new();
    let a = aig.create_primary_input();
    let b = aig.create_primary_input();
    let c = aig.create_primary_input();

    assert_ne!(a, b);
    assert_ne!(b, c);

    assert!(aig.is_input(a));
    assert!(aig.is_input(b));
    assert!(aig.is_input(c));

    assert!(!aig.is_constant(a));
}

#[test]
fn test_aig_node_deduplication() {
    let mut aig = Aig::new();

    let a = aig.create_primary_input();
    let b = aig.create_primary_input();

    let a_and_b_1 = aig.create_and(a, b);
    let a_and_b_2 = aig.create_and(a, b);

    assert_eq!(a_and_b_1, a_and_b_2);
}

#[test]
fn test_aig_node_simplification_by_commutativity() {
    let mut aig = Aig::new();

    let a = aig.create_primary_input();
    let b = aig.create_primary_input();

    let a_and_b_1 = aig.create_and(a, b);
    let a_and_b_2 = aig.create_and(b, a);

    assert_eq!(a_and_b_1, a_and_b_2);
}

#[test]
fn test_aig_node_simplification_by_majority() {
    let mut aig = Aig::new();

    let a = aig.create_primary_input();

    let a_and_a = aig.create_and(a, a);
    assert_eq!(a_and_a, a);
}

#[test]
fn test_aig_node_simplification_with_constants() {
    let mut aig = Aig::new();

    let a = aig.create_primary_input();

    let zero = aig.get_constant(false);

    let a_and_zero = aig.create_and(a, zero);

    assert_eq!(a_and_zero, zero);
}

#[test]
fn test_aig_simulation() {
    use crate::native_boolean_functions::NativeBooleanFunction;
    use crate::traits::BooleanSystem;

    // Construct a one-bit full adder.
    let mut aig = Aig::new();
    let [in1, in2, carry_in] = aig.create_primary_inputs();

    let sum = aig.create_xor3(in1, in2, carry_in);
    let carry = aig.create_maj3(in1, in2, carry_in);

    let output_sum = aig.create_primary_output(sum);
    let output_carry = aig.create_primary_output(carry);

    let simulator = crate::network_simulator::RecursiveSim::new(&aig);

    // Reference model of the full adder.
    fn full_adder([a, b, c]: [bool; 3]) -> [bool; 2] {
        let sum = (a as usize) + (b as usize) + (c as usize);
        [
            sum & 0b1 == 1,
            sum & 0b10 == 0b10, // carry
        ]
    }

    let reference = NativeBooleanFunction::new(full_adder);

    for i in 0..(1 << 3) {
        let inputs = [0, 1, 2].map(|idx| (i >> idx) & 1 == 1);

        let exptected_output = [0, 1].map(|out| reference.evaluate_term(&out, &inputs));
        let actual_output: Vec<_> = simulator
            .simulate(&[output_sum, output_carry], &inputs)
            .collect();

        dbg!(inputs);

        assert_eq!(exptected_output.as_slice(), actual_output.as_slice());
    }
}