Update copyrights, add missing file-level documentation; fix perms.

diff --git a/examples/hashsmt/sha1.hpp b/examples/hashsmt/sha1.hpp
index dc7146ef5a97840cc720830b3ac68301416bac17..0d4bbbf33033917a830ffb8b7679da8a1edab886 100644 (file)
--- a/examples/hashsmt/sha1.hpp
+++ b/examples/hashsmt/sha1.hpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Dejan Jovanovic
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Morgan Deters
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/examples/hashsmt/sha1smt.cpp b/examples/hashsmt/sha1smt.cpp
index 29f8e61ad5b65298b437716e96b16f0f238317e8..1bdd380c139b4a3f01d391e47fe312a0399c9775 100644 (file)
--- a/examples/hashsmt/sha1smt.cpp
+++ b/examples/hashsmt/sha1smt.cpp
@@ -2,7 +2,7 @@
 /*! \file sha1smt.cpp
  ** \verbatim
  ** Original author: Dejan Jovanovic
- ** Major contributors: none
+ ** Major contributors: Morgan Deters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa

diff --git a/examples/hashsmt/word.h b/examples/hashsmt/word.h
index 55caa47d323c83eec5a4dbcf06963cb48e238972..f8c03f7b2d26e396144474c3067fdbd11d6567dd 100644 (file)
--- a/examples/hashsmt/word.h
+++ b/examples/hashsmt/word.h
@@ -2,8 +2,8 @@
 /*! \file word.h
  ** \verbatim
  ** Original author: Dejan Jovanovic
- ** Major contributors: none
- ** Minor contributors (to current version): Morgan Deters
+ ** Major contributors: Morgan Deters
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/examples/nra-translate/normalize.cpp b/examples/nra-translate/normalize.cpp
index 2a8c177e7fb2997dd179405420db72ca48012226..c3985ebf42318e06aca7cd650e5024a3aa0b9ae2 100644 (file)
--- a/examples/nra-translate/normalize.cpp
+++ b/examples/nra-translate/normalize.cpp
@@ -2,8 +2,8 @@
 /*! \file normalize.cpp
  ** \verbatim
  ** Original author: Dejan Jovanovic
- ** Major contributors: none
- ** Minor contributors (to current version): Morgan Deters
+ ** Major contributors: Morgan Deters
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/examples/nra-translate/smt2info.cpp b/examples/nra-translate/smt2info.cpp
index 6ad621b16bdd027b3be32bc32710dcd043482247..9154232d8eeae701ebf8ed680c4314ea6a400aea 100644 (file)
--- a/examples/nra-translate/smt2info.cpp
+++ b/examples/nra-translate/smt2info.cpp
@@ -2,8 +2,8 @@
 /*! \file smt2info.cpp
  ** \verbatim
  ** Original author: Dejan Jovanovic
- ** Major contributors: none
- ** Minor contributors (to current version): Morgan Deters
+ ** Major contributors: Morgan Deters
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/examples/nra-translate/smt2todreal.cpp b/examples/nra-translate/smt2todreal.cpp
index 13feb41352972367c79bc7a1aee68e848e8cd85b..a19b83c6c8679787737f2890f533aa992b58f5f0 100644 (file)
--- a/examples/nra-translate/smt2todreal.cpp
+++ b/examples/nra-translate/smt2todreal.cpp
@@ -2,8 +2,8 @@
 /*! \file smt2todreal.cpp
  ** \verbatim
  ** Original author: Dejan Jovanovic
- ** Major contributors: none
- ** Minor contributors (to current version): Morgan Deters
+ ** Major contributors: Morgan Deters
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp
index 2b552684aa290577e5143998a106df116df55c50..27d1249a179b7a914aeab254dafaaeb5426076b3 100644 (file)
--- a/src/compat/cvc3_compat.cpp
+++ b/src/compat/cvc3_compat.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Morgan Deters
  ** Major contributors: none
- ** Minor contributors (to current version): Tim King, Dejan Jovanovic
+ ** Minor contributors (to current version): Tim King, Dejan Jovanovic, Tianyi Liang
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/context/cdvector.h b/src/context/cdvector.h
index 6792cca9d828b2d775c9ebc89b572be9dd50f7c9..52e1d52bbca00d5846eacfa449b962c6c109a9ab 100644 (file)
--- a/src/context/cdvector.h
+++ b/src/context/cdvector.h
@@ -2,8 +2,8 @@
 /*! \file cdvector.h
  ** \verbatim
  ** Original author: Tim King
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
+ ** Major contributors: none
+ ** Minor contributors (to current version): Morgan Deters
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h
index f28b13774a8b642580a94edb714ef0b25e1c294f..cda696a03331ee1deda7064ff283bcdef1881958 100644 (file)
--- a/src/decision/decision_engine.h
+++ b/src/decision/decision_engine.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Kshitij Bansal
  ** Major contributors: none
- ** Minor contributors (to current version): Clark Barrett, Dejan Jovanovic, Morgan Deters
+ ** Minor contributors (to current version): Clark Barrett, Dejan Jovanovic, Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/decision/decision_mode.h b/src/decision/decision_mode.h
index 20743cba106ebc9eb34c093b9eb3b81cb95dc3ab..3c5d9834065157c85f7604826e5febe484d7e751 100644 (file)
--- a/src/decision/decision_mode.h
+++ b/src/decision/decision_mode.h
@@ -2,7 +2,7 @@
 /*! \file decision_mode.h
  ** \verbatim
  ** Original author: Morgan Deters
- ** Major contributors: none
+ ** Major contributors: Kshitij Bansal
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa

diff --git a/src/decision/options_handlers.h b/src/decision/options_handlers.h
index 44a6239704f635cf29fb388c02c4f0e061bd3672..f538ba94772af7ed33eba785217b66e0725de0b9 100644 (file)
--- a/src/decision/options_handlers.h
+++ b/src/decision/options_handlers.h
@@ -2,8 +2,8 @@
 /*! \file options_handlers.h
  ** \verbatim
  ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): Kshitij Bansal
+ ** Major contributors: Kshitij Bansal
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp
index 056e68c6990ed1601a1bfcaf45c19b2820fbc24a..86768500b09b87f2a177f8e65d7e739d32a889e0 100644 (file)
--- a/src/expr/attribute.cpp
+++ b/src/expr/attribute.cpp
@@ -2,7 +2,7 @@
 /*! \file attribute.cpp
  ** \verbatim
  ** Original author: Morgan Deters
- ** Major contributors: Dejan Jovanovic
+ ** Major contributors: Dejan Jovanovic, Tim King
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa

diff --git a/src/expr/attribute.h b/src/expr/attribute.h
index 1e3f25461db84dab9d5ba30ccf592ef949930d14..d203b75ada5c5fa0002a111e82fae462469eae7e 100644 (file)
--- a/src/expr/attribute.h
+++ b/src/expr/attribute.h
@@ -2,8 +2,8 @@
 /*! \file attribute.h
  ** \verbatim
  ** Original author: Morgan Deters
- ** Major contributors: Dejan Jovanovic
- ** Minor contributors (to current version): Christopher L. Conway, Tim King
+ ** Major contributors: Tim King
+ ** Minor contributors (to current version): Christopher L. Conway, Dejan Jovanovic
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h
index fa6459481c623825694304c30acdbc66fc22e09d..0a3d389e70a4ecedb5400903221de54cdf371135 100644 (file)
--- a/src/expr/attribute_internals.h
+++ b/src/expr/attribute_internals.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Morgan Deters
  ** Major contributors: none
- ** Minor contributors (to current version): Dejan Jovanovic
+ ** Minor contributors (to current version): Dejan Jovanovic, Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/expr/attribute_unique_id.h b/src/expr/attribute_unique_id.h
index 79c6bfd8fd349e2d38315128e5497b42d51aa635..08b31a4c0492dcd24c04267df4488aa83199073e 100644 (file)
--- a/src/expr/attribute_unique_id.h
+++ b/src/expr/attribute_unique_id.h
@@ -1,7 +1,24 @@
+/*********************                                                        */
+/*! \file attribute_unique_id.h
+ ** \verbatim
+ ** Original author: Tim King
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** 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
 
-#include "cvc4_private.h"
 #include <stdint.h>
 
 // ATTRIBUTE IDs ============================================================

diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index d3e4b8553c0262c0f4d8a6ed34127ad5e283cf22..0b664ceb4a0031a562aa95f61002ea882dfe07a9 100644 (file)
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -2,8 +2,8 @@
 /*! \file command.cpp
  ** \verbatim
  ** Original author: Morgan Deters
- ** Major contributors: Francois Bobot
- ** Minor contributors (to current version): Kshitij Bansal, Dejan Jovanovic, Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): Kshitij Bansal, Dejan Jovanovic, Andrew Reynolds, Francois Bobot
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index 085a3a0c8f0c9b21d6460b167a64bc9d8c99a4ec..e1578efa7a9c5d16f0be30ac6dc4bf7cbccc1271 100644 (file)
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Morgan Deters
  ** Major contributors: Dejan Jovanovic
- ** Minor contributors (to current version): Tim King, Kshitij Bansal, Christopher L. Conway
+ ** Minor contributors (to current version): Tim King, Christopher L. Conway, Kshitij Bansal
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h
index a330aa4a96fb221fe03639797e2d8ffd4dfafbbb..ea9a598c0f95c4c959f5872ec96736c1dc192409 100644 (file)
--- a/src/expr/metakind_template.h
+++ b/src/expr/metakind_template.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Morgan Deters
  ** Major contributors: none
- ** Minor contributors (to current version): Dejan Jovanovic
+ ** Minor contributors (to current version): Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index 39bbfbc2e3822bd00d6a6744b76ccb783eb74317..c88fd187dd322702239494495267cf89ae35a7d2 100644 (file)
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Dejan Jovanovic
  ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/expr/node.h b/src/expr/node.h
index 0a4b853aaa1a7e4b20235447982f60fbd8968e65..1c13c467415c4b88ff70e60b0362d2958cdfeaa0 100644 (file)
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Dejan Jovanovic
  ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): Francois Bobot, Tim King, Clark Barrett, Christopher L. Conway
+ ** Minor contributors (to current version): Kshitij Bansal, Francois Bobot, Clark Barrett, Tim King, Christopher L. Conway
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 9c76a41f31b99d2d5b4f26b6603ce67e5847c0fc..22c47da59bc83454e6f49c5c9f8430f877a0c129 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: Dejan Jovanovic
- ** Major contributors: Christopher L. Conway, Morgan Deters
- ** Minor contributors (to current version): ACSYS, Tim King
+ ** Major contributors: Morgan Deters
+ ** Minor contributors (to current version): ACSYS, Tim King, Christopher L. Conway
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index af771bd89538376621a3af8e40093d27c921b943..caf8f5ad44dc96d7835af5c52ed8196d6c0a1dbb 100644 (file)
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Dejan Jovanovic
  ** Major contributors: Christopher L. Conway, Morgan Deters
- ** Minor contributors (to current version): ACSYS, Tim King, Kshitij Bansal
+ ** Minor contributors (to current version): ACSYS, Tianyi Liang, Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/expr/pickle_data.h b/src/expr/pickle_data.h
index 31751b381dd5ce855236899e089dba66348405b6..beff1f8a968a6c092017aed980abc1e44aa6c37c 100644 (file)
--- a/src/expr/pickle_data.h
+++ b/src/expr/pickle_data.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Morgan Deters
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/expr/type_checker.h b/src/expr/type_checker.h
index d34a7c7d6e50f85d8162599f9d0b21f38f8c1195..491b443475ec807db75ac0cf4e038788e460bc78 100644 (file)
--- a/src/expr/type_checker.h
+++ b/src/expr/type_checker.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Morgan Deters
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/expr/type_checker_template.cpp b/src/expr/type_checker_template.cpp
index 29584216059aad9caef909c2fecc18dbf57035c7..87361e99105cd8b11beaa03c60cfe7d7903198b3 100644 (file)
--- a/src/expr/type_checker_template.cpp
+++ b/src/expr/type_checker_template.cpp
@@ -2,8 +2,8 @@
 /*! \file type_checker_template.cpp
  ** \verbatim
  ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): lianah
+ ** Major contributors: Tim King
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index ae951dbf28204cc09181aad312526f937c1ce413..1dd0ffed13eab2143bb78d38ee236142f95acd12 100644 (file)
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Dejan Jovanovic
  ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): Clark Barrett, Andrew Reynolds, Tim King
+ ** Minor contributors (to current version): Clark Barrett, Andrew Reynolds, Tianyi Liang, Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index 9ee8961073b0d772b28772b2f6d47c26a57f3841..467b150d3abd2b47800133510c2ebc194d76cb22 100644 (file)
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Morgan Deters
  ** Major contributors: Kshitij Bansal
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/main/options_handlers.h b/src/main/options_handlers.h
index 6fe28711b3f6b06e0c972521bfa8660fc19a3646..7723dcb33b17b0cb86353719afe1f8bb85351c46 100644 (file)
--- a/src/main/options_handlers.h
+++ b/src/main/options_handlers.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Morgan Deters
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/parser/bounded_token_factory.cpp b/src/parser/bounded_token_factory.cpp
index b88b09e8b4d46017d48f3390ee165325dc5b6255..59fe5a2d437130e51fc2cd832016c4248d8338c7 100644 (file)
--- a/src/parser/bounded_token_factory.cpp
+++ b/src/parser/bounded_token_factory.cpp
@@ -2,8 +2,8 @@
 /*! \file bounded_token_factory.cpp
  ** \verbatim
  ** Original author: Christopher L. Conway
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
+ ** Major contributors: none
+ ** Minor contributors (to current version): Morgan Deters
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 5d9b6c7ae0600f81d2ab8cdd7eb19d7d9b0a8735..d65a6831011a8d0c00b0ccd0843184a603e5437b 100644 (file)
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Morgan Deters
  ** Major contributors: Christopher L. Conway
- ** Minor contributors (to current version): Tim King, Dejan Jovanovic, Francois Bobot, Andrew Reynolds
+ ** Minor contributors (to current version): Tim King, Dejan Jovanovic, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/parser/smt1/smt1.cpp b/src/parser/smt1/smt1.cpp
index c9bbd386040c5241bb5f7bf191e76284d6a440a6..19be199fda41e48ae66dc160ff2b82529787cbcf 100644 (file)
--- a/src/parser/smt1/smt1.cpp
+++ b/src/parser/smt1/smt1.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Morgan Deters
  ** Major contributors: Christopher L. Conway
- ** Minor contributors (to current version): Tim King, Dejan Jovanovic, Clark Barrett, Tianyi Liang
+ ** Minor contributors (to current version): Tim King, Tianyi Liang, Dejan Jovanovic, Clark Barrett
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 657384e997c7fa439607b908cbbe5c5a4921f1e4..e2e52b1580070a232c4b0e183a6225aee647d49d 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Christopher L. Conway
  ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): Dejan Jovanovic, Andrew Reynolds, Francois Bobot, Tianyi Liang
+ ** Minor contributors (to current version): Dejan Jovanovic, Tianyi Liang, Andrew Reynolds, Francois Bobot
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 884502cf24de09ce442a1069bed9402e37f189fb..b1621e9e5465e6635abc7e4f5f4a9339c0124276 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Christopher L. Conway
  ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): Clark Barrett
+ ** Minor contributors (to current version): Clark Barrett, Tianyi Liang
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index cc46efe079d249faeb9e7398abef545f64da15c6..837adb15c86626b06c1afeacd87f20108166b2b2 100644 (file)
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Christopher L. Conway
  ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Tianyi Liang
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g
index 61e0999e9d53d42999ab5e22b15b33c307fdac25..d1e6f3a898e31d4a76481696c8de05506ce7a6d6 100644 (file)
--- a/src/parser/tptp/Tptp.g
+++ b/src/parser/tptp/Tptp.g
@@ -2,8 +2,8 @@
 /*! \file Tptp.g
  ** \verbatim
  ** Original author: Francois Bobot
- ** Major contributors: none
- ** Minor contributors (to current version): Morgan Deters
+ ** Major contributors: Morgan Deters
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp
index edffaa01f3e7209310d6360ec46b126c823b7f76..6546fd8f35dc66ddacbcd7b8dd0834edbb2b1c94 100644 (file)
--- a/src/parser/tptp/tptp.cpp
+++ b/src/parser/tptp/tptp.cpp
@@ -2,8 +2,8 @@
 /*! \file tptp.cpp
  ** \verbatim
  ** Original author: Francois Bobot
- ** Major contributors: none
- ** Minor contributors (to current version): Morgan Deters
+ ** Major contributors: Morgan Deters
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h
index e180d1524bbad0e21bc5eb0ece0395b270a31428..0981af42ff279f2dc1b3304046742857c7ec82fb 100644 (file)
--- a/src/parser/tptp/tptp.h
+++ b/src/parser/tptp/tptp.h
@@ -2,8 +2,8 @@
 /*! \file tptp.h
  ** \verbatim
  ** Original author: Francois Bobot
- ** Major contributors: none
- ** Minor contributors (to current version): Andrew Reynolds, Morgan Deters
+ ** Major contributors: Morgan Deters
+ ** Minor contributors (to current version): Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/parser/tptp/tptp_input.cpp b/src/parser/tptp/tptp_input.cpp
index bfaeb07c9a8c748d66e71c6e61f1e3ad093fd83d..b41fcdd88404437b036ac0ea180e479b30e472f2 100644 (file)
--- a/src/parser/tptp/tptp_input.cpp
+++ b/src/parser/tptp/tptp_input.cpp
@@ -2,8 +2,8 @@
 /*! \file tptp_input.cpp
  ** \verbatim
  ** Original author: Francois Bobot
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
+ ** Major contributors: none
+ ** Minor contributors (to current version): Morgan Deters
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 78623849229fd227b1c4a505f4f288e10e08ce24..bd2626ddd696e8ef751fe948174b50c01f35bdaa 100644 (file)
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Morgan Deters
  ** Major contributors: Dejan Jovanovic
- ** Minor contributors (to current version): Francois Bobot, lianah, Clark Barrett, Tim King, Andrew Reynolds
+ ** Minor contributors (to current version): Francois Bobot, Liana Hadarean, Clark Barrett, Tim King, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index 263ca50d75faca4920b0490ddb4d84d9f569ed81..39d065065605a8986e1e3079298a225982b60a25 100644 (file)
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Morgan Deters
  ** Major contributors: none
- ** Minor contributors (to current version): Andrew Reynolds, Francois Bobot
+ ** Minor contributors (to current version): Francois Bobot, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/printer/printer.h b/src/printer/printer.h
index e4bc7ce09f877374afce11c7e1008beea65a0985..a7ae8c447ae9f8c722d04852fdd928a621e1a332 100644 (file)
--- a/src/printer/printer.h
+++ b/src/printer/printer.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Morgan Deters
  ** Major contributors: none
- ** Minor contributors (to current version): Clark Barrett, Andrew Reynolds
+ ** Minor contributors (to current version): Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index cac5eb266becbf8683fc37c12a3f474a410644c7..b743ba70e695fc8812d7db33aae8bdbd2109c37a 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -2,8 +2,8 @@
 /*! \file smt2_printer.cpp
  ** \verbatim
  ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): Dejan Jovanovic, lianah, Tim King, Liana Hadarean, Francois Bobot, Andrew Reynolds
+ ** Major contributors: Andrew Reynolds
+ ** Minor contributors (to current version): Dejan Jovanovic, Tim King, Liana Hadarean, Francois Bobot
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h
index a550f274a9967c30c204711344bae3e3e139eb5f..9a2dbe6552cc37536d693fc440ab724ece6c863b 100644 (file)
--- a/src/proof/cnf_proof.h
+++ b/src/proof/cnf_proof.h
@@ -2,8 +2,8 @@
 /*! \file cnf_proof.h
  ** \verbatim
  ** Original author: Liana Hadarean
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
+ ** Major contributors: none
+ ** Minor contributors (to current version): Morgan Deters
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
index 82a1bd6be3690d70db02a567fca1fa9b31579d66..e33f1a63f385685becdb5d113f04270df8648acb 100644 (file)
--- a/src/proof/proof_manager.h
+++ b/src/proof/proof_manager.h
@@ -2,8 +2,8 @@
 /*! \file proof_manager.h
  ** \verbatim
  ** Original author: Liana Hadarean
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
+ ** Major contributors: none
+ ** Minor contributors (to current version): Morgan Deters
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h
index e7e8f65b69b2fb97f84ed8fe49bbbb5085b9e398..a4178f518b1354e51820a49da6f5e1bbd0cc08d0 100644 (file)
--- a/src/proof/sat_proof.h
+++ b/src/proof/sat_proof.h
@@ -2,8 +2,8 @@
 /*! \file sat_proof.h
  ** \verbatim
  ** Original author: Liana Hadarean
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
+ ** Major contributors: none
+ ** Minor contributors (to current version): Morgan Deters
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h
index b8963c50070ebfe59f9caf043de27711f4cf4258..457023a5973b71b7e0cbfcad3328ba2f599f342f 100644 (file)
--- a/src/proof/theory_proof.h
+++ b/src/proof/theory_proof.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Liana Hadarean
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Morgan Deters
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/prop/sat_solver_factory.cpp b/src/prop/sat_solver_factory.cpp
index 8a11f2b9660afde26d497d12272698f7e691b4d2..6cda02c00fd2e397e26ae7dc07d29eb3d0320466 100644 (file)
--- a/src/prop/sat_solver_factory.cpp
+++ b/src/prop/sat_solver_factory.cpp
@@ -2,7 +2,7 @@
 /*! \file sat_solver_factory.cpp
  ** \verbatim
  ** Original author: Dejan Jovanovic
- ** Major contributors: Morgan Deters, Tim King
+ ** Major contributors: Tim King
  ** Minor contributors (to current version): Liana Hadarean
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa

diff --git a/src/prop/sat_solver_types.h b/src/prop/sat_solver_types.h
index 8fee0d11eaa393ab04aa7b030f88c27f26b77a2c..2674c82b14e6c2d28aff30329ef1216cf4e639d9 100644 (file)
--- a/src/prop/sat_solver_types.h
+++ b/src/prop/sat_solver_types.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Dejan Jovanovic
  ** Major contributors: none
- ** Minor contributors (to current version): Morgan Deters, Kshitij Bansal
+ ** Minor contributors (to current version): Morgan Deters, Liana Hadarean, Kshitij Bansal
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h
index 7b0aa2058df6aa463836818230e35b6f3cc6fb0f..f84aecbac1bed3adc54cc50b47edc785e4401aeb 100644 (file)
--- a/src/prop/theory_proxy.h
+++ b/src/prop/theory_proxy.h
@@ -2,8 +2,8 @@
 /*! \file theory_proxy.h
  ** \verbatim
  ** Original author: Dejan Jovanovic
- ** Major contributors: Liana Hadarean, Morgan Deters
- ** Minor contributors (to current version): Christopher L. Conway, Tim King, Kshitij Bansal
+ ** Major contributors: Liana Hadarean, Kshitij Bansal, Morgan Deters
+ ** Minor contributors (to current version): Christopher L. Conway, Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/smt/model_postprocessor.cpp b/src/smt/model_postprocessor.cpp
index a66e02778b6b69b901f5bd7338e81986a8e1842e..5a14924ff8159ed9284eefa6661f459a1b0d39b6 100644 (file)
--- a/src/smt/model_postprocessor.cpp
+++ b/src/smt/model_postprocessor.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Morgan Deters
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/smt/options_handlers.h b/src/smt/options_handlers.h
index 574ef720f9e7326e1bcc048f1d9d9394a90c30e9..51ad7b6ca9b33431aa83654c9bc2fe0e3fc8d150 100644 (file)
--- a/src/smt/options_handlers.h
+++ b/src/smt/options_handlers.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Morgan Deters
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Clark Barrett
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index a2a95d6ca0fa444d3d9b2c937aea566b445483d8..d5131e6f670278436d38a9b49e11bfbc8af1f5c8 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Morgan Deters
  ** Major contributors: Clark Barrett
- ** Minor contributors (to current version): Christopher L. Conway, Liana Hadarean, Tim King, Kshitij Bansal, Dejan Jovanovic, Andrew Reynolds
+ ** Minor contributors (to current version): Tianyi Liang, Christopher L. Conway, Kshitij Bansal, Liana Hadarean, Dejan Jovanovic, Tim King, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/theory/arith/approx_simplex.cpp b/src/theory/arith/approx_simplex.cpp
index 0f5a0fd4e11d0dc01aedc7ec474aa67c3223f22f..1b3099842803738ed2fa59cd098e0862b8c30734 100644 (file)
--- a/src/theory/arith/approx_simplex.cpp
+++ b/src/theory/arith/approx_simplex.cpp
@@ -1,3 +1,20 @@
+/*********************                                                        */
+/*! \file approx_simplex.cpp
+ ** \verbatim
+ ** Original author: Tim King
+ ** Major contributors: none
+ ** Minor contributors (to current version): Morgan Deters
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** 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 "cvc4autoconfig.h"
 
 #include "theory/arith/approx_simplex.h"

diff --git a/src/theory/arith/approx_simplex.h b/src/theory/arith/approx_simplex.h
index a34c8981dcfbd012bf8e9be4dbbc44ee2678f82e..b32fdef2d95434cae50075d3a4a9ed4a1c3c9291 100644 (file)
--- a/src/theory/arith/approx_simplex.h
+++ b/src/theory/arith/approx_simplex.h
@@ -1,3 +1,20 @@
+/*********************                                                        */
+/*! \file approx_simplex.h
+ ** \verbatim
+ ** Original author: Tim King
+ ** Major contributors: none
+ ** Minor contributors (to current version): Morgan Deters
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** 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/theory/arith/arith_heuristic_pivot_rule.cpp b/src/theory/arith/arith_heuristic_pivot_rule.cpp
index 62b5fdff1554c88a315ea1d9862e77c7eeed9ab9..8a1d2b5575d5865971b207e6075023f5ce4bcd8d 100644 (file)
--- a/src/theory/arith/arith_heuristic_pivot_rule.cpp
+++ b/src/theory/arith/arith_heuristic_pivot_rule.cpp
@@ -2,7 +2,7 @@
 /*! \file arith_heuristic_pivot_rule.cpp
  ** \verbatim
  ** Original author: Morgan Deters
- ** Major contributors: none
+ ** Major contributors: Tim King
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa

diff --git a/src/theory/arith/arith_heuristic_pivot_rule.h b/src/theory/arith/arith_heuristic_pivot_rule.h
index 705c3e2f3027de6da823c4e57437403f7c46df95..78313b81b1a5458046b2f5eea027cbdd00ecde46 100644 (file)
--- a/src/theory/arith/arith_heuristic_pivot_rule.h
+++ b/src/theory/arith/arith_heuristic_pivot_rule.h
@@ -2,7 +2,7 @@
 /*! \file arith_heuristic_pivot_rule.h
  ** \verbatim
  ** Original author: Morgan Deters
- ** Major contributors: none
+ ** Major contributors: Tim King
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa

diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index 247c09294e5341463850625919c77c6160ced21d..f725379657e57be18d81c224cc00db2c8214d7a2 100644 (file)
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -2,8 +2,8 @@
 /*! \file arith_rewriter.cpp
  ** \verbatim
  ** Original author: Tim King
- ** Major contributors: none
- ** Minor contributors (to current version): Morgan Deters, Dejan Jovanovic
+ ** Major contributors: Morgan Deters
+ ** Minor contributors (to current version): Dejan Jovanovic
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp
index bf5261439b8fc4303d665310e30e15b696ac9f91..8f6f75295611910d3ed3f3217d400439955a2cf9 100644 (file)
--- a/src/theory/arith/arith_static_learner.cpp
+++ b/src/theory/arith/arith_static_learner.cpp
@@ -2,7 +2,7 @@
 /*! \file arith_static_learner.cpp
  ** \verbatim
  ** Original author: Tim King
- ** Major contributors: Dejan Jovanovic, Morgan Deters
+ ** Major contributors: Morgan Deters, Dejan Jovanovic
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa

diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h
index 6b297f2abed80841808385ce7e719361a5288ac3..11626c1de54738884309f0aab902367528db417f 100644 (file)
--- a/src/theory/arith/arith_utilities.h
+++ b/src/theory/arith/arith_utilities.h
@@ -2,8 +2,8 @@
 /*! \file arith_utilities.h
  ** \verbatim
  ** Original author: Tim King
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): Dejan Jovanovic
+ ** Major contributors: none
+ ** Minor contributors (to current version): Dejan Jovanovic, Morgan Deters
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/theory/arith/arithvar.cpp b/src/theory/arith/arithvar.cpp
index ce05383da842bc39798d009b58b4892bc0850049..d035dde2b1c6fa86f30755609a3f8a543585804f 100644 (file)
--- a/src/theory/arith/arithvar.cpp
+++ b/src/theory/arith/arithvar.cpp
@@ -2,7 +2,7 @@
 /*! \file arithvar.cpp
  ** \verbatim
  ** Original author: Tim King
- ** Major contributors: none
+ ** Major contributors: Morgan Deters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa

diff --git a/src/theory/arith/attempt_solution_simplex.cpp b/src/theory/arith/attempt_solution_simplex.cpp
index f0cecc24b0e5f37a68be132bd257b71f1002e686..01137a33c136d16222d41aaf604c0f686444dc8f 100644 (file)
--- a/src/theory/arith/attempt_solution_simplex.cpp
+++ b/src/theory/arith/attempt_solution_simplex.cpp
@@ -1,3 +1,20 @@
+/*********************                                                        */
+/*! \file attempt_solution_simplex.cpp
+ ** \verbatim
+ ** Original author: Tim King
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** 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/attempt_solution_simplex.h"
 #include "theory/arith/options.h"

diff --git a/src/theory/arith/attempt_solution_simplex.h b/src/theory/arith/attempt_solution_simplex.h
index 5bcdc6aab6d4d37ed66aedb5ae2c220f5f633a10..6e2d86f8aed26c68611f5ffe5086505dfa951531 100644 (file)
--- a/src/theory/arith/attempt_solution_simplex.h
+++ b/src/theory/arith/attempt_solution_simplex.h
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file simplex.h
+/*! \file attempt_solution_simplex.h
  ** \verbatim
- ** Original author: taking
+ ** Original author: Tim King
  ** Major contributors: none
- ** Minor contributors (to current version): kshitij, mdeters
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012  New York University and The University of Iowa
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **

diff --git a/src/theory/arith/bound_counts.h b/src/theory/arith/bound_counts.h
index 49c1a94cec1a089f3e78b668ae89d5cdf00073fb..d3793432d3b8c83af1695062ef6b5b93f35988b6 100644 (file)
--- a/src/theory/arith/bound_counts.h
+++ b/src/theory/arith/bound_counts.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Tim King
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Morgan Deters
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/theory/arith/callbacks.cpp b/src/theory/arith/callbacks.cpp
index 1e827d316a58bc88e2bb3a8f548c84892b83580a..d4a445b70c46303839ce5db6ef2bf4a5ecf34849 100644 (file)
--- a/src/theory/arith/callbacks.cpp
+++ b/src/theory/arith/callbacks.cpp
@@ -1,3 +1,20 @@
+/*********************                                                        */
+/*! \file callbacks.cpp
+ ** \verbatim
+ ** Original author: Tim King
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** 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/callbacks.h"
 #include "theory/arith/theory_arith_private.h"
 

diff --git a/src/theory/arith/callbacks.h b/src/theory/arith/callbacks.h
index 718799e9f3e928116a2034eb0bff3b48128faa33..fd9369bf11103dc8eabe46211a801815e4510ec6 100644 (file)
--- a/src/theory/arith/callbacks.h
+++ b/src/theory/arith/callbacks.h
@@ -1,3 +1,20 @@
+/*********************                                                        */
+/*! \file callbacks.h
+ ** \verbatim
+ ** Original author: Tim King
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** 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
 

diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp
index e3e9055a7ef1c7367897cf2084eecfa6f1ee8b33..a828b9e7f8c08eec30403145d3b6e66cfce73521 100644 (file)
--- a/src/theory/arith/congruence_manager.cpp
+++ b/src/theory/arith/congruence_manager.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Tim King
  ** Major contributors: none
- ** Minor contributors (to current version): Dejan Jovanovic, Morgan Deters
+ ** Minor contributors (to current version): Morgan Deters, Dejan Jovanovic
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/theory/arith/dual_simplex.cpp b/src/theory/arith/dual_simplex.cpp
index a9304ae76f8446a7830e7baad538c7a561d4ee97..b5acb91492453d930785ac640db913b52e233e38 100644 (file)
--- a/src/theory/arith/dual_simplex.cpp
+++ b/src/theory/arith/dual_simplex.cpp
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file simplex.cpp
+/*! \file dual_simplex.cpp
  ** \verbatim
- ** Original author: taking
+ ** Original author: Tim King
  ** Major contributors: none
- ** Minor contributors (to current version): mdeters
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012  New York University and The University of Iowa
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **

diff --git a/src/theory/arith/dual_simplex.h b/src/theory/arith/dual_simplex.h
index 0ec4bc2389beab4d6e8d64a859f0170251dddab4..9d2152800ded21db2828bae0591c26f9657e48bc 100644 (file)
--- a/src/theory/arith/dual_simplex.h
+++ b/src/theory/arith/dual_simplex.h
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file simplex.h
+/*! \file dual_simplex.h
  ** \verbatim
- ** Original author: taking
+ ** Original author: Tim King
  ** Major contributors: none
- ** Minor contributors (to current version): kshitij, mdeters
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012  New York University and The University of Iowa
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **

diff --git a/src/theory/arith/fc_simplex.cpp b/src/theory/arith/fc_simplex.cpp
index e99e625055786bc04a457195a2293c382f734951..c0bffdf077ccfe93b11d207d30b6da7205cc0cf4 100644 (file)
--- a/src/theory/arith/fc_simplex.cpp
+++ b/src/theory/arith/fc_simplex.cpp
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file simplex.cpp
+/*! \file fc_simplex.cpp
  ** \verbatim
- ** Original author: taking
+ ** Original author: Tim King
  ** Major contributors: none
- ** Minor contributors (to current version): mdeters
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012  New York University and The University of Iowa
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **

diff --git a/src/theory/arith/fc_simplex.h b/src/theory/arith/fc_simplex.h
index 51514bcfb3977c0a3214bd93a213f538c3916e92..2397ccdbad1987781db5a0b67311af9b013d5891 100644 (file)
--- a/src/theory/arith/fc_simplex.h
+++ b/src/theory/arith/fc_simplex.h
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file simplex.h
+/*! \file fc_simplex.h
  ** \verbatim
- ** Original author: taking
+ ** Original author: Tim King
  ** Major contributors: none
- ** Minor contributors (to current version): kshitij, mdeters
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012  New York University and The University of Iowa
+ ** Minor contributors (to current version): Morgan Deters
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **

diff --git a/src/theory/arith/options_handlers.h b/src/theory/arith/options_handlers.h
index 899a3a7c665ceed517676c2c4514b8be8345ce92..a72ced0bc94248e0cbb30f6dfa8735b27028f2fb 100644 (file)
--- a/src/theory/arith/options_handlers.h
+++ b/src/theory/arith/options_handlers.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Morgan Deters
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h
index deafb559af51d7491971fb60d59635b1857f9074..c497adb75fbd03cbbc15a5b496dbd9ea9cc8ac22 100644 (file)
--- a/src/theory/arith/partial_model.h
+++ b/src/theory/arith/partial_model.h
@@ -2,8 +2,8 @@
 /*! \file partial_model.h
  ** \verbatim
  ** Original author: Tim King
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
+ ** Major contributors: none
+ ** Minor contributors (to current version): Morgan Deters
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h
index d646ca8891b2d5196c5fbc213fdb78ce95fed67b..b61cadaf87c0b73c596b682883fd41d34f3d5aad 100644 (file)
--- a/src/theory/arith/simplex.h
+++ b/src/theory/arith/simplex.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Tim King
  ** Major contributors: none
- ** Minor contributors (to current version): Kshitij Bansal, Morgan Deters
+ ** Minor contributors (to current version): Morgan Deters
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/theory/arith/simplex_update.cpp b/src/theory/arith/simplex_update.cpp
index cc3b6a4604d47bed62ad62e0d1093cf874f2cd8c..ba19d01b11af7c7d485df97781ae9de61a619832 100644 (file)
--- a/src/theory/arith/simplex_update.cpp
+++ b/src/theory/arith/simplex_update.cpp
@@ -1,11 +1,11 @@
 /*********************                                                        */
 /*! \file simplex_update.cpp
  ** \verbatim
- ** Original author: taking
+ ** Original author: Tim King
  ** Major contributors: none
  ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012  New York University and The University of Iowa
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **

diff --git a/src/theory/arith/simplex_update.h b/src/theory/arith/simplex_update.h
index 64aa193dd7542b01daa6bacc7b71f3af39229b23..5a313e305130e0ad981bb3cc4d6ed0866b6e3462 100644 (file)
--- a/src/theory/arith/simplex_update.h
+++ b/src/theory/arith/simplex_update.h
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file linear_equality.h
+/*! \file simplex_update.h
  ** \verbatim
- ** Original author: taking
+ ** Original author: Tim King
  ** Major contributors: none
- ** Minor contributors (to current version): mdeters
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012  New York University and The University of Iowa
+ ** Minor contributors (to current version): Morgan Deters
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **

diff --git a/src/theory/arith/soi_simplex.cpp b/src/theory/arith/soi_simplex.cpp
index c0ee7ad20db0ec5d001dd1772702212739af2a9e..2eb258d3b5c391a9ce99c199a9ba7190f1872379 100644 (file)
--- a/src/theory/arith/soi_simplex.cpp
+++ b/src/theory/arith/soi_simplex.cpp
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file simplex.cpp
+/*! \file soi_simplex.cpp
  ** \verbatim
- ** Original author: taking
+ ** Original author: Tim King
  ** Major contributors: none
- ** Minor contributors (to current version): mdeters
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012  New York University and The University of Iowa
+ ** Minor contributors (to current version): Morgan Deters
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **

diff --git a/src/theory/arith/soi_simplex.h b/src/theory/arith/soi_simplex.h
index de565df64997f943c3394df206fd95fd2644aaf1..cee6cf81d745a4d229104db3e9bb62e940cb9ad4 100644 (file)
--- a/src/theory/arith/soi_simplex.h
+++ b/src/theory/arith/soi_simplex.h
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file simplex.h
+/*! \file soi_simplex.h
  ** \verbatim
- ** Original author: taking
+ ** Original author: Tim King
  ** Major contributors: none
- ** Minor contributors (to current version): kshitij, mdeters
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012  New York University and The University of Iowa
+ ** Minor contributors (to current version): Morgan Deters
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **

diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp
index 9d06fadc4999492eb56188da7a31c5195df9c1ca..22fbf87137ede9b97177be8ae07c217f9b00f068 100644 (file)
--- a/src/theory/arith/tableau.cpp
+++ b/src/theory/arith/tableau.cpp
@@ -1,3 +1,20 @@
+/*********************                                                        */
+/*! \file tableau.cpp
+ ** \verbatim
+ ** Original author: Tim King
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** 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"
 
 using namespace std;

diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h
index deed7e7bebaa264062de4b51960831174debc5af..3e4cb819ba91a3897c269c1851330a291f031c95 100644 (file)
--- a/src/theory/arith/tableau.h
+++ b/src/theory/arith/tableau.h
@@ -1,3 +1,20 @@
+/*********************                                                        */
+/*! \file tableau.h
+ ** \verbatim
+ ** Original author: Tim King
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** 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/arith/tableau_sizes.cpp b/src/theory/arith/tableau_sizes.cpp
index 7c44f679166ab29410481f3d92418f9c1c349fbb..bc0aa4dcda4823c1171f505b8b804efdc7defd44 100644 (file)
--- a/src/theory/arith/tableau_sizes.cpp
+++ b/src/theory/arith/tableau_sizes.cpp
@@ -1,3 +1,20 @@
+/*********************                                                        */
+/*! \file tableau_sizes.cpp
+ ** \verbatim
+ ** Original author: Tim King
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** 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_sizes.h"
 #include "theory/arith/tableau.h"
 

diff --git a/src/theory/arith/tableau_sizes.h b/src/theory/arith/tableau_sizes.h
index d6b820300cdd5ebc5733052348d97a977083f333..66b091fab4c740cd6cb268c0e89d0016bd24eb0e 100644 (file)
--- a/src/theory/arith/tableau_sizes.h
+++ b/src/theory/arith/tableau_sizes.h
@@ -1,3 +1,20 @@
+/*********************                                                        */
+/*! \file tableau_sizes.h
+ ** \verbatim
+ ** Original author: Tim King
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** 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/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 6c7f622ec71de46fffe770a05b82174c6b23d9a2..395d51d3e9f87177d88fc4a8e8682b7f5f04bbbd 100644 (file)
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -1,11 +1,11 @@
 /*********************                                                        */
 /*! \file theory_arith.cpp
  ** \verbatim
- ** Original author: taking
- ** Major contributors: none
- ** Minor contributors (to current version): kshitij, ajreynol, mdeters, dejan
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012  New York University and The University of Iowa
+ ** Original author: Tim King
+ ** Major contributors: Morgan Deters
+ ** Minor contributors (to current version): Andrew Reynolds, Tianyi Liang, Dejan Jovanovic
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **

diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 451f1e8ffe23f69523ebbb5cb2171be80ce37a5d..2408094d84ffbc86feed963510cc474ec186ebf0 100644 (file)
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -2,8 +2,8 @@
 /*! \file theory_arith.h
  ** \verbatim
  ** Original author: Morgan Deters
- ** Major contributors: Tim King
- ** Minor contributors (to current version): Andrew Reynolds, Dejan Jovanovic
+ ** Major contributors: Dejan Jovanovic, Tim King
+ ** Minor contributors (to current version): Tianyi Liang, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index aa2b2a557190f40d6d2f6a8274a35cffdfe3430e..002d503d080f7a226adcd79a192e4d7fd90603cc 100644 (file)
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file theory_arith.cpp
+/*! \file theory_arith_private.cpp
  ** \verbatim
- ** Original author: taking
+ ** Original author: Tim King
  ** Major contributors: none
- ** Minor contributors (to current version): kshitij, ajreynol, mdeters, dejan
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012  New York University and The University of Iowa
+ ** Minor contributors (to current version): Andrew Reynolds, Tianyi Liang, Morgan Deters
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **

diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index 86de3c1a94517609e3d2f8249eaa2abb882d8916..71061034677a827ebb8a631841df5f068d4989aa 100644 (file)
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file theory_arith.cpp
+/*! \file theory_arith_private.h
  ** \verbatim
- ** Original author: taking
+ ** Original author: Tim King
  ** Major contributors: none
- ** Minor contributors (to current version): kshitij, ajreynol, mdeters, dejan
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012  New York University and The University of Iowa
+ ** Minor contributors (to current version): Andrew Reynolds, Tianyi Liang, Morgan Deters
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **

diff --git a/src/theory/arith/theory_arith_private_forward.h b/src/theory/arith/theory_arith_private_forward.h
index 0dc7cdd5bdb6d7fd0506e25c070128f013eb97d6..62980d83daa8e2b57a62ad25999a76c1b4b63963 100644 (file)
--- a/src/theory/arith/theory_arith_private_forward.h
+++ b/src/theory/arith/theory_arith_private_forward.h
@@ -1,3 +1,20 @@
+/*********************                                                        */
+/*! \file theory_arith_private_forward.h
+ ** \verbatim
+ ** Original author: Tim King
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** 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/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h
index 0d3a578a6ecf09c3501cc1c67def53d75931ce7c..70f55c476fb5d9ac00daef107252feae76f05d8b 100644 (file)
--- a/src/theory/arith/theory_arith_type_rules.h
+++ b/src/theory/arith/theory_arith_type_rules.h
@@ -2,8 +2,8 @@
 /*! \file theory_arith_type_rules.h
  ** \verbatim
  ** Original author: Dejan Jovanovic
- ** Major contributors: Tim King, Christopher L. Conway, Morgan Deters
- ** Minor contributors (to current version): none
+ ** Major contributors: Christopher L. Conway, Morgan Deters
+ ** Minor contributors (to current version): Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/theory/atom_requests.cpp b/src/theory/atom_requests.cpp
index 6070004d2d4d0ffbcdf38fa55f45c01b7c3b6cc9..b84b59d14a132d24a3377bad8651b25b15367287 100644 (file)
--- a/src/theory/atom_requests.cpp
+++ b/src/theory/atom_requests.cpp
@@ -2,7 +2,7 @@
 /*! \file atom_requests.cpp
  ** \verbatim
  ** Original author: Dejan Jovanovic
- ** Major contributors: none
+ ** Major contributors: Morgan Deters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa

diff --git a/src/theory/atom_requests.h b/src/theory/atom_requests.h
index b54ece6383a93984106f21552bde873cbed00472..689d2745b2f9c0372b305537dfe644178f1d54c6 100644 (file)
--- a/src/theory/atom_requests.h
+++ b/src/theory/atom_requests.h
@@ -2,7 +2,7 @@
 /*! \file atom_requests.h
  ** \verbatim
  ** Original author: Dejan Jovanovic
- ** Major contributors: none
+ ** Major contributors: Morgan Deters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa

diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp
index a809ad0e8c8e6a2da6ad449bf4aa33f06cab9763..a0179c1171e9bdc9e0ec3864aab88dbb256c6e7e 100644 (file)
--- a/src/theory/booleans/theory_bool.cpp
+++ b/src/theory/booleans/theory_bool.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Morgan Deters
  ** Major contributors: Dejan Jovanovic
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Clark Barrett
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp
index 00f183eb5a8a27934c68f26fa843ebc212c6cb1c..ef415139d868ce65b910c33cccc8504768601f2d 100644 (file)
--- a/src/theory/booleans/theory_bool_rewriter.cpp
+++ b/src/theory/booleans/theory_bool_rewriter.cpp
@@ -2,8 +2,8 @@
 /*! \file theory_bool_rewriter.cpp
  ** \verbatim
  ** Original author: Dejan Jovanovic
- ** Major contributors: Tim King, Clark Barrett
- ** Minor contributors (to current version): Morgan Deters
+ ** Major contributors: Kshitij Bansal, Tim King
+ ** Minor contributors (to current version): Morgan Deters, Clark Barrett
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/theory/booleans/theory_bool_rewriter.h b/src/theory/booleans/theory_bool_rewriter.h
index ac9469980e9d330df0a627e2f40fb4ddfa7bf46d..ccf7deecf1cab14c35ea79afe6c4b5a1b45b2aeb 100644 (file)
--- a/src/theory/booleans/theory_bool_rewriter.h
+++ b/src/theory/booleans/theory_bool_rewriter.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Dejan Jovanovic
  ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp
index 60199c09a5ca96773a98ac3cdaaf593d01118075..d02c9ace11c9caca9b1ad2ffaba931342c1fc035 100644 (file)
--- a/src/theory/builtin/theory_builtin.cpp
+++ b/src/theory/builtin/theory_builtin.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Morgan Deters
  ** Major contributors: none
- ** Minor contributors (to current version): Andrew Reynolds
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/theory/bv/bitblast_strategies.cpp b/src/theory/bv/bitblast_strategies.cpp
index 19c6a9248f04791e864ebc08d0dc870c26527fa2..4a0b45d626be0fc2f2dd73fde4e0385ae5092b82 100644 (file)
--- a/src/theory/bv/bitblast_strategies.cpp
+++ b/src/theory/bv/bitblast_strategies.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Liana Hadarean
  ** Major contributors: none
- ** Minor contributors (to current version): Clark Barrett, Dejan Jovanovic, Morgan Deters, lianah, Tim King
+ ** Minor contributors (to current version): Clark Barrett, Dejan Jovanovic, Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp
index 1712509b5a082449a6391b597a1a8c88487c4177..cbe550f96a06a5c709c66ec46913b9c5ff7e0688 100644 (file)
--- a/src/theory/bv/bitblaster.cpp
+++ b/src/theory/bv/bitblaster.cpp
@@ -2,8 +2,8 @@
 /*! \file bitblaster.cpp
  ** \verbatim
  ** Original author: Liana Hadarean
- ** Major contributors: Dejan Jovanovic
- ** Minor contributors (to current version): Clark Barrett, Morgan Deters, lianah
+ ** Major contributors: Dejan Jovanovic, Andrew Reynolds
+ ** Minor contributors (to current version): Clark Barrett, Kshitij Bansal, Morgan Deters
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/theory/bv/bitblaster.h b/src/theory/bv/bitblaster.h
index 6fab0369c0ab345860595ba626aa7c610d97874f..2dc82bddc2ef94238fc43a38ef330a854d86b397 100644 (file)
--- a/src/theory/bv/bitblaster.h
+++ b/src/theory/bv/bitblaster.h
@@ -2,8 +2,8 @@
 /*! \file bitblaster.h
  ** \verbatim
  ** Original author: Liana Hadarean
- ** Major contributors: none
- ** Minor contributors (to current version): lianah, Morgan Deters, Dejan Jovanovic
+ ** Major contributors: Andrew Reynolds
+ ** Minor contributors (to current version): Kshitij Bansal, Morgan Deters, Dejan Jovanovic
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/theory/bv/bv_inequality_graph.cpp b/src/theory/bv/bv_inequality_graph.cpp
index ccdfc1583a64fe0f1c376405d9ecbf0c41fe10d3..feb061ee1bb24cd0d72b26c71dce212ce82de018 100644 (file)
--- a/src/theory/bv/bv_inequality_graph.cpp
+++ b/src/theory/bv/bv_inequality_graph.cpp
@@ -2,7 +2,7 @@
 /*! \file bv_inequality_graph.cpp
  ** \verbatim
  ** Original author: Liana Hadarean
- ** Major contributors: lianah
+ ** Major contributors: none
  ** Minor contributors (to current version): Morgan Deters
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa

diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h
index 200c49195805cd3c535ae6efb395799b9b6f7776..9a898ebe63221646fd811b84e8a53428c07ec66b 100644 (file)
--- a/src/theory/bv/bv_inequality_graph.h
+++ b/src/theory/bv/bv_inequality_graph.h
@@ -1,8 +1,8 @@
 /*********************                                                        */
 /*! \file bv_inequality_graph.h
  ** \verbatim
- ** Original author: lianah
- ** Major contributors: Liana Hadarean
+ ** Original author: Liana Hadarean
+ ** Major contributors: none
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa

diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h
index 0b05512839bcf6b2ce3dfa4f8a20036c5ece8647..5a46f7a0fc2698df8e980345603485b4cef04313 100644 (file)
--- a/src/theory/bv/bv_subtheory.h
+++ b/src/theory/bv/bv_subtheory.h
@@ -2,8 +2,8 @@
 /*! \file bv_subtheory.h
  ** \verbatim
  ** Original author: Liana Hadarean
- ** Major contributors: Dejan Jovanovic, lianah
- ** Minor contributors (to current version): Morgan Deters
+ ** Major contributors: Andrew Reynolds, Dejan Jovanovic
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index 5a0c171345440c861a9d1acdd07f44377a1d1da0..e4b1a346d4f9ee19598d53979261c04264646914 100644 (file)
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -2,8 +2,8 @@
 /*! \file bv_subtheory_bitblast.cpp
  ** \verbatim
  ** Original author: Dejan Jovanovic
- ** Major contributors: lianah
- ** Minor contributors (to current version): Liana Hadarean, Morgan Deters
+ ** Major contributors: Liana Hadarean, Clark Barrett
+ ** Minor contributors (to current version): Morgan Deters, Andrew Reynolds, Kshitij Bansal
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h
index f1204dbdff5a41fa64be04b187855a8cf137b6d8..b1c1b3b66f7e5148ac853aff6b410e88c0d4fc09 100644 (file)
--- a/src/theory/bv/bv_subtheory_bitblast.h
+++ b/src/theory/bv/bv_subtheory_bitblast.h
@@ -2,8 +2,8 @@
 /*! \file bv_subtheory_bitblast.h
  ** \verbatim
  ** Original author: Dejan Jovanovic
- ** Major contributors: Morgan Deters, lianah
- ** Minor contributors (to current version): Liana Hadarean
+ ** Major contributors: none
+ ** Minor contributors (to current version): Morgan Deters, Andrew Reynolds, Liana Hadarean, Clark Barrett
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index 6d11364d9c8e167b37e34a169f94061afa49dbfa..2433dc1ee0d8e3487de6e2b54132c6a001a9fc47 100644 (file)
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -2,8 +2,8 @@
 /*! \file bv_subtheory_core.cpp
  ** \verbatim
  ** Original author: Liana Hadarean
- ** Major contributors: lianah
- ** Minor contributors (to current version): none
+ ** Major contributors: Andrew Reynolds
+ ** Minor contributors (to current version): Morgan Deters
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/theory/bv/bv_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h
index b886bbdd582355e10aba2bf4c4417f6f3e16434e..e1a73d40446ba13e6b6a9939f3dee7b291d17696 100644 (file)
--- a/src/theory/bv/bv_subtheory_core.h
+++ b/src/theory/bv/bv_subtheory_core.h
@@ -2,8 +2,8 @@
 /*! \file bv_subtheory_core.h
  ** \verbatim
  ** Original author: Liana Hadarean
- ** Major contributors: lianah
- ** Minor contributors (to current version): Dejan Jovanovic
+ ** Major contributors: Andrew Reynolds
+ ** Minor contributors (to current version): Dejan Jovanovic, Morgan Deters
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp
index 0eac4c035ce21e047e27b057940c7c4287e330ca..222ba303915048a5aba24771b7132518965ce4a3 100644 (file)
--- a/src/theory/bv/bv_subtheory_inequality.cpp
+++ b/src/theory/bv/bv_subtheory_inequality.cpp
@@ -1,9 +1,9 @@
 /*********************                                                        */
 /*! \file bv_subtheory_inequality.cpp
  ** \verbatim
- ** Original author: lianah
- ** Major contributors: Liana Hadarean
- ** Minor contributors (to current version): none
+ ** Original author: Liana Hadarean
+ ** Major contributors: Andrew Reynolds
+ ** Minor contributors (to current version): Morgan Deters
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/theory/bv/bv_subtheory_inequality.h b/src/theory/bv/bv_subtheory_inequality.h
index 6e0139e099cec69d7815b196e33c7c86fc2d7735..f142ff7be3c2f422c366726eea1bbf556ead3092 100644 (file)
--- a/src/theory/bv/bv_subtheory_inequality.h
+++ b/src/theory/bv/bv_subtheory_inequality.h
@@ -1,9 +1,9 @@
 /*********************                                                        */
 /*! \file bv_subtheory_inequality.h
  ** \verbatim
- ** Original author: lianah
- ** Major contributors: none
- ** Minor contributors (to current version): Liana Hadarean
+ ** Original author: Liana Hadarean
+ ** Major contributors: Andrew Reynolds
+ ** Minor contributors (to current version): Morgan Deters
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/theory/bv/bv_to_bool.cpp b/src/theory/bv/bv_to_bool.cpp
index 7bec805ef4dcd1b8726e2bac0d527b39a50adcbd..d137d09a0064ca7b1ebfaff88d91ad8c2971a866 100644 (file)
--- a/src/theory/bv/bv_to_bool.cpp
+++ b/src/theory/bv/bv_to_bool.cpp
@@ -1,9 +1,9 @@
 /*********************                                                        */
