From 7a25f18c805579770a064218385cfd7050b3f3ec Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 17 Jun 2014 17:29:49 -0400 Subject: [PATCH] Documentation clean-ups. --- AUTHORS | 12 ++++++------ COPYING | 2 +- INSTALL | 7 +++++-- NEWS | 2 +- 4 files changed, 13 insertions(+), 10 deletions(-) diff --git a/AUTHORS b/AUTHORS index 6198e25a7..70baafd3c 100644 --- a/AUTHORS +++ b/AUTHORS @@ -18,17 +18,17 @@ authors of previous CVC tools is included with their distributions. CVC4 contains MiniSAT code by Niklas Een and Niklas Sorensson. -The CVC4 parser incorporates some code from ANTLR3, by Jim Idle, -Temporal Wave LLC. +The CVC4 parser incorporates some code from ANTLR3, by Jim Idle, Temporal +Wave LLC. CVC4 contains the doxygen.m4 autoconf module by Oren Ben-Kiki. CVC4 contains the pkg.m4 autoconf module by Scott James Remnant. -CVC4 contains the ax_tls.m4 autoconf module by Alan Woodland and -Diego Elio Petteno. +CVC4 contains the ax_tls.m4 autoconf module by Alan Woodland and Diego Elio +Petteno. CVC4 contains the boost.m4 autoconf module by Benoit Sigoure. -CVC4 maintainer versions contain the script autogen.sh, by the -U.S. Army Research Laboratory. +CVC4 maintainer versions contain the script autogen.sh by Christopher Sean +Morrison, and copyright U.S. Army Research Laboratory. diff --git a/COPYING b/COPYING index 4bccb1d13..102bf41f6 100644 --- a/COPYING +++ b/COPYING @@ -23,7 +23,7 @@ THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. --- Morgan Deters Thu, 02 Jan 2014 14:02:28 -0500 +-- Morgan Deters Tue, 17 Jun 2014 17:08:22 -0400 CVC4 incorporates MiniSat code, excluded from the above copyright. See src/sat/minisat. Its copyright: diff --git a/INSTALL b/INSTALL index 943d2f7e1..5768cfb34 100644 --- a/INSTALL +++ b/INSTALL @@ -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 diff --git a/NEWS b/NEWS index 4f0a96c14..f75febe02 100644 --- a/NEWS +++ b/NEWS @@ -3,7 +3,6 @@ This file contains a summary of important user-visible changes. Changes since 1.3 ================= -* Timed statistics are now properly updated even on process abort. * The LFSC proof checker has been incorporated into CVC4 sources. * By default, CVC4 builds in "production" mode (optimized, with fewer internal checks on). The common alternative is a "debug" build, which @@ -14,6 +13,7 @@ Changes since 1.3 licensing and dependences, see the README file. * Small API adjustments to Datatypes to even out the API and make it function better in Java. +* Timed statistics are now properly updated even on process abort. * Better automatic handling of output language setting when using CVC4 via API. Previously, the "automatic" language setting was sometimes (though not always) defaulting to the internal "AST" language; it -- 2.30.2