fix some file documentation

diff --git a/src/smt/smt_engine_scope.cpp b/src/smt/smt_engine_scope.cpp
index 03298e99a8c08bfe44eeed6159ca6e5c5ff38f17..ec987c25f3785a8b94efefe3b9170898f2028e3d 100644 (file)
--- a/src/smt/smt_engine_scope.cpp
+++ b/src/smt/smt_engine_scope.cpp
@@ -1,3 +1,22 @@
+/*********************                                                        */
+/*! \file smt_engine_scope.cpp
+ ** \verbatim
+ ** Original author: mdeters
+ ** 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
+ **/
+
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 
@@ -6,5 +25,5 @@ namespace smt {
 
 CVC4_THREADLOCAL(SmtEngine*) s_smtEngine_current = NULL;
 
-}
-}
+}/* CVC4::smt namespace */
+}/* CVC4 namespace */

diff --git a/src/smt/smt_engine_scope.h b/src/smt/smt_engine_scope.h
index bcdaefd9f0b95695b463bcd43c1e99c210f562f7..f10f4e767819a8aff44e7761ccfabbc9243bf2e0 100644 (file)
--- a/src/smt/smt_engine_scope.h
+++ b/src/smt/smt_engine_scope.h
@@ -1,3 +1,22 @@
+/*********************                                                        */
+/*! \file smt_engine_scope.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** 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
+ **/
+
 #include "smt/smt_engine.h"
 #include "util/tls.h"
 #include "util/Assert.h"
@@ -36,5 +55,5 @@ public:
   }
 };/* class SmtScope */
 
-}
-}
+}/* CVC4::smt namespace */
+}/* CVC4 namespace */

diff --git a/src/theory/candidate_generator.cpp b/src/theory/candidate_generator.cpp
index 2563ef0d7c5efac6708e272b402dcd9c8e90dceb..de98d709d84fea7e599cfd50ab61fc14293c1cbf 100644 (file)
--- a/src/theory/candidate_generator.cpp
+++ b/src/theory/candidate_generator.cpp
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file theory_uf_candidate_generator.cpp
+/*! \file candidate_generator.cpp
  ** \verbatim
  ** Original author: ajreynol
- ** Major contributors: none
+ ** Major contributors: mdeters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** 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

diff --git a/src/theory/rr_inst_match.cpp b/src/theory/rr_inst_match.cpp
index 21a3096103d6cd6ad5310d50f2390339e882cfd6..0e3e7b9fae839ea115807948ba3c4fe0df816635 100644 (file)
--- a/src/theory/rr_inst_match.cpp
+++ b/src/theory/rr_inst_match.cpp
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file inst_match.cpp
+/*! \file rr_inst_match.cpp
  ** \verbatim
  ** Original author: ajreynol
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Major contributors: bobot
+ ** Minor contributors (to current version): mdeters
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** 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

diff --git a/src/theory/rr_inst_match.h b/src/theory/rr_inst_match.h
index 68b6e1bfdec5e8efb920e14c6e12056c0934edd2..468fe6a898880f1efc6373d2b240d7fec9ddcd26 100644 (file)
--- a/src/theory/rr_inst_match.h
+++ b/src/theory/rr_inst_match.h
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file inst_match.h
+/*! \file rr_inst_match.h
  ** \verbatim
  ** Original author: ajreynol
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Major contributors: bobot
+ ** Minor contributors (to current version): mdeters
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** 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

diff --git a/src/theory/rr_inst_match_impl.h b/src/theory/rr_inst_match_impl.h
index 28bc8c7eb3d28dc7fe3464292c30bfab3285dcab..4bf04cb9652bfe4d117eb20cfab0fd223e8b54f9 100644 (file)
--- a/src/theory/rr_inst_match_impl.h
+++ b/src/theory/rr_inst_match_impl.h
@@ -1,9 +1,9 @@
 /*********************                                                        */
-/*! \file inst_match_impl.h
+/*! \file rr_inst_match_impl.h
  ** \verbatim
  ** Original author: bobot
  ** Major contributors: none
- ** Minor contributors (to current version): taking, mdeters
+ ** Minor contributors (to current version): ajreynol, mdeters
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009-2012  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/theory/rr_trigger.cpp b/src/theory/rr_trigger.cpp
index ece68d137a32af2444d26a3efea5430aaa24d55e..5d56147e86ae4e1bebab4c602d1b2588f6d17217 100644 (file)
--- a/src/theory/rr_trigger.cpp
+++ b/src/theory/rr_trigger.cpp
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file trigger.cpp
+/*! \file rr_trigger.cpp
  ** \verbatim
  ** Original author: ajreynol
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): bobot
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** 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

diff --git a/src/theory/rr_trigger.h b/src/theory/rr_trigger.h
index 7ea4ee1a31579f3765b7f1f9e1731d7986ee8d9e..bc12666d0d57aa02b093244332c442080333e349 100644 (file)
--- a/src/theory/rr_trigger.h
+++ b/src/theory/rr_trigger.h
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file trigger.h
+/*! \file rr_trigger.h
  ** \verbatim
  ** Original author: ajreynol
- ** Major contributors: none
+ ** Major contributors: bobot
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** 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