diff --git a/experiments/experiments.hpp b/experiments/experiments.hpp
index 37e76e9f4..ce76842d5 100644
--- a/experiments/experiments.hpp
+++ b/experiments/experiments.hpp
@@ -1,5 +1,5 @@
 /* mockturtle: C++ logic network library
- * Copyright (C) 2018-2019  EPFL
+ * Copyright (C) 2018-2021  EPFL
  *
  * Permission is hereby granted, free of charge, to any person
  * obtaining a copy of this software and associated documentation
@@ -506,10 +506,10 @@ std::string benchmark_path( std::string const& benchmark_name )
 }
 
 template<class Ntk>
-bool abc_cec( Ntk const& ntk, std::string const& benchmark )
+inline bool abc_cec_impl( Ntk const& ntk, std::string const& benchmark_fullpath )
 {
   mockturtle::write_bench( ntk, "/tmp/test.bench" );
-  std::string command = fmt::format( "abc -q \"cec -n {} /tmp/test.bench\"", benchmark_path( benchmark ) );
+  std::string command = fmt::format( "abc -q \"cec -n {} /tmp/test.bench\"", benchmark_fullpath );
 
   std::array<char, 128> buffer;
   std::string result;
@@ -537,4 +537,10 @@ bool abc_cec( Ntk const& ntk, std::string const& benchmark )
   return false;
 }
 
+template<class Ntk>
+inline bool abc_cec( Ntk const& ntk, std::string const& benchmark )
+{
+  return abc_cec_impl( ntk, benchmark_path( benchmark ) );
+}
+
 } // namespace experiments
diff --git a/include/mockturtle/algorithms/aqfp/mig_algebraic_rewriting_splitters.hpp b/include/mockturtle/algorithms/aqfp/mig_algebraic_rewriting_splitters.hpp
new file mode 100644
index 000000000..605487bfd
--- /dev/null
+++ b/include/mockturtle/algorithms/aqfp/mig_algebraic_rewriting_splitters.hpp
@@ -0,0 +1,406 @@
+/* mockturtle: C++ logic network library
+ * Copyright (C) 2018-2021  EPFL
+ *
+ * Permission is hereby granted, free of charge, to any person
+ * obtaining a copy of this software and associated documentation
+ * files (the "Software"), to deal in the Software without
+ * restriction, including without limitation the rights to use,
+ * copy, modify, merge, publish, distribute, sublicense, and/or sell
+ * copies of the Software, and to permit persons to whom the
+ * Software is furnished to do so, subject to the following
+ * conditions:
+ *
+ * The above copyright notice and this permission notice shall be
+ * included in all copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+ * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES
+ * OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+ * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT
+ * HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
+ * WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
+ * FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR
+ * OTHER DEALINGS IN THE SOFTWARE.
+ */
+
+/*!
+  \file mig_algebraic_rewriting_splitters.hpp
+  \brief MIG algebraric rewriting with fanout size limitation
+
+  \author Mathias Soeken
+  \author Eleonora Testa
+*/
+
+#pragma once
+
+#include "../../utils/stopwatch.hpp"
+#include "../../views/fanout_view.hpp"
+#include "../../views/topo_view.hpp"
+#include "../mig_algebraic_rewriting.hpp"
+
+#include <iostream>
+#include <optional>
+
+namespace mockturtle
+{
+
+namespace detail
+{
+
+template<class Ntk>
+class mig_algebraic_depth_rewriting_splitter_impl
+{
+public:
+  mig_algebraic_depth_rewriting_splitter_impl( Ntk& ntk, mig_algebraic_depth_rewriting_params const& ps, mig_algebraic_depth_rewriting_stats& st )
+      : ntk( ntk ), ps( ps ), st( st )
+  {
+  }
+
+  void run()
+  {
+    stopwatch t( st.time_total );
+
+    switch ( ps.strategy )
+    {
+    case mig_algebraic_depth_rewriting_params::dfs:
+      run_dfs();
+      break;
+    case mig_algebraic_depth_rewriting_params::selective:
+      run_selective();
+      break;
+    case mig_algebraic_depth_rewriting_params::aggressive:
+      run_aggressive();
+      break;
+    }
+  }
+
+private:
+  void run_dfs()
+  {
+    ntk.foreach_po( [this]( auto po ) {
+      const auto driver = ntk.get_node( po );
+      if ( ntk.level( driver ) < ntk.depth() )
+        return;
+      topo_view topo{ntk, po};
+      topo.foreach_node( [this]( auto n ) {
+        mark_critical_paths();
+        reduce_depth( n );
+        return true;
+      } );
+    } );
+  }
+
+  void run_selective()
+  {
+    uint32_t counter{0};
+    while ( true )
+    {
+      mark_critical_paths();
+
+      topo_view topo{ntk};
+      topo.foreach_node( [this, &counter]( auto n ) {
+        if ( ntk.fanout_size( n ) == 0 || ntk.value( n ) == 0 )
+          return;
+        if ( reduce_depth( n ) )
+        {
+          mark_critical_paths();
+        }
+        else
+        {
+          ++counter;
+        }
+      } );
+
+      if ( counter > ntk.size() )
+        break;
+    }
+  }
+
+  void run_aggressive()
+  {
+    uint32_t counter{0}, init_size{ntk.size()};
+    while ( true )
+    {
+      topo_view topo{ntk};
+      topo.foreach_node( [this, &counter]( auto n ) {
+        if ( ntk.fanout_size( n ) == 0 )
+          return;
+
+        if ( !reduce_depth( n ) )
+        {
+          ++counter;
+        }
+      } );
+
+      if ( ntk.size() > ps.overhead * init_size )
+        break;
+      if ( counter > ntk.size() )
+        break;
+    }
+  }
+
+private:
+  bool reduce_depth( node<Ntk> const& n )
+  {
+
+    if ( !ntk.is_maj( n ) )
+      return false;
+
+    if ( ntk.level( n ) == 0 )
+      return false;
+
+    /* get children of top node, ordered by node level (ascending) */
+    const auto ocs = ordered_children( n );
+
+    if ( !ntk.is_maj( ntk.get_node( ocs[2] ) ) )
+      return false;
+
+    if ( ntk.fanout_size( ntk.get_node( ocs[2] ) ) != 1 )
+      return false;
+
+    /* depth of last child must be (significantly) higher than depth of second child */
+    if ( ntk.level( ntk.get_node( ocs[2] ) ) <= ntk.level( ntk.get_node( ocs[1] ) ) + 1 )
+      return false;
+
+    /* child must have single fanout, if no area overhead is allowed */
+    if ( !ps.allow_area_increase && ntk.fanout_size( ntk.get_node( ocs[2] ) ) != 1 )
+      return false;
+
+    /* get children of last child */
+    auto ocs2 = ordered_children( ntk.get_node( ocs[2] ) );
+
+    /* depth of last grand-child must be higher than depth of second grand-child */
+    if ( ntk.level( ntk.get_node( ocs2[2] ) ) == ntk.level( ntk.get_node( ocs2[1] ) ) )
+      return false;
+
+    /* propagate inverter if necessary */
+    if ( ntk.is_complemented( ocs[2] ) )
+    {
+      ocs2[0] = !ocs2[0];
+      ocs2[1] = !ocs2[1];
+      ocs2[2] = !ocs2[2];
+    }
+
+    auto index = 0;
+
+    if ( auto cand = associativity_candidate( ocs[0], ocs[1], ocs2[0], ocs2[1], ocs2[2] ); cand )
+    {
+      const auto& [x, y, z, u, assoc] = *cand;
+
+      signal<Ntk> third;
+      if ( assoc )
+      {
+        third = u;
+      }
+      else
+        third = x;
+
+      auto h = ntk.create_maj( x, y, u );
+      auto opt = ntk.create_maj( z, third, h );
+
+      if ( ntk.fanout_size( ntk.get_node( opt ) ) < 1 ) // opt does not exists
+      {
+        if ( ( ntk.fanout_size( ntk.get_node( h ) ) == 5 ) || ( ntk.fanout_size( ntk.get_node( h ) ) >= 17 ) || ( ntk.fanout_size( ntk.get_node( h ) ) == 2 ) ) // it would mean the depth is actually increased
+        {
+          ntk.take_out_node( ntk.get_node( opt ) );
+          return true;
+        }
+      }
+
+      ntk.substitute_node( n, opt );
+      ntk.update_levels();
+      return true;
+    }
+
+    /* distributivity */
+    if ( ps.allow_area_increase )
+    {
+      auto s1 = ntk.create_maj( ocs[0], ocs[1], ocs2[0] );
+
+      auto s2 = ntk.create_maj( ocs[0], ocs[1], ocs2[1] );
+      if ( ntk.fanout_size( ntk.get_node( s2 ) ) < 1 )
+      {
+        index = ntk.node_to_index( ntk.get_node( ocs[0] ) );
+        if ( ( !ntk.is_pi( ntk.get_node( ocs[0] ) ) ) && ( index != 0 ) ) //&& ( ntk.is_on_critical_path( ntk.get_node( ocs[0] ) ) ) )
+        {
+          if ( ( ntk.fanout_size( ntk.get_node( ocs[0] ) ) == 5 ) || ( ntk.fanout_size( ntk.get_node( ocs[0] ) ) >= 17 ) || ( ntk.fanout_size( ntk.get_node( ocs[0] ) ) == 2 ) ) // it would mean the depth is actually increased
+          {
+            if ( ntk.fanout_size( ntk.get_node( s1 ) ) < 1 )
+              ntk.take_out_node( ntk.get_node( s1 ) );
+            ntk.take_out_node( ntk.get_node( s2 ) );
+            return true;
+          }
+        }
+
+        index = ntk.node_to_index( ntk.get_node( ocs[1] ) );
+        if ( ( !ntk.is_pi( ntk.get_node( ocs[1] ) ) ) && ( index != 0 ) )
+        {
+          if ( ( ntk.fanout_size( ntk.get_node( ocs[1] ) ) == 5 ) || ( ntk.fanout_size( ntk.get_node( ocs[1] ) ) >= 17 ) || ( ntk.fanout_size( ntk.get_node( ocs[1] ) ) == 2 ) ) // it would mean the depth is actually increased
+          {
+            if ( ntk.fanout_size( ntk.get_node( s1 ) ) < 1 )
+              ntk.take_out_node( ntk.get_node( s1 ) );
+            ntk.take_out_node( ntk.get_node( s2 ) );
+            return true;
+          }
+        }
+      }
+
+      auto opt = ntk.create_maj( ocs2[2], s1, s2 );
+  
+      if ( ( ntk.fanout_size( ntk.get_node( s1 ) ) == 5 ) || ( ntk.fanout_size( ntk.get_node( s1 ) ) >= 17 ) || ( ntk.fanout_size( ntk.get_node( s1 ) ) == 2 ) ) // it would mean the depth is actually increased
+      {
+        if ( ntk.fanout_size( ntk.get_node( s2 ) ) == 1 )
+          ntk.take_out_node( ntk.get_node( s2 ) );
+        if ( ntk.fanout_size( ntk.get_node( opt ) ) < 1 )
+          ntk.take_out_node( ntk.get_node( opt ) );
+        return true;
+      }
+      if ( ( ntk.fanout_size( ntk.get_node( s2 ) ) == 5 ) || ( ntk.fanout_size( ntk.get_node( s2 ) ) >= 17 ) || ( ntk.fanout_size( ntk.get_node( s2 ) ) == 2 ) ) // it would mean the depth is actually increased
+      {
+        if ( ntk.fanout_size( ntk.get_node( s1 ) ) == 1 )
+          ntk.take_out_node( ntk.get_node( s1 ) );
+        if ( ntk.fanout_size( ntk.get_node( opt ) ) < 1 )
+          ntk.take_out_node( ntk.get_node( opt ) );
+        return true;
+      }
+      if ( ( ntk.fanout_size( ntk.get_node( opt ) ) == 4 ) || ( ntk.fanout_size( ntk.get_node( opt ) ) >= 16 ) || ( ntk.fanout_size( ntk.get_node( opt ) ) == 1 ) ) // it would mean the depth is actually increased
+      {
+        if ( ntk.fanout_size( ntk.get_node( s1 ) ) == 1 )
+          ntk.take_out_node( ntk.get_node( s1 ) );
+        if ( ntk.fanout_size( ntk.get_node( s2 ) ) == 1 )
+          ntk.take_out_node( ntk.get_node( s2 ) );
+        return true;
+      }
+      ntk.substitute_node( n, opt );
+      ntk.update_levels();
+    }
+    return true;
+  }
+
+  using candidate_t = std::tuple<signal<Ntk>, signal<Ntk>, signal<Ntk>, signal<Ntk>, bool>;
+  std::optional<candidate_t> associativity_candidate( signal<Ntk> const& v, signal<Ntk> const& w, signal<Ntk> const& x, signal<Ntk> const& y, signal<Ntk> const& z ) const
+  {
+    if ( v.index == x.index )
+    {
+      return candidate_t{w, y, z, v, v.complement == x.complement};
+    }
+    if ( v.index == y.index )
+    {
+      return candidate_t{w, x, z, v, v.complement == y.complement};
+    }
+    if ( w.index == x.index )
+    {
+      return candidate_t{v, y, z, w, w.complement == x.complement};
+    }
+    if ( w.index == y.index )
+    {
+      return candidate_t{v, x, z, w, w.complement == y.complement};
+    }
+
+    return std::nullopt;
+  }
+
+  std::array<signal<Ntk>, 3> ordered_children( node<Ntk> const& n ) const
+  {
+    std::array<signal<Ntk>, 3> children;
+    ntk.foreach_fanin( n, [&children]( auto const& f, auto i ) { children[i] = f; } );
+    std::sort( children.begin(), children.end(), [this]( auto const& c1, auto const& c2 ) {
+      return ntk.level( ntk.get_node( c1 ) ) < ntk.level( ntk.get_node( c2 ) );
+    } );
+    return children;
+  }
+
+  void mark_critical_path( node<Ntk> const& n )
+  {
+    if ( ntk.is_pi( n ) || ntk.is_constant( n ) || ntk.value( n ) )
+      return;
+
+    const auto level = ntk.level( n );
+    ntk.set_value( n, 1 );
+    ntk.foreach_fanin( n, [this, level]( auto const& f ) {
+      if ( ntk.level( ntk.get_node( f ) ) == level - 1 )
+      {
+        mark_critical_path( ntk.get_node( f ) );
+      }
+    } );
+  }
+
+  void mark_critical_paths()
+  {
+    ntk.clear_values();
+    ntk.foreach_po( [this]( auto const& f ) {
+      if ( ntk.level( ntk.get_node( f ) ) == ntk.depth() )
+      {
+        mark_critical_path( ntk.get_node( f ) );
+      }
+    } );
+  }
+
+private:
+  Ntk& ntk;
+  mig_algebraic_depth_rewriting_params const& ps;
+  mig_algebraic_depth_rewriting_stats& st;
+}; // namespace detail
+
+} // namespace detail
+
+/*! \brief Majority algebraic depth rewriting.
+ *
+ * This algorithm tries to rewrite a network with majority gates for depth
+ * optimization using the associativity and distributivity rule in
+ * majority-of-3 logic.  It can be applied to networks other than MIGs, but
+ * only considers pairs of nodes which both implement the majority-of-3
+ * function.
+ *
+ * **Required network functions:**
+ * - `get_node`
+ * - `level`
+ * - `update_levels`
+ * - `create_maj`
+ * - `substitute_node`
+ * - `foreach_node`
+ * - `foreach_po`
+ * - `foreach_fanin`
+ * - `is_maj`
+ * - `clear_values`
+ * - `set_value`
+ * - `value`
+ * - `fanout_size`
+ *
+   \verbatim embed:rst
+
+  .. note::
+
+      The implementation of this algorithm was heavily inspired by an
+      implementation from Luca Amarù.
+   \endverbatim
+ */
+template<class Ntk>
+void mig_algebraic_depth_rewriting_splitters( Ntk& ntk, mig_algebraic_depth_rewriting_params const& ps = {}, mig_algebraic_depth_rewriting_stats* pst = nullptr )
+{
+  static_assert( is_network_type_v<Ntk>, "Ntk is not a network type" );
+  static_assert( has_get_node_v<Ntk>, "Ntk does not implement the get_node method" );
+  static_assert( has_level_v<Ntk>, "Ntk does not implement the level method" );
+  static_assert( has_create_maj_v<Ntk>, "Ntk does not implement the create_maj method" );
+  static_assert( has_substitute_node_v<Ntk>, "Ntk does not implement the substitute_node method" );
+  static_assert( has_update_levels_v<Ntk>, "Ntk does not implement the update_levels method" );
+  static_assert( has_foreach_node_v<Ntk>, "Ntk does not implement the foreach_node method" );
+  static_assert( has_foreach_po_v<Ntk>, "Ntk does not implement the foreach_po method" );
+  static_assert( has_foreach_fanin_v<Ntk>, "Ntk does not implement the foreach_fanin method" );
+  static_assert( has_is_maj_v<Ntk>, "Ntk does not implement the is_maj method" );
+  static_assert( has_clear_values_v<Ntk>, "Ntk does not implement the clear_values method" );
+  static_assert( has_set_value_v<Ntk>, "Ntk does not implement the set_value method" );
+  static_assert( has_value_v<Ntk>, "Ntk does not implement the value method" );
+  static_assert( has_fanout_size_v<Ntk>, "Ntk does not implement the fanout_size method" );
+
+  mig_algebraic_depth_rewriting_stats st;
+  detail::mig_algebraic_depth_rewriting_splitter_impl<Ntk> p( ntk, ps, st );
+  p.run();
+
+  if ( pst )
+  {
+    *pst = st;
+  }
+}
+
+} /* namespace mockturtle */
diff --git a/include/mockturtle/algorithms/aqfp/mig_resub_splitters.hpp b/include/mockturtle/algorithms/aqfp/mig_resub_splitters.hpp
new file mode 100644
index 000000000..e915b3818
--- /dev/null
+++ b/include/mockturtle/algorithms/aqfp/mig_resub_splitters.hpp
@@ -0,0 +1,580 @@
+/* mockturtle: C++ logic network library
+  * Copyright (C) 2018-2021  EPFL
+  *
+  * Permission is hereby granted, free of charge, to any person
+  * obtaining a copy of this software and associated documentation
+  * files (the "Software"), to deal in the Software without
+  * restriction, including without limitation the rights to use,
+  * copy, modify, merge, publish, distribute, sublicense, and/or sell
+  * copies of the Software, and to permit persons to whom the
+  * Software is furnished to do so, subject to the following
+  * conditions:
+  *
+  * The above copyright notice and this permission notice shall be
+  * included in all copies or substantial portions of the Software.
+  *
+  * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+  * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES
+  * OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+  * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT
+  * HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
+  * WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
+  * FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR
+  * OTHER DEALINGS IN THE SOFTWARE.
+  */
+
+/*!
+   \file mig_resub_splitters.hpp
+   \brief Modified MIG resubstitution to consider splitters in AQFP
+
+   \author Heinz Riener
+   \author Eleonora Testa
+ */
+
+#pragma once
+
+#include "../resubstitution.hpp"
+#include "../../networks/mig.hpp"
+#include "../../utils/truth_table_utils.hpp"
+
+#include <kitty/kitty.hpp>
+
+namespace mockturtle
+{
+
+struct mig_resub_splitters_stats
+{
+  /*! \brief Accumulated runtime for const-resub */
+  stopwatch<>::duration time_resubC{0};
+
+  /*! \brief Accumulated runtime for zero-resub */
+  stopwatch<>::duration time_resub0{0};
+
+  /*! \brief Accumulated runtime for collecting unate divisors. */
+  stopwatch<>::duration time_collect_unate_divisors{0};
+
+  /*! \brief Accumulated runtime for one-resub */
+  stopwatch<>::duration time_resub1{0};
+
+  /*! \brief Accumulated runtime for relevance resub */
+  stopwatch<>::duration time_resubR{0};
+
+  /*! \brief Number of accepted constant resubsitutions */
+  uint32_t num_const_accepts{0};
+
+  /*! \brief Number of accepted zero resubsitutions */
+  uint32_t num_div0_accepts{0};
+
+  /*! \brief Number of accepted one resubsitutions */
+  uint64_t num_div1_accepts{0};
+
+  /*! \brief Number of accepted relevance resubsitutions */
+  uint32_t num_divR_accepts{0};
+
+  void report() const
+  {
+    std::cout << "[i] kernel: mig_resub_splitters_functor\n";
+    std::cout << fmt::format( "[i]     constant-resub {:6d}                                   ({:>5.2f} secs)\n",
+                              num_const_accepts, to_seconds( time_resubC ) );
+    std::cout << fmt::format( "[i]            0-resub {:6d}                                   ({:>5.2f} secs)\n",
+                              num_div0_accepts, to_seconds( time_resub0 ) );
+    std::cout << fmt::format( "[i]            R-resub {:6d}                                   ({:>5.2f} secs)\n",
+                              num_divR_accepts, to_seconds( time_resubR ) );
+    std::cout << fmt::format( "[i]            collect unate divisors                           ({:>5.2f} secs)\n", to_seconds( time_collect_unate_divisors ) );
+    std::cout << fmt::format( "[i]            1-resub {:6d} = {:6d} MAJ                      ({:>5.2f} secs)\n",
+                              num_div1_accepts, num_div1_accepts, to_seconds( time_resub1 ) );
+    std::cout << fmt::format( "[i]            total   {:6d}\n",
+                              (num_const_accepts + num_div0_accepts + num_divR_accepts + num_div1_accepts) );
+  }
+}; /* mig_resub_splitters_stats */
+
+template<typename Ntk, typename Simulator, typename TT>
+struct mig_resub_splitters_functor
+{
+public:
+  using node = mig_network::node;
+  using signal = mig_network::signal;
+  using stats = mig_resub_splitters_stats;
+
+  struct unate_divisors
+  {
+    std::vector<signal> positive_divisors0;
+    std::vector<signal> positive_divisors1;
+    std::vector<signal> negative_divisors0;
+    std::vector<signal> negative_divisors1;
+    std::vector<signal> next_candidates;
+
+    void clear()
+    {
+      positive_divisors0.clear();
+      positive_divisors1.clear();
+      negative_divisors0.clear();
+      negative_divisors1.clear();
+      next_candidates.clear();
+    }
+  };
+
+public:
+  explicit mig_resub_splitters_functor( Ntk& ntk, Simulator const& sim, std::vector<node> const& divs, uint32_t num_divs, stats& st )
+      : ntk( ntk ), sim( sim ), divs( divs ), num_divs( num_divs ), st( st )
+  {
+  }
+
+  std::optional<signal> operator()( node const& root, TT care, uint32_t required, uint32_t max_inserts, uint32_t num_mffc, uint32_t& last_gain )
+  {
+    (void)care;
+    assert( is_const0( ~care ) );
+
+    /* consider constants */
+    auto g = call_with_stopwatch( st.time_resubC, [&]() {
+      return resub_const( root, required );
+    } );
+    if ( g )
+    {
+      ++st.num_const_accepts;
+      last_gain = num_mffc;
+      return g; /* accepted resub */
+    }
+
+    /* consider equal nodes */
+    g = call_with_stopwatch( st.time_resub0, [&]() {
+      return resub_div0( root, required );
+    } );
+    if ( g )
+    {
+      ++st.num_div0_accepts;
+      last_gain = num_mffc;
+      return g; /* accepted resub */
+    }
+
+    /* consider relevance optimization */
+    g = call_with_stopwatch( st.time_resubR, [&]() {
+      return resub_divR( root, required );
+    } );
+    if ( g )
+    {
+      ++st.num_divR_accepts;
+      last_gain = num_mffc;
+      return g; /* accepted resub */
+    }
+
+    if ( max_inserts == 0 || num_mffc == 1 )
+      return std::nullopt;
+
+    /* collect level one divisors */
+    call_with_stopwatch( st.time_collect_unate_divisors, [&]() {
+      collect_unate_divisors( root, required );
+    } );
+
+    /* consider equal nodes */
+    g = call_with_stopwatch( st.time_resub1, [&]() {
+      return resub_div1( root, required );
+    } );
+    if ( g )
+    {
+      ++st.num_div1_accepts;
+      last_gain = num_mffc - 1;
+      return g; /* accepted resub */
+    }
+
+    return std::nullopt;
+  }
+
+  std::optional<signal> resub_const( node const& root, uint32_t required ) const
+  {
+    (void)required;
+    auto const tt = sim.get_tt( ntk.make_signal( root ) );
+    if ( tt == sim.get_tt( ntk.get_constant( false ) ) )
+    {
+      return sim.get_phase( root ) ? ntk.get_constant( true ) : ntk.get_constant( false );
+    }
+    return std::nullopt;
+  }
+
+  std::optional<signal> resub_div0( node const& root, uint32_t required ) const
+  {
+    (void)required;
+    auto const tt = sim.get_tt( ntk.make_signal( root ) );
+    for ( auto i = 0u; i < num_divs; ++i )
+    {
+      auto const d = divs.at( i );
+      if ( !ntk.is_pi( d ) )
+      {
+        if ( (  ntk.fanout_size( d ) == 4 ) || (  ntk.fanout_size( d )  >= 16 ) || (  ntk.fanout_size( d )  == 1 ) ) // it would mean the depth is actually increased
+          continue;
+        auto fanout = ntk.fanout_size( root ) ;
+        if ( ( ntk.fanout_size( d ) < 4 ) && (  ntk.fanout_size( d ) + fanout  > 4 ) )
+          continue;
+        else if ( (  ntk.fanout_size( d )  < 16 ) && (  ntk.fanout_size( d )  > 4 ) && (  ntk.fanout_size( d ) + fanout  > 16 ) )
+          continue;
+      }
+
+      if ( tt != sim.get_tt( ntk.make_signal( d ) ) )
+        continue; /* next */
+
+      return ( sim.get_phase( d ) ^ sim.get_phase( root ) ) ? !ntk.make_signal( d ) : ntk.make_signal( d );
+    }
+
+    return std::nullopt;
+  }
+
+  std::optional<signal> resub_divR( node const& root, uint32_t required )
+  {
+    (void)required;
+
+    std::vector<signal> fs;
+    ntk.foreach_fanin( root, [&]( const auto& f ) {
+      fs.emplace_back( f );
+    } );
+
+    for ( auto i = 0u; i < divs.size(); ++i )
+    {
+      auto const& d0 = divs.at( i );
+
+      if ( !ntk.is_pi( d0 ) )
+      {
+        if ( (  ntk.fanout_size( d0 ) == 4 ) || (  ntk.fanout_size( d0 ) >= 16 ) || (  ntk.fanout_size( d0 )  == 1 ) ) // it would mean the depth is actually increased
+          continue;
+      }
+
+      auto const& s = ntk.make_signal( d0 );
+      auto const& tt = sim.get_tt( s );
+
+      if ( d0 == root )
+        break;
+
+      auto const tt0 = sim.get_tt( fs[0] );
+      auto const tt1 = sim.get_tt( fs[1] );
+      auto const tt2 = sim.get_tt( fs[2] );
+
+      if ( ntk.get_node( fs[0] ) != d0 && ntk.fanout_size( ntk.get_node( fs[0] ) ) == 1 && can_replace_majority_fanin( tt0, tt1, tt2, tt ) )
+      {
+        auto const b = sim.get_phase( ntk.get_node( fs[1] ) ) ? !fs[1] : fs[1];
+        auto const c = sim.get_phase( ntk.get_node( fs[2] ) ) ? !fs[2] : fs[2];
+
+        return sim.get_phase( root ) ? !ntk.create_maj( sim.get_phase( d0 ) ? !s : s, b, c ) : ntk.create_maj( sim.get_phase( d0 ) ? !s : s, b, c );
+      }
+      else if ( ntk.get_node( fs[1] ) != d0 && ntk.fanout_size( ntk.get_node( fs[1] ) ) == 1 && can_replace_majority_fanin( tt1, tt0, tt2, tt ) )
+      {
+        auto const a = sim.get_phase( ntk.get_node( fs[0] ) ) ? !fs[0] : fs[0];
+        auto const c = sim.get_phase( ntk.get_node( fs[2] ) ) ? !fs[2] : fs[2];
+
+        return sim.get_phase( root ) ? !ntk.create_maj( sim.get_phase( d0 ) ? !s : s, a, c ) : ntk.create_maj( sim.get_phase( d0 ) ? !s : s, a, c );
+      }
+      else if ( ntk.get_node( fs[2] ) != d0 && ntk.fanout_size( ntk.get_node( fs[2] ) ) == 1 && can_replace_majority_fanin( tt2, tt0, tt1, tt ) )
+      {
+        auto const a = sim.get_phase( ntk.get_node( fs[0] ) ) ? !fs[0] : fs[0];
+        auto const b = sim.get_phase( ntk.get_node( fs[1] ) ) ? !fs[1] : fs[1];
+
+        return sim.get_phase( root ) ? !ntk.create_maj( sim.get_phase( d0 ) ? !s : s, a, b ) : ntk.create_maj( sim.get_phase( d0 ) ? !s : s, a, b );
+      }
+      else if ( ntk.get_node( fs[0] ) != d0 && ntk.fanout_size( ntk.get_node( fs[0] ) ) == 1 && can_replace_majority_fanin( ~tt0, tt1, tt2, tt ) )
+      {
+        auto const b = sim.get_phase( ntk.get_node( fs[1] ) ) ? !fs[1] : fs[1];
+        auto const c = sim.get_phase( ntk.get_node( fs[2] ) ) ? !fs[2] : fs[2];
+
+        return sim.get_phase( root ) ? !ntk.create_maj( sim.get_phase( d0 ) ? s : !s, b, c ) : ntk.create_maj( sim.get_phase( d0 ) ? s : !s, b, c );
+      }
+      else if ( ntk.get_node( fs[1] ) != d0 && ntk.fanout_size( ntk.get_node( fs[1] ) ) == 1 && can_replace_majority_fanin( ~tt1, tt0, tt2, tt ) )
+      {
+        auto const a = sim.get_phase( ntk.get_node( fs[0] ) ) ? !fs[0] : fs[0];
+        auto const c = sim.get_phase( ntk.get_node( fs[2] ) ) ? !fs[2] : fs[2];
+
+        return sim.get_phase( root ) ? !ntk.create_maj( sim.get_phase( d0 ) ? s : !s, a, c ) : ntk.create_maj( sim.get_phase( d0 ) ? s : !s, a, c );
+      }
+      else if ( ntk.get_node( fs[2] ) != d0 && ntk.fanout_size( ntk.get_node( fs[2] ) ) == 1 && can_replace_majority_fanin( ~tt2, tt0, tt1, tt ) )
+      {
+        auto const a = sim.get_phase( ntk.get_node( fs[0] ) ) ? !fs[0] : fs[0];
+        auto const b = sim.get_phase( ntk.get_node( fs[1] ) ) ? !fs[1] : fs[1];
+
+        return sim.get_phase( root ) ? !ntk.create_maj( sim.get_phase( d0 ) ? s : !s, a, b ) : ntk.create_maj( sim.get_phase( d0 ) ? s : !s, a, b );
+      }
+    }
+
+    return std::nullopt;
+  }
+
+  void collect_unate_divisors( node const& root, uint32_t required )
+  {
+    udivs.clear();
+
+    auto const& tt = sim.get_tt( ntk.make_signal( root ) );
+    for ( auto i = 0u; i < num_divs; ++i )
+    {
+      auto const d0 = divs.at( i );
+      if ( ntk.level( d0 ) > required - 1 )
+        continue;
+
+      for ( auto j = i + 1; j < num_divs; ++j )
+      {
+        auto const d1 = divs.at( j );
+        if ( ntk.level( d1 ) > required - 1 )
+          continue;
+
+        auto const& tt_s0 = sim.get_tt( ntk.make_signal( d0 ) );
+        auto const& tt_s1 = sim.get_tt( ntk.make_signal( d1 ) );
+
+        /* Boolean filtering rule for MAJ-3 */
+        if ( kitty::ternary_majority( tt_s0, tt_s1, tt ) == tt )
+        {
+          udivs.positive_divisors0.emplace_back( ntk.make_signal( d0 ) );
+          udivs.positive_divisors1.emplace_back( ntk.make_signal( d1 ) );
+          continue;
+        }
+
+        if ( kitty::ternary_majority( ~tt_s0, tt_s1, tt ) == tt )
+        {
+          udivs.negative_divisors0.emplace_back( ntk.make_signal( d0 ) );
+          udivs.negative_divisors1.emplace_back( ntk.make_signal( d1 ) );
+          continue;
+        }
+
+        if ( std::find( udivs.next_candidates.begin(), udivs.next_candidates.end(), ntk.make_signal( d1 ) ) == udivs.next_candidates.end() )
+          udivs.next_candidates.emplace_back( ntk.make_signal( d1 ) );
+      }
+
+      if ( std::find( udivs.next_candidates.begin(), udivs.next_candidates.end(), ntk.make_signal( d0 ) ) == udivs.next_candidates.end() )
+        udivs.next_candidates.emplace_back( ntk.make_signal( d0 ) );
+    }
+  }
+
+  std::optional<signal> resub_div1( node const& root, uint32_t required )
+  {
+    (void)required;
+    auto const& tt = sim.get_tt( ntk.make_signal( root ) );
+
+    /* check for positive unate divisors */
+    for ( auto i = 0u; i < udivs.positive_divisors0.size(); ++i )
+    {
+      auto const s0 = udivs.positive_divisors0.at( i );
+      auto const s1 = udivs.positive_divisors1.at( i );
+
+      if ( !ntk.is_pi( ntk.get_node( s0 ) ) )
+      {
+        if ( (  ntk.fanout_size( ntk.get_node( s0 ) )  == 4 ) || ( ntk.fanout_size( ntk.get_node( s0 ) )  >= 16 ) || (  ntk.fanout_size( ntk.get_node( s0 ) )  == 1 ) ) // it would mean the depth is actually increased
+          continue;
+      }
+      if ( !ntk.is_pi( ntk.get_node( s1 ) ) )
+      {
+        if ( (  ntk.fanout_size( ntk.get_node( s1 ) ) == 4 ) || (  ntk.fanout_size( ntk.get_node( s1 ) )  >= 16 ) || (  ntk.fanout_size( ntk.get_node( s1 ) )  == 1 ) ) // it would mean the depth is actually increased
+          continue;
+      }
+
+      for ( auto j = i + 1; j < udivs.positive_divisors0.size(); ++j )
+      {
+        auto s2 = udivs.positive_divisors0.at( j );
+        if ( !ntk.is_pi( ntk.get_node( s2 ) ) )
+        {
+          if ( (  ntk.fanout_size( ntk.get_node( s2 ) )  == 4 ) || (  ntk.fanout_size( ntk.get_node( s2 ) )  >= 16 ) || (  ntk.fanout_size( ntk.get_node( s2 ) )  == 1 ) ) // it would mean the depth is actually increased
+            continue;
+        }
+
+        auto const& tt_s0 = sim.get_tt( s0 );
+        auto const& tt_s1 = sim.get_tt( s1 );
+        auto tt_s2 = sim.get_tt( s2 );
+
+        if ( kitty::ternary_majority( tt_s0, tt_s1, tt_s2 ) == tt )
+        {
+          // ++st.num_div1_maj_accepts;
+          auto const a = sim.get_phase( ntk.get_node( s0 ) ) ? !s0 : s0;
+          auto const b = sim.get_phase( ntk.get_node( s1 ) ) ? !s1 : s1;
+          auto const c = sim.get_phase( ntk.get_node( s2 ) ) ? !s2 : s2;
+          auto e = ntk.create_maj( a, b, c );
+          if ( (  ntk.fanout_size( ntk.get_node( e ) )  == 2 ) || (  ntk.fanout_size( ntk.get_node( e ) )  == 5 ) || (  ntk.fanout_size( ntk.get_node( e ) )  > 16 ) )
+          {
+            continue;
+          }
+          else
+            return sim.get_phase( root ) ? !e : e;
+        }
+
+        s2 = udivs.positive_divisors1.at( j );
+        if ( !ntk.is_pi( ntk.get_node( s2 ) ) )
+        {
+          if ( (  ntk.fanout_size( ntk.get_node( s2 ) )  == 4 ) || (  ntk.fanout_size( ntk.get_node( s2 ) ) >= 16 ) || (  ntk.fanout_size( ntk.get_node( s2 ) )  == 1 ) )
+            continue;
+        }
+        tt_s2 = sim.get_tt( s2 );
+
+        if ( kitty::ternary_majority( tt_s0, tt_s1, tt_s2 ) == tt )
+        {
+          // ++st.num_div1_maj_accepts;
+          auto const a = sim.get_phase( ntk.get_node( s0 ) ) ? !s0 : s0;
+          auto const b = sim.get_phase( ntk.get_node( s1 ) ) ? !s1 : s1;
+          auto const c = sim.get_phase( ntk.get_node( s2 ) ) ? !s2 : s2;
+          auto e = ntk.create_maj( a, b, c );
+          if ( ( ntk.fanout_size( ntk.get_node( e ) )  == 2 ) || (  ntk.fanout_size( ntk.get_node( e ) )  == 5 ) || ( ntk.fanout_size( ntk.get_node( e ) )  > 16 ) )
+            continue;
+          else
+            return sim.get_phase( root ) ? !e : e;
+        }
+      }
+    }
+
+    /* check for negative unate divisors */
+    for ( auto i = 0u; i < udivs.negative_divisors0.size(); ++i )
+    {
+      auto const s0 = udivs.negative_divisors0.at( i );
+      if ( !ntk.is_pi( ntk.get_node( s0 ) ) )
+      {
+        if ( (  ntk.fanout_size( ntk.get_node( s0 ) )  == 4 ) || ( ntk.fanout_size( ntk.get_node( s0 ) )  >= 16 ) || (  ntk.fanout_size( ntk.get_node( s0 ) )  == 1 ) ) // it would mean the depth is actually increased
+          continue;
+      }
+      auto const s1 = udivs.negative_divisors1.at( i );
+      if ( !ntk.is_pi( ntk.get_node( s1 ) ) )
+      {
+        if ( (  ntk.fanout_size( ntk.get_node( s1 ) ) == 4 ) || (  ntk.fanout_size( ntk.get_node( s1 ) )  >= 16 ) || (  ntk.fanout_size( ntk.get_node( s1 ) )  == 1 ) ) // it would mean the depth is actually increased
+          continue;
+      }
+
+      for ( auto j = i + 1; j < udivs.negative_divisors0.size(); ++j )
+      {
+        auto s2 = udivs.negative_divisors0.at( j );
+        if ( !ntk.is_pi( ntk.get_node( s2 ) ) )
+        {
+          if ( (  ntk.fanout_size( ntk.get_node( s2 ) )  == 4 ) || (  ntk.fanout_size( ntk.get_node( s2 ) ) >= 16 ) || (  ntk.fanout_size( ntk.get_node( s2 ) )  == 1 ) )
+            continue;
+        }
+
+        auto const& tt_s0 = sim.get_tt( s0 );
+        auto const& tt_s1 = sim.get_tt( s1 );
+        auto tt_s2 = sim.get_tt( s2 );
+
+        if ( kitty::ternary_majority( ~tt_s0, tt_s1, tt_s2 ) == tt )
+        {
+          // ++st.num_div1_maj_accepts;
+          auto const a = sim.get_phase( ntk.get_node( s0 ) ) ? !s0 : s0;
+          auto const b = sim.get_phase( ntk.get_node( s1 ) ) ? !s1 : s1;
+          auto const c = sim.get_phase( ntk.get_node( s2 ) ) ? !s2 : s2;
+          auto e = ntk.create_maj( !a, b, c );
+          if ( ( ntk.fanout_size( ntk.get_node( e ) )  == 2 ) || (  ntk.fanout_size( ntk.get_node( e ) )  == 5 ) || ( ntk.fanout_size( ntk.get_node( e ) )  > 16 ) )
+            continue;
+          else
+            return sim.get_phase( root ) ? !e : e;
+        }
+
+        s2 = udivs.negative_divisors1.at( j );
+        if ( !ntk.is_pi( ntk.get_node( s2 ) ) )
+        {
+          if ( (  ntk.fanout_size( ntk.get_node( s2 ) )  == 4 ) || (  ntk.fanout_size( ntk.get_node( s2 ) ) >= 16 ) || (  ntk.fanout_size( ntk.get_node( s2 ) )  == 1 ) )
+            continue;
+        }
+        tt_s2 = sim.get_tt( s2 );
+
+        if ( kitty::ternary_majority( ~tt_s0, tt_s1, tt_s2 ) == tt )
+        {
+          // ++st.num_div1_maj_accepts;
+          auto const a = sim.get_phase( ntk.get_node( s0 ) ) ? !s0 : s0;
+          auto const b = sim.get_phase( ntk.get_node( s1 ) ) ? !s1 : s1;
+          auto const c = sim.get_phase( ntk.get_node( s2 ) ) ? !s2 : s2;
+          auto e = ntk.create_maj( !a, b, c );
+          if ( ( ntk.fanout_size( ntk.get_node( e ) )  == 2 ) || (  ntk.fanout_size( ntk.get_node( e ) )  == 5 ) || ( ntk.fanout_size( ntk.get_node( e ) )  > 16 ) )
+            continue;
+          else
+            return sim.get_phase( root ) ? !e : e;
+        }
+      }
+    }
+
+    return std::nullopt;
+  }
+
+private:
+  Ntk& ntk;
+  Simulator const& sim;
+  std::vector<node> const& divs;
+  uint32_t const num_divs;
+  stats& st;
+
+  unate_divisors udivs;
+}; /* mig_resub_functor */
+
+template<typename Ntk>
+bool substitute_and_update_fn( Ntk& ntk, typename Ntk::node const& n, typename Ntk::signal const& g )
+{
+  ntk.substitute_node( n, g );
+  ntk.update_levels();
+  ntk.update_fanout();
+  return true;
+};
+
+template<class Ntk, class NodeCostFn>
+void mig_resubstitution_splitters( depth_view<Ntk, NodeCostFn>& ntk, resubstitution_params const& ps = {}, resubstitution_stats* pst = nullptr )
+{
+  static_assert( is_network_type_v<Ntk>, "Ntk is not a network type" );
+  static_assert( std::is_same_v<typename Ntk::base_type, mig_network>, "Network type is not mig_network" );
+  static_assert( has_clear_values_v<Ntk>, "Ntk does not implement the clear_values method" );
+  static_assert( has_fanout_size_v<Ntk>, "Ntk does not implement the fanout_size method" );
+  static_assert( has_foreach_fanin_v<Ntk>, "Ntk does not implement the foreach_fanin method" );
+  static_assert( has_foreach_gate_v<Ntk>, "Ntk does not implement the foreach_gate method" );
+  static_assert( has_foreach_node_v<Ntk>, "Ntk does not implement the foreach_node method" );
+  static_assert( has_get_constant_v<Ntk>, "Ntk does not implement the get_constant method" );
+  static_assert( has_get_node_v<Ntk>, "Ntk does not implement the get_node method" );
+  static_assert( has_is_complemented_v<Ntk>, "Ntk does not implement the is_complemented method" );
+  static_assert( has_is_pi_v<Ntk>, "Ntk does not implement the is_pi method" );
+  static_assert( has_make_signal_v<Ntk>, "Ntk does not implement the make_signal method" );
+  static_assert( has_set_value_v<Ntk>, "Ntk does not implement the set_value method" );
+  static_assert( has_set_visited_v<Ntk>, "Ntk does not implement the set_visited method" );
+  static_assert( has_size_v<Ntk>, "Ntk does not implement the has_size method" );
+  static_assert( has_substitute_node_v<Ntk>, "Ntk does not implement the has substitute_node method" );
+  static_assert( has_value_v<Ntk>, "Ntk does not implement the has_value method" );
+  static_assert( has_visited_v<Ntk>, "Ntk does not implement the has_visited method" );
+
+  using resub_view_t = fanout_view<depth_view<Ntk, NodeCostFn>>;
+  resub_view_t resub_view{ntk};
+
+  if ( ps.max_pis == 8 )
+  {
+    using truthtable_t = kitty::static_truth_table<8>;
+    using truthtable_dc_t = kitty::dynamic_truth_table;    
+    using functor_t = mig_resub_splitters_functor<resub_view_t, typename detail::window_simulator<resub_view_t, truthtable_t>, truthtable_dc_t>;
+    using resub_impl_t = detail::resubstitution_impl<resub_view_t, typename detail::window_based_resub_engine<resub_view_t, truthtable_t, truthtable_dc_t, functor_t>>;
+
+    resubstitution_stats st;
+    typename resub_impl_t::engine_st_t engine_st;
+    typename resub_impl_t::collector_st_t collector_st;
+
+    resub_impl_t p( resub_view, ps, st, engine_st, collector_st );
+    p.run( substitute_and_update_fn<resub_view_t> );
+
+    if ( ps.verbose )
+    {
+      st.report();
+      collector_st.report();
+      engine_st.report();
+    }
+
+    if ( pst )
+    {
+      *pst = st;
+    }
+  }
+  else
+  {
+    using truthtable_t = kitty::dynamic_truth_table;
+    using truthtable_dc_t = kitty::dynamic_truth_table;
+    using functor_t = mig_resub_splitters_functor<resub_view_t, typename detail::window_simulator<resub_view_t, truthtable_t>, truthtable_dc_t>;
+    using resub_impl_t = detail::resubstitution_impl<resub_view_t, typename detail::window_based_resub_engine<resub_view_t, truthtable_t, truthtable_dc_t, functor_t>>;
+
+    resubstitution_stats st;
+    typename resub_impl_t::engine_st_t engine_st;
+    typename resub_impl_t::collector_st_t collector_st;
+
+    resub_impl_t p( resub_view, ps, st, engine_st, collector_st );
+    p.run( substitute_and_update_fn<resub_view_t> );
+
+    if ( ps.verbose )
+    {
+      st.report();
+      collector_st.report();
+      engine_st.report();
+    }
+
+    if ( pst )
+    {
+      *pst = st;
+    }
+  }
+}
+
+} /* namespace mockturtle */
\ No newline at end of file
diff --git a/include/mockturtle/algorithms/mig_resub.hpp b/include/mockturtle/algorithms/mig_resub.hpp
index 22bf011c2..25091d365 100644
--- a/include/mockturtle/algorithms/mig_resub.hpp
+++ b/include/mockturtle/algorithms/mig_resub.hpp
@@ -39,24 +39,9 @@
 #include "resyn_engines/mig_resyn_engines.hpp"
 #include "../networks/mig.hpp"
 #include "../utils/index_list.hpp"
