Add CVC3 license for sci-mathematics/cvc3

1 files changed, 73 insertions, 0 deletions

diff --git a/licenses/CVC3 b/licenses/CVC3
new file mode 100644
index 000000000000..d3cf05ca7344
--- /dev/null
+++ b/licenses/CVC3
@@ -0,0 +1,73 @@
+/*!\page LICENSE LICENSE
+
+Copyright (C) 2003-2009 by the Board of Trustees of Leland Stanford Junior
+University, New York University, and the University of Iowa, hereafter
+designated as the Copyright Owners.
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without modification,
+are permitted provided that the following conditions are met:
+
+* Redistributions of source code must retain the above copyright notice, this
+list of conditions and the following disclaimer.
+* 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.
+* Neither the names of the Copyright Owners nor the names of any 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.
+
+Note:
+
+The following files contain code whose copyright does not belong to the
+Copyright Owners.  However, separate copyright notices in these files give
+express permission to copy, use, modify, sell, or distribute the code.  Please
+see the copyright notices in the individual files for details.
+
+<pre>
+src/include/fdstream.h
+src/include/hash_map.h
+src/include/hash_fun.h
+src/include/hash_set.h
+src/include/hash_table.h
+src/sat/minisat_varorder.h
+src/sat/minisat_solver.cpp
+src/sat/minisat_heap.h
+src/sat/minisat_types.h
+src/sat/minisat_solver.h
+src/sat/minisat_global.h
+</pre>
+This copy of CVC3 is also configured to use the SAT solver zchaff whose
+copyright is owned by Princeton University and is more restrictive.
+
+Specifically, it may be used for internal, noncommercial, research purposes
+only.  See the copyright notice in the following files for more information.
+To build CVC3 without these files, please delete them and then run:
+<pre>
+   ./configure --disable-zchaff
+   make
+</pre>
+
+<pre>
+src/sat/xchaff_base.h
+src/sat/xchaff_dbase.h
+src/sat/xchaff_solver.h
+src/sat/xchaff_utils.h
+src/sat/xchaff_dbase.cpp
+src/sat/xchaff_solver.cpp
+src/sat/xchaff_utils.cpp
+</pre>
+
+*/