diff options
| -rw-r--r-- | COPYING | 28 | ||||
| -rw-r--r-- | README | 2 | ||||
| -rw-r--r-- | configure.ac | 1 | ||||
| -rw-r--r-- | src/util/Makefile.am | 1 | ||||
| -rw-r--r-- | src/util/channel.cpp | 2 | ||||
| -rw-r--r-- | src/util/channel.h | 31 |
6 files changed, 53 insertions, 12 deletions
@@ -171,6 +171,34 @@ See config/boost.m4. Its copyright: configuration script generated by Autoconf, you may do so under terms of your choice. +CVC4 incorporates some code from Boost (see src/util/channel.h). This +is covered by the Boost Software License, version 1.0, available at +http://www.boost.org/LICENSE_1_0.txt and reprinted below: + + Boost Software License - Version 1.0 - August 17th, 2003 + + Permission is hereby granted, free of charge, to any person or organization + obtaining a copy of the software and accompanying documentation covered by + this license (the "Software") to use, reproduce, display, distribute, + execute, and transmit the Software, and to prepare derivative works of the + Software, and to permit third-parties to whom the Software is furnished to + do so, all subject to the following: + + The copyright notices in the Software and this entire statement, including + the above license grant, this restriction and the following disclaimer, + must be included in all copies of the Software, in whole or in part, and + all derivative works of the Software, unless such copies or derivative + works are solely in the form of machine-executable object code generated by + a source language processor. + + THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, + FITNESS FOR A PARTICULAR PURPOSE, TITLE AND NON-INFRINGEMENT. IN NO EVENT + SHALL THE COPYRIGHT HOLDERS OR ANYONE DISTRIBUTING THE SOFTWARE BE LIABLE + FOR ANY DAMAGES OR OTHER LIABILITY, WHETHER IN CONTRACT, TORT OR OTHERWISE, + ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER + DEALINGS IN THE SOFTWARE. + CVC4 incorporates code from ANTLR3, excluded from the above copyright. See http://www.antlr.org/, and the files src/parser/bounded_token_buffer.h, src/parser/bounded_token_buffer.cpp, and src/parser/antlr_input_imports.cpp. @@ -37,11 +37,11 @@ GNU C and C++ (gcc and g++), reasonably recent versions GNU Make GNU Bash GMP v4.2 (GNU Multi-Precision arithmetic library) -The Boost C++ threading library (libboost_thread) libantlr3c v3.2 (ANTLR parser generator) Optional: CLN v1.3 (Class Library for Numbers) Optional: CUDD v2.4.2 (Colorado University Decision Diagram package) Optional: GNU Readline library (for an improved interactive experience) +Optional: The Boost C++ threading library (libboost_thread) If "make" is non-GNU on your system, make sure to invoke "gmake" (or whatever GNU Make is installed as). If your usual shell is not diff --git a/configure.ac b/configure.ac index 2687ccb3f..6f5568bd2 100644 --- a/configure.ac +++ b/configure.ac @@ -1129,7 +1129,6 @@ gcov support : $enable_coverage gprof support: $enable_profiling CUDD : $cvc4cudd Readline : $with_readline -TLS support : $CVC4_TLS Static libs : $enable_static Shared libs : $enable_shared diff --git a/src/util/Makefile.am b/src/util/Makefile.am index 33123772d..e24184ad2 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -53,7 +53,6 @@ libutil_la_SOURCES = \ lemma_input_channel.h \ lemma_output_channel.h \ channel.h \ - channel.cpp \ language.cpp \ ntuple.h \ recursion_breaker.h \ diff --git a/src/util/channel.cpp b/src/util/channel.cpp deleted file mode 100644 index 998550f8e..000000000 --- a/src/util/channel.cpp +++ /dev/null @@ -1,2 +0,0 @@ -#include "channel.h" - diff --git a/src/util/channel.h b/src/util/channel.h index 1701feba9..eae7a4f11 100644 --- a/src/util/channel.h +++ b/src/util/channel.h @@ -1,3 +1,21 @@ +/********************* */ +/*! \file channel.h + ** \verbatim + ** Original author: kshitij + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ #ifndef __CVC4__CHANNEL_H #define __CVC4__CHANNEL_H @@ -10,7 +28,6 @@ #include <boost/progress.hpp> #include <boost/bind.hpp> - namespace CVC4 { template <typename T> @@ -32,15 +49,17 @@ public: /* */ virtual bool full() = 0; -}; +};/* class SharedChannel<T> */ /* This code is from -http://live.boost.org/doc/libs/1_46_1/libs/circular_buffer/doc/circular_buffer.html#boundedbuffer +http://live.boost.org/doc/libs/1_46_1/libs/circular_buffer/doc/circular_buffer.html#boundedbuffer + +and is covered by the Boost Software License, version 1.0. */ template <typename T> -class SynchronizedSharedChannel: public SharedChannel<T> { +class SynchronizedSharedChannel : public SharedChannel<T> { public: typedef boost::circular_buffer<T> container_type; typedef typename container_type::size_type size_type; @@ -87,10 +106,8 @@ private: boost::mutex m_mutex; boost::condition m_not_empty; boost::condition m_not_full; -}; +};/* class SynchronizedSharedChannel<T> */ } #endif /* __CVC4__CHANNEL_H */ - - |