From b42416c83262cee3f00bf11a813eb0dc494e554f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9o=20Johansson?= Date: Sat, 5 Dec 2020 13:07:34 +0100 Subject: [PATCH 1/4] first test change --- 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 02533d8e..76b1648f 100755 --- a/include/kitty/threshold_identification.hpp +++ b/include/kitty/threshold_identification.hpp @@ -60,7 +60,7 @@ bool is_threshold( const TT& tt, std::vector* plf = nullptr ) { std::vector linear_form; - /* TODO */ + /* TODO.. */ /* if tt is non-TF: */ return false; From 690cbcb85a122407d8f6cb381ab8ac10624f31fa Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9o=20Johansson?= Date: Fri, 11 Dec 2020 12:39:26 +0100 Subject: [PATCH 2/4] version 1 still verbose --- include/kitty/threshold_identification.hpp | 264 ++++++++++++++++++++- 1 file changed, 260 insertions(+), 4 deletions(-) diff --git a/include/kitty/threshold_identification.hpp b/include/kitty/threshold_identification.hpp index 76b1648f..2edac3d6 100755 --- a/include/kitty/threshold_identification.hpp +++ b/include/kitty/threshold_identification.hpp @@ -33,12 +33,220 @@ #pragma once #include -// #include /* uncomment this line to include lp_solve */ +#include /* uncomment this line to include lp_solve */ #include "traits.hpp" +#include "isop.hpp" +#include "print.hpp" namespace kitty { + +enum Unate_type { BINATE, POS_UNATE, NEG_UNATE }; +void print_vector(std::vector vec) +{ + for (uint8_t i = 0; i < vec.size(); i++) + { + std::cout << vec.at(i) << " "; + } + std::cout << std::endl; +} + +template::value>> +bool tt_bitwise_less_equal( TT& lhs, TT& rhs ) +{ + assert( lhs.num_vars() == rhs.num_vars() ); + for ( uint64_t i = 0; i < lhs.num_bits(); i++ ) + { + if ( get_bit( lhs, i ) > get_bit( rhs, i ) ) return false; + } + return true; +} + +template::value>> +bool tt_bitwise_greater_equal( TT& lhs, TT& rhs ) +{ + assert( lhs.num_vars() == rhs.num_vars() ); + for ( uint64_t i = 0; i < lhs.num_bits(); i++ ) + { + if ( get_bit( lhs, i ) < get_bit( rhs, i ) ) return false; + } + return true; +} + + +template::value>> +Unate_type is_unate_in_var( uint8_t var_num, TT& tt ) +{ + TT cofactor_true = cofactor1( tt, var_num ); + TT cofactor_false = cofactor0( tt, var_num ); + + std::cout << "Check wether is unate in var " << int(var_num) << std::endl; + + std::cout << "Cofactor true:" << std::endl; + print_binary( cofactor_true, std::cout); + std::cout << std::endl; + std::cout << "Cofactor false:" << std::endl; + print_binary( cofactor_false, std::cout); + std::cout << std::endl; + + + if( tt_bitwise_greater_equal( cofactor_true, cofactor_false ) ) + { + std::cout << "-> is positive unate in Var "<< var_num << var_num << std::endl; + return POS_UNATE; + } + else if ( tt_bitwise_greater_equal( cofactor_false, cofactor_true ) ) + { + std::cout << "-> is negative unate in Var "<< var_num << var_num << std::endl; + flip_inplace( tt, var_num ); + std::cout << "The TT after fliping is: "; + print_binary( tt, std::cout); + std::cout << std::endl; + + return NEG_UNATE; + } + else + { + std::cout << "-> is binate in Var "<< var_num << var_num << std::endl; + return BINATE; + } +} + + +template::value>> +bool is_unate( TT& tt, std::vector& should_invert ) +{ + for ( uint8_t i = 0; i < tt.num_vars(); i++) + { + Unate_type unateness = is_unate_in_var( i, tt); + + if ( unateness == POS_UNATE ) + { + should_invert[i] = false; + } + else if ( unateness == NEG_UNATE ) + { + should_invert[i] = true; + } + else + { + return false; + } + } + + return true; +} + +template::value>> +bool ilp_solve( std::vector& linear_form, const TT& fstar ) +{ + // Create lp context + lprec *lp( make_lp( 0, 1+fstar.num_vars() ) ); + + + std::cout << "Number of Columns = " << get_Ncolumns( lp ) << std::endl; + + // Function to minimize + std::vector obj_fn_row( 2+fstar.num_vars(), 1.0 ); + + std::cout << "Set ojective fun" << std::endl; + print_vector(obj_fn_row); + + set_obj_fn( lp, obj_fn_row.data() ); + set_minim(lp); + + // All weights and T are positive + std::vector ilp_row( 2+fstar.num_vars(), 0.0 ); + + std::cout << "Contraint all positive" << std::endl; + + for (uint32_t i = 0; i < fstar.num_vars()+1; i++) + { + std::fill( ilp_row.begin(), ilp_row.end(), 0.0 ); + ilp_row.at(i+1) = 1.0; + print_vector(ilp_row); + add_constraint( lp, ilp_row.data(), GE, 0.0 ); + } + + // All variables are integers + for( uint8_t i = 1; i < 2+fstar.num_vars(); i++ ) + { + set_int(lp, i, TRUE); + } + + // Define On-set constraints + std::vector on_cubes = isop( fstar ); + + std::cout << "On-set Cubes and constraints" << std::endl; + print_cubes(on_cubes); + + + for ( cube cub : on_cubes ) + { + std::fill( ilp_row.begin(), ilp_row.end(), 0.0 ); + for (uint32_t i = 0; i < fstar.num_vars(); i++) + { + if ( cub.get_bit(i) && cub.get_mask(i) ) + { + ilp_row[i+1] = 1.0; + } + } + ilp_row[ fstar.num_vars()+1 ] = -1.0; + print_vector(ilp_row); + add_constraint( lp, ilp_row.data(), GE, 0.0 ); + } + + // Define Off-set constraints + std::vector off_cubes = isop( unary_not( fstar ) ); + std::fill( ilp_row.begin(), ilp_row.end(), 0.0 ); + + std::cout << "Off-set Cubes and constraints" << std::endl; + print_cubes(off_cubes); + + for ( cube cub : off_cubes ) + { + std::fill( ilp_row.begin(), ilp_row.end(), 0.0 ); + for (uint32_t i = 0; i < fstar.num_vars(); i++) + { + if ( !cub.get_mask(i) || ( cub.get_mask(i) && cub.get_bit(i) ) ) + { + ilp_row[i+1] = 1.0; + } + } + ilp_row[ fstar.num_vars()+1 ] = -1.0; + print_vector(ilp_row); + add_constraint( lp, ilp_row.data(), LE, -1.0 ); + } + + int ilp_status = solve(lp); + std::vector result( 1+fstar.num_vars() ); + + std::cout << "Result vector" << std::endl; + + get_variables( lp, result.data() ); + print_vector(result); + + + std::cout << "Solving status " << ilp_status << std::endl; + /* + for (uint32_t i = 0; i < 1+fstar.num_vars(); i++) + { + linear_form.at(i) = int64_t(result.at(i)); + } + */ + linear_form.insert(linear_form.begin(), result.begin(), result.end()); + std::cout << "End of ILP solving" << std::endl; + delete_lp(lp); + + if ( ilp_status ) + { + return false; + } + + return true; +} + /*! \brief Threshold logic function identification Given a truth table, this function determines whether it is a threshold logic function (TF) @@ -60,16 +268,64 @@ bool is_threshold( const TT& tt, std::vector* plf = nullptr ) { std::vector linear_form; - /* TODO.. */ - /* if tt is non-TF: */ - return false; + std::cout << " ********* Check if threshold function ************" << std::endl; + std::cout << "The TT is: "; + print_binary( tt, std::cout); + std::cout << std::endl; + + std::vector should_invert( tt.num_vars(), false ); + + TT tt_fstar = tt; + + if ( !is_unate( tt_fstar, should_invert ) ) + { + std::cout << "The function is not unate" << std::endl; + return false; + } + + std::cout << "Should invert vector" << std::endl; + for ( uint8_t i = 0; i < should_invert.size(); i++ ) + { + std::cout << should_invert.at(i) << " "; + } + std::cout << std::endl; + + if ( !ilp_solve( linear_form, tt_fstar ) ) return false; + + + std::cout << "Content of linear form before variable recovery:" << std::endl; + for (uint8_t i = 0 ; i < linear_form.size(); i++ ) + { + std::cout << linear_form.at(i) << " "; + } + std::cout << std::endl; + + std::cout << "Let's start variable recovery" << std::endl; + + for (uint64_t i = 0; i < tt_fstar.num_vars(); i++) + { + std::cout << "In the for loop" << std::endl; + if ( should_invert.at(i) == true ) + { + std::cout << "Substract weight" << std::endl; + linear_form.at( tt_fstar.num_vars() ) = linear_form.at( tt_fstar.num_vars() ) - linear_form.at(i); + std::cout << "Change sign" << std::endl; + linear_form.at(i) = -linear_form.at(i); + std::cout << "end of correction "<< i << std::endl; + } + } + + + std::cout << "let's assign the pointer" << std::endl; /* if tt is TF: */ /* push the weight and threshold values into `linear_form` */ if ( plf ) { *plf = linear_form; } + + std::cout << "End of is threshold function" << std::endl; return true; } From 8e5ff14c8025847e5fe3dbdaa0333edac167296d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9o=20Johansson?= Date: Fri, 11 Dec 2020 13:13:23 +0100 Subject: [PATCH 3/4] version 2 no more verbose --- include/kitty/threshold_identification.hpp | 129 +++++---------------- 1 file changed, 30 insertions(+), 99 deletions(-) diff --git a/include/kitty/threshold_identification.hpp b/include/kitty/threshold_identification.hpp index 2edac3d6..926650ed 100755 --- a/include/kitty/threshold_identification.hpp +++ b/include/kitty/threshold_identification.hpp @@ -43,19 +43,11 @@ namespace kitty enum Unate_type { BINATE, POS_UNATE, NEG_UNATE }; -void print_vector(std::vector vec) -{ - for (uint8_t i = 0; i < vec.size(); i++) - { - std::cout << vec.at(i) << " "; - } - std::cout << std::endl; -} - template::value>> bool tt_bitwise_less_equal( TT& lhs, TT& rhs ) { assert( lhs.num_vars() == rhs.num_vars() ); + for ( uint64_t i = 0; i < lhs.num_bits(); i++ ) { if ( get_bit( lhs, i ) > get_bit( rhs, i ) ) return false; @@ -63,10 +55,12 @@ bool tt_bitwise_less_equal( TT& lhs, TT& rhs ) return true; } + template::value>> bool tt_bitwise_greater_equal( TT& lhs, TT& rhs ) { assert( lhs.num_vars() == rhs.num_vars() ); + for ( uint64_t i = 0; i < lhs.num_bits(); i++ ) { if ( get_bit( lhs, i ) < get_bit( rhs, i ) ) return false; @@ -80,35 +74,19 @@ Unate_type is_unate_in_var( uint8_t var_num, TT& tt ) { TT cofactor_true = cofactor1( tt, var_num ); TT cofactor_false = cofactor0( tt, var_num ); - - std::cout << "Check wether is unate in var " << int(var_num) << std::endl; - - std::cout << "Cofactor true:" << std::endl; - print_binary( cofactor_true, std::cout); - std::cout << std::endl; - std::cout << "Cofactor false:" << std::endl; - print_binary( cofactor_false, std::cout); - std::cout << std::endl; - - + if( tt_bitwise_greater_equal( cofactor_true, cofactor_false ) ) { - std::cout << "-> is positive unate in Var "<< var_num << var_num << std::endl; return POS_UNATE; } else if ( tt_bitwise_greater_equal( cofactor_false, cofactor_true ) ) { - std::cout << "-> is negative unate in Var "<< var_num << var_num << std::endl; flip_inplace( tt, var_num ); - std::cout << "The TT after fliping is: "; - print_binary( tt, std::cout); - std::cout << std::endl; return NEG_UNATE; } else { - std::cout << "-> is binate in Var "<< var_num << var_num << std::endl; return BINATE; } } @@ -123,11 +101,11 @@ bool is_unate( TT& tt, std::vector& should_invert ) if ( unateness == POS_UNATE ) { - should_invert[i] = false; + should_invert.at(i) = false; } else if ( unateness == NEG_UNATE ) { - should_invert[i] = true; + should_invert.at(i) = true; } else { @@ -143,29 +121,22 @@ bool ilp_solve( std::vector& linear_form, const TT& fstar ) { // Create lp context lprec *lp( make_lp( 0, 1+fstar.num_vars() ) ); - - - std::cout << "Number of Columns = " << get_Ncolumns( lp ) << std::endl; - + // Function to minimize std::vector obj_fn_row( 2+fstar.num_vars(), 1.0 ); - - std::cout << "Set ojective fun" << std::endl; - print_vector(obj_fn_row); - set_obj_fn( lp, obj_fn_row.data() ); set_minim(lp); + // Remove prints from terminal + set_verbose( lp, 0 ); + // All weights and T are positive std::vector ilp_row( 2+fstar.num_vars(), 0.0 ); - std::cout << "Contraint all positive" << std::endl; - for (uint32_t i = 0; i < fstar.num_vars()+1; i++) { - std::fill( ilp_row.begin(), ilp_row.end(), 0.0 ); - ilp_row.at(i+1) = 1.0; - print_vector(ilp_row); + std::fill( ilp_row.begin(), ilp_row.end(), 0.0 ); //reset vector + ilp_row.at( 1+i ) = 1.0; add_constraint( lp, ilp_row.data(), GE, 0.0 ); } @@ -178,57 +149,45 @@ bool ilp_solve( std::vector& linear_form, const TT& fstar ) // Define On-set constraints std::vector on_cubes = isop( fstar ); - std::cout << "On-set Cubes and constraints" << std::endl; - print_cubes(on_cubes); - - for ( cube cub : on_cubes ) { - std::fill( ilp_row.begin(), ilp_row.end(), 0.0 ); + std::fill( ilp_row.begin(), ilp_row.end(), 0.0 ); //reset vector for (uint32_t i = 0; i < fstar.num_vars(); i++) { - if ( cub.get_bit(i) && cub.get_mask(i) ) + // If var is in cube and is not inverted + if ( cub.get_bit( i ) && cub.get_mask( i ) ) { - ilp_row[i+1] = 1.0; + ilp_row.at( 1+i ) = 1.0; } } ilp_row[ fstar.num_vars()+1 ] = -1.0; - print_vector(ilp_row); add_constraint( lp, ilp_row.data(), GE, 0.0 ); } // Define Off-set constraints std::vector off_cubes = isop( unary_not( fstar ) ); std::fill( ilp_row.begin(), ilp_row.end(), 0.0 ); - - std::cout << "Off-set Cubes and constraints" << std::endl; - print_cubes(off_cubes); - + for ( cube cub : off_cubes ) { - std::fill( ilp_row.begin(), ilp_row.end(), 0.0 ); + std::fill( ilp_row.begin(), ilp_row.end(), 0.0 ); //reset vector for (uint32_t i = 0; i < fstar.num_vars(); i++) { if ( !cub.get_mask(i) || ( cub.get_mask(i) && cub.get_bit(i) ) ) { - ilp_row[i+1] = 1.0; + ilp_row.at( 1+i ) = 1.0; } } - ilp_row[ fstar.num_vars()+1 ] = -1.0; - print_vector(ilp_row); + ilp_row.at( fstar.num_vars()+1 ) = -1.0; add_constraint( lp, ilp_row.data(), LE, -1.0 ); } int ilp_status = solve(lp); std::vector result( 1+fstar.num_vars() ); - - std::cout << "Result vector" << std::endl; - + get_variables( lp, result.data() ); - print_vector(result); - + delete_lp(lp); - std::cout << "Solving status " << ilp_status << std::endl; /* for (uint32_t i = 0; i < 1+fstar.num_vars(); i++) { @@ -236,8 +195,8 @@ bool ilp_solve( std::vector& linear_form, const TT& fstar ) } */ linear_form.insert(linear_form.begin(), result.begin(), result.end()); - std::cout << "End of ILP solving" << std::endl; - delete_lp(lp); + + if ( ilp_status ) { @@ -266,66 +225,38 @@ bool ilp_solve( std::vector& linear_form, const TT& fstar ) template::value>> bool is_threshold( const TT& tt, std::vector* plf = nullptr ) { - std::vector linear_form; - - - std::cout << " ********* Check if threshold function ************" << std::endl; - std::cout << "The TT is: "; - print_binary( tt, std::cout); - std::cout << std::endl; - + std::vector linear_form; std::vector should_invert( tt.num_vars(), false ); TT tt_fstar = tt; + // Check if function is unate and inverts negative unate variables if needed if ( !is_unate( tt_fstar, should_invert ) ) { - std::cout << "The function is not unate" << std::endl; return false; } - - std::cout << "Should invert vector" << std::endl; - for ( uint8_t i = 0; i < should_invert.size(); i++ ) - { - std::cout << should_invert.at(i) << " "; - } - std::cout << std::endl; - + + // Solves the ILP problem and checks if there is a solution if ( !ilp_solve( linear_form, tt_fstar ) ) return false; - std::cout << "Content of linear form before variable recovery:" << std::endl; - for (uint8_t i = 0 ; i < linear_form.size(); i++ ) - { - std::cout << linear_form.at(i) << " "; - } - std::cout << std::endl; - - std::cout << "Let's start variable recovery" << std::endl; - + // Corrects the linear form vector associated with fstar to get the one associated with f for (uint64_t i = 0; i < tt_fstar.num_vars(); i++) { - std::cout << "In the for loop" << std::endl; if ( should_invert.at(i) == true ) { - std::cout << "Substract weight" << std::endl; linear_form.at( tt_fstar.num_vars() ) = linear_form.at( tt_fstar.num_vars() ) - linear_form.at(i); - std::cout << "Change sign" << std::endl; linear_form.at(i) = -linear_form.at(i); - std::cout << "end of correction "<< i << std::endl; } } - - std::cout << "let's assign the pointer" << std::endl; /* if tt is TF: */ /* push the weight and threshold values into `linear_form` */ if ( plf ) { *plf = linear_form; } - - std::cout << "End of is threshold function" << std::endl; + return true; } From 79706177adf8dcb23ae8cc08b77ba8af87eb2f74 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9o=20Johansson?= Date: Sat, 19 Dec 2020 21:27:42 +0100 Subject: [PATCH 4/4] ve3 clean un-used sections --- include/kitty/threshold_identification.hpp | 9 ++------- 1 file changed, 2 insertions(+), 7 deletions(-) diff --git a/include/kitty/threshold_identification.hpp b/include/kitty/threshold_identification.hpp index 926650ed..e8dd244c 100755 --- a/include/kitty/threshold_identification.hpp +++ b/include/kitty/threshold_identification.hpp @@ -116,6 +116,7 @@ bool is_unate( TT& tt, std::vector& should_invert ) return true; } + template::value>> bool ilp_solve( std::vector& linear_form, const TT& fstar ) { @@ -188,16 +189,9 @@ bool ilp_solve( std::vector& linear_form, const TT& fstar ) get_variables( lp, result.data() ); delete_lp(lp); - /* - for (uint32_t i = 0; i < 1+fstar.num_vars(); i++) - { - linear_form.at(i) = int64_t(result.at(i)); - } - */ linear_form.insert(linear_form.begin(), result.begin(), result.end()); - if ( ilp_status ) { return false; @@ -206,6 +200,7 @@ bool ilp_solve( std::vector& linear_form, const TT& fstar ) return true; } + /*! \brief Threshold logic function identification Given a truth table, this function determines whether it is a threshold logic function (TF)