From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Wed, 8 Jan 2014 20:32:59 +0000 (-0500)
Subject: Merge branch '1.3.x'
X-Git-Tag: cvc5-1.0.0~7161
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e6fb65b8a960db1e4a21d7414f3270f03a474384;p=cvc5.git

Merge branch '1.3.x'

Conflicts:
	COPYING
	NEWS
	config/cvc4.m4
---

e6fb65b8a960db1e4a21d7414f3270f03a474384
diff --cc COPYING
index 28e814415,c02b10910..4bccb1d13
--- a/COPYING
+++ b/COPYING
@@@ -269,26 -269,6 +269,27 @@@ Please be advised that as this library 
  you choose to use the combined work, "CVC4+Readline," by building CVC4 with
  Readline, then it is also covered under the GPLv3.  If you want to make sure
  you build a version of CVC4 that uses no GPLed libraries, configure CVC4 with
- the "--bsd" option before building.  CVC4 can then be used in contexts where
- you want to license CVC4 under the (modified) BSD license.
+ the "--bsd" option before building (which is the default).  CVC4 can then be
+ used in contexts where you want to license CVC4 under the (modified) BSD
+ license.
 +
 +CVC4 sources incorporate those of the LFSC proof checker, which is
 +covered by the following license:
 +
 +  LFSC is copyright (C) 2012, 2013 The University of Iowa. All rights
 +  reserved.
 +
 +  LFSC is open-source; distribution is under the terms of the modified
 +  BSD license.
 +
 +  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT OWNERS AND CONTRIBUTORS
 +  AS IS AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
 +  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
 +  A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
 +  OWNERS OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
 +  SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
 +  LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
 +  DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
 +  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.
diff --cc NEWS
index d30c0ab77,05234ebff..f0159f4a1
--- a/NEWS
+++ b/NEWS
@@@ -4,16 -4,13 +4,16 @@@ Changes since 1.
  =================
  
  * 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
-   is much slower.  CVC4 also builds with GPL dependences by default now
-   (if those libraries are available), as this is the best-performing
-   version of CVC4.  However, the new configure option "--bsd" disables
-   these GPL dependences and builds the best-performing BSD-licenced version
-   of CVC4.
+   is much slower.  By default, CVC4 builds with no GPL'ed dependences.
+   However, this is not the best-performing version; for that, you should
+   configure with "--enable-gpl --best", which links against GPL'ed
+   libraries that improve usability and performance.  For details on
+   licensing and dependences, see the README file.
 +* Small API adjustments to Datatypes to even out the API and make it
 +  function better in Java.
  * 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
diff --cc config/cvc4.m4
index 87d984ab4,7c2f6c82d..40e2054e6
--- a/config/cvc4.m4
+++ b/config/cvc4.m4
@@@ -16,9 -24,26 +24,29 @@@ Licensing and performance options
  handle_option() {
    ac_option="$[]1"
    case $ac_option in
-     --bsd) ac_option='CVC4_BSD_LICENSED_CODE_ONLY=1' ;;
-     -enable-proofs | --enable-proofs) ac_option='--enable-proof' ;;
-     -*|*=*) ;;
+     --bsd|--disable-gpl|CVC4_BSD_LICENSED_CODE_ONLY=1)
+       if test "$CVC4_LICENSE_OPTION" = gpl; then AC_ERROR([cannot give both --bsd and --enable-gpl]); fi
+       CVC4_LICENSE_OPTION=bsd
+       ac_option="CVC4_BSD_LICENSED_CODE_ONLY=1"
+       eval $ac_option
+       ;;
+     --enable-gpl|--gpl|CVC4_BSD_LICENSED_CODE_ONLY=0)
+       if test "$CVC4_LICENSE_OPTION" = bsd; then AC_ERROR([cannot give both --bsd and --enable-gpl]); fi
+       CVC4_LICENSE_OPTION=gpl
+       ac_option="CVC4_BSD_LICENSED_CODE_ONLY=0"
+       eval $ac_option
+       ;;
+     --best)
+       # set the best configuration
+       handle_option --with-readline
+       handle_option --with-cln
+       return
+       ;;
++    -enable-proofs|--enable-proofs)
++      ac_option='--enable-proof'
++      ;;
+     -*|*=*)
+       ;;
      production|production-*|debug|debug-*|competition|competition-*)
        # regexp `\?' not supported on Mac OS X
        ac_option_build=`expr "$ac_option" : '\([[^-]]*\)-\{0,1\}'`