Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

NPN classification #8

Merged
merged 14 commits into from
Oct 18, 2017
2 changes: 1 addition & 1 deletion bench/CMakeLists.txt
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
file(GLOB FILENAMES *.cpp)

# No debugging and full optimization for benchmark test
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -O3 -DNODEBUG")
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -O2 -DNDEBUG")

set(BENCHMARK_ENABLE_TESTING OFF CACHE BOOL "Enable testing of the benchmark library." FORCE)
set(CMAKE_BUILD_TYPE "Release")
Expand Down
55 changes: 55 additions & 0 deletions bench/canonization.cpp
Original file line number Diff line number Diff line change
@@ -0,0 +1,55 @@
/* kitty: C++ truth table library
* Copyright (C) 2017 EPFL
*
* Permission is hereby granted, free of charge, to any person
* obtaining a copy of this software and associated documentation
* files (the "Software"), to deal in the Software without
* restriction, including without limitation the rights to use,
* copy, modify, merge, publish, distribute, sublicense, and/or sell
* copies of the Software, and to permit persons to whom the
* Software is furnished to do so, subject to the following
* conditions:
*
* The above copyright notice and this permission notice shall be
* included in all copies or substantial portions of the Software.
*
* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
* EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES
* OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
* NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT
* HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
* WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
* FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR
* OTHER DEALINGS IN THE SOFTWARE.
*/

#include <benchmark/benchmark.h>

#include <kitty/kitty.hpp>

using namespace kitty;

void BM_exact_npn_canonization_static( benchmark::State& state )
{
while ( state.KeepRunning() )
{
static_truth_table<6> tt;
create_from_hex_string( tt, "17cad20f55459c3f" );
exact_npn_canonization( tt );
}
}

void BM_exact_npn_canonization_dynamic( benchmark::State& state )
{
while ( state.KeepRunning() )
{
dynamic_truth_table tt( 6 );
create_from_hex_string( tt, "17cad20f55459c3f" );
exact_npn_canonization( tt );
}
}

BENCHMARK( BM_exact_npn_canonization_static );
BENCHMARK( BM_exact_npn_canonization_dynamic );

BENCHMARK_MAIN()
21 changes: 21 additions & 0 deletions bench/operations.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -105,6 +105,24 @@ void BM_bitwise_majority_func_dynamic( benchmark::State& state )
}
}

void BM_unary_not_ite_dynamic( benchmark::State& state )
{
while ( state.KeepRunning() )
{
dynamic_truth_table tt( state.range( 0 ) );
const auto tt_new = !get_bit( tt, 0 ) ? unary_not( tt ) : tt;
}
}

void BM_unary_not_if_dynamic( benchmark::State& state )
{
while ( state.KeepRunning() )
{
dynamic_truth_table tt( state.range( 0 ) );
const auto tt_new = unary_not_if( tt, get_bit( tt, 0 ) );
}
}

BENCHMARK_TEMPLATE( BM_bitwise_and_lambda_static, 5 );
BENCHMARK_TEMPLATE( BM_bitwise_and_lambda_static, 7 );
BENCHMARK_TEMPLATE( BM_bitwise_and_lambda_static, 9 );
Expand All @@ -123,4 +141,7 @@ BENCHMARK( BM_bitwise_and_std_dynamic )->Arg( 5 )->Arg( 7 )->Arg( 9 );
BENCHMARK( BM_bitwise_and_func_dynamic )->Arg( 5 )->Arg( 7 )->Arg( 9 );
BENCHMARK( BM_bitwise_majority_func_dynamic )->Arg( 5 )->Arg( 7 )->Arg( 9 );

BENCHMARK( BM_unary_not_ite_dynamic )->Arg( 5 )->Arg( 7 )->Arg( 9 );
BENCHMARK( BM_unary_not_if_dynamic )->Arg( 5 )->Arg( 7 )->Arg( 9 );