+#include "../utils/truth_table_utils.hpp"
 
-namespace kitty
-{
-
-/*! \brief Relevance */
-inline bool relevance( const dynamic_truth_table& tt0, const dynamic_truth_table& tt1, const dynamic_truth_table& tt2, const dynamic_truth_table& tt )
-{
-  return is_const0( ( ( tt0 ^ tt ) & ( tt1 ^ tt2 ) ) );
-}
-
-/*! \brief Relevance */
-template<uint32_t NumVars>
-inline bool relevance( const static_truth_table<NumVars>& tt0, const static_truth_table<NumVars>& tt1, const static_truth_table<NumVars>& tt2, const static_truth_table<NumVars>& tt )
-{
-  return is_const0( ( ( tt0 ^ tt ) & ( tt1 ^ tt2 ) ) );
-}
-
-} /* namespace kitty */
+#include <kitty/kitty.hpp>
 
 namespace mockturtle
 {
@@ -293,7 +278,7 @@ struct mig_enumerative_resub_functor
       auto const tt1 = sim.get_tt( fs[1] );
       auto const tt2 = sim.get_tt( fs[2] );
 
-      if ( ntk.get_node( fs[0] ) != d0 && ntk.fanout_size( ntk.get_node( fs[0] ) ) == 1 && relevance( tt0, tt1, tt2, tt ) )
+      if ( ntk.get_node( fs[0] ) != d0 && ntk.fanout_size( ntk.get_node( fs[0] ) ) == 1 && can_replace_majority_fanin( tt0, tt1, tt2, tt ) )
       {
         auto const b = sim.get_phase( ntk.get_node( fs[1] ) ) ? !fs[1] : fs[1];
         auto const c = sim.get_phase( ntk.get_node( fs[2] ) ) ? !fs[2] : fs[2];
@@ -302,7 +287,7 @@ struct mig_enumerative_resub_functor
           !ntk.create_maj( sim.get_phase( d0 ) ? !s : s, b, c ) :
            ntk.create_maj( sim.get_phase( d0 ) ? !s : s, b, c );
       }
-      else if ( ntk.get_node( fs[1] ) != d0 && ntk.fanout_size( ntk.get_node( fs[1] ) ) == 1 && relevance( tt1, tt0, tt2, tt ) )
+      else if ( ntk.get_node( fs[1] ) != d0 && ntk.fanout_size( ntk.get_node( fs[1] ) ) == 1 && can_replace_majority_fanin( tt1, tt0, tt2, tt ) )
       {
         auto const a = sim.get_phase( ntk.get_node( fs[0] ) ) ? !fs[0] : fs[0];
         auto const c = sim.get_phase( ntk.get_node( fs[2] ) ) ? !fs[2] : fs[2];
@@ -311,7 +296,7 @@ struct mig_enumerative_resub_functor
           !ntk.create_maj( sim.get_phase( d0 ) ? !s : s, a, c ) :
            ntk.create_maj( sim.get_phase( d0 ) ? !s : s, a, c );
       }
-      else if ( ntk.get_node( fs[2] ) != d0 && ntk.fanout_size( ntk.get_node( fs[2] ) ) == 1 && relevance( tt2, tt0, tt1, tt ) )
+      else if ( ntk.get_node( fs[2] ) != d0 && ntk.fanout_size( ntk.get_node( fs[2] ) ) == 1 && can_replace_majority_fanin( tt2, tt0, tt1, tt ) )
       {
         auto const a = sim.get_phase( ntk.get_node( fs[0] ) ) ? !fs[0] : fs[0];
         auto const b = sim.get_phase( ntk.get_node( fs[1] ) ) ? !fs[1] : fs[1];
@@ -320,7 +305,7 @@ struct mig_enumerative_resub_functor
           !ntk.create_maj( sim.get_phase( d0 ) ? !s : s, a, b ) :
           ntk.create_maj( sim.get_phase( d0 ) ? !s : s, a, b );
       }
-      else if ( ntk.get_node( fs[0] ) != d0 && ntk.fanout_size( ntk.get_node( fs[0] ) ) == 1 && relevance( ~tt0, tt1, tt2, tt ) )
+      else if ( ntk.get_node( fs[0] ) != d0 && ntk.fanout_size( ntk.get_node( fs[0] ) ) == 1 && can_replace_majority_fanin( ~tt0, tt1, tt2, tt ) )
       {
         auto const b = sim.get_phase( ntk.get_node( fs[1] ) ) ? !fs[1] : fs[1];
         auto const c = sim.get_phase( ntk.get_node( fs[2] ) ) ? !fs[2] : fs[2];
@@ -329,7 +314,7 @@ struct mig_enumerative_resub_functor
           !ntk.create_maj( sim.get_phase( d0 ) ? s : !s, b, c ) :
            ntk.create_maj( sim.get_phase( d0 ) ? s : !s, b, c );
       }
-      else if ( ntk.get_node( fs[1] ) != d0 && ntk.fanout_size( ntk.get_node( fs[1] ) ) == 1 && relevance( ~tt1, tt0, tt2, tt ) )
+      else if ( ntk.get_node( fs[1] ) != d0 && ntk.fanout_size( ntk.get_node( fs[1] ) ) == 1 && can_replace_majority_fanin( ~tt1, tt0, tt2, tt ) )
       {
         auto const a = sim.get_phase( ntk.get_node( fs[0] ) ) ? !fs[0] : fs[0];
         auto const c = sim.get_phase( ntk.get_node( fs[2] ) ) ? !fs[2] : fs[2];
@@ -338,7 +323,7 @@ struct mig_enumerative_resub_functor
           !ntk.create_maj( sim.get_phase( d0 ) ? s : !s, a, c ) :
            ntk.create_maj( sim.get_phase( d0 ) ? s : !s, a, c );
       }
-      else if ( ntk.get_node( fs[2] ) != d0 && ntk.fanout_size( ntk.get_node( fs[2] ) ) == 1 && relevance( ~tt2, tt0, tt1, tt ) )
+      else if ( ntk.get_node( fs[2] ) != d0 && ntk.fanout_size( ntk.get_node( fs[2] ) ) == 1 && can_replace_majority_fanin( ~tt2, tt0, tt1, tt ) )
       {
         auto const a = sim.get_phase( ntk.get_node( fs[0] ) ) ? !fs[0] : fs[0];
         auto const b = sim.get_phase( ntk.get_node( fs[1] ) ) ? !fs[1] : fs[1];
diff --git a/include/mockturtle/algorithms/resubstitution.hpp b/include/mockturtle/algorithms/resubstitution.hpp
index 7aae71b1f..f014a6c5b 100644
--- a/include/mockturtle/algorithms/resubstitution.hpp
+++ b/include/mockturtle/algorithms/resubstitution.hpp
@@ -84,9 +84,12 @@ struct resubstitution_params
   /*! \brief Use don't cares for optimization. Only used by window-based resub engine. */
   bool use_dont_cares{false};
 
-  /* \brief Window size for don't cares calculation. Only used by window-based resub engine. */
+  /*! \brief Window size for don't cares calculation. Only used by window-based resub engine. */
   uint32_t window_size{12u};
 
+  /*! \brief Whether to prevent from increasing depth. Currently only used by window-based resub engine. */
+  bool preserve_depth{false};
+
   /****** simulation-based resub engine ******/
 
   /*! \brief Whether to use pre-generated patterns stored in a file.
@@ -295,6 +298,11 @@ class default_divisor_collector
 
   bool collect_divisors( node const& root )
   {
+    auto max_depth = std::numeric_limits<uint32_t>::max();
+    if ( ps.preserve_depth )
+    {
+      max_depth = ntk.level( root ) - 1;
+    }
     /* add the leaves of the cuts to the divisors */
     divs.clear();
 
@@ -346,7 +354,7 @@ class default_divisor_collector
 
       /* if the fanout has all fanins in the set, add it */
       ntk.foreach_fanout( d, [&]( node const& p ) {
-        if ( ntk.visited( p ) == ntk.trav_id() )
+        if ( ntk.visited( p ) == ntk.trav_id() || ntk.level( p ) > max_depth )
         {
           return true; /* next fanout */
         }
@@ -517,7 +525,12 @@ class window_based_resub_engine
 
     ResubFn resub_fn( ntk, sim, divs, divs.size(), st.functor_st );
     auto res = call_with_stopwatch( st.time_compute_function, [&]() {
-      return resub_fn( n, care, std::numeric_limits<uint32_t>::max(), ps.max_inserts, potential_gain, last_gain );
+      auto max_depth = std::numeric_limits<uint32_t>::max();
+      if ( ps.preserve_depth )
+      {
+        max_depth = ntk.level( n ) - 1;
+      }
+      return resub_fn( n, care, max_depth, ps.max_inserts, potential_gain, last_gain );
     });
     if ( res )
     {
diff --git a/include/mockturtle/utils/truth_table_utils.hpp b/include/mockturtle/utils/truth_table_utils.hpp
new file mode 100644
index 000000000..eab35bcd3
--- /dev/null
+++ b/include/mockturtle/utils/truth_table_utils.hpp
@@ -0,0 +1,63 @@
+/* mockturtle: C++ logic network library
+ * Copyright (C) 2018-2021  EPFL
+ *
+ * Permission is hereby granted, free of charge, to any person
+ * obtaining a copy of this software and associated documentation
+ * files (the "Software"), to deal in the Software without
+ * restriction, including without limitation the rights to use,
+ * copy, modify, merge, publish, distribute, sublicense, and/or sell
+ * copies of the Software, and to permit persons to whom the
+ * Software is furnished to do so, subject to the following
+ * conditions:
+ *
+ * The above copyright notice and this permission notice shall be
+ * included in all copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+ * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES
+ * OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+ * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT
+ * HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
+ * WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
+ * FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR
+ * OTHER DEALINGS IN THE SOFTWARE.
+ */
+
+/*!
+  \file truth_table_utils.hpp
+  \brief Truth table manipulation utils
+
+  \author Siang-Yun Lee
+*/
+
+#pragma once
+
+#include <kitty/kitty.hpp>
+
+namespace mockturtle
+{
+
+/*! \brief Replacement rule of MAJ3
+ *
+ * Given a majority gate with fanin functions `fanin0`, `fanin1` and `fanin2`,
+ * check if the first fanin `fanin0` can be replaced by `replacement`
+ * without changing the output function of the majority gate.
+ *
+ * By the replacement rule, `<x, y, z> = <w, y, z>` if and only if
+ * `(x ^ w)(y ^ z) = 0`, i.e., `y != z` implies `w = x`.
+ *
+ * This check is used in relevance optimization in MIG resubstitution.
+ *
+ * \param fanin0 Truth table of the first fanin function; also the fanin to be replaced.
+ * \param fanin1 Truth table of the second fanin function.
+ * \param fanin2 Truth table of the third fanin function.
+ * \param replacement Truth table of the candidate to replace `fanin0`.
+ * \return `<fanin0, fanin1, fanin2> = <replacement, fanin1, fanin2>`
+ */
+template<typename TT, typename = std::enable_if_t<kitty::is_truth_table<TT>::value>>
+bool can_replace_majority_fanin( TT const& fanin0, TT const& fanin1, TT const& fanin2, TT const& replacement )
+{
+  return kitty::is_const0( ( ( fanin0 ^ replacement ) & ( fanin1 ^ fanin2 ) ) );
+}
+
+} // namespace mockturtle
\ No newline at end of file
diff --git a/include/mockturtle/views/fanout_limit_view.hpp b/include/mockturtle/views/fanout_limit_view.hpp
new file mode 100644
index 000000000..62fb24eb8
--- /dev/null
+++ b/include/mockturtle/views/fanout_limit_view.hpp
@@ -0,0 +1,293 @@
+/* mockturtle: C++ logic network library
+ * Copyright (C) 2018-2021  EPFL
+ *
+ * Permission is hereby granted, free of charge, to any person
+ * obtaining a copy of this software and associated documentation
+ * files (the "Software"), to deal in the Software without
+ * restriction, including without limitation the rights to use,
+ * copy, modify, merge, publish, distribute, sublicense, and/or sell
+ * copies of the Software, and to permit persons to whom the
+ * Software is furnished to do so, subject to the following
+ * conditions:
+ *
+ * The above copyright notice and this permission notice shall be
+ * included in all copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+ * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES
+ * OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+ * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT
+ * HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
+ * WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
+ * FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR
+ * OTHER DEALINGS IN THE SOFTWARE.
+ */
+
+/*!
+  \file fanout_limit_view.hpp
+  \brief View that replicates nodes whose fanout size exceed a limit
+  \author Heinz Riener
+*/
+
+#pragma once
+
+#include "../networks/mig.hpp"
+#include "../utils/node_map.hpp"
+
+namespace mockturtle
+{
+
+struct fanout_limit_view_params
+{
+  uint64_t fanout_limit{16};
+};
+
+
+template<typename Ntk>
+class fanout_limit_view : public Ntk
+{
+public:
+  using storage = typename Ntk::storage;
+  using node    = typename Ntk::node;
+  using signal  = typename Ntk::signal;
+
+public:
+  fanout_limit_view( fanout_limit_view_params const ps = {} )
+    : replicas( *this )
+    , ps( ps )
+  {
+    static_assert( is_network_type_v<Ntk>, "Ntk is not a network type" );
+    assert( ps.fanout_limit > 0u );
+  }
+
+  uint32_t create_po( signal const& f, std::string const& name = std::string() )
+  {
+    if ( Ntk::is_maj( Ntk::get_node( f ) ) && Ntk::fanout_size( Ntk::get_node( f ) ) + 1 > ps.fanout_limit )
+    {
+      return Ntk::create_po( replicate_node( f ), name );
+    }
+    else
+    {
+      return Ntk::create_po( f, name );
+    }
+  }
+
+  signal create_maj( signal const& a, signal const& b, signal const& c )
+  {
+    std::array<signal,3u> fanins;
+    fanins[0u] = ( Ntk::is_maj( Ntk::get_node( a ) ) && Ntk::fanout_size( Ntk::get_node( a ) ) > ps.fanout_limit - 1 ) ? replicate_node( a ) : a;
+    fanins[1u] = ( Ntk::is_maj( Ntk::get_node( b ) ) && Ntk::fanout_size( Ntk::get_node( b ) ) > ps.fanout_limit - 1 ) ? replicate_node( b ) : b;
+    fanins[2u] = ( Ntk::is_maj( Ntk::get_node( c ) ) && Ntk::fanout_size( Ntk::get_node( c ) ) > ps.fanout_limit - 1 ) ? replicate_node( c ) : c;
+    return Ntk::create_maj( fanins[0u], fanins[1u], fanins[2u] );
+  }
+
+  signal create_and( signal const& a, signal const& b )
+  {
+    return create_maj( Ntk::get_constant( false ), a, b );
+  }
+
+  signal create_nand( signal const& a, signal const& b )
+  {
+    return !create_and( a, b );
+  }
+
+  signal create_or( signal const& a, signal const& b )
+  {
+    return create_maj( Ntk::get_constant( true ), a, b );
+  }
+
+  signal create_nor( signal const& a, signal const& b )
+  {
+    return !create_or( a, b );
+  }
+
+  signal create_lt( signal const& a, signal const& b )
+  {
+    return create_and( !a, b );
+  }
+
+  signal create_le( signal const& a, signal const& b )
+  {
+    return !create_and( a, !b );
+  }
+
+  signal create_xor( signal const& a, signal const& b )
+  {
+    const auto fcompl = a.complement ^ b.complement;
+    const auto c1 = create_and( +a, -b );
+    const auto c2 = create_and( +b, -a );
+    return create_and( !c1, !c2 ) ^ !fcompl;
+  }
+
+  signal create_ite( signal cond, signal f_then, signal f_else )
+  {
+    bool f_compl{false};
+    if ( f_then.index < f_else.index )
+    {
+      std::swap( f_then, f_else );
+      cond.complement ^= 1;
+    }
+    if ( f_then.complement )
+    {
+      f_then.complement = 0;
+      f_else.complement ^= 1;
+      f_compl = true;
+    }
+
+    return create_and( !create_and( !cond, f_else ), !create_and( cond, f_then ) ) ^ !f_compl;
+  }
+
+  signal create_xor3( signal const& a, signal const& b, signal const& c )
+  {
+    const auto f = create_maj( a, !b, c );
+    const auto g = create_maj( a, b, !c );
+    return create_maj( !a, f, g );
+  }
+#pragma endregion
+
+#pragma region Create nary functions
+  signal create_nary_and( std::vector<signal> const& fs )
+  {
+    return tree_reduce( fs.begin(), fs.end(), Ntk::get_constant( true ), [this]( auto const& a, auto const& b ) { return create_and( a, b ); } );
+  }
+
+  signal create_nary_or( std::vector<signal> const& fs )
+  {
+    return tree_reduce( fs.begin(), fs.end(), Ntk::get_constant( false ), [this]( auto const& a, auto const& b ) { return create_or( a, b ); } );
+  }
+
+  signal create_nary_xor( std::vector<signal> const& fs )
+  {
+    return tree_reduce( fs.begin(), fs.end(), Ntk::get_constant( false ), [this]( auto const& a, auto const& b ) { return create_xor( a, b ); } );
+  }
+#pragma endregion
+
+#pragma region Create arbitrary functions
+  signal clone_node( mig_network const& other, node const& source, std::vector<signal> const& children )
+  {
+    (void)other;
+    (void)source;
+    assert( children.size() == 3u );
+    return create_maj( children[0u], children[1u], children[2u] );
+  }
+#pragma endregion
+
+  signal replicate_node( signal const& s )
+  {
+    return Ntk::is_complemented( s ) ? !replicate_node( Ntk::get_node( s ) ) : replicate_node( Ntk::get_node( s ) );
+  }
+
+  signal replicate_node( node const& n )
+  {
+    if ( replicas.has( n ) )
+    {
+      auto replica = replicas[n];
+      if ( Ntk::fanout_size( replica ) < ps.fanout_limit )
+      {
+        return Ntk::make_signal( replica );
+      }
+    }
+
+    std::array<signal,3u> fanins;
+    Ntk::foreach_fanin( n, [&]( signal const& f, auto index ){
+        fanins[index] = ( Ntk::is_maj( Ntk::get_node( f ) ) && Ntk::fanout_size( Ntk::get_node( f ) ) > ps.fanout_limit - 1u ) ? replicate_node( f ) : f;
+      });
+
+    auto const new_signal = create_maj_overwrite_strash( fanins[0u], fanins[1u], fanins[2u] );
+    replicas[n] = Ntk::get_node( new_signal );
+    return new_signal;
+  }
+
+  uint32_t num_gates() const
+  {
+    return Ntk::num_gates() + count_hash_overwrites;
+  }
+
+protected:
+  signal create_maj_overwrite_strash( signal a, signal b, signal c )
+  {
+    /* order inputs */
+    if ( a.index > b.index )
+    {
+      std::swap( a, b );
+      if ( b.index > c.index )
+        std::swap( b, c );
+      if ( a.index > b.index )
+        std::swap( a, b );
+    }
+    else
+    {
+      if ( b.index > c.index )
+        std::swap( b, c );
+      if ( a.index > b.index )
+        std::swap( a, b );
+    }
+
+    /* trivial cases */
+    if ( a.index == b.index )
+    {
+      return ( a.complement == b.complement ) ? a : c;
+    }
+    else if ( b.index == c.index )
+    {
+      return ( b.complement == c.complement ) ? b : a;
+    }
+
+    /*  complemented edges minimization */
+    auto node_complement = false;
+    if ( static_cast<unsigned>( a.complement ) + static_cast<unsigned>( b.complement ) +
+             static_cast<unsigned>( c.complement ) >=
+         2u )
+    {
+      node_complement = true;
+      a.complement = !a.complement;
+      b.complement = !b.complement;
+      c.complement = !c.complement;
+    }
+
+    typename storage::element_type::node_type node;
+    node.children[0] = a;
+    node.children[1] = b;
+    node.children[2] = c;
+
+    /* structural hashing */
+    if ( true )
+    {
+      const auto it = Ntk::_storage->hash.find( node );
+      if ( it != Ntk::_storage->hash.end() )
+      {
+        ++count_hash_overwrites;
+      }
+    }
+
+    const auto index = Ntk::_storage->nodes.size();
+
+    if ( index >= .9 * Ntk::_storage->nodes.capacity() )
+    {
+      Ntk::_storage->nodes.reserve( static_cast<uint64_t>( 3.1415f * index ) );
+      Ntk::_storage->hash.reserve( static_cast<uint64_t>( 3.1415f * index ) );
+    }
+
+    Ntk::_storage->nodes.push_back( node );
+    Ntk::_storage->hash[node] = index;
+
+    /* increase ref-count to children */
+    Ntk::_storage->nodes[a.index].data[0].h1++;
+    Ntk::_storage->nodes[b.index].data[0].h1++;
+    Ntk::_storage->nodes[c.index].data[0].h1++;
+
+    for ( auto const& fn : Ntk::_events->on_add )
+    {
+      fn( index );
+    }
+
+    return {index, node_complement};
+  }
+
+protected:
+  uint32_t count_hash_overwrites{0};
+  unordered_node_map<node, Ntk> replicas;
+  fanout_limit_view_params const ps;
+};
+
+} /* namespace mockturtle */
\ No newline at end of file
diff --git a/lib/kitty/kitty/affine.hpp b/lib/kitty/kitty/affine.hpp
index 0675d7eb5..868f0495a 100644
--- a/lib/kitty/kitty/affine.hpp
+++ b/lib/kitty/kitty/affine.hpp
@@ -1,5 +1,5 @@
 /* kitty: C++ truth table library
- * Copyright (C) 2017-2020  EPFL
+ * Copyright (C) 2017-2021  EPFL
  *
  * Permission is hereby granted, free of charge, to any person
  * obtaining a copy of this software and associated documentation
@@ -215,4 +215,4 @@ TT exact_affine_output_canonization( const TT& tt )
   return std::min( exact_affine_canonization_old( tt ), exact_affine_canonization_old( ~tt ) );
 }
 
-} /* namespace kitty */
+} /* namespace kitty */
\ No newline at end of file
diff --git a/lib/kitty/kitty/algorithm.hpp b/lib/kitty/kitty/algorithm.hpp
index 679621b87..663b78ed3 100644
--- a/lib/kitty/kitty/algorithm.hpp
+++ b/lib/kitty/kitty/algorithm.hpp
@@ -1,5 +1,5 @@
 /* kitty: C++ truth table library
- * Copyright (C) 2017-2020  EPFL
+ * Copyright (C) 2017-2021  EPFL
  *
  * Permission is hereby granted, free of charge, to any person
  * obtaining a copy of this software and associated documentation
@@ -379,4 +379,4 @@ inline void for_each_one_bit( const TT& tt, Fn&& op )
 {
   for_each_one_bit_naive( tt, op );
 }
-} /* namespace kitty */
+} /* namespace kitty */
\ No newline at end of file
diff --git a/lib/kitty/kitty/bit_operations.hpp b/lib/kitty/kitty/bit_operations.hpp
index ed3f162d0..44e222409 100644
--- a/lib/kitty/kitty/bit_operations.hpp
+++ b/lib/kitty/kitty/bit_operations.hpp
@@ -1,5 +1,5 @@
 /* kitty: C++ truth table library
- * Copyright (C) 2017-2020  EPFL
+ * Copyright (C) 2017-2021  EPFL
  *
  * Permission is hereby granted, free of charge, to any person
  * obtaining a copy of this software and associated documentation
@@ -376,4 +376,4 @@ int64_t find_last_bit_difference( const TT& first, const TT& second )
   return -1;
 }
 
-} // namespace kitty
+} // namespace kitty
\ No newline at end of file
diff --git a/lib/kitty/kitty/cnf.hpp b/lib/kitty/kitty/cnf.hpp
index 1359f92fd..f8a60c3b2 100644
--- a/lib/kitty/kitty/cnf.hpp
+++ b/lib/kitty/kitty/cnf.hpp
@@ -1,5 +1,5 @@
 /* kitty: C++ truth table library
- * Copyright (C) 2017-2020  EPFL
+ * Copyright (C) 2017-2021  EPFL
  *
  * Permission is hereby granted, free of charge, to any person
  * obtaining a copy of this software and associated documentation
@@ -76,4 +76,4 @@ std::vector<cube> cnf_characteristic( const TT& tt )
   return cubes;
 }
 
-} // namespace kitty
+} // namespace kitty
\ No newline at end of file
diff --git a/lib/kitty/kitty/constructors.hpp b/lib/kitty/kitty/constructors.hpp
index 23d68d5d7..784709d58 100644
--- a/lib/kitty/kitty/constructors.hpp
+++ b/lib/kitty/kitty/constructors.hpp
@@ -1,5 +1,5 @@
 /* kitty: C++ truth table library
- * Copyright (C) 2017-2020  EPFL
+ * Copyright (C) 2017-2021  EPFL
  *
  * Permission is hereby granted, free of charge, to any person
  * obtaining a copy of this software and associated documentation
@@ -972,20 +972,19 @@ inline void create_characteristic( TT& tt, const TTFrom& from )
 
 /*! \brief Creates truth table from textual expression
 
-  An expression `E` is a constant `0` or `1`, or a variable `a`, `b`, ..., `p`,
-  the negation of an expression `!E`, the conjunction of multiple expressions
-  `(E...E)`, the disjunction of multiple expressions `{E...E}`, the exclusive
-  OR of multiple expressions `[E...E]`, or the majority of three expressions
-  `<EEE>`.  Examples are `[(ab)(!ac)]` to describe if-then-else, or `!{!a!b}`
-  to describe the application of De Morgan's law to `(ab)`.  The size of the
-  truth table must fit the largest variable in the expression, e.g., if `c` is
-  the largest variable, then the truth table have at least three variables.
+  An expression `E` is a constant `0` or `1`, or a truth table `a`,
+  `b`, ..., `p` from the vector `input_tts`, the negation of an
+  expression `!E`, the conjunction of multiple expressions `(E...E)`,
+  the disjunction of multiple expressions `{E...E}`, the exclusive OR
+  of multiple expressions `[E...E]`, or the majority of three
+  expressions `<EEE>`.
 
   \param tt Truth table
   \param from Expression as string
+  \param input_tts Input truth tables assigned to a, b, ...
 */
 template<typename TT, typename = std::enable_if_t<is_complete_truth_table<TT>::value>>
-bool create_from_expression( TT& tt, const std::string& expression )
+bool create_from_expression( TT& tt, const std::string& expression, std::vector<TT> const& input_tts )
 {
   enum stack_symbols
   {
@@ -1016,8 +1015,8 @@ bool create_from_expression( TT& tt, const std::string& expression )
     default:
       if ( c >= 'a' && c <= 'p' )
       {
-        auto var = tt.construct();
-        create_nth_var( var, c - 'a' );
+        assert( input_tts.size() > uint64_t( c - 'a' ) );
+        auto var = input_tts[c - 'a'];
         push_tt( var );
       }
       else
@@ -1144,6 +1143,33 @@ bool create_from_expression( TT& tt, const std::string& expression )
   return true;
 }
 
+/*! \brief Creates truth table from textual expression
+
+  An expression `E` is a constant `0` or `1`, or a variable `a`, `b`, ..., `p`,
+  the negation of an expression `!E`, the conjunction of multiple expressions
+  `(E...E)`, the disjunction of multiple expressions `{E...E}`, the exclusive
+  OR of multiple expressions `[E...E]`, or the majority of three expressions
+  `<EEE>`.  Examples are `[(ab)(!ac)]` to describe if-then-else, or `!{!a!b}`
+  to describe the application of De Morgan's law to `(ab)`.  The size of the
+  truth table must fit the largest variable in the expression, e.g., if `c` is
+  the largest variable, then the truth table have at least three variables.
+
+  \param tt Truth table
+  \param from Expression as string
+*/
+template<typename TT, typename = std::enable_if_t<is_complete_truth_table<TT>::value>>
+bool create_from_expression( TT& tt, const std::string& expression )
+{
+  std::vector<TT> inputs_tts( tt.num_vars() );
+  for ( uint8_t i = 0u; i < tt.num_vars(); ++i )
+  {
+    auto var = tt.construct();
+    create_nth_var( var, i );
+    inputs_tts[i] = var;
+  }
+  return create_from_expression( tt, expression, inputs_tts );
+}
+
 /*! \brief Creates function where on-set corresponds to prime numbers
 
   This creates a function in which \f$f(x) = 1\f$, if and only if \f$x\f$ is
@@ -1167,4 +1193,4 @@ void create_prime( TT& tt )
   }
 }
 
-} // namespace kitty
+} // namespace kitty
\ No newline at end of file
diff --git a/lib/kitty/kitty/cube.hpp b/lib/kitty/kitty/cube.hpp
index 1dc5863f9..4819de38a 100644
--- a/lib/kitty/kitty/cube.hpp
+++ b/lib/kitty/kitty/cube.hpp
@@ -1,5 +1,5 @@
 /* kitty: C++ truth table library
- * Copyright (C) 2017-2020  EPFL
+ * Copyright (C) 2017-2021  EPFL
  *
  * Permission is hereby granted, free of charge, to any person
  * obtaining a copy of this software and associated documentation
@@ -288,4 +288,4 @@ struct hash<cube>
     return std::hash<uint64_t>{}( c._value );
   }
 };
-} // namespace kitty
+} // namespace kitty
\ No newline at end of file
diff --git a/lib/kitty/kitty/decomposition.hpp b/lib/kitty/kitty/decomposition.hpp
index 7d02433c9..54f54a291 100644
--- a/lib/kitty/kitty/decomposition.hpp
+++ b/lib/kitty/kitty/decomposition.hpp
@@ -1,5 +1,5 @@
 /* kitty: C++ truth table library
- * Copyright (C) 2017-2020  EPFL
+ * Copyright (C) 2017-2021  EPFL
  *
  * Permission is hereby granted, free of charge, to any person
  * obtaining a copy of this software and associated documentation
@@ -953,4 +953,4 @@ uint32_t ashenhurst_decomposition( const TTf& tt, const std::vector<uint32_t>& y
   return static_cast<uint32_t>( decomposition.size() );
 }
 
-} // namespace kitty
+} // namespace kitty
\ No newline at end of file
diff --git a/lib/kitty/kitty/detail/constants.hpp b/lib/kitty/kitty/detail/constants.hpp
index daf6f6716..326044a3c 100644
--- a/lib/kitty/kitty/detail/constants.hpp
+++ b/lib/kitty/kitty/detail/constants.hpp
@@ -1,5 +1,5 @@
 /* kitty: C++ truth table library
- * Copyright (C) 2017-2020  EPFL
+ * Copyright (C) 2017-2021  EPFL
  *
  * Permission is hereby granted, free of charge, to any person
  * obtaining a copy of this software and associated documentation
@@ -193,4 +193,4 @@ static constexpr int8_t log2[] = {-1, 0, 1, -1, 2, -1, -1, -1, 3, -1,
 
 } // namespace detail
 } // namespace kitty
-/*! \endcond */
+/*! \endcond */
\ No newline at end of file
diff --git a/lib/kitty/kitty/detail/linear_constants.hpp b/lib/kitty/kitty/detail/linear_constants.hpp
index ea45fb8bf..f2f41efce 100644
--- a/lib/kitty/kitty/detail/linear_constants.hpp
+++ b/lib/kitty/kitty/detail/linear_constants.hpp
@@ -1,5 +1,5 @@
 /* kitty: C++ truth table library
- * Copyright (C) 2017-2020  EPFL
+ * Copyright (C) 2017-2021  EPFL
  *
  * Permission is hereby granted, free of charge, to any person
  * obtaining a copy of this software and associated documentation
@@ -48,4 +48,4 @@ const unsigned masks_start[] = {0u, 18u, 858u};
 const unsigned masks_end[] = {18u, 858u, 141978u};
 } // namespace detail
 } // namespace kitty
-/*! \endcond */
+/*! \endcond */
\ No newline at end of file
diff --git a/lib/kitty/kitty/detail/mscfix.hpp b/lib/kitty/kitty/detail/mscfix.hpp
index 506c017a2..c6088f5b2 100644
--- a/lib/kitty/kitty/detail/mscfix.hpp
+++ b/lib/kitty/kitty/detail/mscfix.hpp
@@ -1,5 +1,5 @@
 /* kitty: C++ truth table library
- * Copyright (C) 2017-2020  EPFL
+ * Copyright (C) 2017-2021  EPFL
  *
  * Permission is hereby granted, free of charge, to any person
  * obtaining a copy of this software and associated documentation
@@ -36,4 +36,4 @@
 #ifdef _MSC_VER
 #include <intrin.h>
 #define __builtin_popcount __popcnt
-#endif
+#endif
\ No newline at end of file
diff --git a/lib/kitty/kitty/detail/shift.hpp b/lib/kitty/kitty/detail/shift.hpp
index 92769c931..65891c93f 100644
--- a/lib/kitty/kitty/detail/shift.hpp
+++ b/lib/kitty/kitty/detail/shift.hpp
@@ -1,5 +1,5 @@
 /* kitty: C++ truth table library
- * Copyright (C) 2017-2020  EPFL
+ * Copyright (C) 2017-2021  EPFL
  *
  * Permission is hereby granted, free of charge, to any person
  * obtaining a copy of this software and associated documentation
@@ -870,4 +870,4 @@ inline uint64_t compute_shift(uint64_t x, unsigned code) {
 }
 }
 
-/*! \endcond */
+/*! \endcond */
\ No newline at end of file
diff --git a/lib/kitty/kitty/detail/utils.hpp b/lib/kitty/kitty/detail/utils.hpp
index 9960baa38..c082a2135 100644
--- a/lib/kitty/kitty/detail/utils.hpp
+++ b/lib/kitty/kitty/detail/utils.hpp
@@ -1,5 +1,5 @@
 /* kitty: C++ truth table library
- * Copyright (C) 2017-2020  EPFL
+ * Copyright (C) 2017-2021  EPFL
  *
  * Permission is hereby granted, free of charge, to any person
  * obtaining a copy of this software and associated documentation
@@ -84,4 +84,4 @@ inline std::string trim_copy( std::string s )
 }
 } /* namespace detail */
 } /* namespace kitty */
-/*! \endcond */
+/*! \endcond */
\ No newline at end of file
diff --git a/lib/kitty/kitty/dynamic_truth_table.hpp b/lib/kitty/kitty/dynamic_truth_table.hpp
index 8f88875fb..9963db4bd 100644
--- a/lib/kitty/kitty/dynamic_truth_table.hpp
+++ b/lib/kitty/kitty/dynamic_truth_table.hpp
@@ -1,5 +1,5 @@
 /* kitty: C++ truth table library
- * Copyright (C) 2017-2020  EPFL
+ * Copyright (C) 2017-2021  EPFL
  *
  * Permission is hereby granted, free of charge, to any person
  * obtaining a copy of this software and associated documentation
@@ -178,4 +178,4 @@ struct is_truth_table<kitty::dynamic_truth_table> : std::true_type {};
 
 template<>
 struct is_complete_truth_table<kitty::dynamic_truth_table> : std::true_type {};
-} // namespace kitty
+} // namespace kitty
\ No newline at end of file
diff --git a/lib/kitty/kitty/enumeration.hpp b/lib/kitty/kitty/enumeration.hpp
index 868775aa9..99d7bba95 100644
--- a/lib/kitty/kitty/enumeration.hpp
+++ b/lib/kitty/kitty/enumeration.hpp
@@ -1,5 +1,5 @@
 /* kitty: C++ truth table library
- * Copyright (C) 2017-2020  EPFL
+ * Copyright (C) 2017-2021  EPFL
  *
  * Permission is hereby granted, free of charge, to any person
  * obtaining a copy of this software and associated documentation
@@ -102,4 +102,4 @@ void fuller_neighborhood_enumeration( std::vector<TT>& functions, CanonizationFn
   }
 }
 
-} /* namespace kitty */
+} /* namespace kitty */
\ No newline at end of file
diff --git a/lib/kitty/kitty/esop.hpp b/lib/kitty/kitty/esop.hpp
index 2fbd81e63..b6c4bd115 100644
--- a/lib/kitty/kitty/esop.hpp
+++ b/lib/kitty/kitty/esop.hpp
@@ -1,5 +1,5 @@
 /* kitty: C++ truth table library
- * Copyright (C) 2017-2020  EPFL
+ * Copyright (C) 2017-2021  EPFL
  *
  * Permission is hereby granted, free of charge, to any person
  * obtaining a copy of this software and associated documentation
@@ -347,4 +347,4 @@ std::vector<cube> esop_from_pprm( const TT& func )
   return cubes;
 }
 
-} // namespace kitty
+} // namespace kitty
\ No newline at end of file
diff --git a/lib/kitty/kitty/hash.hpp b/lib/kitty/kitty/hash.hpp
index d9f384156..6757c3b6b 100644
--- a/lib/kitty/kitty/hash.hpp
+++ b/lib/kitty/kitty/hash.hpp
@@ -1,5 +1,5 @@
 /* kitty: C++ truth table library
- * Copyright (C) 2017-2020  EPFL
+ * Copyright (C) 2017-2021  EPFL
  *
  * Permission is hereby granted, free of charge, to any person
  * obtaining a copy of this software and associated documentation
@@ -92,4 +92,4 @@ struct hash<static_truth_table<NumVars, true>>
   }
 };
 /*! \endcond */
-} // namespace kitty
+} // namespace kitty
\ No newline at end of file
diff --git a/lib/kitty/kitty/implicant.hpp b/lib/kitty/kitty/implicant.hpp
index 1ca4fde1d..1aea7f4bc 100644
--- a/lib/kitty/kitty/implicant.hpp
+++ b/lib/kitty/kitty/implicant.hpp
@@ -1,5 +1,5 @@
 /* kitty: C++ truth table library
- * Copyright (C) 2017-2020  EPFL
+ * Copyright (C) 2017-2021  EPFL
  *
  * Permission is hereby granted, free of charge, to any person
  * obtaining a copy of this software and associated documentation
@@ -240,4 +240,4 @@ std::vector<cube> get_prime_implicants_morreale( const TT& tt )
 
   return get_prime_implicants_morreale( get_minterms( tt ), tt.num_vars() );
 }
-} // namespace kitty
+} // namespace kitty
\ No newline at end of file
diff --git a/lib/kitty/kitty/isop.hpp b/lib/kitty/kitty/isop.hpp
index d81a15351..6104189d2 100644
--- a/lib/kitty/kitty/isop.hpp
+++ b/lib/kitty/kitty/isop.hpp
@@ -1,5 +1,5 @@
 /* kitty: C++ truth table library
- * Copyright (C) 2017-2020  EPFL
+ * Copyright (C) 2017-2021  EPFL
  *
  * Permission is hereby granted, free of charge, to any person
  * obtaining a copy of this software and associated documentation
@@ -127,4 +127,4 @@ inline std::vector<cube> isop( const TT& tt )
   return cubes;
 }
 
-} /* namespace kitty */
+} /* namespace kitty */
\ No newline at end of file
diff --git a/lib/kitty/kitty/kitty.hpp b/lib/kitty/kitty/kitty.hpp
index 1d012ca7d..b1d0d4a51 100644
--- a/lib/kitty/kitty/kitty.hpp
+++ b/lib/kitty/kitty/kitty.hpp
@@ -1,5 +1,5 @@
 /* kitty: C++ truth table library
- * Copyright (C) 2017-2020  EPFL
+ * Copyright (C) 2017-2021  EPFL
  *
  * Permission is hereby granted, free of charge, to any person
  * obtaining a copy of this software and associated documentation
@@ -64,4 +64,4 @@
           /   \
          / ___ \
          \/___\/
-*/
+*/
\ No newline at end of file
diff --git a/lib/kitty/kitty/npn.hpp b/lib/kitty/kitty/npn.hpp
index c6df745fe..e3a654e8b 100755
--- a/lib/kitty/kitty/npn.hpp
+++ b/lib/kitty/kitty/npn.hpp
@@ -1,5 +1,5 @@
 /* kitty: C++ truth table library
- * Copyright (C) 2017-2020  EPFL
+ * Copyright (C) 2017-2021  EPFL
  *
  * Permission is hereby granted, free of charge, to any person
  * obtaining a copy of this software and associated documentation
@@ -593,4 +593,4 @@ TT create_from_npn_config( const std::tuple<TT, uint32_t, std::vector<uint8_t>>&
   return res;
 }
 
-} /* namespace kitty */
+} /* namespace kitty */
\ No newline at end of file
diff --git a/lib/kitty/kitty/operations.hpp b/lib/kitty/kitty/operations.hpp
index 5c4ba139c..31a8d486e 100644
--- a/lib/kitty/kitty/operations.hpp
+++ b/lib/kitty/kitty/operations.hpp
@@ -1,5 +1,5 @@
 /* kitty: C++ truth table library
- * Copyright (C) 2017-2020  EPFL
+ * Copyright (C) 2017-2021  EPFL
  *
  * Permission is hereby granted, free of charge, to any person
  * obtaining a copy of this software and associated documentation
@@ -1191,4 +1191,4 @@ inline TT shift_with_mask( const TT& f, uint8_t mask )
   return copy;
 }
 
-} // namespace kitty
+} // namespace kitty
\ No newline at end of file
diff --git a/lib/kitty/kitty/operators.hpp b/lib/kitty/kitty/operators.hpp
index cd56fd31e..ea0144a22 100644
--- a/lib/kitty/kitty/operators.hpp
+++ b/lib/kitty/kitty/operators.hpp
@@ -1,5 +1,5 @@
 /* kitty: C++ truth table library
- * Copyright (C) 2017-2020  EPFL
+ * Copyright (C) 2017-2021  EPFL
  *
  * Permission is hereby granted, free of charge, to any person
  * obtaining a copy of this software and associated documentation
@@ -306,4 +306,4 @@ inline void operator>>=( partial_truth_table& tt, uint64_t shift )
   shift_right_inplace( tt, shift );
 }
 
-} // namespace kitty
+} // namespace kitty
\ No newline at end of file
diff --git a/lib/kitty/kitty/partial_truth_table.hpp b/lib/kitty/kitty/partial_truth_table.hpp
index 848e3ab65..8565da204 100644
--- a/lib/kitty/kitty/partial_truth_table.hpp
+++ b/lib/kitty/kitty/partial_truth_table.hpp
@@ -1,5 +1,5 @@
 /* kitty: C++ truth table library
- * Copyright (C) 2017-2020  EPFL
+ * Copyright (C) 2017-2021  EPFL
  *
  * Permission is hereby granted, free of charge, to any person
  * obtaining a copy of this software and associated documentation
@@ -288,4 +288,4 @@ struct is_truth_table<kitty::partial_truth_table> : std::true_type {};
 template<>
 struct is_complete_truth_table<kitty::partial_truth_table> : std::false_type {};
 
-} // namespace kitty
+} // namespace kitty
\ No newline at end of file
diff --git a/lib/kitty/kitty/permutation.hpp b/lib/kitty/kitty/permutation.hpp
index 0a8d0be39..3bf926405 100644
--- a/lib/kitty/kitty/permutation.hpp
+++ b/lib/kitty/kitty/permutation.hpp
@@ -1,5 +1,5 @@
 /* kitty: C++ truth table library
- * Copyright (C) 2017-2020  EPFL
+ * Copyright (C) 2017-2021  EPFL
  *
  * Permission is hereby granted, free of charge, to any person
  * obtaining a copy of this software and associated documentation
diff --git a/lib/kitty/kitty/print.hpp b/lib/kitty/kitty/print.hpp
index debbc9821..b209a5e59 100644
--- a/lib/kitty/kitty/print.hpp
+++ b/lib/kitty/kitty/print.hpp
@@ -1,5 +1,5 @@
 /* kitty: C++ truth table library
- * Copyright (C) 2017-2020  EPFL
+ * Copyright (C) 2017-2021  EPFL
  *
  * Permission is hereby granted, free of charge, to any person
  * obtaining a copy of this software and associated documentation
@@ -381,4 +381,4 @@ std::string anf_to_expression( const TT& anf )
   return terms == 1 ? expr : "[" + expr + "]";
 }
 
-} /* namespace kitty */
+} /* namespace kitty */
\ No newline at end of file
diff --git a/lib/kitty/kitty/properties.hpp b/lib/kitty/kitty/properties.hpp
index 9155e46de..df0a2bd6e 100644
--- a/lib/kitty/kitty/properties.hpp
+++ b/lib/kitty/kitty/properties.hpp
@@ -1,5 +1,5 @@
 /* kitty: C++ truth table library
- * Copyright (C) 2017-2020  EPFL
+ * Copyright (C) 2017-2021  EPFL
  *
  * Permission is hereby granted, free of charge, to any person
  * obtaining a copy of this software and associated documentation
diff --git a/lib/kitty/kitty/spectral.hpp b/lib/kitty/kitty/spectral.hpp
index bd1dbc804..4c98340fd 100644
--- a/lib/kitty/kitty/spectral.hpp
+++ b/lib/kitty/kitty/spectral.hpp
@@ -1,6 +1,6 @@
 /* kitty: C++ truth table library
- * Copyright (C) 2017-2020  EPFL
- * Copyright (C) 2017-2020  University of Victoria
+ * Copyright (C) 2017-2021  EPFL
+ * Copyright (C) 2017-2021  University of Victoria
  *
  * Permission is hereby granted, free of charge, to any person
  * obtaining a copy of this software and associated documentation
diff --git a/lib/kitty/kitty/spp.hpp b/lib/kitty/kitty/spp.hpp
index 098cd70ee..f71f27ae0 100644
--- a/lib/kitty/kitty/spp.hpp
+++ b/lib/kitty/kitty/spp.hpp
@@ -1,5 +1,5 @@
 /* kitty: C++ truth table library
- * Copyright (C) 2017-2020  EPFL
+ * Copyright (C) 2017-2021  EPFL
  *
  * Permission is hereby granted, free of charge, to any person
  * obtaining a copy of this software and associated documentation
@@ -152,4 +152,4 @@ void create_from_spp( TT& tt, const std::vector<cube>& cubes, const std::vector<
   }
 }
 
-} // namespace kitty
+} // namespace kitty
\ No newline at end of file
diff --git a/lib/kitty/kitty/static_truth_table.hpp b/lib/kitty/kitty/static_truth_table.hpp
index ce8000d6b..9637b8236 100644
--- a/lib/kitty/kitty/static_truth_table.hpp
+++ b/lib/kitty/kitty/static_truth_table.hpp
@@ -1,5 +1,5 @@
 /* kitty: C++ truth table library
- * Copyright (C) 2017-2020  EPFL
+ * Copyright (C) 2017-2021  EPFL
  *
  * Permission is hereby granted, free of charge, to any person
  * obtaining a copy of this software and associated documentation
@@ -278,4 +278,4 @@ struct is_truth_table<kitty::static_truth_table<NumVars>> : std::true_type {};
 template<uint32_t NumVars>
 struct is_complete_truth_table<kitty::static_truth_table<NumVars>> : std::true_type {};
 
-} // namespace kitty
+} // namespace kitty
\ No newline at end of file
diff --git a/lib/kitty/kitty/traits.hpp b/lib/kitty/kitty/traits.hpp
index 0d42f1284..179f38710 100644
--- a/lib/kitty/kitty/traits.hpp
+++ b/lib/kitty/kitty/traits.hpp
@@ -1,5 +1,5 @@
 /* kitty: C++ truth table library
- * Copyright (C) 2017-2020  EPFL
+ * Copyright (C) 2017-2021  EPFL
  *
  * Permission is hereby granted, free of charge, to any person
  * obtaining a copy of this software and associated documentation
@@ -43,4 +43,4 @@ struct is_truth_table : std::false_type {};
 template<class TT>
 struct is_complete_truth_table : std::false_type {};
 
-}
+}
\ No newline at end of file
diff --git a/lib/lorina/lorina/aiger.hpp b/lib/lorina/lorina/aiger.hpp
index 8b20d85a6..8bf040c83 100644
--- a/lib/lorina/lorina/aiger.hpp
+++ b/lib/lorina/lorina/aiger.hpp
@@ -28,6 +28,8 @@
   \brief Implements Aiger parser
 
   \author Heinz Riener
+  \author Mathias Soeken
+  \author Siang-Yun (Sonia) Lee
 */
 
 #pragma once
