don't require libboost_thread (its presence is detected at configure-time), and other...

diff --git a/COPYING b/COPYING
index 9d9e116fd3d628a56f9f557839880b27f5858c37..5c6be04c2e5f4f3b34a52ba92c977dc477023481 100644 (file)
--- a/COPYING
+++ b/COPYING
@@ -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.

diff --git a/README b/README
index 981eeaa603c127d97bc20eec34ca1875304e07a5..ed8edd53a4b318cbd2bb832ca37883a65670f6de 100644 (file)
--- a/README
+++ b/README
@@ -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 2687ccb3fa16922bc40eb062b3fb105177704a88..6f5568bd2f173ec5cabdcbbbc37898ee2e42f8cb 100644 (file)
--- 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 33123772dd308edb53d025a5d4b893049b921aa9..e24184ad25edb9fe678cca8d0a638fb5f50f83d0 100644 (file)
--- 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 (file)
index 998550f..0000000
--- 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 1701feba93fbfd0aa4e428553684c980418602c3..eae7a4f11e83fdd12b0975913cf1bd8e7e60f672 100644 (file)
--- 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 */
-
-