DTIS project

include/kitty/threshold_identification.hpp

@@ -33,8 +33,20 @@
 #pragma once
 
 #include <vector>
-// #include <lpsolve/lp_lib.h> /* uncomment this line to include lp_solve */
+#include <algorithm>
+#include <bitset>
+#include <string>
+#include <lpsolve/lp_lib.h>
 #include "traits.hpp"
+#include "algorithm.hpp"
+#include "properties.hpp"
+#include "print.hpp"
+#include "cube.hpp"
+#include "bit_operations.hpp"
+#include "isop.hpp"
+#include "dynamic_truth_table.hpp"
+#include "static_truth_table.hpp"
+
 
 namespace kitty
 {
@@ -55,22 +67,208 @@ namespace kitty
              in the end.
   \return `true` if `tt` is a TF; `false` if `tt` is a non-TF.
 */
+
+
 template<typename TT, typename = std::enable_if_t<is_complete_truth_table<TT>::value>>
 bool is_threshold( const TT& tt, std::vector<int64_t>* plf = nullptr )
-{
-  std::vector<int64_t> linear_form;
-
-  /* TODO */
-  /* if tt is non-TF: */
-  return false;
-
-  /* if tt is TF: */
-  /* push the weight and threshold values into `linear_form` */
-  if ( plf )
-  {
-    *plf = linear_form;
-  }
-  return true;
+{	
+    TT ttable = tt;
+    std::vector<bool> inv_var(ttable.num_vars(),false);
+    std::vector<int64_t> linear_form;
+    auto num_vars = ttable.num_vars();
+    bool n, p;
+
+	for (int i = 0; i< num_vars; i++){
+
+	  n=p=false;   
+
+	  for (auto bit = 0u; bit< (2 << (num_vars -1)); bit++){ //from monotone.properties
+
+		  if (get_bit( cofactor0(ttable, i), bit ) > get_bit( cofactor1(ttable, i), bit )){
+
+			  n = true;
+		  }
+		  if (get_bit( cofactor0(ttable, i), bit ) < get_bit( cofactor1(ttable, i), bit )){
+
+			  p = true;
+		  }  
+		  if (n && p){  // binate check
+
+			return false;
+		  }			  
+
+	  }
+	  if (n == true){
+
+		  inv_var.at(i) = true; //n_unate = true, there is a negative unate at i 
+
+		  flip_inplace(ttable, i); //flip variable i
+
+	  }
+	} 
+
+    const auto on_set =  isop(ttable);
+    auto temp = unary_not(ttable);
+    const auto off_set = isop(temp);
+
+
+    /* lp_source code from lpsolve.sourceforge.net using version 5.5*/
+
+    lprec *lp;
+    int Ncol, *colno = NULL, ret = 0;  
+    REAL *row = NULL;  
+
+    int T_pos = num_vars + 1;
+    Ncol = T_pos; // The number of columns is num_vars + 1 for T constraint (last)
+    lp = make_lp(0, Ncol); 
+    if(lp == NULL) 
+
+        return false;       
+
+    if(ret == 0) {
+
+        colno = (int *) malloc(Ncol * sizeof(*colno));
+        row = (REAL *) malloc(Ncol * sizeof(*row));
+        if((colno == NULL) || (row == NULL))
+
+            return false;
+    }
+
+    if(ret == 0) {
+        set_add_rowmode(lp, TRUE);  
+
+		for(int j = 0; j < Ncol; j++){
+
+			auto k = 0;
+            		colno[k] = j+1;
+            		row[j] = ++k;
+
+            add_constraintex(lp, k, row, colno, GE, 0);
+
+        }
+
+        // using the on set cubes. First see if they exist, then add 1, otherwise 0
+        for(int i = 0; i < on_set.size() ; i++){
+
+            auto term = on_set.at(i);
+
+            for(int j = 0; j < num_vars; j++){
+
+                if(term.get_mask(j)){  
+
+                    colno[j] = j+1;
+                    row[j] = 1;
+
+                }else{
+
+		    colno[j] = j+1;                                        
+                    row[j] = 0;
+
+                }
+            }
+            // ex : x1 + x2 >= T -> x1 + x2 - T >= 0
+            colno[num_vars] = T_pos; //T constraint is on num+1
+            row[num_vars] = -1;
+            add_constraintex(lp, T_pos, row, colno, GE, 0);
+        }
+    }
+    if(ret == 0) {
+
+        for(int i = 0; i < off_set.size() ; i++){
+
+            auto term = off_set.at(i);
+
+            for(int j = 0; j < num_vars; j++){	
+
+                if(term.get_mask(j)){  
+
+		    colno[j] = j+1;                         
+                    row[j] = 0;
+
+                }else{
+
+		    colno[j] = j+1;                                             
+                    row[j] = 1;
+
+                }
+
+            }
+            //ex: x1 + x2 <= T - 1 -> x1 + x2 - T <= -1
+            colno[num_vars] = T_pos;
+            row[num_vars] = -1;
+            add_constraintex(lp, T_pos, row, colno, LE, -1);
+        }
+    }
+
+    /*Add the objective function */
+    if(ret == 0) {
+        set_add_rowmode(lp, FALSE); /* rowmode should be turned off again when done building the model */
+
+        for(int i = 0; i < Ncol; i++){
+
+            colno[i] = i + 1;
+            row[i] = 1;
+        }
+
+        if(!set_obj_fnex(lp, Ncol, row, colno))
+
+		return false;
+    }
+
+    if(ret == 0) { //set for minimization (code from lpsolve.sourceforge)
+
+        set_minim(lp);
+        //write_LP( lp, stdout );
+		set_verbose( lp, IMPORTANT);
+
+        ret = solve(lp);
+        if(ret == OPTIMAL)
+            ret = 0;
+		else 
+
+		return false;
+    }
+
+    if(ret == 0) {	// fill the linear form 
+
+        get_variables(lp, row);
+        for(int j = 0; j < Ncol; j++){
+            //printf("%s: %f\n", get_col_name(lp, j + 1), row[j]);
+            linear_form.push_back(row[j]);
+        }
+
+    }
+    // We inverted some variables due to neg. unate. We need to acquire the originals again
+    for(int i = 0; i < num_vars; i++){
+
+        if(inv_var.at(i)==true){
+
+            linear_form.at(i) = -linear_form.at(i);
+            linear_form.at(num_vars) = linear_form.at(num_vars) + linear_form.at(i); //rem. num vars is 1 more
+
+        }
+    }
+
+    // free allocated memory (code from lpsolve.sourceforge)
+    if(row != NULL)
+
+        free(row);
+
+    if(colno != NULL)
+
+        free(colno);
+
+    if(lp != NULL) {
+
+        delete_lp(lp);
+    }
+
+	// finish!
+    if ( plf )
+    {
+        *plf = linear_form;
+    }
+    return true;
 }
 
-} /* namespace kitty */
+}