Merge pull request #11 from msoeken/isop

Create ISOP representations

Author: msoeken

docs/changelog.rst

@@ -12,11 +12,12 @@ v0.1
   `#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``, ``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 <https://github.com/msoeken/kitty/pull/1>`_
   `#4 <https://github.com/msoeken/kitty/pull/4>`_
   `#5 <https://github.com/msoeken/kitty/pull/5>`_
   `#9 <https://github.com/msoeken/kitty/pull/9>`_
+  `#11 <https://github.com/msoeken/kitty/pull/11>`_
 
 * Unary and binary operations: ``unary_not``, ``unary_not_if``, ``binary_and``, ``binary_or``, and ``binary_xor``
   `#2 <https://github.com/msoeken/kitty/pull/2>`_
@@ -29,8 +30,12 @@ v0.1
   `#4 <https://github.com/msoeken/kitty/pull/4>`_
   `#8 <https://github.com/msoeken/kitty/pull/8>`_
 
-* Operators: ``~``, ``==``, ``<``
+* Predicates: ``has_var``, ``is_const0``
+  `#11 <https://github.com/msoeken/kitty/pull/11>`_
+
+* Operators: ``~``, ``&``, ``&=``, ``|``, ``|=``, ``^``, ``^=``, ``==``, ``<``
   `#8 <https://github.com/msoeken/kitty/pull/8>`_
+  `#11 <https://github.com/msoeken/kitty/pull/11>`_
 
 * Swap adjacent variables: ``swap_adjacent_inplace``, ``swap_adjacent``
   `#6 <https://github.com/msoeken/kitty/pull/6>`_
@@ -44,5 +49,11 @@ v0.1
 * Enumerate truth tables: ``next_inplace``, ``next``
   `#10 <https://github.com/msoeken/kitty/pull/10>`_
 
+* Compute co-factors: ``cofactor0_inplace``, ``cofactor0``, ``cofactor1_inplace``, ``cofactor1``
+  `#11 <https://github.com/msoeken/kitty/pull/11>`_
+
 * NPN canonization: ``exact_npn_canonization``, ``create_from_npn_config``
   `#8 <https://github.com/msoeken/kitty/pull/8>`_
+
+* Compute ISOP representation: ``isop``
+  `#11 <https://github.com/msoeken/kitty/pull/11>`_

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)))

docs/constructors.rst

@@ -8,6 +8,7 @@ The header ``<kitty/constructors.hpp>`` implements operations to construct truth
    create_from_binary_string
    create_from_hex_string
    create_random
+   create_from_cubes
    create_majority
 
 

docs/index.rst

@@ -16,6 +16,7 @@ Welcome to kitty's documentation!
    operations
    operators
    canonization
+   isop
    examples
    reference
    changelog

docs/isop.rst

@@ -0,0 +1,9 @@
+ISOP representations
+====================
+
+The header ``<kitty/isop.hpp>`` implements methods to compute irredundant sum-of-products (ISOP) representations.
+
+.. doc_brief_table::
+   isop
+
+

docs/operations.rst

@@ -19,9 +19,11 @@ Predicates
 .. doc_brief_table::
    equal
    less_than
+   has_var
+   is_const0
 
-Truth table combination and manipulation
-----------------------------------------
+Combination and manipulation
+----------------------------
 
 .. doc_brief_table::
    unary_not
@@ -32,6 +34,10 @@ Truth table combination and manipulation
    ternary_majority
    next_inplace
    next
+   cofactor0_inplace
+   cofactor0
+   cofactor1_inplace
+   cofactor1
    swap_inplace
    swap
    swap_adjacent_inplace

docs/operators.rst

@@ -5,6 +5,12 @@ The header ``<kitty/operators.hpp>`` implements operator shortcuts to operations
 
 .. doc_brief_table::
    operator~
+   operator&
+   operator&=
+   operator|
+   operator|=
+   operator^
+   operator^=
    operator==
    operator<
 

docs/reference.rst

@@ -46,3 +46,8 @@ Canonization
 
 .. doxygenfile:: canonization.hpp
 
+ISOP representations
+--------------------
+
+.. doxygenfile:: isop.hpp
+

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<typename TT>
+void create_from_cubes( TT& tt, const std::vector<uint64_t>& 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.

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] = {

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<typename TT>
+TT isop_rec( const TT& tt, const TT& dc, uint8_t var_index, std::vector<uint64_t>& 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<typename TT>
+inline std::vector<uint64_t> isop( const TT& tt )
+{
+  std::vector<uint64_t> cubes;
+  isop_rec( tt, tt, tt.num_vars(), cubes );
+  return cubes;
+}
+
+}

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"