-/*! \file bv_to_bool.h
+/*! \file bv_to_bool.cpp
  ** \verbatim
- ** Original author: Liana Hadarean 
- ** Major contributors: None. 
- ** Minor contributors (to current version): None. 
+ ** Original author: Liana Hadarean
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/theory/bv/bv_to_bool.h b/src/theory/bv/bv_to_bool.h
index 186f2b317971ad51370dbaccc77a66a8e950a83b..b349237280e941afd3e8600c382ad58db4c6feaa 100644 (file)
--- a/src/theory/bv/bv_to_bool.h
+++ b/src/theory/bv/bv_to_bool.h
@@ -1,9 +1,9 @@
 /*********************                                                        */
 /*! \file bv_to_bool.h
  ** \verbatim
- ** Original author: Liana Hadarean 
- ** Major contributors: None. 
- ** Minor contributors (to current version): None. 
+ ** Original author: Liana Hadarean
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/theory/bv/slicer.cpp b/src/theory/bv/slicer.cpp
index e8e4ff84b7e4331a86e97a06ef350688e2c2b83a..56e0a479e1413d22dcafec27ac7ad16ee1f92685 100644 (file)
--- a/src/theory/bv/slicer.cpp
+++ b/src/theory/bv/slicer.cpp
@@ -2,8 +2,8 @@
 /*! \file slicer.cpp
  ** \verbatim
  ** Original author: Liana Hadarean
- ** Major contributors: lianah
- ** Minor contributors (to current version): none
+ ** Major contributors: none
+ ** Minor contributors (to current version): Morgan Deters
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/theory/bv/slicer.h b/src/theory/bv/slicer.h
index fefbad7561550c144c3befd3f69bddd8a786e83d..15c0b9c0b097df4f35e5700a887b0eca17b0417b 100644 (file)
--- a/src/theory/bv/slicer.h
+++ b/src/theory/bv/slicer.h
@@ -2,7 +2,7 @@
 /*! \file slicer.h
  ** \verbatim
  ** Original author: Liana Hadarean
- ** Major contributors: lianah
+ ** Major contributors: none
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index ce44b312df9f4ce445b2bf64778ce7c64dca82f6..14a19f2d0c8f8fdc057f14b31cac7d345d6f91aa 100644 (file)
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -2,8 +2,8 @@
 /*! \file theory_bv.cpp
  ** \verbatim
  ** Original author: Dejan Jovanovic
- ** Major contributors: Morgan Deters, Liana Hadarean, lianah
- ** Minor contributors (to current version): Tim King, Andrew Reynolds, Clark Barrett
+ ** Major contributors: Morgan Deters, Liana Hadarean
+ ** Minor contributors (to current version): Tim King, Kshitij Bansal, Clark Barrett, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 708206d28119128bcb9af7231bcb4603fc485fda..90093edfd38c9e043cb39da1293c6d7d8d52e86d 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: Morgan Deters
- ** Major contributors: lianah, Dejan Jovanovic, Liana Hadarean
- ** Minor contributors (to current version): Clark Barrett, Tim King, Andrew Reynolds
+ ** Major contributors: Dejan Jovanovic, Liana Hadarean
+ ** Minor contributors (to current version): Clark Barrett, Kshitij Bansal, Tim King, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
index 9f3d12415dc96d98bd3b7708e32473ccee75dace..db774ebe375ee4358315dd1d70dd96ba55a35350 100644 (file)
--- a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Liana Hadarean
  ** Major contributors: Clark Barrett
- ** Minor contributors (to current version): lianah, Morgan Deters, Tim King
+ ** Minor contributors (to current version): Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
index b513dbf904d9708b8db2c89a6fa7d9d4964ed91f..6c0ba90d4a4b0576b0467b478019b0a4d5f68ca3 100644 (file)
--- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
@@ -2,8 +2,8 @@
 /*! \file theory_bv_rewrite_rules_operator_elimination.h
  ** \verbatim
  ** Original author: Liana Hadarean
- ** Major contributors: Clark Barrett
- ** Minor contributors (to current version): Morgan Deters, Tim King
+ ** Major contributors: Morgan Deters, Clark Barrett
+ ** Minor contributors (to current version): Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index 76eb97b39ff3d7442912d50118e2410e1a9015f4..0b09bce4dcef2c980624bd6e0db2be2f8c209f30 100644 (file)
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Dejan Jovanovic
  ** Major contributors: Liana Hadarean
- ** Minor contributors (to current version): Tim King, Morgan Deters, Clark Barrett
+ ** Minor contributors (to current version): Tim King, Clark Barrett, Morgan Deters
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h
index b51c56b182f2428e3505ccd065c4e0e247f66791..12e2581772f063c21cc05b6a0a90a25f9dbaa540 100644 (file)
--- a/src/theory/bv/theory_bv_type_rules.h
+++ b/src/theory/bv/theory_bv_type_rules.h
@@ -2,7 +2,7 @@
 /*! \file theory_bv_type_rules.h
  ** \verbatim
  ** Original author: Dejan Jovanovic
- ** Major contributors: Liana Hadarean, Morgan Deters, Christopher L. Conway
+ ** Major contributors: Liana Hadarean, Christopher L. Conway, Morgan Deters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa

diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index ab6a615a2e7dfb354adcb5dbf9b7df179c6664a1..5140bd498d60893153bbce3bef1d4de6ec39bb09 100644 (file)
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -2,8 +2,8 @@
 /*! \file theory_bv_utils.h
  ** \verbatim
  ** Original author: Dejan Jovanovic
- ** Major contributors: lianah, Liana Hadarean
- ** Minor contributors (to current version): Clark Barrett, Morgan Deters
+ ** Major contributors: Liana Hadarean
+ ** Minor contributors (to current version): Clark Barrett, Morgan Deters, Kshitij Bansal
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h
index cec1dccfcf21ef34e11a202453b32025f45320f8..ffd34d7773745cc5841b2816d05577d540c85197 100644 (file)
--- a/src/theory/datatypes/type_enumerator.h
+++ b/src/theory/datatypes/type_enumerator.h
@@ -2,7 +2,7 @@
 /*! \file type_enumerator.h
  ** \verbatim
  ** Original author: Morgan Deters
- ** Major contributors: none
+ ** Major contributors: Andrew Reynolds
  ** Minor contributors (to current version): Dejan Jovanovic
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa

diff --git a/src/theory/decision_attributes.h b/src/theory/decision_attributes.h
index 79f58feb1888b6c31969923cb24990e9c44c0c9d..fa934ecc7cb09c2d42f4508bad459e6e97afb000 100644 (file)
--- a/src/theory/decision_attributes.h
+++ b/src/theory/decision_attributes.h
@@ -2,7 +2,7 @@
 /*! \file decision_attributes.h
  ** \verbatim
  ** Original author: Kshitij Bansal
- ** Major contributors: none
+ ** Major contributors: Morgan Deters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa

diff --git a/src/theory/idl/idl_assertion.cpp b/src/theory/idl/idl_assertion.cpp
index 1e725932bf782cbf1ecbfabbf5b2c5a13d3d91d6..717122195ba17d4f49e997bd8588a85a793fdacc 100644 (file)
--- a/src/theory/idl/idl_assertion.cpp
+++ b/src/theory/idl/idl_assertion.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Dejan Jovanovic
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Morgan Deters
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/theory/idl/idl_assertion.h b/src/theory/idl/idl_assertion.h
index 8ce0e93b280694fbbab5b4352c5cd88854615bdc..d0328e6006fef838e2750c3ae8aa2dbe12e9024e 100644 (file)
--- a/src/theory/idl/idl_assertion.h
+++ b/src/theory/idl/idl_assertion.h
@@ -2,7 +2,7 @@
 /*! \file idl_assertion.h
  ** \verbatim
  ** Original author: Dejan Jovanovic
- ** Major contributors: none
+ ** Major contributors: Morgan Deters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa

diff --git a/src/theory/idl/idl_assertion_db.cpp b/src/theory/idl/idl_assertion_db.cpp
index 697c70c025d86c5012f81ed712a52b6cdece983b..6920840711fd1bb0c00a51e8f03a0a6c73d83959 100644 (file)
--- a/src/theory/idl/idl_assertion_db.cpp
+++ b/src/theory/idl/idl_assertion_db.cpp
@@ -2,7 +2,7 @@
 /*! \file idl_assertion_db.cpp
  ** \verbatim
  ** Original author: Dejan Jovanovic
- ** Major contributors: none
+ ** Major contributors: Morgan Deters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa

diff --git a/src/theory/idl/idl_assertion_db.h b/src/theory/idl/idl_assertion_db.h
index 0501bc6bf144d3e51eb11fcd9482c05ccdb0cc00..205102b0f7c63f65624ac6543df9dd639be6c196 100644 (file)
--- a/src/theory/idl/idl_assertion_db.h
+++ b/src/theory/idl/idl_assertion_db.h
@@ -2,7 +2,7 @@
 /*! \file idl_assertion_db.h
  ** \verbatim
  ** Original author: Dejan Jovanovic
- ** Major contributors: none
+ ** Major contributors: Morgan Deters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa

diff --git a/src/theory/idl/idl_model.cpp b/src/theory/idl/idl_model.cpp
index 75f4834eaeef69636e1ae91c12f66974c00dff17..71cd443145dddca069e77b16603e71d1b8c5d02e 100644 (file)
--- a/src/theory/idl/idl_model.cpp
+++ b/src/theory/idl/idl_model.cpp
@@ -2,7 +2,7 @@
 /*! \file idl_model.cpp
  ** \verbatim
  ** Original author: Dejan Jovanovic
- ** Major contributors: none
+ ** Major contributors: Morgan Deters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa

diff --git a/src/theory/idl/idl_model.h b/src/theory/idl/idl_model.h
index 64407684b8861c816da8b132e52614bfdf83519b..22e05c469ca4a1bc004f3d03bda70d70556a696e 100644 (file)
--- a/src/theory/idl/idl_model.h
+++ b/src/theory/idl/idl_model.h
@@ -2,7 +2,7 @@
 /*! \file idl_model.h
  ** \verbatim
  ** Original author: Dejan Jovanovic
- ** Major contributors: none
+ ** Major contributors: Morgan Deters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa

diff --git a/src/theory/idl/theory_idl.cpp b/src/theory/idl/theory_idl.cpp
index e5100fc715ff6afdf55e4e97456842788005d2dd..987973bf3333dda5f32a93c8928c88ec6f4e5e77 100644 (file)
--- a/src/theory/idl/theory_idl.cpp
+++ b/src/theory/idl/theory_idl.cpp
@@ -2,7 +2,7 @@
 /*! \file theory_idl.cpp
  ** \verbatim
  ** Original author: Dejan Jovanovic
- ** Major contributors: none
+ ** Major contributors: Morgan Deters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa

diff --git a/src/theory/idl/theory_idl.h b/src/theory/idl/theory_idl.h
index c629ad2b05b68ce3885074120470b7c5f3bcab11..4597d4c6abaf74a26a492095a23e031cd49b043a 100644 (file)
--- a/src/theory/idl/theory_idl.h
+++ b/src/theory/idl/theory_idl.h
@@ -2,7 +2,7 @@
 /*! \file theory_idl.h
  ** \verbatim
  ** Original author: Dejan Jovanovic
- ** Major contributors: none
+ ** Major contributors: Morgan Deters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa

diff --git a/src/theory/ite_utilities.cpp b/src/theory/ite_utilities.cpp
index facd5f4f0ce74070517c1e55d5448c49da8a1f9c..1b4e096f2d8382192b39fafc250830e9625a57eb 100644 (file)
--- a/src/theory/ite_utilities.cpp
+++ b/src/theory/ite_utilities.cpp
@@ -1,9 +1,9 @@
 /*********************                                                        */
