another pass

25 files changed, 109 insertions, 64 deletions

diff --git a/src/include/assert.h b/src/include/assert.h
index 473cd21f1..a66503641 100644
--- a/src/include/assert.h
+++ b/src/include/assert.h
@@ -1,10 +1,12 @@
 /*********************                                           -*- C++ -*-  */
 /** assert.h
  ** This file is part of the CVC4 prototype.
- **
- ** The Analysis of Computer Systems Group (ACSys)
+ ** 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.
+ **
  **/
 
 #ifndef __CVC4_ASSERT_H
diff --git a/src/include/attr_type.h b/src/include/attr_type.h
index e5eb222fe..d24385f8e 100644
--- a/src/include/attr_type.h
+++ b/src/include/attr_type.h
@@ -1,10 +1,12 @@
 /*********************                                           -*- C++ -*-  */
 /** attr_type.h
  ** This file is part of the CVC4 prototype.
- **
- ** The Analysis of Computer Systems Group (ACSys)
+ ** 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.
+ **
  **/
 
 #ifndef __CVC4_ATTR_TYPE_H
diff --git a/src/include/command.h b/src/include/command.h
index 45b59a95b..944b9c621 100644
--- a/src/include/command.h
+++ b/src/include/command.h
@@ -1,10 +1,12 @@
 /*********************                                           -*- C++ -*-  */
 /** command.h
  ** This file is part of the CVC4 prototype.
- **
- ** The Analysis of Computer Systems Group (ACSys)
+ ** 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.
+ **
  **/
 
 #ifndef __CVC4_COMMAND_H
diff --git a/src/include/context.h b/src/include/context.h
index 1997e63d6..fce2f0b8d 100644
--- a/src/include/context.h
+++ b/src/include/context.h
@@ -1,10 +1,12 @@
 /*********************                                           -*- C++ -*-  */
 /** context.h
  ** This file is part of the CVC4 prototype.
- **
- ** The Analysis of Computer Systems Group (ACSys)
+ ** 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.
+ **
  **/
 
 #ifndef __CVC4_CONTEXT_H
diff --git a/src/include/debug.h b/src/include/debug.h
index 95e705bcb..36942d1ae 100644
--- a/src/include/debug.h
+++ b/src/include/debug.h
@@ -1,10 +1,12 @@
 /*********************                                           -*- C++ -*-  */
 /** debug.h
  ** This file is part of the CVC4 prototype.
- **
- ** The Analysis of Computer Systems Group (ACSys)
+ ** 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.
+ **
  **/
 
 #ifndef __CVC4_DEBUG_H
diff --git a/src/include/decision_engine.h b/src/include/decision_engine.h
index 8745adad5..ec0172535 100644
--- a/src/include/decision_engine.h
+++ b/src/include/decision_engine.h
@@ -1,17 +1,19 @@
 /*********************                                           -*- C++ -*-  */
 /** decision_engine.h
  ** This file is part of the CVC4 prototype.
- **
- ** The Analysis of Computer Systems Group (ACSys)
+ ** 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.
+ **
  **/
 
-#include "literal.h"
-
 #ifndef __CVC4_DECISION_ENGINE_H
 #define __CVC4_DECISION_ENGINE_H
 
