update-copyright.pl now retrieves and incorporates author information from repository history; re-ran update-copyright.pl; cleaned up some things with make

15 files changed, 77 insertions, 8 deletions

diff --git a/src/util/Assert.cpp b/src/util/Assert.cpp
index a86e2021a..337649039 100644
--- a/src/util/Assert.cpp
+++ b/src/util/Assert.cpp
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** Assert.cpp
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
diff --git a/src/util/Assert.h b/src/util/Assert.h
index 26a1ee7d4..49c97e9b6 100644
--- a/src/util/Assert.h
+++ b/src/util/Assert.h
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** Assert.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
diff --git a/src/util/command.cpp b/src/util/command.cpp
index 3911897f5..5a5b766cb 100644
--- a/src/util/command.cpp
+++ b/src/util/command.cpp
@@ -1,3 +1,18 @@
+/*********************                                           -*- C++ -*-  */
+/** command.cpp
+ ** Original author: mdeters
+ ** Major contributors: dejan
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009 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.
+ **
+ ** [[ Add file-specific comments here ]]
+ **/
+
 /*
  * command.cpp
  *
diff --git a/src/util/command.h b/src/util/command.h
index 221c513f0..9cc009d01 100644
--- a/src/util/command.h
+++ b/src/util/command.h
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** command.h
+ ** Original author: mdeters
+ ** Major contributors: dejan
+ ** Minor contributors (to current version): cconway
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -7,6 +10,8 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
+ ** Implementation of the command pattern on SmtEngines.  Generated by
+ ** the parser.
  **/
 
 #ifndef __CVC4__COMMAND_H
diff --git a/src/util/debug.h b/src/util/debug.h
index 14dc0fbd1..800106764 100644
--- a/src/util/debug.h
+++ b/src/util/debug.h
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** debug.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -7,20 +10,27 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
+ ** Debugging things.
+ **
+ ** These are low-level assertions!  Generally you should use
+ ** CVC4::Assert() instead (they throw an exception!).  See
+ ** util/Assert.h.
  **/
 
 #ifndef __CVC4__DEBUG_H
 #define __CVC4__DEBUG_H
 
+#include "cvc4_config.h"
+
 #include <cassert>
 
-#ifdef DEBUG
+#ifdef CVC4_ASSERTIONS
 // the __builtin_expect() helps us if assert is built-in or a macro
-# define cvc4assert(x) assert(__builtin_expect((x), 1))
+#  define cvc4assert(x) assert(EXPECT_TRUE( x ))
 #else
 // TODO: use a compiler annotation when assertions are off ?
 // (to improve optimization)
-# define cvc4assert(x)
-#endif /* DEBUG */
+#  define cvc4assert(x) /*EXPECT_TRUE( x )*/
+#endif /* CVC4_ASSERTIONS */
 
 #endif /* __CVC4__DEBUG_H */
diff --git a/src/util/decision_engine.cpp b/src/util/decision_engine.cpp
index ae79f920d..36f99f4ac 100644
--- a/src/util/decision_engine.cpp
+++ b/src/util/decision_engine.cpp
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** decision_engine.cpp
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
diff --git a/src/util/decision_engine.h b/src/util/decision_engine.h
index 3a093211c..58f9400b5 100644
--- a/src/util/decision_engine.h
+++ b/src/util/decision_engine.h
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** decision_engine.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -7,6 +10,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
+ ** A decision engine for CVC4.
  **/
 
 #ifndef __CVC4__DECISION_ENGINE_H
diff --git a/src/util/exception.h b/src/util/exception.h
index d239f48de..8481a8504 100644
--- a/src/util/exception.h
+++ b/src/util/exception.h
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** exception.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -7,9 +10,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
- ** Exception class.
- **
- ** As many paragraphs as you like.
+ ** CVC4's exception base class and some associated utilities.
  **/
 
 #ifndef __CVC4__EXCEPTION_H
diff --git a/src/util/literal.h b/src/util/literal.h
index 3ec216a6a..921a9ef0d 100644
--- a/src/util/literal.h
+++ b/src/util/literal.h
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** literal.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -7,6 +10,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
+ ** A literal.
  **/
 
 #ifndef __CVC4__LITERAL_H
diff --git a/src/util/model.h b/src/util/model.h
index cf006b3e1..b79032221 100644
--- a/src/util/model.h
+++ b/src/util/model.h
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** model.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -7,6 +10,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
+ ** A model.
  **/
 
 #ifndef __CVC4__MODEL_H
diff --git a/src/util/options.h b/src/util/options.h
index 8d2d113a2..2bfbf675f 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** options.h
+ ** Original author: mdeters
+ ** Major contributors: dejan
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -7,7 +10,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
- ** [[ Add file-specific comments here ]]
+ ** Global (command-line or equivalent) tuning parameters.
  **/
 
 #include <iostream>
diff --git a/src/util/output.cpp b/src/util/output.cpp
index 103a3d61a..05c74918c 100644
--- a/src/util/output.cpp
+++ b/src/util/output.cpp
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** output.cpp
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
diff --git a/src/util/output.h b/src/util/output.h
index 43dfe8a40..57ce5f3ca 100644
--- a/src/util/output.h
+++ b/src/util/output.h
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** output.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
diff --git a/src/util/result.h b/src/util/result.h
index 8d9b93a1e..87686d59c 100644
--- a/src/util/result.h
+++ b/src/util/result.h
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** result.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -7,6 +10,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
+ ** Encapsulation of the result of a query.
  **/
 
 #ifndef __CVC4__RESULT_H
diff --git a/src/util/unique_id.h b/src/util/unique_id.h
index 4ac80f772..633a544f0 100644
--- a/src/util/unique_id.h
+++ b/src/util/unique_id.h
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** unique_id.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -7,6 +10,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
+ ** A mechanism for getting a compile-time unique ID.
  **/
 
 #ifndef __CVC4__UNIQUE_ID_H