Merge pull request #41 from msoeken/cnf

Generate CNF.

Author: msoeken

docs/changelog.rst

@@ -1,6 +1,15 @@
 Change Log
 ==========
 
+v0.4 (not yet released)
+-----------------------
+
+* Constructors: ``create_from_clauses``, ``create_characteristic``
+  `#41 <https://github.com/msoeken/kitty/pull/41>`_
+
+* CNF generation: ``cnf_characteristic``
+  `#41 <https://github.com/msoeken/kitty/pull/41>`_
+
 v0.3 (February 25, 2018)
 ------------------------
 

docs/cnf.rst

@@ -0,0 +1,10 @@
+CNF representations
+===================
+
+The header ``<kitty/cnf.hpp>`` implements methods to compute conjunctive normal
+forms (CNF).
+
+.. doc_brief_table::
+   cnf_characteristic
+
+

docs/constructors.rst

@@ -11,10 +11,12 @@ The header ``<kitty/constructors.hpp>`` implements operations to construct truth
    create_random
    create_from_words
    create_from_cubes
+   create_from_clauses
    create_majority
    create_threshold
    create_equals
    create_symmetric
    create_from_chain
+   create_characteristic
 
 

docs/index.rst

@@ -32,6 +32,7 @@ Welcome to kitty's documentation!
    permutation
    esop
    isop
+   cnf
    reference
 
 Indices and tables

include/kitty/cnf.hpp

@@ -0,0 +1,78 @@
+/* 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 cnf.hpp
+  \brief Implements methods to compute conjunctive normal forms (CNF)
+
+  \author Mathias Soeken
+*/
+
+#pragma once
+
+#include <vector>
+
+#include "cube.hpp"
+#include "isop.hpp"
+#include "operators.hpp"
+
+namespace kitty
+{
+
+/*! \brief Create CNF of the characteristic function
+
+  Creates a CNF representation for the characteritic function of the input
+  function, also known as Tseytin transformation.  To obtain small CNF,
+  an ISOP is computed.
+
+  \param tt Truth table
+*/
+template<typename TT>
+std::vector<cube> cnf_characteristic( const TT& tt )
+{
+  std::vector<cube> cubes;
+  detail::isop_rec( tt, tt, tt.num_vars(), cubes );
+
+  for ( auto& cube : cubes )
+  {
+    cube._bits = ~cube._bits & cube._mask;
+    cube.add_literal( tt.num_vars(), true );
+  }
+
+  const auto end = cubes.size();
+
+  detail::isop_rec( ~tt, ~tt, tt.num_vars(), cubes );
+
+  for ( auto i = end; i < cubes.size(); ++i )
+  {
+    auto& cube = cubes[i];
+    cube._bits = ~cube._bits & cube._mask;
+    cube.add_literal( tt.num_vars(), false );
+  }
+
+  return cubes;
+}
+
+} // namespace kitty

include/kitty/constructors.hpp

@@ -294,6 +294,59 @@ void create_from_cubes( TT& tt, const std::vector<cube>& cubes, bool esop = fals
   }
 }
 
+/*! \brief Creates truth table from clause representation
+
+  A product-of-sum is represented as a vector of sums (called clauses).
+
+  An empty truth table is given as first argument to determine type
+  and number of variables.  Literals in sums that do not fit the
+  number of variables of the truth table are ignored.
+
+  The clause representation only allows truth table sizes up to 32
+  variables.
+
+  \param tt Truth table
+  \param clauses Vector of clauses
+  \param esop Use product of exclusive sums instead of POS
+*/
+template<typename TT>
+void create_from_clauses( TT& tt, const std::vector<cube>& clauses, bool esop = false )
+{
+  /* we collect product terms for an (E)SOP, start with const0 */
+  clear( tt );
+  tt = ~tt;
+
+  for ( auto clause : clauses )
+  {
+    auto sum = tt.construct(); /* const1 of same size */
+
+    auto bits = clause._bits;
+    auto mask = clause._mask;
+
+    for ( auto i = 0; i < tt.num_vars(); ++i )
+    {
+      if ( mask & 1 )
+      {
+        auto var = tt.construct();
+        create_nth_var( var, i, !( bits & 1 ) );
+
+        if ( esop )
+        {
+          sum ^= var;
+        }
+        else
+        {
+          sum |= var;
+        }
+      }
+      bits >>= 1;
+      mask >>= 1;
+    }
+
+    tt &= sum;
+  }
+}
+
 /*! \brief Constructs majority-n function
 
   The number of variables is determined from the truth table.
@@ -660,4 +713,28 @@ bool create_from_chain( TT& tt, std::istream& in, std::string* error = nullptr )
     return true;
   }
 }
+
+/*! \brief Creates characteristic function
+
+  Creates the truth table of the characteristic function, which contains one
+  additional variable.  The new output variable will be the most-significant
+  variable of the new function.
+
+  \param tt Truth table for characteristic function
+  \param from Input truth table
+*/
+template<typename TT, typename TTFrom>
+inline void create_characteristic( TT& tt, const TTFrom& from )
+{
+  assert( tt.num_vars() == from.num_vars() + 1 );
+
+  auto var = tt.construct();
+  create_nth_var( var, from.num_vars() );
+
+  auto ext = tt.construct();
+  extend_to( ext, from );
+
+  tt = ~var ^ ext;
+}
+
 } // namespace kitty

include/kitty/isop.hpp

@@ -40,6 +40,8 @@ namespace kitty
 {
 
 /*! \cond PRIVATE */
+namespace detail
+{
 template<typename TT>
 TT isop_rec( const TT& tt, const TT& dc, uint8_t var_index, std::vector<cube>& cubes )
 {
@@ -99,6 +101,7 @@ TT isop_rec( const TT& tt, const TT& dc, uint8_t var_index, std::vector<cube>& c
 
   return res2;
 }
+}
 /* \endcond */
 
 /*! \brief Computes ISOP representation
@@ -113,7 +116,7 @@ template<typename TT>
 inline std::vector<cube> isop( const TT& tt )
 {
   std::vector<cube> cubes;
-  isop_rec( tt, tt, tt.num_vars(), cubes );
+  detail::isop_rec( tt, tt, tt.num_vars(), cubes );
   return cubes;
 }
 

include/kitty/kitty.hpp

@@ -38,6 +38,7 @@
 #include "affine.hpp"
 #include "algorithm.hpp"
 #include "bit_operations.hpp"
+#include "cnf.hpp"
 #include "constructors.hpp"
 #include "cube.hpp"
 #include "esop.hpp"

test/cnf.cpp

@@ -0,0 +1,75 @@
+/* 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/constructors.hpp>
+#include <kitty/cnf.hpp>
+#include <kitty/dynamic_truth_table.hpp>
+#include <kitty/static_truth_table.hpp>
+
+#include "utility.hpp"
+
+using namespace kitty;
+
+class CNFTest : public kitty::testing::Test
+{
+};
+
+TEST_F( CNFTest, small_cnf_dynamic )
+{
+  auto f = from_hex( 3, "c2" );
+  const auto cubes = cnf_characteristic( f );
+
+  dynamic_truth_table char1( f.num_vars() + 1 ), char2( f.num_vars() + 1 );
+  create_from_clauses( char1, cubes );
+  create_characteristic( char2, f );
+  EXPECT_EQ( char1, char2 );
+}
+
+TEST_F( CNFTest, random_cnf_dynamic )
+{
+  dynamic_truth_table f( 10u ), f_c1( 11u ), f_c2( 11u );
+  for ( auto i = 0; i < 50; ++i )
+  {
+    create_random( f );
+    create_from_clauses( f_c1, cnf_characteristic( f ) );
+    create_characteristic( f_c2, f );
+    EXPECT_EQ( f_c1, f_c2 );
+  }
+}
+
+TEST_F( CNFTest, random_cnf_static )
+{
+  static_truth_table<10> f;
+  static_truth_table<11> f_c1, f_c2;
+  for ( auto i = 0; i < 50; ++i )
+  {
+    create_random( f );
+    create_from_clauses( f_c1, cnf_characteristic( f ) );
+    create_characteristic( f_c2, f );
+    EXPECT_EQ( f_c1, f_c2 );
+  }
+}