BENCHMARK_MAIN()
18 changes: 15 additions & 3 deletions docs/changelog.rst
Original file line number Diff line number Diff line change
Expand Up @@ -8,25 +8,37 @@ v0.1
* Data structures ``static_truth_table`` and ``dynamic_truth_table``
`#1 <https://github.com/msoeken/kitty/pull/1>`_

* Bit-access functions ``set_bit`` and ``get_bit``
* Bit functions: ``set_bit``, ``get_bit``, ``clear_bit``, ``clear``
`#1 <https://github.com/msoeken/kitty/pull/1>`_
`#8 <https://github.com/msoeken/kitty/pull/8>`_

* Constructors ``create_nth_var``, ``create_from_binary_string``, ``create_from_hex_string``, and ``create_majority``
`#1 <https://github.com/msoeken/kitty/pull/1>`_
`#4 <https://github.com/msoeken/kitty/pull/4>`_
`#5 <https://github.com/msoeken/kitty/pull/5>`_

* Unary and binary operations: ``unary_not``, ``binary_and``, ``binary_or``, and ``binary_xor``
* Unary and binary operations: ``unary_not``, ``unary_not_if``, ``binary_and``, ``binary_or``, and ``binary_xor``
`#2 <https://github.com/msoeken/kitty/pull/2>`_
`#8 <https://github.com/msoeken/kitty/pull/8>`_

* Ternary operations: ``ternary_majority`` and ``ternary_ite``
`#3 <https://github.com/msoeken/kitty/pull/3>`_

* Binary predicates: ``equal``
* Binary predicates: ``equal``, ``less_than``
`#4 <https://github.com/msoeken/kitty/pull/4>`_
`#8 <https://github.com/msoeken/kitty/pull/8>`_

* Operators: ``~``, ``==``, ``<``
`#8 <https://github.com/msoeken/kitty/pull/8>`_

* Swap adjacent variables: ``swap_adjacent_inplace``, ``swap_adjacent``
`#6 <https://github.com/msoeken/kitty/pull/6>`_

* Swap variables: ``swap_inplace``, ``swap``
`#8 <https://github.com/msoeken/kitty/pull/8>`_

* Flip variable: ``flip_inplace``, ``flip``
`#7 <https://github.com/msoeken/kitty/pull/7>`_

* NPN canonization: ``exact_npn_canonization``, ``create_from_npn_config``
`#8 <https://github.com/msoeken/kitty/pull/8>`_
10 changes: 10 additions & 0 deletions docs/reference.rst
Original file line number Diff line number Diff line change
Expand Up @@ -36,3 +36,13 @@ Operations

.. doxygenfile:: operations.hpp

Operators
---------

.. doxygenfile:: operators.hpp

Canonization
------------

.. doxygenfile:: canonization.hpp

18 changes: 18 additions & 0 deletions include/kitty/bit_operations.hpp
Original file line number Diff line number Diff line change
Expand Up @@ -92,4 +92,22 @@ void clear_bit( static_truth_table<NumVars, true>& tt, uint64_t index )
tt._bits &= ~( uint64_t( 1 ) << index );
}
/*! \endcond */

/*! Clears all bits.

\param tt Truth table
*/
template<typename TT>
void clear( TT& tt )
{
std::fill( std::begin( tt._bits ), std::end( tt._bits ), 0 );
}

/*! \cond PRIVATE */
template<int NumVars>
void clear( static_truth_table<NumVars, true>& tt )
{
tt._bits = 0;
}
/*! \endcond */
} // namespace kitty
194 changes: 194 additions & 0 deletions include/kitty/canonization.hpp
Original file line number Diff line number Diff line change
@@ -0,0 +1,194 @@
/* kitty: C++ truth table library
* Copyright (C) 2017 EPFL
*
* Permission is hereby granted, free of charge, to any person
* obtaining a copy of this software and associated documentation
* files (the "Software"), to deal in the Software without
* restriction, including without limitation the rights to use,
* copy, modify, merge, publish, distribute, sublicense, and/or sell
* copies of the Software, and to permit persons to whom the
* Software is furnished to do so, subject to the following
* conditions:
*
* The above copyright notice and this permission notice shall be
* included in all copies or substantial portions of the Software.
*
* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
* EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES
* OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
* NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT
* HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
* WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
* FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR
* OTHER DEALINGS IN THE SOFTWARE.
*/

