1 CVC4 is copyright (C) 2009, 2010, 2011 the ACSys research group at the
2 Courant Institute for Mathematical Sciences, New York University.
5 CVC4 is open-source; distribution is under the terms of the modified BSD
6 license. However, certain builds of CVC4 link against GPLed libraries,
7 and therefore the use of these builds is restricted in non-open-source
8 projects. See below for a discussion of CLN and how to ensure you have
9 a build that doesn't link against GPLed libraries.
11 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT OWNERS AND CONTRIBUTORS
12 ''AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
13 LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
14 A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
15 OWNERS OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
16 SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
17 LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
18 DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
19 THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
20 (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
21 OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
23 -- Morgan Deters <mdeters@cs.nyu.edu> Fri, 04 Feb 2011 14:56:41 -0500
25 CVC4 incorporates MiniSat code, excluded from the above copyright.
26 See src/sat/minisat. Its copyright:
28 MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
29 Copyright (c) 2007-2010 Niklas Sorensson
31 Permission is hereby granted, free of charge, to any person obtaining a
32 copy of this software and associated documentation files (the
33 "Software"), to deal in the Software without restriction, including
34 without limitation the rights to use, copy, modify, merge, publish,
35 distribute, sublicense, and/or sell copies of the Software, and to
36 permit persons to whom the Software is furnished to do so, subject to
37 the following conditions:
39 The above copyright notice and this permission notice shall be included
40 in all copies or substantial portions of the Software.
42 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS
43 OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
44 MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
45 NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
46 LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
47 OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
48 WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
50 CVC4 incorporates the script "autogen.sh", excluded from the above copyright.
51 See autogen.sh. Its copyright:
53 Copyright (c) 2005-2009 United States Government as represented by
54 the U.S. Army Research Laboratory.
56 Redistribution and use in source and binary forms, with or without
57 modification, are permitted provided that the following conditions
60 1. Redistributions of source code must retain the above copyright
61 notice, this list of conditions and the following disclaimer.
63 2. Redistributions in binary form must reproduce the above
64 copyright notice, this list of conditions and the following
65 disclaimer in the documentation and/or other materials provided
66 with the distribution.
68 3. The name of the author may not be used to endorse or promote
69 products derived from this software without specific prior written
72 THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS
73 OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
74 WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
75 ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY
76 DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
77 DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE
78 GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
79 INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY,
80 WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
81 NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
82 SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
84 CVC4 incorporates the script "doxygen.am", excluded from the above copyright.
85 See config/doxygen.am. Its copyright:
87 Copyright (C) 2004 Oren Ben-Kiki
88 This file is distributed under the same terms as the Automake macro files.
90 CVC4 incorporates the m4 macro file "pkg.m4", excluded from the above
91 copyright. See config/pkg.m4. Its copyright:
93 Copyright (c) 2004 Scott James Remnant <scott@netsplit.com>.
95 This program is free software; you can redistribute it and/or modify
96 it under the terms of the GNU General Public License as published by
97 the Free Software Foundation; either version 2 of the License, or
98 (at your option) any later version.
100 This program is distributed in the hope that it will be useful, but
101 WITHOUT ANY WARRANTY; without even the implied warranty of
102 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
103 General Public License for more details.
105 You should have received a copy of the GNU General Public License
106 along with this program; if not, write to the Free Software
107 Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
109 As a special exception to the GNU General Public License, if you
110 distribute this file as part of a program that contains a
111 configuration script generated by Autoconf, you may include it under
112 the same distribution terms that you use for the rest of that program.
114 CVC4 incorporates the m4 macro file "ax_tls.m4", excluded from the above
115 copyright and downloaded from
116 http://www.gnu.org/software/autoconf-archive/ax_tls.html.
117 See config/ax_tls.m4. Its copyright:
119 Copyright (c) 2008 Alan Woodland <ajw05@aber.ac.uk>
120 Copyright (c) 2010 Diego Elio Pettenò <flameeyes@gmail.com>
122 This program is free software: you can redistribute it and/or modify it
123 under the terms of the GNU General Public License as published by the
124 Free Software Foundation, either version 3 of the License, or (at your
125 option) any later version.
127 This program is distributed in the hope that it will be useful, but
128 WITHOUT ANY WARRANTY; without even the implied warranty of
129 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General
130 Public License for more details.
132 You should have received a copy of the GNU General Public License along
133 with this program. If not, see <http://www.gnu.org/licenses/>.
135 As a special exception, the respective Autoconf Macro's copyright owner
136 gives unlimited permission to copy, distribute and modify the configure
137 scripts that are the output of Autoconf when processing the Macro. You
138 need not follow the terms of the GNU General Public License when using
139 or distributing such scripts, even though portions of the text of the
140 Macro appear in them. The GNU General Public License (GPL) does govern
141 all other use of the material that constitutes the Autoconf Macro.
143 This special exception to the GPL applies to versions of the Autoconf
144 Macro released by the Autoconf Archive. When you make and distribute a
145 modified version of the Autoconf Macro, you may extend this special
146 exception to the GPL to apply to your modified version as well.
148 CVC4 incorporates code from ANTLR3, excluded from the above copyright.
149 See http://www.antlr.org/, and the files src/parser/bounded_token_buffer.h,
150 src/parser/bounded_token_buffer.cpp, and src/parser/antlr_input_imports.cpp.
154 Copyright (c) 2005-2009 Jim Idle, Temporal Wave LLC
155 http://www.temporal-wave.com
156 http://www.linkedin.com/in/jimidle
160 Redistribution and use in source and binary forms, with or without
161 modification, are permitted provided that the following conditions
163 1. Redistributions of source code must retain the above copyright
164 notice, this list of conditions and the following disclaimer.
165 2. Redistributions in binary form must reproduce the above copyright
166 notice, this list of conditions and the following disclaimer in the
167 documentation and/or other materials provided with the distribution.
168 3. The name of the author may not be used to endorse or promote products
169 derived from this software without specific prior written permission.
171 THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR
172 IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES
173 OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED.
174 IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT,
175 INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT
176 NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
177 DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
178 THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
179 (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF
180 THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
182 Certain builds of CVC4 link against a GPLed library, CLN, the Class Library
183 for Numbers, available here:
185 http://www.ginac.de/CLN/
187 Please be advised that as this class library is covered under the GPL, the
188 combined work, CVC4+CLN, is also covered under the GPL and cannot be used
189 by proprietary software projects. For the full text of the GPL, please
190 consult the CLN website. CVC4 does not require CLN; it can be built against
191 libgmp, the GNU Multiple Precision Arithmetic Library, which is covered by
192 the more permissive LGPL. To ensure that CLN is not used in the build,
193 configure CVC4 with "--without-cln".