@@ -923,4 +925,4 @@ inline return_code read_aiger( const std::string& filename, const aiger_reader&
   }
 }
 
-} // namespace lorina
+} // namespace lorina
\ No newline at end of file
diff --git a/lib/lorina/lorina/bench.hpp b/lib/lorina/lorina/bench.hpp
index 475662baf..4290668c6 100644
--- a/lib/lorina/lorina/bench.hpp
+++ b/lib/lorina/lorina/bench.hpp
@@ -28,6 +28,7 @@
   \brief Implements bench parser
 
   \author Heinz Riener
+  \author Siang-Yun (Sonia) Lee
 */
 
 #pragma once
@@ -316,4 +317,4 @@ inline return_code read_bench( const std::string& filename, const bench_reader&
   }
 }
 
-} // namespace lorina
+} // namespace lorina
\ No newline at end of file
diff --git a/lib/lorina/lorina/blif.hpp b/lib/lorina/lorina/blif.hpp
index 009c2f630..c23c453d0 100644
--- a/lib/lorina/lorina/blif.hpp
+++ b/lib/lorina/lorina/blif.hpp
@@ -28,6 +28,7 @@
   \brief Implements BLIF parser
 
   \author Heinz Riener
+  \author Siang-Yun (Sonia) Lee
 */
 
 #pragma once
