diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-12-05 15:04:30 -0500 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-12-05 15:41:28 -0500 |
| commit | d692211d62a5d5a58c4bbe11b495554671c43847 (patch) | |
| tree | 5097a72499b72d54630d7dc7f890831eb1996b00 | |
| parent | 2fab0a67761f8b63a3c3f5abdbe7f382f722a04f (diff) | |
Update copyrights, add missing file-level documentation; fix perms.
195 files changed, 579 insertions, 344 deletions
diff --git a/examples/hashsmt/sha1.hpp b/examples/hashsmt/sha1.hpp index dc7146ef5..0d4bbbf33 100644 --- 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 29f8e61ad..1bdd380c1 100644 --- 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 55caa47d3..f8c03f7b2 100644 --- 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 2a8c177e7..c3985ebf4 100644 --- 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 6ad621b16..9154232d8 100644 --- 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 13feb4135..a19b83c6c 100644 --- 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 2b552684a..27d1249a1 100644 --- 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 6792cca9d..52e1d52bb 100644 --- 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 f28b13774..cda696a03 100644 --- 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 20743cba1..3c5d98340 100644 --- 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 44a623970..f538ba947 100644 --- 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 056e68c69..86768500b 100644 --- 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 1e3f25461..d203b75ad 100644 --- 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 fa6459481..0a3d389e7 100644 --- 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 79c6bfd8f..08b31a4c0 100644 --- 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 d3e4b8553..0b664ceb4 100644 --- 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 085a3a0c8..e1578efa7 100644 --- 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 a330aa4a9..ea9a598c0 100644 --- 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 39bbfbc2e..c88fd187d 100644 --- 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 0a4b853aa..1c13c4674 100644 --- 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 9c76a41f3..22c47da59 100644 --- 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 af771bd89..caf8f5ad4 100644 --- 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 31751b381..beff1f8a9 100644 --- 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 d34a7c7d6..491b44347 100644 --- 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 295842160..87361e991 100644 --- 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 ae951dbf2..1dd0ffed1 100644 --- 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 9ee896107..467b150d3 100644 --- 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 6fe28711b..7723dcb33 100644 --- 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 b88b09e8b..59fe5a2d4 100644 --- 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 5d9b6c7ae..d65a68310 100644 --- 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 c9bbd3860..19be199fd 100644 --- 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 657384e99..e2e52b158 100644 --- 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 884502cf2..b1621e9e5 100644 --- 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 cc46efe07..837adb15c 100644 --- 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 61e0999e9..d1e6f3a89 100644 --- 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 edffaa01f..6546fd8f3 100644 --- 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 e180d1524..0981af42f 100644 --- 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 bfaeb07c9..b41fcdd88 100644 --- 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 786238492..bd2626ddd 100644 --- 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 263ca50d7..39d065065 100644 --- 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 e4bc7ce09..a7ae8c447 100644 --- 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 cac5eb266..b743ba70e 100644 --- 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 a550f274a..9a2dbe655 100644 --- 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 82a1bd6be..e33f1a63f 100644 --- 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 e7e8f65b6..a4178f518 100644 --- 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 b8963c500..457023a59 100644 --- 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 8a11f2b96..6cda02c00 100644 --- 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 8fee0d11e..2674c82b1 100644 --- 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 7b0aa2058..f84aecbac 100644 --- 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 a66e02778..5a14924ff 100644 --- 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 574ef720f..51ad7b6ca 100644 --- 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 a2a95d6ca..d5131e6f6 100644 --- 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 0f5a0fd4e..1b3099842 100644 --- 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 a34c8981d..b32fdef2d 100644 --- 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 62b5fdff1..8a1d2b557 100644 --- 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 705c3e2f3..78313b81b 100644 --- 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 247c09294..f72537965 100644 --- 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 bf5261439..8f6f75295 100644 --- 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 6b297f2ab..11626c1de 100644 --- 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 ce05383da..d035dde2b 100644 --- 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 f0cecc24b..01137a33c 100644 --- 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 5bcdc6aab..6e2d86f8a 100644 --- 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 49c1a94ce..d3793432d 100644 --- 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 1e827d316..d4a445b70 100644 --- 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 718799e9f..fd9369bf1 100644 --- 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 e3e9055a7..a828b9e7f 100644 --- 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 a9304ae76..b5acb9149 100644 --- 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 0ec4bc238..9d2152800 100644 --- 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 e99e62505..c0bffdf07 100644 --- 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 51514bcfb..2397ccdba 100644 --- 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 899a3a7c6..a72ced0bc 100644 --- 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 deafb559a..c497adb75 100644 --- 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 d646ca889..b61cadaf8 100644 --- 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 cc3b6a460..ba19d01b1 100644 --- 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 64aa193dd..5a313e305 100644 --- 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 c0ee7ad20..2eb258d3b 100644 --- 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 de565df64..cee6cf81d 100644 --- 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 9d06fadc4..22fbf8713 100644 --- 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 deed7e7be..3e4cb819b 100644 --- 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 7c44f6791..bc0aa4dcd 100644 --- 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 d6b820300..66b091fab 100644 --- 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 6c7f622ec..395d51d3e 100644 --- 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 451f1e8ff..2408094d8 100644 --- 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 aa2b2a557..002d503d0 100644 --- 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 86de3c1a9..710610346 100644 --- 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 0dc7cdd5b..62980d83d 100644 --- 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 0d3a578a6..70f55c476 100644 --- 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 6070004d2..b84b59d14 100644 --- 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 b54ece638..689d2745b 100644 --- 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 a809ad0e8..a0179c117 100644 --- 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 00f183eb5..ef415139d 100644 --- 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 ac9469980..ccf7deecf 100644 --- 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 60199c09a..d02c9ace1 100644 --- 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 19c6a9248..4a0b45d62 100644 --- 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 1712509b5..cbe550f96 100644 --- 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 6fab0369c..2dc82bddc 100644 --- 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 ccdfc1583..feb061ee1 100644 --- 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 200c49195..9a898ebe6 100644 --- 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 0b0551283..5a46f7a0f 100644 --- 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 5a0c17134..e4b1a346d 100644 --- 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 f1204dbdf..b1c1b3b66 100644 --- 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 6d11364d9..2433dc1ee 100644 --- 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 b886bbdd5..e1a73d404 100644 --- 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 0eac4c035..222ba3039 100644 --- 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 6e0139e09..f142ff7be 100644 --- 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 7bec805ef..d137d09a0 100644 --- 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 186f2b317..b34923728 100644 --- 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 e8e4ff84b..56e0a479e 100644 --- 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 fefbad756..15c0b9c0b 100644 --- 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 ce44b312d..14a19f2d0 100644 --- 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 708206d28..90093edfd 100644 --- 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 9f3d12415..db774ebe3 100644 --- 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 b513dbf90..6c0ba90d4 100644 --- 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 76eb97b39..0b09bce4d 100644 --- 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 b51c56b18..12e258177 100644 --- 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 ab6a615a2..5140bd498 100644 --- 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 cec1dccfc..ffd34d777 100644 --- 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 79f58feb1..fa934ecc7 100644 --- 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 1e725932b..717122195 100644 --- 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 8ce0e93b2..d0328e600 100644 --- 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 697c70c02..692084071 100644 --- 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 0501bc6bf..205102b0f 100644 --- 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 75f4834ea..71cd44314 100644 --- 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 64407684b..22e05c469 100644 --- 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 e5100fc71..987973bf3 100644 --- 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 c629ad2b0..4597d4c6a 100644 --- 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 facd5f4f0..1b4e096f2 100644 --- 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 73f0386d2..d9e6120aa 100644 --- 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 080550a16..28485a979 100644 --- 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 3da938d31..972bdb2ec 100644 --- 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 42b49cf01..783f6284d 100644 --- 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 402a29848..a87c24596 100644 --- 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 fa4961352..bda124e96 100644 --- 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 ebfb55f08..a696af3c2 100644 --- 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 5f217050c..6bc5c21c1 100644 --- 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 c22d903f9..2f32ec5e6 100644 --- 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 abe05d3c7..606392831 100644 --- 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 4fe4072a3..6cc446e35 100644 --- 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 821beeae0..c70c90b29 100644 --- 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 index b079ae75c..b079ae75c 100755..100644 --- a/src/theory/quantifiers/relevant_domain.cpp +++ b/src/theory/quantifiers/relevant_domain.cpp diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h index c4345f828..c4345f828 100755..100644 --- a/src/theory/quantifiers/relevant_domain.h +++ b/src/theory/quantifiers/relevant_domain.h diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp index 107a99014..441ab029c 100755..100644 --- 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 index 2d9d751c2..a9a2f9b46 100755..100644 --- 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 index 507a50838..66a3ac79f 100755..100644 --- 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 index 7f6855fea..d7d9e0f6f 100755..100644 --- 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 066282c2c..e72242fe9 100644 --- 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 index e9a69bd30..e9a69bd30 100755..100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index f9add4fac..f12184869 100644 --- 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 24f09e62d..f88de72f9 100644 --- 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 17aed4e42..aa2964e13 100644 --- 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 f49471407..511ef3515 100644 --- 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 f26037cf0..e7079081b 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -1,14 +1,14 @@ -/********************* */
-/*! \file regexp_operation.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
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
+/********************* */ +/*! \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
**
** Regular Expresion Operations
diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h index 702e5ba84..a47f7bd77 100644 --- a/src/theory/strings/regexp_operation.h +++ b/src/theory/strings/regexp_operation.h @@ -1,14 +1,14 @@ -/********************* */
-/*! \file regexp_operation.h
- ** \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
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
+/********************* */ +/*! \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
**
** Regular Expresion Operations
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 9a88883fc..9f4d84765 100644 --- 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 9fae67a9f..4d2a192cf 100644 --- 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 c54cbb3b2..9da0e343d 100644 --- 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 7bc60c1a1..698ef6ba1 100644 --- 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 73f17a146..cd9db85c7 100644 --- 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 78f0da59e..318176297 100644 --- 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 080d6abf5..d5019ab39 100644 --- 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 af4dea293..7cf4d7ad9 100644 --- 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 e5b2ad8d2..ffc36e59b 100644 --- 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 73ff068b4..4f753187f 100644 --- 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 9da9cb5e2..598db2683 100644 --- 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 d77bf1eb0..691c1147b 100644 --- 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 199581b98..cb44b42df 100644 --- 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 a9294dc69..ab106bc8d 100644 --- 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 bf41a256d..409b41e3f 100644 --- 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 40713fa41..3bd316c93 100644 --- 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 50a746205..b4d1b6d48 100644 --- 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 8bbdded3e..a6e885f97 100644 --- 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 0ee754256..d41c7db5d 100644 --- 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 04e23217b..e826a6704 100644 --- 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 f03c5e959..0d22325e7 100644 --- 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 7e543c54e..be49e3dcf 100644 --- 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 3b3115887..e33c5fa36 100644 --- 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 8f8b63668..10ca9f72f 100644 --- 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 f2cd0004f..b5654e9cb 100644 --- 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 34ca8be5b..0cdc96fcb 100644 --- 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 356dbdd8f..be3e2918b 100644 --- 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 5231e05c2..0dfea4399 100644 --- 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 9d79687f4..c2464636e 100644 --- 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 795eac759..e90953e0b 100644 --- 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 1d14a7c4f..e25065c21 100644 --- 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 2224f74db..1d80b0308 100644 --- 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 004dd3382..08aceef6f 100644 --- 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 ceaa44e77..7676cadbc 100644 --- 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 bcd569df0..3a8fc7170 100644 --- 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 54fdd277e..87cb19121 100644 --- 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 f5d1af5cd..7fa9972a6 100644 --- 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 204f1bcd2..f7c7f403a 100644 --- 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 8f9417966..5f6a93ae7 100644 --- 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 8ea9f42a7..8aa84e58d 100644 --- 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 4035b85da..99dc17594 100644 --- 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 d9df2912b..a824a3f68 100644 --- 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 |