Reference

namespace kitty

Enums

enum top_decomposition

Values:

enumerator none
enumerator and_
enumerator or_
enumerator lt_
enumerator le_
enumerator xor_
enum bottom_decomposition

Values:

enumerator none
enumerator and_
enumerator or_
enumerator lt_
enumerator le_
enumerator xor_
enum bi_decomposition

Values:

enumerator none
enumerator and_
enumerator or_
enumerator xor_
enumerator weak_and_
enumerator weak_or_

Functions

template<typename TT, typename Callback = decltype(detail::exact_spectral_canonization_null_callback)>
TT exact_linear_canonization(const TT &tt, Callback &&fn = detail::exact_spectral_canonization_null_callback)

Applies exact linear classification.

This algorithms applies all linear input transformations to a function and returns the function with the smallest integer representation as representative of the equivalence class.

Parameters

tt – Truth table

template<typename TT>
TT exact_linear_output_canonization(const TT &tt)

Applies exact linear classification and output negation.

This algorithms applies all linear input transformations to a function and its complement and returns the function with the smallest integer representation as representative of the equivalence class.

Parameters

tt – Truth table

template<typename TT, typename Callback = decltype(detail::exact_spectral_canonization_null_callback)>
TT exact_affine_canonization(const TT &tt, Callback &&fn = detail::exact_spectral_canonization_null_callback)

Applies exact affine classification.

This algorithms applies all linear input transformations and input complementations to a function and returns the function with the smallest integer representation as representative of the equivalence class.

Parameters

tt – Truth table

template<typename TT>
TT exact_affine_output_canonization(const TT &tt)

Applies exact affine classification and output negation.

This algorithms applies all linear input transformations and input complementations to a function and its complement and returns the function with the smallest integer representation as representative of the equivalence class.

Parameters

tt – Truth table

template<typename TT, typename Fn>
auto unary_operation(const TT &tt, Fn &&op)

Perform bitwise unary operation on truth table.

Parameters
  • tt – Truth table

  • op – Unary operation that takes as input a word (uint64_t) and returns a word

Returns

new constructed truth table of same type and dimensions

template<typename TT, typename Fn>
auto binary_operation(const TT &first, const TT &second, Fn &&op)

Perform bitwise binary operation on two truth tables.

The dimensions of first and second must match. This is ensured at compile-time for static truth tables, but at run-time for dynamic truth tables.

Parameters
  • first – First truth table

  • second – Second truth table

  • op – Binary operation that takes as input two words (uint64_t) and returns a word

Returns

new constructed truth table of same type and dimensions

template<typename TT, typename Fn>
auto ternary_operation(const TT &first, const TT &second, const TT &third, Fn &&op)

Perform bitwise ternary operation on three truth tables.

The dimensions of first, second, and third must match. This is ensured at compile-time for static truth tables, but at run-time for dynamic truth tables.

Parameters
  • first – First truth table

  • second – Second truth table

  • third – Third truth table

  • op – Ternary operation that takes as input two words (uint64_t) and returns a word

Returns

new constructed truth table of same type and dimensions

template<typename TT, typename Fn>
bool binary_predicate(const TT &first, const TT &second, Fn &&op)

Computes a predicate based on two truth tables.

The dimensions of first and second must match. This is ensured at compile-time for static truth tables, but at run-time for dynamic truth tables.

Parameters
  • first – First truth table

  • second – Second truth table

  • op – Binary operation that takes as input two words (uint64_t) and returns a Boolean

Returns

true or false based on the predicate

template<typename TT, typename Fn>
bool ternary_predicate(const TT &first, const TT &second, const TT &third, Fn &&op)

Computes a predicate based on three truth tables.

The dimensions of first, second and third must match. This is ensured at compile-time for static truth tables, but at run-time for dynamic truth tables.

Parameters
  • first – First truth table

  • second – Second truth table

  • third – Third truth table

  • op – Ternary operation that takes as input three words (uint64_t) and returns a Boolean

Returns

true or false based on the predicate

template<typename TT, typename Fn>
void assign_operation(TT &tt, Fn &&op)

Assign computed values to bits.

The functor op computes bits which are assigned to the bits of the truth table.

Parameters
  • tt – Truth table

  • op – Unary operation that takes no input and returns a word (uint64_t)

template<typename TT, typename Fn>
void for_each_block(const TT &tt, Fn &&op)

Iterates through each block of a truth table.

The functor op is called for every block of the truth table.

Parameters
  • tt – Truth table

  • op – Unary operation that takes as input a word (uint64_t) and returns void

template<typename TT, typename Fn>
void for_each_block_reversed(const TT &tt, Fn &&op)

Iterates through each block of a truth table in reverse order.

The functor op is called for every block of the truth table in reverse order.

Parameters
  • tt – Truth table

  • op – Unary operation that takes as input a word (uint64_t) and returns void

template<typename TT, typename Fn>
inline void for_each_one_bit(const TT &tt, Fn &&op)

Iterates through each 1-bit in the truth table.

The functor op is called for every bit position of the truth table for which the bit is assigned 1.

Parameters
  • tt – Truth table

  • op – Unary operation that takes as input a word (uint64_t) and returns void

template<typename TT>
void set_bit(TT &tt, uint64_t index)

Sets bit at index to true.

Parameters
  • tt – Truth table

  • index – Bit index

template<typename TT>
auto get_bit(const TT &tt, uint64_t index)

Gets bit at index.

Parameters
  • tt – Truth table

  • index – Bit index

Returns

1 if bit is set, otherwise 0

template<typename TT>
void clear_bit(TT &tt, uint64_t index)

Clears bit at index.

Parameters
  • tt – Truth table

  • index – Bit index

Returns

1 if bit is set, otherwise 0

template<typename TT>
void flip_bit(TT &tt, uint64_t index)

Flip bit at index.

Parameters
  • tt – Truth table

  • index – Bit index

template<typename TT>
inline uint64_t count_ones(const TT &tt)

Count ones in truth table.

Parameters

tt – Truth table

template<typename TT>
inline uint64_t count_zeros(const TT &tt)

Count zeros in truth table.

Parameters

tt – Truth table

template<typename TT>
int64_t find_first_one_bit(const TT &tt, int64_t start = 0)

Finds least-significant one-bit.

Returns -1, if truth table is constant 0.

Parameters
  • tt – Truth table

  • start – Bit to start from (default is 0)

template<typename TT>
int64_t find_last_one_bit(const TT &tt)

Finds most-significant one-bit.

Returns -1, if truth table is constant 0.

Parameters

tt – Truth table

template<typename TT>
int64_t find_first_bit_difference(const TT &first, const TT &second)

Finds least-significant bit difference.

Returns -1, if truth tables are the same

Parameters
  • first – First truth table

  • second – Second truth table

template<typename TT>
int64_t find_last_bit_difference(const TT &first, const TT &second)

Finds most-significant bit difference.

Returns -1, if truth tables are the same

Parameters
  • first – First truth table

  • second – Second truth table

template<typename TT, typename = std::enable_if_t<is_complete_truth_table<TT>::value>>
std::vector<cube> cnf_characteristic(const TT &tt)

Create CNF of the characteristic function.

Creates a CNF representation for the characteritic function of the input function, also known as Tseytin transformation. To obtain small CNF, an ISOP is computed.

Parameters

tt – Truth table

template<typename TT>
inline TT create(unsigned num_vars)

Creates truth table with number of variables.

If some truth table instance is given, one can create a truth table with the same type by calling the construct() method on it. This function helps if only the number of variables is known and the base type and uniforms the creation of static and dynamic truth tables. Note, however, that for static truth tables num_vars must be consistent to the number of variables in the truth table type.

Parameters

num_vars – Number of variables

template<typename TT>
void create_nth_var(TT &tt, uint8_t var_index, bool complement = false)

Constructs projections (single-variable functions)

Parameters
  • tt – Truth table

  • var_index – Index of the variable, must be smaller than the truth table’s number of variables

  • complement – If true, realize inverse projection

template<class TT>
TT nth_var(uint8_t num_vars, uint8_t var_index, bool complement = false)

Constructs projections (single-variable functions) out-of-place.

Parameters
  • tt – Truth table

  • var_index – Index of the variable, must be smaller than the truth table’s number of variables

  • complement – If true, realize inverse projection

template<typename TT>
void create_from_binary_string(TT &tt, const std::string &binary)

Constructs truth table from binary string.

Note that the first character in the string represents the most significant bit in the truth table. For example, the 2-input AND function is represented by the binary string “1000”. The number of characters in binary must match the number of bits in tt.

Parameters
  • tt – Truth table

  • binary – Binary string with as many characters as bits in the truth table

template<typename TT>
void create_from_hex_string(TT &tt, const std::string &hex)

