diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-17 17:29:49 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2014-06-19 18:24:39 -0400 |
commit | 11a370348f92dfcf723b6a9318769ba3b27167e4 (patch) | |
tree | a3f997148567d7e381d0aef1234d2ee41a7231bd /INSTALL | |
parent | d6eb4cccbac83fef58e98847178c04bf1b8b0ff2 (diff) |
Documentation clean-ups.
Diffstat (limited to 'INSTALL')
-rw-r--r-- | INSTALL | 7 |
1 files changed, 5 insertions, 2 deletions
@@ -97,6 +97,7 @@ None of these is required, but can improve CVC4 as described below: Optional: SWIG 2.0.x (Simplified Wrapper and Interface Generator) Optional: CLN v1.3 or newer (Class Library for Numbers) Optional: glpk-cut-log (A fork of the GNU Linear Programming Kit) + Optional: ABC library (for improved bitvector support) Optional: GNU Readline library (for an improved interactive experience) Optional: The Boost C++ threading library (libboost_thread) Optional: CxxTest unit testing framework @@ -128,6 +129,9 @@ licensing CVC4 under that same license. (Usually CVC4's license is more permissive; see above discussion.) Please visit http://www.gnu.org/software/glpk/ for more details about GLPK. +ABC: A System for Sequential Synthesis and Verification is a library +for synthesis and verification of logic circuits. + The GNU Readline library is optionally used to provide command editing, tab completion, and history functionality at the CVC prompt (when running in interactive mode). Check your distribution for a @@ -230,8 +234,7 @@ directory, the objects will actually all appear in builds/${arch}/${build_id}. This is to allow multiple, separate builds in the same place (e.g., an assertions-enabled debugging build alongside a production build), without changing directories at the -shell. The "current" build is maintained, and you can still use -(e.g.) "make -C src/main" to rebuild objects in just one subdirectory. +shell. The "current" build is maintained until you re-configure. You can also create your own build directory inside or outside of the source tree and configure from there. All objects will then be built |