From ee3f93f0ab20b588c7b3b757621b003a977c1b79 Mon Sep 17 00:00:00 2001 From: Mathias Soeken Date: Mon, 19 Mar 2018 15:52:55 +0100 Subject: [PATCH] Boolean function property checks. --- docs/changelog.rst | 3 + docs/index.rst | 1 + docs/properties.rst | 11 +++ include/kitty/kitty.hpp | 1 + include/kitty/properties.hpp | 161 +++++++++++++++++++++++++++++++++++ test/properties.cpp | 96 +++++++++++++++++++++ 6 files changed, 273 insertions(+) create mode 100644 docs/properties.rst create mode 100644 include/kitty/properties.hpp create mode 100644 test/properties.cpp diff --git a/docs/changelog.rst b/docs/changelog.rst index a00718e5..d3558a3e 100644 --- a/docs/changelog.rst +++ b/docs/changelog.rst @@ -25,6 +25,9 @@ v0.4 (not yet released) * Generate implicants and prime implicants: ``get_minterms``, ``get_jbuddies``, ``get_prime_implicants_morreale`` `#46 `_ +* Function properties: ``chow_parameters``, ``is_canalizing``, ``is_horn``, ``is_krom`` + `#48 `_ + v0.3 (February 25, 2018) ------------------------ diff --git a/docs/index.rst b/docs/index.rst index 1427a9f6..960b439c 100644 --- a/docs/index.rst +++ b/docs/index.rst @@ -25,6 +25,7 @@ Welcome to kitty's documentation! constructors operations operators + properties print hash implicant diff --git a/docs/properties.rst b/docs/properties.rst new file mode 100644 index 00000000..bc8108ad --- /dev/null +++ b/docs/properties.rst @@ -0,0 +1,11 @@ +Properties +========== + +The header ```` implements functions compute function +properties. + +.. doc_brief_table:: + chow_parameters + is_canalizing + is_horn + is_krom diff --git a/include/kitty/kitty.hpp b/include/kitty/kitty.hpp index 5ed28fbc..82fece86 100644 --- a/include/kitty/kitty.hpp +++ b/include/kitty/kitty.hpp @@ -50,6 +50,7 @@ #include "operators.hpp" #include "permutation.hpp" #include "print.hpp" +#include "properties.hpp" #include "spectral.hpp" /* diff --git a/include/kitty/properties.hpp b/include/kitty/properties.hpp new file mode 100644 index 00000000..76ed07d3 --- /dev/null +++ b/include/kitty/properties.hpp @@ -0,0 +1,161 @@ +/* kitty: C++ truth table library + * Copyright (C) 2017-2018 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. + */ + +/*! + \file properties.hpp + \brief Implements property checks for Boolean function + + \author Mathias Soeken +*/ + +#pragma once + +#include +#include +#include + +#include "bit_operations.hpp" + +namespace kitty +{ + +/*! \brief Returns the Chow parameter of a function + + The Chow parameters is a set of values \f$N(f), \Sigma(f)\f$, where \f$N(f)\f$ + is the size of the ON-set, and \f$\Sigma(f)\f$ is the sum of all input + assignments in the ON-set. For example for \f$f = x_1 \lor x_2\f$ the + function returns \f$(3, (2,2))\f$. + + \param tt Truth table +*/ +template +std::pair> chow_parameters( const TT& tt ) +{ + assert( tt.num_vars() <= 32 ); + + const auto n = tt.num_vars(); + const auto nf = count_ones( tt ); + + std::vector sf( n, 0u ); + for_each_one_bit( tt, [n, &sf]( auto minterm ) { + for ( auto i = 0u; minterm; ++i ) + { + if ( minterm & 1 ) + { + ++sf[i]; + } + minterm >>= 1; + } + } ); + + return {nf, sf}; +} + +/*! \brief Checks whether a function is canalizing + + \param tt Truth table +*/ +template +bool is_canalizing( const TT& tt ) +{ + uint32_t f1or{}, f0or{}; + uint32_t f1and, f0and; + + uint32_t max = static_cast( ( uint64_t( 1 ) << tt.num_vars() ) - 1 ); + f1and = f0and = max; + + for ( uint32_t i = 0u; i < tt.num_bits(); ++i ) + { + if ( get_bit( tt, i ) == 0 ) + { + f0and &= i; + f0or |= i; + } + else + { + f1and &= i; + f1or |= i; + } + + if ( f0and == 0 && f1and == 0 && f0or == max && f1or == max ) + { + return false; + } + } + + return true; +} + +/*! \brief Checks whether a function is Horn + + A function is Horn, if it can be represented using Horn clauses. + + \param tt Truth table +*/ +template +bool is_horn( const TT& tt ) +{ + for ( uint32_t i = 1u; i < tt.num_bits(); ++i ) + { + for ( uint32_t j = 0u; j < i; ++j ) + { + if ( get_bit( tt, j ) && get_bit( tt, i ) && !get_bit( tt, i & j ) ) + { + return false; + } + } + } + + return true; +} + +/*! \brief Checks whether a function is Krom + + A function is Krom, if it can be represented using Krom clauses. + + \param tt Truth table +*/ +template +bool is_krom( const TT& tt ) +{ + for ( uint32_t i = 2u; i < tt.num_bits(); ++i ) + { + for ( uint32_t j = 1u; j < i; ++j ) + { + for ( uint32_t k = 0u; k < j; ++k ) + { + const auto maj = ( i & j ) | ( i & k ) | ( j & k ); + if ( get_bit( tt, k ) && get_bit( tt, j ) && get_bit( tt, i ) && !get_bit( tt, maj ) ) + { + return false; + } + } + } + } + + return true; +} + +} // namespace kitty diff --git a/test/properties.cpp b/test/properties.cpp new file mode 100644 index 00000000..64e1a7f7 --- /dev/null +++ b/test/properties.cpp @@ -0,0 +1,96 @@ +/* kitty: C++ truth table library + * Copyright (C) 2017-2018 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 "utility.hpp" + +using namespace kitty; + +class PropertiesTest : public kitty::testing::Test +{ +}; + +TEST_F( PropertiesTest, chow_small_example ) +{ + auto r = chow_parameters( from_hex<2>( "e" ) ); + EXPECT_EQ( r.first, 3u ); + EXPECT_EQ( r.second.size(), 2u ); + EXPECT_EQ( r.second[0u], 2u ); + EXPECT_EQ( r.second[1u], 2u ); +} + +TEST_F( PropertiesTest, is_canalizing ) +{ + static_truth_table<4> tt; + uint32_t counter{}; + + do { + if ( is_canalizing( tt ) ) + { + ++counter; + } + + next_inplace( tt ); + } while ( !is_const0( tt ) ); + + EXPECT_EQ( counter, 3514u ); +} + +TEST_F( PropertiesTest, is_horn ) +{ + static_truth_table<4> tt; + uint32_t counter{}; + + do { + if ( is_horn( tt ) ) + { + ++counter; + } + + next_inplace( tt ); + } while ( !is_const0( tt ) ); + + EXPECT_EQ( counter, 4960u ); +} + +TEST_F( PropertiesTest, is_krom ) +{ + static_truth_table<4> tt; + uint32_t counter{}; + + do { + if ( is_krom( tt ) ) + { + ++counter; + } + + next_inplace( tt ); + } while ( !is_const0( tt ) ); + + EXPECT_EQ( counter, 4170u ); +} \ No newline at end of file