#pragma once

#include <numeric>

#include "detail/constants.hpp"
#include "operators.hpp"

namespace kitty
{

/*! 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 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

\param tt The truth table
\return NPN configuration
*/
template<typename TT>
std::tuple<TT, uint32_t, std::vector<uint8_t>> exact_npn_canonization( const TT& tt )
{
const auto num_vars = tt.num_vars();

/* Special case for n = 0 */
if ( num_vars == 0 )
{
const auto bit = get_bit( tt, 0 );
return std::make_tuple( unary_not_if( tt, bit ), bit, std::vector<uint8_t>{} );
}

/* Special case for n = 1 */
if ( num_vars == 1 )
{
const auto bit1 = get_bit( tt, 1 );
return std::make_tuple( unary_not_if( tt, bit1 ), bit1 << 1, std::vector<uint8_t>{ 0 } );
}

assert( num_vars >= 2 && num_vars <= 6u );

auto t1 = tt, t2 = ~tt;
auto tmin = std::min( t1, t2 );
auto invo = tmin == t2;

const auto& swaps = detail::swaps[num_vars - 2u];
const auto& flips = detail::flips[num_vars - 2u];

int best_swap = -1;
int best_flip = -1;

for ( int i = 0; i < swaps.size(); ++i )
{
const auto pos = swaps[i];
swap_adjacent_inplace( t1, pos );
swap_adjacent_inplace( t2, pos );
if ( t1 < tmin || t2 < tmin )
{
best_swap = i;
tmin = std::min( t1, t2 );
invo = tmin == t2;
}
}

for ( int j = 0; j < flips.size(); ++j )
{
const auto pos = flips[j];
swap_adjacent_inplace( t1, 0 );
flip_inplace( t1, pos );
swap_adjacent_inplace( t2, 0 );
flip_inplace( t2, pos );
if ( t1 < tmin || t2 < tmin )
{
best_swap = -1;
best_flip = j;
tmin = std::min( t1, t2 );
invo = tmin == t2;
}

for ( int i = 0; i < swaps.size(); ++i )
{
const auto pos = swaps[i];
swap_adjacent_inplace( t1, pos );
swap_adjacent_inplace( t2, pos );
if ( t1 < tmin || t2 < tmin )
{
best_swap = i;
best_flip = j;
tmin = std::min( t1, t2 );
invo = tmin == t2;
}
}
}

std::vector<uint8_t> perm( num_vars );
std::iota( perm.begin(), perm.end(), 0u );

for ( auto i = 0; i <= best_swap; ++i )
{
const auto pos = swaps[i];
std::swap( perm[pos], perm[pos + 1] );
}

uint32_t phase = uint32_t( invo ) << num_vars;
for ( auto i = 0; i <= best_flip; ++i )
{
phase ^= 1 << flips[i];
}

return std::make_tuple( tmin, phase, perm );
}

/*! 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.

\param config NPN configuration
*/
template<typename TT>
TT create_from_npn_config( const std::tuple<TT, uint32_t, std::vector<uint8_t>>& config )
{
const auto& from = std::get<0>( config );
const auto& phase = std::get<1>( config );
auto perm = std::get<2>( config );
const auto num_vars = from.num_vars();

/* is output complemented? */
auto res = ( ( phase >> num_vars ) & 1 ) ? ~from : from;

/* input permutations */
for ( auto i = 0; i < num_vars; ++i )
{
if ( perm[i] == i ) continue;

int k = i;
while ( perm[k] != i )
{
++k;
}

swap_inplace( res, i, k );
std::swap( perm[i], perm[k] );
}

/* input complementations */
for ( auto i = 0; i < num_vars; ++i )
{
if ( ( phase >> i ) & 1 )
{
flip_inplace( res, i );
}
}


return res;
}

} // namespace kitty
Loading