Boolean function property checks.

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 <https://github.com/msoeken/kitty/pull/46>`_
 
+* Function properties: ``chow_parameters``, ``is_canalizing``, ``is_horn``, ``is_krom``
+  `#48 <https://github.com/msoeken/kitty/pull/48>`_
+
 v0.3 (February 25, 2018)
 ------------------------
 

docs/index.rst

@@ -25,6 +25,7 @@ Welcome to kitty's documentation!
    constructors
    operations
    operators
+   properties
    print
    hash
    implicant

docs/properties.rst

@@ -0,0 +1,11 @@
+Properties
+==========
+
+The header ``<kitty/properties.hpp>`` implements functions compute function
+properties.
+
+.. doc_brief_table::
+   chow_parameters
+   is_canalizing
+   is_horn
+   is_krom

include/kitty/kitty.hpp

@@ -50,6 +50,7 @@
 #include "operators.hpp"
 #include "permutation.hpp"
 #include "print.hpp"
+#include "properties.hpp"
 #include "spectral.hpp"
 
 /*

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 <cinttypes>
+#include <utility>
+#include <vector>
+
+#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<typename TT>
+std::pair<uint32_t, std::vector<uint32_t>> chow_parameters( const TT& tt )
+{
+  assert( tt.num_vars() <= 32 );
+
+  const auto n = tt.num_vars();
+  const auto nf = count_ones( tt );
+
+  std::vector<uint32_t> 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<typename TT>
+bool is_canalizing( const TT& tt )
+{
+  uint32_t f1or{}, f0or{};
+  uint32_t f1and, f0and;
+
+  uint32_t max = static_cast<uint32_t>( ( 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<typename TT>
+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<typename TT>
+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

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 <gtest/gtest.h>
+
+#include <kitty/properties.hpp>
+
+#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 );
+}