From 4415cf5ede04c1f7169d73b7312e04d3c6e154e0 Mon Sep 17 00:00:00 2001
From: thomasKalts <thomas.kaltsounis@epfl.ch>
Date: Fri, 18 Dec 2020 16:24:01 +0200
Subject: [PATCH 1/2] first commit

---
 include/kitty/threshold_identification.hpp | 263 ++++++++++++++++++++-
 1 file changed, 261 insertions(+), 2 deletions(-)
 mode change 100755 => 100644 include/kitty/threshold_identification.hpp

diff --git a/include/kitty/threshold_identification.hpp b/include/kitty/threshold_identification.hpp
old mode 100755
new mode 100644
index 02533d8e..b8efea47
--- a/include/kitty/threshold_identification.hpp
+++ b/include/kitty/threshold_identification.hpp
@@ -33,8 +33,24 @@
 #pragma once
 
 #include <vector>
-// #include <lpsolve/lp_lib.h> /* uncomment this line to include lp_solve */
+#include <iostream>
+#include <math.h>
+#include <lpsolve/lp_lib.h> /* uncomment this line to include lp_solve */
+//#include <lp_lib.h>
 #include "traits.hpp"
+#include "print.hpp"
+
+#include "static_truth_table.hpp"
+#include "dynamic_truth_table.hpp"
+#include "properties.hpp"
+#include "bit_operations.hpp"
+#include "operations.hpp"
+#include "cube.hpp"
+#include "isop.hpp"
+
+//using namespace std;
+
+
 
 namespace kitty
 {
@@ -59,10 +75,253 @@ 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::cout << to_binary(tt);
 
   /* TODO */
   /* if tt is non-TF: */
-  return false;
+  //return false; 
+
+  int variables = tt.num_vars();  //number of variables
+  TT new_truth_table = tt;
+  int variables_unateness[variables];
+
+  //std::cout << "num vars is" << variables << std::endl;
+  
+
+  for (int i = 0; i<variables ; i++) {
+  
+	  auto F = cofactor1( new_truth_table , i );       //we will use the cofactors to check the unateness
+	  auto F_star = cofactor0( new_truth_table , i );
+	  
+	  //std::cout << "F cofactor is " << to_binary(F) <<std::endl;
+	  //std::cout << "F star cofactor is " << to_binary(F_star) <<std::endl;
+
+	  if (implies( F, F_star )) {	// check negative unateness in i
+			
+		//std::cout << "F is negative unate in " << i <<std::endl;	
+		new_truth_table = flip( new_truth_table , i ); //change bit in variable i
+		variables_unateness[i] = 1;
+
+			  }
+
+	 else if (implies ( F_star , F )) {		//check positive unate in i
+	 
+		//std::cout << "F is positive unate in  "  << i   << std::endl; 
+		variables_unateness[i] = 0;
+	 }
+
+	 else {		// if F is binate in 1 
+		//std::cout << "F is biante !" << std::endl; 
+	 	return false;
+		}
+  	}
+	
+	/*for (int j = 0 ;  j < variables ; j++){
+		std::cout << variables_unateness[j] << std::endl; 
+	} 	*/																					 
+
+	//std::cout << "truth table new is" << to_binary(new_truth_table) << std::endl;
+	
+	 auto F_onset = isop(new_truth_table); // onset of new(fliped) truth table
+	 auto F_offset = isop( unary_not(new_truth_table)); //offset of new (fliped)  truth table
+	 
+	 //std::cout << "size of onset is  " << F_onset.size() <<std::endl;
+	 //std::cout << "size of offset is  " << F_offset.size() << std::endl; 
+
+	//build ilp
+
+  	lprec *lp;
+	int Ncol, *colno = NULL; 
+	REAL *row = NULL;
+	int ret  = 0;
+
+	Ncol = variables + 1;
+	lp = make_lp( 0, Ncol);
+
+	if (lp == NULL)     //couldn't construct a model 
+		return false ; 
+	
+	
+	//colno = (int *) malloc(Ncol * sizeof(*colno));
+	//row = (REAL *) malloc(Ncol * sizeof(*row));
+
+//	if (condition == 0) {  // naming the variables 
+		
+		/*	set_col_name(lp, 1, "w1" );
+			set_col_name(lp, 2, "w2");
+			set_col_name(lp, 3 , "w3");
+		    set_col_name(lp, 4, "w4");
+			set_col_name(lp, 5, "w5");
+			set_col_name(lp, 6, "w6");
+			set_col_name(lp, 7, "w7");
+			set_col_name(lp, 8 ,"w8");
+			set_col_name(lp, 9, "w9");	
+		
+			set_col_name( lp, variables + 1, "T");*/
+			
+			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) { 	//every variable is positive	   INITIAL CONSTRAINTS
+	
+		set_add_rowmode(lp, TRUE);
+
+		for (int i = 0; i<Ncol; i++) {
+			
+			for (int j = 0; j<Ncol; j++){
+				
+			colno[j] = j + 1 ;
+			
+			if (i == j) {
+				
+				row[j] = 1;
+			}
+			
+			else{
+				
+				row[j] = 0;
+				
+			}
+			}
+			
+		add_constraintex(lp, Ncol, row, colno, GE, 0);
+		
+		}
+	
+		
+		for (long unsigned int i = 0 ; i < F_onset.size() ; i++) {   //constraints for the onset set of the function
+			
+			auto ONSET = F_onset.at(i); 
+			
+			for (int k = 0 ; k< variables ; k++) {
+				
+				auto positive = ONSET.get_mask(k);
+				colno[k] = k+1; 
+				
+				if (positive){
+					row[k] = 1;
+					
+				}
+				else  {
+					row[k] = 0 ;
+					
+				}
+			}
+				
+				colno[variables] = Ncol;
+				row[variables] = -1;
+				
+				add_constraintex(lp, Ncol, row, colno, GE , 0);	
+		}
+			
+	}
+	
+	
+	if (ret == 0) {    // constraints with OFFSET set of function 
+	
+	//set_add_rowmode(lp, TRUE);
+	
+		for (long unsigned int i = 0 ; i < F_offset.size() ; i++) {
+			
+			auto OFFSET = F_offset.at(i); 
+		
+			for (int k = 0 ; k< variables ; k++) {
+				
+				colno[k] = k + 1; 
+				auto negative = OFFSET.get_mask(k); 
+				
+				if (negative){
+					row[k] = 0;
+					
+				}
+				else {
+					row[k] = 1 ;
+					
+				}
+			}
+				
+				colno[variables] = Ncol;
+				row[variables] = -1;
+				
+				add_constraintex(lp, Ncol, row, colno, LE , -1);	
+		}
+			
+	} 
+	
+//	std::cout << to_binary(F_onset) << std::endl;
+
+	if (ret == 0 ) {  		//objective function    			//objective function is fine 
+		set_add_rowmode(lp, FALSE);
+
+		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_minim(lp); //object direction to minimize
+		
+		//write_LP(lp, stdout);
+		set_verbose(lp , IMPORTANT);
+		ret = solve(lp);
+		 if (ret == OPTIMAL) {
+			ret = 0;
+		}
+		else {
+			return false ;	
+		} 
+	} 
+
+
+	if (ret == 0) {
+		
+		get_variables(lp, row);
+
+		for (int i =0 ; i<Ncol ; i++) {
+			linear_form.push_back(row[i]); 
+		}
+	}
+	
+	/*for (int j = 0 ;  j < linear_form.size() ; j++){
+		std::cout << linear_form.at(j) << std::endl; 
+	} 	*/
+
+		for (int k = 0; k<variables; k++) {
+			if (variables_unateness[k] == 1){
+				linear_form.at(k) = -linear_form.at(k);	
+				linear_form.at(variables) = linear_form.at(variables) + linear_form.at(k);
+			}
+		}
+
+	
+	if (row != NULL)
+		free(row);
+	
+	if ( colno != NULL) 
+		free(colno);	
+	
+
+	if ( lp != NULL) {
+		delete_lp(lp);
+	}
+	
+  
 
   /* if tt is TF: */
   /* push the weight and threshold values into `linear_form` */

From db860321889da4a4936f5ea5ea80299a25383965 Mon Sep 17 00:00:00 2001
From: thomasKalts <thomas.kaltsounis@epfl.ch>
Date: Fri, 18 Dec 2020 16:37:48 +0200
Subject: [PATCH 2/2] second  commit

---
 include/kitty/threshold_identification.hpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/include/kitty/threshold_identification.hpp b/include/kitty/threshold_identification.hpp
index b8efea47..f79ca143 100644
--- a/include/kitty/threshold_identification.hpp
+++ b/include/kitty/threshold_identification.hpp
@@ -83,7 +83,7 @@ bool is_threshold( const TT& tt, std::vector<int64_t>* plf = nullptr )
 
   int variables = tt.num_vars();  //number of variables
   TT new_truth_table = tt;
-  int variables_unateness[variables];
+  int variables_unateness[15];
 
   //std::cout << "num vars is" << variables << std::endl;