License to use, copy, modify, sell and/or distribute this software and its documentation for any purpose is hereby granted without royalty, subject to the following terms and conditions:
1. The above copyright notice and this permission notice must appear in all copies of the software and related documentation.
2. The names of the Copyright Owners may not be used in advertising or publicity pertaining to distribution of the software without the specific, prior written permission of the Copyright Owners.
3. This software may not be called "CVC3" if it has been modified in any way, without the specific prior written permission of Clark Barrett.
4. THE SOFTWARE IS PROVIDED "AS-IS" AND THE COPYRIGHT OWNERS MAKE NO REPRESENTATIONS OR WARRANTIES, EXPRESS OR IMPLIED, BY WAY OF EXAMPLE, BUT NOT LIMITATION. THE COPYRIGHT OWNERS MAKE NO REPRESENTATIONS OR WARRANTIES OF MERCHANTABILITY OR FITNESS FOR ANY PARTICULAR PURPOSE OR THAT THE USE OF THE SOFTWARE WILL NOT INFRINGE ANY PATENTS, COPYRIGHTS TRADEMARKS OR OTHER RIGHTS. THE COPYRIGHT OWNERS SHALL NOT BE LIABLE FOR ANY LIABILITY OR DAMAGES WITH RESPECT TO ANY CLAIM BY LICENSEE OR ANY THIRD PARTY ON ACCOUNT OF, OR ARISING FROM THE LICENSE, OR ANY SUBLICENSE OR USE OF THE SOFTWARE OR ANY SERVICE OR SUPPORT.
LICENSEE shall indemnify, hold harmless and defend the Copyright Owners and their trustees, officers, employees, students and agents against any and all claims arising out of the exercise of any rights under this Agreement, including, without limiting the generality of the foregoing, against any damages, losses or liabilities whatsoever with respect to death or injury to person or damage to property arising from or out of the possession, use, or operation of Software or Licensed Program(s) by LICENSEE or its customers.
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.
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
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:
./configure --disable-zchaff make
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
1.5.1