You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
74 lines
2.8 KiB
74 lines
2.8 KiB
12 years ago
|
/*!\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>
|
||
|
|
||
|
*/
|