Extend ternary truth table operations to handle don't cares

docs/operations.rst

@@ -10,6 +10,7 @@ Predicates
    equal
    less_than
    has_var
+   has_var_inplace
    is_const0
    implies
    intersection_is_empty

include/kitty/operations.hpp

@@ -768,18 +768,6 @@ bool has_var( const static_truth_table<NumVars, true>& tt, uint8_t var_index )
 }
 /*! \endcond */
 
-/*! \brief Checks whether a ternary truth table depends on given variable index
-           Don't cares are treated like zeros.
-
-  \param tt Truth table
-  \param var_index Variable index
-*/
-template<typename TT>
-bool has_var( const ternary_truth_table<TT>& tt, uint8_t var_index )
-{
-  return has_var( tt._bits, var_index );
-}
-
 /*! \brief Checks whether a quaternary truth table depends on given variable index.
            This function returns false if the truth table potentially does not depend
            on the variable (due to don't cares) and returns true if the truth table potentially
@@ -844,6 +832,74 @@ bool has_var( const quaternary_truth_table<TT>& tt, uint8_t var_index )
   return false;
 }
 
+/*! \brief Checks whether a ternary truth table depends on given variable index.\
+
+           When the template parameter UseDCs is false, don't cares are treated like zeros.
+           When the template parameter UseDCs is true, this function returns:
+           - true if the onset shows that the function depends on the variable.
+           - false if a don't cares assignments makes the function independent of the variable.
+
+           For example, let the hexadecimal representation of the onset be 0xF0000000, and
+           the hexadecimal representation of the careset be 0xF0000000. This function is
+           independent of the variable 2, with projection function 0xF0F0F0F0 for the following
+           onset, careset pair ( 0xFF000000, 0xFF000000 ).
+
+           Reassigning the careset and the onset is essential when checking if an incompletely
+           specified function depends on multiple variables, since different variables might
+           require different don't cares assignments to achieve indendence on different variables.
+
+  \param tt Truth table
+  \param var_index Variable index
+*/
+template<typename TT, bool UseDCs = false, typename = std::enable_if_t<is_complete_truth_table<TT>::value>>
+bool has_var_inplace( ternary_truth_table<TT>& tt, uint8_t var_index )
+{
+  if constexpr ( UseDCs )
+  {
+    ternary_truth_table<TT> tt0 = tt;
+    ternary_truth_table<TT> tt1 = tt;
+    cofactor0_inplace( tt0, var_index );
+    cofactor1_inplace( tt1, var_index );
+    const TT diff = tt0._bits ^ tt1._bits;
+    const TT mask = tt0._care & tt1._care;
+    if ( kitty::count_ones( diff & mask ) > 0 )
+      return true;
+    /* Adjust the careset and the onset to avoid contradictions. */
+    tt._care |= ( ~mask ) & diff;
+    tt._bits = tt0._bits | tt1._bits;
+    return false;
+  }
+  else
+  {
+    return has_var( tt._bits, var_index );
+  }
+}
+
+/*! \brief Checks whether a ternary truth table depends on given variable index.\
+
+           When the template parameter UseDCs is false, don't cares are treated like zeros.
+           When the template parameter UseDCs is true, this function returns:
+           - true if the onset shows that the function depends on the variable.
+           - false if a don't cares assignments makes the function independent of the variable.
+
+           For example, let the hexadecimal representation of the onset be 0xF0000000, and
+           the hexadecimal representation of the careset be 0xF0000000. This function is
+           independent of the variable 2, with projection function 0xF0F0F0F0 for the following
+           onset, careset pair ( 0xFF000000, 0xFF000000 ).
+
+           Warning. This function DOES NOT perform the reassignment. Use has_var_inplace if that
+           is the desired behavior.
+
+  \param tt Truth table
+  \param var_index Variable index
+*/
+template<typename TT, bool UseDCs = false, typename = std::enable_if_t<is_complete_truth_table<TT>::value>>
+bool has_var( ternary_truth_table<TT> const& tt, uint8_t var_index )
+{
+  ternary_truth_table<TT> ttc = tt;
+  return has_var_inplace<TT, UseDCs>( ttc, var_index );
+}
+
 /*! \brief Computes the next lexicographically larger truth table
 
   This methods updates `tt` to become the next lexicographically
@@ -1548,6 +1604,45 @@ std::vector<uint8_t> min_base_inplace( TT& tt )
   return support;
 }
 
+/*! \brief Reorders truth table to have minimum base
+
+  This function will reorder variables, such that there are no
+  "holes".  For example, the function \f$ x_0 \land x_2 \f$ will be
+  changed to \f$ x_0 \land x_1 \f$ by swapping \f$ x_1 \f$ with \f$
+  x_2 \f$.  That is all variables that are not in the functional
+  support will be moved to the back.  Note that the size of the truth
+  table is not changed, because for `static_truth_table` one cannot
+  compute it at compile-time.
+
+  The function changes the truth table and returns a vector with all
+  variable indexes that were in the functional support of the original
+  function.
+
+  \param tt Truth table
+ */
+template<typename TT, bool UseDCs, typename = std::enable_if_t<is_complete_truth_table<TT>::value>>
+std::vector<uint8_t> min_base_inplace( ternary_truth_table<TT>& tt )
+{
+  std::vector<uint8_t> support;
+
+  auto k = 0u;
+  for ( auto i = 0u; i < tt.num_vars(); ++i )
+  {
+    if ( !has_var<TT, UseDCs>( tt, i ) )
+    {
+      continue;
+    }
+    if ( k < i )
+    {
+      swap_inplace( tt, k, i );
+    }
+    support.push_back( i );
+    ++k;
+  }
+
+  return support;
+}
+
 /*! \brief Expands truth table from minimum base to original based on support
 
   This is the inverse operation to `min_base_inplace`, where the

test/operations.cpp

@@ -1481,3 +1481,34 @@ TEST_F( OperationsTest, shift_mask_for_quaternary )
   EXPECT_EQ( tttabd, quaternary_truth_table<dynamic_truth_table>( from_hex( 4, "a124" ), from_hex( 4, "55a5" ) ) );
   EXPECT_EQ( shift_with_mask( ttt, 0b1110 ), quaternary_truth_table<dynamic_truth_table>( from_hex( 4, "c142" ), from_hex( 4, "33c3" ) ) );
 }
+
+TEST_F( OperationsTest, ternary_operations_exploiting_dont_cares )
+{
+  using TT = kitty::static_truth_table<5u>;
+  TT bits, care, evol[5];
+  kitty::create_from_hex_string( bits, "80000000" );
+  kitty::create_from_hex_string( care, "80000000" );
+  kitty::create_from_hex_string( evol[0], "C0000000" );
+  kitty::create_from_hex_string( evol[1], "F0000000" );
+  kitty::create_from_hex_string( evol[2], "FF000000" );
+  kitty::create_from_hex_string( evol[3], "FFFF0000" );
+  kitty::create_from_hex_string( evol[4], "FFFFFFFF" );
+  auto tt = ternary_truth_table<TT>( bits, care );
+  std::array<bool, 5u> vars;
+  static constexpr bool UseDCs = true;
+  for ( int i = 0; i < 5; i++ )
+  {
+    vars[i] = has_var_inplace<TT, !UseDCs>( tt, i );
+    EXPECT_EQ( vars[i], true );
+    vars[i] = has_var_inplace<TT, UseDCs>( tt, i );
+    EXPECT_EQ( vars[i], false );
+    EXPECT_EQ( tt._bits, evol[i] );
+    EXPECT_EQ( tt._care, evol[i] );
+  }
+  tt = ternary_truth_table<TT>( bits, care );
+  std::vector<uint8_t> supp;
+  supp = kitty::min_base_inplace<TT, !UseDCs>( tt );
+  EXPECT_EQ( supp.size(), 5 );
+  supp = kitty::min_base_inplace<TT, UseDCs>( tt );
+  EXPECT_EQ( supp.size(), 0 );
+}