file header documentation regenerated with contributors names; no code modified in...

diff --git a/src/context/cdmap.h b/src/context/cdmap.h
index 0b75ee2845c81c509a18036b72536cfca05ca7e8..76c05fd4df5eb33df9f414f7d27bb633cfa45015 100644 (file)
--- a/src/context/cdmap.h
+++ b/src/context/cdmap.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: none
- ** Minor contributors (to current version): dejan
+ ** Minor contributors (to current version): taking, dejan
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/context/cdvector.h b/src/context/cdvector.h
index 0076d509fcfbc9861ce2d765f4fdad88deb79815..cb86d5c4d1ebfed34885660578f99f049666ea9c 100644 (file)
--- a/src/context/cdvector.h
+++ b/src/context/cdvector.h
@@ -2,7 +2,7 @@
 /*! \file cdvector.h
  ** \verbatim
  ** Original author: taking
- ** Major contributors: none
+ ** Major contributors: mdeters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 04ebfa94f10b6660962a1f20c7de81901688ff80..3fd3cce28bc8b886da62028f2db5fd9095f4f97c 100644 (file)
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -2,7 +2,7 @@
 /*! \file expr_manager_template.cpp
  ** \verbatim
  ** Original author: dejan
- ** Major contributors: cconway, mdeters
+ ** Major contributors: mdeters, cconway
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)

diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index aaaaf0026fbd9d6ef6b4881b0a52d7e7485be665..8e02c8ca426f23044f0bcec1de04f7c290444675 100644 (file)
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -2,8 +2,8 @@
 /*! \file expr_manager_template.h
  ** \verbatim
  ** Original author: dejan
- ** Major contributors: cconway, mdeters
- ** Minor contributors (to current version): taking
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): taking, cconway
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index becdd46e23ecdece751f5455b5fce70ee5ff2e11..15938b16087da919a07df97c7b9e92e7399cdc82 100644 (file)
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: dejan
  ** Major contributors: mdeters
- ** Minor contributors (to current version): cconway, taking
+ ** Minor contributors (to current version): taking, cconway
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  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 8b64dc781dc1e36d7a9bdd15d7301eb5d66fc6cc..b5f6307ed711aeacc68ebba723db0eb200dcbfd0 100644 (file)
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -2,8 +2,8 @@
 /*! \file node.h
  ** \verbatim
  ** Original author: mdeters
- ** Major contributors: cconway, dejan
- ** Minor contributors (to current version): taking
+ ** Major contributors: dejan
+ ** Minor contributors (to current version): taking, cconway
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 5d99fb31ef638dc74b70493a7e370b4070926494..942906fbde44e36ade6f5e306755b2b59c37cff3 100644 (file)
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -2,8 +2,8 @@
 /*! \file node_manager.cpp
  ** \verbatim
  ** Original author: mdeters
- ** Major contributors: dejan
- ** Minor contributors (to current version): taking, cconway
+ ** Major contributors: cconway, dejan
+ ** Minor contributors (to current version): acsys, taking
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  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 4f658c507cc60eb1268db168e96760acf6bd7218..77f00ab33eb43fa67a0a36dce32d66da5f3b4745 100644 (file)
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: cconway, dejan
- ** Minor contributors (to current version): taking
+ ** Minor contributors (to current version): acsys, taking
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/lib/clock_gettime.c b/src/lib/clock_gettime.c
index 682269458904012c8f9d2d2ebc0604ad304e95ec..b1bc24ed894ecd59a65bceaf821355ec65ac46d7 100644 (file)
--- a/src/lib/clock_gettime.c
+++ b/src/lib/clock_gettime.c
@@ -1,7 +1,7 @@
 /*********************                                                        */
 /*! \file clock_gettime.c
  ** \verbatim
- ** Original author: 
+ ** Original author: mdeters
  ** Major contributors: none
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.

diff --git a/src/lib/clock_gettime.h b/src/lib/clock_gettime.h
index aac80dadf85756264a22fb8ad6419ca30bca1379..e419e16b064fe3c8a4b474191c8099da476f7cd8 100644 (file)
--- a/src/lib/clock_gettime.h
+++ b/src/lib/clock_gettime.h
@@ -1,7 +1,7 @@
 /*********************                                                        */
 /*! \file clock_gettime.h
  ** \verbatim
- ** Original author: 
+ ** Original author: mdeters
  ** Major contributors: none
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.

diff --git a/src/lib/replacements.h b/src/lib/replacements.h
index d38331b669f230cea41f9c1802d17d5b73ad2983..c930d2654184299deaa3a209c078eac3a1e48100 100644 (file)
--- a/src/lib/replacements.h
+++ b/src/lib/replacements.h
@@ -1,7 +1,7 @@
 /*********************                                                        */
 /*! \file replacements.h
  ** \verbatim
- ** Original author: 
+ ** Original author: mdeters
  ** Major contributors: none
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.

diff --git a/src/main/main.cpp b/src/main/main.cpp
index 950e991c63738a8886ae44fbcc065ef89af1314a..f0c04e5f698394fb6bb8712c5b2ae781dc9a5358 100644 (file)
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -2,8 +2,8 @@
 /*! \file main.cpp
  ** \verbatim
  ** Original author: mdeters
- ** Major contributors: cconway
- ** Minor contributors (to current version): barrett, dejan, taking
+ ** Major contributors: taking, cconway
+ ** Minor contributors (to current version): barrett, dejan
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/main/util.cpp b/src/main/util.cpp
index 65f6ed329e3ab33b803961640195858d56b957ed..760bd52581331a008b60e35ad807304ee56158aa 100644 (file)
--- a/src/main/util.cpp
+++ b/src/main/util.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): acsys
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/parser/bounded_token_buffer.h b/src/parser/bounded_token_buffer.h
index 289480e2da6761cb56789f9c7eaf16c29a79820e..fad5edc1ee7f82e23a68cb4880d1a19c909d86ee 100644 (file)
--- a/src/parser/bounded_token_buffer.h
+++ b/src/parser/bounded_token_buffer.h
@@ -2,8 +2,8 @@
 /*! \file bounded_token_buffer.h
  ** \verbatim
  ** Original author: cconway
- ** Major contributors: none
- ** Minor contributors (to current version): mdeters
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/parser/smt/smt.cpp b/src/parser/smt/smt.cpp
index 2e0e0087c75f16e99aef0d5d113cadb9293f73ca..1bb8f0679cc2b1d25490c96ff9c699c3b44f6612 100644 (file)
--- a/src/parser/smt/smt.cpp
+++ b/src/parser/smt/smt.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: cconway
  ** Major contributors: none
- ** Minor contributors (to current version): mdeters
+ ** Minor contributors (to current version): mdeters, dejan
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/parser/smt2/smt2_input.cpp b/src/parser/smt2/smt2_input.cpp
index cbb9c57a3481fb9e1eb04e26d1bfaa1dd8a49444..9a349785cec20359cb12f8c1483292df3a89ac41 100644 (file)
--- a/src/parser/smt2/smt2_input.cpp
+++ b/src/parser/smt2/smt2_input.cpp
@@ -2,8 +2,8 @@
 /*! \file smt2_input.cpp
  ** \verbatim
  ** Original author: cconway
- ** Major contributors: none
- ** Minor contributors (to current version): mdeters
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index c719c66da266f54bca0f481e54bd9ed9da5372dd..7b986cf83522c601d8886d318f8276c008f246e7 100644 (file)
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: taking
  ** Major contributors: dejan
- ** Minor contributors (to current version): mdeters, cconway
+ ** Minor contributors (to current version): cconway, mdeters
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/prop/sat.h b/src/prop/sat.h
index 63c17f5130507ee3840d3b1cfdbb2ab8a044361c..d780230a8c4013c84bd117bff22858a36a343c09 100644 (file)
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -2,8 +2,8 @@
 /*! \file sat.h
  ** \verbatim
  ** Original author: mdeters
- ** Major contributors: taking, dejan, cconway
- ** Minor contributors (to current version): none
+ ** Major contributors: taking, cconway, dejan
+ ** Minor contributors (to current version): barrett
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp
index 14c52526729b53c0ff4b48ce344ca3c8d9b1b954..60f6fa022aafdd32cf5bfdcde9468fcf5b9cb8d0 100644 (file)
--- a/src/theory/arith/normal_form.cpp
+++ b/src/theory/arith/normal_form.cpp
@@ -2,7 +2,7 @@
 /*! \file normal_form.cpp
  ** \verbatim
  ** Original author: taking
- ** Major contributors: none
+ ** Major contributors: mdeters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)

diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h
index a09437160b2a8122f68346fc96c76b61983d66f3..2e20c62c5b2345c7f32b6d0371977c4a65f5ed21 100644 (file)
--- a/src/theory/arith/normal_form.h
+++ b/src/theory/arith/normal_form.h
@@ -2,7 +2,7 @@
 /*! \file normal_form.h
  ** \verbatim
  ** Original author: taking
- ** Major contributors: none
+ ** Major contributors: mdeters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)

diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp
index e43458a23a81a3508851925bec2518d51fc7030c..df80c11183a9b5065a7cfb478f93a7004949f3db 100644 (file)
--- a/src/theory/arith/tableau.cpp
+++ b/src/theory/arith/tableau.cpp
@@ -1,3 +1,22 @@
+/*********************                                                        */
+/*! \file tableau.cpp
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  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
+ **/
+
 
 #include "theory/arith/tableau.h"
 

diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h
index dc2c199368be685f641809f52a31f901693e8474..ed173a1826c2341fe009baad67bf0174ba1536bb 100644 (file)
--- a/src/theory/arith/tableau.h
+++ b/src/theory/arith/tableau.h
@@ -2,8 +2,8 @@
 /*! \file tableau.h
  ** \verbatim
  ** Original author: taking
- ** Major contributors: none
- ** Minor contributors (to current version): dejan, mdeters
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): dejan
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 8b5f7d3e765c4d440b41db90fec645124619e4f8..8997138cb9172680b7bfd35a80570f923c97793a 100644 (file)
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: barrett
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): mdeters
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/theory/arrays/theory_arrays_type_rules.h b/src/theory/arrays/theory_arrays_type_rules.h
index 5d0713a894773456fa4ea02f1e19dbca7d2a0358..25083688ab2f574acc7919302f75bf3a8b13b18f 100644 (file)
--- a/src/theory/arrays/theory_arrays_type_rules.h
+++ b/src/theory/arrays/theory_arrays_type_rules.h
@@ -2,7 +2,7 @@
 /*! \file theory_arrays_type_rules.h
  ** \verbatim
  ** Original author: mdeters
- ** Major contributors: none
+ ** Major contributors: cconway
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)

diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h
index f492041b8a2db9e121b99df02594eb0dbcd32bbb..d87aa95b5b06a3cc40c6d58ef9c4b8985740c720 100644 (file)
--- a/src/theory/booleans/theory_bool.h
+++ b/src/theory/booleans/theory_bool.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: taking
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): barrett
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/theory/booleans/theory_bool_type_rules.h b/src/theory/booleans/theory_bool_type_rules.h
index fddced8efc702ac35c4fbf5f3b9554eb84a883ef..20dd56fa780b73b57ce5b87a7c90c33262f75a67 100644 (file)
--- a/src/theory/booleans/theory_bool_type_rules.h
+++ b/src/theory/booleans/theory_bool_type_rules.h
@@ -2,7 +2,7 @@
 /*! \file theory_bool_type_rules.h
  ** \verbatim
  ** Original author: dejan
- ** Major contributors: mdeters
+ ** Major contributors: mdeters, cconway
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)

diff --git a/src/theory/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h
index e76b3fb4b19bcec8e90ca2ef8d819e71ccef4041..a08ed9b780165b347cad939165b09f0d77906399 100644 (file)
--- a/src/theory/builtin/theory_builtin.h
+++ b/src/theory/builtin/theory_builtin.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): barrett
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index 42c9902e581f0bbe1fa9f135714c1a84b30406c0..5d1137d27c71ae5c297c0e1276214465eadff651 100644 (file)
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -2,8 +2,8 @@
 /*! \file theory_builtin_type_rules.h
  ** \verbatim
  ** Original author: dejan
- ** Major contributors: mdeters
- ** Minor contributors (to current version): taking
+ ** Major contributors: cconway, mdeters
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/theory/bv/equality_engine.cpp b/src/theory/bv/equality_engine.cpp
index b88a3cc863433ee797ed4f3efa0e530e74efff76..fa0650506ebd01947c19f043dfd710870773672a 100644 (file)
--- a/src/theory/bv/equality_engine.cpp
+++ b/src/theory/bv/equality_engine.cpp
@@ -1,3 +1,22 @@
+/*********************                                                        */
+/*! \file equality_engine.cpp
+ ** \verbatim
+ ** Original author: dejan
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  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
+ **/
+
 #include "equality_engine.h"
 
 using namespace CVC4::theory::bv;

