| 1 | Copyright (C) 2003-2009 by the Board of Trustees of Leland Stanford Junior
|
|---|
| 2 | University, New York University, and the University of Iowa, hereafter
|
|---|
| 3 | designated as the Copyright Owners.
|
|---|
| 4 |
|
|---|
| 5 | All rights reserved.
|
|---|
| 6 |
|
|---|
| 7 | Redistribution and use in source and binary forms, with or without modification,
|
|---|
| 8 | are permitted provided that the following conditions are met:
|
|---|
| 9 |
|
|---|
| 10 | * Redistributions of source code must retain the above copyright notice, this
|
|---|
| 11 | list of conditions and the following disclaimer.
|
|---|
| 12 | * Redistributions in binary form must reproduce the above copyright notice,
|
|---|
| 13 | this list of conditions and the following disclaimer in the documentation
|
|---|
| 14 | and/or other materials provided with the distribution.
|
|---|
| 15 | * Neither the names of the Copyright Owners nor the names of any contributors
|
|---|
| 16 | may be used to endorse or promote products derived from this software
|
|---|
| 17 | without specific prior written permission.
|
|---|
| 18 |
|
|---|
| 19 | THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT OWNERS AND CONTRIBUTORS ''AS IS'' AND ANY
|
|---|
| 20 | EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
|
|---|
| 21 | WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
|
|---|
| 22 | DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNERS OR CONTRIBUTORS BE LIABLE FOR ANY
|
|---|
| 23 | DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
|
|---|
| 24 | (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
|
|---|
| 25 | LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON
|
|---|
| 26 | ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
|
|---|
| 27 | (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
|
|---|
| 28 | SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
|
|---|
| 29 |
|
|---|
| 30 | Note:
|
|---|
| 31 |
|
|---|
| 32 | The following files contain code whose copyright does not belong to the
|
|---|
| 33 | Copyright Owners. However, separate copyright notices in these files give
|
|---|
| 34 | express permission to copy, use, modify, sell, or distribute the code. Please
|
|---|
| 35 | see the copyright notices in the individual files for details.
|
|---|
| 36 |
|
|---|
| 37 | <pre>
|
|---|
| 38 | src/include/fdstream.h
|
|---|
| 39 | src/include/hash_map.h
|
|---|
| 40 | src/include/hash_fun.h
|
|---|
| 41 | src/include/hash_set.h
|
|---|
| 42 | src/include/hash_table.h
|
|---|
| 43 | src/sat/minisat_varorder.h
|
|---|
| 44 | src/sat/minisat_solver.cpp
|
|---|
| 45 | src/sat/minisat_heap.h
|
|---|
| 46 | src/sat/minisat_types.h
|
|---|
| 47 | src/sat/minisat_solver.h
|
|---|
| 48 | src/sat/minisat_global.h
|
|---|
| 49 | </pre>
|
|---|
| 50 | This copy of CVC3 is also configured to use the SAT solver zchaff whose
|
|---|
| 51 | copyright is owned by Princeton University and is more restrictive.
|
|---|
| 52 |
|
|---|
| 53 | Specifically, it may be used for internal, noncommercial, research purposes
|
|---|
| 54 | only. See the copyright notice in the following files for more information.
|
|---|
| 55 | To build CVC3 without these files, please delete them and then run:
|
|---|
| 56 | <pre>
|
|---|
| 57 | ./configure --disable-zchaff
|
|---|
| 58 | make
|
|---|
| 59 | </pre>
|
|---|
| 60 |
|
|---|
| 61 | <pre>
|
|---|
| 62 | src/sat/xchaff_base.h
|
|---|
| 63 | src/sat/xchaff_dbase.h
|
|---|
| 64 | src/sat/xchaff_solver.h
|
|---|
| 65 | src/sat/xchaff_utils.h
|
|---|
| 66 | src/sat/xchaff_dbase.cpp
|
|---|
| 67 | src/sat/xchaff_solver.cpp
|
|---|
| 68 | src/sat/xchaff_utils.cpp
|
|---|
| 69 | </pre>
|
|---|
