Use ABC as an external process

[atomb]

Currently, we link with ABC as a static library. This provides a tightly-integrated system with good performance. However, it leads to significant build difficulties (including the inability to build on Windows recently, due to recent additions of C++ to the ABC codebase) and hard-to-diagnose bugs.

Since we already depend on one external solver (Z3), depending on ABC as an external binary isn't a huge additional burden.

Allowing ABC to be invoked as a separate process would resolve many open bugs (including probably #54, #55, #76, #156, #233, and maybe others).

The key consideration for performance would be to support word-level interaction with ABC. We can currently do this from Cryptol using ABC's SMT-Lib interface. However, this only supports description of predicates, not arbitrary functions. To make best use of ABC's equivalence checking functionality, comparing distinct functions is sometimes useful. To support this, it seems as though a restricted subset of Verilog may be the best-supported word-level input format for ABC.

[RyanGlScott]

See #1004 (comment) for some of the aforementioned build difficulties on macOS.