Constructs truth table from hexadecimal string.

Note that the first character in the string represents the four most significant bit in the truth table. For example, the 3-input majority function is represented by the binary string “E8” or “e8”. The number of characters in hex must be one fourth the number of bits in tt.

Parameters
  • tt – Truth table

  • hex – Hexadecimal string

template<typename TT>
void create_from_raw(TT &tt, std::istream &in)

Creates string from raw character data.

Can create a truth table from the data that is produced by print_raw, e.g., from binary files or std::stringstream.

Parameters
  • tt – Truth table

  • in – Input stream

template<typename TT>
void create_random(TT &tt, std::default_random_engine::result_type seed)

Constructs a truth table from random value.

Computes random words and assigns them to the truth table. The number of variables is determined from the truth table.

Parameters
  • tt – Truth table

  • seed – Random seed

template<typename TT>
void create_random(TT &tt)

Constructs a truth table from random value.

Computes random words and assigns them to the truth table. The number of variables is determined from the truth table. Seed is taken from current time.

Parameters

tt – Truth table

template<typename TT, typename InputIt>
void create_from_words(TT &tt, InputIt begin, InputIt end)

Constructs a truth table from a range of words.

The range of words is given in terms of a begin and end iterator. Hence, it’s possible to copy words from a C++ container or a C array.

Parameters
  • tt – Truth table

  • begin – Begin iterator

  • end – End iterator

template<typename TT, typename = std::enable_if_t<is_complete_truth_table<TT>::value>>
void create_from_cubes(TT &tt, const std::vector<cube> &cubes, bool esop = false)

Creates truth table from cubes representation.

A sum-of-product is represented as a vector of products (called cubes).

An empty truth table is given as first argument to determine type and number of variables. Literals in products that do not fit the number of variables of the truth table are ignored.

The cube representation only allows truth table sizes up to 32 variables.

Parameters
  • tt – Truth table

  • cubes – Vector of cubes

  • esop – Use ESOP instead of SOP

template<typename TT, typename = std::enable_if_t<is_complete_truth_table<TT>::value>>
void create_from_clauses(TT &tt, const std::vector<cube> &clauses, bool esop = false)

Creates truth table from clause representation.

A product-of-sum is represented as a vector of sums (called clauses).

An empty truth table is given as first argument to determine type and number of variables. Literals in sums that do not fit the number of variables of the truth table are ignored.

The clause representation only allows truth table sizes up to 32 variables.

Parameters
  • tt – Truth table

  • clauses – Vector of clauses

  • esop – Use product of exclusive sums instead of POS

template<typename TT, typename = std::enable_if_t<is_complete_truth_table<TT>::value>>
inline void create_majority(TT &tt)

Constructs majority-n function.

The number of variables is determined from the truth table.

Parameters

tt – Truth table

template<typename TT>
void create_threshold(TT &tt, uint8_t threshold)

Constructs threshold function.

The resulting function is true, if strictly more than threshold inputs are

  1. The number of variables is determined from the truth table.

Parameters
  • tt – Truth table

  • threshold – threshold value

template<typename TT, typename = std::enable_if_t<is_complete_truth_table<TT>::value>>
void create_equals(TT &tt, uint8_t bitcount)

Constructs equals-k function.

The resulting function is true, if exactly bitcount bits are 1. The number of variables is determiend from the truth table.

Parameters
  • tt – Truth table

  • bitcount – equals-k value

template<typename TT>
void create_symmetric(TT &tt, uint64_t counts)

Constructs symmetric function.

Bits in counts are numbered from 0 to 63. If bit i is set in counts, the created truth table will evaluate to true, if i bits are set in the input assignment.

Parameters
  • tt – Truth table

  • counts – Bitcount mask

template<typename TT, typename = std::enable_if_t<is_complete_truth_table<TT>::value>>
void create_parity(TT &tt)

Constructs parity function over n variables.

The number of variables is determined from the truth table.

Parameters

tt – Truth table

template<typename TT, typename = std::enable_if_t<is_complete_truth_table<TT>::value>>
bool create_from_chain(TT &tt, const std::vector<std::string> &steps, std::string *error = nullptr)

Constructs truth table from Boolean chain.

If tt has \(n\) variables, then each string in steps is of the form

x<i> = x<j> <op> x<k>

where <i> is an increasing number starting from \(n + 1\), and <j> and <k> refer to previous steps or primary inputs where \(j < i\) and \(k < i\). Primary inputs are indexed from \(1\) to \(n\). The last computed step will be assigned to tt. The following operators are supported:

<op>

Operation

Truth table

"!|"

Nondisjunction

0001

">"

Nonimplication

0010

"<"

Converse nonimplication

0100

"^"

Exclusive disjunction

0110

"!&"

Nonconjunction

0111

"&"

Conjunction

1000

"="

Equivalence

1001

">="

Nonimplication

1011

"<="

Implication

1101

"|"

Disjunction

1110

The following example will generate the majority function:

kitty::static_truth_table<3> tt;
kitty::create_from_chain( tt, {"x4 = x1 & x2",
                               "x5 = x1 & x3",
                               "x6 = x2 & x3",
                               "x7 = x4 | x5",
                               "x8 = x6 | x7"} );

If parsing fails, the function returns false, and if error is not nullptr, it contains a descriptive reason, why parsing failed. Otherwise, the function returns true.

Parameters
  • tt – Truth table

  • steps – Vector of steps

  • error – If not null, a pointer to store the error message

Returns

True on success

template<typename TT, typename = std::enable_if_t<is_complete_truth_table<TT>::value>>
bool create_multiple_from_chain(unsigned num_vars, std::vector<TT> &tts, const std::vector<std::string> &steps, std::string *error = nullptr)

Constructs truth tables from Boolean chain.

Like create_from_chain, but also returns all internally computed steps.

Parameters
  • num_vars – Number of input variables

  • tts – Truth table for all steps, tt[i] corresponds to step x \((i + 1)\)

  • steps – Vector of steps

  • error – If not null, a pointer to store the error message

Returns

True on success

template<typename TT, typename = std::enable_if_t<is_complete_truth_table<TT>::value>>
bool create_from_chain(TT &tt, std::istream &in, std::string *error = nullptr)

Constructs truth table from Boolean chain.

Like the other create_from_chain function, but reads chain from an input stream instead of a vector of strings. Lines are separated by a new line. Empty lines are skipped over.

Parameters
  • tt – Truth table

  • in – Input stream to read chain

  • error – If not null, a pointer to store the error message

Returns

True on success

template<typename TT, typename = std::enable_if_t<is_complete_truth_table<TT>::value>>
bool create_multiple_from_chain(unsigned num_vars, std::vector<TT> &tts, std::istream &in, std::string *error = nullptr)

Constructs truth tables from Boolean chain.

Like create_from_chain, but also returns all internally computed steps.

Parameters
  • num_vars – Number of input variables

  • tts – Truth table for all steps, tt[i] corresponds to step x \((i + 1)\)

  • in – Input stream to read chain

  • error – If not null, a pointer to store the error message

Returns

True on success

template<typename TT, typename TTFrom, typename = std::enable_if_t<is_complete_truth_table<TT>::value>>
inline void create_characteristic(TT &tt, const TTFrom &from)

Creates characteristic function.

Creates the truth table of the characteristic function, which contains one additional variable. The new output variable will be the most-significant variable of the new function.

Parameters
  • tt – Truth table for characteristic function

  • from – Input truth table

template<typename TT, typename = std::enable_if_t<is_complete_truth_table<TT>::value>>
bool create_from_expression(TT &tt, const std::string &expression, std::vector<TT> const &input_tts)

Creates truth table from textual expression.

An expression E is a constant 0 or 1, or a truth table a, b, …, p from the vector input_tts, the negation of an expression !E, the conjunction of multiple expressions (E...E), the disjunction of multiple expressions {E...E}, the exclusive OR of multiple expressions [E...E], or the majority of three expressions <EEE>.

Parameters
  • tt – Truth table

  • from – Expression as string

  • input_tts – Input truth tables assigned to a, b, …

template<typename TT, typename = std::enable_if_t<is_complete_truth_table<TT>::value>>
bool create_from_expression(TT &tt, const std::string &expression)

Creates truth table from textual expression.

An expression E is a constant 0 or 1, or a variable a, b, …, p, the negation of an expression !E, the conjunction of multiple expressions (E...E), the disjunction of multiple expressions {E...E}, the exclusive OR of multiple expressions [E...E], or the majority of three expressions <EEE>. Examples are [(ab)(!ac)] to describe if-then-else, or !{!a!b} to describe the application of De Morgan’s law to (ab). The size of the truth table must fit the largest variable in the expression, e.g., if c is the largest variable, then the truth table have at least three variables.

