Skip to main content

volute/
decomposition.rs

1use crate::operations::*;
2
3/// A helper function to many properties of an input using the cofactors
4/// * Insensitive to input: c0 == c1
5/// * And/Or/Nand/Nor canalizing: c0 or c1 is 0 or 1
6/// * Xor-separable: c0 == !c1
7/// * Positive/negative unate: c0 | !c1 or !c0 | c1
8///
9/// The given operation takes two words of the cofactor and returns one word with a bit set for all positions that match
10pub fn input_property_helper<F>(num_vars: usize, table: &[u64], ind: usize, op: F) -> bool
11where
12    F: Fn(u64, u64) -> u64,
13{
14    assert!(table.len() == table_size(num_vars));
15    assert!(ind < num_vars);
16    let mask = num_vars_mask(num_vars);
17    let mut ret = true;
18    if ind <= 5 {
19        let shift = 1 << ind;
20        let m1 = VAR_MASK[ind];
21        let m0 = !VAR_MASK[ind];
22        for t in table {
23            let c1 = ((*t & m1) >> shift) | (*t & m1);
24            let c0 = ((*t & m0) << shift) | (*t & m0);
25            ret &= !op(c0, c1) & mask == 0;
26        }
27    } else {
28        let stride = 1 << (ind - 6);
29        for i in 0..table.len() {
30            if i & stride == 0 {
31                let c0 = table[i];
32                let c1 = table[i + stride];
33                ret &= !op(c0, c1) & mask == 0;
34            }
35        }
36    }
37    ret
38}
39
40pub fn input_independent(num_vars: usize, table: &[u64], ind: usize) -> bool {
41    input_property_helper(num_vars, table, ind, |c0, c1| !(c0 ^ c1))
42}
43
44pub fn input_and(num_vars: usize, table: &[u64], ind: usize) -> bool {
45    input_property_helper(num_vars, table, ind, |c0, _| !c0)
46}
47
48pub fn input_or(num_vars: usize, table: &[u64], ind: usize) -> bool {
49    input_property_helper(num_vars, table, ind, |_, c1| c1)
50}
51
52pub fn input_nand(num_vars: usize, table: &[u64], ind: usize) -> bool {
53    input_property_helper(num_vars, table, ind, |c0, _| c0)
54}
55
56pub fn input_nor(num_vars: usize, table: &[u64], ind: usize) -> bool {
57    input_property_helper(num_vars, table, ind, |_, c1| !c1)
58}
59
60pub fn input_xor(num_vars: usize, table: &[u64], ind: usize) -> bool {
61    input_property_helper(num_vars, table, ind, |c0, c1| c0 ^ c1)
62}
63
64pub fn input_pos_unate(num_vars: usize, table: &[u64], ind: usize) -> bool {
65    input_property_helper(num_vars, table, ind, |c0, c1| !c0 | c1)
66}
67
68pub fn input_neg_unate(num_vars: usize, table: &[u64], ind: usize) -> bool {
69    input_property_helper(num_vars, table, ind, |c0, c1| !c1 | c0)
70}
71
72/// Basic boolean function families to describe decompositions
73#[derive(Debug, PartialEq, Eq, Hash)]
74pub enum DecompositionType {
75    /// No valid decomposition with this variable
76    None,
77    /// The function is independent of this variable
78    Independent,
79    /// The function returns this variable
80    Identity,
81    /// The function returns the negation of this variable
82    Negation,
83    /// Decomposition possible as And
84    And,
85    /// Decomposition possible as Or
86    Or,
87    /// Decomposition possible as Less-Or-Equal (equivalent to Nand for a top decomposition)
88    Le,
89    /// Decomposition possible as Less-Than (equivalent to Nor for a top decomposition)
90    Lt,
91    /// Decomposition possible as Xor
92    Xor,
93}
94
95impl DecompositionType {
96    /// Returns whether the decomposition is trivial (independent, x or !x)
97    pub fn is_trivial(&self) -> bool {
98        [Self::Independent, Self::Identity, Self::Negation].contains(self)
99    }
100
101    /// Returns whether the decomposition is based on an and gate or similar
102    pub fn is_and_type(&self) -> bool {
103        [Self::And, Self::Or, Self::Le, Self::Lt].contains(self)
104    }
105
106    /// Returns whether the decomposition is based on a xor gate
107    pub fn is_xor_type(&self) -> bool {
108        [Self::Xor].contains(self)
109    }
110
111    /// Returns whether the decomposition is based on any 2-input gate
112    pub fn is_simple_gate(&self) -> bool {
113        [Self::And, Self::Or, Self::Le, Self::Lt, Self::Xor].contains(self)
114    }
115}
116
117pub fn top_decomposition(num_vars: usize, table: &[u64], ind: usize) -> DecompositionType {
118    let indep: bool = input_independent(num_vars, table, ind);
119    let and = input_and(num_vars, table, ind);
120    let or = input_or(num_vars, table, ind);
121    let nand = input_nand(num_vars, table, ind);
122    let nor = input_nor(num_vars, table, ind);
123    let xor = input_xor(num_vars, table, ind);
124
125    if indep {
126        DecompositionType::Independent
127    } else if and && or {
128        DecompositionType::Identity
129    } else if nand && nor {
130        DecompositionType::Negation
131    } else if and {
132        DecompositionType::And
133    } else if or {
134        DecompositionType::Or
135    } else if nand {
136        DecompositionType::Le
137    } else if nor {
138        DecompositionType::Lt
139    } else if xor {
140        DecompositionType::Xor
141    } else {
142        DecompositionType::None
143    }
144}