From 07e03c9a6c7622a7bb5de225adf9040130fc4b00 Mon Sep 17 00:00:00 2001 From: Kyritsisapo <75628885+Kyritsisapo@users.noreply.github.com> Date: Thu, 17 Dec 2020 17:33:50 +0100 Subject: [PATCH 1/2] Update threshold_identification.hpp --- include/kitty/threshold_identification.hpp | 233 +++++++++++++++++++-- 1 file changed, 217 insertions(+), 16 deletions(-) diff --git a/include/kitty/threshold_identification.hpp b/include/kitty/threshold_identification.hpp index 02533d8e..1de27c1c 100755 --- a/include/kitty/threshold_identification.hpp +++ b/include/kitty/threshold_identification.hpp @@ -33,8 +33,20 @@ #pragma once #include -// #include /* uncomment this line to include lp_solve */ +#include +#include +#include +#include #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,211 @@ namespace kitty in the end. \return `true` if `tt` is a TF; `false` if `tt` is a non-TF. */ + + template::value>> bool is_threshold( const TT& tt, std::vector* plf = nullptr ) -{ - std::vector 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 inv_var(ttable.num_vars(),false); + std::vector linear_form; + auto num_vars = ttable.num_vars(); + bool n, p; + //std::cout << num_vars <<" number of variables \n"; + + + + 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 if they are 1, then add, otherwise dont + 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; + + } + } + // 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; + + } + + } + // 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 */ +} From 8be5fa0ffb7758934e2614e29a44825259edbad5 Mon Sep 17 00:00:00 2001 From: Kyritsisapo <75628885+Kyritsisapo@users.noreply.github.com> Date: Fri, 18 Dec 2020 01:31:56 +0100 Subject: [PATCH 2/2] Update threshold_identification.hpp final --- include/kitty/threshold_identification.hpp | 29 ++++++++++------------ 1 file changed, 13 insertions(+), 16 deletions(-) diff --git a/include/kitty/threshold_identification.hpp b/include/kitty/threshold_identification.hpp index 1de27c1c..bad30099 100755 --- a/include/kitty/threshold_identification.hpp +++ b/include/kitty/threshold_identification.hpp @@ -72,15 +72,12 @@ namespace kitty template::value>> bool is_threshold( const TT& tt, std::vector* plf = nullptr ) { - TT ttable = tt; - std::vector inv_var(ttable.num_vars(),false); + TT ttable = tt; + std::vector inv_var(ttable.num_vars(),false); std::vector linear_form; auto num_vars = ttable.num_vars(); bool n, p; - //std::cout << num_vars <<" number of variables \n"; - - - + for (int i = 0; i< num_vars; i++){ n=p=false; @@ -143,14 +140,14 @@ bool is_threshold( const TT& tt, std::vector* plf = nullptr ) for(int j = 0; j < Ncol; j++){ auto k = 0; - colno[k] = j+1; - row[j] = ++k; + 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 if they are 1, then add, otherwise dont + // 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); @@ -164,12 +161,12 @@ bool is_threshold( const TT& tt, std::vector* plf = nullptr ) }else{ - colno[j] = j+1; + colno[j] = j+1; row[j] = 0; } } - // x1 + x2 >= T -> x1 + x2 - T >= 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); @@ -185,18 +182,18 @@ bool is_threshold( const TT& tt, std::vector* plf = nullptr ) if(term.get_mask(j)){ - colno[j] = j+1; + colno[j] = j+1; row[j] = 0; }else{ - colno[j] = j+1; + colno[j] = j+1; row[j] = 1; } } - // x1 + x2 <= T - 1 -> x1 + x2 - T <= -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); @@ -215,7 +212,7 @@ bool is_threshold( const TT& tt, std::vector* plf = nullptr ) if(!set_obj_fnex(lp, Ncol, row, colno)) - return false; + return false; } if(ret == 0) { //set for minimization (code from lpsolve.sourceforge) @@ -229,7 +226,7 @@ bool is_threshold( const TT& tt, std::vector* plf = nullptr ) ret = 0; else - return false; + return false; } if(ret == 0) { // fill the linear form