@@ -479,4 +480,4 @@ inline return_code read_blif( const std::string& filename, const blif_reader& re
   }
 }
 
-} // namespace lorina
+} // namespace lorina
\ No newline at end of file
diff --git a/lib/lorina/lorina/bristol.hpp b/lib/lorina/lorina/bristol.hpp
index 4f52931d0..0c77d6697 100644
--- a/lib/lorina/lorina/bristol.hpp
+++ b/lib/lorina/lorina/bristol.hpp
@@ -27,9 +27,11 @@
   \file bristol.hpp
   \brief Implements a parser for Bristol fashion
 
-  \author Heinz Riener
-
   Reference: https://homes.esat.kuleuven.be/~nsmart/MPC/
+
+  \author Heinz Riener
+  \author Mathias Soeken
+  \author Siang-Yun (Sonia) Lee
 */
 
 #pragma once
@@ -118,6 +120,7 @@ class bristol_parser
 
       assert( tokens.size() == num_input_wires + num_output_wires + 3u );
       assert( num_output_wires == 1u );
+      (void)num_output_wires;
 
       std::vector<uint32_t> inputs;
       for ( uint32_t i = 0; i < num_input_wires; ++i )
@@ -177,6 +180,7 @@ class bristol_parser
  */
 inline return_code read_bristol( std::istream& is, bristol_reader const& reader, diagnostic_engine* diag = nullptr )
 {
+  (void)diag;
   return bristol_parser( is, reader ).run();
 }
 