diff --git a/src/theory/bv/equality_engine.h b/src/theory/bv/equality_engine.h
index 9f3064483432cfa6b8ec3e2ccdaf3c888b6dc9af..8f596723cc6435ffc4f40f7dd882dd06678af04e 100644 (file)
--- a/src/theory/bv/equality_engine.h
+++ b/src/theory/bv/equality_engine.h
@@ -1,3 +1,22 @@
+/*********************                                                        */
+/*! \file equality_engine.h
+ ** \verbatim
+ ** Original author: dejan
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  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
+ **/
+
 #include "cvc4_private.h"
 
 #pragma once

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index f957c4f49b45c7499a531c5331e28920063265ed..bd0d738657c9e3e3c77c2064b908bd6297dbb738 100644 (file)
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -1,3 +1,22 @@
+/*********************                                                        */
+/*! \file theory_bv.cpp
+ ** \verbatim
+ ** Original author: dejan
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  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
+ **/
+
 #include "theory_bv.h"
 #include "theory_bv_utils.h"
 #include "theory_bv_rewrite_rules.h"

diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index b712337976daecc2e2d3631e00784cedba1150ed..ff5d4c2a25aa1e339dfa1444970e0cf02395a18d 100644 (file)
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -2,8 +2,8 @@
 /*! \file theory_bv.h
  ** \verbatim
  ** Original author: mdeters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Major contributors: dejan
+ ** Minor contributors (to current version): barrett
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/theory/bv/theory_bv_rewrite_rules.cpp b/src/theory/bv/theory_bv_rewrite_rules.cpp
index 8c5dfc415de354672918f8e67245d9b5bfa67371..637a4269d040a73a362f39481d3c5172c1b56150 100644 (file)
--- a/src/theory/bv/theory_bv_rewrite_rules.cpp
+++ b/src/theory/bv/theory_bv_rewrite_rules.cpp
@@ -1,3 +1,22 @@
+/*********************                                                        */
+/*! \file theory_bv_rewrite_rules.cpp
+ ** \verbatim
+ ** Original author: dejan
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  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
+ **/
+
 #include <vector>
 #include "expr/node_builder.h"
 #include "theory_bv_rewrite_rules.h"

diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h
index ea396e32cec361c9523df9be60ace022c6ad97e0..eba8f917c8af004949bc6a3e7d539a2b6e8d512d 100644 (file)
--- a/src/theory/bv/theory_bv_rewrite_rules.h
+++ b/src/theory/bv/theory_bv_rewrite_rules.h
@@ -1,3 +1,22 @@
+/*********************                                                        */
+/*! \file theory_bv_rewrite_rules.h
+ ** \verbatim
+ ** Original author: dejan
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  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
+ **/
+
 #pragma once 
 
 #include "cvc4_private.h"

diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h
index 7c4ff495e099eea0ecb6e731b2dcd29f3ee5a517..49b2105011f5b610e77082ca76509c703f3a1541 100644 (file)
--- a/src/theory/bv/theory_bv_type_rules.h
+++ b/src/theory/bv/theory_bv_type_rules.h
@@ -2,8 +2,8 @@
 /*! \file theory_bv_type_rules.h
  ** \verbatim
  ** Original author: dejan
- ** Major contributors: mdeters
- ** Minor contributors (to current version): none
+ ** Major contributors: cconway
+ ** Minor contributors (to current version): mdeters
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index ce829870204d667cdb48dc890e86b098b24c52bb..6e9dbef3e66ccf5d5fed17963b014a41b705d757 100644 (file)
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -1,3 +1,22 @@
+/*********************                                                        */
+/*! \file theory_bv_utils.h
+ ** \verbatim
+ ** Original author: dejan
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  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
+ **/
+
 #pragma once 
 
 #include <vector>

diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h
index ab94fbcc8309ee1246d170d53791b31f0f2072b7..fb2fde5894a9a75aeca89e5d80553f5a06058018 100644 (file)
--- a/src/theory/output_channel.h
+++ b/src/theory/output_channel.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: taking
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): barrett
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/theory/shared_term_manager.h b/src/theory/shared_term_manager.h
index 8b5567e4e083e6408adfb899d42b18f8fd11ea72..49bd447d71d9fefbc49d1c4bdd88cd16572911b6 100644 (file)
--- a/src/theory/shared_term_manager.h
+++ b/src/theory/shared_term_manager.h
@@ -2,8 +2,8 @@
 /*! \file shared_term_manager.h
  ** \verbatim
  ** Original author: barrett
- ** Major contributors: 
- ** Minor contributors (to current version): 
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/theory/theory.h b/src/theory/theory.h
index 1cce09439eb23cf9f9015e8c1027b104a27a3e66..2711a0b95c825558eb0fdd4a0699442eb8adc022 100644 (file)
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: none
- ** Minor contributors (to current version): dejan, taking
+ ** Minor contributors (to current version): dejan, taking, barrett
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index da161097fc565e91043eab21482ce2ce2b7bd5d7..041b6852bc659038725075c45ac7b9d0e695b642 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -2,8 +2,8 @@
 /*! \file theory_engine.cpp
  ** \verbatim
  ** Original author: mdeters
- ** Major contributors: taking
- ** Minor contributors (to current version): none
+ ** Major contributors: barrett
+ ** Minor contributors (to current version): cconway, taking
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 074d40d05104b7cd22178138ad47b4ab9be7333d..5227d32f02ba95f0cccbfd83c2468379490de844 100644 (file)
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: dejan, taking
- ** Minor contributors (to current version): cconway
+ ** Minor contributors (to current version): cconway, barrett
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/theory/uf/morgan/theory_uf_morgan.cpp b/src/theory/uf/morgan/theory_uf_morgan.cpp
index a0b4651bb9017178a5df1a84423160b161bfa752..eb6c430ba6845c90a5491326f32d63093a9e6b9f 100644 (file)
--- a/src/theory/uf/morgan/theory_uf_morgan.cpp
+++ b/src/theory/uf/morgan/theory_uf_morgan.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: taking
  ** Major contributors: mdeters
- ** Minor contributors (to current version): dejan
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h
index 38018112a4d1c8eff4e1f142a80a208900e38858..b0f899f9b2718ea17a47b9d7031eaa43bf1796ec 100644 (file)
--- a/src/theory/uf/theory_uf_type_rules.h
+++ b/src/theory/uf/theory_uf_type_rules.h
@@ -2,7 +2,7 @@
 /*! \file theory_uf_type_rules.h
  ** \verbatim
  ** Original author: dejan
- ** Major contributors: mdeters
+ ** Major contributors: cconway, mdeters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)

diff --git a/src/theory/uf/tim/theory_uf_tim.h b/src/theory/uf/tim/theory_uf_tim.h
index 1591cc05cb54b54275c82f09300697f0f9eed6a5..9a2d252c098e83802436709d882d9511849cc702 100644 (file)
--- a/src/theory/uf/tim/theory_uf_tim.h
+++ b/src/theory/uf/tim/theory_uf_tim.h
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file theory_uf.h
+/*! \file theory_uf_tim.h
  ** \verbatim
  ** Original author: taking
  ** Major contributors: mdeters

diff --git a/src/util/Assert.cpp b/src/util/Assert.cpp
index 1435515ad34fe23015e218174647cefcaa7ab105..cdfdb0284a10a7842f91e1302a2119af071970ef 100644 (file)
--- a/src/util/Assert.cpp
+++ b/src/util/Assert.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): acsys
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  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 65c067b7e7a8f8a8dc390440ce14ec8bc9da2e05..87db28d44b20b4083799350308e71a4f56f05d4b 100644 (file)
--- a/src/util/Assert.h
+++ b/src/util/Assert.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): acsys
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/util/configuration.cpp b/src/util/configuration.cpp
index 499b0c8e21fbc7fd76ea2d748c9f66df76c2e9cd..c1b7acd7185963d733472509bdb581530226a900 100644 (file)
--- a/src/util/configuration.cpp
+++ b/src/util/configuration.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): acsys, cconway
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/util/configuration.h b/src/util/configuration.h
index ff89a3d6ce9984823ce7eaa72c9b8180fcc89512..907cd1d31123e6a28f7d8aea6e5a623c0c6d384e 100644 (file)
--- a/src/util/configuration.h
+++ b/src/util/configuration.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): acsys
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/util/configuration_private.h b/src/util/configuration_private.h
index 227250745683546d214f0788d0c9290bc65856b0..69c22c964f86a912972b98c4234a4555618af45a 100644 (file)
--- a/src/util/configuration_private.h
+++ b/src/util/configuration_private.h
@@ -1,8 +1,8 @@
 /*********************                                                        */
 /*! \file configuration_private.h
  ** \verbatim
- ** Original author: cconway
- ** Major contributors: none
+ ** Original author: mdeters
+ ** Major contributors: cconway, acsys
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)

diff --git a/src/util/dynamic_array.h b/src/util/dynamic_array.h
index 8672fa1e9c584a2ee42779d7dba13d80f6f37e11..c1298500ecf70818dc988c9afffdfea0da542a0f 100644 (file)
--- a/src/util/dynamic_array.h
+++ b/src/util/dynamic_array.h
@@ -1,3 +1,22 @@
+/*********************                                                        */
+/*! \file dynamic_array.h
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  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
+ **/
+
 
 #include "cvc4_private.h"
 

diff --git a/src/util/integer_cln_imp.cpp b/src/util/integer_cln_imp.cpp
index a6cad96d1b18720463e8e71dd4ddc365f1a5dfa7..6925202570abfa6689ef6062dc95fbe0595d6e2a 100644 (file)
--- a/src/util/integer_cln_imp.cpp
+++ b/src/util/integer_cln_imp.cpp
@@ -2,7 +2,7 @@
 /*! \file integer_cln_imp.cpp
  ** \verbatim
  ** Original author: taking
- ** Major contributors: none
+ ** Major contributors: mdeters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)

diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h
index 233b3aa08a84ed602e32cee09dcc71fc5ed09b19..828fb26f37911e8be703b388593f19bfa19048ac 100644 (file)
--- a/src/util/integer_cln_imp.h
+++ b/src/util/integer_cln_imp.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: taking
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): mdeters, dejan
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/util/integer_gmp_imp.cpp b/src/util/integer_gmp_imp.cpp
index 112713aa5e306b2e076213045776907069501528..1c2bd7ccde63495355ecb9d2a20c4cb6ecf92d97 100644 (file)
--- a/src/util/integer_gmp_imp.cpp
+++ b/src/util/integer_gmp_imp.cpp
@@ -2,7 +2,7 @@
 /*! \file integer_gmp_imp.cpp
  ** \verbatim
  ** Original author: taking
- ** Major contributors: none
+ ** Major contributors: mdeters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)

diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h
index 4b2ab1a79f3949a751e56862da903382ec7f7fce..ecda616f4908de4f92c12f677e6656c92206449a 100644 (file)
--- a/src/util/integer_gmp_imp.h
+++ b/src/util/integer_gmp_imp.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: taking
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): dejan, mdeters
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  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 84e566e94db818cb63ef63dcfa726d59c78808ab..d722b10d1d16f42cfc7892ab4a455148716853f5 100644 (file)
--- a/src/util/output.h
+++ b/src/util/output.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: none
- ** Minor contributors (to current version): dejan, cconway
+ ** Minor contributors (to current version): cconway
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/util/rational_cln_imp.cpp b/src/util/rational_cln_imp.cpp
index 7baf8d3bf88e102e98a32b426e6850bc6c354baf..b9768e6f5e789fd0ba730f9b153082d56137788f 100644 (file)
--- a/src/util/rational_cln_imp.cpp
+++ b/src/util/rational_cln_imp.cpp
@@ -2,7 +2,7 @@
 /*! \file rational_cln_imp.cpp
  ** \verbatim
  ** Original author: taking
- ** Major contributors: none
+ ** Major contributors: mdeters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)

diff --git a/src/util/rational_cln_imp.h b/src/util/rational_cln_imp.h
index ae172f262c8f2702018ef44839c631109cfd4b28..62f4d4376effaefeafeb177941d0d8b9a492646d 100644 (file)
--- a/src/util/rational_cln_imp.h
+++ b/src/util/rational_cln_imp.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: taking
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): mdeters
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/util/rational_gmp_imp.cpp b/src/util/rational_gmp_imp.cpp
index a0af69b4c811e5daafeafd8737f45f520bcad880..0db1d2ffff9d9b4a0479fcb2eb71a9d6ff0f6ddf 100644 (file)
--- a/src/util/rational_gmp_imp.cpp
+++ b/src/util/rational_gmp_imp.cpp
@@ -2,7 +2,7 @@
 /*! \file rational_gmp_imp.cpp
  ** \verbatim
  ** Original author: taking
- ** Major contributors: none
+ ** Major contributors: mdeters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)

diff --git a/src/util/rational_gmp_imp.h b/src/util/rational_gmp_imp.h
index ce94dfe24d13beec17d888a687d9fdeb5abdca1d..e4bba78c2954be06e98528d16ea07adaf736ef54 100644 (file)
--- a/src/util/rational_gmp_imp.h
+++ b/src/util/rational_gmp_imp.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: taking
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): mdeters
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/util/stats.h b/src/util/stats.h
index 3a1b8550675af5764bee3a98e73f98c0107deeed..43b48140ed341784da7f650a12b887d087145f6c 100644 (file)
--- a/src/util/stats.h
+++ b/src/util/stats.h
@@ -2,8 +2,8 @@
 /*! \file stats.h
  ** \verbatim
  ** Original author: taking
- ** Major contributors: none
- ** Minor contributors (to current version): mdeters
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/test/unit/context/cdvector_black.h b/test/unit/context/cdvector_black.h
index 3e9a7b87bc8e589550a3aa9cbc663a7cfee8747d..37a285abe37c77fa295336f8ecbe9b84ad3d6e66 100644 (file)
--- a/test/unit/context/cdvector_black.h
+++ b/test/unit/context/cdvector_black.h
@@ -2,7 +2,7 @@
 /*! \file cdvector_black.h
  ** \verbatim
  ** Original author: taking
- ** Major contributors: none
+ ** Major contributors: mdeters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)

diff --git a/test/unit/expr/attribute_white.h b/test/unit/expr/attribute_white.h
index ea1f40eac50f0e66e817675f051953e40c45b660..5f9ea3db97cedfbb90597c071ef8d91a3226d6b4 100644 (file)
--- a/test/unit/expr/attribute_white.h
+++ b/test/unit/expr/attribute_white.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: none
- ** Minor contributors (to current version): dejan, cconway
+ ** Minor contributors (to current version): barrett, dejan, cconway
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/test/unit/expr/expr_public.h b/test/unit/expr/expr_public.h
index e000e618eaef1243c99d3cd00b5071934fd03526..32e8da287052184605b7bfa19c35412c81dab53e 100644 (file)
--- a/test/unit/expr/expr_public.h
+++ b/test/unit/expr/expr_public.h
@@ -2,7 +2,7 @@
 /*! \file expr_public.h
  ** \verbatim
  ** Original author: mdeters
- ** Major contributors: dejan
+ ** Major contributors: cconway, dejan
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)

diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h
index 131d96bb9ef5b417c70068f8c97f2af29098d026..46fb82546909a840abf8a44ac78695bf0b009de6 100644 (file)
--- a/test/unit/expr/node_builder_black.h
+++ b/test/unit/expr/node_builder_black.h
@@ -2,7 +2,7 @@
 /*! \file node_builder_black.h
  ** \verbatim
  ** Original author: taking
- ** Major contributors: mdeters
+ ** Major contributors: cconway, mdeters
  ** Minor contributors (to current version): dejan
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)

diff --git a/test/unit/theory/shared_term_manager_black.h b/test/unit/theory/shared_term_manager_black.h
index def2f70498523fa61af6156a1ae4b6563dd1209a..a9b902deafeb27fbe79ec4c6a0356ba85188e1ab 100644 (file)
--- a/test/unit/theory/shared_term_manager_black.h
+++ b/test/unit/theory/shared_term_manager_black.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: barrett
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): mdeters
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h
index 763e03fdb42d1198467fcf8cd0a14f123407488e..029bf9f06d9a374f6fd4bc41200376f042580fd4 100644 (file)
--- a/test/unit/theory/theory_arith_white.h
+++ b/test/unit/theory/theory_arith_white.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: taking
  ** Major contributors: none
- ** Minor contributors (to current version): mdeters
+ ** Minor contributors (to current version): barrett, mdeters
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h
index 0c6a38d0ba353baa0bfc0e4b89ce599890eef3c4..193ba3792e9dec9fa3d7f703d6191393a6bb6bc3 100644 (file)
--- a/test/unit/theory/theory_black.h
+++ b/test/unit/theory/theory_black.h
@@ -2,8 +2,8 @@
 /*! \file theory_black.h
  ** \verbatim
  ** Original author: taking
- ** Major contributors: mdeters
- ** Minor contributors (to current version): cconway, dejan
+ ** Major contributors: barrett, mdeters
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h
index 148fb80e6d3e6b9417acbe36bed50e91835ffa23..4365e7db2067043d8015bd3417b5be14822c94e4 100644 (file)
--- a/test/unit/theory/theory_engine_white.h
+++ b/test/unit/theory/theory_engine_white.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): barrett, cconway
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/test/unit/theory/theory_uf_tim_white.h b/test/unit/theory/theory_uf_tim_white.h
index aec999293b02e9cc2c36b30f7a15e95598cf7f50..e831dce4a8be886abbb902dffe4b2a7c336a476e 100644 (file)
--- a/test/unit/theory/theory_uf_tim_white.h
+++ b/test/unit/theory/theory_uf_tim_white.h
@@ -1,9 +1,9 @@
 /*********************                                                        */
-/*! \file theory_uf_white.h
+/*! \file theory_uf_tim_white.h
  ** \verbatim
  ** Original author: taking
- ** Major contributors: mdeters
- ** Minor contributors (to current version): dejan
+ ** Major contributors: barrett
+ ** Minor contributors (to current version): cconway, dejan, mdeters
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences