From: Morgan Deters Date: Tue, 17 Dec 2013 22:14:45 +0000 (-0500) Subject: Merge branch '1.3.x' X-Git-Tag: cvc5-1.0.0~7177^2 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f411ca8ce97f488fd0db0a79abe8b4e61521ae69;p=cvc5.git Merge branch '1.3.x' Conflicts: COPYING NEWS --- f411ca8ce97f488fd0db0a79abe8b4e61521ae69 diff --cc COPYING index dd6a1582a,8babef432..4be4fdfa4 --- a/COPYING +++ b/COPYING @@@ -252,29 -255,19 +255,40 @@@ Programming Kit, available here Please be advised that as this library is covered under the GPLv3, if you choose to use the combined work, "CVC4+GLPK," by building CVC4 with - GLPK, then it is also covered under the GPLv3. If you want to make sure - you build a version of CVC4 that does not use GLPK, configure CVC4 with - "--without-glpk" before building (though that is the default). It can - then be used in contexts where you want to license CVC4 under the - (modified) BSD license. + GLPK, 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. + + CVC4 can be optionally configured to link against GNU Readline for improved + text-editing support in interactive mode. GNU Readline is available here: + + http://cnswww.cns.cwru.edu/php/chet/readline/rltop.html + + Please be advised that as this library is covered under the GPLv3, if + 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. + +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 9f17bfaa4,5c42481b4..dd1de35a4 --- a/NEWS +++ b/NEWS @@@ -4,7 -4,13 +4,14 @@@ 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. Changes since 1.2 =================