-/*! \file ite_simplifier.cpp
+/*! \file ite_utilities.cpp
  ** \verbatim
- ** Original author: Clark Barrett
+ ** Original author: Tim King
  ** Major contributors: none
- ** Minor contributors (to current version): Morgan Deters
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/theory/ite_utilities.h b/src/theory/ite_utilities.h
index 73f0386d208409ad6ddf1031c0e812a75d01e768..d9e6120aa533821f8401db155dd6d3a6e2ce341c 100644 (file)
--- a/src/theory/ite_utilities.h
+++ b/src/theory/ite_utilities.h
@@ -1,9 +1,9 @@
 /*********************                                                        */
-/*! \file ite_simplifier.h
+/*! \file ite_utilities.h
  ** \verbatim
- ** Original author: Clark Barrett
+ ** Original author: Tim King
  ** Major contributors: none
- ** Minor contributors (to current version): Morgan Deters
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp
index 080550a166fd25a15a141f96778c4a6d58215783..28485a979710599f9d847d9bc7fb52301e06b9a3 100644 (file)
--- a/src/theory/quantifiers/bounded_integers.cpp
+++ b/src/theory/quantifiers/bounded_integers.cpp
@@ -2,6 +2,8 @@
 /*! \file bounded_integers.cpp
  ** \verbatim
  ** Original author: Andrew Reynolds
+ ** Major contributors: Morgan Deters
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/theory/quantifiers/bounded_integers.h b/src/theory/quantifiers/bounded_integers.h
index 3da938d3120506e063b9a830aacef1c31f6882cc..972bdb2ec9ffa869a16aa4735afb74b5eff0e09f 100644 (file)
--- a/src/theory/quantifiers/bounded_integers.h
+++ b/src/theory/quantifiers/bounded_integers.h
@@ -1,13 +1,16 @@
 /*********************                                                        */
 /*! \file bounded_integers.h
-** \verbatim
-** Original author: Andrew Reynolds
-** This file is part of the CVC4 project.
-** Copyright (c) 2009-2013  New York University and The University of Iowa
-** See the file COPYING in the top-level source directory for licensing
-** information.\endverbatim
-**
-** \brief This class manages integer bounds for quantifiers
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: Morgan Deters
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
 **/
 
 #include "cvc4_private.h"

diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp
index 42b49cf01d77ae0c32180ea7796eb137bab27fbf..783f6284d4dc5d343b695d331abc0d62ef4ea4d5 100644 (file)
--- a/src/theory/quantifiers/candidate_generator.cpp
+++ b/src/theory/quantifiers/candidate_generator.cpp
@@ -2,7 +2,7 @@
 /*! \file candidate_generator.cpp
  ** \verbatim
  ** Original author: Morgan Deters
- ** Major contributors: none
+ ** Major contributors: Andrew Reynolds
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa

diff --git a/src/theory/quantifiers/candidate_generator.h b/src/theory/quantifiers/candidate_generator.h
index 402a298485d7042a1a3bb74b0adf4be655c2e398..a87c24596e9cfe3516ef96a3689ede69b7b6e71f 100644 (file)
--- a/src/theory/quantifiers/candidate_generator.h
+++ b/src/theory/quantifiers/candidate_generator.h
@@ -2,7 +2,7 @@
 /*! \file candidate_generator.h
  ** \verbatim
  ** Original author: Morgan Deters
- ** Major contributors: none
+ ** Major contributors: Andrew Reynolds
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa

diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index fa4961352d6a68d52836df4b8c3171b0c62067a9..bda124e963680e04aed4167aa4995a1ea34ed5a8 100644 (file)
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -2,8 +2,8 @@
 /*! \file first_order_model.cpp
  ** \verbatim
  ** Original author: Andrew Reynolds
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
+ ** Major contributors: none
+ ** Minor contributors (to current version): Morgan Deters
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/theory/quantifiers/first_order_reasoning.cpp b/src/theory/quantifiers/first_order_reasoning.cpp
index ebfb55f08f7589fa10d0df0e4e0a7e968fd4340c..a696af3c2a08da6c6035c764a7068cd784c5a067 100644 (file)
--- a/src/theory/quantifiers/first_order_reasoning.cpp
+++ b/src/theory/quantifiers/first_order_reasoning.cpp
@@ -1,11 +1,11 @@
 /*********************                                                        */
 /*! \file first_order_reasoning.cpp
  ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: none
+ ** Original author: Andrew Reynolds
+ ** Major contributors: Morgan Deters
  ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012  New York University and The University of Iowa
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **

diff --git a/src/theory/quantifiers/first_order_reasoning.h b/src/theory/quantifiers/first_order_reasoning.h
index 5f217050cfe7c97839b6eb45bff019405f4b89db..6bc5c21c1be0a6a33ed2b489adf074b9ae26bc48 100644 (file)
--- a/src/theory/quantifiers/first_order_reasoning.h
+++ b/src/theory/quantifiers/first_order_reasoning.h
@@ -1,11 +1,11 @@
 /*********************                                                        */
 /*! \file first_order_reasoning.h
  ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: none
+ ** Original author: Andrew Reynolds
+ ** Major contributors: Morgan Deters
  ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012  New York University and The University of Iowa
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **

diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index c22d903f969c3424a6e769bcc595856aceb7ffbc..2f32ec5e664ffd227bd64a93ca12388404a6e39f 100644 (file)
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -2,6 +2,8 @@
 /*! \file full_model_check.cpp
  ** \verbatim
  ** Original author: Andrew Reynolds
+ ** Major contributors: Morgan Deters
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h
index abe05d3c7a2afb65b45657e2f20f5afb63952b24..6063928313c4bdd8f4c03926899dd31ca5fe2a30 100644 (file)
--- a/src/theory/quantifiers/full_model_check.h
+++ b/src/theory/quantifiers/full_model_check.h
@@ -2,6 +2,8 @@
 /*! \file full_model_check.h
  ** \verbatim
  ** Original author: Andrew Reynolds
+ ** Major contributors: Morgan Deters
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index 4fe4072a380ddd74453632efb73c099a03256a14..6cc446e35468ac99813b77ef27d0de5da017c792 100644 (file)
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Andrew Reynolds
  ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h
index 821beeae0f2b668272641a3a2b5adb0274e06dd9..c70c90b2953d70cc3834979da617839c41a09aba 100644 (file)
--- a/src/theory/quantifiers/inst_strategy_cbqi.h
+++ b/src/theory/quantifiers/inst_strategy_cbqi.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Andrew Reynolds
  ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp
old mode 100755 (executable)
new mode 100644 (file)

diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h
old mode 100755 (executable)
new mode 100644 (file)

diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp
old mode 100755 (executable)
new mode 100644 (file)
index 107a990..441ab02
--- a/src/theory/quantifiers/rewrite_engine.cpp
+++ b/src/theory/quantifiers/rewrite_engine.cpp
@@ -1,7 +1,9 @@
 /*********************                                                        */
