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

16 files changed, 102 insertions, 21 deletions

diff --git a/src/expr/attr_type.h b/src/expr/attr_type.h
index 597be0fe7..7fa828237 100644
--- a/src/expr/attr_type.h
+++ b/src/expr/attr_type.h
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** attr_type.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): dejan, taking
  ** 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.
  **
+ ** Node attribute describing the type of a node.
  **/
 
 #ifndef __CVC4__EXPR__ATTR_TYPE_H
diff --git a/src/expr/attr_var_name.h b/src/expr/attr_var_name.h
index 13a2ec36f..a17a3ba18 100644
--- a/src/expr/attr_var_name.h
+++ b/src/expr/attr_var_name.h
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
-/** attr_type.h
+/** attr_var_name.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): dejan
  ** 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.
  **
+ ** The node attribute describing variable names.
  **/
 
 #ifndef __CVC4__EXPR__ATTR_VAR_NAME_H
diff --git a/src/expr/expr.cpp b/src/expr/expr.cpp
index eacd1cb24..ee9334f3c 100644
--- a/src/expr/expr.cpp
+++ b/src/expr/expr.cpp
@@ -1,9 +1,17 @@
-/*
- * expr.cpp
- *
- *  Created on: Dec 10, 2009
- *      Author: dejan
- */
+/*********************                                           -*- C++ -*-  */
+/** expr.cpp
+ ** Original author: dejan
+ ** Major contributors: none
+ ** Minor contributors (to current version): taking
+ ** 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 ]]
+ **/
 
 #include "expr/expr.h"
 #include "expr/node.h"
diff --git a/src/expr/expr.h b/src/expr/expr.h
index a0a646900..447c35f77 100644
--- a/src/expr/expr.h
+++ b/src/expr/expr.h
@@ -1,9 +1,17 @@
-/*
- * expr.h
- *
- *  Created on: Dec 10, 2009
- *      Author: dejan
- */
+/*********************                                           -*- C++ -*-  */
+/** expr.h
+ ** Original author: dejan
+ ** Major contributors: none
+ ** Minor contributors (to current version): taking, mdeters
+ ** 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.
+ **
+ ** Public-facing expression interface.
+ **/
 
 #ifndef __CVC4__EXPR_H
 #define __CVC4__EXPR_H
diff --git a/src/expr/expr_manager.cpp b/src/expr/expr_manager.cpp
index ea1649e12..ea1ade477 100644
--- a/src/expr/expr_manager.cpp
+++ b/src/expr/expr_manager.cpp
@@ -1,3 +1,18 @@
+/*********************                                           -*- C++ -*-  */
+/** expr_manager.cpp
+ ** Original author: dejan
+ ** Major contributors: none
+ ** Minor contributors (to current version): mdeters
+ ** 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 ]]
+ **/
+
 /*
  * expr_manager.cpp
  *
diff --git a/src/expr/expr_manager.h b/src/expr/expr_manager.h
index 645193ecf..ace8b2d1c 100644
--- a/src/expr/expr_manager.h
+++ b/src/expr/expr_manager.h
@@ -1,9 +1,17 @@
-/*
- * expr_manager.h
- *
- *  Created on: Dec 10, 2009
- *      Author: dejan
- */
+/*********************                                           -*- C++ -*-  */
+/** expr_manager.h
+ ** Original author: dejan
+ ** Major contributors: none
+ ** Minor contributors (to current version): taking
+ ** 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.
+ **
+ ** Public-facing expression manager interface.
+ **/
 
 #ifndef __CVC4__EXPR_MANAGER_H
 #define __CVC4__EXPR_MANAGER_H
diff --git a/src/expr/kind.h b/src/expr/kind.h
index 624ab7337..ea9dbd662 100644
--- a/src/expr/kind.h
+++ b/src/expr/kind.h
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** kind.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): dejan
  ** 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.
  **
+ ** Kinds of Nodes.
  **/
 
 #ifndef __CVC4__KIND_H
diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index 334cf1b0e..9c73b982c 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** node.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
diff --git a/src/expr/node.h b/src/expr/node.h
index aad0689bb..9bb138b21 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** node.h
+ ** Original author: mdeters
+ ** Major contributors: dejan
+ ** Minor contributors (to current version): taking
  ** 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.
  **
- ** Reference-counted encapsulation of a pointer to an expression.
+ ** Reference-counted encapsulation of a pointer to node information.
  **/
 
 #include "expr/node_value.h"
diff --git a/src/expr/node_attribute.h b/src/expr/node_attribute.h
index 0b759efb4..021e64649 100644
--- a/src/expr/node_attribute.h
+++ b/src/expr/node_attribute.h
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
-/** expr_attribute.h
+/** node_attribute.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,6 +10,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
+ ** Node attributes.
  **/
 
 #ifndef __CVC4__EXPR__NODE_ATTRIBUTE_H
diff --git a/src/expr/node_builder.cpp b/src/expr/node_builder.cpp
index 0a36421f2..9e24fa280 100644
--- a/src/expr/node_builder.cpp
+++ b/src/expr/node_builder.cpp
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** node_builder.cpp
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): dejan
  ** 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/expr/node_builder.h b/src/expr/node_builder.h
index 63048c1ac..b974ecc67 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** node_builder.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): dejan
  ** 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 builder interface for nodes.
  **/
 
 #ifndef __CVC4__NODE_BUILDER_H
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 7e871d9c3..d752db88f 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** node_manager.cpp
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): dejan
  ** 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/expr/node_manager.h b/src/expr/node_manager.h
index 643f09f11..827c6c1b7 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** node_manager.h
+ ** Original author: mdeters
+ ** Major contributors: dejan
+ ** Minor contributors (to current version): taking
  ** 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 manager for Nodes.
  **/
 
 #ifndef __CVC4__NODE_MANAGER_H
diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp
index 42b7b05e4..6724b0771 100644
--- a/src/expr/node_value.cpp
+++ b/src/expr/node_value.cpp
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** node_value.cpp
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): dejan
  ** 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/expr/node_value.h b/src/expr/node_value.h
index 75c694ec9..352be7d27 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** node_value.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