|
CVC3
|
00001 /*!\page LICENSE LICENSE 00002 00003 Copyright (C) 2003-2009 by the Board of Trustees of Leland Stanford Junior 00004 University, New York University, and the University of Iowa, hereafter 00005 designated as the Copyright Owners. 00006 00007 All rights reserved. 00008 00009 Redistribution and use in source and binary forms, with or without modification, 00010 are permitted provided that the following conditions are met: 00011 00012 * Redistributions of source code must retain the above copyright notice, this 00013 list of conditions and the following disclaimer. 00014 * Redistributions in binary form must reproduce the above copyright notice, 00015 this list of conditions and the following disclaimer in the documentation 00016 and/or other materials provided with the distribution. 00017 * Neither the names of the Copyright Owners nor the names of any contributors 00018 may be used to endorse or promote products derived from this software 00019 without specific prior written permission. 00020 00021 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT OWNERS AND CONTRIBUTORS ''AS IS'' AND ANY 00022 EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED 00023 WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE 00024 DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNERS OR CONTRIBUTORS BE LIABLE FOR ANY 00025 DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES 00026 (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; 00027 LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON 00028 ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT 00029 (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS 00030 SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. 00031 00032 Note: 00033 00034 The following files contain code whose copyright does not belong to the 00035 Copyright Owners. However, separate copyright notices in these files give 00036 express permission to copy, use, modify, sell, or distribute the code. Please 00037 see the copyright notices in the individual files for details. 00038 00039 <pre> 00040 src/include/fdstream.h 00041 src/include/hash_map.h 00042 src/include/hash_fun.h 00043 src/include/hash_set.h 00044 src/include/hash_table.h 00045 src/sat/minisat_varorder.h 00046 src/sat/minisat_solver.cpp 00047 src/sat/minisat_heap.h 00048 src/sat/minisat_types.h 00049 src/sat/minisat_solver.h 00050 src/sat/minisat_global.h 00051 </pre> 00052 This copy of CVC3 is also configured to use the SAT solver zchaff whose 00053 copyright is owned by Princeton University and is more restrictive. 00054 00055 Specifically, it may be used for internal, noncommercial, research purposes 00056 only. See the copyright notice in the following files for more information. 00057 To build CVC3 without these files, please delete them and then run: 00058 <pre> 00059 ./configure --disable-zchaff 00060 make 00061 </pre> 00062 00063 <pre> 00064 src/sat/xchaff_base.h 00065 src/sat/xchaff_dbase.h 00066 src/sat/xchaff_solver.h 00067 src/sat/xchaff_utils.h 00068 src/sat/xchaff_dbase.cpp 00069 src/sat/xchaff_solver.cpp 00070 src/sat/xchaff_utils.cpp 00071 </pre> 00072 00073 */
1.7.3