diff --git a/lib/lorina/lorina/common.hpp b/lib/lorina/lorina/common.hpp
index 69c2e58b7..3dd1272b4 100644
--- a/lib/lorina/lorina/common.hpp
+++ b/lib/lorina/lorina/common.hpp
@@ -41,4 +41,4 @@ enum class return_code
   parse_error,
 };
 
-} // namespace lorina
+} // namespace lorina
\ No newline at end of file
diff --git a/lib/lorina/lorina/diagnostics.hpp b/lib/lorina/lorina/diagnostics.hpp
index 23c562beb..2d905d0e2 100644
--- a/lib/lorina/lorina/diagnostics.hpp
+++ b/lib/lorina/lorina/diagnostics.hpp
@@ -160,4 +160,4 @@ class silent_diagnostic_engine : public diagnostic_engine
   }
 }; /* silent_diagnostic_engine */
 
-} // namespace lorina
+} // namespace lorina
\ No newline at end of file
diff --git a/lib/lorina/lorina/dimacs.hpp b/lib/lorina/lorina/dimacs.hpp
index f0a9c1910..2477b5287 100644
--- a/lib/lorina/lorina/dimacs.hpp
+++ b/lib/lorina/lorina/dimacs.hpp
@@ -28,6 +28,8 @@
   \brief Implements DIMACS parser
 
   \author Bruno Schmitt
