diff --git a/docs/utils/util_data_structures.rst b/docs/utils/util_data_structures.rst index 1e5850112..67e59e590 100644 --- a/docs/utils/util_data_structures.rst +++ b/docs/utils/util_data_structures.rst @@ -166,16 +166,11 @@ Cut sets .. _index_list: -Index List +Index list ~~~~~~~~~~ **Header:** ``mockturtle/utils/index_list.hpp`` -.. doxygenstruct:: mockturtle::abc_index_list -.. doxygenfunction:: mockturtle::encode( abc_index_list&, Ntk const& ) -.. doxygenfunction:: mockturtle::insert( Ntk&, BeginIter, EndIter, abc_index_list const&, Fn&& ) -.. doxygenfunction:: mockturtle::to_index_list_string( abc_index_list const& ) - .. doxygenstruct:: mockturtle::mig_index_list .. doxygenfunction:: mockturtle::encode( mig_index_list&, Ntk const& ) .. doxygenfunction:: mockturtle::insert( Ntk&, BeginIter, EndIter, mig_index_list const&, Fn&& ) diff --git a/include/CMakeLists.txt b/include/CMakeLists.txt index 808310180..96c1a3b82 100644 --- a/include/CMakeLists.txt +++ b/include/CMakeLists.txt @@ -1,6 +1,6 @@ add_library(mockturtle INTERFACE) target_include_directories(mockturtle SYSTEM INTERFACE ${PROJECT_SOURCE_DIR}/include) -target_link_libraries(mockturtle INTERFACE kitty lorina parallel_hashmap percy json bill libabcesop abcresub) +target_link_libraries(mockturtle INTERFACE kitty lorina parallel_hashmap percy json bill libabcesop) if(CMAKE_CXX_COMPILER_ID STREQUAL "GNU" AND CMAKE_CXX_COMPILER_VERSION VERSION_LESS 9) target_link_libraries(mockturtle INTERFACE stdc++fs) diff --git a/include/mockturtle/algorithms/circuit_validator.hpp b/include/mockturtle/algorithms/circuit_validator.hpp index 6b57fe4d8..45f0afc44 100644 --- a/include/mockturtle/algorithms/circuit_validator.hpp +++ b/include/mockturtle/algorithms/circuit_validator.hpp @@ -210,8 +210,7 @@ class circuit_validator template std::optional validate( node const& root, iterator_type divs_begin, iterator_type divs_end, index_list_type const& id_list, bool inverted = false ) { - static_assert( std::is_same_v || - std::is_same_v || + static_assert( std::is_same_v || std::is_same_v> || std::is_same_v> || std::is_same_v, "Unknown type of index list" ); @@ -240,7 +239,7 @@ class circuit_validator push(); } - if constexpr ( std::is_same_v || std::is_same_v> || std::is_same_v> ) + if constexpr ( std::is_same_v> || std::is_same_v> ) { id_list.foreach_gate( [&]( uint32_t id_lit0, uint32_t id_lit1 ) { uint32_t const node_pos0 = id_lit0 >> 1; diff --git a/include/mockturtle/algorithms/resyn_engines/xag_resyn.hpp b/include/mockturtle/algorithms/resyn_engines/xag_resyn.hpp index fafe8f283..a7c3628e5 100644 --- a/include/mockturtle/algorithms/resyn_engines/xag_resyn.hpp +++ b/include/mockturtle/algorithms/resyn_engines/xag_resyn.hpp @@ -37,7 +37,6 @@ #include "../../utils/node_map.hpp" #include "../../utils/stopwatch.hpp" -#include #include #include @@ -873,130 +872,4 @@ class xag_resyn_decompose stats& st; }; /* xag_resyn_decompose */ -struct xag_resyn_abc_stats -{ -}; - -template> -class xag_resyn_abc -{ -public: - using stats = xag_resyn_abc_stats; - using index_list_t = large_xag_index_list; - using truth_table_t = TT; - - explicit xag_resyn_abc( stats& st ) noexcept - : st( st ), counter( 0 ) - { - static_assert( std::is_same_v, "Invalid static_params type" ); - static_assert( !static_params::preserve_depth && static_params::uniform_div_cost, "Advanced resynthesis is not implemented for this solver" ); - } - - virtual ~xag_resyn_abc() - { - abcresub::Abc_ResubPrepareManager( 0 ); - release(); - } - - template - std::optional operator()( TT const& target, TT const& care, iterator_type begin, iterator_type end, truth_table_storage_type const& tts, uint32_t max_size = std::numeric_limits::max(), uint32_t max_level = std::numeric_limits::max() ) - { - (void)max_level; - num_divisors = std::distance( begin, end ) + 2; - num_blocks_per_truth_table = target.num_blocks(); - abcresub::Abc_ResubPrepareManager( num_blocks_per_truth_table ); - alloc(); - - add_divisor( ~target & care ); /* off-set */ - add_divisor( target & care ); /* on-set */ - - while ( begin != end ) - { - add_divisor( tts[*begin] ); - ++begin; - } - - return compute_function( max_size ); - } - -protected: - void add_divisor( TT const& tt ) - { - assert( tt.num_blocks() == num_blocks_per_truth_table ); - for ( uint64_t i = 0ul; i < num_blocks_per_truth_table; ++i ) - { - if constexpr ( std::is_same_v || std::is_same_v ) - Vec_WrdPush( abc_tts, tt._bits[i] ); - else // static_truth_table - Vec_WrdPush( abc_tts, tt._bits ); - } - Vec_PtrPush( abc_divs, Vec_WrdEntryP( abc_tts, counter * num_blocks_per_truth_table ) ); - ++counter; - } - - std::optional compute_function( uint32_t num_inserts ) - { - int nLimit = num_inserts > std::numeric_limits::max() ? std::numeric_limits::max() : num_inserts; - int* raw_list; - int size = abcresub::Abc_ResubComputeFunction( - /* ppDivs */ (void**)Vec_PtrArray( abc_divs ), - /* nDivs */ Vec_PtrSize( abc_divs ), - /* nWords */ num_blocks_per_truth_table, - /* nLimit */ nLimit, - /* nDivsMax */ static_params::max_binates, - /* iChoice */ 0, /* fUseXor */ int( static_params::use_xor ), /* fDebug */ 0, /* fVerbose */ 0, - /* ppArray */ &raw_list ); - - if ( size ) - { - index_list_t xag_list; - xag_list.add_inputs( num_divisors - 2 ); - for ( int i = 0; i < size - 1; i += 2 ) - { - if ( raw_list[i] < raw_list[i + 1] ) - xag_list.add_and( raw_list[i] - 2, raw_list[i + 1] - 2 ); - else - xag_list.add_xor( raw_list[i] - 2, raw_list[i + 1] - 2 ); - } - xag_list.add_output( raw_list[size - 1] < 2 ? raw_list[size - 1] : raw_list[size - 1] - 2 ); - return xag_list; - } - - return std::nullopt; - } - - void dump( std::string const file = "dump.txt" ) const - { - abcresub::Abc_ResubDumpProblem( file.c_str(), (void**)Vec_PtrArray( abc_divs ), Vec_PtrSize( abc_divs ), num_blocks_per_truth_table ); - } - - void alloc() - { - assert( abc_tts == nullptr ); - assert( abc_divs == nullptr ); - abc_tts = abcresub::Vec_WrdAlloc( num_divisors * num_blocks_per_truth_table ); - abc_divs = abcresub::Vec_PtrAlloc( num_divisors ); - } - - void release() - { - assert( abc_divs != nullptr ); - assert( abc_tts != nullptr ); - Vec_PtrFree( abc_divs ); - Vec_WrdFree( abc_tts ); - abc_divs = nullptr; - abc_tts = nullptr; - } - -protected: - uint64_t num_divisors; - uint64_t num_blocks_per_truth_table; - uint64_t counter; - - abcresub::Vec_Wrd_t* abc_tts{ nullptr }; - abcresub::Vec_Ptr_t* abc_divs{ nullptr }; - - stats& st; -}; /* xag_resyn_abc */ - } /* namespace mockturtle */ \ No newline at end of file diff --git a/include/mockturtle/algorithms/window_rewriting.hpp b/include/mockturtle/algorithms/window_rewriting.hpp index ec928b52e..a35ef2d6a 100644 --- a/include/mockturtle/algorithms/window_rewriting.hpp +++ b/include/mockturtle/algorithms/window_rewriting.hpp @@ -1,5 +1,5 @@ /* mockturtle: C++ logic network library - * Copyright (C) 2018-2022 EPFL + * Copyright (C) 2018-2023 EPFL * * Permission is hereby granted, free of charge, to any person * obtaining a copy of this software and associated documentation @@ -31,9 +31,13 @@ \author Siang-Yun (Sonia) Lee */ +#include "../networks/aig.hpp" #include "../networks/events.hpp" +#include "../networks/xag.hpp" #include "../utils/debugging_utils.hpp" #include "../utils/index_list.hpp" +#include "../utils/network_utils.hpp" +#include "../utils/node_map.hpp" #include "../utils/stopwatch.hpp" #include "../utils/window_utils.hpp" #include "../views/color_view.hpp" @@ -41,9 +45,12 @@ #include "../views/fanout_view.hpp" #include "../views/topo_view.hpp" #include "../views/window_view.hpp" +#include "detail/resub_utils.hpp" +#include "resyn_engines/xag_resyn.hpp" +#include "simulation.hpp" -#include #include +#include #include #pragma once @@ -77,6 +84,8 @@ struct window_rewriting_params recompute, } level_update_strategy = dont_update; + uint64_t max_num_divs{ 100 }; + bool filter_cyclic_substitutions{ false }; }; /* window_rewriting_params */ @@ -103,10 +112,29 @@ struct window_rewriting_stats /*! \brief Time for encoding index_list. */ stopwatch<>::duration time_encode{ 0 }; + /*! \brief Time for computing dependency circuit. */ + stopwatch<>::duration time_resyn{ 0 }; + + /*! \brief Time for simulation. */ + stopwatch<>::duration time_simulate{ 0 }; + + /*! \brief Time for marking TFO and MFFC. */ + stopwatch<>::duration time_mark{ 0 }; + + /*! \brief Time for adding divisor truth tables. */ + stopwatch<>::duration time_add_divisor{ 0 }; + + /*! \brief Time for substitution within windows. */ + stopwatch<>::duration time_window_substitute{ 0 }; + + /*! \brief Time for constructing fanout_view within windows. */ + stopwatch<>::duration time_fanout_view{ 0 }; + /*! \brief Time for detecting cycles. */ stopwatch<>::duration time_cycle{ 0 }; /*! \brief Total number of calls to the resub. engine. */ + uint64_t num_resyn_invokes{ 0 }; uint64_t num_substitutions{ 0 }; uint64_t num_restrashes{ 0 }; uint64_t num_windows{ 0 }; @@ -121,9 +149,16 @@ struct window_rewriting_stats time_levels += other.time_levels; time_topo_sort += other.time_topo_sort; time_encode += other.time_encode; + time_resyn += other.time_resyn; + time_simulate += other.time_simulate; + time_mark += other.time_mark; + time_add_divisor += other.time_add_divisor; + time_window_substitute += other.time_window_substitute; + time_fanout_view += other.time_fanout_view; num_substitutions += other.num_substitutions; num_restrashes += other.num_restrashes; num_windows += other.num_windows; + num_resyn_invokes += other.num_resyn_invokes; gain += other.gain; return *this; } @@ -138,8 +173,14 @@ struct window_rewriting_stats to_seconds( time_window ), to_seconds( time_window ) / to_seconds( time_total ) * 100, num_windows ); fmt::print( "[i] Top.sort = {:7.2f} ({:5.2f}%)\n", to_seconds( time_topo_sort ), to_seconds( time_topo_sort ) / to_seconds( time_total ) * 100 ); fmt::print( "[i] Enc.list = {:7.2f} ({:5.2f}%)\n", to_seconds( time_encode ), to_seconds( time_encode ) / to_seconds( time_total ) * 100 ); - fmt::print( "[i] Optimize = {:7.2f} ({:5.2f}%) (#resubs = {}, est. gain = {})\n", - to_seconds( time_optimize ), to_seconds( time_optimize ) / to_seconds( time_total ) * 100, num_substitutions, gain ); + fmt::print( "[i] Optimize = {:7.2f} ({:5.2f}%) (#invokes = {}, #resubs = {}, est. gain = {})\n", + to_seconds( time_optimize ), to_seconds( time_optimize ) / to_seconds( time_total ) * 100, num_resyn_invokes, num_substitutions, gain ); + fmt::print( "[i] >> resynthesis = {:7.2f} ({:5.2f}%)\n", to_seconds( time_resyn ), to_seconds( time_resyn ) / to_seconds( time_optimize ) * 100 ); + fmt::print( "[i] >> simulate = {:7.2f} ({:5.2f}%)\n", to_seconds( time_simulate ), to_seconds( time_simulate ) / to_seconds( time_optimize ) * 100 ); + fmt::print( "[i] >> marking = {:7.2f} ({:5.2f}%)\n", to_seconds( time_mark ), to_seconds( time_mark ) / to_seconds( time_optimize ) * 100 ); + fmt::print( "[i] >> add div. = {:7.2f} ({:5.2f}%)\n", to_seconds( time_add_divisor ), to_seconds( time_add_divisor ) / to_seconds( time_optimize ) * 100 ); + fmt::print( "[i] >> substitute = {:7.2f} ({:5.2f}%)\n", to_seconds( time_window_substitute ), to_seconds( time_window_substitute ) / to_seconds( time_optimize ) * 100 ); + fmt::print( "[i] >> fanout_view = {:7.2f} ({:5.2f}%)\n", to_seconds( time_fanout_view ), to_seconds( time_fanout_view ) / to_seconds( time_optimize ) * 100 ); fmt::print( "[i] Substitute = {:7.2f} ({:5.2f}%) (#hash upd. = {})\n", to_seconds( time_substitute ), to_seconds( time_substitute ) / to_seconds( time_total ) * 100, @@ -195,7 +236,15 @@ bool is_contained_in_tfi( Ntk const& ntk, typename Ntk::node const& node, typena namespace detail { -template +template +struct resyn_sparams : public xag_resyn_static_params +{ + using truth_table_storage_type = node_map; + using node_type = typename NtkWin::signal; + static constexpr bool use_xor = false; +}; + +template>> class window_rewriting_impl { public: @@ -207,7 +256,7 @@ class window_rewriting_impl : ntk( ntk ), ps( ps ), st( st ) /* initialize levels to network depth */ , - levels( ntk.depth() ) + levels( ntk.depth() ), engine( engine_st ) { register_events(); } @@ -223,6 +272,15 @@ class window_rewriting_impl { stopwatch t( st.time_total ); + if constexpr ( std::is_same_v ) + { + sim = new default_simulator( ps.cut_size ); + } + else + { + sim = new default_simulator(); + } + create_window_impl windowing( ntk ); uint32_t const size = ntk.size(); for ( uint32_t n = 0u; n < size; ++n ) @@ -232,23 +290,16 @@ class window_rewriting_impl continue; } - if ( const auto w = call_with_stopwatch( st.time_window, [&]() { return windowing.run( n, ps.cut_size, ps.num_levels ); } ) ) + if ( auto w = call_with_stopwatch( st.time_window, [&]() { return windowing.run( n, ps.cut_size, ps.num_levels ); } ) ) { ++st.num_windows; - auto topo_win = call_with_stopwatch( st.time_topo_sort, ( [&]() { - window_view win( ntk, w->inputs, w->outputs, w->nodes ); - topo_view topo_win{ win }; - return topo_win; - } ) ); - - abc_index_list il; + NtkWin win; call_with_stopwatch( st.time_encode, [&]() { - encode( il, topo_win ); + clone_subnetwork( ntk, w->inputs, w->outputs, w->nodes, win ); } ); - auto il_opt = optimize( il ); - if ( !il_opt ) + if ( !optimize( win ) ) { continue; } @@ -259,48 +310,42 @@ class window_rewriting_impl signals.push_back( ntk.make_signal( i ) ); } - std::vector outputs; - topo_win.foreach_co( [&]( signal const& o ) { - outputs.push_back( o ); - } ); - uint32_t counter{ 0 }; ++st.num_substitutions; - /* ensure that no dead nodes are reachable */ assert( count_reachable_dead_nodes( ntk ) == 0u ); std::list> substitutions; - insert( ntk, std::begin( signals ), std::end( signals ), *il_opt, - [&]( signal const& _new ) { - assert( !ntk.is_dead( ntk.get_node( _new ) ) ); - auto const _old = outputs.at( counter++ ); - if ( _old == _new ) - { - return true; - } - - /* ensure that _old is not in the TFI of _new */ - // assert( !is_contained_in_tfi( ntk, ntk.get_node( _new ), ntk.get_node( _old ) ) ); - if ( ps.filter_cyclic_substitutions && - call_with_stopwatch( st.time_window, [&]() { return is_contained_in_tfi( ntk, ntk.get_node( _new ), ntk.get_node( _old ) ); } ) ) - { - std::cout << "undo resubstitution " << ntk.get_node( _old ) << std::endl; - substitutions.emplace_back( std::make_pair( ntk.get_node( _old ), ntk.is_complemented( _old ) ? !_new : _new ) ); - for ( auto it = std::rbegin( substitutions ); it != std::rend( substitutions ); ++it ) - { - if ( ntk.fanout_size( ntk.get_node( it->second ) ) == 0u ) + insert_ntk( ntk, std::begin( signals ), std::end( signals ), win, + [&]( signal const& _new ) { + assert( !ntk.is_dead( ntk.get_node( _new ) ) ); + auto const _old = w->outputs.at( counter++ ); + if ( _old == _new ) { - ntk.take_out_node( ntk.get_node( it->second ) ); + return true; } - } - substitutions.clear(); - return false; - } - substitutions.emplace_back( std::make_pair( ntk.get_node( _old ), ntk.is_complemented( _old ) ? !_new : _new ) ); - return true; - } ); + /* ensure that _old is not in the TFI of _new */ + // assert( !is_contained_in_tfi( ntk, ntk.get_node( _new ), ntk.get_node( _old ) ) ); + if ( ps.filter_cyclic_substitutions && + call_with_stopwatch( st.time_window, [&]() { return is_contained_in_tfi( ntk, ntk.get_node( _new ), ntk.get_node( _old ) ); } ) ) + { + std::cout << "undo resubstitution " << ntk.get_node( _old ) << std::endl; + substitutions.emplace_back( std::make_pair( ntk.get_node( _old ), ntk.is_complemented( _old ) ? !_new : _new ) ); + for ( auto it = std::rbegin( substitutions ); it != std::rend( substitutions ); ++it ) + { + if ( ntk.fanout_size( ntk.get_node( it->second ) ) == 0u ) + { + ntk.take_out_node( ntk.get_node( it->second ) ); + } + } + substitutions.clear(); + return false; + } + + substitutions.emplace_back( std::make_pair( ntk.get_node( _old ), ntk.is_complemented( _old ) ? !_new : _new ) ); + return true; + } ); /* ensure that no dead nodes are reachable */ assert( count_reachable_dead_nodes( ntk ) == 0u ); @@ -336,6 +381,8 @@ class window_rewriting_impl /* ensure that no dead nodes are reachable */ assert( count_reachable_dead_nodes( ntk ) == 0u ); + + delete sim; } private: @@ -364,58 +411,126 @@ class window_rewriting_impl delete_event = ntk.events().register_delete_event( update_level_of_deleted_node ); } - /* optimize an index_list and return the new list */ - std::optional optimize( abc_index_list const& il, bool verbose = false ) + bool optimize( NtkWin& win ) { stopwatch t( st.time_optimize ); + bool changed = false; - int* raw = ABC_CALLOC( int, il.size() + 1u ); - uint64_t i = 0; - for ( auto const& v : il.raw() ) - { - raw[i++] = v; - } - raw[1] = 0; /* fix encoding */ + node_map tts = call_with_stopwatch( st.time_simulate, [&]() { + return simulate_nodes( win, *sim ); + } ); + auto win_add_event = win.events().register_add_event( [&]( auto const& n ) { + call_with_stopwatch( st.time_simulate, [&]() { + tts.resize(); + std::vector fanin_values( win.fanin_size( n ) ); + win.foreach_fanin( n, [&]( auto const& f, auto i ) { + fanin_values[i] = tts[f]; + } ); + tts[n] = win.compute( n, fanin_values.begin(), fanin_values.end() ); + } ); + } ); + fanout_view fanout_win = make_with_stopwatch, NtkWin&>( st.time_fanout_view, win ); + // fanout_view fanout_win{win}; - abcresub::Abc_ResubPrepareManager( 1 ); - int* new_raw = nullptr; - int num_resubs = 0; - uint64_t new_entries = abcresub::Abc_ResubComputeWindow( raw, ( il.size() / 2u ), 1000, -1, 0, 0, 0, 0, &new_raw, &num_resubs ); - abcresub::Abc_ResubPrepareManager( 0 ); + win.foreach_po( [&]( auto const& f ) { + auto root = win.get_node( f ); + if ( win.value( root ) != 1 ) + { + win.set_value( root, 1 ); + changed |= optimize_node( win, fanout_win, tts, root ); + } + } ); - if ( verbose ) - { - fmt::print( "Performed resub {} times. Reduced {} nodes.\n", - num_resubs, new_entries > 0 ? ( ( il.size() / 2u ) - new_entries ) : 0 ); - } - st.gain += new_entries > 0 ? ( ( il.size() / 2u ) - new_entries ) : 0; + win.foreach_gate( [&]( auto const& root ) { + if ( win.value( root ) != 1 ) + { + win.set_value( root, 1 ); + bool all_fanin_is_pi = true; + win.foreach_fanin( root, [&]( auto const& fi ) { + if ( !win.is_pi( win.get_node( fi ) ) ) + { + all_fanin_is_pi = false; + } + } ); + if ( !all_fanin_is_pi ) + changed |= optimize_node( win, fanout_win, tts, root ); + } + } ); - if ( raw ) - { - ABC_FREE( raw ); - } + win.events().release_add_event( win_add_event ); + return changed; + } - if ( new_entries > 0 ) - { - std::vector values; - for ( uint32_t i = 0; i < 2 * new_entries; ++i ) + bool optimize_node( NtkWin& win, fanout_view& fanout_win, node_map& tts, typename NtkWin::node const& root ) + { + st.num_resyn_invokes++; + + auto mffc_size = call_with_stopwatch( st.time_mark, [&]() { + /* mark MFFC */ + std::vector mffc; + node_mffc_inside mffc_mgr( win ); + auto mffc_size = mffc_mgr.run( root, {}, mffc ); + win.incr_trav_id(); + for ( auto const& n : mffc ) { - values.push_back( new_raw[i] ); + win.set_visited( n, win.trav_id() ); } - values[1u] = 1; /* fix encoding */ - if ( new_raw ) + /* mark TFO */ + mark_tfo( fanout_win, root ); + + /* exclude constant node */ + if constexpr ( std::is_same_v || std::is_same_v ) { - ABC_FREE( new_raw ); + win.set_visited( win.get_node( win.get_constant( false ) ), win.trav_id() ); } - return abc_index_list( values, il.num_pis() ); - } - else + return mffc_size; + } ); + + /* add divisors (all nodes in the window except TFO and MFFC) */ + std::vector divs; + call_with_stopwatch( st.time_add_divisor, [&]() { + win.foreach_node( [&]( auto const& n ) { + if ( win.visited( n ) != win.trav_id() ) + { + divs.emplace_back( win.make_signal( n ) ); + if ( divs.size() > ps.max_num_divs ) + { + return false; + } + } + return true; + } ); + } ); + + /* run resynthesis */ + auto const il = call_with_stopwatch( st.time_resyn, [&]() { + return engine( tts[root], ~tts[win.get_constant( false )], divs.begin(), divs.end(), tts, mffc_size - 1 ); + } ); + if ( il ) { - assert( new_raw == nullptr ); - return std::nullopt; + st.gain += mffc_size - il->num_gates(); + call_with_stopwatch( st.time_window_substitute, [&]() { + insert( win, divs.begin(), divs.end(), *il, [&]( auto const& s ) { + win.substitute_node( root, s ); + } ); + } ); + return true; } + return false; } + void mark_tfo( fanout_view& fanout_win, typename NtkWin::node const& n ) + { + fanout_win.set_visited( n, fanout_win.trav_id() ); + fanout_win.foreach_fanout( n, [&]( auto const& fo ) { + if ( fanout_win.visited( fo ) != fanout_win.trav_id() ) + { + mark_tfo( fanout_win, fo ); + } + } ); + } + +private: void substitute_nodes( std::list> substitutions ) { stopwatch t( st.time_substitute ); @@ -656,7 +771,11 @@ class window_rewriting_impl std::shared_ptr::add_event_type> add_event; std::shared_ptr::modified_event_type> modified_event; std::shared_ptr::delete_event_type> delete_event; -}; + + default_simulator* sim; + typename ResynEngine::stats engine_st; + ResynEngine engine; +}; /* window_rewriting_impl */ } /* namespace detail */ @@ -668,12 +787,13 @@ void window_rewriting( Ntk& ntk, window_rewriting_params const& ps = {}, window_ color_view cntk{ dntk }; window_rewriting_stats st; - detail::window_rewriting_impl p( cntk, ps, st ); - p.run(); + using NtkWin = typename Ntk::base_type; + using TT = kitty::dynamic_truth_table; + detail::window_rewriting_impl( cntk, ps, st ).run(); if ( pst ) { *pst = st; } } -} /* namespace mockturtle */ \ No newline at end of file +} /* namespace mockturtle */ diff --git a/include/mockturtle/utils/index_list.hpp b/include/mockturtle/utils/index_list.hpp index 95c0befa8..74674812c 100644 --- a/include/mockturtle/utils/index_list.hpp +++ b/include/mockturtle/utils/index_list.hpp @@ -43,328 +43,6 @@ namespace mockturtle { -/*! \brief An ABC-compatible index list. - * - * Small network represented as a list of literals. The - * implementation supports AND and XOR gates and is compatible with - * ABC's encoding. - * - * Example: The following index list creates the output function `(x1 - * AND x2) XOR (x3 AND x4)` with 4 inputs, 1 output, and 3 gates: - * `{0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 2, 4, 6, 8, 12, 10, 14, 14}` - */ -struct abc_index_list -{ -public: - using element_type = uint32_t; - -public: - explicit abc_index_list( uint32_t num_pis = 0 ) - { - /* add constants */ - values.push_back( 0u ); - values.push_back( 1u ); - - /* add inputs */ - if ( num_pis > 0 ) - { - add_inputs( num_pis ); - } - } - - explicit abc_index_list( std::vector const& values, uint32_t num_pis ) - : values( std::begin( values ), std::end( values ) ) - { - /* The number of primary inputs has to be passed as a parameter - because constant outputs cannot be distinguished from primary - inputs, e.g., - - 0 0 | 0 0 0 0 0 0 | 0 0 77 - - could be either read as 3 PIs and 2 POs (the first is a - constant 0) or 4 PIs and 1 POs. - */ - _num_pis = num_pis; - - /* parse the values to determine the number of outputs */ - for ( auto i = ( num_pis + 1 ) << 1; ( i + 1 ) < values.size(); i += 2 ) - { - if ( values.at( i ) == values.at( i + 1 ) ) - { - ++_num_pos; - } - } - } - - std::vector raw() const - { - return values; - } - - uint64_t size() const - { - return values.size(); - } - - uint64_t num_gates() const - { - return ( values.size() - ( ( 1 + _num_pis + _num_pos ) << 1u ) ) >> 1u; - } - - uint64_t num_pis() const - { - return _num_pis; - } - - uint64_t num_pos() const - { - return _num_pos; - } - - template - void foreach_gate( Fn&& fn ) const - { - assert( ( values.size() % 2 ) == 0 ); - for ( uint64_t i = ( 1 + _num_pis ) << 1u; i < values.size() - ( _num_pos << 1 ); i += 2 ) - { - fn( values.at( i ), values.at( i + 1 ) ); - } - } - - template - void foreach_po( Fn&& fn ) const - { - for ( uint64_t i = values.size() - 2 * _num_pos; i < values.size(); i += 2 ) - { - fn( values.at( i ) ); - } - } - - void clear() - { - values.resize( 2 ); - } - - void add_inputs( uint32_t num_pis = 1u ) - { - _num_pis += num_pis; - for ( auto i = 0u; i < num_pis; ++i ) - { - values.push_back( 0u ); - values.push_back( 0u ); - } - } - - void add_and( element_type lit0, element_type lit1 ) - { - assert( lit0 < lit1 ); - values.push_back( lit0 ); - values.push_back( lit1 ); - } - - void add_xor( element_type lit0, element_type lit1 ) - { - assert( lit0 > lit1 ); - values.push_back( lit0 ); - values.push_back( lit1 ); - } - - void add_output( element_type lit ) - { - ++_num_pos; - values.push_back( lit ); - values.push_back( lit ); - } - -private: - uint32_t _num_pis{ 0 }; - uint32_t _num_pos{ 0 }; - std::vector values; -}; - -/*! \brief Generates an abc_index_list from a network - * - * **Required network functions:** - * - `foreach_fanin` - * - `foreach_gate` - * - `get_node` - * - `is_and` - * - `is_complemented` - * - `is_xor` - * - `node_to_index` - * - `num_gates` - * - `num_pis` - * - `num_pos` - * - * \param indices An index list - * \param ntk A logic network - */ -template -void encode( abc_index_list& indices, Ntk const& ntk ) -{ - static_assert( is_network_type_v, "Ntk is not a network type" ); - static_assert( has_foreach_fanin_v, "Ntk does not implement the foreach_fanin method" ); - static_assert( has_foreach_gate_v, "Ntk does not implement the foreach_gate method" ); - static_assert( has_is_and_v, "Ntk does not implement the is_and method" ); - static_assert( has_get_node_v, "Ntk does not implement the get_node method" ); - static_assert( has_is_complemented_v, "Ntk does not implement the is_complemented method" ); - static_assert( has_is_xor_v, "Ntk does not implement the is_xor method" ); - static_assert( has_node_to_index_v, "Ntk does not implement the node_to_index method" ); - static_assert( has_num_gates_v, "Ntk does not implement the num_gates method" ); - static_assert( has_num_pis_v, "Ntk does not implement the num_pis method" ); - static_assert( has_num_pos_v, "Ntk does not implement the num_pos method" ); - - using node = typename Ntk::node; - using signal = typename Ntk::signal; - - ntk.foreach_pi( [&]( node const& n, uint64_t index ) { - if ( ntk.node_to_index( n ) != index + 1 ) - { - fmt::print( "[e] network is not in normalized index order (violated by PI {})\n", index + 1 ); - std::abort(); - } - } ); - - /* inputs */ - indices.add_inputs( ntk.num_pis() ); - - /* gates */ - ntk.foreach_gate( [&]( node const& n, uint64_t index ) { - assert( ntk.is_and( n ) || ntk.is_xor( n ) ); - if ( ntk.node_to_index( n ) != ntk.num_pis() + index + 1 ) - { - fmt::print( "[e] network is not in normalized index order (violated by node {})\n", ntk.node_to_index( n ) ); - std::abort(); - } - - std::array lits; - ntk.foreach_fanin( n, [&]( signal const& fi, uint64_t index ) { - if ( ntk.node_to_index( ntk.get_node( fi ) ) > ntk.node_to_index( n ) ) - { - fmt::print( "[e] node {} not in topological order\n", ntk.node_to_index( n ) ); - std::abort(); - } - lits[index] = 2 * ntk.node_to_index( ntk.get_node( fi ) ) + ntk.is_complemented( fi ); - } ); - - if ( ntk.is_and( n ) ) - { - if ( lits[0] > lits[1] ) - { - std::swap( lits[0], lits[1] ); - } - indices.add_and( lits[0u], lits[1u] ); - } - else if ( ntk.is_xor( n ) ) - { - if ( lits[0] < lits[1] ) - { - std::swap( lits[0], lits[1] ); - } - indices.add_xor( lits[0u], lits[1u] ); - } - } ); - - /* outputs */ - ntk.foreach_po( [&]( signal const& f ) { - indices.add_output( 2 * ntk.node_to_index( ntk.get_node( f ) ) + ntk.is_complemented( f ) ); - } ); - - assert( indices.size() == ( 1u + ntk.num_pis() + ntk.num_gates() + ntk.num_pos() ) << 1u ); -} - -/*! \brief Inserts an abc_index_list into an existing network - * - * **Required network functions:** - * - `get_constant` - * - `create_and` - * - `create_xor` - * - * \param ntk A logic network - * \param begin Begin iterator of signal inputs - * \param end End iterator of signal inputs - * \param indices An index list - * \param fn Callback function - */ -template -void insert( Ntk& ntk, BeginIter begin, EndIter end, abc_index_list const& indices, Fn&& fn ) -{ - static_assert( is_network_type_v, "Ntk is not a network type" ); - static_assert( has_create_and_v, "Ntk does not implement the create_and method" ); - static_assert( has_create_xor_v, "Ntk does not implement the create_xor method" ); - static_assert( has_get_constant_v, "Ntk does not implement the get_constant method" ); - - using node = typename Ntk::node; - using signal = typename Ntk::signal; - - if constexpr ( useSignal ) - { - static_assert( std::is_same_v::value_type>, signal>, "BeginIter value_type must be Ntk signal type" ); - static_assert( std::is_same_v::value_type>, signal>, "EndIter value_type must be Ntk signal type" ); - } - else - { - static_assert( std::is_same_v::value_type>, node>, "BeginIter value_type must be Ntk node type" ); - static_assert( std::is_same_v::value_type>, node>, "EndIter value_type must be Ntk node type" ); - } - - assert( uint64_t( std::distance( begin, end ) ) == indices.num_pis() ); - - std::vector signals; - signals.emplace_back( ntk.get_constant( false ) ); - for ( auto it = begin; it != end; ++it ) - { - if constexpr ( useSignal ) - { - signals.push_back( *it ); - } - else - { - signals.emplace_back( ntk.make_signal( *it ) ); - } - } - - indices.foreach_gate( [&]( uint32_t lit0, uint32_t lit1 ) { - assert( lit0 != lit1 ); - - uint32_t const i0 = lit0 >> 1; - uint32_t const i1 = lit1 >> 1; - signal const s0 = ( lit0 % 2 ) ? !signals.at( i0 ) : signals.at( i0 ); - signal const s1 = ( lit1 % 2 ) ? !signals.at( i1 ) : signals.at( i1 ); - - signals.push_back( lit0 < lit1 ? ntk.create_and( s0, s1 ) : ntk.create_xor( s0, s1 ) ); - } ); - - indices.foreach_po( [&]( uint32_t lit ) { - uint32_t const i = lit >> 1; - fn( ( lit % 2 ) ? !signals.at( i ) : signals.at( i ) ); - } ); -} - -/*! \brief Converts an abc_index_list to a string - * - * \param indices An index list - * \return A string representation of the index list - */ -inline std::string to_index_list_string( abc_index_list const& indices ) -{ - auto const raw = indices.raw(); - - std::string s{ "{" }; - auto it = std::begin( raw ); - while ( it != std::end( raw ) ) - { - s += std::to_string( *it ); - ++it; - if ( it != std::end( raw ) ) - { - s += ", "; - } - } - s += "}"; - return s; -} - /*! \brief Index list for mux-inverter graphs. * * Small network consisting of mux gates and inverters @@ -1368,11 +1046,6 @@ struct is_index_list : std::false_type { }; -template<> -struct is_index_list : std::true_type -{ -}; - template<> struct is_index_list> : std::true_type { diff --git a/lib/CMakeLists.txt b/lib/CMakeLists.txt index 9cb7fd5f8..b6594fa1a 100644 --- a/lib/CMakeLists.txt +++ b/lib/CMakeLists.txt @@ -78,11 +78,6 @@ if (NOT TARGET bill) endif() endif() -if (NOT TARGET abcresub) - add_library(abcresub INTERFACE) - target_include_directories(abcresub SYSTEM INTERFACE ${CMAKE_CURRENT_SOURCE_DIR}/abcresub) -endif() - if (NOT TARGET libabcesop) set(STATIC_LIBABC true) add_subdirectory(abcesop) diff --git a/lib/abcresub/abcresub/abc_global.hpp b/lib/abcresub/abcresub/abc_global.hpp deleted file mode 100644 index 6e20dab22..000000000 --- a/lib/abcresub/abcresub/abc_global.hpp +++ /dev/null @@ -1,204 +0,0 @@ -/*! - \file abc_global.hpp - \brief Extracted from ABC - https://github.com/berkeley-abc/abc - - \author Alan Mishchenko (UC Berkeley) -*/ - -#pragma once - -namespace abcresub -{ - -typedef uint64_t word; -inline int Abc_MaxInt( int a, int b ) { return a > b ? a : b; } -inline int Abc_MinInt( int a, int b ) { return a < b ? a : b; } -inline int Abc_LitIsCompl( int Lit ) { assert(Lit >= 0); return Lit & 1; } -inline int Abc_Lit2Var( int Lit ) { assert(Lit >= 0); return Lit >> 1; } -inline int Abc_Var2Lit( int Var, int c ) { assert(Var >= 0 && !(c >> 1)); return Var + Var + c; } -inline int Abc_LitNot( int Lit ) { assert(Lit >= 0); return Lit ^ 1; } -inline int Abc_LitNotCond( int Lit, int c ) { assert(Lit >= 0); return Lit ^ (int)(c > 0); } -inline int Abc_Lit2LitL( int * pMap, int Lit ) { assert(Lit >= 0); return Abc_LitNotCond( pMap[Abc_Lit2Var(Lit)], Abc_LitIsCompl(Lit) ); } - -#ifndef ABC_SWAP -#define ABC_SWAP(Type, a, b) { Type t = a; a = b; b = t; } -#endif /* ABC_SWAP */ - -#ifndef ABC_CONST -#define ABC_CONST(number) number ## ULL -#endif /* ABC_CONST */ - -#ifndef ABC_ALLOC -#define ABC_ALLOC(type, num) ((type *) malloc(sizeof(type) * (size_t)(num))) -#endif /* ABC_ALLOC */ - -#ifndef ABC_CALLOC -#define ABC_CALLOC(type, num) ((type *) calloc((size_t)(num), sizeof(type))) -#endif /* ABC_CALLOC */ - -#ifndef ABC_FREE -#define ABC_FREE(obj) ((obj) ? (free((char *) (obj)), (obj) = 0) : 0) -#endif /* ABC_FREE */ - -#ifndef ABC_REALLOC -#define ABC_REALLOC(type, obj, num) \ - ((obj) ? ((type *) realloc((char *)(obj), sizeof(type) * (size_t)(num))) : \ - ((type *) malloc(sizeof(type) * (size_t)(num)))) -#endif /* ABC_REALLOC */ - -inline void Abc_SortMerge( int * p1Beg, int * p1End, int * p2Beg, int * p2End, int * pOut ) -{ - int nEntries = (p1End - p1Beg) + (p2End - p2Beg); - int * pOutBeg = pOut; - (void)nEntries; - (void)pOutBeg; - while ( p1Beg < p1End && p2Beg < p2End ) - { - if ( *p1Beg == *p2Beg ) - *pOut++ = *p1Beg++, *pOut++ = *p2Beg++; - else if ( *p1Beg < *p2Beg ) - *pOut++ = *p1Beg++; - else // if ( *p1Beg > *p2Beg ) - *pOut++ = *p2Beg++; - } - while ( p1Beg < p1End ) - *pOut++ = *p1Beg++; - while ( p2Beg < p2End ) - *pOut++ = *p2Beg++; - assert( pOut - pOutBeg == nEntries ); -} - -inline void Abc_Sort_rec( int * pInBeg, int * pInEnd, int * pOutBeg ) -{ - int nSize = pInEnd - pInBeg; - assert( nSize > 0 ); - if ( nSize == 1 ) - return; - if ( nSize == 2 ) - { - if ( pInBeg[0] > pInBeg[1] ) - { - pInBeg[0] ^= pInBeg[1]; - pInBeg[1] ^= pInBeg[0]; - pInBeg[0] ^= pInBeg[1]; - } - } - else if ( nSize < 8 ) - { - int temp, i, j, best_i; - for ( i = 0; i < nSize-1; i++ ) - { - best_i = i; - for ( j = i+1; j < nSize; j++ ) - if ( pInBeg[j] < pInBeg[best_i] ) - best_i = j; - temp = pInBeg[i]; - pInBeg[i] = pInBeg[best_i]; - pInBeg[best_i] = temp; - } - } - else - { - Abc_Sort_rec( pInBeg, pInBeg + nSize/2, pOutBeg ); - Abc_Sort_rec( pInBeg + nSize/2, pInEnd, pOutBeg + nSize/2 ); - Abc_SortMerge( pInBeg, pInBeg + nSize/2, pInBeg + nSize/2, pInEnd, pOutBeg ); - memcpy( pInBeg, pOutBeg, sizeof(int) * nSize ); - } -} - -inline void Abc_MergeSort( int * pInput, int nSize ) -{ - int * pOutput; - if ( nSize < 2 ) - return; - pOutput = (int *) malloc( sizeof(int) * nSize ); - Abc_Sort_rec( pInput, pInput + nSize, pOutput ); - free( pOutput ); -} - -inline void Abc_MergeSortCostMerge( int * p1Beg, int * p1End, int * p2Beg, int * p2End, int * pOut ) -{ - int nEntries = (p1End - p1Beg) + (p2End - p2Beg); - int * pOutBeg = pOut; - (void)nEntries; - (void)pOutBeg; - while ( p1Beg < p1End && p2Beg < p2End ) - { - if ( p1Beg[1] == p2Beg[1] ) - *pOut++ = *p1Beg++, *pOut++ = *p1Beg++, *pOut++ = *p2Beg++, *pOut++ = *p2Beg++; - else if ( p1Beg[1] < p2Beg[1] ) - *pOut++ = *p1Beg++, *pOut++ = *p1Beg++; - else // if ( p1Beg[1] > p2Beg[1] ) - *pOut++ = *p2Beg++, *pOut++ = *p2Beg++; - } - while ( p1Beg < p1End ) - *pOut++ = *p1Beg++, *pOut++ = *p1Beg++; - while ( p2Beg < p2End ) - *pOut++ = *p2Beg++, *pOut++ = *p2Beg++; - assert( pOut - pOutBeg == nEntries ); -} - -inline void Abc_MergeSortCost_rec( int * pInBeg, int * pInEnd, int * pOutBeg ) -{ - int nSize = (pInEnd - pInBeg)/2; - assert( nSize > 0 ); - if ( nSize == 1 ) - return; - if ( nSize == 2 ) - { - if ( pInBeg[1] > pInBeg[3] ) - { - pInBeg[1] ^= pInBeg[3]; - pInBeg[3] ^= pInBeg[1]; - pInBeg[1] ^= pInBeg[3]; - pInBeg[0] ^= pInBeg[2]; - pInBeg[2] ^= pInBeg[0]; - pInBeg[0] ^= pInBeg[2]; - } - } - else if ( nSize < 8 ) - { - int temp, i, j, best_i; - for ( i = 0; i < nSize-1; i++ ) - { - best_i = i; - for ( j = i+1; j < nSize; j++ ) - if ( pInBeg[2*j+1] < pInBeg[2*best_i+1] ) - best_i = j; - temp = pInBeg[2*i]; - pInBeg[2*i] = pInBeg[2*best_i]; - pInBeg[2*best_i] = temp; - temp = pInBeg[2*i+1]; - pInBeg[2*i+1] = pInBeg[2*best_i+1]; - pInBeg[2*best_i+1] = temp; - } - } - else - { - Abc_MergeSortCost_rec( pInBeg, pInBeg + 2*(nSize/2), pOutBeg ); - Abc_MergeSortCost_rec( pInBeg + 2*(nSize/2), pInEnd, pOutBeg + 2*(nSize/2) ); - Abc_MergeSortCostMerge( pInBeg, pInBeg + 2*(nSize/2), pInBeg + 2*(nSize/2), pInEnd, pOutBeg ); - memcpy( pInBeg, pOutBeg, sizeof(int) * 2 * nSize ); - } -} - -inline int * Abc_MergeSortCost( int * pCosts, int nSize ) -{ - int i, * pResult, * pInput, * pOutput; - pResult = (int *) calloc( sizeof(int), nSize ); - if ( nSize < 2 ) - return pResult; - pInput = (int *) malloc( sizeof(int) * 2 * nSize ); - pOutput = (int *) malloc( sizeof(int) * 2 * nSize ); - for ( i = 0; i < nSize; i++ ) - pInput[2*i] = i, pInput[2*i+1] = pCosts[i]; - Abc_MergeSortCost_rec( pInput, pInput + 2*nSize, pOutput ); - for ( i = 0; i < nSize; i++ ) - pResult[i] = pInput[2*i]; - free( pOutput ); - free( pInput ); - return pResult; -} - -} /* namespace abcresub */ diff --git a/lib/abcresub/abcresub/abcresub.hpp b/lib/abcresub/abcresub/abcresub.hpp deleted file mode 100644 index 914d53633..000000000 --- a/lib/abcresub/abcresub/abcresub.hpp +++ /dev/null @@ -1,1711 +0,0 @@ -/*! - \file abcresub.hpp - \brief Extracted from ABC - https://github.com/berkeley-abc/abc - - \author Alan Mishchenko (UC Berkeley) -*/ - -#pragma once - -#include "abc_global.hpp" -#include "vec_ptr.hpp" -#include "vec_int.hpp" -#include "vec_wec.hpp" -#include "vec_wrd.hpp" -#include "tt.hpp" - -namespace abcresub -{ - -#if 0 -/**Function************************************************************* - - Synopsis [Computes MFFCs of all qualifying nodes.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Gia_ObjCheckMffc_rec( Gia_Man_t * p,Gia_Obj_t * pObj, int Limit, Vec_Int_t * vNodes ) -{ - int iFanin; - if ( Gia_ObjIsCi(pObj) ) - return 1; - assert( Gia_ObjIsAnd(pObj) ); - iFanin = Gia_ObjFaninId0p(p, pObj); - Vec_IntPush( vNodes, iFanin ); - if ( !Gia_ObjRefDecId(p, iFanin) && (Vec_IntSize(vNodes) > Limit || !Gia_ObjCheckMffc_rec(p, Gia_ObjFanin0(pObj), Limit, vNodes)) ) - return 0; - iFanin = Gia_ObjFaninId1p(p, pObj); - Vec_IntPush( vNodes, iFanin ); - if ( !Gia_ObjRefDecId(p, iFanin) && (Vec_IntSize(vNodes) > Limit || !Gia_ObjCheckMffc_rec(p, Gia_ObjFanin1(pObj), Limit, vNodes)) ) - return 0; - if ( !Gia_ObjIsMux(p, pObj) ) - return 1; - iFanin = Gia_ObjFaninId2p(p, pObj); - Vec_IntPush( vNodes, iFanin ); - if ( !Gia_ObjRefDecId(p, iFanin) && (Vec_IntSize(vNodes) > Limit || !Gia_ObjCheckMffc_rec(p, Gia_ObjFanin2(p, pObj), Limit, vNodes)) ) - return 0; - return 1; -} -static inline int Gia_ObjCheckMffc( Gia_Man_t * p, Gia_Obj_t * pRoot, int Limit, Vec_Int_t * vNodes, Vec_Int_t * vLeaves, Vec_Int_t * vInners ) -{ - int RetValue, iObj, i; - Vec_IntClear( vNodes ); - RetValue = Gia_ObjCheckMffc_rec( p, pRoot, Limit, vNodes ); - if ( RetValue ) - { - Vec_IntClear( vLeaves ); - Vec_IntClear( vInners ); - Vec_IntSort( vNodes, 0 ); - Vec_IntForEachEntry( vNodes, iObj, i ) - if ( Gia_ObjRefNumId(p, iObj) > 0 || Gia_ObjIsCi(Gia_ManObj(p, iObj)) ) - { - if ( !Vec_IntSize(vLeaves) || Vec_IntEntryLast(vLeaves) != iObj ) - Vec_IntPush( vLeaves, iObj ); - } - else - { - if ( !Vec_IntSize(vInners) || Vec_IntEntryLast(vInners) != iObj ) - Vec_IntPush( vInners, iObj ); - } - Vec_IntPush( vInners, Gia_ObjId(p, pRoot) ); - } - Vec_IntForEachEntry( vNodes, iObj, i ) - Gia_ObjRefIncId( p, iObj ); - return RetValue; -} -Vec_Wec_t * Gia_ManComputeMffcs( Gia_Man_t * p, int LimitMin, int LimitMax, int SuppMax, int RatioBest ) -{ - Gia_Obj_t * pObj; - Vec_Wec_t * vMffcs; - Vec_Int_t * vNodes, * vLeaves, * vInners, * vMffc; - int i, iPivot; - assert( p->pMuxes ); - vNodes = Vec_IntAlloc( 2 * LimitMax ); - vLeaves = Vec_IntAlloc( 2 * LimitMax ); - vInners = Vec_IntAlloc( 2 * LimitMax ); - vMffcs = Vec_WecAlloc( 1000 ); - Gia_ManCreateRefs( p ); - Gia_ManForEachAnd( p, pObj, i ) - { - if ( !Gia_ObjRefNum(p, pObj) ) - continue; - if ( !Gia_ObjCheckMffc(p, pObj, LimitMax, vNodes, vLeaves, vInners) ) - continue; - if ( Vec_IntSize(vInners) < LimitMin ) - continue; - if ( Vec_IntSize(vLeaves) > SuppMax ) - continue; - // improve cut - // collect cut - vMffc = Vec_WecPushLevel( vMffcs ); - Vec_IntGrow( vMffc, Vec_IntSize(vLeaves) + Vec_IntSize(vInners) + 20 ); - Vec_IntPush( vMffc, i ); - Vec_IntPush( vMffc, Vec_IntSize(vLeaves) ); - Vec_IntPush( vMffc, Vec_IntSize(vInners) ); - Vec_IntAppend( vMffc, vLeaves ); -// Vec_IntAppend( vMffc, vInners ); - // add last entry equal to the ratio - Vec_IntPush( vMffc, 1000 * Vec_IntSize(vInners) / Vec_IntSize(vLeaves) ); - } - Vec_IntFree( vNodes ); - Vec_IntFree( vLeaves ); - Vec_IntFree( vInners ); - // sort MFFCs by their inner/leaf ratio - Vec_WecSortByLastInt( vMffcs, 1 ); - Vec_WecForEachLevel( vMffcs, vMffc, i ) - Vec_IntPop( vMffc ); - // remove those whose ratio is not good - iPivot = RatioBest * Vec_WecSize(vMffcs) / 100; - Vec_WecForEachLevelStart( vMffcs, vMffc, i, iPivot ) - Vec_IntErase( vMffc ); - assert( iPivot <= Vec_WecSize(vMffcs) ); - Vec_WecShrink( vMffcs, iPivot ); - return vMffcs; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Gia_ManPrintDivStats( Gia_Man_t * p, Vec_Wec_t * vMffcs, Vec_Wec_t * vPivots ) -{ - int fVerbose = 0; - Vec_Int_t * vMffc; - int i, nDivs, nDivsAll = 0, nDivs0 = 0; - Vec_WecForEachLevel( vMffcs, vMffc, i ) - { - nDivs = Vec_IntSize(vMffc) - 3 - Vec_IntEntry(vMffc, 1) - Vec_IntEntry(vMffc, 2); - nDivs0 += (nDivs == 0); - nDivsAll += nDivs; - if ( !fVerbose ) - continue; - printf( "%6d : ", Vec_IntEntry(vMffc, 0) ); - printf( "Leaf =%3d ", Vec_IntEntry(vMffc, 1) ); - printf( "Mffc =%4d ", Vec_IntEntry(vMffc, 2) ); - printf( "Divs =%4d ", nDivs ); - printf( "\n" ); - } - printf( "Collected %d (%.1f %%) MFFCs and %d (%.1f %%) have no divisors (div ave for others is %.2f).\n", - Vec_WecSize(vMffcs), 100.0 * Vec_WecSize(vMffcs) / Gia_ManAndNum(p), - nDivs0, 100.0 * nDivs0 / Gia_ManAndNum(p), - 1.0*nDivsAll/Abc_MaxInt(1, Vec_WecSize(vMffcs) - nDivs0) ); - printf( "Using %.2f MB for MFFCs and %.2f MB for pivots. ", - Vec_WecMemory(vMffcs)/(1<<20), Vec_WecMemory(vPivots)/(1<<20) ); -} - -/**Function************************************************************* - - Synopsis [Compute divisors and Boolean functions for the nodes.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Gia_ManAddDivisors( Gia_Man_t * p, Vec_Wec_t * vMffcs ) -{ - Vec_Wec_t * vPivots; - Vec_Int_t * vMffc, * vPivot, * vPivot0, * vPivot1; - Vec_Int_t * vCommon, * vCommon2, * vMap; - Gia_Obj_t * pObj; - int i, k, iObj, iPivot, iMffc; -//abctime clkStart = Abc_Clock(); - // initialize pivots (mapping of nodes into MFFCs whose leaves they are) - vMap = Vec_IntStartFull( Gia_ManObjNum(p) ); - vPivots = Vec_WecStart( Gia_ManObjNum(p) ); - Vec_WecForEachLevel( vMffcs, vMffc, i ) - { - assert( Vec_IntSize(vMffc) == 3 + Vec_IntEntry(vMffc, 1) ); - iPivot = Vec_IntEntry( vMffc, 0 ); - Vec_IntWriteEntry( vMap, iPivot, i ); - // iterate through the MFFC leaves - Vec_IntForEachEntryStart( vMffc, iObj, k, 3 ) - { - vPivot = Vec_WecEntry( vPivots, iObj ); - if ( Vec_IntSize(vPivot) == 0 ) - Vec_IntGrow(vPivot, 4); - Vec_IntPush( vPivot, iPivot ); - } - } - Vec_WecForEachLevel( vPivots, vPivot, i ) - Vec_IntSort( vPivot, 0 ); - // create pivots for internal nodes while growing MFFCs - vCommon = Vec_IntAlloc( 100 ); - vCommon2 = Vec_IntAlloc( 100 ); - Gia_ManForEachAnd( p, pObj, i ) - { - // find commont pivots - // the slow down happens because some PIs have very large sets of pivots - vPivot0 = Vec_WecEntry( vPivots, Gia_ObjFaninId0(pObj, i) ); - vPivot1 = Vec_WecEntry( vPivots, Gia_ObjFaninId1(pObj, i) ); - Vec_IntTwoFindCommon( vPivot0, vPivot1, vCommon ); - if ( Gia_ObjIsMuxId(p, i) ) - { - vPivot = Vec_WecEntry( vPivots, Gia_ObjFaninId2(p, i) ); - Vec_IntTwoFindCommon( vPivot, vCommon, vCommon2 ); - ABC_SWAP( Vec_Int_t *, vCommon, vCommon2 ); - } - if ( Vec_IntSize(vCommon) == 0 ) - continue; - // add new pivots (this trick increased memory used in vPivots) - vPivot = Vec_WecEntry( vPivots, i ); - Vec_IntTwoMerge2( vPivot, vCommon, vCommon2 ); - ABC_SWAP( Vec_Int_t, *vPivot, *vCommon2 ); - // grow MFFCs - Vec_IntForEachEntry( vCommon, iObj, k ) - { - iMffc = Vec_IntEntry( vMap, iObj ); - assert( iMffc != -1 ); - vMffc = Vec_WecEntry( vMffcs, iMffc ); - Vec_IntPush( vMffc, i ); - } - } -//Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart ); - Vec_IntFree( vCommon ); - Vec_IntFree( vCommon2 ); - Vec_IntFree( vMap ); - Gia_ManPrintDivStats( p, vMffcs, vPivots ); - Vec_WecFree( vPivots ); - // returns the modified array of MFFCs -} -void Gia_ManResubTest( Gia_Man_t * p ) -{ - Vec_Wec_t * vMffcs; - Gia_Man_t * pNew = Gia_ManDupMuxes( p, 2 ); -abctime clkStart = Abc_Clock(); - vMffcs = Gia_ManComputeMffcs( pNew, 4, 100, 8, 100 ); - Gia_ManAddDivisors( pNew, vMffcs ); - Vec_WecFree( vMffcs ); -Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart ); - Gia_ManStop( pNew ); -} -#endif - - - - -/**Function************************************************************* - - Synopsis [Resubstitution data-structure.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -typedef struct Gia_ResbMan_t_ Gia_ResbMan_t; -struct Gia_ResbMan_t_ -{ - int nWords; - int nLimit; - int nDivsMax; - int iChoice; - int fUseXor; - int fDebug; - int fVerbose; - int fVeryVerbose; - Vec_Ptr_t * vDivs; - Vec_Int_t * vGates; - Vec_Int_t * vUnateLits[2]; - Vec_Int_t * vNotUnateVars[2]; - Vec_Int_t * vUnatePairs[2]; - Vec_Int_t * vBinateVars; - Vec_Int_t * vUnateLitsW[2]; - Vec_Int_t * vUnatePairsW[2]; - Vec_Wec_t * vSorter; - word * pSets[2]; - word * pDivA; - word * pDivB; - Vec_Wrd_t * vSims; -}; -inline Gia_ResbMan_t * Gia_ResbAlloc( int nWords ) -{ - Gia_ResbMan_t * p = ABC_CALLOC( Gia_ResbMan_t, 1 ); - p->nWords = nWords; - p->vUnateLits[0] = Vec_IntAlloc( 100 ); - p->vUnateLits[1] = Vec_IntAlloc( 100 ); - p->vNotUnateVars[0] = Vec_IntAlloc( 100 ); - p->vNotUnateVars[1] = Vec_IntAlloc( 100 ); - p->vUnatePairs[0] = Vec_IntAlloc( 100 ); - p->vUnatePairs[1] = Vec_IntAlloc( 100 ); - p->vUnateLitsW[0] = Vec_IntAlloc( 100 ); - p->vUnateLitsW[1] = Vec_IntAlloc( 100 ); - p->vUnatePairsW[0] = Vec_IntAlloc( 100 ); - p->vUnatePairsW[1] = Vec_IntAlloc( 100 ); - p->vSorter = Vec_WecAlloc( nWords*64 ); - p->vBinateVars = Vec_IntAlloc( 100 ); - p->vGates = Vec_IntAlloc( 100 ); - p->vDivs = Vec_PtrAlloc( 100 ); - p->pSets[0] = ABC_CALLOC( word, nWords ); - p->pSets[1] = ABC_CALLOC( word, nWords ); - p->pDivA = ABC_CALLOC( word, nWords ); - p->pDivB = ABC_CALLOC( word, nWords ); - p->vSims = Vec_WrdAlloc( 100 ); - return p; -} -inline void Gia_ResbInit( Gia_ResbMan_t * p, Vec_Ptr_t * vDivs, int nWords, int nLimit, int nDivsMax, int iChoice, int fUseXor, int fDebug, int fVerbose, int fVeryVerbose ) -{ - assert( p->nWords == nWords ); - p->nLimit = nLimit; - p->nDivsMax = nDivsMax; - p->iChoice = iChoice; - p->fUseXor = fUseXor; - p->fDebug = fDebug; - p->fVerbose = fVerbose; - p->fVeryVerbose = fVeryVerbose; - Abc_TtCopy( p->pSets[0], (word *)Vec_PtrEntry(vDivs, 0), nWords, 0 ); - Abc_TtCopy( p->pSets[1], (word *)Vec_PtrEntry(vDivs, 1), nWords, 0 ); - Vec_PtrClear( p->vDivs ); - Vec_PtrAppend( p->vDivs, vDivs ); - Vec_IntClear( p->vGates ); - Vec_IntClear( p->vUnateLits[0] ); - Vec_IntClear( p->vUnateLits[1] ); - Vec_IntClear( p->vNotUnateVars[0] ); - Vec_IntClear( p->vNotUnateVars[1] ); - Vec_IntClear( p->vUnatePairs[0] ); - Vec_IntClear( p->vUnatePairs[1] ); - Vec_IntClear( p->vUnateLitsW[0] ); - Vec_IntClear( p->vUnateLitsW[1] ); - Vec_IntClear( p->vUnatePairsW[0] ); - Vec_IntClear( p->vUnatePairsW[1] ); - Vec_IntClear( p->vBinateVars ); -} -inline void Gia_ResbFree( Gia_ResbMan_t * p ) -{ - Vec_IntFree( p->vUnateLits[0] ); - Vec_IntFree( p->vUnateLits[1] ); - Vec_IntFree( p->vNotUnateVars[0] ); - Vec_IntFree( p->vNotUnateVars[1] ); - Vec_IntFree( p->vUnatePairs[0] ); - Vec_IntFree( p->vUnatePairs[1] ); - Vec_IntFree( p->vUnateLitsW[0] ); - Vec_IntFree( p->vUnateLitsW[1] ); - Vec_IntFree( p->vUnatePairsW[0] ); - Vec_IntFree( p->vUnatePairsW[1] ); - Vec_IntFree( p->vBinateVars ); - Vec_IntFree( p->vGates ); - Vec_WrdFree( p->vSims ); - Vec_PtrFree( p->vDivs ); - Vec_WecFree( p->vSorter ); - ABC_FREE( p->pSets[0] ); - ABC_FREE( p->pSets[1] ); - ABC_FREE( p->pDivA ); - ABC_FREE( p->pDivB ); - ABC_FREE( p ); -} - -/**Function************************************************************* - - Synopsis [Print resubstitution.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -inline void Gia_ManResubPrintNode( Vec_Int_t * vRes, int nVars, int Node, int fCompl ) -{ - extern void Gia_ManResubPrintLit( Vec_Int_t * vRes, int nVars, int iLit ); - int iLit0 = Vec_IntEntry( vRes, 2*Node + 0 ); - int iLit1 = Vec_IntEntry( vRes, 2*Node + 1 ); - assert( iLit0 != iLit1 ); - if ( iLit0 > iLit1 && Abc_LitIsCompl(fCompl) ) // xor - { - printf( "~" ); - fCompl = 0; - } - printf( "(" ); - Gia_ManResubPrintLit( vRes, nVars, Abc_LitNotCond(iLit0, fCompl) ); - printf( " %c ", iLit0 > iLit1 ? '^' : (fCompl ? '|' : '&') ); - Gia_ManResubPrintLit( vRes, nVars, Abc_LitNotCond(iLit1, fCompl) ); - printf( ")" ); -} -inline void Gia_ManResubPrintLit( Vec_Int_t * vRes, int nVars, int iLit ) -{ - if ( Abc_Lit2Var(iLit) < nVars ) - { - if ( nVars < 26 ) - printf( "%s%c", Abc_LitIsCompl(iLit) ? "~":"", 'a' + Abc_Lit2Var(iLit)-2 ); - else - printf( "%si%d", Abc_LitIsCompl(iLit) ? "~":"", Abc_Lit2Var(iLit)-2 ); - } - else - Gia_ManResubPrintNode( vRes, nVars, Abc_Lit2Var(iLit) - nVars, Abc_LitIsCompl(iLit) ); -} -inline int Gia_ManResubPrint( Vec_Int_t * vRes, int nVars ) -{ - int iTopLit; - if ( Vec_IntSize(vRes) == 0 ) - return printf( "none" ); - assert( Vec_IntSize(vRes) % 2 == 1 ); - iTopLit = Vec_IntEntryLast(vRes); - if ( iTopLit == 0 ) - return printf( "const0" ); - if ( iTopLit == 1 ) - return printf( "const1" ); - Gia_ManResubPrintLit( vRes, nVars, iTopLit ); - return 0; -} - -/**Function************************************************************* - - Synopsis [Verify resubstitution.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -inline int Gia_ManResubVerify( Gia_ResbMan_t * p, word * pFunc ) -{ - int nVars = Vec_PtrSize(p->vDivs); - int iTopLit, RetValue; - word * pDivRes; - if ( Vec_IntSize(p->vGates) == 0 ) - return -1; - iTopLit = Vec_IntEntryLast(p->vGates); - assert( iTopLit >= 0 ); - if ( iTopLit == 0 ) - { - if ( pFunc ) Abc_TtClear( pFunc, p->nWords ); - return Abc_TtIsConst0( p->pSets[1], p->nWords ); - } - if ( iTopLit == 1 ) - { - if ( pFunc ) Abc_TtFill( pFunc, p->nWords ); - return Abc_TtIsConst0( p->pSets[0], p->nWords ); - } - if ( Abc_Lit2Var(iTopLit) < nVars ) - { - assert( Vec_IntSize(p->vGates) == 1 ); - pDivRes = (word *)Vec_PtrEntry( p->vDivs, Abc_Lit2Var(iTopLit) ); - } - else - { - int i, iLit0, iLit1; - assert( Vec_IntSize(p->vGates) > 1 ); - assert( Vec_IntSize(p->vGates) % 2 == 1 ); - assert( Abc_Lit2Var(iTopLit)-nVars == Vec_IntSize(p->vGates)/2-1 ); - Vec_WrdFill( p->vSims, p->nWords * Vec_IntSize(p->vGates)/2, 0 ); - Vec_IntForEachEntryDouble( p->vGates, iLit0, iLit1, i ) - { - int iVar0 = Abc_Lit2Var(iLit0); - int iVar1 = Abc_Lit2Var(iLit1); - word * pDiv0 = iVar0 < nVars ? (word *)Vec_PtrEntry(p->vDivs, iVar0) : Vec_WrdEntryP(p->vSims, p->nWords*(iVar0 - nVars)); - word * pDiv1 = iVar1 < nVars ? (word *)Vec_PtrEntry(p->vDivs, iVar1) : Vec_WrdEntryP(p->vSims, p->nWords*(iVar1 - nVars)); - word * pDiv = Vec_WrdEntryP(p->vSims, p->nWords*i/2); - if ( iVar0 < iVar1 ) - Abc_TtAndCompl( pDiv, pDiv0, Abc_LitIsCompl(iLit0), pDiv1, Abc_LitIsCompl(iLit1), p->nWords ); - else if ( iVar0 > iVar1 ) - { - assert( !Abc_LitIsCompl(iLit0) ); - assert( !Abc_LitIsCompl(iLit1) ); - Abc_TtXor( pDiv, pDiv0, pDiv1, p->nWords, 0 ); - } - else assert( 0 ); - } - pDivRes = Vec_WrdEntryP( p->vSims, p->nWords*(Vec_IntSize(p->vGates)/2-1) ); - } - if ( Abc_LitIsCompl(iTopLit) ) - RetValue = !Abc_TtIntersectOne(p->pSets[1], 0, pDivRes, 0, p->nWords) && !Abc_TtIntersectOne(p->pSets[0], 0, pDivRes, 1, p->nWords); - else - RetValue = !Abc_TtIntersectOne(p->pSets[0], 0, pDivRes, 0, p->nWords) && !Abc_TtIntersectOne(p->pSets[1], 0, pDivRes, 1, p->nWords); - if ( pFunc ) Abc_TtCopy( pFunc, pDivRes, p->nWords, Abc_LitIsCompl(iTopLit) ); - return RetValue; -} - -#if 0 -/**Function************************************************************* - - Synopsis [Construct AIG manager from gates.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Gia_ManConstructFromMap( Gia_Man_t * pNew, Vec_Int_t * vGates, int nVars, Vec_Int_t * vUsed, Vec_Int_t * vCopy, int fHash ) -{ - int i, iLit0, iLit1, iLitRes, iTopLit = Vec_IntEntryLast( vGates ); - assert( Vec_IntSize(vUsed) == nVars ); - assert( Vec_IntSize(vGates) > 1 ); - assert( Vec_IntSize(vGates) % 2 == 1 ); - assert( Abc_Lit2Var(iTopLit)-nVars == Vec_IntSize(vGates)/2-1 ); - Vec_IntClear( vCopy ); - Vec_IntForEachEntryDouble( vGates, iLit0, iLit1, i ) - { - int iVar0 = Abc_Lit2Var(iLit0); - int iVar1 = Abc_Lit2Var(iLit1); - int iRes0 = iVar0 < nVars ? Vec_IntEntry(vUsed, iVar0) : Vec_IntEntry(vCopy, iVar0 - nVars); - int iRes1 = iVar1 < nVars ? Vec_IntEntry(vUsed, iVar1) : Vec_IntEntry(vCopy, iVar1 - nVars); - if ( iVar0 < iVar1 ) - { - if ( fHash ) - iLitRes = Gia_ManHashAnd( pNew, Abc_LitNotCond(iRes0, Abc_LitIsCompl(iLit0)), Abc_LitNotCond(iRes1, Abc_LitIsCompl(iLit1)) ); - else - iLitRes = Gia_ManAppendAnd( pNew, Abc_LitNotCond(iRes0, Abc_LitIsCompl(iLit0)), Abc_LitNotCond(iRes1, Abc_LitIsCompl(iLit1)) ); - } - else if ( iVar0 > iVar1 ) - { - assert( !Abc_LitIsCompl(iLit0) ); - assert( !Abc_LitIsCompl(iLit1) ); - if ( fHash ) - iLitRes = Gia_ManHashXor( pNew, Abc_LitNotCond(iRes0, Abc_LitIsCompl(iLit0)), Abc_LitNotCond(iRes1, Abc_LitIsCompl(iLit1)) ); - else - iLitRes = Gia_ManAppendXor( pNew, Abc_LitNotCond(iRes0, Abc_LitIsCompl(iLit0)), Abc_LitNotCond(iRes1, Abc_LitIsCompl(iLit1)) ); - } - else assert( 0 ); - Vec_IntPush( vCopy, iLitRes ); - } - assert( Vec_IntSize(vCopy) == Vec_IntSize(vGates)/2 ); - iLitRes = Vec_IntEntry( vCopy, Vec_IntSize(vGates)/2-1 ); - return iLitRes; -} -Gia_Man_t * Gia_ManConstructFromGates( Vec_Wec_t * vFuncs, int nVars ) -{ - Vec_Int_t * vGates; int i, k, iLit; - Vec_Int_t * vCopy = Vec_IntAlloc( 100 ); - Vec_Int_t * vUsed = Vec_IntStartFull( nVars ); - Gia_Man_t * pNew = Gia_ManStart( 100 ); - pNew->pName = Abc_UtilStrsav( "resub" ); - Vec_WecForEachLevel( vFuncs, vGates, i ) - { - assert( Vec_IntSize(vGates) % 2 == 1 ); - Vec_IntForEachEntry( vGates, iLit, k ) - { - int iVar = Abc_Lit2Var(iLit); - if ( iVar > 0 && iVar < nVars && Vec_IntEntry(vUsed, iVar) == -1 ) - Vec_IntWriteEntry( vUsed, iVar, Gia_ManAppendCi(pNew) ); - } - } - Vec_WecForEachLevel( vFuncs, vGates, i ) - { - int iLitRes, iTopLit = Vec_IntEntryLast( vGates ); - if ( Abc_Lit2Var(iTopLit) == 0 ) - iLitRes = 0; - else if ( Abc_Lit2Var(iTopLit) < nVars ) - iLitRes = Gia_ManAppendCi(pNew); - else - iLitRes = Gia_ManConstructFromMap( pNew, vGates, nVars, vUsed, vCopy, 0 ); - Gia_ManAppendCo( pNew, Abc_LitNotCond( iLitRes, Abc_LitIsCompl(iTopLit) ) ); - } - Vec_IntFree( vCopy ); - Vec_IntFree( vUsed ); - return pNew; -} -#endif - -#if 0 -/**Function************************************************************* - - Synopsis [Construct AIG manager from gates.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Gia_ManInsertOrder_rec( Gia_Man_t * p, int iObj, Vec_Int_t * vObjs, Vec_Wec_t * vFuncs, Vec_Int_t * vNodes ) -{ - Gia_Obj_t * pObj = Gia_ManObj( p, iObj ); - if ( iObj == 0 ) - return; - if ( pObj->fPhase ) - { - int nVars = Gia_ManObjNum(p); - int k, iLit, Index = Vec_IntFind( vObjs, iObj ); - Vec_Int_t * vGates = Vec_WecEntry( vFuncs, Index ); - assert( Gia_ObjIsCo(pObj) || Gia_ObjIsAnd(pObj) ); - Vec_IntForEachEntry( vGates, iLit, k ) - if ( Abc_Lit2Var(iLit) < nVars ) - Gia_ManInsertOrder_rec( p, Abc_Lit2Var(iLit), vObjs, vFuncs, vNodes ); - } - else if ( Gia_ObjIsCo(pObj) ) - Gia_ManInsertOrder_rec( p, Gia_ObjFaninId0p(p, pObj), vObjs, vFuncs, vNodes ); - else if ( Gia_ObjIsAnd(pObj) ) - { - Gia_ManInsertOrder_rec( p, Gia_ObjFaninId0p(p, pObj), vObjs, vFuncs, vNodes ); - Gia_ManInsertOrder_rec( p, Gia_ObjFaninId1p(p, pObj), vObjs, vFuncs, vNodes ); - } - else assert( Gia_ObjIsCi(pObj) ); - if ( !Gia_ObjIsCi(pObj) ) - Vec_IntPush( vNodes, iObj ); -} -Vec_Int_t * Gia_ManInsertOrder( Gia_Man_t * p, Vec_Int_t * vObjs, Vec_Wec_t * vFuncs ) -{ - int i, Id; - Vec_Int_t * vNodes = Vec_IntAlloc( Gia_ManObjNum(p) ); - Gia_ManForEachCoId( p, Id, i ) - Gia_ManInsertOrder_rec( p, Id, vObjs, vFuncs, vNodes ); - return vNodes; -} -Gia_Man_t * Gia_ManInsertFromGates( Gia_Man_t * p, Vec_Int_t * vObjs, Vec_Wec_t * vFuncs ) -{ - Gia_Man_t * pNew, * pTemp; - Gia_Obj_t * pObj; - int i, nVars = Gia_ManObjNum(p); - Vec_Int_t * vUsed = Vec_IntStartFull( nVars ); - Vec_Int_t * vNodes, * vCopy = Vec_IntAlloc(100); - Gia_ManForEachObjVec( vObjs, p, pObj, i ) - pObj->fPhase = 1; - vNodes = Gia_ManInsertOrder( p, vObjs, vFuncs ); - pNew = Gia_ManStart( Gia_ManObjNum(p) + 1000 ); - Gia_ManHashStart( pNew ); - Gia_ManConst0(p)->Value = 0; - Gia_ManForEachCi( p, pObj, i ) - pObj->Value = Gia_ManAppendCi( pNew ); - Gia_ManForEachObjVec( vNodes, p, pObj, i ) - if ( !pObj->fPhase ) - { - if ( Gia_ObjIsCo(pObj) ) - pObj->Value = Gia_ObjFanin0Copy(pObj); - else if ( Gia_ObjIsAnd(pObj) ) - pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); - else assert( 0 ); - } - else - { - int k, iLit, Index = Vec_IntFind( vObjs, Gia_ObjId(p, pObj) ); - Vec_Int_t * vGates = Vec_WecEntry( vFuncs, Index ); - int iLitRes, iTopLit = Vec_IntEntryLast( vGates ); - if ( Abc_Lit2Var(iTopLit) == 0 ) - iLitRes = 0; - else if ( Abc_Lit2Var(iTopLit) < nVars ) - iLitRes = Gia_ManObj(p, Abc_Lit2Var(iTopLit))->Value; - else - { - Vec_IntForEachEntry( vGates, iLit, k ) - Vec_IntWriteEntry( vUsed, Abc_Lit2Var(iLit), Gia_ManObj(p, Abc_Lit2Var(iLit))->Value ); - iLitRes = Gia_ManConstructFromMap( pNew, vGates, nVars, vUsed, vCopy, 1 ); - Vec_IntForEachEntry( vGates, iLit, k ) - Vec_IntWriteEntry( vUsed, Abc_Lit2Var(iLit), -1 ); - } - pObj->Value = Abc_LitNotCond( iLitRes, Abc_LitIsCompl(iTopLit) ); - } - Gia_ManForEachCo( p, pObj, i ) - Gia_ManAppendCo( pNew, pObj->Value ); - Gia_ManForEachObjVec( vObjs, p, pObj, i ) - pObj->fPhase = 0; - Gia_ManHashStop( pNew ); - pNew = Gia_ManCleanup( pTemp = pNew ); - Gia_ManStop( pTemp ); - Vec_IntFree( vNodes ); - Vec_IntFree( vUsed ); - Vec_IntFree( vCopy ); - Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); - return pNew; -} -#endif - -/**Function************************************************************* - - Synopsis [Perform resubstitution.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline int Gia_ManFindFirstCommonLit( Vec_Int_t * vArr1, Vec_Int_t * vArr2, int fVerbose ) -{ - (void)fVerbose; - - int * pBeg1 = vArr1->pArray; - int * pBeg2 = vArr2->pArray; - int * pEnd1 = vArr1->pArray + vArr1->nSize; - int * pEnd2 = vArr2->pArray + vArr2->nSize; - int * pStart1 = vArr1->pArray; - int * pStart2 = vArr2->pArray; - int nRemoved = 0; - while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 ) - { - if ( Abc_Lit2Var(*pBeg1) == Abc_Lit2Var(*pBeg2) ) - { - if ( *pBeg1 != *pBeg2 ) - return *pBeg1; - else - pBeg1++, pBeg2++; - nRemoved++; - } - else if ( *pBeg1 < *pBeg2 ) - *pStart1++ = *pBeg1++; - else - *pStart2++ = *pBeg2++; - } - while ( pBeg1 < pEnd1 ) - *pStart1++ = *pBeg1++; - while ( pBeg2 < pEnd2 ) - *pStart2++ = *pBeg2++; - Vec_IntShrink( vArr1, pStart1 - vArr1->pArray ); - Vec_IntShrink( vArr2, pStart2 - vArr2->pArray ); - //if ( fVerbose ) printf( "Removed %d duplicated entries. Array1 = %d. Array2 = %d.\n", nRemoved, Vec_IntSize(vArr1), Vec_IntSize(vArr2) ); - return -1; -} - -inline void Gia_ManFindOneUnateInt( word * pOff, word * pOn, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits, Vec_Int_t * vNotUnateVars ) -{ - (void)pOn; - - word * pDiv; int i; - Vec_IntClear( vUnateLits ); - Vec_IntClear( vNotUnateVars ); - Vec_PtrForEachEntryStart( word *, vDivs, pDiv, i, 2 ) - if ( !Abc_TtIntersectOne( pOff, 0, pDiv, 0, nWords ) ) - Vec_IntPush( vUnateLits, Abc_Var2Lit(i, 0) ); - else if ( !Abc_TtIntersectOne( pOff, 0, pDiv, 1, nWords ) ) - Vec_IntPush( vUnateLits, Abc_Var2Lit(i, 1) ); - else - Vec_IntPush( vNotUnateVars, i ); -} -inline int Gia_ManFindOneUnate( word * pSets[2], Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits[2], Vec_Int_t * vNotUnateVars[2], int fVerbose ) -{ - int n; - if ( fVerbose ) printf( " " ); - for ( n = 0; n < 2; n++ ) - { - Gia_ManFindOneUnateInt( pSets[n], pSets[!n], vDivs, nWords, vUnateLits[n], vNotUnateVars[n] ); - if ( fVerbose ) printf( "U%d =%4d ", n, Vec_IntSize(vUnateLits[n]) ); - } - return Gia_ManFindFirstCommonLit( vUnateLits[0], vUnateLits[1], fVerbose ); -} - -static inline int Gia_ManDivCover( word * pOff, word * pOn, word * pDivA, int ComplA, word * pDivB, int ComplB, int nWords ) -{ - (void)pOff; - - //assert( !Abc_TtIntersectOne(pOff, 0, pDivA, ComplA, nWords) ); - //assert( !Abc_TtIntersectOne(pOff, 0, pDivB, ComplB, nWords) ); - return !Abc_TtIntersectTwo( pOn, 0, pDivA, !ComplA, pDivB, !ComplB, nWords ); -} -inline int Gia_ManFindTwoUnateInt( word * pOff, word * pOn, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits, Vec_Int_t * vUnateLitsW, int * pnPairs ) -{ - int i, k, iDiv0_, iDiv1_, Cover0, Cover1; - int nTotal = Abc_TtCountOnesVec( pOn, nWords ); - (*pnPairs) = 0; - Vec_IntForEachEntryTwo( vUnateLits, vUnateLitsW, iDiv0_, Cover0, i ) - { - if ( 2*Cover0 < nTotal ) - break; - Vec_IntForEachEntryTwoStart( vUnateLits, vUnateLitsW, iDiv1_, Cover1, k, i+1 ) - { - int iDiv0 = Abc_MinInt( iDiv0_, iDiv1_ ); - int iDiv1 = Abc_MaxInt( iDiv0_, iDiv1_ ); - word * pDiv0 = (word *)Vec_PtrEntry(vDivs, Abc_Lit2Var(iDiv0)); - word * pDiv1 = (word *)Vec_PtrEntry(vDivs, Abc_Lit2Var(iDiv1)); - if ( Cover0 + Cover1 < nTotal ) - break; - (*pnPairs)++; - if ( Gia_ManDivCover(pOff, pOn, pDiv1, Abc_LitIsCompl(iDiv1), pDiv0, Abc_LitIsCompl(iDiv0), nWords) ) - return Abc_Var2Lit((Abc_LitNot(iDiv1) << 15) | Abc_LitNot(iDiv0), 1); - } - } - return -1; -} -inline int Gia_ManFindTwoUnate( word * pSets[2], Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits[2], Vec_Int_t * vUnateLitsW[2], int fVerbose ) -{ - int n, iLit, nPairs; - if ( fVerbose ) printf( " " ); - for ( n = 0; n < 2; n++ ) - { - //int nPairsAll = Vec_IntSize(vUnateLits[n])*(Vec_IntSize(vUnateLits[n])-1)/2; - iLit = Gia_ManFindTwoUnateInt( pSets[n], pSets[!n], vDivs, nWords, vUnateLits[n], vUnateLitsW[n], &nPairs ); - if ( fVerbose ) printf( "UU%d =%5d ", n, nPairs ); - if ( iLit >= 0 ) - return Abc_LitNotCond(iLit, n); - } - return -1; -} - -inline void Gia_ManFindXorInt( word * pOff, word * pOn, Vec_Int_t * vBinate, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnatePairs ) -{ - (void)pOn; - - int i, k, iDiv0_, iDiv1_; - int Limit2 = Vec_IntSize(vBinate);//Abc_MinInt( Vec_IntSize(vBinate), 100 ); - Vec_IntForEachEntryStop( vBinate, iDiv1_, i, Limit2 ) - Vec_IntForEachEntryStop( vBinate, iDiv0_, k, i ) - { - int iDiv0 = Abc_MinInt( iDiv0_, iDiv1_ ); - int iDiv1 = Abc_MaxInt( iDiv0_, iDiv1_ ); - word * pDiv0 = (word *)Vec_PtrEntry(vDivs, iDiv0); - word * pDiv1 = (word *)Vec_PtrEntry(vDivs, iDiv1); - if ( !Abc_TtIntersectXor( pOff, 0, pDiv0, pDiv1, 0, nWords ) ) - Vec_IntPush( vUnatePairs, Abc_Var2Lit((Abc_Var2Lit(iDiv0, 0) << 15) | Abc_Var2Lit(iDiv1, 0), 0) ); - else if ( !Abc_TtIntersectXor( pOff, 0, pDiv0, pDiv1, 1, nWords ) ) - Vec_IntPush( vUnatePairs, Abc_Var2Lit((Abc_Var2Lit(iDiv0, 0) << 15) | Abc_Var2Lit(iDiv1, 0), 1) ); - } -} -inline int Gia_ManFindXor( word * pSets[2], Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vBinateVars, Vec_Int_t * vUnatePairs[2], int fVerbose ) -{ - int n; - if ( fVerbose ) printf( " " ); - for ( n = 0; n < 2; n++ ) - { - Vec_IntClear( vUnatePairs[n] ); - Gia_ManFindXorInt( pSets[n], pSets[!n], vBinateVars, vDivs, nWords, vUnatePairs[n] ); - if ( fVerbose ) printf( "UX%d =%5d ", n, Vec_IntSize(vUnatePairs[n]) ); - } - return Gia_ManFindFirstCommonLit( vUnatePairs[0], vUnatePairs[1], fVerbose ); -} - -inline void Gia_ManFindUnatePairsInt( word * pOff, word * pOn, Vec_Int_t * vBinate, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnatePairs ) -{ - int n, i, k, iDiv0_, iDiv1_; - int Limit2 = Vec_IntSize(vBinate);//Abc_MinInt( Vec_IntSize(vBinate), 100 ); - Vec_IntForEachEntryStop( vBinate, iDiv1_, i, Limit2 ) - Vec_IntForEachEntryStop( vBinate, iDiv0_, k, i ) - { - int iDiv0 = Abc_MinInt( iDiv0_, iDiv1_ ); - int iDiv1 = Abc_MaxInt( iDiv0_, iDiv1_ ); - word * pDiv0 = (word *)Vec_PtrEntry(vDivs, iDiv0); - word * pDiv1 = (word *)Vec_PtrEntry(vDivs, iDiv1); - for ( n = 0; n < 4; n++ ) - { - int iLit0 = Abc_Var2Lit( iDiv0, n&1 ); - int iLit1 = Abc_Var2Lit( iDiv1, n>>1 ); - //if ( !Abc_TtIntersectTwo( pOff, 0, pDiv1, n>>1, pDiv0, n&1, nWords ) ) - if ( !Abc_TtIntersectTwo( pOff, 0, pDiv1, n>>1, pDiv0, n&1, nWords ) && Abc_TtIntersectTwo( pOn, 0, pDiv1, n>>1, pDiv0, n&1, nWords ) ) - Vec_IntPush( vUnatePairs, Abc_Var2Lit((iLit1 << 15) | iLit0, 0) ); - } - } -} -inline void Gia_ManFindUnatePairs( word * pSets[2], Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vBinateVars, Vec_Int_t * vUnatePairs[2], int fVerbose ) -{ - int n, RetValue; - if ( fVerbose ) printf( " " ); - for ( n = 0; n < 2; n++ ) - { - int nBefore = Vec_IntSize(vUnatePairs[n]); - Gia_ManFindUnatePairsInt( pSets[n], pSets[!n], vBinateVars, vDivs, nWords, vUnatePairs[n] ); - if ( fVerbose ) printf( "UP%d =%5d ", n, Vec_IntSize(vUnatePairs[n])-nBefore ); - } - RetValue = Gia_ManFindFirstCommonLit( vUnatePairs[0], vUnatePairs[1], fVerbose ); - assert( RetValue == -1 ); (void)RetValue; -} - -inline void Gia_ManDeriveDivPair( int iDiv, Vec_Ptr_t * vDivs, int nWords, word * pRes ) -{ - int fComp = Abc_LitIsCompl(iDiv); - int iDiv0 = Abc_Lit2Var(iDiv) & 0x7FFF; - int iDiv1 = Abc_Lit2Var(iDiv) >> 15; - word * pDiv0 = (word *)Vec_PtrEntry(vDivs, Abc_Lit2Var(iDiv0)); - word * pDiv1 = (word *)Vec_PtrEntry(vDivs, Abc_Lit2Var(iDiv1)); - if ( iDiv0 < iDiv1 ) - { - assert( !fComp ); (void)fComp; - Abc_TtAndCompl( pRes, pDiv0, Abc_LitIsCompl(iDiv0), pDiv1, Abc_LitIsCompl(iDiv1), nWords ); - } - else - { - assert( !Abc_LitIsCompl(iDiv0) ); - assert( !Abc_LitIsCompl(iDiv1) ); - Abc_TtXor( pRes, pDiv0, pDiv1, nWords, 0 ); - } -} -inline int Gia_ManFindDivGateInt( word * pOff, word * pOn, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits, Vec_Int_t * vUnatePairs, Vec_Int_t * vUnateLitsW, Vec_Int_t * vUnatePairsW, word * pDivTemp ) -{ - int i, k, iDiv0, iDiv1, Cover0, Cover1; - int nTotal = Abc_TtCountOnesVec( pOn, nWords ); - Vec_IntForEachEntryTwo( vUnateLits, vUnateLitsW, iDiv0, Cover0, i ) - { - word * pDiv0 = (word *)Vec_PtrEntry(vDivs, Abc_Lit2Var(iDiv0)); - if ( 2*Cover0 < nTotal ) - break; - Vec_IntForEachEntryTwo( vUnatePairs, vUnatePairsW, iDiv1, Cover1, k ) - { - int fComp1 = Abc_LitIsCompl(iDiv1); - if ( Cover0 + Cover1 < nTotal ) - break; - Gia_ManDeriveDivPair( iDiv1, vDivs, nWords, pDivTemp ); - if ( Gia_ManDivCover(pOff, pOn, pDiv0, Abc_LitIsCompl(iDiv0), pDivTemp, fComp1, nWords) ) - return Abc_Var2Lit((Abc_Var2Lit(k, 1) << 15) | Abc_LitNot(iDiv0), 1); - } - } - return -1; -} -inline int Gia_ManFindDivGate( word * pSets[2], Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits[2], Vec_Int_t * vUnatePairs[2], Vec_Int_t * vUnateLitsW[2], Vec_Int_t * vUnatePairsW[2], word * pDivTemp ) -{ - int n, iLit; - for ( n = 0; n < 2; n++ ) - { - iLit = Gia_ManFindDivGateInt( pSets[n], pSets[!n], vDivs, nWords, vUnateLits[n], vUnatePairs[n], vUnateLitsW[n], vUnatePairsW[n], pDivTemp ); - if ( iLit >= 0 ) - return Abc_LitNotCond( iLit, n ); - } - return -1; -} - -inline int Gia_ManFindGateGateInt( word * pOff, word * pOn, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnatePairs, Vec_Int_t * vUnatePairsW, word * pDivTempA, word * pDivTempB ) -{ - int i, k, iDiv0, iDiv1, Cover0, Cover1; - int nTotal = Abc_TtCountOnesVec( pOn, nWords ); - Vec_IntForEachEntryTwo( vUnatePairs, vUnatePairsW, iDiv0, Cover0, k ) - { - int fCompA = Abc_LitIsCompl(iDiv0); - if ( 2*Cover0 < nTotal ) - break; - Gia_ManDeriveDivPair( iDiv0, vDivs, nWords, pDivTempA ); - Vec_IntForEachEntryTwoStart( vUnatePairs, vUnatePairsW, iDiv1, Cover1, i, k+1 ) - { - int fCompB = Abc_LitIsCompl(iDiv1); - if ( Cover0 + Cover1 < nTotal ) - break; - Gia_ManDeriveDivPair( iDiv1, vDivs, nWords, pDivTempB ); - if ( Gia_ManDivCover(pOff, pOn, pDivTempA, fCompA, pDivTempB, fCompB, nWords) ) - return Abc_Var2Lit((Abc_Var2Lit(i, 1) << 15) | Abc_Var2Lit(k, 1), 1); - } - } - return -1; -} -inline int Gia_ManFindGateGate( word * pSets[2], Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnatePairs[2], Vec_Int_t * vUnatePairsW[2], word * pDivTempA, word * pDivTempB ) -{ - int n, iLit; - for ( n = 0; n < 2; n++ ) - { - iLit = Gia_ManFindGateGateInt( pSets[n], pSets[!n], vDivs, nWords, vUnatePairs[n], vUnatePairsW[n], pDivTempA, pDivTempB ); - if ( iLit >= 0 ) - return Abc_LitNotCond( iLit, n ); - } - return -1; -} - -inline void Gia_ManSortUnatesInt( word * pOff, word * pOn, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits, Vec_Int_t * vUnateLitsW, Vec_Wec_t * vSorter ) -{ - (void)pOff; - - int i, k, iLit; - Vec_Int_t * vLevel; - Vec_WecInit( vSorter, nWords*64 ); - Vec_IntForEachEntry( vUnateLits, iLit, i ) - { - word * pDiv = (word *)Vec_PtrEntry(vDivs, Abc_Lit2Var(iLit)); - //assert( !Abc_TtIntersectOne( pOff, 0, pDiv, Abc_LitIsCompl(iLit), nWords ) ); - Vec_WecPush( vSorter, Abc_TtCountOnesVecMask(pDiv, pOn, nWords, Abc_LitIsCompl(iLit)), iLit ); - } - Vec_IntClear( vUnateLits ); - Vec_IntClear( vUnateLitsW ); - Vec_WecForEachLevelReverse( vSorter, vLevel, k ) - Vec_IntForEachEntry( vLevel, iLit, i ) - { - Vec_IntPush( vUnateLits, iLit ); - Vec_IntPush( vUnateLitsW, k ); - } - //Vec_IntPrint( Vec_WecEntry(vSorter, 0) ); - Vec_WecClear( vSorter ); -} -inline void Gia_ManSortUnates( word * pSets[2], Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits[2], Vec_Int_t * vUnateLitsW[2], Vec_Wec_t * vSorter ) -{ - int n; - for ( n = 0; n < 2; n++ ) - Gia_ManSortUnatesInt( pSets[n], pSets[!n], vDivs, nWords, vUnateLits[n], vUnateLitsW[n], vSorter ); -} - -inline void Gia_ManSortPairsInt( word * pOff, word * pOn, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnatePairs, Vec_Int_t * vUnatePairsW, Vec_Wec_t * vSorter ) -{ - (void)pOff; - - int i, k, iPair; - Vec_Int_t * vLevel; - Vec_WecInit( vSorter, nWords*64 ); - Vec_IntForEachEntry( vUnatePairs, iPair, i ) - { - int fComp = Abc_LitIsCompl(iPair); - int iLit0 = Abc_Lit2Var(iPair) & 0x7FFF; - int iLit1 = Abc_Lit2Var(iPair) >> 15; - word * pDiv0 = (word *)Vec_PtrEntry( vDivs, Abc_Lit2Var(iLit0) ); - word * pDiv1 = (word *)Vec_PtrEntry( vDivs, Abc_Lit2Var(iLit1) ); - if ( iLit0 < iLit1 ) - { - assert( !fComp ); - //assert( !Abc_TtIntersectTwo( pOff, 0, pDiv0, Abc_LitIsCompl(iLit0), pDiv1, Abc_LitIsCompl(iLit1), nWords ) ); - Vec_WecPush( vSorter, Abc_TtCountOnesVecMask2(pDiv0, pDiv1, Abc_LitIsCompl(iLit0), Abc_LitIsCompl(iLit1), pOn, nWords), iPair ); - } - else - { - assert( !Abc_LitIsCompl(iLit0) ); - assert( !Abc_LitIsCompl(iLit1) ); - //assert( !Abc_TtIntersectXor( pOff, 0, pDiv0, pDiv1, fComp, nWords ) ); - Vec_WecPush( vSorter, Abc_TtCountOnesVecXorMask(pDiv0, pDiv1, fComp, pOn, nWords), iPair ); - } - } - Vec_IntClear( vUnatePairs ); - Vec_IntClear( vUnatePairsW ); - Vec_WecForEachLevelReverse( vSorter, vLevel, k ) - Vec_IntForEachEntry( vLevel, iPair, i ) - { - Vec_IntPush( vUnatePairs, iPair ); - Vec_IntPush( vUnatePairsW, k ); - } - //Vec_IntPrint( Vec_WecEntry(vSorter, 0) ); - Vec_WecClear( vSorter ); - -} -inline void Gia_ManSortPairs( word * pSets[2], Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits[2], Vec_Int_t * vUnateLitsW[2], Vec_Wec_t * vSorter ) -{ - int n; - for ( n = 0; n < 2; n++ ) - Gia_ManSortPairsInt( pSets[n], pSets[!n], vDivs, nWords, vUnateLits[n], vUnateLitsW[n], vSorter ); -} - -inline void Gia_ManSortBinate( word * pSets[2], Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vBinateVars, Vec_Wec_t * vSorter ) -{ - Vec_Int_t * vLevel; - int nMints[2] = { Abc_TtCountOnesVec(pSets[0], nWords), Abc_TtCountOnesVec(pSets[1], nWords) }; - word * pBig = nMints[0] > nMints[1] ? pSets[0] : pSets[1]; - word * pSmo = nMints[0] > nMints[1] ? pSets[1] : pSets[0]; - int Big = Abc_MaxInt( nMints[0], nMints[1] ); - int Smo = Abc_MinInt( nMints[0], nMints[1] ); - int i, k, iDiv, Gain; - - Vec_WecInit( vSorter, nWords*64 ); - Vec_IntForEachEntry( vBinateVars, iDiv, i ) - { - word * pDiv = (word *)Vec_PtrEntry( vDivs, iDiv ); - int nInter[2] = { Abc_TtCountOnesVecMask(pBig, pDiv, nWords, 0), Abc_TtCountOnesVecMask(pSmo, pDiv, nWords, 0) }; - if ( nInter[0] < Big/2 ) // complement the divisor - { - nInter[0] = Big - nInter[0]; - nInter[1] = Smo - nInter[1]; - } - assert( nInter[0] >= Big/2 ); - Gain = Abc_MaxInt( 0, nInter[0] - Big/2 + Smo/2 - nInter[1] ); - Vec_WecPush( vSorter, Gain, iDiv ); - } - - Vec_IntClear( vBinateVars ); - Vec_WecForEachLevelReverse( vSorter, vLevel, k ) - Vec_IntForEachEntry( vLevel, iDiv, i ) - Vec_IntPush( vBinateVars, iDiv ); - Vec_WecClear( vSorter ); - - if ( Vec_IntSize(vBinateVars) > 2000 ) - Vec_IntShrink( vBinateVars, 2000 ); -} - -/**Function************************************************************* - - Synopsis [Perform resubstitution.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -inline int Gia_ManResubPerform_rec( Gia_ResbMan_t * p, int nLimit ) -{ - int TopOneW[2] = {0}, TopTwoW[2] = {0}, Max1, Max2, iResLit, nVars = Vec_PtrSize(p->vDivs); - if ( p->fVerbose ) - { - int nMints[2] = { Abc_TtCountOnesVec(p->pSets[0], p->nWords), Abc_TtCountOnesVec(p->pSets[1], p->nWords) }; - printf( " " ); - printf( "ISF: " ); - printf( "0=%5d (%5.2f %%) ", nMints[0], 100.0*nMints[0]/(64*p->nWords) ); - printf( "1=%5d (%5.2f %%) ", nMints[1], 100.0*nMints[1]/(64*p->nWords) ); - } - if ( Abc_TtIsConst0( p->pSets[1], p->nWords ) ) - return 0; - if ( Abc_TtIsConst0( p->pSets[0], p->nWords ) ) - return 1; - iResLit = Gia_ManFindOneUnate( p->pSets, p->vDivs, p->nWords, p->vUnateLits, p->vNotUnateVars, p->fVerbose ); - if ( iResLit >= 0 ) // buffer - return iResLit; - if ( nLimit == 0 ) - return -1; - Gia_ManSortUnates( p->pSets, p->vDivs, p->nWords, p->vUnateLits, p->vUnateLitsW, p->vSorter ); - iResLit = Gia_ManFindTwoUnate( p->pSets, p->vDivs, p->nWords, p->vUnateLits, p->vUnateLitsW, p->fVerbose ); - if ( iResLit >= 0 ) // and - { - int iNode = nVars + Vec_IntSize(p->vGates)/2; - int fComp = Abc_LitIsCompl(iResLit); - int iDiv0 = Abc_Lit2Var(iResLit) & 0x7FFF; - int iDiv1 = Abc_Lit2Var(iResLit) >> 15; - assert( iDiv0 < iDiv1 ); - Vec_IntPushTwo( p->vGates, iDiv0, iDiv1 ); - return Abc_Var2Lit( iNode, fComp ); - } - Vec_IntTwoFindCommon( p->vNotUnateVars[0], p->vNotUnateVars[1], p->vBinateVars ); - if ( Vec_IntSize(p->vBinateVars) > p->nDivsMax ) - Vec_IntShrink( p->vBinateVars, p->nDivsMax ); - if ( p->fVerbose ) printf( " B = %3d", Vec_IntSize(p->vBinateVars) ); - //Gia_ManSortBinate( p->pSets, p->vDivs, p->nWords, p->vBinateVars, p->vSorter ); - if ( p->fUseXor ) - { - iResLit = Gia_ManFindXor( p->pSets, p->vDivs, p->nWords, p->vBinateVars, p->vUnatePairs, p->fVerbose ); - if ( iResLit >= 0 ) // xor - { - int iNode = nVars + Vec_IntSize(p->vGates)/2; - int fComp = Abc_LitIsCompl(iResLit); - int iDiv0 = Abc_Lit2Var(iResLit) & 0x7FFF; - int iDiv1 = Abc_Lit2Var(iResLit) >> 15; - assert( !Abc_LitIsCompl(iDiv0) ); - assert( !Abc_LitIsCompl(iDiv1) ); - assert( iDiv0 > iDiv1 ); - Vec_IntPushTwo( p->vGates, iDiv0, iDiv1 ); - return Abc_Var2Lit( iNode, fComp ); - } - } - if ( nLimit == 1 ) - return -1; - Gia_ManFindUnatePairs( p->pSets, p->vDivs, p->nWords, p->vBinateVars, p->vUnatePairs, p->fVerbose ); - Gia_ManSortPairs( p->pSets, p->vDivs, p->nWords, p->vUnatePairs, p->vUnatePairsW, p->vSorter ); - iResLit = Gia_ManFindDivGate( p->pSets, p->vDivs, p->nWords, p->vUnateLits, p->vUnatePairs, p->vUnateLitsW, p->vUnatePairsW, p->pDivA ); - if ( iResLit >= 0 ) // and(div,pair) - { - int iNode = nVars + Vec_IntSize(p->vGates)/2; - - int fComp = Abc_LitIsCompl(iResLit); - int iDiv0 = Abc_Lit2Var(iResLit) & 0x7FFF; // div - int iDiv1 = Abc_Lit2Var(iResLit) >> 15; // pair - - int Div1 = Vec_IntEntry( p->vUnatePairs[!fComp], Abc_Lit2Var(iDiv1) ); - int fComp1 = Abc_LitIsCompl(Div1) ^ Abc_LitIsCompl(iDiv1); - int iDiv10 = Abc_Lit2Var(Div1) & 0x7FFF; - int iDiv11 = Abc_Lit2Var(Div1) >> 15; - - Vec_IntPushTwo( p->vGates, iDiv10, iDiv11 ); - Vec_IntPushTwo( p->vGates, iDiv0, Abc_Var2Lit(iNode, fComp1) ); - return Abc_Var2Lit( iNode+1, fComp ); - } - if ( nLimit >= 3 ) - { - iResLit = Gia_ManFindGateGate( p->pSets, p->vDivs, p->nWords, p->vUnatePairs, p->vUnatePairsW, p->pDivA, p->pDivB ); - if ( iResLit >= 0 ) // and(pair,pair) - { - int iNode = nVars + Vec_IntSize(p->vGates)/2; - - int fComp = Abc_LitIsCompl(iResLit); - int iDiv0 = Abc_Lit2Var(iResLit) & 0x7FFF; // pair - int iDiv1 = Abc_Lit2Var(iResLit) >> 15; // pair - - int Div0 = Vec_IntEntry( p->vUnatePairs[!fComp], Abc_Lit2Var(iDiv0) ); - int fComp0 = Abc_LitIsCompl(Div0) ^ Abc_LitIsCompl(iDiv0); - int iDiv00 = Abc_Lit2Var(Div0) & 0x7FFF; - int iDiv01 = Abc_Lit2Var(Div0) >> 15; - - int Div1 = Vec_IntEntry( p->vUnatePairs[!fComp], Abc_Lit2Var(iDiv1) ); - int fComp1 = Abc_LitIsCompl(Div1) ^ Abc_LitIsCompl(iDiv1); - int iDiv10 = Abc_Lit2Var(Div1) & 0x7FFF; - int iDiv11 = Abc_Lit2Var(Div1) >> 15; - - Vec_IntPushTwo( p->vGates, iDiv00, iDiv01 ); - Vec_IntPushTwo( p->vGates, iDiv10, iDiv11 ); - Vec_IntPushTwo( p->vGates, Abc_Var2Lit(iNode, fComp0), Abc_Var2Lit(iNode+1, fComp1) ); - return Abc_Var2Lit( iNode+2, fComp ); - } - } - if ( Vec_IntSize(p->vUnateLits[0]) + Vec_IntSize(p->vUnateLits[1]) + Vec_IntSize(p->vUnatePairs[0]) + Vec_IntSize(p->vUnatePairs[1]) == 0 ) - return -1; - - TopOneW[0] = Vec_IntSize(p->vUnateLitsW[0]) ? Vec_IntEntry(p->vUnateLitsW[0], 0) : 0; - TopOneW[1] = Vec_IntSize(p->vUnateLitsW[1]) ? Vec_IntEntry(p->vUnateLitsW[1], 0) : 0; - - TopTwoW[0] = Vec_IntSize(p->vUnatePairsW[0]) ? Vec_IntEntry(p->vUnatePairsW[0], 0) : 0; - TopTwoW[1] = Vec_IntSize(p->vUnatePairsW[1]) ? Vec_IntEntry(p->vUnatePairsW[1], 0) : 0; - - Max1 = Abc_MaxInt(TopOneW[0], TopOneW[1]); - Max2 = Abc_MaxInt(TopTwoW[0], TopTwoW[1]); - if ( Abc_MaxInt(Max1, Max2) == 0 ) - return -1; - - if ( Max1 > Max2/2 ) - { - if ( nLimit >= 2 && (Max1 == TopOneW[0] || Max1 == TopOneW[1]) ) - { - int fUseOr = Max1 == TopOneW[0]; - int iDiv = Vec_IntEntry( p->vUnateLits[!fUseOr], 0 ); - int fComp = Abc_LitIsCompl(iDiv); - word * pDiv = (word *)Vec_PtrEntry( p->vDivs, Abc_Lit2Var(iDiv) ); - Abc_TtAndSharp( p->pSets[fUseOr], p->pSets[fUseOr], pDiv, p->nWords, !fComp ); - if ( p->fVerbose ) - printf( "\n" ); - iResLit = Gia_ManResubPerform_rec( p, nLimit-1 ); - if ( iResLit >= 0 ) - { - int iNode = nVars + Vec_IntSize(p->vGates)/2; - Vec_IntPushTwo( p->vGates, Abc_LitNot(iDiv), Abc_LitNotCond(iResLit, fUseOr) ); - return Abc_Var2Lit( iNode, fUseOr ); - } - } - if ( Max2 == 0 ) - return -1; -/* - if ( Max2 == TopTwoW[0] || Max2 == TopTwoW[1] ) - { - int fUseOr = Max2 == TopTwoW[0]; - int iDiv = Vec_IntEntry( p->vUnatePairs[!fUseOr], 0 ); - int fComp = Abc_LitIsCompl(iDiv); - Gia_ManDeriveDivPair( iDiv, p->vDivs, p->nWords, p->pDivA ); - Abc_TtAndSharp( p->pSets[fUseOr], p->pSets[fUseOr], p->pDivA, p->nWords, !fComp ); - if ( p->fVerbose ) - printf( "\n " ); - iResLit = Gia_ManResubPerform_rec( p, nLimit-2 ); - if ( iResLit >= 0 ) - { - int iNode = nVars + Vec_IntSize(p->vGates)/2; - int iDiv0 = Abc_Lit2Var(iDiv) & 0x7FFF; - int iDiv1 = Abc_Lit2Var(iDiv) >> 15; - Vec_IntPushTwo( p->vGates, iDiv0, iDiv1 ); - Vec_IntPushTwo( p->vGates, Abc_LitNotCond(iResLit, fUseOr), Abc_Var2Lit(iNode, !fComp) ); - return Abc_Var2Lit( iNode+1, fUseOr ); - } - } -*/ - } - else - { - if ( nLimit >= 3 && (Max2 == TopTwoW[0] || Max2 == TopTwoW[1]) ) - { - int fUseOr = Max2 == TopTwoW[0]; - int iDiv = Vec_IntEntry( p->vUnatePairs[!fUseOr], 0 ); - int fComp = Abc_LitIsCompl(iDiv); - Gia_ManDeriveDivPair( iDiv, p->vDivs, p->nWords, p->pDivA ); - Abc_TtAndSharp( p->pSets[fUseOr], p->pSets[fUseOr], p->pDivA, p->nWords, !fComp ); - if ( p->fVerbose ) - printf( "\n" ); - iResLit = Gia_ManResubPerform_rec( p, nLimit-2 ); - if ( iResLit >= 0 ) - { - int iNode = nVars + Vec_IntSize(p->vGates)/2; - int iDiv0 = Abc_Lit2Var(iDiv) & 0x7FFF; - int iDiv1 = Abc_Lit2Var(iDiv) >> 15; - Vec_IntPushTwo( p->vGates, iDiv0, iDiv1 ); - Vec_IntPushTwo( p->vGates, Abc_LitNotCond(iResLit, fUseOr), Abc_Var2Lit(iNode, !fComp) ); - return Abc_Var2Lit( iNode+1, fUseOr ); - } - } - if ( Max1 == 0 ) - return -1; -/* - if ( Max1 == TopOneW[0] || Max1 == TopOneW[1] ) - { - int fUseOr = Max1 == TopOneW[0]; - int iDiv = Vec_IntEntry( p->vUnateLits[!fUseOr], 0 ); - int fComp = Abc_LitIsCompl(iDiv); - word * pDiv = (word *)Vec_PtrEntry( p->vDivs, Abc_Lit2Var(iDiv) ); - Abc_TtAndSharp( p->pSets[fUseOr], p->pSets[fUseOr], pDiv, p->nWords, !fComp ); - if ( p->fVerbose ) - printf( "\n " ); - iResLit = Gia_ManResubPerform_rec( p, nLimit-1 ); - if ( iResLit >= 0 ) - { - int iNode = nVars + Vec_IntSize(p->vGates)/2; - Vec_IntPushTwo( p->vGates, Abc_LitNot(iDiv), Abc_LitNotCond(iResLit, fUseOr) ); - return Abc_Var2Lit( iNode, fUseOr ); - } - } -*/ - } - return -1; -} -inline void Gia_ManResubPerform( Gia_ResbMan_t * p, Vec_Ptr_t * vDivs, int nWords, int nLimit, int nDivsMax, int iChoice, int fUseXor, int fDebug, int fVerbose ) -{ - int Res; - Gia_ResbInit( p, vDivs, nWords, nLimit, nDivsMax, iChoice, fUseXor, fDebug, fVerbose, fVerbose ); - Res = Gia_ManResubPerform_rec( p, nLimit ); - if ( Res >= 0 ) Vec_IntPush( p->vGates, Res ); - if ( fVerbose ) - printf( "\n" ); -} -inline Vec_Int_t * Gia_ManResubOne( Vec_Ptr_t * vDivs, int nWords, int nLimit, int nDivsMax, int iChoice, int fUseXor, int fDebug, int fVerbose, word * pFunc ) -{ - Vec_Int_t * vRes; - Gia_ResbMan_t * p = Gia_ResbAlloc( nWords ); - Gia_ManResubPerform( p, vDivs, nWords, nLimit, nDivsMax, iChoice, fUseXor, fDebug, fVerbose ); - if ( fVerbose ) - Gia_ManResubPrint( p->vGates, Vec_PtrSize(vDivs) ); - if ( fVerbose ) - printf( "\n" ); - if ( !Gia_ManResubVerify(p, pFunc) ) - { - Gia_ManResubPrint( p->vGates, Vec_PtrSize(vDivs) ); - printf( "Verification FAILED.\n" ); - } - else if ( fDebug && fVerbose ) - printf( "Verification succeeded." ); - if ( fVerbose ) - printf( "\n" ); - vRes = Vec_IntDup( p->vGates ); - Gia_ResbFree( p ); - return vRes; -} - -/**Function************************************************************* - - Synopsis [Top level.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static Gia_ResbMan_t * s_pResbMan = NULL; - -inline void Abc_ResubPrepareManager( int nWords ) -{ - if ( s_pResbMan != NULL ) - Gia_ResbFree( s_pResbMan ); - s_pResbMan = NULL; - if ( nWords > 0 ) - s_pResbMan = Gia_ResbAlloc( nWords ); -} - -inline int Abc_ResubComputeFunction( void ** ppDivs, int nDivs, int nWords, int nLimit, int nDivsMax, int iChoice, int fUseXor, int fDebug, int fVerbose, int ** ppArray ) -{ - Vec_Ptr_t Divs = { nDivs, nDivs, ppDivs }; - assert( s_pResbMan != NULL ); // first call Abc_ResubPrepareManager() - Gia_ManResubPerform( s_pResbMan, &Divs, nWords, nLimit, nDivsMax, iChoice, fUseXor, fDebug, fVerbose==2 ); - if ( fVerbose ) - { - int nGates = Vec_IntSize(s_pResbMan->vGates)/2; - if ( nGates ) - { - printf( " Gain = %2d Gates = %2d __________ F = ", nLimit+1-nGates, nGates ); - Gia_ManResubPrint( s_pResbMan->vGates, nDivs ); - printf( "\n" ); - } - } - if ( fDebug ) - { - if ( !Gia_ManResubVerify(s_pResbMan, NULL) ) - { - Gia_ManResubPrint( s_pResbMan->vGates, nDivs ); - printf( "Verification FAILED.\n" ); - } - //else - // printf( "Verification succeeded.\n" ); - } - *ppArray = Vec_IntArray(s_pResbMan->vGates); - assert( Vec_IntSize(s_pResbMan->vGates)/2 <= nLimit ); - return Vec_IntSize(s_pResbMan->vGates); -} - -inline void Gia_ManSimPatWriteOne( FILE * pFile, word * pSim, int nWords ) -{ - int k, Digit, nDigits = nWords*16; - for ( k = 0; k < nDigits; k++ ) - { - Digit = (int)((pSim[k/16] >> ((k%16) * 4)) & 15); - if ( Digit < 10 ) - fprintf( pFile, "%d", Digit ); - else - fprintf( pFile, "%c", 'A' + Digit-10 ); - } - fprintf( pFile, "\n" ); -} -inline void Gia_ManSimPatWrite( const char * pFileName, Vec_Wrd_t * vSimsIn, int nWords ) -{ - int i, nNodes = Vec_WrdSize(vSimsIn) / nWords; - FILE * pFile = fopen( pFileName, "wb" ); - if ( pFile == NULL ) - { - printf( "Cannot open file \"%s\" for writing.\n", pFileName ); - return; - } - assert( Vec_WrdSize(vSimsIn) % nWords == 0 ); - for ( i = 0; i < nNodes; i++ ) - Gia_ManSimPatWriteOne( pFile, Vec_WrdEntryP(vSimsIn, i*nWords), nWords ); - fclose( pFile ); - printf( "Written %d words of simulation data for %d objects into file \"%s\".\n", nWords, Vec_WrdSize(vSimsIn)/nWords, pFileName ); -} - -inline void Abc_ResubDumpProblem( const char * pFileName, void ** ppDivs, int nDivs, int nWords ) -{ - Vec_Wrd_t * vSims = Vec_WrdAlloc( nDivs * nWords ); - word ** pDivs = (word **)ppDivs; - int d, w; - for ( d = 0; d < nDivs; d++ ) - for ( w = 0; w < nWords; w++ ) - Vec_WrdPush( vSims, pDivs[d][w] ); - Gia_ManSimPatWrite( pFileName, vSims, nWords ); - Vec_WrdFree( vSims ); -} - -/**Function************************************************************* - - Synopsis [Top level.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ - -#if 0 -extern void Extra_PrintHex( FILE * pFile, unsigned * pTruth, int nVars ); -extern void Dau_DsdPrintFromTruth2( word * pTruth, int nVarsInit ); - -void Gia_ManResubTest3() -{ - int nVars = 3; - int fVerbose = 1; - word Divs[6] = { 0, 0, - ABC_CONST(0xAAAAAAAAAAAAAAAA), - ABC_CONST(0xCCCCCCCCCCCCCCCC), - ABC_CONST(0xF0F0F0F0F0F0F0F0), - ABC_CONST(0xFF00FF00FF00FF00) - }; - Vec_Ptr_t * vDivs = Vec_PtrAlloc( 6 ); - Vec_Int_t * vRes = Vec_IntAlloc( 100 ); - int i, k, ArraySize, * pArray; - for ( i = 0; i < 6; i++ ) - Vec_PtrPush( vDivs, Divs+i ); - Abc_ResubPrepareManager( 1 ); - for ( i = 0; i < (1<<(1<= (1<<14) ) - { - printf( "Reducing all divs from %d to %d.\n", Vec_PtrSize(vDivs), (1<<14)-1 ); - Vec_PtrShrink( vDivs, (1<<14)-1 ); - } - assert( Vec_PtrSize(vDivs) < (1<<14) ); - Gia_ManResubPerform( p, vDivs, nWords, 100, 50, iChoice, fUseXor, 1, 1 ); - if ( Vec_IntSize(p->vGates) ) - { - Vec_Wec_t * vGates = Vec_WecStart(1); - Vec_IntAppend( Vec_WecEntry(vGates, 0), p->vGates ); - pMan = Gia_ManConstructFromGates( vGates, Vec_PtrSize(vDivs) ); - Vec_WecFree( vGates ); - } - else - printf( "Decomposition did not succeed.\n" ); - Gia_ResbFree( p ); - Vec_PtrFree( vDivs ); - Vec_WrdFree( vSims ); - return pMan; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Gia_ManUnivTfo_rec( Gia_Man_t * p, int iObj, Vec_Int_t * vNodes, Vec_Int_t * vPos ) -{ - int i, iFan, Count = 1; - if ( Gia_ObjIsTravIdCurrentId(p, iObj) ) - return 0; - Gia_ObjSetTravIdCurrentId(p, iObj); - if ( vNodes && Gia_ObjIsCo(Gia_ManObj(p, iObj)) ) - Vec_IntPush( vNodes, iObj ); - if ( vPos && Gia_ObjIsCo(Gia_ManObj(p, iObj)) ) - Vec_IntPush( vPos, iObj ); - Gia_ObjForEachFanoutStaticId( p, iObj, iFan, i ) - Count += Gia_ManUnivTfo_rec( p, iFan, vNodes, vPos ); - return Count; -} -int Gia_ManUnivTfo( Gia_Man_t * p, int * pObjs, int nObjs, Vec_Int_t ** pvNodes, Vec_Int_t ** pvPos ) -{ - int i, Count = 0; - if ( pvNodes ) - { - if ( *pvNodes ) - Vec_IntClear( *pvNodes ); - else - *pvNodes = Vec_IntAlloc( 100 ); - } - if ( pvPos ) - { - if ( *pvPos ) - Vec_IntClear( *pvPos ); - else - *pvPos = Vec_IntAlloc( 100 ); - } - Gia_ManIncrementTravId( p ); - for ( i = 0; i < nObjs; i++ ) - Count += Gia_ManUnivTfo_rec( p, pObjs[i], pvNodes ? *pvNodes : NULL, pvPos ? *pvPos : NULL ); - if ( pvNodes ) - Vec_IntSort( *pvNodes, 0 ); - if ( pvPos ) - Vec_IntSort( *pvPos, 0 ); - return Count; -} - -/**Function************************************************************* - - Synopsis [Tuning resub.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Gia_ManTryResub( Gia_Man_t * p ) -{ - int nLimit = 20; - int nDivsMax = 200; - int iChoice = 0; - int fUseXor = 1; - int fDebug = 1; - int fVerbose = 0; - abctime clk, clkResub = 0, clkStart = Abc_Clock(); - Vec_Ptr_t * vvSims = Vec_PtrAlloc( 100 ); - Vec_Wrd_t * vSims; - word * pSets[2], * pFunc; - Gia_Obj_t * pObj, * pObj2; - int i, i2, nWords, nNonDec = 0, nTotal = 0; - assert( Gia_ManCiNum(p) < 16 ); - Vec_WrdFreeP( &p->vSimsPi ); - p->vSimsPi = Vec_WrdStartTruthTables( Gia_ManCiNum(p) ); - nWords = Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p); - //Vec_WrdPrintHex( p->vSimsPi, nWords ); - pSets[0] = ABC_CALLOC( word, nWords ); - pSets[1] = ABC_CALLOC( word, nWords ); - vSims = Gia_ManSimPatSim( p ); - Gia_ManLevelNum(p); - Gia_ManCreateRefs(p); - Abc_ResubPrepareManager( nWords ); - Gia_ManStaticFanoutStart( p ); - Gia_ManForEachAnd( p, pObj, i ) - { - Vec_Int_t vGates; - int * pArray, nArray, nTfo, iObj = Gia_ObjId(p, pObj); - int Level = Gia_ObjLevel(p, pObj); - int nMffc = Gia_NodeMffcSizeMark(p, pObj); - pFunc = Vec_WrdEntryP( vSims, nWords*iObj ); - Abc_TtCopy( pSets[0], pFunc, nWords, 1 ); - Abc_TtCopy( pSets[1], pFunc, nWords, 0 ); - Vec_PtrClear( vvSims ); - Vec_PtrPushTwo( vvSims, pSets[0], pSets[1] ); - nTfo = Gia_ManUnivTfo( p, &iObj, 1, NULL, NULL ); - Gia_ManForEachCi( p, pObj2, i2 ) - Vec_PtrPush( vvSims, Vec_WrdEntryP(vSims, nWords*Gia_ObjId(p, pObj2)) ); - Gia_ManForEachAnd( p, pObj2, i2 ) - if ( !Gia_ObjIsTravIdCurrent(p, pObj2) && !Gia_ObjIsTravIdPrevious(p, pObj2) && Gia_ObjLevel(p, pObj2) <= Level ) - Vec_PtrPush( vvSims, Vec_WrdEntryP(vSims, nWords*Gia_ObjId(p, pObj2)) ); - if ( fVerbose ) - printf( "%3d : Lev = %2d Mffc = %2d Divs = %3d Tfo = %3d\n", iObj, Level, nMffc, Vec_PtrSize(vvSims)-2, nTfo ); - clk = Abc_Clock(); - nArray = Abc_ResubComputeFunction( (void **)Vec_PtrArray(vvSims), Vec_PtrSize(vvSims), nWords, Abc_MinInt(nMffc-1, nLimit), nDivsMax, iChoice, fUseXor, fDebug, fVerbose, &pArray ); - clkResub += Abc_Clock() - clk; - vGates.nSize = vGates.nCap = nArray; - vGates.pArray = pArray; - assert( nMffc > Vec_IntSize(&vGates)/2 ); - if ( Vec_IntSize(&vGates) > 0 ) - nTotal += nMffc - Vec_IntSize(&vGates)/2; - nNonDec += Vec_IntSize(&vGates) == 0; - } - printf( "Total nodes = %5d. Non-realizable = %5d. Gain = %6d. ", Gia_ManAndNum(p), nNonDec, nTotal ); - Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart ); - Abc_PrintTime( 1, "Pure resub time", clkResub ); - Abc_ResubPrepareManager( 0 ); - Gia_ManStaticFanoutStop( p ); - Vec_PtrFree( vvSims ); - Vec_WrdFree( vSims ); - ABC_FREE( pSets[0] ); - ABC_FREE( pSets[1] ); -} -#endif - -} /* namespace abcresub */ diff --git a/lib/abcresub/abcresub/abcresub2.hpp b/lib/abcresub/abcresub/abcresub2.hpp deleted file mode 100644 index 17bba0b6d..000000000 --- a/lib/abcresub/abcresub/abcresub2.hpp +++ /dev/null @@ -1,419 +0,0 @@ -/*! - \file abcresub2.hpp - \brief Extracted from ABC - https://github.com/berkeley-abc/abc - - \author Alan Mishchenko (UC Berkeley) -*/ - -#pragma once - -#include "abcresub.hpp" - -namespace abcresub -{ - -static word s_Truths6[6] = { - ABC_CONST(0xAAAAAAAAAAAAAAAA), - ABC_CONST(0xCCCCCCCCCCCCCCCC), - ABC_CONST(0xF0F0F0F0F0F0F0F0), - ABC_CONST(0xFF00FF00FF00FF00), - ABC_CONST(0xFFFF0000FFFF0000), - ABC_CONST(0xFFFFFFFF00000000) -}; - -typedef struct Gia_Rsb2Man_t_ Gia_Rsb2Man_t; -struct Gia_Rsb2Man_t_ -{ - // hyper-parameters - int nDivsMax; - int nLevelIncrease; - int fUseXor; - int fUseZeroCost; - int fDebug; - int fVerbose; - // input AIG - int nObjs; - int nPis; - int nNodes; - int nPos; - int iFirstPo; - int Level; - int nMffc; - // intermediate data - Vec_Int_t vObjs; - Vec_Wrd_t vSims; - Vec_Ptr_t vpDivs; - Vec_Int_t vDivs; - Vec_Int_t vLevels; - Vec_Int_t vRefs; - Vec_Int_t vCopies; - Vec_Int_t vTried; - word Truth0; - word Truth1; - word CareSet; -}; - -inline Gia_Rsb2Man_t * Gia_Rsb2ManAlloc() -{ - Gia_Rsb2Man_t * p = ABC_CALLOC( Gia_Rsb2Man_t, 1 ); - return p; -} - -inline void Gia_Rsb2ManFree( Gia_Rsb2Man_t * p ) -{ - Vec_IntErase( &p->vObjs ); - Vec_WrdErase( &p->vSims ); - Vec_PtrErase( &p->vpDivs ); - Vec_IntErase( &p->vDivs ); - Vec_IntErase( &p->vLevels ); - Vec_IntErase( &p->vRefs ); - Vec_IntErase( &p->vCopies ); - Vec_IntErase( &p->vTried ); - ABC_FREE( p ); -} - -inline void Gia_Rsb2ManStart( Gia_Rsb2Man_t * p, int * pObjs, int nObjs, int nDivsMax, int nLevelIncrease, int fUseXor, int fUseZeroCost, int fDebug, int fVerbose ) -{ - int i; - // hyper-parameters - p->nDivsMax = nDivsMax; - p->nLevelIncrease = nLevelIncrease; - p->fUseXor = fUseXor; - p->fUseZeroCost = fUseZeroCost; - p->fDebug = fDebug; - p->fVerbose = fVerbose; - // user data - Vec_IntClear( &p->vObjs ); - Vec_IntPushArray( &p->vObjs, pObjs, 2*nObjs ); - assert( pObjs[0] == 0 ); - assert( pObjs[1] == 0 ); - p->nObjs = nObjs; - p->nPis = 0; - p->nNodes = 0; - p->nPos = 0; - p->iFirstPo = 0; - for ( i = 1; i < nObjs; i++ ) - { - if ( pObjs[2*i+0] == 0 && pObjs[2*i+1] == 0 ) - p->nPis++; - else if ( pObjs[2*i+0] == pObjs[2*i+1] ) - p->nPos++; - else - p->nNodes++; - } - assert( nObjs == 1 + p->nPis + p->nNodes + p->nPos ); - p->iFirstPo = nObjs - p->nPos; - Vec_WrdClear( &p->vSims ); - Vec_WrdGrow( &p->vSims, 2*nObjs ); - Vec_WrdPush( &p->vSims, 0 ); - Vec_WrdPush( &p->vSims, 0 ); - for ( i = 0; i < p->nPis; i++ ) - { - Vec_WrdPush( &p->vSims, s_Truths6[i] ); - Vec_WrdPush( &p->vSims, ~s_Truths6[i] ); - } - p->vSims.nSize = 2*p->nObjs; - Vec_IntClear( &p->vDivs ); - Vec_IntClear( &p->vLevels ); - Vec_IntClear( &p->vRefs ); - Vec_IntClear( &p->vCopies ); - Vec_IntClear( &p->vTried ); - Vec_PtrClear( &p->vpDivs ); - Vec_IntGrow( &p->vDivs, nObjs ); - Vec_IntGrow( &p->vLevels, nObjs ); - Vec_IntGrow( &p->vRefs, nObjs ); - Vec_IntGrow( &p->vCopies, nObjs ); - Vec_IntGrow( &p->vTried, nObjs ); - Vec_PtrGrow( &p->vpDivs, nObjs ); -} - -inline void Gia_Rsb2ManPrint( Gia_Rsb2Man_t * p ) -{ - int i, * pObjs = Vec_IntArray( &p->vObjs ); - printf( "PI = %d. PO = %d. Obj = %d.\n", p->nPis, p->nPos, p->nObjs ); - for ( i = p->nPis + 1; i < p->iFirstPo; i++ ) - printf( "%2d = %c%2d & %c%2d;\n", i, - Abc_LitIsCompl(pObjs[2*i+0]) ? '!' : ' ', Abc_Lit2Var(pObjs[2*i+0]), - Abc_LitIsCompl(pObjs[2*i+1]) ? '!' : ' ', Abc_Lit2Var(pObjs[2*i+1]) ); - for ( i = p->iFirstPo; i < p->nObjs; i++ ) - printf( "%2d = %c%2d;\n", i, - Abc_LitIsCompl(pObjs[2*i+0]) ? '!' : ' ', Abc_Lit2Var(pObjs[2*i+0]) ); -} - -inline int Gia_Rsb2ManLevel( Gia_Rsb2Man_t * p ) -{ - int i, * pLevs, Level = 0; - Vec_IntClear( &p->vLevels ); - Vec_IntGrow( &p->vLevels, p->nObjs ); - pLevs = Vec_IntArray( &p->vLevels ); - for ( i = p->nPis + 1; i < p->iFirstPo; i++ ) - pLevs[i] = 1 + Abc_MaxInt( pLevs[2*i+0]/2, pLevs[2*i+1]/2 ); - for ( i = p->iFirstPo; i < p->nObjs; i++ ) - Level = Abc_MaxInt( Level, pLevs[i] = pLevs[2*i+0]/2 ); - return Level; -} - -inline word Gia_Rsb2ManOdcs( Gia_Rsb2Man_t * p, int iNode ) -{ - int i; word Res = 0; - int * pObjs = Vec_IntArray( &p->vObjs ); - word * pSims = Vec_WrdArray( &p->vSims ); - for ( i = p->nPis + 1; i < p->iFirstPo; i++ ) - { - if ( pObjs[2*i+0] < pObjs[2*i+1] ) - pSims[2*i+0] = pSims[pObjs[2*i+0]] & pSims[pObjs[2*i+1]]; - else if ( pObjs[2*i+0] > pObjs[2*i+1] ) - pSims[2*i+0] = pSims[pObjs[2*i+0]] ^ pSims[pObjs[2*i+1]]; - else assert( 0 ); - pSims[2*i+1] = ~pSims[2*i+0]; - } - for ( i = p->iFirstPo; i < p->nObjs; i++ ) - pSims[2*i+0] = pSims[pObjs[2*i+0]]; - ABC_SWAP( word, pSims[2*iNode+0], pSims[2*iNode+1] ); - for ( i = iNode + 1; i < p->iFirstPo; i++ ) - { - if ( pObjs[2*i+0] < pObjs[2*i+1] ) - pSims[2*i+0] = pSims[pObjs[2*i+0]] & pSims[pObjs[2*i+1]]; - else if ( pObjs[2*i+0] < pObjs[2*i+1] ) - pSims[2*i+0] = pSims[pObjs[2*i+0]] ^ pSims[pObjs[2*i+1]]; - else assert( 0 ); - pSims[2*i+1] = ~pSims[2*i+0]; - } - for ( i = p->iFirstPo; i < p->nObjs; i++ ) - Res |= pSims[2*i+0] ^ pSims[pObjs[2*i+0]]; - ABC_SWAP( word, pSims[2*iNode+0], pSims[2*iNode+1] ); - return Res; -} - -// marks MFFC and returns its size -inline int Gia_Rsb2ManDeref_rec( Gia_Rsb2Man_t * p, int * pObjs, int * pRefs, int iNode ) -{ - int Counter = 1; - if ( iNode <= p->nPis ) - return 0; - if ( --pRefs[Abc_Lit2Var(pObjs[2*iNode+0])] == 0 ) - Counter += Gia_Rsb2ManDeref_rec( p, pObjs, pRefs, Abc_Lit2Var(pObjs[2*iNode+0]) ); - if ( --pRefs[Abc_Lit2Var(pObjs[2*iNode+1])] == 0 ) - Counter += Gia_Rsb2ManDeref_rec( p, pObjs, pRefs, Abc_Lit2Var(pObjs[2*iNode+1]) ); - return Counter; -} - -inline int Gia_Rsb2ManMffc( Gia_Rsb2Man_t * p, int iNode ) -{ - int i, * pRefs, * pObjs; - Vec_IntFill( &p->vRefs, p->nObjs, 0 ); - pRefs = Vec_IntArray( &p->vRefs ); - pObjs = Vec_IntArray( &p->vObjs ); - assert( pObjs[2*iNode+0] != pObjs[2*iNode+1] ); - for ( i = p->nPis + 1; i < p->iFirstPo; i++ ) - pRefs[Abc_Lit2Var(pObjs[2*i+0])]++, - pRefs[Abc_Lit2Var(pObjs[2*i+1])]++; - for ( i = p->iFirstPo; i < p->nObjs; i++ ) - pRefs[Abc_Lit2Var(pObjs[2*i+0])]++; - for ( i = p->nPis + 1; i < p->iFirstPo; i++ ) - assert( pRefs[i] ); - pRefs[iNode] = 0; - for ( i = iNode + 1; i < p->iFirstPo; i++ ) - if ( !pRefs[Abc_Lit2Var(pObjs[2*i+0])] || !pRefs[Abc_Lit2Var(pObjs[2*i+1])] ) - pRefs[i] = 0; - return Gia_Rsb2ManDeref_rec( p, pObjs, pRefs, iNode ); -} - -// collects divisors and maps them into nodes -// assumes MFFC is already marked -inline int Gia_Rsb2ManDivs( Gia_Rsb2Man_t * p, int iNode ) -{ - int i, iNodeLevel = 0; - int * pRefs = Vec_IntArray( &p->vRefs ); - p->CareSet = Gia_Rsb2ManOdcs( p, iNode ); - p->Truth1 = p->CareSet & Vec_WrdEntry(&p->vSims, 2*iNode); - p->Truth0 = p->CareSet & ~p->Truth1; - Vec_PtrClear( &p->vpDivs ); - Vec_PtrPush( &p->vpDivs, &p->Truth0 ); - Vec_PtrPush( &p->vpDivs, &p->Truth1 ); - Vec_IntClear( &p->vDivs ); - Vec_IntPushTwo( &p->vDivs, -1, -1 ); - for ( i = 1; i <= p->nPis; i++ ) - { - Vec_PtrPush( &p->vpDivs, Vec_WrdEntryP(&p->vSims, 2*i) ); - Vec_IntPush( &p->vDivs, i ); - } - p->nMffc = Gia_Rsb2ManMffc( p, iNode ); - if ( p->nLevelIncrease >= 0 ) - { - p->Level = Gia_Rsb2ManLevel(p); - iNodeLevel = Vec_IntEntry(&p->vLevels, iNode); - } - for ( i = p->nPis + 1; i < p->iFirstPo; i++ ) - { - if ( !pRefs[i] || (p->nLevelIncrease >= 0 && Vec_IntEntry(&p->vLevels, i) > iNodeLevel + p->nLevelIncrease) ) - continue; - Vec_PtrPush( &p->vpDivs, Vec_WrdEntryP(&p->vSims, 2*i) ); - Vec_IntPush( &p->vDivs, i ); - } - assert( Vec_IntSize(&p->vDivs) == Vec_PtrSize(&p->vpDivs) ); - return Vec_IntSize(&p->vDivs); -} - -inline int Gia_Rsb2AddNode( Vec_Int_t * vRes, int iLit0, int iLit1, int iRes0, int iRes1 ) -{ - int iLitMin = iRes0 < iRes1 ? Abc_LitNotCond(iRes0, Abc_LitIsCompl(iLit0)) : Abc_LitNotCond(iRes1, Abc_LitIsCompl(iLit1)); - int iLitMax = iRes0 < iRes1 ? Abc_LitNotCond(iRes1, Abc_LitIsCompl(iLit1)) : Abc_LitNotCond(iRes0, Abc_LitIsCompl(iLit0)); - int iLitRes = Vec_IntSize(vRes); - if ( iLit0 < iLit1 ) // and - { - if ( iLitMin == 0 ) - return 0; - if ( iLitMin == 1 ) - return iLitMax; - if ( iLitMin == Abc_LitNot(iLitMax) ) - return 0; - } - else if ( iLit0 > iLit1 ) // xor - { - if ( iLitMin == 0 ) - return iLitMax; - if ( iLitMin == 1 ) - return Abc_LitNot(iLitMax); - if ( iLitMin == Abc_LitNot(iLitMax) ) - return 1; - } - else assert( 0 ); - assert( iLitMin >= 2 && iLitMax >= 2 ); - if ( iLit0 < iLit1 ) // and - { - Vec_IntPushTwo( vRes, iLitMin, iLitMax ); - } - else if ( iLit0 > iLit1 ) // xor - { - assert( !Abc_LitIsCompl(iLit0) ); - assert( !Abc_LitIsCompl(iLit1) ); - Vec_IntPushTwo( vRes, iLitMax, iLitMin ); - } - else assert( 0 ); - return iLitRes; -} - -inline int Gia_Rsb2ManInsert_rec( Vec_Int_t * vRes, int nPis, Vec_Int_t * vObjs, int iNode, Vec_Int_t * vResub, Vec_Int_t * vDivs, Vec_Int_t * vCopies, int iObj ) -{ - if ( Vec_IntEntry(vCopies, iObj) >= 0 ) - return Vec_IntEntry(vCopies, iObj); - assert( iObj > nPis ); - if ( iObj == iNode ) - { - int nVars = Vec_IntSize(vDivs); - int iLitRes = -1, iTopLit = Vec_IntEntryLast( vResub ); - if ( Abc_Lit2Var(iTopLit) == 0 ) - iLitRes = 0; - else if ( Abc_Lit2Var(iTopLit) < nVars ) - iLitRes = Gia_Rsb2ManInsert_rec( vRes, nPis, vObjs, -1, vResub, vDivs, vCopies, Vec_IntEntry(vDivs, Abc_Lit2Var(iTopLit)) ); - else - { - Vec_Int_t * vCopy = Vec_IntAlloc( 10 ); - int k, iLit, iLit0, iLit1; - Vec_IntForEachEntryStop( vResub, iLit, k, Vec_IntSize(vResub)-1 ) - if ( Abc_Lit2Var(iLit) < nVars ) - Gia_Rsb2ManInsert_rec( vRes, nPis, vObjs, -1, vResub, vDivs, vCopies, Vec_IntEntry(vDivs, Abc_Lit2Var(iLit)) ); - Vec_IntForEachEntryDouble( vResub, iLit0, iLit1, k ) - { - int iVar0 = Abc_Lit2Var(iLit0); - int iVar1 = Abc_Lit2Var(iLit1); - int iRes0 = iVar0 < nVars ? Vec_IntEntry(vCopies, Vec_IntEntry(vDivs, iVar0)) : Vec_IntEntry(vCopy, iVar0 - nVars); - int iRes1 = iVar1 < nVars ? Vec_IntEntry(vCopies, Vec_IntEntry(vDivs, iVar1)) : Vec_IntEntry(vCopy, iVar1 - nVars); - iLitRes = Gia_Rsb2AddNode( vRes, iLit0, iLit1, iRes0, iRes1 ); - Vec_IntPush( vCopy, iLitRes ); - } - Vec_IntFree( vCopy ); - } - iLitRes = Abc_LitNotCond( iLitRes, Abc_LitIsCompl(iTopLit) ); - Vec_IntWriteEntry( vCopies, iObj, iLitRes ); - return iLitRes; - } - else - { - int iLit0 = Vec_IntEntry( vObjs, 2*iObj+0 ); - int iLit1 = Vec_IntEntry( vObjs, 2*iObj+1 ); - int iRes0 = Gia_Rsb2ManInsert_rec( vRes, nPis, vObjs, iNode, vResub, vDivs, vCopies, Abc_Lit2Var(iLit0) ); - int iRes1 = Gia_Rsb2ManInsert_rec( vRes, nPis, vObjs, iNode, vResub, vDivs, vCopies, Abc_Lit2Var(iLit1) ); - int iLitRes = Gia_Rsb2AddNode( vRes, iLit0, iLit1, iRes0, iRes1 ); - Vec_IntWriteEntry( vCopies, iObj, iLitRes ); - return iLitRes; - } -} - -inline Vec_Int_t * Gia_Rsb2ManInsert( int nPis, int nPos, Vec_Int_t * vObjs, int iNode, Vec_Int_t * vResub, Vec_Int_t * vDivs, Vec_Int_t * vCopies ) -{ - int i, nObjs = Vec_IntSize(vObjs)/2, iFirstPo = nObjs - nPos; - Vec_Int_t * vRes = Vec_IntAlloc( Vec_IntSize(vObjs) ); -//Vec_IntPrint( vDivs ); -//Vec_IntPrint( vResub ); - Vec_IntFill( vCopies, Vec_IntSize(vObjs), -1 ); - Vec_IntFill( vRes, 2*(nPis + 1), 0 ); - for ( i = 0; i <= nPis; i++ ) - Vec_IntWriteEntry( vCopies, i, 2*i ); - for ( i = iFirstPo; i < nObjs; i++ ) - Gia_Rsb2ManInsert_rec( vRes, nPis, vObjs, iNode, vResub, vDivs, vCopies, Abc_Lit2Var( Vec_IntEntry(vObjs, 2*i) ) ); - for ( i = iFirstPo; i < nObjs; i++ ) - { - int iLitNew = Abc_Lit2LitL( Vec_IntArray(vCopies), Vec_IntEntry(vObjs, 2*i) ); - Vec_IntPushTwo( vRes, iLitNew, iLitNew ); - } - return vRes; -} - -inline int Abc_ResubNodeToTry( Vec_Int_t * vTried, int iFirst, int iLast ) -{ - int iNode; - //for ( iNode = iFirst; iNode < iLast; iNode++ ) - for ( iNode = iLast - 1; iNode >= iFirst; iNode-- ) - if ( Vec_IntFind(vTried, iNode) == -1 ) - return iNode; - return -1; -} - -inline int Abc_ResubComputeWindow( int * pObjs, int nObjs, int nDivsMax, int nLevelIncrease, int fUseXor, int fUseZeroCost, int fDebug, int fVerbose, int ** ppArray, int * pnResubs ) -{ - int iNode, nChanges = 0, RetValue = 0; - Gia_Rsb2Man_t * p = Gia_Rsb2ManAlloc(); - Gia_Rsb2ManStart( p, pObjs, nObjs, nDivsMax, nLevelIncrease, fUseXor, fUseZeroCost, fDebug, fVerbose ); - *ppArray = NULL; - while ( (iNode = Abc_ResubNodeToTry(&p->vTried, p->nPis+1, p->iFirstPo)) > 0 ) - { - int nDivs = Gia_Rsb2ManDivs( p, iNode ); - int * pResub, nResub = Abc_ResubComputeFunction( Vec_PtrArray(&p->vpDivs), nDivs, 1, p->nMffc-1, nDivsMax, 0, fUseXor, fDebug, fVerbose, &pResub ); - if ( nResub == 0 ) - Vec_IntPush( &p->vTried, iNode ); - else - { - int i, k = 0, iTried; - Vec_Int_t vResub = { nResub, nResub, pResub }; - Vec_Int_t * vRes = Gia_Rsb2ManInsert( p->nPis, p->nPos, &p->vObjs, iNode, &vResub, &p->vDivs, &p->vCopies ); - //printf( "\nResubing node %d:\n", iNode ); - //Gia_Rsb2ManPrint( p ); - p->nObjs = Vec_IntSize(vRes)/2; - p->iFirstPo = p->nObjs - p->nPos; - Vec_IntClear( &p->vObjs ); - Vec_IntAppend( &p->vObjs, vRes ); - Vec_IntFree( vRes ); - Vec_IntForEachEntry( &p->vTried, iTried, i ) - if ( Vec_IntEntry(&p->vCopies, iTried) > Abc_Var2Lit(p->nPis, 0) ) // internal node - Vec_IntWriteEntry( &p->vTried, k++, Abc_Lit2Var(Vec_IntEntry(&p->vCopies, iTried)) ); - Vec_IntShrink( &p->vTried, k ); - nChanges++; - //Gia_Rsb2ManPrint( p ); - } - } - if ( nChanges ) - { - RetValue = p->nObjs; - *ppArray = p->vObjs.pArray; - Vec_IntZero( &p->vObjs ); - } - Gia_Rsb2ManFree( p ); - if ( pnResubs ) - *pnResubs = nChanges; - return RetValue; -} - -} /* abcresub */ diff --git a/lib/abcresub/abcresub/tt.hpp b/lib/abcresub/abcresub/tt.hpp deleted file mode 100644 index 482a3b08b..000000000 --- a/lib/abcresub/abcresub/tt.hpp +++ /dev/null @@ -1,331 +0,0 @@ -/*! - \file tt.hpp - \brief Extracted from ABC - https://github.com/berkeley-abc/abc - - \author Alan Mishchenko (UC Berkeley) -*/ - -#pragma once - -namespace abcresub -{ - -// read/write/flip i-th bit of a bit string table: -inline int Abc_TtGetBit( word * p, int i ) { return (int)(p[i>>6] >> (word)(i & 63)) & 1; } -inline void Abc_TtSetBit( word * p, int i ) { p[i>>6] |= (word)(((word)1)<<(i & 63)); } -inline void Abc_TtXorBit( word * p, int i ) { p[i>>6] ^= (word)(((word)1)<<(i & 63)); } - -// read/write k-th digit d of a quaternary number: -inline int Abc_TtGetQua( word * p, int k ) { return (int)(p[k>>5] >> (word)((k<<1) & 63)) & 3; } -inline void Abc_TtSetQua( word * p, int k, int d ) { p[k>>5] |= (word)(((word)d)<<((k<<1) & 63)); } -inline void Abc_TtXorQua( word * p, int k, int d ) { p[k>>5] ^= (word)(((word)d)<<((k<<1) & 63)); } - -// read/write k-th digit d of a hexadecimal number: -inline int Abc_TtGetHex( word * p, int k ) { return (int)(p[k>>4] >> (word)((k<<2) & 63)) & 15; } -inline void Abc_TtSetHex( word * p, int k, int d ) { p[k>>4] |= (word)(((word)d)<<((k<<2) & 63)); } -inline void Abc_TtXorHex( word * p, int k, int d ) { p[k>>4] ^= (word)(((word)d)<<((k<<2) & 63)); } - -// read/write k-th digit d of a 256-base number: -inline int Abc_TtGet256( word * p, int k ) { return (int)(p[k>>3] >> (word)((k<<3) & 63)) & 255; } -inline void Abc_TtSet256( word * p, int k, int d ) { p[k>>3] |= (word)(((word)d)<<((k<<3) & 63)); } -inline void Abc_TtXor256( word * p, int k, int d ) { p[k>>3] ^= (word)(((word)d)<<((k<<3) & 63)); } - -inline int Abc_TtCountOnes( word x ) -{ - x = x - ((x >> 1) & ABC_CONST(0x5555555555555555)); - x = (x & ABC_CONST(0x3333333333333333)) + ((x >> 2) & ABC_CONST(0x3333333333333333)); - x = (x + (x >> 4)) & ABC_CONST(0x0F0F0F0F0F0F0F0F); - x = x + (x >> 8); - x = x + (x >> 16); - x = x + (x >> 32); - return (int)(x & 0xFF); -} - -inline int Abc_TtCountOnesVec( word * x, int nWords ) -{ - int w, Count = 0; - for ( w = 0; w < nWords; w++ ) - Count += Abc_TtCountOnes( x[w] ); - return Count; -} - -inline int Abc_TtCountOnesVecMask( word * x, word * pMask, int nWords, int fCompl ) -{ - int w, Count = 0; - if ( fCompl ) - for ( w = 0; w < nWords; w++ ) - Count += Abc_TtCountOnes( pMask[w] & ~x[w] ); - else - for ( w = 0; w < nWords; w++ ) - Count += Abc_TtCountOnes( pMask[w] & x[w] ); - return Count; -} - -inline int Abc_TtCountOnesVecMask2( word * x0, word * x1, int fComp0, int fComp1, word * pMask, int nWords ) -{ - int w, Count = 0; - if ( !fComp0 && !fComp1 ) - for ( w = 0; w < nWords; w++ ) - Count += Abc_TtCountOnes( pMask[w] & x0[w] & x1[w] ); - else if ( fComp0 && !fComp1 ) - for ( w = 0; w < nWords; w++ ) - Count += Abc_TtCountOnes( pMask[w] & ~x0[w] & x1[w] ); - else if ( !fComp0 && fComp1 ) - for ( w = 0; w < nWords; w++ ) - Count += Abc_TtCountOnes( pMask[w] & x0[w] & ~x1[w] ); - else - for ( w = 0; w < nWords; w++ ) - Count += Abc_TtCountOnes( pMask[w] & ~x0[w] & ~x1[w] ); - return Count; -} - -inline int Abc_TtCountOnesVecXorMask( word * x, word * y, int fCompl, word * pMask, int nWords ) -{ - int w, Count = 0; - if ( fCompl ) - for ( w = 0; w < nWords; w++ ) - Count += Abc_TtCountOnes( pMask[w] & (x[w] ^ ~y[w]) ); - else - for ( w = 0; w < nWords; w++ ) - Count += Abc_TtCountOnes( pMask[w] & (x[w] ^ y[w]) ); - return Count; -} - -inline void Abc_TtCopy( word * pOut, word * pIn, int nWords, int fCompl ) -{ - int w; - if ( fCompl ) - for ( w = 0; w < nWords; w++ ) - pOut[w] = ~pIn[w]; - else - for ( w = 0; w < nWords; w++ ) - pOut[w] = pIn[w]; -} - -inline int Abc_TtIsConst0( word * pIn1, int nWords ) -{ - int w; - for ( w = 0; w < nWords; w++ ) - if ( pIn1[w] ) - return 0; - return 1; -} - -inline void Abc_TtClear( word * pOut, int nWords ) -{ - int w; - for ( w = 0; w < nWords; w++ ) - pOut[w] = 0; -} - -inline void Abc_TtFill( word * pOut, int nWords ) -{ - int w; - for ( w = 0; w < nWords; w++ ) - pOut[w] = ~(word)0; -} - -inline void Abc_TtAndCompl( word * pOut, word * pIn1, int fCompl1, word * pIn2, int fCompl2, int nWords ) -{ - int w; - if ( fCompl1 ) - { - if ( fCompl2 ) - for ( w = 0; w < nWords; w++ ) - pOut[w] = ~pIn1[w] & ~pIn2[w]; - else - for ( w = 0; w < nWords; w++ ) - pOut[w] = ~pIn1[w] & pIn2[w]; - } - else - { - if ( fCompl2 ) - for ( w = 0; w < nWords; w++ ) - pOut[w] = pIn1[w] & ~pIn2[w]; - else - for ( w = 0; w < nWords; w++ ) - pOut[w] = pIn1[w] & pIn2[w]; - } -} - -inline void Abc_TtAndSharp( word * pOut, word * pIn1, word * pIn2, int nWords, int fCompl ) -{ - int w; - if ( fCompl ) - for ( w = 0; w < nWords; w++ ) - pOut[w] = pIn1[w] & ~pIn2[w]; - else - for ( w = 0; w < nWords; w++ ) - pOut[w] = pIn1[w] & pIn2[w]; -} - -inline void Abc_TtXor( word * pOut, word * pIn1, word * pIn2, int nWords, int fCompl ) -{ - int w; - if ( fCompl ) - for ( w = 0; w < nWords; w++ ) - pOut[w] = pIn1[w] ^ ~pIn2[w]; - else - for ( w = 0; w < nWords; w++ ) - pOut[w] = pIn1[w] ^ pIn2[w]; -} - -inline int Abc_TtIntersectOne( word * pOut, int fComp, word * pIn, int fComp0, int nWords ) -{ - int w; - if ( fComp0 ) - { - if ( fComp ) - { - for ( w = 0; w < nWords; w++ ) - if ( ~pIn[w] & ~pOut[w] ) - return 1; - } - else - { - for ( w = 0; w < nWords; w++ ) - if ( ~pIn[w] & pOut[w] ) - return 1; - } - } - else - { - if ( fComp ) - { - for ( w = 0; w < nWords; w++ ) - if ( pIn[w] & ~pOut[w] ) - return 1; - } - else - { - for ( w = 0; w < nWords; w++ ) - if ( pIn[w] & pOut[w] ) - return 1; - } - } - return 0; -} - -inline int Abc_TtIntersectTwo( word * pOut, int fComp, word * pIn0, int fComp0, word * pIn1, int fComp1, int nWords ) -{ - int w; - if ( fComp0 && fComp1 ) - { - if ( fComp ) - { - for ( w = 0; w < nWords; w++ ) - if ( ~pIn0[w] & ~pIn1[w] & ~pOut[w] ) - return 1; - } - else - { - for ( w = 0; w < nWords; w++ ) - if ( ~pIn0[w] & ~pIn1[w] & pOut[w] ) - return 1; - } - } - else if ( fComp0 ) - { - if ( fComp ) - { - for ( w = 0; w < nWords; w++ ) - if ( ~pIn0[w] & pIn1[w] & ~pOut[w] ) - return 1; - } - else - { - for ( w = 0; w < nWords; w++ ) - if ( ~pIn0[w] & pIn1[w] & pOut[w] ) - return 1; - } - } - else if ( fComp1 ) - { - if ( fComp ) - { - for ( w = 0; w < nWords; w++ ) - if ( pIn0[w] & ~pIn1[w] & ~pOut[w] ) - return 1; - } - else - { - for ( w = 0; w < nWords; w++ ) - if ( pIn0[w] & ~pIn1[w] & pOut[w] ) - return 1; - } - } - else - { - if ( fComp ) - { - for ( w = 0; w < nWords; w++ ) - if ( pIn0[w] & pIn1[w] & ~pOut[w] ) - return 1; - } - else - { - for ( w = 0; w < nWords; w++ ) - if ( pIn0[w] & pIn1[w] & pOut[w] ) - return 1; - } - } - return 0; -} - -inline int Abc_TtIntersectXor( word * pOut, int fComp, word * pIn0, word * pIn1, int fComp01, int nWords ) -{ - int w; - if ( fComp01 ) - { - if ( fComp ) - { - for ( w = 0; w < nWords; w++ ) - if ( ~(pIn0[w] ^ pIn1[w]) & ~pOut[w] ) - return 1; - } - else - { - for ( w = 0; w < nWords; w++ ) - if ( ~(pIn0[w] ^ pIn1[w]) & pOut[w] ) - return 1; - } - } - else - { - if ( fComp ) - { - for ( w = 0; w < nWords; w++ ) - if ( (pIn0[w] ^ pIn1[w]) & ~pOut[w] ) - return 1; - } - else - { - for ( w = 0; w < nWords; w++ ) - if ( (pIn0[w] ^ pIn1[w]) & pOut[w] ) - return 1; - } - } - return 0; -} - -inline word Abc_Tt6Stretch( word t, int nVars ) -{ - assert( nVars >= 0 ); - if ( nVars == 0 ) - nVars++, t = (t & 0x1) | ((t & 0x1) << 1); - if ( nVars == 1 ) - nVars++, t = (t & 0x3) | ((t & 0x3) << 2); - if ( nVars == 2 ) - nVars++, t = (t & 0xF) | ((t & 0xF) << 4); - if ( nVars == 3 ) - nVars++, t = (t & 0xFF) | ((t & 0xFF) << 8); - if ( nVars == 4 ) - nVars++, t = (t & 0xFFFF) | ((t & 0xFFFF) << 16); - if ( nVars == 5 ) - nVars++, t = (t & 0xFFFFFFFF) | ((t & 0xFFFFFFFF) << 32); - assert( nVars == 6 ); - return t; -} - -} /* abcresub */ diff --git a/lib/abcresub/abcresub/vec_int.hpp b/lib/abcresub/abcresub/vec_int.hpp deleted file mode 100644 index de8868893..000000000 --- a/lib/abcresub/abcresub/vec_int.hpp +++ /dev/null @@ -1,203 +0,0 @@ -/*! - \file vec_int.hpp - \brief Extracted from ABC - https://github.com/berkeley-abc/abc - - \author Alan Mishchenko (UC Berkeley) -*/ - -#pragma once - -namespace abcresub -{ - -typedef struct Vec_Int_t_ Vec_Int_t; - -struct Vec_Int_t_ -{ - int nCap; - int nSize; - int * pArray; -}; - -#define Vec_IntForEachEntry( vVec, Entry, i ) \ - for ( i = 0; (i < Vec_IntSize(vVec)) && (((Entry) = Vec_IntEntry(vVec, i)), 1); i++ ) -#define Vec_IntForEachEntryStop( vVec, Entry, i, Stop ) \ - for ( i = 0; (i < Stop) && (((Entry) = Vec_IntEntry(vVec, i)), 1); i++ ) -#define Vec_IntForEachEntryDouble( vVec, Entry1, Entry2, i ) \ - for ( i = 0; (i+1 < Vec_IntSize(vVec)) && (((Entry1) = Vec_IntEntry(vVec, i)), 1) && (((Entry2) = Vec_IntEntry(vVec, i+1)), 1); i += 2 ) -#define Vec_IntForEachEntryTwo( vVec1, vVec2, Entry1, Entry2, i ) \ - for ( i = 0; (i < Vec_IntSize(vVec1)) && (((Entry1) = Vec_IntEntry(vVec1, i)), 1) && (((Entry2) = Vec_IntEntry(vVec2, i)), 1); i++ ) -#define Vec_IntForEachEntryTwoStart( vVec1, vVec2, Entry1, Entry2, i, Start ) \ - for ( i = Start; (i < Vec_IntSize(vVec1)) && (((Entry1) = Vec_IntEntry(vVec1, i)), 1) && (((Entry2) = Vec_IntEntry(vVec2, i)), 1); i++ ) - -inline Vec_Int_t * Vec_IntAlloc( int nCap ) -{ - Vec_Int_t * p; - p = ABC_ALLOC( Vec_Int_t, 1 ); - if ( nCap > 0 && nCap < 16 ) - nCap = 16; - p->nSize = 0; - p->nCap = nCap; - p->pArray = p->nCap? ABC_ALLOC( int, p->nCap ) : NULL; - return p; -} - -inline Vec_Int_t * Vec_IntStartFull( int nSize ) -{ - Vec_Int_t * p; - p = Vec_IntAlloc( nSize ); - p->nSize = nSize; - if ( p->pArray ) memset( p->pArray, 0xff, sizeof(int) * (size_t)nSize ); - return p; -} - -inline void Vec_IntWriteEntry( Vec_Int_t * p, int i, int Entry ) -{ - assert( i >= 0 && i < p->nSize ); - p->pArray[i] = Entry; -} - -inline void Vec_IntClear( Vec_Int_t * p ) -{ - p->nSize = 0; -} - -inline void Vec_IntErase( Vec_Int_t * p ) -{ - ABC_FREE( p->pArray ); - p->nSize = 0; - p->nCap = 0; -} - -inline void Vec_IntFree( Vec_Int_t * p ) -{ - ABC_FREE( p->pArray ); - ABC_FREE( p ); -} - -inline int * Vec_IntArray( Vec_Int_t * p ) -{ - return p->pArray; -} - -inline int Vec_IntSize( Vec_Int_t * p ) -{ - return p->nSize; -} - -inline int Vec_IntEntry( Vec_Int_t * p, int i ) -{ - assert( i >= 0 && i < p->nSize ); - return p->pArray[i]; -} - -inline int Vec_IntEntryLast( Vec_Int_t * p ) -{ - assert( p->nSize > 0 ); - return p->pArray[p->nSize-1]; -} - -inline void Vec_IntGrow( Vec_Int_t * p, int nCapMin ) -{ - if ( p->nCap >= nCapMin ) - return; - p->pArray = ABC_REALLOC( int, p->pArray, nCapMin ); - assert( p->pArray ); - p->nCap = nCapMin; -} - -inline void Vec_IntShrink( Vec_Int_t * p, int nSizeNew ) -{ - assert( p->nSize >= nSizeNew ); - p->nSize = nSizeNew; -} - -inline void Vec_IntPush( Vec_Int_t * p, int Entry ) -{ - if ( p->nSize == p->nCap ) - { - if ( p->nCap < 16 ) - Vec_IntGrow( p, 16 ); - else - Vec_IntGrow( p, 2 * p->nCap ); - } - p->pArray[p->nSize++] = Entry; -} - -inline void Vec_IntPushTwo( Vec_Int_t * p, int Entry1, int Entry2 ) -{ - Vec_IntPush( p, Entry1 ); - Vec_IntPush( p, Entry2 ); -} - -inline void Vec_IntPushArray( Vec_Int_t * p, int * pEntries, int nEntries ) -{ - int i; - for ( i = 0; i < nEntries; i++ ) - Vec_IntPush( p, pEntries[i] ); -} - -inline int Vec_IntTwoFindCommon( Vec_Int_t * vArr1, Vec_Int_t * vArr2, Vec_Int_t * vArr ) -{ - int * pBeg1 = vArr1->pArray; - int * pBeg2 = vArr2->pArray; - int * pEnd1 = vArr1->pArray + vArr1->nSize; - int * pEnd2 = vArr2->pArray + vArr2->nSize; - Vec_IntClear( vArr ); - while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 ) - { - if ( *pBeg1 == *pBeg2 ) - Vec_IntPush( vArr, *pBeg1 ), pBeg1++, pBeg2++; - else if ( *pBeg1 < *pBeg2 ) - pBeg1++; - else - pBeg2++; - } - return Vec_IntSize(vArr); -} - -inline Vec_Int_t * Vec_IntDup( Vec_Int_t * pVec ) -{ - Vec_Int_t * p; - p = ABC_ALLOC( Vec_Int_t, 1 ); - p->nSize = pVec->nSize; - p->nCap = pVec->nSize; - p->pArray = p->nCap? ABC_ALLOC( int, p->nCap ) : NULL; - memcpy( p->pArray, pVec->pArray, sizeof(int) * (size_t)pVec->nSize ); - return p; -} - -inline void Vec_IntAppend( Vec_Int_t * vVec1, Vec_Int_t * vVec2 ) -{ - int Entry, i; - Vec_IntForEachEntry( vVec2, Entry, i ) - Vec_IntPush( vVec1, Entry ); -} - -inline int Vec_IntFind( Vec_Int_t * p, int Entry ) -{ - int i; - for ( i = 0; i < p->nSize; i++ ) - if ( p->pArray[i] == Entry ) - return i; - return -1; -} - -inline void Vec_IntZero( Vec_Int_t * p ) -{ - p->pArray = NULL; - p->nSize = 0; - p->nCap = 0; -} - -inline void Vec_IntFill( Vec_Int_t * p, int nSize, int Fill ) -{ - int i; - Vec_IntGrow( p, nSize ); - for ( i = 0; i < nSize; i++ ) - p->pArray[i] = Fill; - p->nSize = nSize; -} - -} /* namespace abcresub */ diff --git a/lib/abcresub/abcresub/vec_ptr.hpp b/lib/abcresub/abcresub/vec_ptr.hpp deleted file mode 100644 index 6d2997b14..000000000 --- a/lib/abcresub/abcresub/vec_ptr.hpp +++ /dev/null @@ -1,101 +0,0 @@ -/*! - \file vec_ptr.hpp - \brief Extracted from ABC - https://github.com/berkeley-abc/abc - - \author Alan Mishchenko (UC Berkeley) -*/ - -#pragma once - -namespace abcresub -{ - -typedef struct Vec_Ptr_t_ Vec_Ptr_t; - -struct Vec_Ptr_t_ -{ - int nCap; - int nSize; - void ** pArray; -}; - -#define Vec_PtrForEachEntry( Type, vVec, pEntry, i ) \ - for ( i = 0; (i < Vec_PtrSize(vVec)) && (((pEntry) = (Type)Vec_PtrEntry(vVec, i)), 1); i++ ) -#define Vec_PtrForEachEntryStart( Type, vVec, pEntry, i, Start ) \ - for ( i = Start; (i < Vec_PtrSize(vVec)) && (((pEntry) = (Type)Vec_PtrEntry(vVec, i)), 1); i++ ) - -inline Vec_Ptr_t * Vec_PtrAlloc( int nCap ) -{ - Vec_Ptr_t * p; - p = ABC_ALLOC( Vec_Ptr_t, 1 ); - if ( nCap > 0 && nCap < 8 ) - nCap = 8; - p->nSize = 0; - p->nCap = nCap; - p->pArray = p->nCap? ABC_ALLOC( void *, p->nCap ) : NULL; - return p; -} - -inline void * Vec_PtrEntry( Vec_Ptr_t * p, int i ) -{ - assert( i >= 0 && i < p->nSize ); - return p->pArray[i]; -} - -inline void Vec_PtrGrow( Vec_Ptr_t * p, int nCapMin ) -{ - if ( p->nCap >= nCapMin ) - return; - p->pArray = ABC_REALLOC( void *, p->pArray, nCapMin ); - p->nCap = nCapMin; -} - -inline void Vec_PtrClear( Vec_Ptr_t * p ) -{ - p->nSize = 0; -} - -inline void Vec_PtrErase( Vec_Ptr_t * p ) -{ - ABC_FREE( p->pArray ); - p->nSize = 0; - p->nCap = 0; -} - -inline void Vec_PtrFree( Vec_Ptr_t * p ) -{ - ABC_FREE( p->pArray ); - ABC_FREE( p ); -} - -inline void ** Vec_PtrArray( Vec_Ptr_t * p ) -{ - return p->pArray; -} - -inline int Vec_PtrSize( Vec_Ptr_t * p ) -{ - return p->nSize; -} - -inline void Vec_PtrPush( Vec_Ptr_t * p, void * Entry ) -{ - if ( p->nSize == p->nCap ) - { - if ( p->nCap < 16 ) - Vec_PtrGrow( p, 16 ); - else - Vec_PtrGrow( p, 2 * p->nCap ); - } - p->pArray[p->nSize++] = Entry; -} - -inline void Vec_PtrAppend( Vec_Ptr_t * vVec1, Vec_Ptr_t * vVec2 ) -{ - void * Entry; int i; - Vec_PtrForEachEntry( void *, vVec2, Entry, i ) - Vec_PtrPush( vVec1, Entry ); -} - -} /* abcresub */ diff --git a/lib/abcresub/abcresub/vec_wec.hpp b/lib/abcresub/abcresub/vec_wec.hpp deleted file mode 100644 index d4145daaf..000000000 --- a/lib/abcresub/abcresub/vec_wec.hpp +++ /dev/null @@ -1,100 +0,0 @@ -/*! - \file vec_wec.hpp - \brief Extracted from ABC - https://github.com/berkeley-abc/abc - - \author Alan Mishchenko (UC Berkeley) -*/ - -#pragma once - -namespace abcresub -{ - -typedef struct Vec_Wec_t_ Vec_Wec_t; -struct Vec_Wec_t_ -{ - int nCap; - int nSize; - Vec_Int_t * pArray; -}; - -#define Vec_WecForEachLevel( vGlob, vVec, i ) \ - for ( i = 0; (i < Vec_WecSize(vGlob)) && (((vVec) = Vec_WecEntry(vGlob, i)), 1); i++ ) -#define Vec_WecForEachLevelReverse( vGlob, vVec, i ) \ - for ( i = Vec_WecSize(vGlob)-1; (i >= 0) && (((vVec) = Vec_WecEntry(vGlob, i)), 1); i-- ) - -inline Vec_Wec_t * Vec_WecAlloc( int nCap ) -{ - Vec_Wec_t * p; - p = ABC_ALLOC( Vec_Wec_t, 1 ); - if ( nCap > 0 && nCap < 8 ) - nCap = 8; - p->nSize = 0; - p->nCap = nCap; - p->pArray = p->nCap? ABC_CALLOC( Vec_Int_t, p->nCap ) : NULL; - return p; -} - -inline void Vec_WecErase( Vec_Wec_t * p ) -{ - int i; - for ( i = 0; i < p->nCap; i++ ) - ABC_FREE( p->pArray[i].pArray ); - ABC_FREE( p->pArray ); - p->nSize = 0; - p->nCap = 0; -} - -inline void Vec_WecFree( Vec_Wec_t * p ) -{ - Vec_WecErase( p ); - ABC_FREE( p ); -} - -inline int Vec_WecSize( Vec_Wec_t * p ) -{ - return p->nSize; -} - -inline void Vec_WecGrow( Vec_Wec_t * p, int nCapMin ) -{ - if ( p->nCap >= nCapMin ) - return; - p->pArray = ABC_REALLOC( Vec_Int_t, p->pArray, nCapMin ); - memset( p->pArray + p->nCap, 0, sizeof(Vec_Int_t) * (size_t)(nCapMin - p->nCap) ); - p->nCap = nCapMin; -} - -inline void Vec_WecInit( Vec_Wec_t * p, int nSize ) -{ - Vec_WecGrow( p, nSize ); - p->nSize = nSize; -} - -inline Vec_Int_t * Vec_WecEntry( Vec_Wec_t * p, int i ) -{ - assert( i >= 0 && i < p->nSize ); - return p->pArray + i; -} - -inline void Vec_WecClear( Vec_Wec_t * p ) -{ - Vec_Int_t * vVec; - int i; - Vec_WecForEachLevel( p, vVec, i ) - Vec_IntClear( vVec ); - p->nSize = 0; -} - -inline void Vec_WecPush( Vec_Wec_t * p, int Level, int Entry ) -{ - if ( p->nSize < Level + 1 ) - { - Vec_WecGrow( p, Abc_MaxInt(2*p->nSize, Level + 1) ); - p->nSize = Level + 1; - } - Vec_IntPush( Vec_WecEntry(p, Level), Entry ); -} - -} /* namespace abcresub */ diff --git a/lib/abcresub/abcresub/vec_wrd.hpp b/lib/abcresub/abcresub/vec_wrd.hpp deleted file mode 100644 index 88b4bbed9..000000000 --- a/lib/abcresub/abcresub/vec_wrd.hpp +++ /dev/null @@ -1,105 +0,0 @@ -/*! - \file vec_wrd.hpp - \brief Extracted from ABC - https://github.com/berkeley-abc/abc - - \author Alan Mishchenko (UC Berkeley) -*/ - -#pragma once - -namespace abcresub -{ - -typedef struct Vec_Wrd_t_ Vec_Wrd_t; - -struct Vec_Wrd_t_ -{ - int nCap; - int nSize; - word * pArray; -}; - -inline Vec_Wrd_t * Vec_WrdAlloc( int nCap ) -{ - Vec_Wrd_t * p; - p = ABC_ALLOC( Vec_Wrd_t, 1 ); - if ( nCap > 0 && nCap < 16 ) - nCap = 16; - p->nSize = 0; - p->nCap = nCap; - p->pArray = p->nCap? ABC_ALLOC( word, p->nCap ) : NULL; - return p; -} - -inline void Vec_WrdErase( Vec_Wrd_t * p ) -{ - ABC_FREE( p->pArray ); - p->nSize = 0; - p->nCap = 0; -} - -inline void Vec_WrdFree( Vec_Wrd_t * p ) -{ - ABC_FREE( p->pArray ); - ABC_FREE( p ); -} - -inline word * Vec_WrdArray( Vec_Wrd_t * p ) -{ - return p->pArray; -} - -inline word Vec_WrdEntry( Vec_Wrd_t * p, int i ) -{ - assert( i >= 0 && i < p->nSize ); - return p->pArray[i]; -} - -inline word * Vec_WrdEntryP( Vec_Wrd_t * p, int i ) -{ - assert( i >= 0 && i < p->nSize ); - return p->pArray + i; -} - -inline void Vec_WrdGrow( Vec_Wrd_t * p, int nCapMin ) -{ - if ( p->nCap >= nCapMin ) - return; - p->pArray = ABC_REALLOC( word, p->pArray, nCapMin ); - assert( p->pArray ); - p->nCap = nCapMin; -} - -inline void Vec_WrdFill( Vec_Wrd_t * p, int nSize, word Fill ) -{ - int i; - Vec_WrdGrow( p, nSize ); - for ( i = 0; i < nSize; i++ ) - p->pArray[i] = Fill; - p->nSize = nSize; -} - -inline void Vec_WrdClear( Vec_Wrd_t * p ) -{ - p->nSize = 0; -} - -inline void Vec_WrdPush( Vec_Wrd_t * p, word Entry ) -{ - if ( p->nSize == p->nCap ) - { - if ( p->nCap < 16 ) - Vec_WrdGrow( p, 16 ); - else - Vec_WrdGrow( p, 2 * p->nCap ); - } - p->pArray[p->nSize++] = Entry; -} - -inline int Vec_WrdSize( Vec_Wrd_t * p ) -{ - return p->nSize; -} - -} /* namespace abcresub */ diff --git a/test/algorithms/resyn_engines/xag_resyn.cpp b/test/algorithms/resyn_engines/xag_resyn.cpp index 22a52f152..eee245835 100644 --- a/test/algorithms/resyn_engines/xag_resyn.cpp +++ b/test/algorithms/resyn_engines/xag_resyn.cpp @@ -221,14 +221,6 @@ TEST_CASE( "Synthesize XAGs for all 3-input functions", "[xag_resyn]" ) CHECK( success_counter == 254 ); CHECK( failed_counter == 2 ); - - using engine_abc_t = xag_resyn_abc; - success_counter = 0; - failed_counter = 0; - test_xag_n_input_functions( success_counter, failed_counter ); - - CHECK( success_counter == 254 ); - CHECK( failed_counter == 2 ); } TEST_CASE( "Synthesize XAGs for all 4-input functions", "[xag_resyn]" ) diff --git a/test/utils/index_list.cpp b/test/utils/index_list.cpp index 0c1ada39a..b8c16acef 100644 --- a/test/utils/index_list.cpp +++ b/test/utils/index_list.cpp @@ -47,45 +47,6 @@ TEST_CASE( "encode mig_network into mig_index_list", "[index_list]" ) CHECK( to_index_list_string( mig_il ) == "{4 | 1 << 8 | 2 << 16, 2, 4, 6, 4, 8, 10, 12}" ); } -TEST_CASE( "decode abc_index_list into xag_network", "[index_list]" ) -{ - std::vector const raw_list{ 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 2, 4, 6, 8, 12, 10, 14, 14 }; - abc_index_list xag_il( raw_list, 4u ); - - xag_network xag; - decode( xag, xag_il ); - - CHECK( xag.num_gates() == 3u ); - CHECK( xag.num_pis() == 4u ); - CHECK( xag.num_pos() == 1u ); - - const auto tt = simulate>( xag )[0]; - CHECK( tt._bits == 0x7888 ); -} - -TEST_CASE( "encode xag_network into abc_index_list", "[index_list]" ) -{ - xag_network xag; - auto const a = xag.create_pi(); - auto const b = xag.create_pi(); - auto const c = xag.create_pi(); - auto const d = xag.create_pi(); - auto const t0 = xag.create_and( a, b ); - auto const t1 = xag.create_and( c, d ); - auto const t2 = xag.create_xor( t0, t1 ); - xag.create_po( t2 ); - - abc_index_list xag_il; - encode( xag_il, xag ); - - CHECK( xag_il.num_pis() == 4u ); - CHECK( xag_il.num_pos() == 1u ); - CHECK( xag_il.num_gates() == 3u ); - CHECK( xag_il.size() == 18u ); - CHECK( xag_il.raw() == std::vector{ 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 2, 4, 6, 8, 12, 10, 14, 14 } ); - CHECK( to_index_list_string( xag_il ) == "{0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 2, 4, 6, 8, 12, 10, 14, 14}" ); -} - TEST_CASE( "decode xag_index_list into xag_network", "[index_list]" ) { std::vector const raw_list{ 4 | ( 1 << 8 ) | ( 3 << 16 ), 2, 4, 6, 8, 12, 10, 14 };