Parameters
  • tt – Truth table

  • from – Expression as string

template<typename TT, typename = std::enable_if_t<is_complete_truth_table<TT>::value>>
bool create_from_formula(TT &tt, const std::string &expression, const std::vector<std::string> &var_names)

Creates a truth table from a Boolean formula.

Translates a Boolean expression to a truth table with the variable names and ordering defined by var_names. The supported Boolean operations are the negation !a or a', the conjunction a*b or a&b or a b, the disjunction a+b, or a|b, and the exclusive OR a^b. Brackets () can be used for the operation order.

Parameters
  • tt – Truth table

  • from – Expression as string

  • input_tts – Variable names

template<class TT, typename = std::enable_if_t<is_complete_truth_table<TT>::value>>
void create_prime(TT &tt)

Creates function where on-set corresponds to prime numbers.

This creates a function in which \(f(x) = 1\), if and only if \(x\) is a prime number in its integer representation. The function only works for truth tables with at most 10 variables. The number of variables is determined from the truth table.

Parameters

tt – Truth table

inline void print_cubes(const std::vector<cube> &cubes, unsigned length = 32u, std::ostream &os = std::cout)

Prints all cubes in a vector.

Parameters
  • cubes – Vector of cubes

  • length – Number of variables in each cube

  • os – Output stream

template<class TT>
top_decomposition is_top_decomposable(const TT &tt, uint32_t var_index, TT *func = nullptr, bool allow_xor = true)

Checks, whether function is top disjoint decomposable.

Checks whether the input function tt can be represented by the function \(f = g(h(X_1), a)\), where \(a \notin X_1\). The return value is \(g\):

  • top_decomposition::and_: \(g = a \land h(X_1)\)

  • top_decomposition::or_: \(g = a \lor h(X_1)\)

  • top_decomposition::lt_: \(g = \bar a \land h(X_1)\)

  • top_decomposition::le_: \(g = \bar a \lor h(X_1)\)

  • top_decomposition::xor_: \(g = a \oplus h(X_1)\)

  • top_decomposition::none: decomposition does not exist

The function can return the remainder function \(h\), whic will not depend on \(a\).

Parameters
  • tt – Input function \(f\)

  • var_index – Variable \(a\)

  • func – If not null and decomposition exists, its value is assigned the remainder \(h\)

  • allow_xor – Set to false to disable XOR decomposition

template<class TT>
bottom_decomposition is_bottom_decomposable(const TT &tt, uint32_t var_index1, uint32_t var_index2, TT *func = nullptr, bool allow_xor = true)

Checks, whether function is bottom disjoint decomposable.

Checks whether the input function tt can be represented by the function \(f = h(X_1, g(a, b))\), where \(a, b \notin X_1\). The return value is \(g\):

  • bottom_decomposition::and_: \(g = a \land b\)

  • bottom_decomposition::or_: \(g = a \lor b\)

  • bottom_decomposition::lt_: \(g = \bar a \land b\)

  • bottom_decomposition::le_: \(g = \bar a \lor b\)

  • bottom_decomposition::xor_: \(g = a \oplus b\)

  • bottom_decomposition::none: decomposition does not exist

The function can return the remainder function \(h\) in where \(g\) is substituted by \(a\). The remainder function will not depend on \(b\).

Parameters
  • tt – Input function \(f\)

  • var_index1 – Variable \(a\)

  • var_index2 – Variable \(b\)

  • func – If not null and decomposition exists, its value is assigned the remainder \(h\)

  • allow_xor – Set to false to disable XOR decomposition

template<class TT>
std::tuple<TT, bi_decomposition, std::vector<TT>> is_bi_decomposable(const TT &tt, const TT &dc)

Checks whether a function is bi-decomposable.

Checks whether an incompletely specified function (ISF) tt can be represented by the function \(f = h(l(X_1, X_3), g(X_2, X_3))\). It returns a tuple of: 1. :math:’f’, which is a completely specified Boolean function compatible with the input ISF 2. :math:’h’, which is the type of decomposition (and, or, xor, weak and, weak or) 3. :math:’l’ and :math:’g’, given as ISF (ON-set and DC-set)

The algorithm is inspired by “An Algorithm for Bi-Decomposition of Logic Functions” by A. Mishchenko et al. presented in DAC 2001.

Parameters
  • tt – ON-set of the input function \(f\)

  • dc – DC-set of the input function \(f\)

template<class TT>
std::tuple<TT, bi_decomposition, std::vector<TT>> is_bi_decomposable_mc(const TT &tt, const TT &dc)

Checks whether a function is bi-decomposable using XOR as preferred operation.

Checks whether an incompletely specified function (ISF) tt can be represented by the function \(f = h(l(X_1, X_3), g(X_2, X_3))\). It returns a tuple of: 1. :math:’f’, which is a completely specified Boolean function compatible with the input ISF 2. :math:’h’, which is the type of decomposition (and, or, xor, weak and, weak or) 3. :math:’l’ and :math:’g’, given as ISF (ON-set and DC-set)

The algorithm is inspired by “An Algorithm for Bi-Decomposition of Logic Functions” by A. Mishchenko et al. presented in DAC 2001.

The cost is changed to add more XOR gates compared to AND/OR gates. This cost function is motivated by minimizing the number of AND gates in XAGs for cryptography and security applications. For these applications XOR gates are “free”.

Parameters
  • tt – ON-set of the input function \(f\)

  • dc – DC-set of the input function \(f\)

template<class TTf, class TTg, class TTh>
bool is_ashenhurst_decomposable(const TTf &tt, const std::vector<uint32_t> &zs_index, const std::vector<uint32_t> &ys_index, const TTg &outer_func, const TTh &inner_func)

Checks, whether a function is Ashenhurst decomposable.

Given functions f(.), g(.), and h(.) and a partition on arguments into z and y. This function determines whether f(x) is decomposable into g(z, h(y)) where x = union(z,y) and intersect(z, y) = null. This function does not check for permutation of variables given by zs_index and ys_index. The elements in these vectors are treated as ordered values.

Parameters
  • tt – The function to the check the decomposition on (function f)

  • zs_index – The ordered set of indices of vector x (input to f) that are the inputs to outer_func (g).

  • ys_index – The ordered set of indices of vector x (input to f) that are input to the inner_func (h).

  • outer_func – The outer decomposition function (function g).

  • inner_func – The inner decomposition function (function h).

Returns

true if the given decomposition is a valid one, false otherwise.

template<class TTf, class TTg, class TTh>
uint32_t ashenhurst_decomposition(const TTf &tt, const std::vector<uint32_t> &ys_index, std::vector<std::pair<TTg, TTh>> &decomposition)

Finds all of the possible Ashenhurst decompositions of a function given an input partitioning.

Parameters
  • tt – The function to find all of its decompositions

  • ys_index – Indices indicating the partitioning of inputs

  • decomposition – A vector of decomposition pairs. This serves as a return return container.

Returns

Returns the number of possible decompositions.

template<class TT, class CanonizationFn>
void fuller_neighborhood_enumeration(std::vector<TT> &functions, CanonizationFn &&canonization_fn)

Enumerate all representatives using 1-neighborhood search.

This function is based on Algorithm 4.2.1 in the PhD thesis “Analysis of Affine Equivalent Boolean Functions for Cryptography” by J.E. Fuller (Queensland University of Technology)

Parameters
  • functions – Vector must be initialized with single seed function, will contain all enumerated functions after call

  • canonization_fn – A canonization function, which takes as input a truth table and returns a truth table

template<typename TT>
inline std::vector<cube> esop_from_optimum_pkrm(const TT &tt)

Computes ESOP representation using optimum PKRM.

This algorithm first computes an ESOP using the algorithm described in [R. Drechsler, IEEE Trans. C 48(9), 1999, 987–990].

The algorithm applies post-optimization to merge distance-1 cubes.

Parameters

tt – Truth table

template<typename TT>
inline std::vector<cube> esop_from_pprm_slow(const TT &tt)
template<class TT>
std::vector<cube> esop_from_pprm(const TT &func)

Computes PPRM representation for a function.

This algorithm applies recursively the positive Davio decomposition which eventually leads into the PPRM representation of a function.

Parameters

tt – Truth table

inline std::size_t hash_block(uint64_t word)

Hash function for 64-bit word.

inline void hash_combine(std::size_t &seed, std::size_t other)

Combines two hash values.

template<typename TT>
std::vector<uint32_t> get_minterms(const TT &tt)

Computes all minterms.

Parameters

tt – Truth table

inline std::vector<std::pair<std::vector<uint32_t>::const_iterator, std::vector<uint32_t>::const_iterator>> get_jbuddies(const std::vector<uint32_t> &minterms, uint32_t j)

