Circuit validator

[lee30sonia]

Validates potential circuit optimization choices with SAT by checking functional equivalence to the root node.
Supports dependency functions of more than one gate.
Supports AND2, XOR2, XOR3, MAJ.
Supports CEX randomization.
Supports ODC consideration.
Not yet supported: incremental CNF construction.

[lee30sonia]

Hmm I think checks are failing because of Z3 dependency.

[coveralls]

Pull Request Test Coverage Report for Build 123768403

• 175 of 216 (81.02%) changed or added relevant lines in 2 files are covered.
• 52 unchanged lines in 4 files lost coverage.
• Overall coverage decreased (-0.1%) to 79.857%

---

Changes Missing Coverage	Covered Lines	Changed/Added Lines	%
include/mockturtle/algorithms/cnf.hpp	28	38	73.68%
include/mockturtle/algorithms/circuit_validator.hpp	147	178	82.58%

Files with Coverage Reduction	New Missed Lines	%
include/mockturtle/views/depth_view.hpp	2	97.7%
include/mockturtle/algorithms/dsd_decomposition.hpp	3	87.5%
include/mockturtle/algorithms/balancing.hpp	14	78.13%
include/mockturtle/algorithms/cut_rewriting.hpp	33	83.5%

Totals
Change from base Build 98232457:	-0.1%
Covered Lines:	8722
Relevant Lines:	10922

---

💛 - Coveralls

[hriener]

Thank you for this contribution. The PR looks very good.

Here are a few minor comments:

• The changes to bill (bookmark, rollback, set_random_phase) should be contributed back to bill via PR. I believe that the names push and pop are more common and intuitive for bookmark and rollback.
• Some of the static_asserts in circuit_validator are disabled.
• The circuit_validator should be mentioned in the documentation and changelog of mockturtle.
• Is there a particular reason for not supporting validate with a signal argument? This may simplify some of the test cases.

[hriener]

Looks good to me. Is it ready to be merged?

The class circuit_validator should be also mentioned in mockturtle's documentation and changelog. However, it can be also added afterward.

[lee30sonia]

Looks good to me. Is it ready to be merged?

The class circuit_validator should be also mentioned in mockturtle's documentation and changelog. However, it can be also added afterward.

I am working on the documentation.

[lee30sonia]

Documentation is committed, but I'm not sure if the syntax is all good...

[hriener]

Documentation is committed, but I'm not sure if the syntax is all good...

If you run make html in your docs directory, the Makefile will locally generate the documentation on your computer in a directory called docs/build. You can then check if the markup looks correct.