+#include "literal.h"
+
 namespace CVC4 {
 
 // In terms of abstraction, this is below (and provides services to)
diff --git a/src/include/exception.h b/src/include/exception.h
index ce19b0d68..792a98701 100644
--- a/src/include/exception.h
+++ b/src/include/exception.h
@@ -1,12 +1,13 @@
 /*********************                                           -*- C++ -*-  */
 /** exception.h
  ** This file is part of the CVC4 prototype.
- **
- ** Exception class.
- **
- ** The Analysis of Computer Systems Group (ACSys)
+ ** 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.
+ **
+ ** Exception class.
  **/
 
 #ifndef __CVC4_EXCEPTION_H
diff --git a/src/include/expr.h b/src/include/expr.h
index 9ca449ce7..e92ece93d 100644
--- a/src/include/expr.h
+++ b/src/include/expr.h
@@ -1,12 +1,13 @@
 /*********************                                           -*- C++ -*-  */
 /** expr.h
  ** This file is part of the CVC4 prototype.
- **
- ** Reference-counted encapsulation of a pointer to an expression.
- **
- ** The Analysis of Computer Systems Group (ACSys)
+ ** 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.
+ **
+ ** Reference-counted encapsulation of a pointer to an expression.
  **/
 
 #ifndef __CVC4_EXPR_H
diff --git a/src/include/expr_attribute.h b/src/include/expr_attribute.h
index 1c10a6663..77700096e 100644
--- a/src/include/expr_attribute.h
+++ b/src/include/expr_attribute.h
@@ -1,10 +1,12 @@
 /*********************                                           -*- C++ -*-  */
 /** expr_attribute.h
  ** This file is part of the CVC4 prototype.
- **
- ** The Analysis of Computer Systems Group (ACSys)
+ ** 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.
+ **
  **/
 
 #ifndef __CVC4_EXPR_ATTRIBUTE_H
diff --git a/src/include/expr_builder.h b/src/include/expr_builder.h
index 342834e37..a95ecb2e3 100644
--- a/src/include/expr_builder.h
+++ b/src/include/expr_builder.h
@@ -1,10 +1,12 @@
 /*********************                                           -*- C++ -*-  */
 /** expr_builder.h
  ** This file is part of the CVC4 prototype.
- **
- ** The Analysis of Computer Systems Group (ACSys)
+ ** 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.
+ **
  **/
 
 #ifndef __CVC4_EXPR_BUILDER_H
diff --git a/src/include/expr_manager.h b/src/include/expr_manager.h
index 5dae5b854..59a3eb7a3 100644
--- a/src/include/expr_manager.h
+++ b/src/include/expr_manager.h
@@ -1,10 +1,12 @@
 /*********************                                           -*- C++ -*-  */
 /** expr_manager.h
  ** This file is part of the CVC4 prototype.
- **
- ** The Analysis of Computer Systems Group (ACSys)
+ ** 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.
+ **
  **/
 
 #ifndef __CVC4_EXPR_MANAGER_H
diff --git a/src/include/expr_value.h b/src/include/expr_value.h
index c15241ebf..ea14c3fa7 100644
--- a/src/include/expr_value.h
+++ b/src/include/expr_value.h
@@ -1,16 +1,17 @@
-/*********************
+/*********************                                           -*- C++ -*-  */
 /** expr_value.h
  ** 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.
  **
  ** An expression node.
  **
  ** Instances of this class are generally referenced through
  ** cvc4::Expr rather than by pointer; cvc4::Expr maintains the
  ** reference count on ExprValue instances and
- **
- ** The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
  **/
 
 #ifndef __CVC4_EXPR_VALUE_H
diff --git a/src/include/kind.h b/src/include/kind.h
index a015a6b71..5d99330ca 100644
--- a/src/include/kind.h
+++ b/src/include/kind.h
@@ -1,10 +1,12 @@
 /*********************                                           -*- C++ -*-  */
 /** kind.h
  ** This file is part of the CVC4 prototype.
- **
- ** The Analysis of Computer Systems Group (ACSys)
+ ** 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.
+ **
  **/
 
 #ifndef __CVC4_KIND_H
diff --git a/src/include/literal.h b/src/include/literal.h
index 93855edb8..8b147c640 100644
--- a/src/include/literal.h
+++ b/src/include/literal.h
@@ -1,10 +1,12 @@
 /*********************                                           -*- C++ -*-  */
 /** literal.h
  ** This file is part of the CVC4 prototype.
- **
- ** The Analysis of Computer Systems Group (ACSys)
+ ** 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.
+ **
  **/
 
 #ifndef __CVC4_LITERAL_H
diff --git a/src/include/model.h b/src/include/model.h
index 205dcf18f..c07b75dfa 100644
--- a/src/include/model.h
+++ b/src/include/model.h
@@ -1,10 +1,12 @@
 /*********************                                           -*- C++ -*-  */
 /** model.h
  ** This file is part of the CVC4 prototype.
- **
- ** The Analysis of Computer Systems Group (ACSys)
+ ** 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.
+ **
  **/
 
 #ifndef __CVC4_MODEL_H
diff --git a/src/include/parser.h b/src/include/parser.h
index 63a448b28..e30b31b1c 100644
--- a/src/include/parser.h
+++ b/src/include/parser.h
@@ -1,12 +1,13 @@
 /*********************                                           -*- C++ -*-  */
 /** parser.h
  ** This file is part of the CVC4 prototype.
- **
- ** Parser abstraction.
- **
- ** The Analysis of Computer Systems Group (ACSys)
+ ** 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.
+ **
+ ** Parser abstraction.
  **/
 
 #ifndef __CVC4_PARSER_H
diff --git a/src/include/parser_exception.h b/src/include/parser_exception.h
index 8bad801f4..debb75e70 100644
--- a/src/include/parser_exception.h
+++ b/src/include/parser_exception.h
@@ -1,12 +1,13 @@
 /*********************                                           -*- C++ -*-  */
-/** exception.h
+/** parser_exception.h
  ** This file is part of the CVC4 prototype.
- **
- ** Exception class.
- **
- ** The Analysis of Computer Systems Group (ACSys)
+ ** 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.
+ **
+ ** Exception class.
  **/
 
 #ifndef __CVC4_PARSER_EXCEPTION_H
diff --git a/src/include/prop_engine.h b/src/include/prop_engine.h
index 90d07a47b..de25c5594 100644
--- a/src/include/prop_engine.h
+++ b/src/include/prop_engine.h
@@ -1,10 +1,12 @@
 /*********************                                           -*- C++ -*-  */
 /** prop_engine.h
  ** This file is part of the CVC4 prototype.
- **
- ** The Analysis of Computer Systems Group (ACSys)
+ ** 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.
+ **
  **/
 
 #ifndef __CVC4_PROP_ENGINE_H
diff --git a/src/include/prover.h b/src/include/prover.h
index e48d6336c..de29f48c0 100644
--- a/src/include/prover.h
+++ b/src/include/prover.h
@@ -1,10 +1,12 @@
 /*********************                                           -*- C++ -*-  */
 /** prover.h
  ** This file is part of the CVC4 prototype.
- **
- ** The Analysis of Computer Systems Group (ACSys)
+ ** 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.
+ **
  **/
 
 #ifndef __CVC4_PROVER_H
diff --git a/src/include/result.h b/src/include/result.h
index cfabd3be2..50f488682 100644
--- a/src/include/result.h
+++ b/src/include/result.h
@@ -1,10 +1,12 @@
 /*********************                                           -*- C++ -*-  */
 /** result.h
  ** This file is part of the CVC4 prototype.
- **
- ** The Analysis of Computer Systems Group (ACSys)
+ ** 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.
+ **
  **/
 
 #ifndef __CVC4_RESULT_H
diff --git a/src/include/sat.h b/src/include/sat.h
index 13578ec8d..00a94c142 100644
--- a/src/include/sat.h
+++ b/src/include/sat.h
@@ -1,10 +1,12 @@
 /*********************                                           -*- C++ -*-  */
 /** sat.h
  ** This file is part of the CVC4 prototype.
- **
- ** The Analysis of Computer Systems Group (ACSys)
+ ** 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.
+ **
  **/
 
 #ifndef __CVC4_SAT_H
diff --git a/src/include/theory.h b/src/include/theory.h
index 5c50c7a37..935c23b08 100644
--- a/src/include/theory.h
+++ b/src/include/theory.h
@@ -1,10 +1,12 @@
 /*********************                                           -*- C++ -*-  */
 /** theory.h
  ** This file is part of the CVC4 prototype.
- **
- ** The Analysis of Computer Systems Group (ACSys)
+ ** 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.
+ **
  **/
 
 #ifndef __CVC4_THEORY_H
diff --git a/src/include/theory_engine.h b/src/include/theory_engine.h
index f4e36f604..2a0841d8d 100644
--- a/src/include/theory_engine.h
+++ b/src/include/theory_engine.h
@@ -1,10 +1,12 @@
 /*********************                                           -*- C++ -*-  */
 /** theory_engine.h
  ** This file is part of the CVC4 prototype.
- **
- ** The Analysis of Computer Systems Group (ACSys)
+ ** 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.
+ **
  **/
 
 #ifndef __CVC4_THEORY_ENGINE_H
diff --git a/src/include/unique_id.h b/src/include/unique_id.h
index 55fa24e51..1a6f3427a 100644
--- a/src/include/unique_id.h
+++ b/src/include/unique_id.h
@@ -1,10 +1,12 @@
 /*********************                                           -*- C++ -*-  */
 /** unique_id.h
  ** This file is part of the CVC4 prototype.
- **
- ** The Analysis of Computer Systems Group (ACSys)
+ ** 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.
+ **
  **/
 
 #ifndef __CVC4_UNIQUE_ID_H
diff --git a/src/include/vc.h b/src/include/vc.h
index 57d8a957e..845d1eb6d 100644
--- a/src/include/vc.h
+++ b/src/include/vc.h
@@ -1,10 +1,12 @@
 /*********************                                           -*- C++ -*-  */
 /** vc.h
  ** This file is part of the CVC4 prototype.
- **
- ** The Analysis of Computer Systems Group (ACSys)
+ ** 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.
+ **
  **/
 
 #ifndef __CVC4_VC_H