Computes all j-buddies in a list of minterms.

Computes all pairs \((k, k')\) such that \(k < k'\) and the two minterms at indexes \(k\) and \(k'\) only differ in bit \(j\).

This algorithm is described by Knuth in Exercise TAOCP 7.1.1-29.

Parameters
  • minterms – Vector of minterms

  • j – Bit position

inline std::vector<cube> get_prime_implicants_morreale(const std::vector<uint32_t> &minterms, unsigned num_vars)

Computes all prime implicants (from minterms)

This algorithm computes all prime implicants for a list of minterms. The running time is at most proportional to \(mn\), where \(m\) is the number of minterms and \(n\) is the number of variables.

The algorithm is described in Exercise TAOCP 7.1.1-30 by Knuth and is inspired by the algorithm described in [E. Morreale, IEEE Trans. EC 16(5), 1967, 611–620].

Parameters
  • minterms – Vector of minterms (as integer values)

  • num_vars – Number of variables

template<typename TT>
std::vector<cube> get_prime_implicants_morreale(const TT &tt)

Computes all prime implicants (from truth table)

Computes minterms from truth table and calls overloaded function.

Parameters

tt – Truth table

template<typename TT>
inline std::vector<cube> isop(const TT &tt)

Computes ISOP representation.

Computes the irredundant sum-of-products representation using the Minato-Morreale algorithm [S. Minato, IEEE Trans. CAD 15(4), 1996, 377-384].

Parameters

tt – Truth table

template<typename TT, typename Callback = decltype(detail::exact_npn_canonization_null_callback<TT>)>
std::tuple<TT, uint32_t, std::vector<uint8_t>> exact_p_canonization(const TT &tt, Callback &&fn = detail::exact_npn_canonization_null_callback<TT>)

Exact P canonization.

Given a truth table, this function finds the lexicographically smallest truth table in its P class, called P representative. Two functions are in the same P class, if one can obtain one from the other by input permutation.

The function can accept a callback as second parameter which is called for every visited function when trying out all combinations. This allows to exhaustively visit the whole P class.

The function returns a NPN configuration which contains the necessary transformations to obtain the representative. It is a tuple of

  • the P representative

  • input negations and output negation, which is 0 in this case

  • input permutation to apply

Parameters
  • tt – The truth table

  • fn – Callback for each visited truth table in the class (default does nothing)

Returns

NPN configuration

template<typename TT, typename Callback = decltype(detail::exact_npn_canonization_null_callback<TT>)>
std::tuple<TT, uint32_t, std::vector<uint8_t>> exact_npn_canonization(const TT &tt, Callback &&fn = detail::exact_npn_canonization_null_callback<TT>)

Exact NPN canonization.

Given a truth table, this function finds the lexicographically smallest truth table in its NPN class, called NPN representative. Two functions are in the same NPN class, if one can obtain one from the other by input negation, input permutation, and output negation.

The function can accept a callback as second parameter which is called for every visited function when trying out all combinations. This allows to exhaustively visit the whole NPN class.

The function returns a NPN configuration which contains the necessary transformations to obtain the representative. It is a tuple of

  • the NPN representative

  • input negations and output negation, output negation is stored as bit n, where n is the number of variables in tt

  • input permutation to apply

Parameters
  • tt – The truth table (with at most 6 variables)

  • fn – Callback for each visited truth table in the class (default does nothing)

Returns

NPN configuration

template<typename TT, typename Callback = decltype(detail::exact_npn_canonization_null_callback<TT>)>
std::tuple<TT, uint32_t> exact_n_canonization(const TT &tt, Callback &&fn = detail::exact_npn_canonization_null_callback<TT>)

Exact N canonization.

Given a truth table, this function finds the lexicographically smallest truth table in its N class, called N representative. Two functions are in the same N class, if one can obtain one from the other by input negations.

The function can accept a callback as second parameter which is called for every visited function when trying out all combinations. This allows to exhaustively visit the whole N class.

The function returns a N configuration which contains the necessary transformations to obtain the representative. It is a tuple of

  • the N representative

  • input negations that lead to the representative

Parameters
  • tt – The truth table

  • fn – Callback for each visited truth table in the class (default does nothing)

Returns

N configurations

template<typename TT>
std::tuple<TT, uint32_t, std::vector<uint8_t>> flip_swap_npn_canonization(const TT &tt)

Flip-swap NPN heuristic.

This algorithm will iteratively try to reduce the numeric value of the truth table by first inverting each input, then inverting the output, and then swapping each pair of inputs. Every improvement is accepted, the algorithm stops, if no more improvement can be achieved.

The function returns a NPN configuration which contains the necessary transformations to obtain the representative. It is a tuple of

  • the NPN representative

  • input negations and output negation, output negation is stored as bit n, where n is the number of variables in tt

  • input permutation to apply

Parameters

tt – Truth table

Returns

NPN configuration

template<typename TT>
std::tuple<TT, uint32_t, std::vector<uint8_t>> sifting_npn_canonization(const TT &tt)

Sifting NPN heuristic.

The algorithm will always consider two adjacent variables and try all possible transformations on these two. It will try once in forward direction and once in backward direction. It will try for the regular function and inverted function.

The function returns a NPN configuration which contains the necessary transformations to obtain the representative. It is a tuple of

  • the NPN representative

  • input negations and output negation, output negation is stored as bit n, where n is the number of variables in tt

  • input permutation to apply

Parameters

tt – Truth table

Returns

NPN configuration

template<typename TT>
std::tuple<TT, uint32_t, std::vector<uint8_t>> sifting_p_canonization(const TT &tt)

Sifting P heuristic.

The algorithm will always consider two adjacent variables and try all possible transformations on these two. It will try once in forward direction and once in backward direction. It will try for the regular function.

The function returns a P configuration which contains the necessary transformations to obtain the representative. It is a tuple of

  • the P representative

  • input negations and output negation, which is 0 in this case

  • input permutation to apply

Parameters

tt – Truth table

Returns

NPN configuration

template<typename TT, typename Callback>
void exact_np_enumeration(const TT &tt, Callback &&fn)

Exact NP enumeration.

Given a truth table, this function enumerates all the functions in its NP class. Two functions are in the same NP class, if one can be obtained from the other by input negation and input permutation.

The function takes a callback as second parameter which is called for every enumerated function. The callback should take as parameters:

  • NP-enumerated truth table

  • input negations

  • input permutation to apply

Parameters
  • tt – Truth table

  • fn – Callback for each enumerated truth table in the NP class

template<typename TT, typename Callback>
void exact_p_enumeration(const TT &tt, Callback &&fn)

Exact P enumeration.

Given a truth table, this function enumerates all the functions in its P class. Two functions are in the same P class, if one can be obtained from the other by input permutation.

The function takes a callback as second parameter which is called for every enumerated function. The callback should take as parameters:

  • P-enumerated truth table

  • input permutation to apply

Parameters
  • tt – Truth table

  • fn – Callback for each enumerated truth table in the P class

template<typename TT, typename Callback>
void exact_n_enumeration(const TT &tt, Callback &&fn)

Exact N enumeration.

Given a truth table, this function enumerates all the functions in its N class. Two functions are in the same N class, if one can be obtained from the other by input negation.

The function takes a callback as second parameter which is called for every enumerated function. The callback should take as parameters:

  • N-enumerated truth table

  • input negation to apply

Parameters
  • tt – Truth table

  • fn – Callback for each enumerated truth table in the N class

template<typename TT, typename Callback = decltype(detail::exact_npn_canonization_null_callback<TT>)>
std::tuple<TT, std::vector<uint32_t>> exact_n_canonization_complete(const TT &tt, Callback &&fn = detail::exact_npn_canonization_null_callback<TT>)

Exact N canonization complete.

Given a truth table, this function finds the lexicographically smallest truth table in its N class, called N representative. Two functions are in the same N class, if one can obtain one from the other by input negations.

The function can accept a callback as second parameter which is called for every visited function when trying out all combinations. This allows to exhaustively visit the whole N class.

The function returns all the N configurations which contains the necessary transformations to obtain the representative. It is a tuple of

  • the N representative

  • a vector of all input negations that lead to the representative

Parameters
  • tt – The truth table

  • fn – Callback for each visited truth table in the class (default does nothing)

Returns

N configurations

template<typename TT>
TT create_from_npn_config(const std::tuple<TT, uint32_t, std::vector<uint8_t>> &config)

Obtain truth table from NPN configuration.

Given an NPN configuration, which contains a representative function, input/output negations, and input permutations this function computes the original truth table.

Parameters

config – NPN configuration

template<typename TT>
inline TT unary_not(const TT &tt)

Inverts all bits in a truth table.

template<typename TT>
inline TT unary_not_if(const TT &tt, bool cond)

Inverts all bits in a truth table, based on a condition

template<typename TT>
inline TT binary_and(const TT &first, const TT &second)

Bitwise AND of two truth tables.

template<typename TT>
inline TT binary_or(const TT &first, const TT &second)

Bitwise OR of two truth tables.

template<typename TT>
inline TT binary_xor(const TT &first, const TT &second)

Bitwise XOR of two truth tables.

template<typename TT>
inline TT ternary_majority(const TT &first, const TT &second, const TT &third)

Ternary majority of three truth tables.

template<typename TT>
inline TT ternary_ite(const TT &first, const TT &second, const TT &third)

Performs ternary if-then-else of three truth tables.

Parameters
  • first – Truth table for condition

  • second – Truth table for then-case

  • third – Truth table for else-case

template<typename TT>
inline TT mux_var(uint8_t var_index, const TT &then_, const TT &else_)

Muxes two truth tables based on a variable.

Parameters
  • var_index – Variable index

  • then_ – Truth table for the then-case

  • else_ – Truth table for the else-case

template<typename TT>
inline bool equal(const TT &first, const TT &second)

Checks whether two truth tables are equal.

Parameters
  • first – First truth table

  • second – Second truth table

template<typename TT>
inline bool implies(const TT &first, const TT &second)

Checks if first truth table implies a second truth table.

Parameters
  • first – First truth table

  • second – Second truth table

template<typename TT>
inline bool less_than(const TT &first, const TT &second)

Checks whether a truth table is lexicographically smaller than another.

Comparison is initiated from most-significant bit.

Parameters
  • first – First truth table

  • second – Second truth table

template<typename TT>
inline bool is_const0(const TT &tt)

Checks whether truth table is contant 0.

Parameters

tt – Truth table

template<typename TT, bool polarity1 = true, bool polarity2 = true>
bool intersection_is_empty(const TT &first, const TT &second)

Checks whether the intersection of two truth tables is empty.

Parameters
  • first – First truth table

  • second – Second truth table

  • polarity1 – Polarity of the first truth table

  • polarity2 – Polarity of the second truth table

template<typename TT, bool polarity1 = true, bool polarity2 = true, bool polarity3 = true>
bool intersection_is_empty(const TT &first, const TT &second, const TT &third)

Checks whether the intersection of three truth tables is empty.

Parameters
  • first – First truth table

  • second – Second truth table

  • third – Third truth table

  • polarity1 – Polarity of the first truth table

  • polarity2 – Polarity of the second truth table

  • polarity3 – Polarity of the first truth table

template<typename TT, typename = std::enable_if_t<is_complete_truth_table<TT>::value>>
bool has_var(const TT &tt, uint8_t var_index)

Checks whether truth table depends on given variable index.

Parameters
  • tt – Truth table

  • var_index – Variable index

template<typename TT>
void next_inplace(TT &tt)

Computes the next lexicographically larger truth table.

This methods updates tt to become the next lexicographically larger truth table. If tt is already the largest truth table, the updated truth table will contain all zeros.

Parameters

tt – Truth table

template<typename TT>
inline TT next(const TT &tt)

Returns the next lexicographically larger truth table.

Out-of-place variant for next_inplace.

Parameters

tt – Truth table

template<typename TT, typename = std::enable_if_t<is_complete_truth_table<TT>::value>>
void cofactor0_inplace(TT &tt, uint8_t var_index)

Computes co-factor with respect to 0.

Parameters
  • tt – Truth table

  • var_index – Variable index

template<typename TT>
TT cofactor0(const TT &tt, uint8_t var_index)

Returns co-factor with respect to 0.

Parameters
  • tt – Truth table

  • var_index – Variable index

template<typename TT, typename = std::enable_if_t<is_complete_truth_table<TT>::value>>
void cofactor1_inplace(TT &tt, uint8_t var_index)

Computes co-factor with respect to 1.

Parameters
  • tt – Truth table

  • var_index – Variable index

template<typename TT>
TT cofactor1(const TT &tt, uint8_t var_index)

Returns co-factor with respect to 1.

Parameters
  • tt – Truth table

  • var_index – Variable index

template<typename TT, typename = std::enable_if_t<is_complete_truth_table<TT>::value>>
void swap_adjacent_inplace(TT &tt, uint8_t var_index)

Swaps two adjacent variables in a truth table.

The function swaps variable var_index with var_index + 1. The function will change tt in-place. If tt should not be changed, one can use swap_adjacent instead.

Parameters
  • tt – Truth table

  • var_index – A variable

template<typename TT>
inline TT swap_adjacent(const TT &tt, uint8_t var_index)

Swaps two adjacent variables in a truth table.

The function swaps variable var_index with var_index + 1. The function will return a new truth table with the result.

Parameters
  • tt – Truth table

  • var_index – A variable

template<typename TT, typename = std::enable_if_t<is_complete_truth_table<TT>::value>>
void swap_inplace(TT &tt, uint8_t var_index1, uint8_t var_index2)

Swaps two variables in a truth table.

The function swaps variable var_index1 with var_index2. The function will change tt in-place. If tt should not be changed, one can use swap instead.

Parameters
  • tt – Truth table

  • var_index1 – First variable

  • var_index2 – Second variable

template<typename TT>
inline TT swap(const TT &tt, uint8_t var_index1, uint8_t var_index2)

Swaps two adjacent variables in a truth table.

The function swaps variable var_index1 with var_index2. The function will return a new truth table with the result.

Parameters
  • tt – Truth table

  • var_index1 – First variable

  • var_index2 – Second variable

template<typename TT, typename = std::enable_if_t<is_complete_truth_table<TT>::value>>
void flip_inplace(TT &tt, uint8_t var_index)

Flips a variable in a truth table.

The function flips variable var_index in tt. The function will change tt in-place. If tt should not be changed, one can use flip instead.

Parameters
  • tt – Truth table

  • var_index – A variable

template<typename TT>
inline TT flip(const TT &tt, uint8_t var_index)

Flips a variable in a truth table.

The function flips variable var_index in tt. The function will not change tt and return the result as a copy.

Parameters
  • tt – Truth table

  • var_index – A variable

template<typename TT, typename = std::enable_if_t<is_complete_truth_table<TT>::value>>
std::vector<uint8_t> min_base_inplace(TT &tt)

Reorders truth table to have minimum base.

This function will reorder variables, such that there are no “holes”. For example, the function \( x_0 \land x_2 \) will be changed to \( x_0 \land x_1 \) by swapping \( x_1 \) with \( x_2 \). That is all variables that are not in the functional support will be moved to the back. Note that the size of the truth table is not changed, because for static_truth_table one cannot compute it at compile-time.

The function changes the truth table and returns a vector with all variable indexes that were in the functional support of the original function.

Parameters

tt – Truth table

template<typename TT>
void expand_inplace(TT &tt, const std::vector<uint8_t> &support)

Expands truth table from minimum base to original based on support.

This is the inverse operation to min_base_inplace, where the support is used to swap variables back to their original positions.

Parameters
  • tt – Truth table

  • support – Original indexes of support variables

template<typename TT, typename TTFrom, typename = std::enable_if_t<is_complete_truth_table<TT>::value>>
void extend_to_inplace(TT &tt, const TTFrom &from)

Extends smaller truth table to larger one.

The most significant variables will not be in the functional support of the resulting truth table, but the method is helpful to align a truth table when being used with another one.

Parameters
  • tt – Larger truth table to create

  • from – Smaller truth table to copy from

template<uint32_t NumVars, typename TTFrom>
inline static_truth_table<NumVars> extend_to(const TTFrom &from)

Extends smaller truth table to larger static one.

This is an out-of-place version of extend_to_inplace that has the truth table as a return value. It only works for creating static truth tables. The template parameter NumVars must be equal or larger to the number of variables in from.

Parameters

from – Smaller truth table to copy from

template<typename TTFrom>
inline dynamic_truth_table extend_to(const TTFrom &from, unsigned num_vars)

Extends smaller truth table to larger dynamic one.

This is an out-of-place version of extend_to_inplace that has the truth table as a return value. It only works for creating dynamic truth tables. The parameter num_vars must be equal or larger to the number of variables in from.

Parameters

from – Smaller truth table to copy from

template<typename TT, typename TTFrom, typename = std::enable_if_t<is_complete_truth_table<TT>::value>>
void shrink_to_inplace(TT &tt, const TTFrom &from)

Shrinks larger truth table to smaller one.

The function expects that the most significant bits, which are cut off, are not in the functional support of the original function. Only then it is ensured that the resulting function is equivalent.

Parameters
  • tt – Smaller truth table to create

  • from – Larger truth table to copy from

template<uint32_t NumVars, typename TTFrom>
inline static_truth_table<NumVars> shrink_to(const TTFrom &from)

Shrinks larger truth table to smaller static one.

This is an out-of-place version of shrink_to that has the truth table as a return value. It only works for creating static truth tables. The template parameter NumVars must be equal or smaller to the number of variables in from.

Parameters

from – Smaller truth table to copy from

template<typename TTFrom>
inline dynamic_truth_table shrink_to(const TTFrom &from, unsigned num_vars)

Shrinks larger truth table to smaller dynamic one.

This is an out-of-place version of shrink_to that has the truth table as a return value. It only works for creating dynamic tables. The parameter num_vars must be equal or smaller to the number of variables in from.

Parameters

from – Smaller truth table to copy from

template<typename TT>
void shift_left_inplace(TT &tt, uint64_t shift)

Left-shift truth table.

Drops overflowing most-significant bits and fills up least-significant bits with zeroes.

Parameters
  • tt – Truth table

  • shift – Number of bits to shift

template<typename TT>
inline TT shift_left(const TT &tt, uint64_t shift)

Left-shift truth table.

Out-of-place variant of shift_left_inplace.

Parameters
  • tt – Truth table

  • shift – Number of bits to shift

template<typename TT>
void shift_right_inplace(TT &tt, uint64_t shift)

Right-shift truth table.

Drops overflowing least-significant bits and fills up most-significant bits with zeroes.

Parameters
  • tt – Truth table

  • shift – Number of bits to shift

template<typename TT>
inline TT shift_right(const TT &tt, uint64_t shift)

Right-shift truth table.

Out-of-place variant of shift_right_inplace.

Parameters
  • tt – Truth table

  • shift – Number of bits to shift

template<class TTf, class TTv, typename = std::enable_if_t<is_complete_truth_table<TTf>::value>>
inline auto compose_truth_table(const TTf &f, const std::vector<TTv> &vars)

Composes a truth table.

Given a function f, and a set of truth tables as arguments, computes the composed truth table. For example, if f(x1, x2) = 1001 and vars = {x1 = 1001, x2= 1010}, the function returns 1000. This function can be regarded as a general operator with arity vars.size() where the behavior of the operator is given by f.

Parameters
  • f – The outer function

  • vars – The ordered set of input variables

Returns

The composed truth table with vars.size() variables

template<typename TT, typename = std::enable_if_t<is_complete_truth_table<TT>::value>>
inline void shift_with_mask_inplace(TT &f, uint8_t mask)

Shifts a small truth table with respect to a mask.

This function only works for truth tables with up to 6 inputs. The function rearranges the variables according to a mask. For example, assume the 3-input truth table \( x_0 \land x_1 \), which is not defined on \( x_2 \). Applying this funtion with a mask 0b101 yields the function \( x_0 \land x_2 \), and the mask 0b110 yields the function \( x_1 \land x_2 \). The bits in the mask provide the new positions. It is important that the positions in the mask do not exceed the truth table size, since all operations are performed in-place and cannot change the number of variables of the truth table.

Parameters
  • tt – Truth table

  • mask – Shift mask

template<class TT>
inline TT shift_with_mask(const TT &f, uint8_t mask)

Shifts a small truth table with respect to a mask.

Out-of-place variant of shift_with_mask_inplace.

Parameters
  • tt – Truth table

  • mask – Shift mask

inline dynamic_truth_table operator~(const dynamic_truth_table &tt)

Operator for unary_not.

template<uint32_t NumVars>
inline static_truth_table<NumVars> operator~(const static_truth_table<NumVars> &tt)

Operator for unary_not.

inline partial_truth_table operator~(const partial_truth_table &tt)

Operator for unary_not.

inline dynamic_truth_table operator&(const dynamic_truth_table &first, const dynamic_truth_table &second)

Operator for binary_and.

template<uint32_t NumVars>
inline static_truth_table<NumVars> operator&(const static_truth_table<NumVars> &first, const static_truth_table<NumVars> &second)

Operator for binary_and.

inline partial_truth_table operator&(const partial_truth_table &first, const partial_truth_table &second)

Operator for binary_and.

inline void operator&=(dynamic_truth_table &first, const dynamic_truth_table &second)

Operator for binary_and and assign.

template<uint32_t NumVars>
inline void operator&=(static_truth_table<NumVars> &first, const static_truth_table<NumVars> &second)

Operator for binary_and and assign.

inline void operator&=(partial_truth_table &first, const partial_truth_table &second)

Operator for binary_and and assign.

inline dynamic_truth_table operator|(const dynamic_truth_table &first, const dynamic_truth_table &second)

Operator for binary_or.

template<uint32_t NumVars>
inline static_truth_table<NumVars> operator|(const static_truth_table<NumVars> &first, const static_truth_table<NumVars> &second)

Operator for binary_or.

inline partial_truth_table operator|(const partial_truth_table &first, const partial_truth_table &second)

Operator for binary_or.

inline void operator|=(dynamic_truth_table &first, const dynamic_truth_table &second)

Operator for binary_or and assign.

template<uint32_t NumVars>
inline void operator|=(static_truth_table<NumVars> &first, const static_truth_table<NumVars> &second)

Operator for binary_or and assign.

inline void operator|=(partial_truth_table &first, const partial_truth_table &second)

Operator for binary_or and assign.

inline dynamic_truth_table operator^(const dynamic_truth_table &first, const dynamic_truth_table &second)

Operator for binary_xor.

template<uint32_t NumVars>
inline static_truth_table<NumVars> operator^(const static_truth_table<NumVars> &first, const static_truth_table<NumVars> &second)

Operator for binary_xor.

inline partial_truth_table operator^(const partial_truth_table &first, const partial_truth_table &second)

Operator for binary_xor.

inline void operator^=(dynamic_truth_table &first, const dynamic_truth_table &second)

Operator for binary_xor and assign.

template<uint32_t NumVars>
inline void operator^=(static_truth_table<NumVars> &first, const static_truth_table<NumVars> &second)

Operator for binary_xor and assign.

inline void operator^=(partial_truth_table &first, const partial_truth_table &second)

Operator for binary_xor and assign.

inline bool operator==(const dynamic_truth_table &first, const dynamic_truth_table &second)

Operator for equal.

template<uint32_t NumVars>
inline bool operator==(const static_truth_table<NumVars> &first, const static_truth_table<NumVars> &second)

Operator for equal.

inline bool operator==(const partial_truth_table &first, const partial_truth_table &second)

Operator for equal.

inline bool operator!=(const dynamic_truth_table &first, const dynamic_truth_table &second)

Operator for not equals (!equal)

template<uint32_t NumVars>
inline bool operator!=(const static_truth_table<NumVars> &first, const static_truth_table<NumVars> &second)

Operator for not equals (!equal)

inline bool operator!=(const partial_truth_table &first, const partial_truth_table &second)

Operator for not equal.

inline bool operator<(const dynamic_truth_table &first, const dynamic_truth_table &second)

Operator for less_than.

template<uint32_t NumVars>
inline bool operator<(const static_truth_table<NumVars> &first, const static_truth_table<NumVars> &second)

Operator for less_than.

inline bool operator<(const partial_truth_table &first, const partial_truth_table &second)

Operator for less_than.

inline dynamic_truth_table operator<<(const dynamic_truth_table &tt, uint64_t shift)

Operator for left_shift.

template<uint32_t NumVars>
inline static_truth_table<NumVars> operator<<(const static_truth_table<NumVars> &tt, uint64_t shift)

Operator for left_shift.

inline partial_truth_table operator<<(const partial_truth_table &tt, uint64_t shift)

Operator for left_shift.

inline void operator<<=(dynamic_truth_table &tt, uint64_t shift)

Operator for left_shift_inplace.

template<uint32_t NumVars>
inline void operator<<=(static_truth_table<NumVars> &tt, uint64_t shift)

Operator for left_shift_inplace.

inline void operator<<=(partial_truth_table &tt, uint64_t shift)

Operator for left_shift_inplace.

inline dynamic_truth_table operator>>(const dynamic_truth_table &tt, uint64_t shift)

Operator for right_shift.

template<uint32_t NumVars>
inline static_truth_table<NumVars> operator>>(const static_truth_table<NumVars> &tt, uint64_t shift)

Operator for right_shift.

inline partial_truth_table operator>>(const partial_truth_table &tt, uint64_t shift)

Operator for right_shift.

inline void operator>>=(dynamic_truth_table &tt, uint64_t shift)

Operator for right_shift_inplace.

template<uint32_t NumVars>
inline void operator>>=(static_truth_table<NumVars> &tt, uint64_t shift)

Operator for right_shift_inplace.

inline void operator>>=(partial_truth_table &tt, uint64_t shift)

Operator for right_shift_inplace.

template<typename TT>
inline void delta_swap_inplace(TT &tt, uint64_t delta, const TT &omega)

Applies delta-swap operation.

The delta-swap operation swaps all position pairs \((i, i+\delta)\), for which \(\omega\) is set 1 at position \(i\).

See also Eq. 7.1.3-(69) in The Art of Computer Programming.

Parameters
  • tt – Truth table

  • delta – Index distance delta

  • omega – Enable mask

template<typename TT>
TT delta_swap(const TT &tt, uint64_t delta, const TT &omega)

Applies delta-swap operation.

Out-of-place variant for delta_swap_inplace.

template<typename TT>
void permute_with_masks_inplace(TT &tt, const std::vector<TT> &masks)

Permutes a truth table using a sequence of delta-swaps.

Masks is an array containing the \(\omega\) masks. The \(\delta\) values are chosen as increasing and decreasing powers of 2, as described in Eq. 7.1.3-(71) of The Art of Computer Programming.

Parameters
  • tt – Truth table

  • masks – Array of omega-masks

template<typename TT>
TT permute_with_masks(const TT &tt, const std::vector<TT> &masks)

Permutes a truth table using a sequence of delta-swaps.

Out-of-place variant of permute_with_masks_inplace.

template<typename TT>
std::vector<TT> compute_permutation_masks(const TT &tt, const std::vector<uint32_t> &permutation)

Computes permutation bitmasks.

These bitmasks can be used with the permute_with_masks algorithm. The algorithm to compute these masks is described in The Art of Computer Programming, Section 7.1.3 ‘Bit permutation in general’.

The input truth table can be arbitrary but is used to determine the type and size of of the returned permutation masks.

Parameters
  • tt – Base truth table to derive types and size

  • permutation – Permutation

template<typename TT>
void print_binary(const TT &tt, std::ostream &os = std::cout)

Prints truth table in binary representation.

The most-significant bit will be the first character of the string.

Parameters
  • tt – Truth table

  • os – Output stream

template<typename TT>
void print_hex(const TT &tt, std::ostream &os = std::cout)

Prints truth table in hexadecimal representation.

The most-significant bit will be the first character of the string.

Parameters
  • tt – Truth table

  • os – Output stream

template<typename TT>
void print_raw(const TT &tt, std::ostream &os)

Prints truth table in raw binary presentation (for file I/O)

This function is useful to store large truth tables in binary files or std::stringstream. Each word is stored into 8 characters.

Parameters
  • tt – Truth table

  • os – Output stream

template<typename TT>
inline std::string to_binary(const TT &tt)

Returns truth table as a string in binary representation.

Calls print_binary internally on a string stream.

Parameters

tt – Truth table

template<typename TT>
inline std::string to_hex(const TT &tt)

Returns truth table as a string in hexadecimal representation.

Calls print_hex internally on a string stream.

Parameters

tt – Truth table

template<typename TT, typename = std::enable_if_t<!std::is_same<TT, partial_truth_table>::value>>
void print_xmas_tree_for_function(const TT &tt, std::ostream &os = std::cout)

Prints minterms of a Boolean function in christmas tree pattern.

This function prints all minterms of a Boolean function and arranges them according to the christmas tree pattern as described in Section 7.2.1.6 in The Art of Computer Programming by Donald E. Knuth. Minterms from the off-set are printed in red, minterms from the on-set are printed in green.

Parameters
  • tt – Truth table

  • os – Output stream

template<class TT>
void print_xmas_tree_for_functions(uint32_t num_vars, const std::vector<std::pair<std::function<bool(TT const&)>, std::vector<int>>> &style_predicates = {}, std::ostream &os = std::cout)

Prints all Boolean functions of n variables in christmas tree pattern.

This function prints all Boolean functions of n variables and arranges them according to the christmas tree pattern as described in Section 7.2.1.6 in The Art of Computer Programming by Donald E. Knuth. Functions can be printed in different styles according to some properties.

Parameters
  • tt – Number of variables

  • style_predicates – Each pair has a predicate bool(TT const&) to check whether a certain property holds for the truth table the element in the tree represents. If this predicate evaluates to true, then the second element in the pair are indexes of style (ANSI term) to change the string in the output.

  • os – Output stream

template<typename TT, typename = std::enable_if_t<!std::is_same<TT, partial_truth_table>::value>>
std::string anf_to_expression(const TT &anf)

Creates an expression for an ANF form.

Parameters

anf – Truth table in ANF encoding

template<typename TT, typename = std::enable_if_t<is_complete_truth_table<TT>::value>>
std::pair<uint32_t, std::vector<uint32_t>> chow_parameters(const TT &tt)

Returns the Chow parameter of a function The Chow parameters is a set of values \(N(f), \Sigma(f)\), where \(N(f)\) is the size of the ON-set, and \(\Sigma(f)\) is the sum of all input assignments in the ON-set. For example for \(f = x_1 \lor x_2\) the function returns \((3, (2,2))\).

Parameters

tt – Truth table

template<typename TT, typename = std::enable_if_t<is_complete_truth_table<TT>::value>>
bool is_canalizing(const TT &tt)

Checks whether a function is canalizing.

Parameters

tt – Truth table

template<typename TT>
bool is_horn(const TT &tt)

Checks whether a function is Horn A function is Horn, if it can be represented using Horn clauses.

Parameters

tt – Truth table

template<typename TT>
bool is_krom(const TT &tt)

Checks whether a function is Krom A function is Krom, if it can be represented using Krom clauses.

Parameters

tt – Truth table

template<typename TT>
bool is_symmetric_in(const TT &tt, uint8_t var_index1, uint8_t var_index2)

Checks whether a function is symmetric in a pair of variables A function is symmetric in two variables, if it is invariant to swapping them.

Parameters
  • tt – Truth table

  • var_index1 – Index of first variable

  • var_index2 – Index of second variable

template<typename TT, typename = std::enable_if_t<is_complete_truth_table<TT>::value>>
bool is_monotone(const TT &tt)

Checks whether a function is monotone A function is monotone if f(x) ≤ f(y) whenever x ⊆ y.

Parameters

tt – Truth table

template<typename TT, typename = std::enable_if_t<is_complete_truth_table<TT>::value>>
bool is_selfdual(const TT &tt)

Checks whether a function is selfdual A function is selfdual if !f(x, y, …, z) = f(!x, !y, …, !z)

Parameters

tt – Truth table

template<typename TT>
bool is_normal(const TT &tt)

Checks if a function is normal A function is normal iff f(0, …, 0) = 0.

Parameters

tt – Truth table

template<typename TT, typename = std::enable_if_t<is_complete_truth_table<TT>::value>>
bool is_trivial(const TT &tt)

Checks if a function is trivial A function is trival if it is equal to (or the complement of) a variable or constant zero.

Parameters

tt – Truth table

template<typename TT, typename Fn>
void foreach_runlength(const TT &tt, Fn &&fn)

Generate runlength encoding of a function This function iterates through the bits of a function and calls a function for each runlength and value. For example, if this function is called for the AND function 1000, it will call fn first with arguments false and 3, and then a second time with arguments true, and 1.

Parameters
  • tt – Truth table

  • fn – Function of signature void(bool, uint32_t)

template<typename TT>
std::vector<uint32_t> runlength_pattern(const TT &tt)

Returns the runlength encoding pattern of a function This function does only count the lengths, e.g., for 1000 it will return {3, 1}, and so it does for the NAND function 0111.

Parameters

tt – Truth table

template<typename TT>
inline uint32_t polynomial_degree(const TT &tt)

Compute polynomial degree The polyomial degree is the number of variables in the largest monomial in the functoons ANF (PPRM).

Parameters

tt – Truth table

template<typename TT>
inline uint64_t absolute_distinguishing_power(const TT &tt)

Returns the absolute distinguishing power of a function The absolute distinguishing power of a function f is the number of distinguishing bit pair {i,j} such that f(i) != f(j).

Parameters

tt – Truth table

template<typename TT>
inline uint64_t relative_distinguishing_power(const TT &tt, const TT &target_tt)

Returns the relative distinguishing power of a function wrt. to a target function Quantifies the number of distinguishing bit pairs in the target function that can be distinguished by another function.

Parameters
  • tt – Truth table of function

  • target_tt – Truth table of target function

template<typename TT>
bool is_covered_with_divisors(TT const &target, std::vector<TT> const &divisors)

Return true iff each distinguishing bit pair of the target function is also distinguishable by the divisor functions.

Parameters
  • target – Truth table of the target functions

  • divisors – Truth tables of the divisor functions

template<typename TT, typename Callback = decltype(detail::exact_spectral_canonization_null_callback)>
inline TT exact_spectral_canonization(const TT &tt, Callback &&fn = detail::exact_spectral_canonization_null_callback)

Exact spectral canonization.

The function can be passed as second argument a callback that is called with a vector of spectral operations necessary to transform the input function into the representative.

Parameters
  • tt – Truth table

  • fn – Callback to retrieve list of transformations (optional)

template<typename TT, typename Callback = decltype(detail::exact_spectral_canonization_null_callback)>
inline std::pair<TT, bool> exact_spectral_canonization_limit(const TT &tt, unsigned step_limit, Callback &&fn = detail::exact_spectral_canonization_null_callback)

Exact spectral canonization (with recursion limit)

This function gets as additional argument a recursion limit. The canonization is stopped once this limit is reached and the current representative at this point is being returned. The return value is a pair, where the first entry is the representative, and the second entry indicates whether the solution is known to be exact or not.

A function can be passed as second argument that is callback called with a vector of spectral operations necessary to transform the input function into the representative.

Parameters
  • tt – Truth table

  • limit – Recursion limit

  • fn – Callback to retrieve list of transformations (optional)

template<typename TT, typename Callback = decltype(detail::exact_spectral_canonization_null_callback)>
inline TT hybrid_exact_spectral_canonization(const TT &tt, Callback &&fn = detail::exact_spectral_canonization_null_callback)

Exact spectral canonization (with Reed-Muller preprocessor)

A function can be passed as second argument that is callback called with a vector of spectral operations necessary to transform the input function into the representative.

The algorithm is based on the paper: M. Soeken, E. Testa, D.M. Miller: A hybrid spectral method for checking Boolean function equivalence, PACRIM 2019.

Parameters
  • tt – Truth table

  • fn – Callback to retrieve list of transformations (optional)

template<typename TT>
inline void print_spectrum(const TT &tt, std::ostream &os = std::cout)

Print spectral representation of a function in RW order.

Parameters
  • tt – Truth table

  • os – Output stream

template<typename TT>
inline std::vector<int32_t> rademacher_walsh_spectrum(const TT &tt)

Returns the Rademacher-Walsh spectrum of a truth table.

The order of coefficients is in the same order as input assignments to the truth table.

Parameters

tt – Truth table

template<typename TT>
inline std::vector<int32_t> autocorrelation_spectrum(const TT &tt)

Returns the autocorrelation spectrum of a truth table.

The autocorrelation spectrum gives an indication of the imbalance of all first order derivates of a Boolean function.

The spectral coefficient \(r(x)\) for input \(x \in \{0,1\}^n\) is computed by \(r(x) = \sum_{y\in\{0,1\}^n}\hat f(y)\hat f(x \oplus y)\), where \(\hat f\) is the \(\{-1,1\}\) encoding of the input function \(f\).

Parameters

tt – Truth table for input function \(f\)

inline std::vector<uint32_t> spectrum_distribution(const std::vector<int32_t> &spectrum)

Returns distribution of absolute spectrum coefficients.

This functions returns a vector with \(2^{n-1} + 1\) nonnegative entries, in which the entry at position \(i\) indicates how many coeffecients in the spectum have absolute value \(2i\). The compression is possible, since all spectra in this package have positive coefficients.

Parameters

spectrum – Spectrum

template<typename TT>
inline uint32_t get_spectral_class(const TT &tt)

Returns unique index for a spectral equivalence class.

This functions works for functions with up to 5 inputs. It uses the distribution of coefficients in the Rademacher Walsh spectrum, and in case of ambiguity also the coeffcienents in the auto-correlation spectrum. It does not compute the transformation sequences in order to get to the class representative and is therefore faster than canoninization.

Parameters

tt – Truth table

template<class TT>
TT spectral_representative(const TT &func)

Returns spectral representative using lookup.

This function returns the spectral representative for functions with up to 5 variables, but does not give the possibility to obtain the transformation sequence to obtain the function from the representative.

func Truth table for function with at most 5 variables.

inline std::pair<std::vector<cube>, std::vector<uint64_t>> simple_spp(const std::vector<cube> &esop, uint32_t num_vars)

Merges products in an ESOP into pseudo products.

Given, e.g., the two cubes abc and abd, this algorithm will combine them into a single cube ab(c+d). The term (c+d) is stored as a literal in the first argument of the result pair, starting free indexes after num_vars. Which literals are used is stored in the second argument of the result pair, as bitpattern over the original inputs.

Parameters
  • esop – ESOP form

  • num_vars – Number of variables in ESOP form

template<typename TT>
void create_from_spp(TT &tt, const std::vector<cube> &cubes, const std::vector<uint64_t> &sums)

Creates truth table from SPP.

This method is helpful to check which truth table is computed by an SPP form.

class cube
struct dynamic_truth_table
#include <dynamic_truth_table.hpp>

Truth table in which number of variables is known at runtime.

template<typename TT>
struct hash
#include <hash.hpp>

Computes hash values for truth tables.

template<>
struct hash<cube>
template<class TT>
struct is_complete_truth_table : public false_type
template<> dynamic_truth_table > : public true_type
template<> partial_truth_table > : public false_type
template<uint32_t NumVars> static_truth_table< NumVars > > : public true_type
template<class TT>
struct is_truth_table : public false_type
template<> dynamic_truth_table > : public true_type
template<> partial_truth_table > : public true_type
template<uint32_t NumVars> static_truth_table< NumVars > > : public true_type
struct partial_truth_table
#include <partial_truth_table.hpp>

Truth table with resizable, arbitrary number of bits

template<uint32_t NumVars, bool = (NumVars <= 6)>
struct static_truth_table
#include <static_truth_table.hpp>

Truth table in which number of variables is known at compile time.

We dispatch on the Boolean template parameter to distinguish between a small truth table (up to 6 variables) and a large truth table (more than 6 variables). A small truth table fits into a single block and therefore dedicated optimizations are possible.

template<uint32_t NumVars>
struct static_truth_table<NumVars, false>
#include <static_truth_table.hpp>

Truth table (more than 6 variables) in which number of variables is known at compile time.

template<uint32_t NumVars>
struct static_truth_table<NumVars, true>
#include <static_truth_table.hpp>

Truth table (for up to 6 variables) in which number of variables is known at compile time.

namespace detail

Functions

template<typename TT, typename = std::enable_if_t<is_complete_truth_table<TT>::value>>
bool formula_execute_operation(std::stack<TT> &truth_tables, unsigned const op)
inline std::vector<uint32_t> enumerate_zs_index(const std::vector<uint32_t> &ys_index, uint32_t max_index)

A helper function to enumerate missing indices.

Parameters
  • ys_index – A list of already selected indices

  • max_index – The maximum value for an index

Returns

Remaining indices

template<typename TT>
std::pair<TT, TT> compute_permutation_masks_pair(const TT &tt, std::vector<uint32_t> &left, std::vector<uint32_t> &right, unsigned step)
inline std::string to_binary(uint16_t value, uint32_t num_vars)
inline void print_xmas_tree(std::ostream &os, uint32_t num_vars, const std::vector<std::pair<std::function<bool(uint16_t)>, std::vector<int>>> &style_predicates = {})
inline void fast_hadamard_transform(std::vector<int32_t> &s, bool reverse = false)
inline std::vector<uint32_t> get_rw_coeffecient_order(uint32_t num_vars)
inline void exact_spectral_canonization_null_callback(const std::vector<spectral_operation> &operations)

Variables

static std::vector<uint64_t> spectral_repr[] = {{0x0}, {0x0}, {0x0, 0x8}, {0x00, 0x80, 0x88}, {0x0000, 0x8000, 0x8080, 0x0888, 0x8888, 0x2a80, 0xf888, 0x7888}, {0x00000000, 0x80000000, 0x80008000, 0x00808080, 0x80808080, 0x08888000, 0xaa2a2a80, 0x88080808, 0x2888a000, 0xf7788000, 0xa8202020, 0x08880888, 0xbd686868, 0xaa808080, 0x7e686868, 0x2208a208, 0x08888888, 0x88888888, 0xea404040, 0x2a802a80, 0x73d28c88, 0xea808080, 0xa28280a0, 0x13284c88, 0xa2220888, 0xaae6da80, 0x58d87888, 0x8c88ac28, 0x8880f880, 0x9ee8e888, 0x4268c268, 0x16704c80, 0x78888888, 0x4966bac0, 0x372840a0, 0x5208d288, 0x7ca00428, 0xf8880888, 0x2ec0ae40, 0xf888f888, 0x58362ec0, 0x0eb8f6c0, 0x567cea40, 0xf8887888, 0x78887888, 0xe72890a0, 0x268cea40, 0x6248eac0}}
template<class TT>
struct anf_spectrum
template<typename TT>
class miller_spectral_canonization_impl
struct spectral_operation
class spectrum