diff --git a/include/kitty/threshold_identification.hpp b/include/kitty/threshold_identification.hpp index 02533d8e..e8dd244c 100755 --- a/include/kitty/threshold_identification.hpp +++ b/include/kitty/threshold_identification.hpp @@ -33,12 +33,174 @@ #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 }; +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 ); + + if( tt_bitwise_greater_equal( cofactor_true, cofactor_false ) ) + { + return POS_UNATE; + } + else if ( tt_bitwise_greater_equal( cofactor_false, cofactor_true ) ) + { + flip_inplace( tt, var_num ); + + return NEG_UNATE; + } + else + { + 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.at(i) = false; + } + else if ( unateness == NEG_UNATE ) + { + should_invert.at(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() ) ); + + // Function to minimize + std::vector obj_fn_row( 2+fstar.num_vars(), 1.0 ); + 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 ); + + for (uint32_t i = 0; i < fstar.num_vars()+1; i++) + { + 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 ); + } + + // 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 ); + + for ( cube cub : on_cubes ) + { + std::fill( ilp_row.begin(), ilp_row.end(), 0.0 ); //reset vector + for (uint32_t i = 0; i < fstar.num_vars(); i++) + { + // If var is in cube and is not inverted + if ( cub.get_bit( i ) && cub.get_mask( i ) ) + { + ilp_row.at( 1+i ) = 1.0; + } + } + ilp_row[ fstar.num_vars()+1 ] = -1.0; + 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 ); + + for ( cube cub : off_cubes ) + { + 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.at( 1+i ) = 1.0; + } + } + 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() ); + + get_variables( lp, result.data() ); + delete_lp(lp); + + linear_form.insert(linear_form.begin(), result.begin(), result.end()); + + + 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) @@ -58,18 +220,38 @@ namespace kitty template::value>> bool is_threshold( const TT& tt, std::vector* plf = nullptr ) { - std::vector linear_form; + std::vector linear_form; + std::vector should_invert( tt.num_vars(), false ); - /* TODO */ - /* if tt is non-TF: */ - return false; + TT tt_fstar = tt; + // Check if function is unate and inverts negative unate variables if needed + if ( !is_unate( tt_fstar, should_invert ) ) + { + return false; + } + + // Solves the ILP problem and checks if there is a solution + if ( !ilp_solve( linear_form, tt_fstar ) ) return false; + + + // 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++) + { + if ( should_invert.at(i) == true ) + { + linear_form.at( tt_fstar.num_vars() ) = linear_form.at( tt_fstar.num_vars() ) - linear_form.at(i); + linear_form.at(i) = -linear_form.at(i); + } + } + /* if tt is TF: */ /* push the weight and threshold values into `linear_form` */ if ( plf ) { *plf = linear_form; } + return true; }