-CVC4 is copyright (C) 2009 the ACSys research group at the Courant
-Institute for Mathematical Sciences, New York University.
-All rights reserved.
+cvc5 is copyright (C) 2009-2021 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 cvc5 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 cvc5 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 and GLPK (the two GPLed optional
+library dependences for cvc5), 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:
+
+1. Redistributions of source code must retain the above copyright
+ notice, this list of conditions and the following disclaimer.
+
+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.
+
+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.
+
+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.
+
+
+-------------------------------------------------------------------------------
+ Third-Party Software
+-------------------------------------------------------------------------------
+
+The cvc5 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.
+
+cvc5 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.
+
+cvc5 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.
+
+cvc5 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 cvc5's source, and the combined work (cvc5 linked with
+GMP) may (and do) remain under the more permissive modified BSD license.
+
+The implementation of the floating point solver in cvc5 depends on symfpu
+(https://github.com/martin-cs/symfpu) written by Martin Brain.
+See https://raw.githubusercontent.com/martin-cs/symfpu/cvc5/LICENSE for
+copyright and licensing information.
+
+cvc5 optionally links against the following libraries:
+
+ ABC (https://bitbucket.org/alanmi/abc)
+ CaDiCaL (https://github.com/arminbiere/cadical)
+ CryptoMiniSat (https://github.com/msoos/cryptominisat)
+ LibPoly (https://github.com/SRI-CSL/libpoly)
+ libedit (https://thrysoee.dk/editline)
+
+Linking cvc5 against these libraries does not affect the license terms of the
+cvc5 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 cvc5 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 cvc5 that uses no GPLed libraries, configure cvc5
+with the "--no-gpl" option before building (which is the default). cvc5 can
+then be used in contexts where you want to use cvc5 under the terms of the
+(modified) BSD license. See licenses/gpl-3.0.txt for more information.
+
+cvc5 can be optionally configured to link against CLN, the Class Library for
+Numbers, available here:
+
+ http://www.ginac.de/CLN/
+
+cvc5 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
projects / cvc5.git / blobdiff