+  \author Heinz Riener
+  \author Siang-Yun (Sonia) Lee
 */
 
 #pragma once
@@ -217,4 +219,4 @@ inline return_code read_dimacs( const std::string& filename, const dimacs_reader
   }
 }
 
-} // namespace lorina
+} // namespace lorina
\ No newline at end of file
diff --git a/lib/lorina/lorina/genlib.hpp b/lib/lorina/lorina/genlib.hpp
index e48d7a77e..357bf56f7 100644
--- a/lib/lorina/lorina/genlib.hpp
+++ b/lib/lorina/lorina/genlib.hpp
@@ -1,5 +1,5 @@
 /* lorina: C++ parsing library
- * Copyright (C) 2021  EPFL
+ * Copyright (C) 2018-2021  EPFL
  *
  * Permission is hereby granted, free of charge, to any person
  * obtaining a copy of this software and associated documentation
@@ -232,4 +232,4 @@ inline return_code read_genlib( const std::string& filename, const genlib_reader
   }
 }
 
-} /* lorina */
+} /* lorina */
\ No newline at end of file
diff --git a/lib/lorina/lorina/lorina.hpp b/lib/lorina/lorina/lorina.hpp
index 928a13146..7445031f7 100644
--- a/lib/lorina/lorina/lorina.hpp
+++ b/lib/lorina/lorina/lorina.hpp
@@ -39,4 +39,4 @@
 #include "dimacs.hpp"
 #include "genlib.hpp"
 #include "pla.hpp"
