Added CVC3's parser for the SMT-LIB grammar.

git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73059 91177308-0d34-0410-b5e6-96231b3b80d8

1 files changed, 53 insertions, 0 deletions

diff --git a/lib/SMT/LICENSE.CVC3 b/lib/SMT/LICENSE.CVC3
new file mode 100644
index 00000000..a70d12d5
--- /dev/null
+++ b/lib/SMT/LICENSE.CVC3
@@ -0,0 +1,53 @@
+/*!\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>
+
+*/