Documentation clean-ups.

diff --git a/AUTHORS b/AUTHORS
index 6198e25a7e9e299c83822d1b66f602590d540855..70baafd3c7c4824dfa62d67b5bc09b18bfcd98bd 100644 (file)
--- 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 4bccb1d13990ec911109009fccb92de1289b6e3c..102bf41f62bada8a686a9a346927e63271a54208 100644 (file)
--- 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 <mdeters@cs.nyu.edu>  Thu, 02 Jan 2014 14:02:28 -0500
+-- Morgan Deters <mdeters@cs.nyu.edu>  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 943d2f7e1e1b87e0e65d8eb901c3f2277768ef2a..5768cfb34110efae33020ed5ee829cb8e8f4cb71 100644 (file)
--- 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 4f0a96c14abbe94accfadebeb68e1a7ea3b3a6f7..f75febe02e418ddc46378fe3a5330558aa01fb30 100644 (file)
--- 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