From 9a513c603147be00bb7a825cd15d39927f1fb270 Mon Sep 17 00:00:00 2001 From: Mathias Soeken Date: Fri, 20 Oct 2017 16:32:51 +0200 Subject: [PATCH 1/9] Documentation. --- docs/changelog.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/changelog.rst b/docs/changelog.rst index ea79be5d..d085b5b2 100644 --- a/docs/changelog.rst +++ b/docs/changelog.rst @@ -12,7 +12,7 @@ v0.1 `#1 `_ `#8 `_ -* Constructors ``create_nth_var``, ``create_from_binary_string``, ``create_from_hex_string``, ``create_random``, and ``create_majority`` +* Constructors: ``create_nth_var``, ``create_from_binary_string``, ``create_from_hex_string``, ``create_random``, and ``create_majority`` `#1 `_ `#4 `_ `#5 `_ From e099d306a66ed79021489b3ec8528cd3098d2901 Mon Sep 17 00:00:00 2001 From: Mathias Soeken Date: Fri, 20 Oct 2017 16:33:08 +0200 Subject: [PATCH 2/9] Check whether function depends on variable with `has_var`. --- docs/changelog.rst | 3 ++ docs/operations.rst | 1 + include/kitty/detail/constants.hpp | 2 ++ include/kitty/operations.hpp | 47 +++++++++++++++++++++++++++++- test/operations.cpp | 21 +++++++++++++ 5 files changed, 73 insertions(+), 1 deletion(-) diff --git a/docs/changelog.rst b/docs/changelog.rst index d085b5b2..e8a81e63 100644 --- a/docs/changelog.rst +++ b/docs/changelog.rst @@ -29,6 +29,9 @@ v0.1 `#4 `_ `#8 `_ +* Predicates: ``has_var`` + `#11 `_ + * Operators: ``~``, ``==``, ``<`` `#8 `_ diff --git a/docs/operations.rst b/docs/operations.rst index 83f4686e..554174e6 100644 --- a/docs/operations.rst +++ b/docs/operations.rst @@ -19,6 +19,7 @@ Predicates .. doc_brief_table:: equal less_than + has_var Truth table combination and manipulation ---------------------------------------- diff --git a/include/kitty/detail/constants.hpp b/include/kitty/detail/constants.hpp index 2912094b..3b653fcd 100644 --- a/include/kitty/detail/constants.hpp +++ b/include/kitty/detail/constants.hpp @@ -37,6 +37,8 @@ namespace detail static constexpr uint64_t projections[] = {0xaaaaaaaaaaaaaaaa, 0xcccccccccccccccc, 0xf0f0f0f0f0f0f0f0, 0xff00ff00ff00ff00, 0xffff0000ffff0000, 0xffffffff00000000}; +static constexpr uint64_t projections_neg[] = {0x5555555555555555, 0x3333333333333333, 0x0f0f0f0f0f0f0f0f, 0x00ff00ff00ff00ff, 0x0000ffff0000ffff, 0x00000000ffffffff}; + static constexpr uint64_t masks[] = {0x0000000000000001, 0x0000000000000003, 0x000000000000000f, 0x00000000000000ff, 0x000000000000ffff, 0x00000000ffffffff, 0xffffffffffffffff}; static constexpr uint64_t permutation_masks[][3] = { diff --git a/include/kitty/operations.hpp b/include/kitty/operations.hpp index fc536d05..30e0d11b 100644 --- a/include/kitty/operations.hpp +++ b/include/kitty/operations.hpp @@ -281,6 +281,50 @@ inline bool less_than( const static_truth_table& first, const sta } /*! \endcond PRIVATE */ +/*! \brief Checks whether truth table depends on given variable index + + \param tt Truth table + \param var_index Variable index +*/ +template +bool has_var( const TT& tt, uint8_t var_index ) +{ + assert( var_index < tt.num_vars() ); + + if ( tt.num_vars() <= 6 || var_index < 6 ) + { + return std::any_of( std::begin( tt._bits ), std::end( tt._bits ), + [var_index]( uint64_t word ) { return ( ( word >> ( 1 << var_index ) ) & detail::projections_neg[var_index] ) != + ( word & detail::projections_neg[var_index] ); } ); + } + else + { + const auto step = 1 << ( var_index - 6 ); + for ( auto i = 0; i < tt.num_blocks(); i += 2 * step ) + { + for ( auto j = 0; j < step; ++j ) + { + if ( tt._bits[i + j] != tt._bits[i + j + step] ) + { + return true; + } + } + } + return false; + } +} + +/*! \cond PRIVATE */ +template +bool has_var( const static_truth_table& tt, uint8_t var_index ) +{ + assert( var_index < tt.num_vars() ); + + return ( ( tt._bits >> ( 1 << var_index ) ) & detail::projections_neg[var_index] ) != + ( tt._bits & detail::projections_neg[var_index] ); +} +/*! \endcond */ + /*! \brief Computes the next lexicographically larger truth table This methods updates `tt` to become the next lexicographically @@ -302,7 +346,8 @@ void next_inplace( TT& tt ) for ( auto i = 0; i < tt.num_blocks(); ++i ) { /* If incrementing the word does not lead to an overflow, we're done*/ - if ( ++tt._bits[i] != 0 ) break; + if ( ++tt._bits[i] != 0 ) + break; } } } diff --git a/test/operations.cpp b/test/operations.cpp index 14135d61..a69a3919 100644 --- a/test/operations.cpp +++ b/test/operations.cpp @@ -196,6 +196,27 @@ TEST_F( OperationsTest, comparisons ) EXPECT_FALSE( less_than( from_hex( 7, "e92c774439c72c8955906ef92ecefec9" ), from_hex( 7, "e92c774439c72c8955906ef92ebefec9" ) ) ); } +TEST_F( OperationsTest, support ) +{ + EXPECT_TRUE( has_var( from_hex<3>( "77" ), 0 ) ); + EXPECT_TRUE( has_var( from_hex<3>( "77" ), 1 ) ); + EXPECT_TRUE( !has_var( from_hex<3>( "77" ), 2 ) ); + + EXPECT_TRUE( has_var( from_hex( 3, "77" ), 0 ) ); + EXPECT_TRUE( has_var( from_hex( 3, "77" ), 1 ) ); + EXPECT_TRUE( !has_var( from_hex( 3, "77" ), 2 ) ); + + for ( auto i = 0; i < 8; ++i ) + { + EXPECT_EQ( has_var( from_hex<8>( "3333333333cc33cc3333333333cc33cc33cc33cccccccccc33cc33cccccccccc" ), i ), i % 2 == 1 ); + } + + for ( auto i = 0; i < 8; ++i ) + { + EXPECT_EQ( has_var( from_hex( 8, "3333333333cc33cc3333333333cc33cc33cc33cccccccccc33cc33cccccccccc" ), i ), i % 2 == 1 ); + } +} + TEST_F( OperationsTest, next ) { EXPECT_EQ( next( from_hex<3>( "00" ) ), from_hex<3>( "01" ) ); From b87fc9398aa27b81ad5eb0caa3d0124362c53cbf Mon Sep 17 00:00:00 2001 From: Mathias Soeken Date: Fri, 20 Oct 2017 18:10:16 +0200 Subject: [PATCH 3/9] Co-factors. --- docs/changelog.rst | 3 ++ docs/operations.rst | 4 ++ include/kitty/operations.hpp | 99 ++++++++++++++++++++++++++++++++++++ test/operations.cpp | 57 +++++++++++++++++++++ 4 files changed, 163 insertions(+) diff --git a/docs/changelog.rst b/docs/changelog.rst index e8a81e63..aa27e030 100644 --- a/docs/changelog.rst +++ b/docs/changelog.rst @@ -47,5 +47,8 @@ v0.1 * Enumerate truth tables: ``next_inplace``, ``next`` `#10 `_ +* Compute co-factors: ``cofactor0_inplace``, ``cofactor0``, ``cofactor1_inplace``, ``cofactor1`` + `#11 `_ + * NPN canonization: ``exact_npn_canonization``, ``create_from_npn_config`` `#8 `_ diff --git a/docs/operations.rst b/docs/operations.rst index 554174e6..7548a1f1 100644 --- a/docs/operations.rst +++ b/docs/operations.rst @@ -33,6 +33,10 @@ Truth table combination and manipulation ternary_majority next_inplace next + cofactor0_inplace + cofactor0 + cofactor1_inplace + cofactor1 swap_inplace swap swap_adjacent_inplace diff --git a/include/kitty/operations.hpp b/include/kitty/operations.hpp index 30e0d11b..5b916797 100644 --- a/include/kitty/operations.hpp +++ b/include/kitty/operations.hpp @@ -375,6 +375,105 @@ inline TT next( const TT& tt ) return copy; } +/*! \brief Computes co-factor with respect to 0 + + \param tt Truth table + \param var_index Variable index +*/ +template +void cofactor0_inplace( TT& tt, uint8_t var_index ) +{ + if ( tt.num_vars() <= 6 || var_index < 6 ) + { + std::transform( std::begin( tt._bits ), std::end( tt._bits ), + std::begin( tt._bits ), + [var_index]( uint64_t word ) { return ( ( word & detail::projections_neg[var_index] ) << ( 1 << var_index ) ) | + ( word & detail::projections_neg[var_index] ); } ); + } + else + { + const auto step = 1 << ( var_index - 6 ); + for ( auto i = 0; i < tt.num_blocks(); i += 2 * step ) + { + for ( auto j = 0; j < step; ++j ) + { + tt._bits[i + j + step] = tt._bits[i + j]; + } + } + } +} + +/*! \cond PRIVATE */ +template +void cofactor0_inplace( static_truth_table& tt, uint8_t var_index ) +{ + tt._bits = ( ( tt._bits & detail::projections_neg[var_index] ) << ( 1 << var_index ) ) | + ( tt._bits & detail::projections_neg[var_index] ); +} +/*! \endcond */ + +/*! \brief Returns co-factor with respect to 0 + + \param tt Truth table + \param var_index Variable index +*/ +template +TT cofactor0( const TT& tt, uint8_t var_index ) +{ + auto copy = tt; + cofactor0_inplace( copy, var_index ); + return copy; +} + +/*! \brief Computes co-factor with respect to 1 + + \param tt Truth table + \param var_index Variable index +*/ +template +void cofactor1_inplace( TT& tt, uint8_t var_index ) +{ + if ( tt.num_vars() <= 6 || var_index < 6 ) + { + std::transform( std::begin( tt._bits ), std::end( tt._bits ), + std::begin( tt._bits ), + [var_index]( uint64_t word ) { return ( word & detail::projections[var_index] ) | + ( ( word & detail::projections[var_index] ) >> ( 1 << var_index ) ); } ); + } + else + { + const auto step = 1 << ( var_index - 6 ); + for ( auto i = 0; i < tt.num_blocks(); i += 2 * step ) + { + for ( auto j = 0; j < step; ++j ) + { + tt._bits[i + j] = tt._bits[i + j + step]; + } + } + } +} + +/*! \cond PRIVATE */ +template +void cofactor1_inplace( static_truth_table& tt, uint8_t var_index ) +{ + tt._bits = ( tt._bits & detail::projections[var_index] ) | ( ( tt._bits & detail::projections[var_index] ) >> ( 1 << var_index ) ); +} +/*! \endcond */ + +/*! \brief Returns co-factor with respect to 1 + + \param tt Truth table + \param var_index Variable index +*/ +template +TT cofactor1( const TT& tt, uint8_t var_index ) +{ + auto copy = tt; + cofactor1_inplace( copy, var_index ); + return copy; +} + /*! \brief Swaps two adjacent variables in a truth table The function swaps variable `var_index` with `var_index + 1`. The diff --git a/test/operations.cpp b/test/operations.cpp index a69a3919..dde596cf 100644 --- a/test/operations.cpp +++ b/test/operations.cpp @@ -236,6 +236,63 @@ TEST_F( OperationsTest, next ) EXPECT_EQ( next( from_hex( 7, "ffffffffffffffffffffffffffffffff" ) ), from_hex( 7, "00000000000000000000000000000000" ) ); } +TEST_F( OperationsTest, cofactors ) +{ + EXPECT_EQ( cofactor0( from_hex<3>( "e8" ), 2 ), from_hex<3>( "88" ) ); + EXPECT_EQ( cofactor0( from_hex<3>( "e8" ), 1 ), from_hex<3>( "a0" ) ); + EXPECT_EQ( cofactor0( from_hex<3>( "e8" ), 0 ), from_hex<3>( "c0" ) ); + + EXPECT_EQ( cofactor0( from_hex( 3, "e8" ), 2 ), from_hex( 3, "88" ) ); + EXPECT_EQ( cofactor0( from_hex( 3, "e8" ), 1 ), from_hex( 3, "a0" ) ); + EXPECT_EQ( cofactor0( from_hex( 3, "e8" ), 0 ), from_hex( 3, "c0" ) ); + + // Co-factors of [(d){h}] + EXPECT_EQ( cofactor0( from_hex<8>( "17ff17ff17ff17ff17ff17ff17ff17ff17ff17ff17ffe80017ffe800e800e800" ), 0 ), from_hex<8>( "3fff3fff3fff3fff3fff3fff3fff3fff3fff3fff3fffc0003fffc000c000c000" ) ); + EXPECT_EQ( cofactor0( from_hex<8>( "17ff17ff17ff17ff17ff17ff17ff17ff17ff17ff17ffe80017ffe800e800e800" ), 1 ), from_hex<8>( "5fff5fff5fff5fff5fff5fff5fff5fff5fff5fff5fffa0005fffa000a000a000" ) ); + EXPECT_EQ( cofactor0( from_hex<8>( "17ff17ff17ff17ff17ff17ff17ff17ff17ff17ff17ffe80017ffe800e800e800" ), 2 ), from_hex<8>( "77ff77ff77ff77ff77ff77ff77ff77ff77ff77ff77ff880077ff880088008800" ) ); + EXPECT_EQ( cofactor0( from_hex<8>( "17ff17ff17ff17ff17ff17ff17ff17ff17ff17ff17ffe80017ffe800e800e800" ), 3 ), from_hex<8>( "ffffffffffffffffffffffffffffffffffffffffffff0000ffff000000000000" ) ); + EXPECT_EQ( cofactor0( from_hex<8>( "17ff17ff17ff17ff17ff17ff17ff17ff17ff17ff17ffe80017ffe800e800e800" ), 4 ), from_hex<8>( "17ff17ff17ff17ff17ff17ff17ff17ff17ff17ffe800e800e800e800e800e800" ) ); + EXPECT_EQ( cofactor0( from_hex<8>( "17ff17ff17ff17ff17ff17ff17ff17ff17ff17ff17ffe80017ffe800e800e800" ), 5 ), from_hex<8>( "17ff17ff17ff17ff17ff17ff17ff17ff17ffe80017ffe800e800e800e800e800" ) ); + EXPECT_EQ( cofactor0( from_hex<8>( "17ff17ff17ff17ff17ff17ff17ff17ff17ff17ff17ffe80017ffe800e800e800" ), 6 ), from_hex<8>( "17ff17ff17ff17ff17ff17ff17ff17ff17ffe800e800e80017ffe800e800e800" ) ); + EXPECT_EQ( cofactor0( from_hex<8>( "17ff17ff17ff17ff17ff17ff17ff17ff17ff17ff17ffe80017ffe800e800e800" ), 7 ), from_hex<8>( "17ff17ff17ffe80017ffe800e800e80017ff17ff17ffe80017ffe800e800e800" ) ); + + EXPECT_EQ( cofactor0( from_hex( 8, "17ff17ff17ff17ff17ff17ff17ff17ff17ff17ff17ffe80017ffe800e800e800" ), 0 ), from_hex( 8, "3fff3fff3fff3fff3fff3fff3fff3fff3fff3fff3fffc0003fffc000c000c000" ) ); + EXPECT_EQ( cofactor0( from_hex( 8, "17ff17ff17ff17ff17ff17ff17ff17ff17ff17ff17ffe80017ffe800e800e800" ), 1 ), from_hex( 8, "5fff5fff5fff5fff5fff5fff5fff5fff5fff5fff5fffa0005fffa000a000a000" ) ); + EXPECT_EQ( cofactor0( from_hex( 8, "17ff17ff17ff17ff17ff17ff17ff17ff17ff17ff17ffe80017ffe800e800e800" ), 2 ), from_hex( 8, "77ff77ff77ff77ff77ff77ff77ff77ff77ff77ff77ff880077ff880088008800" ) ); + EXPECT_EQ( cofactor0( from_hex( 8, "17ff17ff17ff17ff17ff17ff17ff17ff17ff17ff17ffe80017ffe800e800e800" ), 3 ), from_hex( 8, "ffffffffffffffffffffffffffffffffffffffffffff0000ffff000000000000" ) ); + EXPECT_EQ( cofactor0( from_hex( 8, "17ff17ff17ff17ff17ff17ff17ff17ff17ff17ff17ffe80017ffe800e800e800" ), 4 ), from_hex( 8, "17ff17ff17ff17ff17ff17ff17ff17ff17ff17ffe800e800e800e800e800e800" ) ); + EXPECT_EQ( cofactor0( from_hex( 8, "17ff17ff17ff17ff17ff17ff17ff17ff17ff17ff17ffe80017ffe800e800e800" ), 5 ), from_hex( 8, "17ff17ff17ff17ff17ff17ff17ff17ff17ffe80017ffe800e800e800e800e800" ) ); + EXPECT_EQ( cofactor0( from_hex( 8, "17ff17ff17ff17ff17ff17ff17ff17ff17ff17ff17ffe80017ffe800e800e800" ), 6 ), from_hex( 8, "17ff17ff17ff17ff17ff17ff17ff17ff17ffe800e800e80017ffe800e800e800" ) ); + EXPECT_EQ( cofactor0( from_hex( 8, "17ff17ff17ff17ff17ff17ff17ff17ff17ff17ff17ffe80017ffe800e800e800" ), 7 ), from_hex( 8, "17ff17ff17ffe80017ffe800e800e80017ff17ff17ffe80017ffe800e800e800" ) ); + + EXPECT_EQ( cofactor1( from_hex<3>( "e8" ), 2 ), from_hex<3>( "ee" ) ); + EXPECT_EQ( cofactor1( from_hex<3>( "e8" ), 1 ), from_hex<3>( "fa" ) ); + EXPECT_EQ( cofactor1( from_hex<3>( "e8" ), 0 ), from_hex<3>( "fc" ) ); + + EXPECT_EQ( cofactor1( from_hex( 3, "e8" ), 2 ), from_hex( 3, "ee" ) ); + EXPECT_EQ( cofactor1( from_hex( 3, "e8" ), 1 ), from_hex( 3, "fa" ) ); + EXPECT_EQ( cofactor1( from_hex( 3, "e8" ), 0 ), from_hex( 3, "fc" ) ); + + // Co-factors of [(d){h}] + EXPECT_EQ( cofactor1( from_hex<8>( "17ff17ff17ff17ff17ff17ff17ff17ff17ff17ff17ffe80017ffe800e800e800" ), 0 ), from_hex<8>( "03ff03ff03ff03ff03ff03ff03ff03ff03ff03ff03fffc0003fffc00fc00fc00" ) ); + EXPECT_EQ( cofactor1( from_hex<8>( "17ff17ff17ff17ff17ff17ff17ff17ff17ff17ff17ffe80017ffe800e800e800" ), 1 ), from_hex<8>( "05ff05ff05ff05ff05ff05ff05ff05ff05ff05ff05fffa0005fffa00fa00fa00" ) ); + EXPECT_EQ( cofactor1( from_hex<8>( "17ff17ff17ff17ff17ff17ff17ff17ff17ff17ff17ffe80017ffe800e800e800" ), 2 ), from_hex<8>( "11ff11ff11ff11ff11ff11ff11ff11ff11ff11ff11ffee0011ffee00ee00ee00" ) ); + EXPECT_EQ( cofactor1( from_hex<8>( "17ff17ff17ff17ff17ff17ff17ff17ff17ff17ff17ffe80017ffe800e800e800" ), 3 ), from_hex<8>( "17171717171717171717171717171717171717171717e8e81717e8e8e8e8e8e8" ) ); + EXPECT_EQ( cofactor1( from_hex<8>( "17ff17ff17ff17ff17ff17ff17ff17ff17ff17ff17ffe80017ffe800e800e800" ), 4 ), from_hex<8>( "17ff17ff17ff17ff17ff17ff17ff17ff17ff17ff17ff17ff17ff17ffe800e800" ) ); + EXPECT_EQ( cofactor1( from_hex<8>( "17ff17ff17ff17ff17ff17ff17ff17ff17ff17ff17ffe80017ffe800e800e800" ), 5 ), from_hex<8>( "17ff17ff17ff17ff17ff17ff17ff17ff17ff17ff17ff17ff17ffe80017ffe800" ) ); + EXPECT_EQ( cofactor1( from_hex<8>( "17ff17ff17ff17ff17ff17ff17ff17ff17ff17ff17ffe80017ffe800e800e800" ), 6 ), from_hex<8>( "17ff17ff17ff17ff17ff17ff17ff17ff17ff17ff17ffe80017ff17ff17ffe800" ) ); + EXPECT_EQ( cofactor1( from_hex<8>( "17ff17ff17ff17ff17ff17ff17ff17ff17ff17ff17ffe80017ffe800e800e800" ), 7 ), from_hex<8>( "17ff17ff17ff17ff17ff17ff17ff17ff17ff17ff17ff17ff17ff17ff17ff17ff" ) ); + + EXPECT_EQ( cofactor1( from_hex( 8, "17ff17ff17ff17ff17ff17ff17ff17ff17ff17ff17ffe80017ffe800e800e800" ), 0 ), from_hex( 8, "03ff03ff03ff03ff03ff03ff03ff03ff03ff03ff03fffc0003fffc00fc00fc00" ) ); + EXPECT_EQ( cofactor1( from_hex( 8, "17ff17ff17ff17ff17ff17ff17ff17ff17ff17ff17ffe80017ffe800e800e800" ), 1 ), from_hex( 8, "05ff05ff05ff05ff05ff05ff05ff05ff05ff05ff05fffa0005fffa00fa00fa00" ) ); + EXPECT_EQ( cofactor1( from_hex( 8, "17ff17ff17ff17ff17ff17ff17ff17ff17ff17ff17ffe80017ffe800e800e800" ), 2 ), from_hex( 8, "11ff11ff11ff11ff11ff11ff11ff11ff11ff11ff11ffee0011ffee00ee00ee00" ) ); + EXPECT_EQ( cofactor1( from_hex( 8, "17ff17ff17ff17ff17ff17ff17ff17ff17ff17ff17ffe80017ffe800e800e800" ), 3 ), from_hex( 8, "17171717171717171717171717171717171717171717e8e81717e8e8e8e8e8e8" ) ); + EXPECT_EQ( cofactor1( from_hex( 8, "17ff17ff17ff17ff17ff17ff17ff17ff17ff17ff17ffe80017ffe800e800e800" ), 4 ), from_hex( 8, "17ff17ff17ff17ff17ff17ff17ff17ff17ff17ff17ff17ff17ff17ffe800e800" ) ); + EXPECT_EQ( cofactor1( from_hex( 8, "17ff17ff17ff17ff17ff17ff17ff17ff17ff17ff17ffe80017ffe800e800e800" ), 5 ), from_hex( 8, "17ff17ff17ff17ff17ff17ff17ff17ff17ff17ff17ff17ff17ffe80017ffe800" ) ); + EXPECT_EQ( cofactor1( from_hex( 8, "17ff17ff17ff17ff17ff17ff17ff17ff17ff17ff17ffe80017ffe800e800e800" ), 6 ), from_hex( 8, "17ff17ff17ff17ff17ff17ff17ff17ff17ff17ff17ffe80017ff17ff17ffe800" ) ); + EXPECT_EQ( cofactor1( from_hex( 8, "17ff17ff17ff17ff17ff17ff17ff17ff17ff17ff17ffe80017ffe800e800e800" ), 7 ), from_hex( 8, "17ff17ff17ff17ff17ff17ff17ff17ff17ff17ff17ff17ff17ff17ff17ff17ff" ) ); +} + TEST_F( OperationsTest, swap_adjacent_inplace_small ) { for ( const auto& p : std::vector>{{0u, "bce8"}, {1u, "e6e8"}, {2u, "dea8"}} ) From 766d3a8724f1d2e3d14711d98108d6d63b6a198f Mon Sep 17 00:00:00 2001 From: Mathias Soeken Date: Fri, 20 Oct 2017 18:13:30 +0200 Subject: [PATCH 4/9] Documentation. --- docs/operations.rst | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/docs/operations.rst b/docs/operations.rst index 7548a1f1..3eee6286 100644 --- a/docs/operations.rst +++ b/docs/operations.rst @@ -21,8 +21,8 @@ Predicates less_than has_var -Truth table combination and manipulation ----------------------------------------- +Combination and manipulation +---------------------------- .. doc_brief_table:: unary_not From 96d5092c3b488fca7febed4e214ad8080390e556 Mon Sep 17 00:00:00 2001 From: Mathias Soeken Date: Fri, 20 Oct 2017 18:27:31 +0200 Subject: [PATCH 5/9] Operators for binary operations. --- docs/changelog.rst | 3 ++- docs/conf.py | 3 ++- docs/operators.rst | 3 +++ include/kitty/operators.hpp | 21 +++++++++++++++++++++ 4 files changed, 28 insertions(+), 2 deletions(-) diff --git a/docs/changelog.rst b/docs/changelog.rst index aa27e030..52a0e935 100644 --- a/docs/changelog.rst +++ b/docs/changelog.rst @@ -32,8 +32,9 @@ v0.1 * Predicates: ``has_var`` `#11 `_ -* Operators: ``~``, ``==``, ``<`` +* Operators: ``~``, ``&``, ``|``, ``^``, ``==``, ``<`` `#8 `_ + `#11 `_ * Swap adjacent variables: ``swap_adjacent_inplace``, ``swap_adjacent`` `#6 `_ diff --git a/docs/conf.py b/docs/conf.py index 69516de0..94f84b21 100644 --- a/docs/conf.py +++ b/docs/conf.py @@ -215,8 +215,9 @@ def run(self): tbody = nodes.tbody() for c in self.content: name = c.strip() + query = name.replace("&", " &") - for elem in tree.findall("./compounddef/sectiondef/memberdef/[name='%s']" % name): + for elem in tree.findall("./compounddef/sectiondef/memberdef/[name='%s']" % query): args = ', '.join(e.text for e in elem.findall("./param/declname")) func = nodes.entry('', nodes.literal(text = '%s(%s)' % (name, args))) diff --git a/docs/operators.rst b/docs/operators.rst index 4909265d..0ff5abe9 100644 --- a/docs/operators.rst +++ b/docs/operators.rst @@ -5,6 +5,9 @@ The header ```` implements operator shortcuts to operations .. doc_brief_table:: operator~ + operator& + operator| + operator^ operator== operator< diff --git a/include/kitty/operators.hpp b/include/kitty/operators.hpp index 718362fd..e40dc209 100644 --- a/include/kitty/operators.hpp +++ b/include/kitty/operators.hpp @@ -37,6 +37,27 @@ inline TT operator~( const TT& tt ) return unary_not( tt ); } +/*! \brief Operator for binary_and */ +template +inline TT operator&( const TT& first, const TT& second ) +{ + return binary_and( first, second ); +} + +/*! \brief Operator for binary_or */ +template +inline TT operator|( const TT& first, const TT& second ) +{ + return binary_or( first, second ); +} + +/*! \brief Operator for binary_xor */ +template +inline TT operator^( const TT& first, const TT& second ) +{ + return binary_xor( first, second ); +} + /*! \brief Operator for equal */ template inline bool operator==( const TT& first, const TT& second ) From e1e0c44dd7bae183e4ae8ef104cb8bb1cdaa3621 Mon Sep 17 00:00:00 2001 From: Mathias Soeken Date: Fri, 20 Oct 2017 18:40:46 +0200 Subject: [PATCH 6/9] Predicate `is_const0`. --- docs/changelog.rst | 2 +- docs/operations.rst | 1 + include/kitty/operations.hpp | 18 ++++++++++++++++++ test/operations.cpp | 10 ++++++++++ 4 files changed, 30 insertions(+), 1 deletion(-) diff --git a/docs/changelog.rst b/docs/changelog.rst index 52a0e935..0d46c794 100644 --- a/docs/changelog.rst +++ b/docs/changelog.rst @@ -29,7 +29,7 @@ v0.1 `#4 `_ `#8 `_ -* Predicates: ``has_var`` +* Predicates: ``has_var``, ``is_const0`` `#11 `_ * Operators: ``~``, ``&``, ``|``, ``^``, ``==``, ``<`` diff --git a/docs/operations.rst b/docs/operations.rst index 3eee6286..84cd6faa 100644 --- a/docs/operations.rst +++ b/docs/operations.rst @@ -20,6 +20,7 @@ Predicates equal less_than has_var + is_const0 Combination and manipulation ---------------------------- diff --git a/include/kitty/operations.hpp b/include/kitty/operations.hpp index 5b916797..aa91da2a 100644 --- a/include/kitty/operations.hpp +++ b/include/kitty/operations.hpp @@ -281,6 +281,24 @@ inline bool less_than( const static_truth_table& first, const sta } /*! \endcond PRIVATE */ +/*! \brief Checks whether truth table is contant 0 + + \param tt Truth table +*/ +template +inline bool is_const0( const TT& tt ) +{ + return std::all_of( std::begin( tt._bits ), std::end( tt._bits ), []( uint64_t word ) { return word == 0; } ); +} + +/*! \cond PRIVATE */ +template +inline bool is_const0( const static_truth_table& tt ) +{ + return tt._bits == 0; +} +/*! \endcond */ + /*! \brief Checks whether truth table depends on given variable index \param tt Truth table diff --git a/test/operations.cpp b/test/operations.cpp index dde596cf..d3c45ea1 100644 --- a/test/operations.cpp +++ b/test/operations.cpp @@ -198,6 +198,16 @@ TEST_F( OperationsTest, comparisons ) TEST_F( OperationsTest, support ) { + EXPECT_TRUE( is_const0( from_hex<0>( "0" ) ) ); + EXPECT_TRUE( is_const0( from_hex<1>( "0" ) ) ); + EXPECT_TRUE( is_const0( from_hex<2>( "0" ) ) ); + EXPECT_TRUE( is_const0( from_hex<3>( "00" ) ) ); + EXPECT_TRUE( is_const0( from_hex<4>( "0000" ) ) ); + EXPECT_TRUE( is_const0( from_hex<5>( "00000000" ) ) ); + EXPECT_TRUE( is_const0( from_hex<6>( "0000000000000000" ) ) ); + EXPECT_TRUE( is_const0( from_hex<7>( "00000000000000000000000000000000" ) ) ); + EXPECT_TRUE( is_const0( from_hex<8>( "0000000000000000000000000000000000000000000000000000000000000000" ) ) ); + EXPECT_TRUE( has_var( from_hex<3>( "77" ), 0 ) ); EXPECT_TRUE( has_var( from_hex<3>( "77" ), 1 ) ); EXPECT_TRUE( !has_var( from_hex<3>( "77" ), 2 ) ); From 59d71fa746367e8149769e97c84adcbf366c20d6 Mon Sep 17 00:00:00 2001 From: Mathias Soeken Date: Sat, 21 Oct 2017 11:17:26 +0200 Subject: [PATCH 7/9] Update operators. --- docs/changelog.rst | 2 +- docs/operators.rst | 3 +++ include/kitty/operators.hpp | 21 +++++++++++++++++++++ 3 files changed, 25 insertions(+), 1 deletion(-) diff --git a/docs/changelog.rst b/docs/changelog.rst index 0d46c794..0cbbe374 100644 --- a/docs/changelog.rst +++ b/docs/changelog.rst @@ -32,7 +32,7 @@ v0.1 * Predicates: ``has_var``, ``is_const0`` `#11 `_ -* Operators: ``~``, ``&``, ``|``, ``^``, ``==``, ``<`` +* Operators: ``~``, ``&``, ``&=``, ``|``, ``|=``, ``^``, ``^=``, ``==``, ``<`` `#8 `_ `#11 `_ diff --git a/docs/operators.rst b/docs/operators.rst index 0ff5abe9..547abfc3 100644 --- a/docs/operators.rst +++ b/docs/operators.rst @@ -6,8 +6,11 @@ The header ```` implements operator shortcuts to operations .. doc_brief_table:: operator~ operator& + operator&= operator| + operator|= operator^ + operator^= operator== operator< diff --git a/include/kitty/operators.hpp b/include/kitty/operators.hpp index e40dc209..099512e1 100644 --- a/include/kitty/operators.hpp +++ b/include/kitty/operators.hpp @@ -44,6 +44,13 @@ inline TT operator&( const TT& first, const TT& second ) return binary_and( first, second ); } +/*! \brief Operator for binary_and and assign */ +template +inline void operator&=( TT& first, const TT& second ) +{ + first = binary_and( first, second ); +} + /*! \brief Operator for binary_or */ template inline TT operator|( const TT& first, const TT& second ) @@ -51,6 +58,13 @@ inline TT operator|( const TT& first, const TT& second ) return binary_or( first, second ); } +/*! \brief Operator for binary_or and assign */ +template +inline void operator|=( TT& first, const TT& second ) +{ + first = binary_or( first, second ); +} + /*! \brief Operator for binary_xor */ template inline TT operator^( const TT& first, const TT& second ) @@ -58,6 +72,13 @@ inline TT operator^( const TT& first, const TT& second ) return binary_xor( first, second ); } +/*! \brief Operator for binary_xor and assign */ +template +inline void operator^=( TT& first, const TT& second ) +{ + first = binary_xor( first, second ); +} + /*! \brief Operator for equal */ template inline bool operator==( const TT& first, const TT& second ) From 2dcbb554d5e98bd5a266b6d9ce0457fd044395c7 Mon Sep 17 00:00:00 2001 From: Mathias Soeken Date: Sat, 21 Oct 2017 11:40:02 +0200 Subject: [PATCH 8/9] Create truth table from cube (SOP) representation. --- docs/changelog.rst | 3 +- docs/constructors.rst | 1 + include/kitty/constructors.hpp | 51 ++++++++++++++++++++++++++++++++++ 3 files changed, 54 insertions(+), 1 deletion(-) diff --git a/docs/changelog.rst b/docs/changelog.rst index 0cbbe374..1cea70b5 100644 --- a/docs/changelog.rst +++ b/docs/changelog.rst @@ -12,11 +12,12 @@ v0.1 `#1 `_ `#8 `_ -* Constructors: ``create_nth_var``, ``create_from_binary_string``, ``create_from_hex_string``, ``create_random``, and ``create_majority`` +* Constructors: ``create_nth_var``, ``create_from_binary_string``, ``create_from_hex_string``, ``create_random``, ``create_from_cubes``, and ``create_majority`` `#1 `_ `#4 `_ `#5 `_ `#9 `_ + `#11 `_ * Unary and binary operations: ``unary_not``, ``unary_not_if``, ``binary_and``, ``binary_or``, and ``binary_xor`` `#2 `_ diff --git a/docs/constructors.rst b/docs/constructors.rst index 6067c415..ce3cd446 100644 --- a/docs/constructors.rst +++ b/docs/constructors.rst @@ -8,6 +8,7 @@ The header ```` implements operations to construct truth create_from_binary_string create_from_hex_string create_random + create_from_cubes create_majority diff --git a/include/kitty/constructors.hpp b/include/kitty/constructors.hpp index 30a940e4..becbee2e 100644 --- a/include/kitty/constructors.hpp +++ b/include/kitty/constructors.hpp @@ -31,6 +31,7 @@ #include "detail/constants.hpp" #include "operations.hpp" +#include "operators.hpp" #include "static_truth_table.hpp" namespace kitty @@ -200,6 +201,56 @@ void create_random( TT& tt ) create_random( tt, std::chrono::system_clock::now().time_since_epoch().count() ); } +/*! \brief Creates truth table from cubes representation + + A sum-of-product is represented as a vector of products (called + cubes). A product is represented as bit-mask, where odd indexes + correspond to negative literals, and positive indexes corrspond to + positive literals. As an example the cube `38` which is `100110` in + binary represents the product \f$ x_2\bar x_1x_0 \f$. + + 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. + + Since product terms are represented as 64-bit bit-masks, a cube + representation only allows truth table sizes up to 32 variables. + + \param tt Truth table + \param cubes Vector of cubes +*/ +template +void create_from_cubes( TT& tt, const std::vector& cubes ) +{ + /* we collect product terms for an SOP, start with const0 */ + clear( tt ); + + for ( auto cube : cubes ) + { + auto product = ~tt.construct(); /* const1 of same size */ + + for ( auto i = 0; i < tt.num_vars(); ++i ) + { + if ( cube & 1 ) /* negative literal */ + { + auto var = tt.construct(); + create_nth_var( var, i, true ); + product &= var; + } + cube >>= 1; + if ( cube & 1 ) /* positive literal */ + { + auto var = tt.construct(); + create_nth_var( var, i ); + product &= var; + } + cube >>= 1; + } + + tt |= product; + } +} + /*! \brief Constructs majority-n function The number of variables is determined from the truth table. From 37d38f366ce543aa4fbfc2e44430e3dd509b7804 Mon Sep 17 00:00:00 2001 From: Mathias Soeken Date: Sat, 21 Oct 2017 11:40:24 +0200 Subject: [PATCH 9/9] Create ISOP repersentation with Minato-Morreale algorithm. --- docs/changelog.rst | 3 ++ docs/index.rst | 1 + docs/isop.rst | 9 ++++ docs/reference.rst | 5 ++ include/kitty/isop.hpp | 115 ++++++++++++++++++++++++++++++++++++++++ include/kitty/kitty.hpp | 1 + test/isop.cpp | 69 ++++++++++++++++++++++++ 7 files changed, 203 insertions(+) create mode 100644 docs/isop.rst create mode 100644 include/kitty/isop.hpp create mode 100644 test/isop.cpp diff --git a/docs/changelog.rst b/docs/changelog.rst index 1cea70b5..47f942aa 100644 --- a/docs/changelog.rst +++ b/docs/changelog.rst @@ -54,3 +54,6 @@ v0.1 * NPN canonization: ``exact_npn_canonization``, ``create_from_npn_config`` `#8 `_ + +* Compute ISOP representation: ``isop`` + `#11 `_ diff --git a/docs/index.rst b/docs/index.rst index 92f425b7..48f4abf2 100644 --- a/docs/index.rst +++ b/docs/index.rst @@ -16,6 +16,7 @@ Welcome to kitty's documentation! operations operators canonization + isop examples reference changelog diff --git a/docs/isop.rst b/docs/isop.rst new file mode 100644 index 00000000..400bf4d8 --- /dev/null +++ b/docs/isop.rst @@ -0,0 +1,9 @@ +ISOP representations +==================== + +The header ```` implements methods to compute irredundant sum-of-products (ISOP) representations. + +.. doc_brief_table:: + isop + + diff --git a/docs/reference.rst b/docs/reference.rst index cdbe119c..169347b8 100644 --- a/docs/reference.rst +++ b/docs/reference.rst @@ -46,3 +46,8 @@ Canonization .. doxygenfile:: canonization.hpp +ISOP representations +-------------------- + +.. doxygenfile:: isop.hpp + diff --git a/include/kitty/isop.hpp b/include/kitty/isop.hpp new file mode 100644 index 00000000..56c77688 --- /dev/null +++ b/include/kitty/isop.hpp @@ -0,0 +1,115 @@ +/* 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 "operations.hpp" +#include "operators.hpp" + +namespace kitty +{ + +/*! \cond PRIVATE */ +template +TT isop_rec( const TT& tt, const TT& dc, uint8_t var_index, std::vector& cubes ) +{ + assert( var_index <= tt.num_vars() ); + assert( is_const0( tt & ~dc ) ); + + if ( is_const0( tt ) ) + return tt; + + if ( is_const0( ~dc ) ) + { + cubes.push_back( 0 ); + return dc; + } + + assert( var_index > 0 ); + + int var = var_index - 1; + for ( ; var >= 0; --var ) + { + if ( has_var( tt, var ) || has_var( dc, var ) ) + break; + } + + assert( var >= 0 ); + + /* co-factor */ + const auto tt0 = cofactor0( tt, var ); + const auto tt1 = cofactor1( tt, var ); + const auto dc0 = cofactor0( dc, var ); + const auto dc1 = cofactor1( dc, var ); + + const auto beg0 = cubes.size(); + const auto res0 = isop_rec( tt0 & ~dc1, dc0, var, cubes ); + const auto end0 = cubes.size(); + const auto res1 = isop_rec( tt1 & ~dc0, dc1, var, cubes ); + const auto end1 = cubes.size(); + auto res2 = isop_rec( ( tt0 & ~res0 ) | ( tt1 & ~res1 ), dc0 & dc1, var, cubes ); + + auto var0 = tt.construct(); + create_nth_var( var0, var, true ); + auto var1 = tt.construct(); + create_nth_var( var1, var ); + res2 |= ( res0 & var0 ) | ( res1 & var1 ); + + for ( auto c = beg0; c < end0; ++c ) + { + cubes[c] |= 1 << ( 2 * var ); + } + for ( auto c = end0; c < end1; ++c ) + { + cubes[c] |= 1 << ( 2 * var + 1 ); + } + + assert( is_const0( tt & ~res2 ) ); + assert( is_const0( res2 & ~dc ) ); + + return res2; +} +/* \endcond */ + +/*! \brief 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]. + + Check the function `create_from_cubes` for a detailed description of + the cubes representation. + + \param tt Truth table +*/ +template +inline std::vector isop( const TT& tt ) +{ + std::vector cubes; + isop_rec( tt, tt, tt.num_vars(), cubes ); + return cubes; +} + +} diff --git a/include/kitty/kitty.hpp b/include/kitty/kitty.hpp index 1dd6ca74..3426450e 100644 --- a/include/kitty/kitty.hpp +++ b/include/kitty/kitty.hpp @@ -31,6 +31,7 @@ #include "bit_operations.hpp" #include "canonization.hpp" #include "constructors.hpp" +#include "isop.hpp" #include "operations.hpp" #include "operators.hpp" diff --git a/test/isop.cpp b/test/isop.cpp new file mode 100644 index 00000000..ec22e0de --- /dev/null +++ b/test/isop.cpp @@ -0,0 +1,69 @@ +/* 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 +#include + +#include + +#include + +#include "utility.hpp" + +using namespace kitty; + +class IsopTest : public kitty::testing::Test +{ +}; + +TEST_F( IsopTest, isop_for_small ) +{ + const auto tt = from_hex<3>( "e8" ); + + const auto cubes = isop( tt ); + + EXPECT_EQ( cubes.size(), 3 ); + EXPECT_TRUE( std::find( std::begin( cubes ), std::end( cubes ), 10 ) != std::end( cubes ) ); + EXPECT_TRUE( std::find( std::begin( cubes ), std::end( cubes ), 34 ) != std::end( cubes ) ); + EXPECT_TRUE( std::find( std::begin( cubes ), std::end( cubes ), 40 ) != std::end( cubes ) ); + + auto tt_copy = tt.construct(); + create_from_cubes( tt_copy, cubes ); + EXPECT_EQ( tt, tt_copy ); +} + +TEST_F( IsopTest, random_isop ) +{ + static_truth_table<10> tt; + + for ( auto i = 0; i < 1000; ++i ) + { + create_random( tt ); + const auto cubes = isop( tt ); + auto tt_copy = tt.construct(); + create_from_cubes( tt_copy, cubes ); + EXPECT_EQ( tt, tt_copy ); + } +}