-CVC4 is copyright (C) 2009 the ACSys research group at the Courant
-Institute for Mathematical Sciences, New York University.
-All rights reserved.
+CVC4 is copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016, 2017 by
+its authors and contributors (see the file AUTHORS) and their institutional
+affiliations. All rights reserved.
-This is a prerelease version; distribution is restricted.
+The source code of CVC4 is open and available to students, researchers,
+software companies, and everyone else to study, to modify, and to redistribute
+original or modified versions; distribution is under the terms of the modified
+BSD license (reproduced below). Please note that CVC4 can be configured
+(however, by default it is not) to link against some GPLed libraries, and
+therefore the use of these builds may be restricted in non-GPL-compatible
+projects. See below for a discussion of CLN, GLPK, and Readline (the three
+GPLed optional library dependences for CVC4), and how to ensure you have a
+build that doesn't link against GPLed libraries.
--- Morgan Deters <mdeters@cs.nyu.edu> Mon, 02 Nov 2009 17:54:27 -0500
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are
+met:
-CVC4 incorporates MiniSat code, excluded from the above copyright.
-See src/sat/minisat.
+1. Redistributions of source code must retain the above copyright
+ notice, this list of conditions and the following disclaimer.
- MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+2. Redistributions in binary form must reproduce the above copyright
+ notice, this list of conditions and the following disclaimer in the
+ documentation and/or other materials provided with the distribution.
- Permission is hereby granted, free of charge, to any person obtaining a
- copy of this software and associated documentation files (the
- "Software"), to deal in the Software without restriction, including
- without limitation the rights to use, copy, modify, merge, publish,
- distribute, sublicense, and/or sell copies of the Software, and to
- permit persons to whom the Software is furnished to do so, subject to
- the following conditions:
+3. Neither the name of the copyright holder nor the names of its
+ contributors may be used to endorse or promote products derived from
+ this software without specific prior written permission.
- The above copyright notice and this permission notice shall be included
- in all copies or substantial portions of the Software.
+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.
- THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS
- OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
- MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
- NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
- LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
- OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
- WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+
+-------------------------------------------------------------------------------
+ Third-Party Software
+-------------------------------------------------------------------------------
+
+The CVC4 source code includes third-party software which has its own copyright
+and licensing terms, as described below.
+
+The following file contains third-party software.
+
+ cmake/CodeCoverage.cmake
+
+The copyright and licensing information of this file is in its header.
+
+CVC4 incorporates MiniSat code (see src/prop/minisat and src/prop/bvminisat),
+excluded from the above copyright. See src/prop/minisat/LICENSE and
+src/prop/bvminisat/LICENSE for copyright and licensing information.
+
+CVC4 incorporates code from ANTLR3 (http://www.antlr3.org/), the files
+src/parser/bounded_token_buffer.h, src/parser/bounded_token_buffer.cpp, and
+src/parser/antlr_input_imports.cpp are excluded from the above copyright.
+See licenses/antlr3-LICENSE for copyright and licensing information.
+
+CVC4 by default links against The GNU Multiple Precision (GMP) Arithmetic
+Library, which is licensed under GNU LGPL v3. See the file
+licenses/lgpl-3.0.txt for a copy of that license. Note that according to the
+terms of the LGPL, both CVC4's source, and the combined work (CVC4 linked with
+GMP) may (and do) remain under the more permissive modified BSD license.
+
+The implementation of the floating point solver in CVC4 depends on symfpu
+(https://github.com/martin-cs/symfpu) written by Martin Brain.
+See https://raw.githubusercontent.com/martin-cs/symfpu/CVC4/LICENSE for
+copyright and licensing information.
+
+CVC4 optionally links against the following libraries:
+
+ ABC (https://bitbucket.org/alanmi/abc)
+ CaDiCaL (https://github.com/arminbiere/cadical)
+ CryptoMiniSat (https://github.com/msoos/cryptominisat)
+ LFSC checker (https://github.com/CVC4/LFSC)
+
+Linking CVC4 against these libraries does not affect the license terms of the
+CVC4 code. See the respective projects for copyright and licensing
+information.
+
+
+-------------------------------------------------------------------------------
+ OPTIONAL GPLv3 libraries
+-------------------------------------------------------------------------------
+
+Please be advised that the following libraries are covered under the GPLv3
+license. If you choose to link CVC4 against one of these libraries, the
+resulting combined work 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 (which is the default). CVC4 can then
+be used in contexts where you want to use CVC4 under the terms of the
+(modified) BSD license. See licenses/gpl-3.0.txt for more information.
+
+CVC4 can be optionally configured to link against CLN, the Class Library for
+Numbers, available here:
+
+ http://www.ginac.de/CLN/
+
+CVC4 can be optionally configured to link against glpk-cut-log, a modified
+version of GLPK, the GNU Linear Programming Kit, available here:
+
+ https://github.com/timothy-king/glpk-cut-log
+
+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
projects / cvc5.git / blobdiff