00001 /*!\page LICENSE LICENSE 00002 00003 Copyright (C) 2003-2007 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 License to use, copy, modify, sell and/or distribute this software and 00008 its documentation for any purpose is hereby granted without royalty, 00009 subject to the following terms and conditions: 00010 00011 1. The above copyright notice and this permission notice must 00012 appear in all copies of the software and related documentation. 00013 00014 2. The names of the Copyright Owners may not be used in advertising or 00015 publicity pertaining to distribution of the software without the specific, 00016 prior written permission of the Copyright Owners. 00017 00018 3. This software may not be called "CVC3" if it has been modified 00019 in any way, without the specific prior written permission of Clark Barrett. 00020 00021 4. THE SOFTWARE IS PROVIDED "AS-IS" AND THE COPYRIGHT OWNERS MAKE NO 00022 REPRESENTATIONS OR WARRANTIES, EXPRESS OR IMPLIED, BY WAY OF EXAMPLE, BUT NOT 00023 LIMITATION. THE COPYRIGHT OWNERS MAKE NO REPRESENTATIONS OR WARRANTIES OF 00024 MERCHANTABILITY OR FITNESS FOR ANY PARTICULAR PURPOSE OR THAT THE USE OF THE 00025 SOFTWARE WILL NOT INFRINGE ANY PATENTS, COPYRIGHTS TRADEMARKS OR OTHER 00026 RIGHTS. THE COPYRIGHT OWNERS SHALL NOT BE LIABLE FOR ANY LIABILITY OR DAMAGES 00027 WITH RESPECT TO ANY CLAIM BY LICENSEE OR ANY THIRD PARTY ON ACCOUNT OF, OR 00028 ARISING FROM THE LICENSE, OR ANY SUBLICENSE OR USE OF THE SOFTWARE OR ANY 00029 SERVICE OR SUPPORT. 00030 00031 LICENSEE shall indemnify, hold harmless and defend the Copyright Owners and 00032 their trustees, officers, employees, students and agents against any and all 00033 claims arising out of the exercise of any rights under this Agreement, 00034 including, without limiting the generality of the foregoing, against any 00035 damages, losses or liabilities whatsoever with respect to death or injury to 00036 person or damage to property arising from or out of the possession, use, or 00037 operation of Software or Licensed Program(s) by LICENSEE or its customers. 00038 00039 Note: 00040 00041 The following files contain code whose copyright does not belong to the 00042 Copyright Owners. However, separate copyright notices in these files give 00043 express permission to copy, use, modify, sell, or distribute the code. Please 00044 see the copyright notices in the individual files for details. 00045 00046 <pre> 00047 src/include/fdstream.h 00048 src/include/hash_map.h 00049 src/include/hash_fun.h 00050 src/include/hash_set.h 00051 src/include/hash_table.h 00052 src/sat/minisat_varorder.h 00053 src/sat/minisat_solver.cpp 00054 src/sat/minisat_heap.h 00055 src/sat/minisat_types.h 00056 src/sat/minisat_solver.h 00057 src/sat/minisat_global.h 00058 </pre> 00059 00060 This copy of CVC3 is also configured to use the SAT solver zchaff whose 00061 copyright is owned by Princeton University and is more restrictive. 00062 00063 Specifically, it may be used for internal, noncommercial, research purposes 00064 only. See the copyright notice in the following files for more information. 00065 To build CVC3 without these files, please delete them and then run: 00066 <pre> 00067 ./configure --disable-zchaff 00068 make 00069 </pre> 00070 00071 <pre> 00072 src/sat/xchaff_base.h 00073 src/sat/xchaff_dbase.h 00074 src/sat/xchaff_solver.h 00075 src/sat/xchaff_utils.h 00076 src/sat/xchaff_dbase.cpp 00077 src/sat/xchaff_solver.cpp 00078 src/sat/xchaff_utils.cpp 00079 </pre> 00080 00081 */
1.5.1