aig_resubstitution following cut_rewriting without cleanup_dangling in between creates NEQ circuits

[lee30sonia]

Describe the bug
What went wrong? (e.g. the optimized circuit was not equivalent to the original one, an assertion failed, etc.)

To Reproduce
Steps to reproduce the behavior:

#include <mockturtle/algorithms/aig_resub.hpp>
#include <mockturtle/algorithms/resubstitution.hpp>
#include <mockturtle/algorithms/cut_rewriting.hpp>
#include <mockturtle/algorithms/node_resynthesis/xag_npn.hpp>
#include <mockturtle/algorithms/equivalence_checking.hpp>
#include <mockturtle/algorithms/miter.hpp>
#include <mockturtle/networks/aig.hpp>
#include <mockturtle/io/aiger_reader.hpp>
#include <lorina/aiger.hpp>

using namespace mockturtle;
int main()
{
  aig_network aig;
  if ( lorina::read_aiger( "debug2_minimized.aig", aiger_reader( aig ) ) != lorina::return_code::success )
  {
    std::cerr << "Cannot read\n";
    return -1;
  }
  aig_network const aig_copy = aig.clone();

  xag_npn_resynthesis<aig_network> resyn;
  cut_rewriting_params cps;
  cps.cut_enumeration_ps.cut_size = 4;
  aig = cut_rewriting( aig, resyn, cps );
  // aig = cleanup_dangling( aig );
  std::cout << "cec after rewrite: " << *equivalence_checking( *miter<aig_network>( aig_copy, aig ) ) << "\n";

  resubstitution_params rps;
  rps.max_pis = 6;
  rps.max_inserts = 2;
  aig_resubstitution( aig, rps );
  aig = cleanup_dangling( aig );

  std::cout << "cec after resub: " << *equivalence_checking( *miter<aig_network>( aig_copy, aig ) ) << "\n";
  return 0;
}

debug2_minimized.aig.zip

Output without cleanup_dangling after cut_rewriting:

cec after rewrite: 1
cec after resub: 0

Output with cleanup_dangling after cut_rewriting:

cec after rewrite: 1
cec after resub: 1

The NEQ issue disappears by adding an additional cleanup_dangling after cut_rewriting, although this should not be needed in principle (because cut_rewriting rebuilds the network).
If we visualize the network after cut_rewriting, it appears to be the same as the original one (i.e., no optimization happened).
I suspect that there is either re-indexing or addition of dangling nodes happening during cut_rewriting, but I haven't investigated further yet.

Check list

• I have tried to run in DEBUG mode and there was no assertion failure (or the reported bug is an assertion failure).
• I have made sure that the provided code compiles and the testcase reproduces the error.
• I have minimized the testcase.

[lee30sonia]

It turns out to be because cut_rewriting uses the custom values in the network without restoring them, and resubstitution also uses these values assuming that they are initialized to 0. Adding ntk.clear_values() in the end of cut_rewriting solves the problem. I will submit a PR later.

[aletempiac]

Good to find! I see two possible policies here:

1. A method should clear values before using them. This is probably the safest option.
2. A method assumes that values are always initialized to 0 and makes sure they are also at 0 before returning. This is probably the most efficient. Nevertheless, the time to clear values is often negligible.

[lee30sonia]

Fixed by #634.