DTIS Project

include/kitty/threshold_identification.hpp

@@ -33,12 +33,53 @@
 #pragma once
 
 #include <vector>
-// #include <lpsolve/lp_lib.h> /* uncomment this line to include lp_solve */
+#include <lpsolve/lp_lib.h> /* uncomment this line to include lp_solve */
 #include "traits.hpp"
+#include "operations.hpp"
+#include "isop.hpp"
 
 namespace kitty
 {
 
+/**
+     * Check if the truth table is unate in a specific variable and, in this case, force its positivity and return true. Otherwise, return false.
+     * @tparam TT
+     * @param tt
+     * @param var_index
+     * @return
+     */
+template<typename TT, typename = std::enable_if_t<is_complete_truth_table<TT>::value>>
+bool force_positive_unate_in_variable( TT& tt, uint32_t var_index, std::vector<bool>& inverted )
+{
+  assert( var_index <= UINT8_MAX );
+  const TT& cof0 = cofactor0( tt, (uint8_t)var_index );
+  const TT& cof1 = cofactor1( tt, (uint8_t)var_index );
+
+  if ( binary_predicate( cof1, cof0, std::greater_equal<>() ) )
+  {
+    inverted[var_index] = false;
+    return true;
+  }
+  else if ( binary_predicate( cof1, cof0, std::less_equal<>() ) )
+  {
+    flip_inplace( tt, (uint8_t)var_index );
+    inverted[var_index] = true;
+    return true;
+  }
+  return false;
+}
+
+template<typename TT, typename = std::enable_if_t<is_complete_truth_table<TT>::value>>
+bool force_positive_unate( TT& tt, std::vector<bool>& inverted )
+{
+  for ( uint32_t i = 0; i < tt.num_vars(); ++i )
+  {
+    if ( !force_positive_unate_in_variable( tt, i, inverted ) )
+      return false;
+  }
+  return true;
+}
+
 /*! \brief Threshold logic function identification
 
   Given a truth table, this function determines whether it is a threshold logic function (TF)
@@ -59,13 +100,91 @@ template<typename TT, typename = std::enable_if_t<is_complete_truth_table<TT>::v
 bool is_threshold( const TT& tt, std::vector<int64_t>* plf = nullptr )
 {
   std::vector<int64_t> linear_form;
+  std::vector<bool> inverted( tt.num_vars() );
+
+  TT mutableTT = tt;
 
-  /* TODO */
   /* if tt is non-TF: */
-  return false;
+  if ( !force_positive_unate( mutableTT, inverted ) )
+    return false;
 
   /* if tt is TF: */
   /* push the weight and threshold values into `linear_form` */
+  lprec* lp( make_lp( 0, mutableTT.num_vars() + 1 ) );
+  set_verbose( lp, 0 );
+
+  set_minim( lp );
+
+  // set the objective
+  std::vector<REAL> objective( mutableTT.num_vars() + 2, 0. );
+  for ( uint32_t i = 0; i <= mutableTT.num_vars(); ++i )
+  {
+    objective[i] = 1.;
+  }
+  set_obj_fn( lp, objective.data() );
+
+  // on-set constraints
+  for ( cube& on_elem : isop( mutableTT ) )
+  {
+    std::vector<REAL> constraint( mutableTT.num_vars() + 2, 0. );
+    for ( uint32_t i = 0; i < mutableTT.num_vars(); ++i )
+    {
+      if ( on_elem.get_mask( i ) && on_elem.get_bit( i ) )
+      {
+        constraint[i + 1] = 1.;
+      }
+    }
+    constraint[mutableTT.num_vars() + 1] = -1.;
+    add_constraint( lp, constraint.data(), GE, 0. );
+  }
+
+  // off-set constraints
+  for ( cube& off_elem : isop( ~mutableTT ) )
+  {
+    std::vector<REAL> constraint( mutableTT.num_vars() + 2, 0. );
+    for ( uint32_t i = 0; i < mutableTT.num_vars(); ++i )
+    {
+      if ( !off_elem.get_mask( i ) || ( off_elem.get_mask( i ) && off_elem.get_bit( i ) ) )
+      {
+        constraint[i + 1] = 1.;
+      }
+    }
+    constraint[mutableTT.num_vars() + 1] = -1.;
+    add_constraint( lp, constraint.data(), LE, -1. );
+  }
+
+  // positivity constraints
+  for ( uint32_t i = 0; i <= mutableTT.num_vars(); ++i )
+  {
+    std::vector<REAL> constraint( mutableTT.num_vars() + 2, 0. );
+    constraint[i + 1] = 1.;
+    add_constraint( lp, constraint.data(), GE, 0. );
+  }
+
+  // ILP constraints
+  for ( uint32_t i = 0; i <= mutableTT.num_vars(); ++i )
+  {
+    set_int( lp, i, true );
+  }
+
+  int status = solve( lp );
+  std::vector<REAL> lp_result( get_Ncolumns( lp ) );
+  get_variables( lp, lp_result.data() );
+  delete_lp( lp );
+  linear_form.insert( linear_form.begin(), lp_result.begin(), lp_result.end() );
+
+  if ( status )
+    return false;
+
+  for ( uint32_t i = 0; i < mutableTT.num_vars(); ++i )
+  {
+    if ( inverted[i] )
+    {
+      linear_form[i] *= -1.;
+      linear_form[mutableTT.num_vars()] += linear_form[i];
+    }
+  }
+
   if ( plf )
   {
     *plf = linear_form;