-#include "verilog.hpp"
+#include "verilog.hpp"
\ No newline at end of file
diff --git a/lib/lorina/lorina/pla.hpp b/lib/lorina/lorina/pla.hpp
index cdb52ce39..2270e6907 100644
--- a/lib/lorina/lorina/pla.hpp
+++ b/lib/lorina/lorina/pla.hpp
@@ -28,6 +28,7 @@
   \brief Implements pla parser
 
   \author Heinz Riener
+  \author Siang-Yun (Sonia) Lee
 */
 
 #pragma once
@@ -359,4 +360,4 @@ inline return_code read_pla( const std::string& filename, const pla_reader& read
   }
 }
 
-} // namespace lorina
+} // namespace lorina
\ No newline at end of file
diff --git a/lib/lorina/lorina/verilog.hpp b/lib/lorina/lorina/verilog.hpp
index ae126db9e..cf3b5845c 100644
--- a/lib/lorina/lorina/verilog.hpp
+++ b/lib/lorina/lorina/verilog.hpp
@@ -28,6 +28,8 @@
   \brief Implements simplistic Verilog parser
 
   \author Heinz Riener
+  \author Mathias Soeken
+  \author Siang-Yun (Sonia) Lee
 */
 
 #pragma once
@@ -1476,4 +1478,4 @@ inline return_code read_verilog( const std::string& filename, const verilog_read
   }
 }
 
-} // namespace lorina
+} // namespace lorina
\ No newline at end of file
diff --git a/lib/lorina/lorina/verilog_regex.hpp b/lib/lorina/lorina/verilog_regex.hpp
index d581d4d2a..ad6a69dc6 100644
--- a/lib/lorina/lorina/verilog_regex.hpp
+++ b/lib/lorina/lorina/verilog_regex.hpp
@@ -28,6 +28,7 @@
   \brief Regular expressions used by the Verilog parser.
 
   \author Heinz Riener
+  \author Mathias Soeken
 */
 
 #pragma once
@@ -47,4 +48,4 @@ static std::regex negated_binary_expression( R"(^~\((~)?([[:alnum:]\[\]_']+)([&|
 static std::regex const_size_range( R"(^(\d+):(\d+)$)" );
 } // namespace verilog_regex
 
-} // namespace lorina
+} // namespace lorina
\ No newline at end of file