-/*! \file bounded_integers.cpp
+/*! \file rewrite_engine.cpp
  ** \verbatim
  ** Original author: Andrew Reynolds
+ ** Major contributors: Morgan Deters
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/theory/quantifiers/rewrite_engine.h b/src/theory/quantifiers/rewrite_engine.h
old mode 100755 (executable)
new mode 100644 (file)
index 2d9d751..a9a2f9b
--- a/src/theory/quantifiers/rewrite_engine.h
+++ b/src/theory/quantifiers/rewrite_engine.h
@@ -1,13 +1,16 @@
 /*********************                                                        */
-/*! \file bounded_integers.h
-** \verbatim
-** Original author: Andrew Reynolds
-** This file is part of the CVC4 project.
-** Copyright (c) 2009-2013  New York University and The University of Iowa
-** See the file COPYING in the top-level source directory for licensing
-** information.\endverbatim
-**
-** \brief This class manages integer bounds for quantifiers
+/*! \file rewrite_engine.h
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: Morgan Deters
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
 **/
 
 #include "cvc4_private.h"

diff --git a/src/theory/quantifiers/symmetry_breaking.cpp b/src/theory/quantifiers/symmetry_breaking.cpp
old mode 100755 (executable)
new mode 100644 (file)
index 507a508..66a3ac7
--- a/src/theory/quantifiers/symmetry_breaking.cpp
+++ b/src/theory/quantifiers/symmetry_breaking.cpp
@@ -1,11 +1,11 @@
 /*********************                                                        */
 /*! \file symmetry_breaking.cpp
  ** \verbatim
- ** Original author: ajreynol
+ ** Original author: Andrew Reynolds
  ** Major contributors: none
  ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012  New York University and The University of Iowa
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **

diff --git a/src/theory/quantifiers/symmetry_breaking.h b/src/theory/quantifiers/symmetry_breaking.h
old mode 100755 (executable)
new mode 100644 (file)
index 7f6855f..d7d9e0f
--- a/src/theory/quantifiers/symmetry_breaking.h
+++ b/src/theory/quantifiers/symmetry_breaking.h
@@ -1,11 +1,11 @@
 /*********************                                                        */
 /*! \file symmetry_breaking.h
  ** \verbatim
- ** Original author: ajreynol
+ ** Original author: Andrew Reynolds
  ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012  New York University and The University of Iowa
+ ** Minor contributors (to current version): Morgan Deters
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **

diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 066282c2ce58d49ac274ed2b43f5d86c872f9ef7..e72242fe9c1f2088f049971312067316acfd0eb4 100644 (file)
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -2,8 +2,8 @@
 /*! \file theory_quantifiers.cpp
  ** \verbatim
  ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): Dejan Jovanovic, Andrew Reynolds
+ ** Major contributors: Andrew Reynolds
+ ** Minor contributors (to current version): Dejan Jovanovic
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
old mode 100755 (executable)
new mode 100644 (file)

diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp
index f9add4faceb59d9704c4e61c3721c83b7a1cb9d7..f121848692e4498b87185ea00a24f4d987973641 100644 (file)
--- a/src/theory/rewriter.cpp
+++ b/src/theory/rewriter.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Dejan Jovanovic
  ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): Clark Barrett
+ ** Minor contributors (to current version): Liana Hadarean, Clark Barrett
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h
index 24f09e62d9535cc1bd0056d272fc69654c276dc2..f88de72f9fa5faf5087ba1528f3ec5dcfaf66ebd 100644 (file)
--- a/src/theory/rewriter.h
+++ b/src/theory/rewriter.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Dejan Jovanovic
  ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/theory/rewriter_tables_template.h b/src/theory/rewriter_tables_template.h
index 17aed4e42afbc763a906f1fc0b4513535a14222c..aa2964e13380fb1c01c64eed841eae9b0b28a057 100644 (file)
--- a/src/theory/rewriter_tables_template.h
+++ b/src/theory/rewriter_tables_template.h
@@ -2,7 +2,7 @@
 /*! \file rewriter_tables_template.h
  ** \verbatim
  ** Original author: Dejan Jovanovic
- ** Major contributors: Morgan Deters
+ ** Major contributors: Morgan Deters, Tim King
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa

diff --git a/src/theory/rewriterules/theory_rewriterules_rewriter.h b/src/theory/rewriterules/theory_rewriterules_rewriter.h
index f494714078bfa3ab39a3efc70a1520e49fae12f4..511ef35151cd2ce125ca912547e7cc43062191c3 100644 (file)
--- a/src/theory/rewriterules/theory_rewriterules_rewriter.h
+++ b/src/theory/rewriterules/theory_rewriterules_rewriter.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Morgan Deters
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index f26037cf050b676ab77be5a0504e0dffbb73e7c2..e7079081bf45a1e95f47070c6148458c1947d5e2 100644 (file)
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -1,14 +1,14 @@
-/*********************                                                        */\r
-/*! \file regexp_operation.CPP\r
- ** \verbatim\r
- ** Original author: Tianyi Liang\r
- ** Major contributors: Tianyi Liang, Andrew Reynolds\r
- ** Minor contributors (to current version): none\r
- ** This file is part of the CVC4 prototype.\r
- ** Copyright (c) 2013-2013  New York University and The University of Iowa\r
- ** See the file COPYING in the top-level source directory for licensing\r
- ** information.\endverbatim\r
- **\r
+/*********************                                                        */
+/*! \file regexp_operation.cpp
+ ** \verbatim
+ ** Original author: Tianyi Liang
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
  ** \brief Regular Expresion Operations\r
  **\r
  ** Regular Expresion Operations\r

diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h
index 702e5ba84d6f39b136a370a801f968c29da31bfb..a47f7bd776f49549d0b3b1db5293b5656686b921 100644 (file)
--- a/src/theory/strings/regexp_operation.h
+++ b/src/theory/strings/regexp_operation.h
@@ -1,14 +1,14 @@
-/*********************                                                        */\r
-/*! \file regexp_operation.h\r
- ** \verbatim\r
- ** Original author: Tianyi Liang\r
- ** Major contributors: Tianyi Liang, Andrew Reynolds\r
- ** Minor contributors (to current version): none\r
- ** This file is part of the CVC4 prototype.\r
- ** Copyright (c) 2013-2013  New York University and The University of Iowa\r
- ** See the file COPYING in the top-level source directory for licensing\r
- ** information.\endverbatim\r
- **\r
+/*********************                                                        */
+/*! \file regexp_operation.h
+ ** \verbatim
+ ** Original author: Tianyi Liang
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
  ** \brief Regular Expresion Operations\r
  **\r
  ** Regular Expresion Operations\r

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 9a88883fc71762dff1d4558d206f4948fc93275b..9f4d84765bbd449a16a281c7393b36510a9baebd 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -2,10 +2,10 @@
 /*! \file theory_strings.cpp
  ** \verbatim
  ** Original author: Tianyi Liang
- ** Major contributors: Tianyi Liang, Andrew Reynolds
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2013-2013  New York University and The University of Iowa
+ ** Major contributors: none
+ ** Minor contributors (to current version): Morgan Deters
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **

diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 9fae67a9f95f8122923102806348898b6147b2c1..4d2a192cf265f5066ffe86b0f94602d0386d1b0a 100644 (file)
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -4,8 +4,8 @@
  ** Original author: Tianyi Liang
  ** Major contributors: none
  ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2013-2013  New York University and The University of Iowa
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **

diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index c54cbb3b2aa121d25d69b24d072cb191c075a837..9da0e343dbfb5ea24c2dd786e89fac27072f1351 100644 (file)
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -2,10 +2,10 @@
 /*! \file theory_strings_preprocess.cpp
  ** \verbatim
  ** Original author: Tianyi Liang
- ** Major contributors: Tianyi Liang, Andrew Reynolds
+ ** Major contributors: Morgan Deters
  ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2013-2013  New York University and The University of Iowa
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **

diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h
index 7bc60c1a1d4c49e5ce54a330a1b09687c8413d4a..698ef6ba158ce72c0c8668a5fc250ea5b476da35 100644 (file)
--- a/src/theory/strings/theory_strings_preprocess.h
+++ b/src/theory/strings/theory_strings_preprocess.h
@@ -2,10 +2,10 @@
 /*! \file theory_strings_preprocess.h
  ** \verbatim
  ** Original author: Tianyi Liang
- ** Major contributors: Tianyi Liang, Andrew Reynolds
+ ** Major contributors: Morgan Deters
  ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2013-2013  New York University and The University of Iowa
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 73f17a146dcd042d1717ca0c7541e513f8ed045a..cd9db85c796daf65ea1a219a67cd4bc19310b607 100644 (file)
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -4,8 +4,8 @@
  ** Original author: Tianyi Liang
  ** Major contributors: none
  ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2013-2013  New York University and The University of Iowa
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **

diff --git a/src/theory/strings/theory_strings_rewriter.h b/src/theory/strings/theory_strings_rewriter.h
index 78f0da59eaeddde830f18fc422f328b744e3eed5..3181762978077eaea33da0738d8959b3e2257f87 100644 (file)
--- a/src/theory/strings/theory_strings_rewriter.h
+++ b/src/theory/strings/theory_strings_rewriter.h
@@ -4,8 +4,8 @@
  ** Original author: Tianyi Liang
  ** Major contributors: none
  ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2013-2013  New York University and The University of Iowa
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **

diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h
index 080d6abf565021089ffb7c8882523a16b3e5dd5e..d5019ab3990730d7f68c463b73e2d47a6f93b1bf 100644 (file)
--- a/src/theory/strings/theory_strings_type_rules.h
+++ b/src/theory/strings/theory_strings_type_rules.h
@@ -4,8 +4,8 @@
  ** Original author: Tianyi Liang
  ** Major contributors: none
  ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2013-2013  New York University and The University of Iowa
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index af4dea293e030ec138fd3826d64737bbc131ee71..7cf4d7ad964422f03e09b27b7e93ac59ca20727c 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Morgan Deters
  ** Major contributors: Dejan Jovanovic
- ** Minor contributors (to current version): Christopher L. Conway, Kshitij Bansal, Tim King, Liana Hadarean, Clark Barrett, Andrew Reynolds
+ ** Minor contributors (to current version): Christopher L. Conway, Kshitij Bansal, Liana Hadarean, Clark Barrett, Tim King, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index e5b2ad8d2c2df07ff053eff445a7623aabd055a9..ffc36e59b7fa5e47fa06be5629746703e6850f92 100644 (file)
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Morgan Deters
  ** Major contributors: Dejan Jovanovic
- ** Minor contributors (to current version): Christopher L. Conway, Francois Bobot, Kshitij Bansal, Liana Hadarean, Clark Barrett, Tim King, Andrew Reynolds
+ ** Minor contributors (to current version): Christopher L. Conway, Francois Bobot, Kshitij Bansal, Clark Barrett, Liana Hadarean, Tim King, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 73ff068b4f82628112e823d867b9b3ab906f69e5..4f753187ffbeef6ddebf8210489599ebbc26e647 100644 (file)
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -1,8 +1,8 @@
 /*********************                                                        */
 /*! \file theory_model.cpp
  ** \verbatim
- ** Original author: Andrew Reynolds
- ** Major contributors: Morgan Deters, Clark Barrett
+ ** Original author: Morgan Deters
+ ** Major contributors: Andrew Reynolds, Clark Barrett
  ** Minor contributors (to current version): Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa

diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h
index 9da9cb5e2bf24cec4b8fa40b480b8aa2583aa70a..598db2683c82e9308395965a92f932c0b313810e 100644 (file)
--- a/src/theory/theory_model.h
+++ b/src/theory/theory_model.h
@@ -1,8 +1,8 @@
 /*********************                                                        */
 /*! \file theory_model.h
  ** \verbatim
- ** Original author: Andrew Reynolds
- ** Major contributors: Morgan Deters, Clark Barrett
+ ** Original author: Morgan Deters
+ ** Major contributors: Andrew Reynolds, Clark Barrett
  ** Minor contributors (to current version): Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa

diff --git a/src/theory/theory_registrar.h b/src/theory/theory_registrar.h
index d77bf1eb09ae36c960e3ecd5b0436ca3204fc21a..691c1147bbdeba76b21afd5ee17183a0fafb6ca9 100644 (file)
--- a/src/theory/theory_registrar.h
+++ b/src/theory/theory_registrar.h
@@ -2,7 +2,7 @@
 /*! \file theory_registrar.h
  ** \verbatim
  ** Original author: Liana Hadarean
- ** Major contributors: Tim King, Morgan Deters
+ ** Major contributors: Morgan Deters, Tim King
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa

diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 199581b989b0b7ed5fabea03a5aa57172a81cd5b..cb44b42dfe605f92a85d9b009759a12dd1889a77 100644 (file)
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Dejan Jovanovic
  ** Major contributors: none
- ** Minor contributors (to current version): Tim King, Francois Bobot, Morgan Deters
+ ** Minor contributors (to current version): Dejan Jovanovic, Tim King, Francois Bobot, Morgan Deters
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index a9294dc696d6e1bc22aaf21651bc0ccfb80b1afc..ab106bc8db62a70c8ae998cf964a13c35cf6207e 100644 (file)
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Dejan Jovanovic
  ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): Tim King, Liana Hadarean, Andrew Reynolds
+ ** Minor contributors (to current version): Tim King, Dejan Jovanovic, Liana Hadarean, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp
index bf41a256de7c4aaaea7aa0a962b852a7b5d6fc14..409b41e3ffa506fdd9010cc963fd963ea11a34b8 100644 (file)
--- a/src/theory/uf/theory_uf_model.cpp
+++ b/src/theory/uf/theory_uf_model.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Andrew Reynolds
  ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): Clark Barrett
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/theory/uf/theory_uf_rewriter.h b/src/theory/uf/theory_uf_rewriter.h
index 40713fa41800382b7919ed56177d17dbffefc37e..3bd316c93456c3232dc911e7a0d346308a09e6dc 100644 (file)
--- a/src/theory/uf/theory_uf_rewriter.h
+++ b/src/theory/uf/theory_uf_rewriter.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Dejan Jovanovic
  ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Clark Barrett
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h
index 50a746205c909e4c81065ba5494207da93e63179..b4d1b6d48482c1a33db4100b50f7984bacad2cf0 100644 (file)
--- a/src/theory/uf/theory_uf_type_rules.h
+++ b/src/theory/uf/theory_uf_type_rules.h
@@ -2,8 +2,8 @@
 /*! \file theory_uf_type_rules.h
  ** \verbatim
  ** Original author: Dejan Jovanovic
- ** Major contributors: Christopher L. Conway, Morgan Deters
- ** Minor contributors (to current version): Andrew Reynolds, Tim King
+ ** Major contributors: Christopher L. Conway, Andrew Reynolds, Morgan Deters
+ ** Minor contributors (to current version): Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/theory/unconstrained_simplifier.cpp b/src/theory/unconstrained_simplifier.cpp
index 8bbdded3e59cacb25892acb8ec7fbc61f5c03866..a6e885f975162c60ed396142bf12b752b3b27252 100644 (file)
--- a/src/theory/unconstrained_simplifier.cpp
+++ b/src/theory/unconstrained_simplifier.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Clark Barrett
  ** Major contributors: none
- ** Minor contributors (to current version): Morgan Deters
+ ** Minor contributors (to current version): Tim King, Morgan Deters
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/theory/unconstrained_simplifier.h b/src/theory/unconstrained_simplifier.h
index 0ee754256c2d6c91cdb3f472c0babb87cd03e28b..d41c7db5d48d7d8786fac62220087d8b85b9fe34 100644 (file)
--- a/src/theory/unconstrained_simplifier.h
+++ b/src/theory/unconstrained_simplifier.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Clark Barrett
  ** Major contributors: none
- ** Minor contributors (to current version): Morgan Deters
+ ** Minor contributors (to current version): Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/util/bitvector.h b/src/util/bitvector.h
index 04e23217bcbce034c7ae1693423f03e27edd0d2b..e826a6704c8ce14117be4a5012bf8546a6199f1a 100644 (file)
--- a/src/util/bitvector.h
+++ b/src/util/bitvector.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Dejan Jovanovic
  ** Major contributors: Morgan Deters, Liana Hadarean
- ** Minor contributors (to current version): lianah, Christopher L. Conway
+ ** Minor contributors (to current version): Christopher L. Conway
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/util/configuration.cpp b/src/util/configuration.cpp
index f03c5e9590260561307fa0ddbdd69572effc33f3..0d22325e79a3c1a714f50e0172af1cbd3c0f4c7f 100644 (file)
--- a/src/util/configuration.cpp
+++ b/src/util/configuration.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Morgan Deters
  ** Major contributors: none
- ** Minor contributors (to current version): Liana Hadarean, ACSYS, Christopher L. Conway, Dejan Jovanovic, Francois Bobot
+ ** Minor contributors (to current version): Liana Hadarean, Tim King, ACSYS, Christopher L. Conway, Dejan Jovanovic, Francois Bobot
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/util/configuration.h b/src/util/configuration.h
index 7e543c54e5eee8f7e8383b198406c1002e84512a..be49e3dcf33d1297ca2838ed78ac93e9db80fc12 100644 (file)
--- a/src/util/configuration.h
+++ b/src/util/configuration.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Morgan Deters
  ** Major contributors: none
- ** Minor contributors (to current version): ACSYS, Liana Hadarean, Francois Bobot
+ ** Minor contributors (to current version): ACSYS, Liana Hadarean, Tim King, Francois Bobot
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/util/configuration_private.h b/src/util/configuration_private.h
index 3b3115887603c8f1ba08e2069615e1716a787f7c..e33c5fa36236d82b16c7604a72f1b104bbf11c65 100644 (file)
--- a/src/util/configuration_private.h
+++ b/src/util/configuration_private.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Christopher L. Conway
  ** Major contributors: ACSYS, Morgan Deters
- ** Minor contributors (to current version): Liana Hadarean
+ ** Minor contributors (to current version): Liana Hadarean, Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/util/dense_map.h b/src/util/dense_map.h
index 8f8b63668d1c2e55ac6f489cae82783e35232ec8..10ca9f72fa6a4b5803b679a2814f8f9f15da819f 100644 (file)
--- a/src/util/dense_map.h
+++ b/src/util/dense_map.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Tim King
  ** Major contributors: none
- ** Minor contributors (to current version): Dejan Jovanovic, Morgan Deters
+ ** Minor contributors (to current version): Morgan Deters, Dejan Jovanovic
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/util/gmp_util.h b/src/util/gmp_util.h
index f2cd0004fb6970004abdee1fd2928d5808beab26..b5654e9cb012b0f25e7d690a3addb116a7ee7406 100644 (file)
--- a/src/util/gmp_util.h
+++ b/src/util/gmp_util.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Dejan Jovanovic
  ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): Tim King
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/util/hash.h b/src/util/hash.h
index 34ca8be5b26fba13faf4d24f6583ddef39a95d19..0cdc96fcb94c0dbb83ac9a2094cb2deb980c9d6a 100644 (file)
--- a/src/util/hash.h
+++ b/src/util/hash.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Christopher L. Conway
  ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): Dejan Jovanovic, Tim King
+ ** Minor contributors (to current version): Dejan Jovanovic
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/util/index.h b/src/util/index.h
index 356dbdd8fe95da6cd8305228bfa377bccf05a408..be3e2918b756d4cf70320a0cb34a6e206bc22651 100644 (file)
--- a/src/util/index.h
+++ b/src/util/index.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Tim King
  ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): lianah
+ ** Minor contributors (to current version): Liana Hadarean
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/src/util/ite_removal.cpp b/src/util/ite_removal.cpp
index 5231e05c2261f4faaf0ca12644ea455aa2deeefc..0dfea439975f2a4728d6ef8d55fc382d2276c2ee 100644 (file)
--- a/src/util/ite_removal.cpp
+++ b/src/util/ite_removal.cpp
@@ -2,7 +2,7 @@
 /*! \file ite_removal.cpp
  ** \verbatim
  ** Original author: Dejan Jovanovic
- ** Major contributors: Andrew Reynolds, Morgan Deters
+ ** Major contributors: Morgan Deters, Andrew Reynolds, Tim King
  ** Minor contributors (to current version): Clark Barrett
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa

diff --git a/src/util/ite_removal.h b/src/util/ite_removal.h
index 9d79687f441bb9e98e73d48c7904d2614b166f45..c2464636e7c5f9b60f17f573da87709364d118c8 100644 (file)
--- a/src/util/ite_removal.h
+++ b/src/util/ite_removal.h
@@ -2,7 +2,7 @@
 /*! \file ite_removal.h
  ** \verbatim
  ** Original author: Dejan Jovanovic
- ** Major contributors: Kshitij Bansal, Morgan Deters
+ ** Major contributors: Kshitij Bansal, Morgan Deters, Tim King
  ** Minor contributors (to current version): Andrew Reynolds, Clark Barrett
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa

diff --git a/src/util/maybe.h b/src/util/maybe.h
index 795eac759a5af3c502a9ee0cb77438d06916555b..e90953e0b864c5999cd73f36d58f2ef4c124a764 100644 (file)
--- a/src/util/maybe.h
+++ b/src/util/maybe.h
@@ -1,11 +1,11 @@
 /*********************                                                        */
 /*! \file maybe.h
  ** \verbatim
- ** Original author: taking
+ ** Original author: Tim King
  ** Major contributors: none
- ** Minor contributors (to current version): mdeters
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012  New York University and The University of Iowa
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **

diff --git a/src/util/model.cpp b/src/util/model.cpp
index 1d14a7c4fc2d17523889afccf11d01ff8f87c8e2..e25065c21982246ffca4272aa157942e9cade6eb 100644 (file)
--- a/src/util/model.cpp
+++ b/src/util/model.cpp
@@ -1,7 +1,7 @@
 /*********************                                                        */
 /*! \file model.cpp
  ** \verbatim
- ** Original author: Clark Barrett
+ ** Original author: Andrew Reynolds
  ** Major contributors: Morgan Deters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.

diff --git a/src/util/model.h b/src/util/model.h
index 2224f74db8d685b7b332dfa05dffce07087533fc..1d80b0308ad8307c9f37d5fbcb2ebd1f7f994bc0 100644 (file)
--- a/src/util/model.h
+++ b/src/util/model.h
@@ -1,8 +1,8 @@
 /*********************                                                        */
 /*! \file model.h
  ** \verbatim
- ** Original author: Clark Barrett
- ** Major contributors: Andrew Reynolds, Morgan Deters
+ ** Original author: Morgan Deters
+ ** Major contributors: Andrew Reynolds
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa

diff --git a/src/util/nary_builder.cpp b/src/util/nary_builder.cpp
index 004dd3382547f5defea588f86440b2a6c6ade494..08aceef6f2f34d1426302d955a5fbdcdf69ba1ad 100644 (file)
--- a/src/util/nary_builder.cpp
+++ b/src/util/nary_builder.cpp
@@ -1,3 +1,20 @@
+/*********************                                                        */
+/*! \file nary_builder.cpp
+ ** \verbatim
+ ** Original author: Tim King
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** 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 "util/nary_builder.h"
 #include "expr/metakind.h"

diff --git a/src/util/nary_builder.h b/src/util/nary_builder.h
index ceaa44e777850ccd54a2d60ee1e2c0403b8c26b8..7676cadbc59d735f7221b1af0292abce927ad7a4 100644 (file)
--- a/src/util/nary_builder.h
+++ b/src/util/nary_builder.h
@@ -1,3 +1,20 @@
+/*********************                                                        */
+/*! \file nary_builder.h
+ ** \verbatim
+ ** Original author: Tim King
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** 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/regexp.h b/src/util/regexp.h
index bcd569df06073e58313267bfad39a2b4f322cfff..3a8fc717071985be3990c07497478af2073cdfac 100644 (file)
--- a/src/util/regexp.h
+++ b/src/util/regexp.h
@@ -3,8 +3,8 @@
  ** \verbatim
  ** Original author: Tianyi Liang
  ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
+ ** Minor contributors (to current version): Morgan Deters
+ ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim

diff --git a/test/unit/context/cdvector_black.h b/test/unit/context/cdvector_black.h
index 54fdd277e698c9e221b7c74391a9c9640ecbe656..87cb19121f5fb5eaee21dbc4236feb570afd7f49 100644 (file)
--- a/test/unit/context/cdvector_black.h
+++ b/test/unit/context/cdvector_black.h
@@ -2,8 +2,8 @@
 /*! \file cdvector_black.h
  ** \verbatim
  ** Original author: Tim King
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
+ ** Major contributors: none
+ ** Minor contributors (to current version): Morgan Deters
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/test/unit/expr/attribute_white.h b/test/unit/expr/attribute_white.h
index f5d1af5cda6705e7dd6e1feedc2c6d29bc583e07..7fa9972a6893b60f3bd05cced6a2b5846a1fb72e 100644 (file)
--- a/test/unit/expr/attribute_white.h
+++ b/test/unit/expr/attribute_white.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Morgan Deters
  ** Major contributors: none
- ** Minor contributors (to current version): Christopher L. Conway, Dejan Jovanovic
+ ** Minor contributors (to current version): Dejan Jovanovic, Christopher L. Conway
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/test/unit/expr/expr_manager_public.h b/test/unit/expr/expr_manager_public.h
index 204f1bcd221c8036e0d88af7e5b388c3d710ec0b..f7c7f403add61a169e441e112ede38b2ff213ef5 100644 (file)
--- a/test/unit/expr/expr_manager_public.h
+++ b/test/unit/expr/expr_manager_public.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Christopher L. Conway
  ** Major contributors: none
- ** Minor contributors (to current version): Morgan Deters
+ ** Minor contributors (to current version): Tim King, Morgan Deters
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/test/unit/theory/logic_info_white.h b/test/unit/theory/logic_info_white.h
index 8f94179663550523e4a827bf74f7d89ba91e1973..5f6a93ae7d95878898fb95f3db5c7b040bbec5c6 100644 (file)
--- a/test/unit/theory/logic_info_white.h
+++ b/test/unit/theory/logic_info_white.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Morgan Deters
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Tianyi Liang
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h
index 8ea9f42a7fc9e14c645a8e5b4c82fad0c8fade91..8aa84e58d79d73ca72f9e82192567cbbe47e34f5 100644 (file)
--- a/test/unit/theory/theory_black.h
+++ b/test/unit/theory/theory_black.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Tim King
  ** Major contributors: Clark Barrett
- ** Minor contributors (to current version): Morgan Deters
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h
index 4035b85daa75eefa3395c40c639edd48f98967ed..99dc17594bc00c72a783b3a560c36b6c76c291b9 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: Morgan Deters
  ** Major contributors: Dejan Jovanovic
- ** Minor contributors (to current version): Tim King, Andrew Reynolds, Christopher L. Conway
+ ** Minor contributors (to current version): Andrew Reynolds, Christopher L. Conway, Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing

diff --git a/test/unit/theory/theory_white.h b/test/unit/theory/theory_white.h
index d9df2912b4c4ea1869e80bbd4767422a08ed20a8..a824a3f68eec470dcccd9195f3daa87a6edd6572 100644 (file)
--- a/test/unit/theory/theory_white.h
+++ b/test/unit/theory/theory_white.h
@@ -2,8 +2,8 @@
 /*! \file theory_white.h
  ** \verbatim
  ** Original author: Morgan Deters
- ** Major contributors: Clark Barrett, Tim King
- ** Minor contributors (to current version): Dejan Jovanovic
+ ** Major contributors: Tim King
+ ** Minor contributors (to current version): Dejan Jovanovic, Clark Barrett
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing