diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2021-11-01 13:59:47 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-11-01 20:59:47 +0000 |
| commit | 9cae42243a4c0be14fd72f5379ee4eb9f4bc88e9 (patch) | |
| tree | 0a9cfac9b3ec68737955d3b05c3ae69088eeaa7b /INSTALL.rst | |
| parent | 77416fa5f7cd004bbec3fb4901f47908d1e8fdd4 (diff) | |
bv: Remove layered solver. (#7455)
This commit removes the old bit-vector solver code.
Diffstat (limited to 'INSTALL.rst')
| -rw-r--r-- | INSTALL.rst | 13 |
1 files changed, 0 insertions, 13 deletions
diff --git a/INSTALL.rst b/INSTALL.rst index 8c2b67315..106948969 100644 --- a/INSTALL.rst +++ b/INSTALL.rst @@ -174,19 +174,6 @@ cvc5 with GLPK support, you are licensing cvc5 under that same license. (Usually cvc5's license is more permissive; see above discussion.) -ABC library (Improved Bit-Vector Support) -^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - -`ABC <http://www.eecs.berkeley.edu/~alanmi/abc/>`_ (A System for Sequential -Synthesis and Verification) is a library for synthesis and verification of logic -circuits. This dependency may improve performance of the eager bit-vector -solver. When enabled, the bit-blasted formula is encoded into -and-inverter-graphs (AIG) and ABC is used to simplify these AIGs. - -ABC can be installed using the ``contrib/get-abc`` script. Configure cvc5 with -``configure.sh --abc`` to build with this dependency. - - Editline library (Improved Interactive Experience) ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ |