Incremental CNF construction in circuit_validator

[lee30sonia]

Only add the clauses for a node when it is used.
Invocation of push/pop is adjusted (only use it for duplicated TFO cone and when validating with non-existing circuit).
Documentation is also updated, referring to cnf_view.

I would suggest to wait until this PR is merged and also port it here. https://github.com/lsils/bill/pull/35

[coveralls]

Pull Request Test Coverage Report for Build 133198198

• 58 of 70 (82.86%) changed or added relevant lines in 2 files are covered.
• 3 unchanged lines in 1 file lost coverage.
• Overall coverage increased (+0.05%) to 79.931%

---

Changes Missing Coverage	Covered Lines	Changed/Added Lines	%
include/mockturtle/algorithms/circuit_validator.hpp	56	68	82.35%

Files with Coverage Reduction	New Missed Lines	%
include/mockturtle/algorithms/cnf.hpp	3	59.3%

Totals
Change from base Build 132216424:	0.05%
Covered Lines:	8742
Relevant Lines:	10937

---

💛 - Coveralls

[hriener]

This looks also very good to me.

Some more minor comments:

• I would prefer more descriptive names for variables (e.g., index instead of idx or inverted instead of inv, circuit instead of ckt, etc.).
• Is it possible to use initializer_lists for fanin? E.g. instead of
  circuit_validator<aig_network>::gate::fanin gi1; gi1.idx = 0; gi1.inv = true;
  you may be able to write
  circuit_validator<aig_network>::gate::fanin gi1{0,true};

[lee30sonia]

• Is it possible to use initializer_lists for fanin? E.g. instead of
  circuit_validator<aig_network>::gate::fanin gi1; gi1.idx = 0; gi1.inv = true;
  you may be able to write
  circuit_validator<aig_network>::gate::fanin gi1{0,true};

I remember this syntax is not available with some operating system / compiler ?
After all, this only appears in the example in the documentation and the test, so I think it doesn't affect too much.

[hriener]

• Is it possible to use initializer_lists for fanin? E.g. instead of
  circuit_validator<aig_network>::gate::fanin gi1; gi1.idx = 0; gi1.inv = true;
  you may be able to write
  circuit_validator<aig_network>::gate::fanin gi1{0,true};

I remember this syntax is not available with some operating system / compiler ?
After all, this only appears in the example in the documentation and the test, so I think it doesn't affect too much.

I think you confuse aggregate initialization [1] (C++20) with list initialization [2] (C++11). If list initialization works, then I would prefer it!

[1] https://en.cppreference.com/w/cpp/language/aggregate_initialization
[2] https://en.cppreference.com/w/cpp/language/list_initialization

[hriener]

Is the PR ready to be merged?

[lee30sonia]

Yes, I think so.

[hriener]

Thanks!