COPYING

   1 CVC4 is copyright (C) 2009, 2010, 2011, 2012, 2013 New York University
   2 and The University of Iowa.  All rights reserved.
   3
   4 CVC4 is open-source; distribution is under the terms of the modified BSD
   5 license.  However, certain builds of CVC4 link against GPLed libraries,
   6 and therefore the use of these builds is restricted in non-open-source
   7 projects.  See below for a discussion of CLN and GLPK, and how to ensure
   8 you have a build that doesn't link against GPLed libraries.
   9
  10 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT OWNERS AND CONTRIBUTORS
  11 ''AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
  12 LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
  13 A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
  14 OWNERS OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
  15 SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
  16 LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
  17 DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
  18 THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
  19 (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
  20 OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
  21
  22 -- Morgan Deters <mdeters@cs.nyu.edu>  Thu, 25 Apr 2013 15:45:40 -0400
  23
  24 CVC4 incorporates MiniSat code, excluded from the above copyright.
  25 See src/sat/minisat.  Its copyright:
  26
  27   MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
  28              Copyright (c) 2007-2010  Niklas Sorensson
  29
  30   Permission is hereby granted, free of charge, to any person obtaining a
  31   copy of this software and associated documentation files (the
  32   "Software"), to deal in the Software without restriction, including
  33   without limitation the rights to use, copy, modify, merge, publish,
  34   distribute, sublicense, and/or sell copies of the Software, and to
  35   permit persons to whom the Software is furnished to do so, subject to
  36   the following conditions:
  37
  38   The above copyright notice and this permission notice shall be included
  39   in all copies or substantial portions of the Software.
  40
  41   THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS
  42   OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
  43   MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
  44   NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
  45   LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
  46   OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
  47   WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
  48
  49 CVC4 incorporates the script "autogen.sh", excluded from the above copyright.
  50 See autogen.sh.  Its copyright:
  51
  52   Copyright (c) 2005-2009 United States Government as represented by
  53   the U.S. Army Research Laboratory.
  54
  55   Redistribution and use in source and binary forms, with or without
  56   modification, are permitted provided that the following conditions
  57   are met:
  58
  59   1. Redistributions of source code must retain the above copyright
  60   notice, this list of conditions and the following disclaimer.
  61
  62   2. Redistributions in binary form must reproduce the above
  63   copyright notice, this list of conditions and the following
  64   disclaimer in the documentation and/or other materials provided
  65   with the distribution.
  66
  67   3. The name of the author may not be used to endorse or promote
  68   products derived from this software without specific prior written
  69   permission.
  70
  71   THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS
  72   OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
  73   WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
  74   ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY
  75   DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
  76   DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE
  77   GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
  78   INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY,
  79   WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
  80   NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
  81   SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
  82
  83 CVC4 incorporates the script "doxygen.am", excluded from the above copyright.
  84 See config/doxygen.am.  Its copyright:
  85
  86   Copyright (C) 2004 Oren Ben-Kiki
  87   This file is distributed under the same terms as the Automake macro files.
  88
  89 CVC4 incorporates the m4 macro file "pkg.m4", excluded from the above
  90 copyright.  See config/pkg.m4.  Its copyright:
  91
  92   Copyright (c) 2004 Scott James Remnant <scott@netsplit.com>.
  93
  94   This program is free software; you can redistribute it and/or modify
  95   it under the terms of the GNU General Public License as published by
  96   the Free Software Foundation; either version 2 of the License, or
  97   (at your option) any later version.
  98
  99   This program is distributed in the hope that it will be useful, but
 100   WITHOUT ANY WARRANTY; without even the implied warranty of
 101   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
 102   General Public License for more details.
 103
 104   You should have received a copy of the GNU General Public License
 105   along with this program; if not, write to the Free Software
 106   Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
 107
 108   As a special exception to the GNU General Public License, if you
 109   distribute this file as part of a program that contains a
 110   configuration script generated by Autoconf, you may include it under
 111   the same distribution terms that you use for the rest of that program.
 112
 113 CVC4 incorporates the m4 macro file "ax_tls.m4", excluded from the above
 114 copyright and downloaded from
 115 http://www.gnu.org/software/autoconf-archive/ax_tls.html.
 116 See config/ax_tls.m4.  Its copyright:
 117
 118   Copyright (c) 2008 Alan Woodland <ajw05@aber.ac.uk>
 119   Copyright (c) 2010 Diego Elio Pettenò <flameeyes@gmail.com>
 120
 121   This program is free software: you can redistribute it and/or modify it
 122   under the terms of the GNU General Public License as published by the
 123   Free Software Foundation, either version 3 of the License, or (at your
 124   option) any later version.
 125
 126   This program is distributed in the hope that it will be useful, but
 127   WITHOUT ANY WARRANTY; without even the implied warranty of
 128   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General
 129   Public License for more details.
 130
 131   You should have received a copy of the GNU General Public License along
 132   with this program. If not, see <http://www.gnu.org/licenses/>.
 133
 134   As a special exception, the respective Autoconf Macro's copyright owner
 135   gives unlimited permission to copy, distribute and modify the configure
 136   scripts that are the output of Autoconf when processing the Macro. You
 137   need not follow the terms of the GNU General Public License when using
 138   or distributing such scripts, even though portions of the text of the
 139   Macro appear in them. The GNU General Public License (GPL) does govern
 140   all other use of the material that constitutes the Autoconf Macro.
 141
 142   This special exception to the GPL applies to versions of the Autoconf
 143   Macro released by the Autoconf Archive. When you make and distribute a
 144   modified version of the Autoconf Macro, you may extend this special
 145   exception to the GPL to apply to your modified version as well.
 146
 147 CVC4 incorporates the m4 macro file "boost.m4", excluded from the above
 148 copyright and downloaded from http://github.com/tsuna/boost.m4 .
 149 See config/boost.m4.  Its copyright:
 150
 151   Copyright (C) 2007  Benoit Sigoure <tsuna@lrde.epita.fr>
 152
 153   This program is free software: you can redistribute it and/or modify
 154   it under the terms of the GNU General Public License as published by
 155   the Free Software Foundation, either version 3 of the License, or
 156   (at your option) any later version.
 157
 158   This program is distributed in the hope that it will be useful,
 159   but WITHOUT ANY WARRANTY; without even the implied warranty of
 160   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 161   GNU General Public License for more details.
 162
 163   You should have received a copy of the GNU General Public License
 164   along with this program.  If not, see <http://www.gnu.org/licenses/>.
 165
 166   Additional permission under section 7 of the GNU General Public
 167   License, version 3 ("GPLv3"):
 168
 169   If you convey this file as part of a work that contains a
 170   configuration script generated by Autoconf, you may do so under
 171   terms of your choice.
 172
 173 CVC4 incorporates some code from Boost (see src/util/channel.h).  This
 174 is covered by the Boost Software License, version 1.0, available at
 175 http://www.boost.org/LICENSE_1_0.txt and reprinted below:
 176
 177   Boost Software License - Version 1.0 - August 17th, 2003
 178
 179   Permission is hereby granted, free of charge, to any person or organization
 180   obtaining a copy of the software and accompanying documentation covered by
 181   this license (the "Software") to use, reproduce, display, distribute,
 182   execute, and transmit the Software, and to prepare derivative works of the
 183   Software, and to permit third-parties to whom the Software is furnished to
 184   do so, all subject to the following:
 185
 186   The copyright notices in the Software and this entire statement, including
 187   the above license grant, this restriction and the following disclaimer,
 188   must be included in all copies of the Software, in whole or in part, and
 189   all derivative works of the Software, unless such copies or derivative
 190   works are solely in the form of machine-executable object code generated by
 191   a source language processor.
 192
 193   THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 194   IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
 195   FITNESS FOR A PARTICULAR PURPOSE, TITLE AND NON-INFRINGEMENT. IN NO EVENT
 196   SHALL THE COPYRIGHT HOLDERS OR ANYONE DISTRIBUTING THE SOFTWARE BE LIABLE
 197   FOR ANY DAMAGES OR OTHER LIABILITY, WHETHER IN CONTRACT, TORT OR OTHERWISE,
 198   ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER
 199   DEALINGS IN THE SOFTWARE.
 200
 201 CVC4 incorporates code from ANTLR3, excluded from the above copyright.
 202 See http://www.antlr3.org/, and the files src/parser/bounded_token_buffer.h,
 203 src/parser/bounded_token_buffer.cpp, and src/parser/antlr_input_imports.cpp.
 204 Their copyright:
 205
 206   [The "BSD licence"]
 207   Copyright (c) 2005-2009 Jim Idle, Temporal Wave LLC
 208   http://www.temporal-wave.com
 209   http://www.linkedin.com/in/jimidle
 210
 211   All rights reserved.
 212
 213   Redistribution and use in source and binary forms, with or without
 214   modification, are permitted provided that the following conditions
 215   are met:
 216   1. Redistributions of source code must retain the above copyright
 217      notice, this list of conditions and the following disclaimer.
 218   2. Redistributions in binary form must reproduce the above copyright
 219      notice, this list of conditions and the following disclaimer in the
 220      documentation and/or other materials provided with the distribution.
 221   3. The name of the author may not be used to endorse or promote products
 222      derived from this software without specific prior written permission.
 223
 224   THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR
 225   IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES
 226   OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED.
 227   IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT,
 228   INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT
 229   NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
 230   DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
 231   THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 232   (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF
 233   THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 234
 235 Certain builds of CVC4 link against a GPLed library, CLN, the Class Library
 236 for Numbers, available here:
 237
 238   http://www.ginac.de/CLN/
 239
 240 Please be advised that as this library is covered under the GPLv3, if you
 241 choose to use the combined work, "CVC4+CLN," by building CVC4 with CLN,
 242 then it is also covered under the GPLv3.  If you want to make sure you build
 243 a version of CVC4 that uses libgmp, the GNU Multiple Precision Arithmetic
 244 Library, configure CVC4 with "--with-gmp" before building (though that is the
 245 default).  It can then be used in contexts where you want to license CVC4
 246 under the (modified) BSD license.
 247
 248 Certain builds of CVC4 link against a GPLed library, GLPK, the GNU Linear
 249 Programming Kit, available here:
 250
 251   http://www.gnu.org/software/glpk/
 252
 253 Please be advised that as this library is covered under the GPLv3, if
 254 you choose to use the combined work, "CVC4+GLPK," by building CVC4 with
 255 GLPK, then it is also covered under the GPLv3.  If you want to make sure
 256 you build a version of CVC4 that does not use GLPK, configure CVC4 with
 257 "--without-glpk" before building (though that is the default).  It can
 258 then be used in contexts where you want to license CVC4 under the
 259 (modified) BSD license.