diff options
296 files changed, 374 insertions, 345 deletions
diff --git a/examples/api/combination.cpp b/examples/api/combination.cpp index 0ac33c6dc..f4dc72e56 100644 --- a/examples/api/combination.cpp +++ b/examples/api/combination.cpp @@ -2,7 +2,7 @@ /*! \file combination.cpp ** \verbatim ** Top contributors (to current version): - ** Aina Niemetz, Tim King, Andrew Reynolds + ** Aina Niemetz, Tim King, Mudathir Mohamed ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/examples/api/linear_arith.cpp b/examples/api/linear_arith.cpp index 2e70460af..77c1e196f 100644 --- a/examples/api/linear_arith.cpp +++ b/examples/api/linear_arith.cpp @@ -2,7 +2,7 @@ /*! \file linear_arith.cpp ** \verbatim ** Top contributors (to current version): - ** Aina Niemetz, Tim King + ** Aina Niemetz, Tim King, Mudathir Mohamed ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/examples/api/python/combination.py b/examples/api/python/combination.py index f063d8c4e..7733437a1 100644 --- a/examples/api/python/combination.py +++ b/examples/api/python/combination.py @@ -2,7 +2,7 @@ ##################### ## combination.py ## Top contributors (to current version): -## Makai Mann, Aina Niemetz, Andrew Reynolds +## Makai Mann, Mudathir Mohamed, Aina Niemetz ## This file is part of the CVC4 project. ## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ## in the top-level source directory and their institutional affiliations. diff --git a/examples/api/python/linear_arith.py b/examples/api/python/linear_arith.py index 94ce730a3..f539d1e05 100644 --- a/examples/api/python/linear_arith.py +++ b/examples/api/python/linear_arith.py @@ -2,7 +2,7 @@ ##################### ## linear_arith.py ## Top contributors (to current version): -## Makai Mann, Aina Niemetz +## Makai Mann, Mudathir Mohamed, Aina Niemetz ## This file is part of the CVC4 project. ## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ## in the top-level source directory and their institutional affiliations. diff --git a/examples/api/python/sequences.py b/examples/api/python/sequences.py index 7ed5448cd..9e3e45dc2 100644 --- a/examples/api/python/sequences.py +++ b/examples/api/python/sequences.py @@ -2,7 +2,7 @@ ##################### ## sequences.py ## Top contributors (to current version): -## Andres Noetzli, Makai Mann +## Andres Noetzli, Makai Mann, Mudathir Mohamed ## This file is part of the CVC4 project. ## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ## in the top-level source directory and their institutional affiliations. diff --git a/examples/api/python/sets.py b/examples/api/python/sets.py index e4350ea1b..5d2f842f5 100644 --- a/examples/api/python/sets.py +++ b/examples/api/python/sets.py @@ -2,7 +2,7 @@ ##################### ## sets.py ## Top contributors (to current version): -## Makai Mann, Aina Niemetz +## Makai Mann, Mudathir Mohamed, Aina Niemetz ## This file is part of the CVC4 project. ## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ## in the top-level source directory and their institutional affiliations. diff --git a/examples/api/python/strings.py b/examples/api/python/strings.py index 1e85c56bb..518a7b993 100644 --- a/examples/api/python/strings.py +++ b/examples/api/python/strings.py @@ -2,7 +2,7 @@ ##################### ## strings.py ## Top contributors (to current version): -## Makai Mann, Andres Noetzli +## Makai Mann, Mudathir Mohamed, Andres Noetzli ## This file is part of the CVC4 project. ## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ## in the top-level source directory and their institutional affiliations. diff --git a/examples/api/python/sygus-fun.py b/examples/api/python/sygus-fun.py index a85902961..9fb7f4648 100644 --- a/examples/api/python/sygus-fun.py +++ b/examples/api/python/sygus-fun.py @@ -2,7 +2,7 @@ ##################### ## sygus-fun.py ## Top contributors (to current version): -## Yoni Zohar, Andres Noetzli +## Yoni Zohar, Andres Noetzli, Mudathir Mohamed ## Copyright (c) 2009-2018 by the authors listed in the file AUTHkinds.OrS ## This file is part of the CVC4 project. ## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS diff --git a/examples/api/python/sygus-grammar.py b/examples/api/python/sygus-grammar.py index cfa342f35..1410e6739 100644 --- a/examples/api/python/sygus-grammar.py +++ b/examples/api/python/sygus-grammar.py @@ -2,7 +2,7 @@ ##################### ## sygus-grammar.py ## Top contributors (to current version): -## Yoni Zohar +## Yoni Zohar, Mudathir Mohamed ## This file is part of the CVC4 project. ## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ## in the top-level source directory and their institutional affiliations. diff --git a/examples/api/python/sygus-inv.py b/examples/api/python/sygus-inv.py index 4e7465382..ac28f8f1b 100644 --- a/examples/api/python/sygus-inv.py +++ b/examples/api/python/sygus-inv.py @@ -2,7 +2,7 @@ ##################### ## sygus-inv.py ## Top contributors (to current version): -## Yoni Zohar +## Yoni Zohar, Mudathir Mohamed ## This file is part of the CVC4 project. ## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ## in the top-level source directory and their institutional affiliations. diff --git a/examples/api/sets.cpp b/examples/api/sets.cpp index f8053a756..6033fb94e 100644 --- a/examples/api/sets.cpp +++ b/examples/api/sets.cpp @@ -2,7 +2,7 @@ /*! \file sets.cpp ** \verbatim ** Top contributors (to current version): - ** Aina Niemetz, Kshitij Bansal + ** Aina Niemetz, Kshitij Bansal, Mudathir Mohamed ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/examples/api/strings.cpp b/examples/api/strings.cpp index 556c49c8e..c95600c30 100644 --- a/examples/api/strings.cpp +++ b/examples/api/strings.cpp @@ -2,7 +2,7 @@ /*! \file strings.cpp ** \verbatim ** Top contributors (to current version): - ** Aina Niemetz, Tianyi Liang, Andres Noetzli + ** Aina Niemetz, Tianyi Liang, Mudathir Mohamed ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/examples/api/sygus-fun.cpp b/examples/api/sygus-fun.cpp index b2d6e9215..a5b421fae 100644 --- a/examples/api/sygus-fun.cpp +++ b/examples/api/sygus-fun.cpp @@ -2,7 +2,7 @@ /*! \file sygus-fun.cpp ** \verbatim ** Top contributors (to current version): - ** Abdalrhman Mohamed + ** Abdalrhman Mohamed, Mudathir Mohamed ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/examples/api/sygus-grammar.cpp b/examples/api/sygus-grammar.cpp index ea8256c70..e5481676a 100644 --- a/examples/api/sygus-grammar.cpp +++ b/examples/api/sygus-grammar.cpp @@ -2,7 +2,7 @@ /*! \file sygus-grammar.cpp ** \verbatim ** Top contributors (to current version): - ** Abdalrhman Mohamed + ** Abdalrhman Mohamed, Mudathir Mohamed ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/examples/api/sygus-inv.cpp b/examples/api/sygus-inv.cpp index d57d9be4e..f903b0242 100644 --- a/examples/api/sygus-inv.cpp +++ b/examples/api/sygus-inv.cpp @@ -2,7 +2,7 @@ /*! \file sygus-inv.cpp ** \verbatim ** Top contributors (to current version): - ** Abdalrhman Mohamed + ** Abdalrhman Mohamed, Mudathir Mohamed ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/examples/simple_vc_cxx.cpp b/examples/simple_vc_cxx.cpp index e648b9994..94bbee564 100644 --- a/examples/simple_vc_cxx.cpp +++ b/examples/simple_vc_cxx.cpp @@ -2,7 +2,7 @@ /*! \file simple_vc_cxx.cpp ** \verbatim ** Top contributors (to current version): - ** Andres Noetzli, Morgan Deters + ** Andres Noetzli, Morgan Deters, Mudathir Mohamed ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/examples/simple_vc_quant_cxx.cpp b/examples/simple_vc_quant_cxx.cpp index 538cb359f..b2dd0d3e6 100644 --- a/examples/simple_vc_quant_cxx.cpp +++ b/examples/simple_vc_quant_cxx.cpp @@ -2,7 +2,7 @@ /*! \file simple_vc_quant_cxx.cpp ** \verbatim ** Top contributors (to current version): - ** Andres Noetzli, Andrew Reynolds + ** Andres Noetzli, Andrew Reynolds, Mudathir Mohamed ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index 391db4bd4..f0825f180 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -1,7 +1,7 @@ ##################### ## CMakeLists.txt ## Top contributors (to current version): -## Mathias Preiner, Aina Niemetz, Andrew Reynolds +## Mathias Preiner, Andrew Reynolds, Aina Niemetz ## This file is part of the CVC4 project. ## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ## in the top-level source directory and their institutional affiliations. diff --git a/src/expr/ascription_type.cpp b/src/expr/ascription_type.cpp index d9466fdbf..cc5fc8557 100644 --- a/src/expr/ascription_type.cpp +++ b/src/expr/ascription_type.cpp @@ -2,7 +2,7 @@ /*! \file ascription_type.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Tim King, Mathias Preiner + ** Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/expr/ascription_type.h b/src/expr/ascription_type.h index 800f46e0a..13715a6d7 100644 --- a/src/expr/ascription_type.h +++ b/src/expr/ascription_type.h @@ -2,7 +2,7 @@ /*! \file ascription_type.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Tim King, Mathias Preiner + ** Morgan Deters, Andrew Reynolds, Mathias Preiner ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/expr/buffered_proof_generator.cpp b/src/expr/buffered_proof_generator.cpp index aa0fe19bd..f6753a601 100644 --- a/src/expr/buffered_proof_generator.cpp +++ b/src/expr/buffered_proof_generator.cpp @@ -5,7 +5,7 @@ ** Andrew Reynolds, Haniel Barbosa ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/src/expr/buffered_proof_generator.h b/src/expr/buffered_proof_generator.h index 987bd2465..f774e383d 100644 --- a/src/expr/buffered_proof_generator.h +++ b/src/expr/buffered_proof_generator.h @@ -2,10 +2,10 @@ /*! \file buffered_proof_generator.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Haniel Barbosa + ** Haniel Barbosa, Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/src/expr/emptybag.cpp b/src/expr/emptybag.cpp index 888b3b92a..8e59a8eb1 100644 --- a/src/expr/emptybag.cpp +++ b/src/expr/emptybag.cpp @@ -5,9 +5,11 @@ ** Mudathir Mohamed ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim + ** + ** \brief A class for empty bags **/ #include "expr/emptybag.h" diff --git a/src/expr/emptybag.h b/src/expr/emptybag.h index a16c12d86..8a9776f42 100644 --- a/src/expr/emptybag.h +++ b/src/expr/emptybag.h @@ -5,11 +5,11 @@ ** Mudathir Mohamed ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief a class for empty bags + ** \brief A class for empty bags **/ #include "cvc4_public.h" diff --git a/src/expr/expr_iomanip.cpp b/src/expr/expr_iomanip.cpp index 0ff29663c..0395a9b07 100644 --- a/src/expr/expr_iomanip.cpp +++ b/src/expr/expr_iomanip.cpp @@ -2,7 +2,7 @@ /*! \file expr_iomanip.cpp ** \verbatim ** Top contributors (to current version): - ** Tim King, Morgan Deters, Kshitij Bansal + ** Morgan Deters, Tim King, Kshitij Bansal ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/expr/lazy_proof_chain.cpp b/src/expr/lazy_proof_chain.cpp index 5c096767b..a98ba7453 100644 --- a/src/expr/lazy_proof_chain.cpp +++ b/src/expr/lazy_proof_chain.cpp @@ -2,10 +2,10 @@ /*! \file lazy_proof_chain.cpp ** \verbatim ** Top contributors (to current version): - ** Haniel Barbosa + ** Haniel Barbosa, Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/src/expr/lazy_proof_chain.h b/src/expr/lazy_proof_chain.h index 28de3cea0..59cab72c9 100644 --- a/src/expr/lazy_proof_chain.h +++ b/src/expr/lazy_proof_chain.h @@ -2,10 +2,10 @@ /*! \file lazy_proof_chain.h ** \verbatim ** Top contributors (to current version): - ** Haniel Barbosa + ** Haniel Barbosa, Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index fde92c4e1..49f460f45 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -2,7 +2,7 @@ /*! \file node_manager.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Andrew Reynolds, Tim King + ** Andrew Reynolds, Morgan Deters, Tim King ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index bbb076fbc..1dd495ba2 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -2,7 +2,7 @@ /*! \file node_manager.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Christopher L. Conway, Andrew Reynolds + ** Morgan Deters, Andrew Reynolds, Christopher L. Conway ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp index 8ceb5476a..9964d7aec 100644 --- a/src/expr/node_value.cpp +++ b/src/expr/node_value.cpp @@ -2,7 +2,7 @@ /*! \file node_value.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Aina Niemetz, Tim King + ** Morgan Deters, Aina Niemetz, Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/expr/proof_node.h b/src/expr/proof_node.h index 6d7db7b25..0c36deada 100644 --- a/src/expr/proof_node.h +++ b/src/expr/proof_node.h @@ -2,7 +2,7 @@ /*! \file proof_node.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Haniel Barbosa ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/expr/proof_node_algorithm.cpp b/src/expr/proof_node_algorithm.cpp index b21bdec23..c3e0aa5b0 100644 --- a/src/expr/proof_node_algorithm.cpp +++ b/src/expr/proof_node_algorithm.cpp @@ -2,7 +2,7 @@ /*! \file proof_node_algorithm.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Haniel Barbosa ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/expr/proof_node_algorithm.h b/src/expr/proof_node_algorithm.h index d6bd1963c..43d06ea91 100644 --- a/src/expr/proof_node_algorithm.h +++ b/src/expr/proof_node_algorithm.h @@ -2,7 +2,7 @@ /*! \file proof_node_algorithm.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Haniel Barbosa ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/expr/proof_node_manager.cpp b/src/expr/proof_node_manager.cpp index 4682bbebb..cacd2c101 100644 --- a/src/expr/proof_node_manager.cpp +++ b/src/expr/proof_node_manager.cpp @@ -2,7 +2,7 @@ /*! \file proof_node_manager.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Haniel Barbosa ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/expr/proof_node_manager.h b/src/expr/proof_node_manager.h index dae0266bb..3ad56c92d 100644 --- a/src/expr/proof_node_manager.h +++ b/src/expr/proof_node_manager.h @@ -2,7 +2,7 @@ /*! \file proof_node_manager.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Haniel Barbosa ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/expr/proof_node_updater.cpp b/src/expr/proof_node_updater.cpp index ac04baa6f..834f4381f 100644 --- a/src/expr/proof_node_updater.cpp +++ b/src/expr/proof_node_updater.cpp @@ -2,7 +2,7 @@ /*! \file proof_node_updater.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Haniel Barbosa ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/expr/proof_node_updater.h b/src/expr/proof_node_updater.h index d4c2e8756..82c2ee068 100644 --- a/src/expr/proof_node_updater.h +++ b/src/expr/proof_node_updater.h @@ -2,7 +2,7 @@ /*! \file proof_node_updater.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Haniel Barbosa ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/expr/proof_set.h b/src/expr/proof_set.h index 20ef67efe..9c6c21ec4 100644 --- a/src/expr/proof_set.h +++ b/src/expr/proof_set.h @@ -2,7 +2,7 @@ /*! \file proof_set.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Gereon Kremer, Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/expr/record.cpp b/src/expr/record.cpp index 08944912a..cddfd7a22 100644 --- a/src/expr/record.cpp +++ b/src/expr/record.cpp @@ -2,7 +2,7 @@ /*! \file record.cpp ** \verbatim ** Top contributors (to current version): - ** Tim King, Morgan Deters, Piotr Trojanek + ** Tim King ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/expr/record.h b/src/expr/record.h index a0d545a56..4e1ff6772 100644 --- a/src/expr/record.h +++ b/src/expr/record.h @@ -2,7 +2,7 @@ /*! \file record.h ** \verbatim ** Top contributors (to current version): - ** Tim King, Morgan Deters, Mathias Preiner + ** Morgan Deters, Tim King, Mathias Preiner ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/expr/symbol_table.h b/src/expr/symbol_table.h index d6a632ac5..0e30d6d73 100644 --- a/src/expr/symbol_table.h +++ b/src/expr/symbol_table.h @@ -2,7 +2,7 @@ /*! \file symbol_table.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Andrew Reynolds, Tim King + ** Andrew Reynolds, Morgan Deters, Christopher L. Conway ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/expr/tconv_seq_proof_generator.cpp b/src/expr/tconv_seq_proof_generator.cpp index b22170b38..8bd850488 100644 --- a/src/expr/tconv_seq_proof_generator.cpp +++ b/src/expr/tconv_seq_proof_generator.cpp @@ -1,5 +1,5 @@ /********************* */ -/*! \file tconv_seq_proof_generator.h +/*! \file tconv_seq_proof_generator.cpp ** \verbatim ** Top contributors (to current version): ** Andrew Reynolds diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index b1a7c70b5..af95ca20f 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -2,7 +2,7 @@ /*! \file command_executor.cpp ** \verbatim ** Top contributors (to current version): - ** Kshitij Bansal, Morgan Deters, Tim King + ** Kshitij Bansal, Andrew Reynolds, Morgan Deters ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/main/command_executor.h b/src/main/command_executor.h index 4023b86de..db2248454 100644 --- a/src/main/command_executor.h +++ b/src/main/command_executor.h @@ -2,7 +2,7 @@ /*! \file command_executor.h ** \verbatim ** Top contributors (to current version): - ** Aina Niemetz, Kshitij Bansal, Morgan Deters + ** Andrew Reynolds, Kshitij Bansal, Aina Niemetz ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/parser/antlr_tracing.h b/src/parser/antlr_tracing.h index b8a18aba8..7030e1177 100644 --- a/src/parser/antlr_tracing.h +++ b/src/parser/antlr_tracing.h @@ -2,7 +2,7 @@ /*! \file antlr_tracing.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Mathias Preiner + ** Morgan Deters, Mathias Preiner, Aina Niemetz ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp index 9adb46af1..b9d0cb415 100644 --- a/src/parser/parser_builder.cpp +++ b/src/parser/parser_builder.cpp @@ -2,7 +2,7 @@ /*! \file parser_builder.cpp ** \verbatim ** Top contributors (to current version): - ** Christopher L. Conway, Morgan Deters, Aina Niemetz + ** Christopher L. Conway, Morgan Deters, Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h index bf205b13a..c28a76879 100644 --- a/src/parser/parser_builder.h +++ b/src/parser/parser_builder.h @@ -2,7 +2,7 @@ /*! \file parser_builder.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Christopher L. Conway, Aina Niemetz + ** Morgan Deters, Christopher L. Conway, Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/preprocessing/assertion_pipeline.cpp b/src/preprocessing/assertion_pipeline.cpp index cd7aadf9a..3b304c8b9 100644 --- a/src/preprocessing/assertion_pipeline.cpp +++ b/src/preprocessing/assertion_pipeline.cpp @@ -2,7 +2,7 @@ /*! \file assertion_pipeline.cpp ** \verbatim ** Top contributors (to current version): - ** Andres Noetzli, Andrew Reynolds, Haniel Barbosa + ** Andrew Reynolds, Andres Noetzli, Haniel Barbosa ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/preprocessing/assertion_pipeline.h b/src/preprocessing/assertion_pipeline.h index 75f370450..fcfce0e87 100644 --- a/src/preprocessing/assertion_pipeline.h +++ b/src/preprocessing/assertion_pipeline.h @@ -2,7 +2,7 @@ /*! \file assertion_pipeline.h ** \verbatim ** Top contributors (to current version): - ** Andres Noetzli, Andrew Reynolds, Justin Xu + ** Andres Noetzli, Andrew Reynolds, Morgan Deters ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/preprocessing/passes/apply_substs.cpp b/src/preprocessing/passes/apply_substs.cpp index 06821ab56..92f31b0b8 100644 --- a/src/preprocessing/passes/apply_substs.cpp +++ b/src/preprocessing/passes/apply_substs.cpp @@ -2,7 +2,7 @@ /*! \file apply_substs.cpp ** \verbatim ** Top contributors (to current version): - ** Aina Niemetz, Andres Noetzli, Mathias Preiner + ** Aina Niemetz, Andrew Reynolds, Mathias Preiner ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/preprocessing/passes/bv_gauss.cpp b/src/preprocessing/passes/bv_gauss.cpp index eaba90561..02a08b133 100644 --- a/src/preprocessing/passes/bv_gauss.cpp +++ b/src/preprocessing/passes/bv_gauss.cpp @@ -2,7 +2,7 @@ /*! \file bv_gauss.cpp ** \verbatim ** Top contributors (to current version): - ** Aina Niemetz, Mathias Preiner, Andres Noetzli + ** Aina Niemetz, Mathias Preiner, Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp index dbe751415..7ffe1bc76 100644 --- a/src/preprocessing/passes/bv_to_int.cpp +++ b/src/preprocessing/passes/bv_to_int.cpp @@ -2,7 +2,7 @@ /*! \file bv_to_int.cpp ** \verbatim ** Top contributors (to current version): - ** Yoni Zohar, Ahmed Irfan, Andres Noetzli + ** Yoni Zohar, Andrew Reynolds, Andres Noetzli ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/preprocessing/passes/fun_def_fmf.cpp b/src/preprocessing/passes/fun_def_fmf.cpp index 6095be228..8c7a71021 100644 --- a/src/preprocessing/passes/fun_def_fmf.cpp +++ b/src/preprocessing/passes/fun_def_fmf.cpp @@ -2,7 +2,7 @@ /*! \file fun_def_fmf.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Haniel Barbosa, Mathias Preiner ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/preprocessing/passes/global_negate.h b/src/preprocessing/passes/global_negate.h index 208b8d990..af8ae5048 100644 --- a/src/preprocessing/passes/global_negate.h +++ b/src/preprocessing/passes/global_negate.h @@ -2,7 +2,7 @@ /*! \file global_negate.h ** \verbatim ** Top contributors (to current version): - ** Yoni Zohar, Mathias Preiner + ** Yoni Zohar, Mathias Preiner, Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/preprocessing/passes/ho_elim.cpp b/src/preprocessing/passes/ho_elim.cpp index 445cac18e..8cf4ad2ed 100644 --- a/src/preprocessing/passes/ho_elim.cpp +++ b/src/preprocessing/passes/ho_elim.cpp @@ -2,7 +2,7 @@ /*! \file ho_elim.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Andres Noetzli ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/preprocessing/passes/ho_elim.h b/src/preprocessing/passes/ho_elim.h index 2edc96074..a1dc05b83 100644 --- a/src/preprocessing/passes/ho_elim.h +++ b/src/preprocessing/passes/ho_elim.h @@ -2,7 +2,7 @@ /*! \file ho_elim.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Andres Noetzli ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/preprocessing/passes/ite_simp.cpp b/src/preprocessing/passes/ite_simp.cpp index 8c99493ba..5568dcad0 100644 --- a/src/preprocessing/passes/ite_simp.cpp +++ b/src/preprocessing/passes/ite_simp.cpp @@ -2,7 +2,7 @@ /*! \file ite_simp.cpp ** \verbatim ** Top contributors (to current version): - ** Aina Niemetz, Tim King, Mathias Preiner + ** Aina Niemetz, Tim King, Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp index f55665bc5..4ed2aede9 100644 --- a/src/preprocessing/passes/miplib_trick.cpp +++ b/src/preprocessing/passes/miplib_trick.cpp @@ -2,7 +2,7 @@ /*! \file miplib_trick.cpp ** \verbatim ** Top contributors (to current version): - ** Mathias Preiner, Tim King, Morgan Deters + ** Mathias Preiner, Andrew Reynolds, Morgan Deters ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp index cedee6d3c..7ace55c0a 100644 --- a/src/preprocessing/passes/non_clausal_simp.cpp +++ b/src/preprocessing/passes/non_clausal_simp.cpp @@ -2,7 +2,7 @@ /*! \file non_clausal_simp.cpp ** \verbatim ** Top contributors (to current version): - ** Aina Niemetz, Haniel Barbosa, Andrew Reynolds + ** Aina Niemetz, Andrew Reynolds, Haniel Barbosa ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/preprocessing/passes/non_clausal_simp.h b/src/preprocessing/passes/non_clausal_simp.h index d3a9e0b1a..f94eb2d70 100644 --- a/src/preprocessing/passes/non_clausal_simp.h +++ b/src/preprocessing/passes/non_clausal_simp.h @@ -2,7 +2,7 @@ /*! \file non_clausal_simp.h ** \verbatim ** Top contributors (to current version): - ** Aina Niemetz, Mathias Preiner + ** Andrew Reynolds, Aina Niemetz, Mathias Preiner ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/preprocessing/passes/theory_preprocess.cpp b/src/preprocessing/passes/theory_preprocess.cpp index bf9c3e9fe..e888e7a2b 100644 --- a/src/preprocessing/passes/theory_preprocess.cpp +++ b/src/preprocessing/passes/theory_preprocess.cpp @@ -2,7 +2,7 @@ /*! \file theory_preprocess.cpp ** \verbatim ** Top contributors (to current version): - ** Mathias Preiner + ** Mathias Preiner, Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/preprocessing/preprocessing_pass.cpp b/src/preprocessing/preprocessing_pass.cpp index 78b0022c6..169f10c9d 100644 --- a/src/preprocessing/preprocessing_pass.cpp +++ b/src/preprocessing/preprocessing_pass.cpp @@ -2,7 +2,7 @@ /*! \file preprocessing_pass.cpp ** \verbatim ** Top contributors (to current version): - ** Justin Xu, Andres Noetzli + ** Justin Xu, Abdalrhman Mohamed, Andres Noetzli ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp index 5893635cf..ff4a0e6ca 100644 --- a/src/preprocessing/preprocessing_pass_context.cpp +++ b/src/preprocessing/preprocessing_pass_context.cpp @@ -2,7 +2,7 @@ /*! \file preprocessing_pass_context.cpp ** \verbatim ** Top contributors (to current version): - ** Aina Niemetz, Mathias Preiner, Andrew Reynolds + ** Aina Niemetz, Andrew Reynolds, Mathias Preiner ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp index 30b09acae..ea0d1b267 100644 --- a/src/printer/ast/ast_printer.cpp +++ b/src/printer/ast/ast_printer.cpp @@ -2,7 +2,7 @@ /*! \file ast_printer.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Abdalrhman Mohamed, Tim King + ** Morgan Deters, Abdalrhman Mohamed, Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/printer/ast/ast_printer.h b/src/printer/ast/ast_printer.h index e0bc7b6bf..732933bb4 100644 --- a/src/printer/ast/ast_printer.h +++ b/src/printer/ast/ast_printer.h @@ -2,7 +2,7 @@ /*! \file ast_printer.h ** \verbatim ** Top contributors (to current version): - ** Abdalrhman Mohamed, Tim King, Morgan Deters + ** Abdalrhman Mohamed, Andrew Reynolds, Tim King ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index c681a223f..6c9009e58 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -2,7 +2,7 @@ /*! \file cvc_printer.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Dejan Jovanovic, Andrew Reynolds + ** Andrew Reynolds, Morgan Deters, Dejan Jovanovic ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/printer/cvc/cvc_printer.h b/src/printer/cvc/cvc_printer.h index 799bba8d2..58e47dbac 100644 --- a/src/printer/cvc/cvc_printer.h +++ b/src/printer/cvc/cvc_printer.h @@ -2,7 +2,7 @@ /*! \file cvc_printer.h ** \verbatim ** Top contributors (to current version): - ** Abdalrhman Mohamed, Tim King, Morgan Deters + ** Abdalrhman Mohamed, Andrew Reynolds, Tim King ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/printer/let_binding.cpp b/src/printer/let_binding.cpp index 2efc98318..afe926a2a 100644 --- a/src/printer/let_binding.cpp +++ b/src/printer/let_binding.cpp @@ -5,7 +5,7 @@ ** Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/src/printer/let_binding.h b/src/printer/let_binding.h index d81274c87..45a09d07f 100644 --- a/src/printer/let_binding.h +++ b/src/printer/let_binding.h @@ -5,7 +5,7 @@ ** Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index 7225721c0..9f8451ba8 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -2,7 +2,7 @@ /*! \file printer.cpp ** \verbatim ** Top contributors (to current version): - ** Abdalrhman Mohamed, Morgan Deters, Aina Niemetz + ** Abdalrhman Mohamed, Andrew Reynolds, Morgan Deters ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/printer/printer.h b/src/printer/printer.h index 5bcccedb8..068c79330 100644 --- a/src/printer/printer.h +++ b/src/printer/printer.h @@ -2,7 +2,7 @@ /*! \file printer.h ** \verbatim ** Top contributors (to current version): - ** Abdalrhman Mohamed, Tim King, Aina Niemetz + ** Abdalrhman Mohamed, Andrew Reynolds, Aina Niemetz ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h index 3d90cee06..287a81286 100644 --- a/src/printer/smt2/smt2_printer.h +++ b/src/printer/smt2/smt2_printer.h @@ -2,7 +2,7 @@ /*! \file smt2_printer.h ** \verbatim ** Top contributors (to current version): - ** Abdalrhman Mohamed, Tim King, Andrew Reynolds + ** Abdalrhman Mohamed, Andrew Reynolds, Tim King ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/printer/tptp/tptp_printer.cpp b/src/printer/tptp/tptp_printer.cpp index f9384b0cb..1c37c3edc 100644 --- a/src/printer/tptp/tptp_printer.cpp +++ b/src/printer/tptp/tptp_printer.cpp @@ -2,7 +2,7 @@ /*! \file tptp_printer.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Morgan Deters + ** Andrew Reynolds, Morgan Deters, Tim King ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/printer/tptp/tptp_printer.h b/src/printer/tptp/tptp_printer.h index 38a56bcb5..46c3184ff 100644 --- a/src/printer/tptp/tptp_printer.h +++ b/src/printer/tptp/tptp_printer.h @@ -2,7 +2,7 @@ /*! \file tptp_printer.h ** \verbatim ** Top contributors (to current version): - ** Tim King, Abdalrhman Mohamed, Morgan Deters + ** Andrew Reynolds, Tim King, Abdalrhman Mohamed ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h index 7276f6402..c7eb2282b 100644 --- a/src/proof/proof_manager.h +++ b/src/proof/proof_manager.h @@ -2,7 +2,7 @@ /*! \file proof_manager.h ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean, Guy Katz, Haniel Barbosa + ** Liana Hadarean, Haniel Barbosa, Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/proof/unsat_core.cpp b/src/proof/unsat_core.cpp index dd470b299..7b0b50605 100644 --- a/src/proof/unsat_core.cpp +++ b/src/proof/unsat_core.cpp @@ -2,7 +2,7 @@ /*! \file unsat_core.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Clark Barrett, Tim King + ** Morgan Deters, Andrew Reynolds, Clark Barrett ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/proof/unsat_core.h b/src/proof/unsat_core.h index fb3401876..3fdbcc4b5 100644 --- a/src/proof/unsat_core.h +++ b/src/proof/unsat_core.h @@ -2,7 +2,7 @@ /*! \file unsat_core.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Andrew Reynolds, Mathias Preiner + ** Andrew Reynolds, Morgan Deters, Mathias Preiner ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 7dcd3f910..e5b778365 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -2,7 +2,7 @@ /*! \file cnf_stream.cpp ** \verbatim ** Top contributors (to current version): - ** Dejan Jovanovic, Liana Hadarean, Tim King + ** Dejan Jovanovic, Haniel Barbosa, Liana Hadarean ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index 74ead0d22..e92532f08 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -2,7 +2,7 @@ /*! \file cnf_stream.h ** \verbatim ** Top contributors (to current version): - ** Dejan Jovanovic, Tim King, Morgan Deters + ** Dejan Jovanovic, Tim King, Haniel Barbosa ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/prop/proof_cnf_stream.cpp b/src/prop/proof_cnf_stream.cpp index 790e5aeb2..d98de2a8a 100644 --- a/src/prop/proof_cnf_stream.cpp +++ b/src/prop/proof_cnf_stream.cpp @@ -2,10 +2,10 @@ /*! \file proof_cnf_stream.cpp ** \verbatim ** Top contributors (to current version): - ** Haniel Barbosa + ** Haniel Barbosa, Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/src/prop/proof_cnf_stream.h b/src/prop/proof_cnf_stream.h index 80be07231..d05dd2f16 100644 --- a/src/prop/proof_cnf_stream.h +++ b/src/prop/proof_cnf_stream.h @@ -2,10 +2,10 @@ /*! \file proof_cnf_stream.h ** \verbatim ** Top contributors (to current version): - ** Haniel Barbosa + ** Haniel Barbosa, Dejan Jovanovic, Liana Hadarean ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/src/prop/prop_proof_manager.cpp b/src/prop/prop_proof_manager.cpp index aa58ffa2c..fc5f92434 100644 --- a/src/prop/prop_proof_manager.cpp +++ b/src/prop/prop_proof_manager.cpp @@ -1,5 +1,5 @@ /********************* */ -/*! \file prop_proof_manager +/*! \file prop_proof_manager.cpp ** \verbatim ** Top contributors (to current version): ** Haniel Barbosa diff --git a/src/prop/sat_proof_manager.cpp b/src/prop/sat_proof_manager.cpp index 36913fda8..985763c84 100644 --- a/src/prop/sat_proof_manager.cpp +++ b/src/prop/sat_proof_manager.cpp @@ -5,7 +5,7 @@ ** Haniel Barbosa ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/src/prop/sat_proof_manager.h b/src/prop/sat_proof_manager.h index da67f0c1e..79dc09549 100644 --- a/src/prop/sat_proof_manager.h +++ b/src/prop/sat_proof_manager.h @@ -5,7 +5,7 @@ ** Haniel Barbosa ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index 65da2fc7c..d0d593f8a 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -2,7 +2,7 @@ /*! \file theory_proxy.cpp ** \verbatim ** Top contributors (to current version): - ** Tim King, Kshitij Bansal, Dejan Jovanovic + ** Kshitij Bansal, Tim King, Dejan Jovanovic ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/smt/check_models.cpp b/src/smt/check_models.cpp index 56d54eec9..a41c750ec 100644 --- a/src/smt/check_models.cpp +++ b/src/smt/check_models.cpp @@ -2,7 +2,7 @@ /*! \file check_models.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Morgan Deters, Yoni Zohar ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 14b9ed0aa..d02c1631e 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -2,7 +2,7 @@ /*! \file command.cpp ** \verbatim ** Top contributors (to current version): - ** Tim King, Morgan Deters, Andrew Reynolds + ** Tim King, Abdalrhman Mohamed, Morgan Deters ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/smt/command.h b/src/smt/command.h index bfe5e737a..399050d94 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -2,7 +2,7 @@ /*! \file command.h ** \verbatim ** Top contributors (to current version): - ** Tim King, Morgan Deters, Abdalrhman Mohamed + ** Abdalrhman Mohamed, Tim King, Morgan Deters ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/smt/dump_manager.cpp b/src/smt/dump_manager.cpp index 51fcf8b5b..706c2e886 100644 --- a/src/smt/dump_manager.cpp +++ b/src/smt/dump_manager.cpp @@ -2,7 +2,7 @@ /*! \file dump_manager.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, Abdalrhman Mohamed + ** Andrew Reynolds, Gereon Kremer, Abdalrhman Mohamed ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/smt/dump_manager.h b/src/smt/dump_manager.h index eaedf39a1..3238d3a8d 100644 --- a/src/smt/dump_manager.h +++ b/src/smt/dump_manager.h @@ -2,7 +2,7 @@ /*! \file dump_manager.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, Abdalrhman Mohamed + ** Andrew Reynolds, Morgan Deters, Aina Niemetz ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/smt/expand_definitions.cpp b/src/smt/expand_definitions.cpp index b0460fcc5..4f49e1bbe 100644 --- a/src/smt/expand_definitions.cpp +++ b/src/smt/expand_definitions.cpp @@ -2,7 +2,7 @@ /*! \file expand_definitions.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Haniel Barbosa + ** Andrew Reynolds, Morgan Deters, Andres Noetzli ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/smt/expand_definitions.h b/src/smt/expand_definitions.h index 5b75ddadd..486aa0c3a 100644 --- a/src/smt/expand_definitions.h +++ b/src/smt/expand_definitions.h @@ -1,8 +1,8 @@ /********************* */ -/*! \file process_assertions.h +/*! \file expand_definitions.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Morgan Deters + ** Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/smt/interpolation_solver.cpp b/src/smt/interpolation_solver.cpp index c47d99951..09ddfde75 100644 --- a/src/smt/interpolation_solver.cpp +++ b/src/smt/interpolation_solver.cpp @@ -2,10 +2,10 @@ /*! \file interpolation_solver.cpp ** \verbatim ** Top contributors (to current version): - ** Ying Sheng + ** Ying Sheng, Andrew Reynolds, Abdalrhman Mohamed ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/src/smt/interpolation_solver.h b/src/smt/interpolation_solver.h index 096cf8983..c52614f74 100644 --- a/src/smt/interpolation_solver.h +++ b/src/smt/interpolation_solver.h @@ -2,10 +2,10 @@ /*! \file interpolation_solver.h ** \verbatim ** Top contributors (to current version): - ** Ying Sheng + ** Ying Sheng, Andrew Reynolds, Morgan Deters ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/src/smt/listeners.h b/src/smt/listeners.h index 150ee7ba8..ce174e872 100644 --- a/src/smt/listeners.h +++ b/src/smt/listeners.h @@ -2,7 +2,7 @@ /*! \file listeners.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Mathias Preiner + ** Andrew Reynolds, Abdalrhman Mohamed, Mathias Preiner ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/smt/managed_ostreams.cpp b/src/smt/managed_ostreams.cpp index 27a90cb56..6056dd3d9 100644 --- a/src/smt/managed_ostreams.cpp +++ b/src/smt/managed_ostreams.cpp @@ -2,7 +2,7 @@ /*! \file managed_ostreams.cpp ** \verbatim ** Top contributors (to current version): - ** Tim King + ** Tim King, Aina Niemetz ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/smt/model.cpp b/src/smt/model.cpp index ccf73dda0..557f9959f 100644 --- a/src/smt/model.cpp +++ b/src/smt/model.cpp @@ -2,7 +2,7 @@ /*! \file model.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Andrew Reynolds, Tim King + ** Andrew Reynolds, Morgan Deters, Tim King ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/smt/model_core_builder.cpp b/src/smt/model_core_builder.cpp index cb8494e85..c2d92d394 100644 --- a/src/smt/model_core_builder.cpp +++ b/src/smt/model_core_builder.cpp @@ -2,7 +2,7 @@ /*! \file model_core_builder.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Mathias Preiner, Haniel Barbosa + ** Andrew Reynolds, Mathias Preiner ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/smt/node_command.cpp b/src/smt/node_command.cpp index 815f99132..33b5d9953 100644 --- a/src/smt/node_command.cpp +++ b/src/smt/node_command.cpp @@ -2,7 +2,7 @@ /*! \file node_command.cpp ** \verbatim ** Top contributors (to current version): - ** Abdalrhman Mohamed + ** Abdalrhman Mohamed, Yoni Zohar, Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/smt/options_manager.cpp b/src/smt/options_manager.cpp index e028068ee..f449e79cb 100644 --- a/src/smt/options_manager.cpp +++ b/src/smt/options_manager.cpp @@ -2,7 +2,7 @@ /*! \file options_manager.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Aina Niemetz ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/smt/preprocess_proof_generator.cpp b/src/smt/preprocess_proof_generator.cpp index bab56a0d2..cb2887ec0 100644 --- a/src/smt/preprocess_proof_generator.cpp +++ b/src/smt/preprocess_proof_generator.cpp @@ -2,7 +2,7 @@ /*! \file preprocess_proof_generator.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Gereon Kremer ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/smt/preprocess_proof_generator.h b/src/smt/preprocess_proof_generator.h index 41add5583..01d9c89da 100644 --- a/src/smt/preprocess_proof_generator.h +++ b/src/smt/preprocess_proof_generator.h @@ -2,7 +2,7 @@ /*! \file preprocess_proof_generator.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Gereon Kremer ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp index 9f2c8f3e7..c2b8f73f1 100644 --- a/src/smt/preprocessor.cpp +++ b/src/smt/preprocessor.cpp @@ -2,7 +2,7 @@ /*! \file preprocessor.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, Aina Niemetz + ** Andrew Reynolds, Morgan Deters, Abdalrhman Mohamed ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp index c68b73336..fe3dbc62b 100644 --- a/src/smt/process_assertions.cpp +++ b/src/smt/process_assertions.cpp @@ -2,7 +2,7 @@ /*! \file process_assertions.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Haniel Barbosa + ** Andrew Reynolds, Yoni Zohar, Mathias Preiner ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp index 53608fa0a..049eb02c0 100644 --- a/src/smt/proof_post_processor.cpp +++ b/src/smt/proof_post_processor.cpp @@ -2,7 +2,7 @@ /*! \file proof_post_processor.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Haniel Barbosa ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/smt/proof_post_processor.h b/src/smt/proof_post_processor.h index 3c0d4fbaa..885608b38 100644 --- a/src/smt/proof_post_processor.h +++ b/src/smt/proof_post_processor.h @@ -2,7 +2,7 @@ /*! \file proof_post_processor.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Haniel Barbosa ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index aaff29479..7e6bed464 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -2,7 +2,7 @@ /*! \file set_defaults.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Andres Noetzli, Haniel Barbosa + ** Andrew Reynolds, Andres Noetzli, Gereon Kremer ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/smt/smt_engine_state.cpp b/src/smt/smt_engine_state.cpp index dada78d9a..e51d17c44 100644 --- a/src/smt/smt_engine_state.cpp +++ b/src/smt/smt_engine_state.cpp @@ -2,7 +2,7 @@ /*! \file smt_engine_state.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, Aina Niemetz + ** Andrew Reynolds, Morgan Deters, Ying Sheng ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/smt/smt_engine_state.h b/src/smt/smt_engine_state.h index f033be031..b085c26a3 100644 --- a/src/smt/smt_engine_state.h +++ b/src/smt/smt_engine_state.h @@ -2,7 +2,7 @@ /*! \file smt_engine_state.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Aina Niemetz, Morgan Deters + ** Andrew Reynolds, Ying Sheng, Aina Niemetz ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp index 0b40bf894..42dbcd43e 100644 --- a/src/smt/sygus_solver.cpp +++ b/src/smt/sygus_solver.cpp @@ -2,7 +2,7 @@ /*! \file sygus_solver.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Haniel Barbosa, Andres Noetzli + ** Andrew Reynolds, Haniel Barbosa, Abdalrhman Mohamed ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/smt/sygus_solver.h b/src/smt/sygus_solver.h index b523ff5b7..c9de7b7e9 100644 --- a/src/smt/sygus_solver.h +++ b/src/smt/sygus_solver.h @@ -2,7 +2,7 @@ /*! \file sygus_solver.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Haniel Barbosa, Morgan Deters + ** Andrew Reynolds, Haniel Barbosa, Abdalrhman Mohamed ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/smt/update_ostream.h b/src/smt/update_ostream.h index fd33beec7..98aaead88 100644 --- a/src/smt/update_ostream.h +++ b/src/smt/update_ostream.h @@ -2,7 +2,7 @@ /*! \file update_ostream.h ** \verbatim ** Top contributors (to current version): - ** Tim King, Mathias Preiner + ** Tim King, Mathias Preiner, Aina Niemetz ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/arith/approx_simplex.cpp b/src/theory/arith/approx_simplex.cpp index 2432e6945..49cf9fe0a 100644 --- a/src/theory/arith/approx_simplex.cpp +++ b/src/theory/arith/approx_simplex.cpp @@ -2,7 +2,7 @@ /*! \file approx_simplex.cpp ** \verbatim ** Top contributors (to current version): - ** Tim King, Mathias Preiner, Morgan Deters + ** Tim King, Aina Niemetz, Mathias Preiner ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index a65fbd961..a990b426f 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -2,7 +2,7 @@ /*! \file arith_rewriter.cpp ** \verbatim ** Top contributors (to current version): - ** Tim King, Andrew Reynolds, Morgan Deters + ** Andrew Reynolds, Tim King, Morgan Deters ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h index 8f35acd1c..6c858d1eb 100644 --- a/src/theory/arith/arith_rewriter.h +++ b/src/theory/arith/arith_rewriter.h @@ -2,7 +2,7 @@ /*! \file arith_rewriter.h ** \verbatim ** Top contributors (to current version): - ** Dejan Jovanovic, Tim King, Andres Noetzli + ** Dejan Jovanovic, Andrew Reynolds, Tim King ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/arith/arith_utilities.cpp b/src/theory/arith/arith_utilities.cpp index 1a5bc356f..fc34d2a6d 100644 --- a/src/theory/arith/arith_utilities.cpp +++ b/src/theory/arith/arith_utilities.cpp @@ -2,7 +2,7 @@ /*! \file arith_utilities.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King + ** Andrew Reynolds, Alex Ozdemir, Tim King ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/arith/attempt_solution_simplex.cpp b/src/theory/arith/attempt_solution_simplex.cpp index 22802b558..72f8e49ff 100644 --- a/src/theory/arith/attempt_solution_simplex.cpp +++ b/src/theory/arith/attempt_solution_simplex.cpp @@ -2,7 +2,7 @@ /*! \file attempt_solution_simplex.cpp ** \verbatim ** Top contributors (to current version): - ** Tim King, Mathias Preiner + ** Tim King, Aina Niemetz, Mathias Preiner ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/arith/bound_inference.cpp b/src/theory/arith/bound_inference.cpp index c8a9527c7..29be87d7b 100644 --- a/src/theory/arith/bound_inference.cpp +++ b/src/theory/arith/bound_inference.cpp @@ -4,8 +4,8 @@ ** Top contributors (to current version): ** Gereon Kremer ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/src/theory/arith/bound_inference.h b/src/theory/arith/bound_inference.h index 174ba3a0f..9d78d88c9 100644 --- a/src/theory/arith/bound_inference.h +++ b/src/theory/arith/bound_inference.h @@ -4,8 +4,8 @@ ** Top contributors (to current version): ** Gereon Kremer ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp index 57214e0f8..03dc28d6a 100644 --- a/src/theory/arith/congruence_manager.cpp +++ b/src/theory/arith/congruence_manager.cpp @@ -2,7 +2,7 @@ /*! \file congruence_manager.cpp ** \verbatim ** Top contributors (to current version): - ** Tim King, Andrew Reynolds, Dejan Jovanovic + ** Tim King, Alex Ozdemir, Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h index 3698f46d8..80e1ef8be 100644 --- a/src/theory/arith/congruence_manager.h +++ b/src/theory/arith/congruence_manager.h @@ -2,7 +2,7 @@ /*! \file congruence_manager.h ** \verbatim ** Top contributors (to current version): - ** Tim King, Andrew Reynolds, Mathias Preiner + ** Alex Ozdemir, Tim King, Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/arith/dual_simplex.cpp b/src/theory/arith/dual_simplex.cpp index 4ac3034ff..374b17d88 100644 --- a/src/theory/arith/dual_simplex.cpp +++ b/src/theory/arith/dual_simplex.cpp @@ -2,7 +2,7 @@ /*! \file dual_simplex.cpp ** \verbatim ** Top contributors (to current version): - ** Tim King, Morgan Deters, Mathias Preiner + ** Tim King, Aina Niemetz, Morgan Deters ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/arith/fc_simplex.cpp b/src/theory/arith/fc_simplex.cpp index 33f01eba1..85af862fa 100644 --- a/src/theory/arith/fc_simplex.cpp +++ b/src/theory/arith/fc_simplex.cpp @@ -2,7 +2,7 @@ /*! \file fc_simplex.cpp ** \verbatim ** Top contributors (to current version): - ** Tim King, Mathias Preiner, Morgan Deters + ** Tim King, Aina Niemetz, Mathias Preiner ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/arith/inference_id.cpp b/src/theory/arith/inference_id.cpp index a93a980ba..0c2ead445 100644 --- a/src/theory/arith/inference_id.cpp +++ b/src/theory/arith/inference_id.cpp @@ -2,7 +2,7 @@ /*! \file inference_id.cpp ** \verbatim ** Top contributors (to current version): - ** Gereon Kremer + ** Gereon Kremer, Yoni Zohar ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/arith/inference_id.h b/src/theory/arith/inference_id.h index c01cd2c8e..ea7fd6fe9 100644 --- a/src/theory/arith/inference_id.h +++ b/src/theory/arith/inference_id.h @@ -2,7 +2,7 @@ /*! \file inference_id.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Gereon Kremer + ** Andrew Reynolds, Gereon Kremer, Yoni Zohar ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/arith/nl/ext/constraint.h b/src/theory/arith/nl/ext/constraint.h index 699d5b350..7b7c604bf 100644 --- a/src/theory/arith/nl/ext/constraint.h +++ b/src/theory/arith/nl/ext/constraint.h @@ -2,7 +2,7 @@ /*! \file constraint.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Gereon Kremer ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/arith/nl/ext/ext_state.cpp b/src/theory/arith/nl/ext/ext_state.cpp index 3ac4699a7..d850ff34e 100644 --- a/src/theory/arith/nl/ext/ext_state.cpp +++ b/src/theory/arith/nl/ext/ext_state.cpp @@ -1,8 +1,8 @@ /********************* */ -/*! \file shared_check_data.cpp +/*! \file ext_state.cpp ** \verbatim ** Top contributors (to current version): - ** Gereon Kremer + ** Andrew Reynolds, Gereon Kremer, Tim King ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/arith/nl/ext/ext_state.h b/src/theory/arith/nl/ext/ext_state.h index 64c9c6b94..adf576c8b 100644 --- a/src/theory/arith/nl/ext/ext_state.h +++ b/src/theory/arith/nl/ext/ext_state.h @@ -1,8 +1,8 @@ /********************* */ -/*! \file shared_check_data.h +/*! \file ext_state.h ** \verbatim ** Top contributors (to current version): - ** Gereon Kremer + ** Gereon Kremer, Andrew Reynolds, Tim King ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/arith/nl/ext/factoring_check.cpp b/src/theory/arith/nl/ext/factoring_check.cpp index e329db121..71c584e91 100644 --- a/src/theory/arith/nl/ext/factoring_check.cpp +++ b/src/theory/arith/nl/ext/factoring_check.cpp @@ -2,7 +2,7 @@ /*! \file factoring_check.cpp ** \verbatim ** Top contributors (to current version): - ** Gereon Kremer + ** Andrew Reynolds, Gereon Kremer, Tim King ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/arith/nl/ext/factoring_check.h b/src/theory/arith/nl/ext/factoring_check.h index 8474ac610..9f879aa39 100644 --- a/src/theory/arith/nl/ext/factoring_check.h +++ b/src/theory/arith/nl/ext/factoring_check.h @@ -2,7 +2,7 @@ /*! \file factoring_check.h ** \verbatim ** Top contributors (to current version): - ** Gereon Kremer + ** Andrew Reynolds, Gereon Kremer ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/arith/nl/ext/monomial.h b/src/theory/arith/nl/ext/monomial.h index 93a291ca0..a1cc8d7ff 100644 --- a/src/theory/arith/nl/ext/monomial.h +++ b/src/theory/arith/nl/ext/monomial.h @@ -2,7 +2,7 @@ /*! \file monomial.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King + ** Andrew Reynolds, Tim King, Gereon Kremer ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/arith/nl/ext/monomial_bounds_check.cpp b/src/theory/arith/nl/ext/monomial_bounds_check.cpp index de6a3c65d..9eb496de8 100644 --- a/src/theory/arith/nl/ext/monomial_bounds_check.cpp +++ b/src/theory/arith/nl/ext/monomial_bounds_check.cpp @@ -2,7 +2,7 @@ /*! \file monomial_bounds_check.cpp ** \verbatim ** Top contributors (to current version): - ** Gereon Kremer + ** Andrew Reynolds, Gereon Kremer, Tim King ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/arith/nl/ext/monomial_bounds_check.h b/src/theory/arith/nl/ext/monomial_bounds_check.h index d919b1272..9977d7534 100644 --- a/src/theory/arith/nl/ext/monomial_bounds_check.h +++ b/src/theory/arith/nl/ext/monomial_bounds_check.h @@ -2,7 +2,7 @@ /*! \file monomial_bounds_check.h ** \verbatim ** Top contributors (to current version): - ** Gereon Kremer + ** Andrew Reynolds, Gereon Kremer, Tim King ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/arith/nl/ext/monomial_check.cpp b/src/theory/arith/nl/ext/monomial_check.cpp index 3b8d52c13..a70fa1bc0 100644 --- a/src/theory/arith/nl/ext/monomial_check.cpp +++ b/src/theory/arith/nl/ext/monomial_check.cpp @@ -2,7 +2,7 @@ /*! \file monomial_check.cpp ** \verbatim ** Top contributors (to current version): - ** Gereon Kremer + ** Andrew Reynolds, Gereon Kremer, Tim King ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/arith/nl/ext/monomial_check.h b/src/theory/arith/nl/ext/monomial_check.h index 89b5847a2..ed8639ef2 100644 --- a/src/theory/arith/nl/ext/monomial_check.h +++ b/src/theory/arith/nl/ext/monomial_check.h @@ -2,7 +2,7 @@ /*! \file monomial_check.h ** \verbatim ** Top contributors (to current version): - ** Gereon Kremer + ** Andrew Reynolds, Gereon Kremer, Tim King ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/arith/nl/ext/split_zero_check.h b/src/theory/arith/nl/ext/split_zero_check.h index 1a9f0a44d..131ad4c99 100644 --- a/src/theory/arith/nl/ext/split_zero_check.h +++ b/src/theory/arith/nl/ext/split_zero_check.h @@ -2,7 +2,7 @@ /*! \file split_zero_check.h ** \verbatim ** Top contributors (to current version): - ** Gereon Kremer + ** Gereon Kremer, Andrew Reynolds, Tim King ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/arith/nl/ext/tangent_plane_check.cpp b/src/theory/arith/nl/ext/tangent_plane_check.cpp index 3849c8424..de6176272 100644 --- a/src/theory/arith/nl/ext/tangent_plane_check.cpp +++ b/src/theory/arith/nl/ext/tangent_plane_check.cpp @@ -2,7 +2,7 @@ /*! \file tangent_plane_check.cpp ** \verbatim ** Top contributors (to current version): - ** Gereon Kremer + ** Andrew Reynolds, Gereon Kremer, Tim King ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/arith/nl/ext/tangent_plane_check.h b/src/theory/arith/nl/ext/tangent_plane_check.h index 748ab6372..84b6c0ba4 100644 --- a/src/theory/arith/nl/ext/tangent_plane_check.h +++ b/src/theory/arith/nl/ext/tangent_plane_check.h @@ -2,7 +2,7 @@ /*! \file tangent_plane_check.h ** \verbatim ** Top contributors (to current version): - ** Gereon Kremer + ** Andrew Reynolds, Gereon Kremer ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/arith/nl/iand_solver.cpp b/src/theory/arith/nl/iand_solver.cpp index e33cfa6cd..4d17080a6 100644 --- a/src/theory/arith/nl/iand_solver.cpp +++ b/src/theory/arith/nl/iand_solver.cpp @@ -2,7 +2,7 @@ /*! \file iand_solver.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Gereon Kremer, Tim King + ** Andrew Reynolds, Yoni Zohar, Gereon Kremer ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/arith/nl/iand_solver.h b/src/theory/arith/nl/iand_solver.h index e00cb92a9..8d91cc28a 100644 --- a/src/theory/arith/nl/iand_solver.h +++ b/src/theory/arith/nl/iand_solver.h @@ -2,7 +2,7 @@ /*! \file iand_solver.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Tianyi Liang + ** Andrew Reynolds, Yoni Zohar, Gereon Kremer ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/arith/nl/iand_table.cpp b/src/theory/arith/nl/iand_table.cpp index 050e6baed..550f36d92 100644 --- a/src/theory/arith/nl/iand_table.cpp +++ b/src/theory/arith/nl/iand_table.cpp @@ -5,7 +5,7 @@ ** Yoni Zohar ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/src/theory/arith/nl/iand_table.h b/src/theory/arith/nl/iand_table.h index 6387885b7..39eb82355 100644 --- a/src/theory/arith/nl/iand_table.h +++ b/src/theory/arith/nl/iand_table.h @@ -5,7 +5,7 @@ ** Yoni Zohar ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/src/theory/arith/nl/icp/candidate.cpp b/src/theory/arith/nl/icp/candidate.cpp index df8e18818..5dc2443d0 100644 --- a/src/theory/arith/nl/icp/candidate.cpp +++ b/src/theory/arith/nl/icp/candidate.cpp @@ -4,8 +4,8 @@ ** Top contributors (to current version): ** Gereon Kremer ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/src/theory/arith/nl/icp/candidate.h b/src/theory/arith/nl/icp/candidate.h index 7980e5c97..a2160472d 100644 --- a/src/theory/arith/nl/icp/candidate.h +++ b/src/theory/arith/nl/icp/candidate.h @@ -4,8 +4,8 @@ ** Top contributors (to current version): ** Gereon Kremer ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/src/theory/arith/nl/icp/contraction_origins.cpp b/src/theory/arith/nl/icp/contraction_origins.cpp index 779c000b7..858915537 100644 --- a/src/theory/arith/nl/icp/contraction_origins.cpp +++ b/src/theory/arith/nl/icp/contraction_origins.cpp @@ -4,8 +4,8 @@ ** Top contributors (to current version): ** Gereon Kremer ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/src/theory/arith/nl/icp/contraction_origins.h b/src/theory/arith/nl/icp/contraction_origins.h index 885fc740a..360641704 100644 --- a/src/theory/arith/nl/icp/contraction_origins.h +++ b/src/theory/arith/nl/icp/contraction_origins.h @@ -4,8 +4,8 @@ ** Top contributors (to current version): ** Gereon Kremer ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/src/theory/arith/nl/icp/icp_solver.cpp b/src/theory/arith/nl/icp/icp_solver.cpp index b4cb54216..ec32656e0 100644 --- a/src/theory/arith/nl/icp/icp_solver.cpp +++ b/src/theory/arith/nl/icp/icp_solver.cpp @@ -2,10 +2,10 @@ /*! \file icp_solver.cpp ** \verbatim ** Top contributors (to current version): - ** Gereon Kremer + ** Gereon Kremer, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/src/theory/arith/nl/icp/icp_solver.h b/src/theory/arith/nl/icp/icp_solver.h index 32861c641..176549d8b 100644 --- a/src/theory/arith/nl/icp/icp_solver.h +++ b/src/theory/arith/nl/icp/icp_solver.h @@ -2,10 +2,10 @@ /*! \file icp_solver.h ** \verbatim ** Top contributors (to current version): - ** Gereon Kremer + ** Gereon Kremer, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/src/theory/arith/nl/icp/intersection.cpp b/src/theory/arith/nl/icp/intersection.cpp index 148059db0..aa8fcf543 100644 --- a/src/theory/arith/nl/icp/intersection.cpp +++ b/src/theory/arith/nl/icp/intersection.cpp @@ -4,8 +4,8 @@ ** Top contributors (to current version): ** Gereon Kremer ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/src/theory/arith/nl/icp/intersection.h b/src/theory/arith/nl/icp/intersection.h index 8d772cb7a..0df6caf34 100644 --- a/src/theory/arith/nl/icp/intersection.h +++ b/src/theory/arith/nl/icp/intersection.h @@ -4,8 +4,8 @@ ** Top contributors (to current version): ** Gereon Kremer ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/src/theory/arith/nl/icp/interval.h b/src/theory/arith/nl/icp/interval.h index 374067961..d2b0fd4f5 100644 --- a/src/theory/arith/nl/icp/interval.h +++ b/src/theory/arith/nl/icp/interval.h @@ -4,8 +4,8 @@ ** Top contributors (to current version): ** Gereon Kremer ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h index b563384a5..88706350b 100644 --- a/src/theory/arith/nl/nonlinear_extension.h +++ b/src/theory/arith/nl/nonlinear_extension.h @@ -2,7 +2,7 @@ /*! \file nonlinear_extension.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Gereon Kremer + ** Andrew Reynolds, Gereon Kremer, Tim King ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/arith/nl/strategy.cpp b/src/theory/arith/nl/strategy.cpp index 627500d68..90ab14ac5 100644 --- a/src/theory/arith/nl/strategy.cpp +++ b/src/theory/arith/nl/strategy.cpp @@ -2,10 +2,10 @@ /*! \file strategy.cpp ** \verbatim ** Top contributors (to current version): - ** Gereon Kremer + ** Gereon Kremer, Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/src/theory/arith/nl/strategy.h b/src/theory/arith/nl/strategy.h index ad96d9442..526ae36f1 100644 --- a/src/theory/arith/nl/strategy.h +++ b/src/theory/arith/nl/strategy.h @@ -5,7 +5,7 @@ ** Gereon Kremer ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/src/theory/arith/nl/transcendental/exponential_solver.cpp b/src/theory/arith/nl/transcendental/exponential_solver.cpp index 482e3bc21..0726e03b3 100644 --- a/src/theory/arith/nl/transcendental/exponential_solver.cpp +++ b/src/theory/arith/nl/transcendental/exponential_solver.cpp @@ -1,8 +1,8 @@ /********************* */ -/*! \file transcendental_solver.cpp +/*! \file exponential_solver.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Gereon Kremer + ** Gereon Kremer, Andrew Reynolds, Tim King ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/arith/nl/transcendental/exponential_solver.h b/src/theory/arith/nl/transcendental/exponential_solver.h index b4d08559a..f1a30b177 100644 --- a/src/theory/arith/nl/transcendental/exponential_solver.h +++ b/src/theory/arith/nl/transcendental/exponential_solver.h @@ -2,7 +2,7 @@ /*! \file exponential_solver.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King + ** Gereon Kremer, Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/arith/nl/transcendental/sine_solver.cpp b/src/theory/arith/nl/transcendental/sine_solver.cpp index cba85b80e..5eed810b3 100644 --- a/src/theory/arith/nl/transcendental/sine_solver.cpp +++ b/src/theory/arith/nl/transcendental/sine_solver.cpp @@ -1,8 +1,8 @@ /********************* */ -/*! \file transcendental_solver.cpp +/*! \file sine_solver.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Gereon Kremer + ** Gereon Kremer, Andrew Reynolds, Tim King ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/arith/nl/transcendental/sine_solver.h b/src/theory/arith/nl/transcendental/sine_solver.h index e41e6bd4f..15f7d46e8 100644 --- a/src/theory/arith/nl/transcendental/sine_solver.h +++ b/src/theory/arith/nl/transcendental/sine_solver.h @@ -2,7 +2,7 @@ /*! \file sine_solver.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King + ** Gereon Kremer, Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/arith/nl/transcendental/taylor_generator.cpp b/src/theory/arith/nl/transcendental/taylor_generator.cpp index 1b7257f8f..745cba17a 100644 --- a/src/theory/arith/nl/transcendental/taylor_generator.cpp +++ b/src/theory/arith/nl/transcendental/taylor_generator.cpp @@ -2,7 +2,7 @@ /*! \file taylor_generator.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King + ** Andrew Reynolds, Gereon Kremer, Tim King ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/arith/nl/transcendental/taylor_generator.h b/src/theory/arith/nl/transcendental/taylor_generator.h index 2dbfcccde..261583ca9 100644 --- a/src/theory/arith/nl/transcendental/taylor_generator.h +++ b/src/theory/arith/nl/transcendental/taylor_generator.h @@ -2,7 +2,7 @@ /*! \file taylor_generator.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King + ** Andrew Reynolds, Gereon Kremer ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.cpp b/src/theory/arith/nl/transcendental/transcendental_solver.cpp index ad3f49576..2a22853a2 100644 --- a/src/theory/arith/nl/transcendental/transcendental_solver.cpp +++ b/src/theory/arith/nl/transcendental/transcendental_solver.cpp @@ -2,7 +2,7 @@ /*! \file transcendental_solver.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Gereon Kremer + ** Andrew Reynolds, Gereon Kremer, Tim King ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.h b/src/theory/arith/nl/transcendental/transcendental_solver.h index b0db79b6a..80def6f05 100644 --- a/src/theory/arith/nl/transcendental/transcendental_solver.h +++ b/src/theory/arith/nl/transcendental/transcendental_solver.h @@ -1,3 +1,19 @@ +/********************* */ +/*! \file transcendental_solver.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Gereon Kremer, Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. 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 + **/ /********************* */ /*! \file transcendental_solver.h diff --git a/src/theory/arith/nl/transcendental/transcendental_state.cpp b/src/theory/arith/nl/transcendental/transcendental_state.cpp index 69678c621..0e47f4257 100644 --- a/src/theory/arith/nl/transcendental/transcendental_state.cpp +++ b/src/theory/arith/nl/transcendental/transcendental_state.cpp @@ -2,7 +2,7 @@ /*! \file transcendental_state.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Gereon Kremer + ** Andrew Reynolds, Gereon Kremer ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/arith/nl/transcendental/transcendental_state.h b/src/theory/arith/nl/transcendental/transcendental_state.h index e1510c3b3..7062e8183 100644 --- a/src/theory/arith/nl/transcendental/transcendental_state.h +++ b/src/theory/arith/nl/transcendental/transcendental_state.h @@ -2,7 +2,7 @@ /*! \file transcendental_state.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King + ** Gereon Kremer, Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp index fc9a86f49..ed02a8d4e 100644 --- a/src/theory/arith/normal_form.cpp +++ b/src/theory/arith/normal_form.cpp @@ -2,7 +2,7 @@ /*! \file normal_form.cpp ** \verbatim ** Top contributors (to current version): - ** Tim King, Andrew Reynolds, Morgan Deters + ** Tim King, Gereon Kremer, Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h index 79cae2fff..ea20de71d 100644 --- a/src/theory/arith/normal_form.h +++ b/src/theory/arith/normal_form.h @@ -2,7 +2,7 @@ /*! \file normal_form.h ** \verbatim ** Top contributors (to current version): - ** Tim King, Morgan Deters, Mathias Preiner + ** Tim King, Morgan Deters, Gereon Kremer ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/arith/soi_simplex.cpp b/src/theory/arith/soi_simplex.cpp index 3f2fca50f..18169474d 100644 --- a/src/theory/arith/soi_simplex.cpp +++ b/src/theory/arith/soi_simplex.cpp @@ -2,7 +2,7 @@ /*! \file soi_simplex.cpp ** \verbatim ** Top contributors (to current version): - ** Tim King, Morgan Deters, Mathias Preiner + ** Tim King, Aina Niemetz, Morgan Deters ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index b5c0d1bd0..247772897 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -2,7 +2,7 @@ /*! \file theory_arith.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Dejan Jovanovic + ** Andrew Reynolds, Tim King, Alex Ozdemir ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 74f2bdbd3..ce0445d1f 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -2,7 +2,7 @@ /*! \file theory_arith_private.cpp ** \verbatim ** Top contributors (to current version): - ** Tim King, Andrew Reynolds, Mathias Preiner + ** Tim King, Alex Ozdemir, Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/arrays/inference_manager.cpp b/src/theory/arrays/inference_manager.cpp index f429140be..ec6890293 100644 --- a/src/theory/arrays/inference_manager.cpp +++ b/src/theory/arrays/inference_manager.cpp @@ -5,7 +5,7 @@ ** Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/src/theory/arrays/inference_manager.h b/src/theory/arrays/inference_manager.h index 2073fac6a..b4ae228be 100644 --- a/src/theory/arrays/inference_manager.h +++ b/src/theory/arrays/inference_manager.h @@ -2,10 +2,10 @@ /*! \file inference_manager.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Morgan Deters ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/src/theory/arrays/proof_checker.cpp b/src/theory/arrays/proof_checker.cpp index a3cd82678..e529d981c 100644 --- a/src/theory/arrays/proof_checker.cpp +++ b/src/theory/arrays/proof_checker.cpp @@ -2,10 +2,10 @@ /*! \file proof_checker.cpp ** \verbatim ** Top contributors (to current version): - ** Haniel Barbosa + ** Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/src/theory/arrays/proof_checker.h b/src/theory/arrays/proof_checker.h index 3bf7afecb..7fa574eeb 100644 --- a/src/theory/arrays/proof_checker.h +++ b/src/theory/arrays/proof_checker.h @@ -5,7 +5,7 @@ ** Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/src/theory/arrays/skolem_cache.cpp b/src/theory/arrays/skolem_cache.cpp index 70217a4d7..4028a53a8 100644 --- a/src/theory/arrays/skolem_cache.cpp +++ b/src/theory/arrays/skolem_cache.cpp @@ -2,10 +2,10 @@ /*! \file skolem_cache.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Morgan Deters ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/src/theory/arrays/skolem_cache.h b/src/theory/arrays/skolem_cache.h index b07e87dc6..dd4ac2e5b 100644 --- a/src/theory/arrays/skolem_cache.h +++ b/src/theory/arrays/skolem_cache.h @@ -2,10 +2,10 @@ /*! \file skolem_cache.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Morgan Deters ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/src/theory/bags/bags_rewriter.cpp b/src/theory/bags/bags_rewriter.cpp index 9479d2cc2..aee57c74d 100644 --- a/src/theory/bags/bags_rewriter.cpp +++ b/src/theory/bags/bags_rewriter.cpp @@ -5,7 +5,7 @@ ** Mudathir Mohamed ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/src/theory/bags/bags_rewriter.h b/src/theory/bags/bags_rewriter.h index a9b3b90bb..8425e3b1f 100644 --- a/src/theory/bags/bags_rewriter.h +++ b/src/theory/bags/bags_rewriter.h @@ -5,7 +5,7 @@ ** Mudathir Mohamed ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/src/theory/bags/inference_manager.cpp b/src/theory/bags/inference_manager.cpp index 4d18ad926..eb695725e 100644 --- a/src/theory/bags/inference_manager.cpp +++ b/src/theory/bags/inference_manager.cpp @@ -2,10 +2,10 @@ /*! \file inference_manager.cpp ** \verbatim ** Top contributors (to current version): - ** Mudathir Mohamed + ** Mudathir Mohamed, Morgan Deters, Dejan Jovanovic ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/src/theory/bags/inference_manager.h b/src/theory/bags/inference_manager.h index 4b4edbaef..90d188d33 100644 --- a/src/theory/bags/inference_manager.h +++ b/src/theory/bags/inference_manager.h @@ -5,7 +5,7 @@ ** Mudathir Mohamed ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/src/theory/bags/make_bag_op.cpp b/src/theory/bags/make_bag_op.cpp index b60822783..ac3d8942a 100644 --- a/src/theory/bags/make_bag_op.cpp +++ b/src/theory/bags/make_bag_op.cpp @@ -1,5 +1,5 @@ /********************* */ -/*! \file bag_op.cpp +/*! \file make_bag_op.cpp ** \verbatim ** Top contributors (to current version): ** Mudathir Mohamed diff --git a/src/theory/bags/make_bag_op.h b/src/theory/bags/make_bag_op.h index b47930879..a53000651 100644 --- a/src/theory/bags/make_bag_op.h +++ b/src/theory/bags/make_bag_op.h @@ -1,5 +1,5 @@ /********************* */ -/*! \file mk_bag_op.h +/*! \file make_bag_op.h ** \verbatim ** Top contributors (to current version): ** Mudathir Mohamed diff --git a/src/theory/bags/normal_form.cpp b/src/theory/bags/normal_form.cpp index 081ed77aa..88c41a961 100644 --- a/src/theory/bags/normal_form.cpp +++ b/src/theory/bags/normal_form.cpp @@ -1,15 +1,16 @@ -/************************* */ +/********************* */ /*! \file normal_form.cpp ** \verbatim ** Top contributors (to current version): ** Mudathir Mohamed ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim + ** + ** \brief Normal form for bag constants. **/ - #include "normal_form.h" #include "theory/sets/normal_form.h" @@ -653,4 +654,4 @@ Node NormalForm::evaluateToSet(TNode n) } // namespace bags } // namespace theory -} // namespace CVC4
\ No newline at end of file +} // namespace CVC4 diff --git a/src/theory/bags/normal_form.h b/src/theory/bags/normal_form.h index 5a7936fa3..e88fe6fef 100644 --- a/src/theory/bags/normal_form.h +++ b/src/theory/bags/normal_form.h @@ -5,7 +5,7 @@ ** Mudathir Mohamed ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/src/theory/bags/solver_state.cpp b/src/theory/bags/solver_state.cpp index 77204ae76..d58b68657 100644 --- a/src/theory/bags/solver_state.cpp +++ b/src/theory/bags/solver_state.cpp @@ -2,10 +2,10 @@ /*! \file solver_state.cpp ** \verbatim ** Top contributors (to current version): - ** Mudathir Mohamed + ** Mudathir Mohamed, Morgan Deters, Dejan Jovanovic ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/src/theory/bags/solver_state.h b/src/theory/bags/solver_state.h index f5b67cb78..9a4bfdae7 100644 --- a/src/theory/bags/solver_state.h +++ b/src/theory/bags/solver_state.h @@ -5,7 +5,7 @@ ** Mudathir Mohamed ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/src/theory/bags/term_registry.cpp b/src/theory/bags/term_registry.cpp index 60beef29f..c413a7f90 100644 --- a/src/theory/bags/term_registry.cpp +++ b/src/theory/bags/term_registry.cpp @@ -2,10 +2,10 @@ /*! \file term_registry.cpp ** \verbatim ** Top contributors (to current version): - ** Mudathir Mohamed + ** Mudathir Mohamed, Morgan Deters, Dejan Jovanovic ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/src/theory/bags/term_registry.h b/src/theory/bags/term_registry.h index d284126ee..abf6f180c 100644 --- a/src/theory/bags/term_registry.h +++ b/src/theory/bags/term_registry.h @@ -5,7 +5,7 @@ ** Mudathir Mohamed ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/src/theory/bags/theory_bags.cpp b/src/theory/bags/theory_bags.cpp index 9f62ea1c6..6ba1ad87a 100644 --- a/src/theory/bags/theory_bags.cpp +++ b/src/theory/bags/theory_bags.cpp @@ -5,7 +5,7 @@ ** Mudathir Mohamed ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/src/theory/bags/theory_bags.h b/src/theory/bags/theory_bags.h index 08bc5f33a..03676c2d2 100644 --- a/src/theory/bags/theory_bags.h +++ b/src/theory/bags/theory_bags.h @@ -5,7 +5,7 @@ ** Mudathir Mohamed ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/src/theory/bags/theory_bags_type_enumerator.cpp b/src/theory/bags/theory_bags_type_enumerator.cpp index 727407937..a1a1d13c2 100644 --- a/src/theory/bags/theory_bags_type_enumerator.cpp +++ b/src/theory/bags/theory_bags_type_enumerator.cpp @@ -5,7 +5,7 @@ ** Mudathir Mohamed ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/src/theory/bags/theory_bags_type_enumerator.h b/src/theory/bags/theory_bags_type_enumerator.h index a1ba896c1..dda87c85e 100644 --- a/src/theory/bags/theory_bags_type_enumerator.h +++ b/src/theory/bags/theory_bags_type_enumerator.h @@ -5,7 +5,7 @@ ** Mudathir Mohamed ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/src/theory/bags/theory_bags_type_rules.h b/src/theory/bags/theory_bags_type_rules.h index cece40c9e..dd8c75328 100644 --- a/src/theory/bags/theory_bags_type_rules.h +++ b/src/theory/bags/theory_bags_type_rules.h @@ -4,8 +4,8 @@ ** Top contributors (to current version): ** Mudathir Mohamed ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/src/theory/booleans/circuit_propagator.cpp b/src/theory/booleans/circuit_propagator.cpp index 270c0b9a9..24e821e33 100644 --- a/src/theory/booleans/circuit_propagator.cpp +++ b/src/theory/booleans/circuit_propagator.cpp @@ -2,7 +2,7 @@ /*! \file circuit_propagator.cpp ** \verbatim ** Top contributors (to current version): - ** Dejan Jovanovic, Morgan Deters, Andrew Reynolds + ** Gereon Kremer, Morgan Deters, Dejan Jovanovic ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h index 4c7c2d124..3546a4d35 100644 --- a/src/theory/booleans/circuit_propagator.h +++ b/src/theory/booleans/circuit_propagator.h @@ -2,7 +2,7 @@ /*! \file circuit_propagator.h ** \verbatim ** Top contributors (to current version): - ** Aina Niemetz, Morgan Deters, Dejan Jovanovic + ** Morgan Deters, Aina Niemetz, Gereon Kremer ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp index c08012b61..90de1d8da 100644 --- a/src/theory/booleans/theory_bool.cpp +++ b/src/theory/booleans/theory_bool.cpp @@ -2,7 +2,7 @@ /*! \file theory_bool.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Dejan Jovanovic, Morgan Deters + ** Andrew Reynolds, Morgan Deters, Dejan Jovanovic ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/builtin/theory_builtin_rewriter.h b/src/theory/builtin/theory_builtin_rewriter.h index 5fe4b159d..f02cc66eb 100644 --- a/src/theory/builtin/theory_builtin_rewriter.h +++ b/src/theory/builtin/theory_builtin_rewriter.h @@ -2,7 +2,7 @@ /*! \file theory_builtin_rewriter.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Andres Noetzli, Dejan Jovanovic + ** Andrew Reynolds, Andres Noetzli, Mathias Preiner ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/builtin/theory_builtin_type_rules.cpp b/src/theory/builtin/theory_builtin_type_rules.cpp index 59c1ecd65..450d4a569 100644 --- a/src/theory/builtin/theory_builtin_type_rules.cpp +++ b/src/theory/builtin/theory_builtin_type_rules.cpp @@ -2,7 +2,7 @@ /*! \file theory_builtin_type_rules.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/bv/bv_solver_simple.cpp b/src/theory/bv/bv_solver_simple.cpp index e03feedfc..153d85df5 100644 --- a/src/theory/bv/bv_solver_simple.cpp +++ b/src/theory/bv/bv_solver_simple.cpp @@ -5,7 +5,7 @@ ** Mathias Preiner ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/src/theory/bv/bv_solver_simple.h b/src/theory/bv/bv_solver_simple.h index 59239a52c..d4010cb95 100644 --- a/src/theory/bv/bv_solver_simple.h +++ b/src/theory/bv/bv_solver_simple.h @@ -2,10 +2,10 @@ /*! \file bv_solver_simple.h ** \verbatim ** Top contributors (to current version): - ** Mathias Preiner + ** Mathias Preiner, Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp index 50a509517..e1230a56c 100644 --- a/src/theory/bv/bv_subtheory_algebraic.cpp +++ b/src/theory/bv/bv_subtheory_algebraic.cpp @@ -2,7 +2,7 @@ /*! \file bv_subtheory_algebraic.cpp ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean, Aina Niemetz, Mathias Preiner + ** Liana Hadarean, Aina Niemetz, Tim King ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index fa228131c..093a35a1b 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -2,7 +2,7 @@ /*! \file theory_bv.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Mathias Preiner, Tim King + ** Mathias Preiner, Andrew Reynolds, Tim King ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp index 747ed89b7..4dbf26062 100644 --- a/src/theory/datatypes/datatypes_rewriter.cpp +++ b/src/theory/datatypes/datatypes_rewriter.cpp @@ -2,7 +2,7 @@ /*! \file datatypes_rewriter.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, Mathias Preiner + ** Andrew Reynolds, Mathias Preiner, Morgan Deters ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/datatypes/infer_proof_cons.cpp b/src/theory/datatypes/infer_proof_cons.cpp index 443218bf4..f483291ca 100644 --- a/src/theory/datatypes/infer_proof_cons.cpp +++ b/src/theory/datatypes/infer_proof_cons.cpp @@ -4,8 +4,8 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/src/theory/datatypes/infer_proof_cons.h b/src/theory/datatypes/infer_proof_cons.h index 34e042237..af6efc0a8 100644 --- a/src/theory/datatypes/infer_proof_cons.h +++ b/src/theory/datatypes/infer_proof_cons.h @@ -4,8 +4,8 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/src/theory/datatypes/inference.cpp b/src/theory/datatypes/inference.cpp index 806dfd418..308222146 100644 --- a/src/theory/datatypes/inference.cpp +++ b/src/theory/datatypes/inference.cpp @@ -2,7 +2,7 @@ /*! \file inference.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Gereon Kremer + ** Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/datatypes/inference_manager.cpp b/src/theory/datatypes/inference_manager.cpp index f391cacd9..e9496ab0a 100644 --- a/src/theory/datatypes/inference_manager.cpp +++ b/src/theory/datatypes/inference_manager.cpp @@ -2,7 +2,7 @@ /*! \file inference_manager.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Gereon Kremer + ** Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/datatypes/proof_checker.cpp b/src/theory/datatypes/proof_checker.cpp index 98060480b..6bfa20151 100644 --- a/src/theory/datatypes/proof_checker.cpp +++ b/src/theory/datatypes/proof_checker.cpp @@ -5,7 +5,7 @@ ** Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/src/theory/datatypes/proof_checker.h b/src/theory/datatypes/proof_checker.h index e5bd7cad5..1e47dd751 100644 --- a/src/theory/datatypes/proof_checker.h +++ b/src/theory/datatypes/proof_checker.h @@ -5,7 +5,7 @@ ** Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 45ce76504..5bff5d305 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -2,7 +2,7 @@ /*! \file theory_datatypes.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Mathias Preiner, Tim King + ** Andrew Reynolds, Tim King, Morgan Deters ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/fp/fp_converter.h b/src/theory/fp/fp_converter.h index 6688e8607..8b5f7905f 100644 --- a/src/theory/fp/fp_converter.h +++ b/src/theory/fp/fp_converter.h @@ -2,7 +2,7 @@ /*! \file fp_converter.h ** \verbatim ** Top contributors (to current version): - ** Martin Brain, Mathias Preiner + ** Martin Brain, Mathias Preiner, Aina Niemetz ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h index fe91a39bd..341955cff 100644 --- a/src/theory/fp/theory_fp.h +++ b/src/theory/fp/theory_fp.h @@ -2,7 +2,7 @@ /*! \file theory_fp.h ** \verbatim ** Top contributors (to current version): - ** Martin Brain, Andrew Reynolds, Mathias Preiner + ** Andrew Reynolds, Martin Brain, Aina Niemetz ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp index 78aba415b..763ca662c 100644 --- a/src/theory/fp/theory_fp_rewriter.cpp +++ b/src/theory/fp/theory_fp_rewriter.cpp @@ -2,7 +2,7 @@ /*! \file theory_fp_rewriter.cpp ** \verbatim ** Top contributors (to current version): - ** Martin Brain, Andres Noetzli, Andrew Reynolds + ** Martin Brain, Andres Noetzli, Aina Niemetz ** Copyright (c) 2013 University of Oxford ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS diff --git a/src/theory/fp/theory_fp_type_rules.h b/src/theory/fp/theory_fp_type_rules.h index d632e80c8..f09f1b449 100644 --- a/src/theory/fp/theory_fp_type_rules.h +++ b/src/theory/fp/theory_fp_type_rules.h @@ -2,7 +2,7 @@ /*! \file theory_fp_type_rules.h ** \verbatim ** Top contributors (to current version): - ** Martin Brain, Tim King, Andres Noetzli + ** Martin Brain, Tim King, Aina Niemetz ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/fp/type_enumerator.h b/src/theory/fp/type_enumerator.h index 47266eda8..79322a314 100644 --- a/src/theory/fp/type_enumerator.h +++ b/src/theory/fp/type_enumerator.h @@ -2,7 +2,7 @@ /*! \file type_enumerator.h ** \verbatim ** Top contributors (to current version): - ** Tim King, Martin Brain, Andrew Reynolds + ** Tim King, Martin Brain, Aina Niemetz ** Copyright (c) 2009-2015 New York University and The University of Iowa ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS diff --git a/src/theory/quantifiers/alpha_equivalence.cpp b/src/theory/quantifiers/alpha_equivalence.cpp index 20fcaad49..b4f9ee015 100644 --- a/src/theory/quantifiers/alpha_equivalence.cpp +++ b/src/theory/quantifiers/alpha_equivalence.cpp @@ -2,7 +2,7 @@ /*! \file alpha_equivalence.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Mathias Preiner, Morgan Deters + ** Andrew Reynolds, Mathias Preiner ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index 1d917b8f4..4884b4e3b 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -2,7 +2,7 @@ /*! \file inst_strategy_cegqi.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, Mathias Preiner + ** Andrew Reynolds, Morgan Deters, Tim King ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/quantifiers/quantifiers_modules.cpp b/src/theory/quantifiers/quantifiers_modules.cpp index 1efd6d38f..9dbca674e 100644 --- a/src/theory/quantifiers/quantifiers_modules.cpp +++ b/src/theory/quantifiers/quantifiers_modules.cpp @@ -2,10 +2,10 @@ /*! \file quantifiers_modules.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Mathias Preiner ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/src/theory/quantifiers/quantifiers_modules.h b/src/theory/quantifiers/quantifiers_modules.h index 87d8af37b..a4c5dfb6e 100644 --- a/src/theory/quantifiers/quantifiers_modules.h +++ b/src/theory/quantifiers/quantifiers_modules.h @@ -2,10 +2,10 @@ /*! \file quantifiers_modules.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Mathias Preiner ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/src/theory/quantifiers/skolemize.h b/src/theory/quantifiers/skolemize.h index 4469fe851..cb81a5c3a 100644 --- a/src/theory/quantifiers/skolemize.h +++ b/src/theory/quantifiers/skolemize.h @@ -2,7 +2,7 @@ /*! \file skolemize.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Mathias Preiner + ** Andrew Reynolds, Mathias Preiner, Abdalrhman Mohamed ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/quantifiers/sygus/sygus_interpol.cpp b/src/theory/quantifiers/sygus/sygus_interpol.cpp index d5ab0e51f..9fdb33700 100644 --- a/src/theory/quantifiers/sygus/sygus_interpol.cpp +++ b/src/theory/quantifiers/sygus/sygus_interpol.cpp @@ -2,7 +2,7 @@ /*! \file sygus_interpol.cpp ** \verbatim ** Top contributors (to current version): - ** Ying Sheng, Andrew Reynolds + ** Ying Sheng, Abdalrhman Mohamed, Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/quantifiers/sygus/sygus_interpol.h b/src/theory/quantifiers/sygus/sygus_interpol.h index 4db5f261a..a8b887172 100644 --- a/src/theory/quantifiers/sygus/sygus_interpol.h +++ b/src/theory/quantifiers/sygus/sygus_interpol.h @@ -2,7 +2,7 @@ /*! \file sygus_interpol.h ** \verbatim ** Top contributors (to current version): - ** Ying Sheng + ** Ying Sheng, Abdalrhman Mohamed ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp b/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp index 1a92cfc7f..b039db482 100644 --- a/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp +++ b/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp @@ -2,7 +2,7 @@ /*! \file sygus_qe_preproc.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Mathias Preiner, Morgan Deters ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index 3e40d6654..f49cc962f 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -2,7 +2,7 @@ /*! \file synth_engine.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Mathias Preiner, Haniel Barbosa + ** Andrew Reynolds, Haniel Barbosa ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/quantifiers/sygus/template_infer.cpp b/src/theory/quantifiers/sygus/template_infer.cpp index 2f6964f3a..0ac984aa3 100644 --- a/src/theory/quantifiers/sygus/template_infer.cpp +++ b/src/theory/quantifiers/sygus/template_infer.cpp @@ -1,8 +1,8 @@ /********************* */ -/*! \file template_infer.cpp +/*! \file template_infer.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Mathias Preiner, Tim King + ** Andrew Reynolds, Mathias Preiner ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp index 119cd925c..50c983ee7 100644 --- a/src/theory/quantifiers/sygus_inst.cpp +++ b/src/theory/quantifiers/sygus_inst.cpp @@ -2,7 +2,7 @@ /*! \file sygus_inst.cpp ** \verbatim ** Top contributors (to current version): - ** Mathias Preiner, Andrew Reynolds + ** Mathias Preiner, Aina Niemetz, Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index 4a7f4367e..d03cc8570 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -2,7 +2,7 @@ /*! \file theory_sep.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Dejan Jovanovic + ** Andrew Reynolds, Tim King, Mudathir Mohamed ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/sep/theory_sep_rewriter.cpp b/src/theory/sep/theory_sep_rewriter.cpp index 78837508e..2373bb6af 100644 --- a/src/theory/sep/theory_sep_rewriter.cpp +++ b/src/theory/sep/theory_sep_rewriter.cpp @@ -2,7 +2,7 @@ /*! \file theory_sep_rewriter.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Andres Noetzli + ** Andrew Reynolds, Mudathir Mohamed, Andres Noetzli ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/sets/normal_form.h b/src/theory/sets/normal_form.h index 2654344f3..08f0c2d1c 100644 --- a/src/theory/sets/normal_form.h +++ b/src/theory/sets/normal_form.h @@ -2,7 +2,7 @@ /*! \file normal_form.h ** \verbatim ** Top contributors (to current version): - ** Kshitij Bansal, Andrew Reynolds, Tim King + ** Andrew Reynolds, Kshitij Bansal, Mudathir Mohamed ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/sets/solver_state.cpp b/src/theory/sets/solver_state.cpp index 1d58945a5..18b384f6a 100644 --- a/src/theory/sets/solver_state.cpp +++ b/src/theory/sets/solver_state.cpp @@ -2,7 +2,7 @@ /*! \file solver_state.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Mudathir Mohamed + ** Andrew Reynolds, Mudathir Mohamed, Paul Meng ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp index 763024d5f..0e6ab1b18 100644 --- a/src/theory/sets/theory_sets.cpp +++ b/src/theory/sets/theory_sets.cpp @@ -2,7 +2,7 @@ /*! \file theory_sets.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Mudathir Mohamed, Kshitij Bansal + ** Andrew Reynolds, Kshitij Bansal, Andres Noetzli ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/sets/theory_sets_rewriter.h b/src/theory/sets/theory_sets_rewriter.h index e7d031b6f..35139331c 100644 --- a/src/theory/sets/theory_sets_rewriter.h +++ b/src/theory/sets/theory_sets_rewriter.h @@ -2,7 +2,7 @@ /*! \file theory_sets_rewriter.h ** \verbatim ** Top contributors (to current version): - ** Kshitij Bansal, Andres Noetzli, Mathias Preiner + ** Kshitij Bansal, Andrew Reynolds, Andres Noetzli ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h index c5e86f10c..3844248f2 100644 --- a/src/theory/sets/theory_sets_type_rules.h +++ b/src/theory/sets/theory_sets_type_rules.h @@ -2,7 +2,7 @@ /*! \file theory_sets_type_rules.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Kshitij Bansal, Paul Meng + ** Andrew Reynolds, Kshitij Bansal, Mudathir Mohamed ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/shared_solver.cpp b/src/theory/shared_solver.cpp index 24d7d29cf..01dd37f19 100644 --- a/src/theory/shared_solver.cpp +++ b/src/theory/shared_solver.cpp @@ -5,7 +5,7 @@ ** Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/src/theory/shared_solver.h b/src/theory/shared_solver.h index c3d95f3c4..46009e23c 100644 --- a/src/theory/shared_solver.h +++ b/src/theory/shared_solver.h @@ -5,7 +5,7 @@ ** Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/src/theory/shared_solver_distributed.cpp b/src/theory/shared_solver_distributed.cpp index c868ed206..fd0071b64 100644 --- a/src/theory/shared_solver_distributed.cpp +++ b/src/theory/shared_solver_distributed.cpp @@ -5,7 +5,7 @@ ** Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/src/theory/shared_solver_distributed.h b/src/theory/shared_solver_distributed.h index de6e29743..a4af0834c 100644 --- a/src/theory/shared_solver_distributed.h +++ b/src/theory/shared_solver_distributed.h @@ -5,7 +5,7 @@ ** Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp index edf512e4b..29bdc03f8 100644 --- a/src/theory/shared_terms_database.cpp +++ b/src/theory/shared_terms_database.cpp @@ -2,7 +2,7 @@ /*! \file shared_terms_database.cpp ** \verbatim ** Top contributors (to current version): - ** Dejan Jovanovic, Andrew Reynolds, Morgan Deters + ** Andrew Reynolds, Dejan Jovanovic, Morgan Deters ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp index 66f71bf14..902b90615 100644 --- a/src/theory/strings/infer_proof_cons.cpp +++ b/src/theory/strings/infer_proof_cons.cpp @@ -4,8 +4,8 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/src/theory/strings/infer_proof_cons.h b/src/theory/strings/infer_proof_cons.h index 63e341dfe..1b066b4b3 100644 --- a/src/theory/strings/infer_proof_cons.h +++ b/src/theory/strings/infer_proof_cons.h @@ -4,8 +4,8 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/src/theory/strings/regexp_elim.cpp b/src/theory/strings/regexp_elim.cpp index aaa9ffc48..770991286 100644 --- a/src/theory/strings/regexp_elim.cpp +++ b/src/theory/strings/regexp_elim.cpp @@ -2,7 +2,7 @@ /*! \file regexp_elim.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tianyi Liang, Mathias Preiner + ** Andrew Reynolds, Mathias Preiner, Andres Noetzli ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index d3e9e34f1..110ff9b2d 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -2,7 +2,7 @@ /*! \file theory_strings.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tianyi Liang, Yoni Zohar + ** Andrew Reynolds, Tianyi Liang, Andres Noetzli ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/strings/theory_strings_utils.cpp b/src/theory/strings/theory_strings_utils.cpp index 286c0dc04..b807fe1b3 100644 --- a/src/theory/strings/theory_strings_utils.cpp +++ b/src/theory/strings/theory_strings_utils.cpp @@ -2,7 +2,7 @@ /*! \file theory_strings_utils.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Andres Noetzli + ** Andrew Reynolds, Andres Noetzli, Yoni Zohar ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 78fe6927f..08ad8ac87 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -2,7 +2,7 @@ /*! \file theory.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Dejan Jovanovic + ** Andrew Reynolds, Tim King, Mathias Preiner ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/theory_eq_notify.h b/src/theory/theory_eq_notify.h index 3df5d32cb..e5137d9e4 100644 --- a/src/theory/theory_eq_notify.h +++ b/src/theory/theory_eq_notify.h @@ -2,10 +2,10 @@ /*! \file theory_eq_notify.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Mathias Preiner, Tim King ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/src/theory/theory_id.cpp b/src/theory/theory_id.cpp index 31b864e7f..e9111db8c 100644 --- a/src/theory/theory_id.cpp +++ b/src/theory/theory_id.cpp @@ -2,7 +2,7 @@ /*! \file theory_id.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Aina Niemetz, Tim King + ** Andrew Reynolds, Aina Niemetz, Mudathir Mohamed ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h index 35d9031ae..124b88e3e 100644 --- a/src/theory/theory_inference_manager.h +++ b/src/theory/theory_inference_manager.h @@ -2,7 +2,7 @@ /*! \file theory_inference_manager.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Mathias Preiner, Martin Brain + ** Andrew Reynolds, Mathias Preiner, Gereon Kremer ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index e8665bb83..19e992dc6 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -2,7 +2,7 @@ /*! \file theory_model.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Clark Barrett + ** Andrew Reynolds, Clark Barrett, Mathias Preiner ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/theory_preprocessor.cpp b/src/theory/theory_preprocessor.cpp index f5e5fa505..7d265fc67 100644 --- a/src/theory/theory_preprocessor.cpp +++ b/src/theory/theory_preprocessor.cpp @@ -2,7 +2,7 @@ /*! \file theory_preprocessor.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, Dejan Jovanovic + ** Andrew Reynolds, Dejan Jovanovic, Morgan Deters ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/theory_proof_step_buffer.cpp b/src/theory/theory_proof_step_buffer.cpp index a08b15901..f9ee77308 100644 --- a/src/theory/theory_proof_step_buffer.cpp +++ b/src/theory/theory_proof_step_buffer.cpp @@ -2,7 +2,7 @@ /*! \file theory_proof_step_buffer.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Haniel Barbosa, Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/theory_proof_step_buffer.h b/src/theory/theory_proof_step_buffer.h index d67781428..9dbd6dc39 100644 --- a/src/theory/theory_proof_step_buffer.h +++ b/src/theory/theory_proof_step_buffer.h @@ -2,7 +2,7 @@ /*! \file theory_proof_step_buffer.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Haniel Barbosa ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h index 5d2711f1d..003e439ae 100644 --- a/src/theory/theory_test_utils.h +++ b/src/theory/theory_test_utils.h @@ -2,7 +2,7 @@ /*! \file theory_test_utils.h ** \verbatim ** Top contributors (to current version): - ** Tim King, Morgan Deters, Mathias Preiner + ** Tim King, Morgan Deters, Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/trust_substitutions.cpp b/src/theory/trust_substitutions.cpp index aaa3b44f7..b289d83cc 100644 --- a/src/theory/trust_substitutions.cpp +++ b/src/theory/trust_substitutions.cpp @@ -2,7 +2,7 @@ /*! \file trust_substitutions.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Gereon Kremer ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/trust_substitutions.h b/src/theory/trust_substitutions.h index c316f08c5..08e2da895 100644 --- a/src/theory/trust_substitutions.h +++ b/src/theory/trust_substitutions.h @@ -2,7 +2,7 @@ /*! \file trust_substitutions.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Gereon Kremer ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/uf/proof_equality_engine.h b/src/theory/uf/proof_equality_engine.h index 4148da1de..8e6ef9a56 100644 --- a/src/theory/uf/proof_equality_engine.h +++ b/src/theory/uf/proof_equality_engine.h @@ -2,7 +2,7 @@ /*! \file proof_equality_engine.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Haniel Barbosa ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 3f76919eb..497e394c7 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -2,7 +2,7 @@ /*! \file theory_uf.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Dejan Jovanovic, Morgan Deters + ** Andrew Reynolds, Morgan Deters, Tim King ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index 24e485f5e..bc4536b72 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -1,7 +1,7 @@ ##################### ## CMakeLists.txt ## Top contributors (to current version): -## Mathias Preiner, Gereon Kremer, Andrew Reynolds +## Mathias Preiner, Gereon Kremer, Aina Niemetz ## This file is part of the CVC4 project. ## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ## in the top-level source directory and their institutional affiliations. diff --git a/src/util/floatingpoint.cpp b/src/util/floatingpoint.cpp index 5b291f3c5..44f31e916 100644 --- a/src/util/floatingpoint.cpp +++ b/src/util/floatingpoint.cpp @@ -2,7 +2,7 @@ /*! \file floatingpoint.cpp ** \verbatim ** Top contributors (to current version): - ** Martin Brain, Aina Niemetz, Haniel Barbosa + ** Aina Niemetz, Martin Brain, Haniel Barbosa ** Copyright (c) 2013 University of Oxford ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS diff --git a/src/util/floatingpoint_literal_symfpu.cpp b/src/util/floatingpoint_literal_symfpu.cpp index 77ab910fa..d1e58495a 100644 --- a/src/util/floatingpoint_literal_symfpu.cpp +++ b/src/util/floatingpoint_literal_symfpu.cpp @@ -2,7 +2,7 @@ /*! \file floatingpoint_literal_symfpu.cpp ** \verbatim ** Top contributors (to current version): - ** Martin Brain, Aina Niemetz + ** Martin Brain, Aina Niemetz, Mathias Preiner ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/util/gmp_util.h b/src/util/gmp_util.h index 995579c3b..80b178eab 100644 --- a/src/util/gmp_util.h +++ b/src/util/gmp_util.h @@ -2,7 +2,7 @@ /*! \file gmp_util.h ** \verbatim ** Top contributors (to current version): - ** Tim King, Andres Noetzli, Mathias Preiner + ** Tim King, Mathias Preiner, Morgan Deters ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/util/integer_cln_imp.cpp b/src/util/integer_cln_imp.cpp index 88db707d9..27863b9f8 100644 --- a/src/util/integer_cln_imp.cpp +++ b/src/util/integer_cln_imp.cpp @@ -2,7 +2,7 @@ /*! \file integer_cln_imp.cpp ** \verbatim ** Top contributors (to current version): - ** Tim King, Aina Niemetz, Morgan Deters + ** Aina Niemetz, Tim King, Gereon Kremer ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h index 29a5248e3..050f05fc3 100644 --- a/src/util/integer_cln_imp.h +++ b/src/util/integer_cln_imp.h @@ -2,7 +2,7 @@ /*! \file integer_cln_imp.h ** \verbatim ** Top contributors (to current version): - ** Tim King, Gereon Kremer, Morgan Deters + ** Aina Niemetz, Tim King, Gereon Kremer ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/util/integer_gmp_imp.cpp b/src/util/integer_gmp_imp.cpp index 5a4fc9349..fec71b26b 100644 --- a/src/util/integer_gmp_imp.cpp +++ b/src/util/integer_gmp_imp.cpp @@ -2,7 +2,7 @@ /*! \file integer_gmp_imp.cpp ** \verbatim ** Top contributors (to current version): - ** Tim King, Aina Niemetz, Liana Hadarean + ** Aina Niemetz, Tim King, Gereon Kremer ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h index a11a15f81..fe05dc982 100644 --- a/src/util/integer_gmp_imp.h +++ b/src/util/integer_gmp_imp.h @@ -2,7 +2,7 @@ /*! \file integer_gmp_imp.h ** \verbatim ** Top contributors (to current version): - ** Tim King, Gereon Kremer, Liana Hadarean + ** Aina Niemetz, Tim King, Gereon Kremer ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/src/util/resource_manager.cpp b/src/util/resource_manager.cpp index 9afa79ef0..17dac50b3 100644 --- a/src/util/resource_manager.cpp +++ b/src/util/resource_manager.cpp @@ -2,7 +2,7 @@ /*! \file resource_manager.cpp ** \verbatim ** Top contributors (to current version): - ** Mathias Preiner, Gereon Kremer, Liana Hadarean + ** Gereon Kremer, Mathias Preiner, Liana Hadarean ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/test/api/CMakeLists.txt b/test/api/CMakeLists.txt index 59df71010..33d5f9c37 100644 --- a/test/api/CMakeLists.txt +++ b/test/api/CMakeLists.txt @@ -1,7 +1,7 @@ ##################### ## CMakeLists.txt ## Top contributors (to current version): -## Aina Niemetz, Andrew V. Jones, Andres Noetzli +## Aina Niemetz, Andrew V. Jones, Makai Mann ## This file is part of the CVC4 project. ## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ## in the top-level source directory and their institutional affiliations. diff --git a/test/api/ouroborous.cpp b/test/api/ouroborous.cpp index efca53ab3..1a23acd29 100644 --- a/test/api/ouroborous.cpp +++ b/test/api/ouroborous.cpp @@ -2,7 +2,7 @@ /*! \file ouroborous.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Aina Niemetz, Tim King + ** Morgan Deters, Andrew Reynolds, Tim King ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/test/api/python/test_grammar.py b/test/api/python/test_grammar.py index 5a0d5101f..54c30b767 100644 --- a/test/api/python/test_grammar.py +++ b/test/api/python/test_grammar.py @@ -1,7 +1,7 @@ ##################### ## test_grammar.py ## Top contributors (to current version): -## Yoni Zohar, Makai Mann +## Yoni Zohar, Makai Mann, Mudathir Mohamed ## This file is part of the CVC4 project. ## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ## in the top-level source directory and their institutional affiliations. diff --git a/test/api/python/test_sort.py b/test/api/python/test_sort.py index cff92ca8d..20ddc6bc1 100644 --- a/test/api/python/test_sort.py +++ b/test/api/python/test_sort.py @@ -1,7 +1,7 @@ ##################### ## test_sort.py ## Top contributors (to current version): -## Makai Mann, Andres Noetzli +## Makai Mann, Andres Noetzli, Mudathir Mohamed ## This file is part of the CVC4 project. ## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ## in the top-level source directory and their institutional affiliations. diff --git a/test/api/python/test_to_python_obj.py b/test/api/python/test_to_python_obj.py index eb15e7469..eeafc4854 100644 --- a/test/api/python/test_to_python_obj.py +++ b/test/api/python/test_to_python_obj.py @@ -1,3 +1,13 @@ +##################### +## test_to_python_obj.py +## Top contributors (to current version): +## Makai Mann, Andres Noetzli, Mudathir Mohamed +## This file is part of the CVC4 project. +## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS +## in the top-level source directory and their institutional affiliations. +## All rights reserved. See the file COPYING in the top-level source +## directory for licensing information. +## from fractions import Fraction import pytest diff --git a/test/api/reset_assertions.cpp b/test/api/reset_assertions.cpp index 2168d053e..0662c7519 100644 --- a/test/api/reset_assertions.cpp +++ b/test/api/reset_assertions.cpp @@ -2,7 +2,7 @@ /*! \file reset_assertions.cpp ** \verbatim ** Top contributors (to current version): - ** Andres Noetzli + ** Andres Noetzli, Mudathir Mohamed ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/test/api/sep_log_api.cpp b/test/api/sep_log_api.cpp index cc20f1ed1..afe264d1f 100644 --- a/test/api/sep_log_api.cpp +++ b/test/api/sep_log_api.cpp @@ -2,7 +2,7 @@ /*! \file sep_log_api.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew V. Jones, Andres Noetzli + ** Andrew V. Jones, Andres Noetzli, Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/test/regress/run_regression.py b/test/regress/run_regression.py index 17aa9e0c6..17aa9e0c6 100755..100644 --- a/test/regress/run_regression.py +++ b/test/regress/run_regression.py diff --git a/test/unit/api/CMakeLists.txt b/test/unit/api/CMakeLists.txt index c6c682365..056f9d891 100644 --- a/test/unit/api/CMakeLists.txt +++ b/test/unit/api/CMakeLists.txt @@ -1,7 +1,7 @@ ##################### ## CMakeLists.txt ## Top contributors (to current version): -## Aina Niemetz, Andres Noetzli, Makai Mann +## Aina Niemetz, Andres Noetzli ## This file is part of the CVC4 project. ## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ## in the top-level source directory and their institutional affiliations. diff --git a/test/unit/api/grammar_black.cpp b/test/unit/api/grammar_black.cpp index 2cfe67825..7e599b135 100644 --- a/test/unit/api/grammar_black.cpp +++ b/test/unit/api/grammar_black.cpp @@ -2,7 +2,7 @@ /*! \file grammar_black.cpp ** \verbatim ** Top contributors (to current version): - ** Abdalrhman Mohamed, Aina Niemetz, Andrew Reynolds + ** Aina Niemetz ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/test/unit/api/result_black.cpp b/test/unit/api/result_black.cpp index 260845495..05427c01d 100644 --- a/test/unit/api/result_black.cpp +++ b/test/unit/api/result_black.cpp @@ -2,7 +2,7 @@ /*! \file result_black.cpp ** \verbatim ** Top contributors (to current version): - ** Aina Niemetz, Andrew Reynolds + ** Aina Niemetz ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/test/unit/api/sort_black.h b/test/unit/api/sort_black.h index e6d712191..baec0f3e9 100644 --- a/test/unit/api/sort_black.h +++ b/test/unit/api/sort_black.h @@ -2,7 +2,7 @@ /*! \file sort_black.h ** \verbatim ** Top contributors (to current version): - ** Aina Niemetz, Andrew Reynolds + ** Aina Niemetz, Andrew Reynolds, Mudathir Mohamed ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/test/unit/api/term_black.cpp b/test/unit/api/term_black.cpp index 71e1c7f6f..8627f6033 100644 --- a/test/unit/api/term_black.cpp +++ b/test/unit/api/term_black.cpp @@ -2,7 +2,7 @@ /*! \file term_black.cpp ** \verbatim ** Top contributors (to current version): - ** Aina Niemetz, Andrew Reynolds, Makai Mann + ** Aina Niemetz, Makai Mann, Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/test/unit/expr/CMakeLists.txt b/test/unit/expr/CMakeLists.txt index 6c0abc4ab..2c698f953 100644 --- a/test/unit/expr/CMakeLists.txt +++ b/test/unit/expr/CMakeLists.txt @@ -1,7 +1,7 @@ ##################### ## CMakeLists.txt ## Top contributors (to current version): -## Aina Niemetz, Yoni Zohar, Alex Ozdemir +## Aina Niemetz ## This file is part of the CVC4 project. ## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ## in the top-level source directory and their institutional affiliations. diff --git a/test/unit/expr/symbol_table_black.h b/test/unit/expr/symbol_table_black.h index 5233c7e09..4aa1e4f65 100644 --- a/test/unit/expr/symbol_table_black.h +++ b/test/unit/expr/symbol_table_black.h @@ -2,7 +2,7 @@ /*! \file symbol_table_black.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Christopher L. Conway, Andres Noetzli + ** Morgan Deters, Christopher L. Conway, Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/test/unit/expr/type_node_white.h b/test/unit/expr/type_node_white.h index 8ac17bbbd..042a7b1da 100644 --- a/test/unit/expr/type_node_white.h +++ b/test/unit/expr/type_node_white.h @@ -2,7 +2,7 @@ /*! \file type_node_white.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Andres Noetzli + ** Morgan Deters, Andrew Reynolds, Andres Noetzli ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/test/unit/main/interactive_shell_black.h b/test/unit/main/interactive_shell_black.h index df6a79bd8..d8cbc19cd 100644 --- a/test/unit/main/interactive_shell_black.h +++ b/test/unit/main/interactive_shell_black.h @@ -2,7 +2,7 @@ /*! \file interactive_shell_black.h ** \verbatim ** Top contributors (to current version): - ** Christopher L. Conway, Aina Niemetz, Andres Noetzli + ** Christopher L. Conway, Aina Niemetz, Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h index ef8f2e3cf..d63f6b029 100644 --- a/test/unit/parser/parser_black.h +++ b/test/unit/parser/parser_black.h @@ -2,7 +2,7 @@ /*! \file parser_black.h ** \verbatim ** Top contributors (to current version): - ** Christopher L. Conway, Morgan Deters, Aina Niemetz + ** Christopher L. Conway, Morgan Deters, Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/test/unit/parser/parser_builder_black.h b/test/unit/parser/parser_builder_black.h index c101542d0..686fc7400 100644 --- a/test/unit/parser/parser_builder_black.h +++ b/test/unit/parser/parser_builder_black.h @@ -2,7 +2,7 @@ /*! \file parser_builder_black.h ** \verbatim ** Top contributors (to current version): - ** Christopher L. Conway, Aina Niemetz, Tim King + ** Christopher L. Conway, Andrew Reynolds, Aina Niemetz ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/test/unit/preprocessing/CMakeLists.txt b/test/unit/preprocessing/CMakeLists.txt index a2381ba90..f2dc0ce79 100644 --- a/test/unit/preprocessing/CMakeLists.txt +++ b/test/unit/preprocessing/CMakeLists.txt @@ -1,7 +1,7 @@ ##################### ## CMakeLists.txt ## Top contributors (to current version): -## Aina Niemetz, Yoni Zohar +## Aina Niemetz ## This file is part of the CVC4 project. ## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ## in the top-level source directory and their institutional affiliations. diff --git a/test/unit/printer/CMakeLists.txt b/test/unit/printer/CMakeLists.txt index 93c241af9..973488a3e 100644 --- a/test/unit/printer/CMakeLists.txt +++ b/test/unit/printer/CMakeLists.txt @@ -1,7 +1,7 @@ ##################### ## CMakeLists.txt ## Top contributors (to current version): -## Andres Noetzli +## Andres Noetzli, Aina Niemetz ## This file is part of the CVC4 project. ## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ## in the top-level source directory and their institutional affiliations. diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt index 334ded2d1..e7528453e 100644 --- a/test/unit/theory/CMakeLists.txt +++ b/test/unit/theory/CMakeLists.txt @@ -1,7 +1,7 @@ ##################### ## CMakeLists.txt ## Top contributors (to current version): -## Aina Niemetz, Andres Noetzli, Andrew Reynolds +## Aina Niemetz ## This file is part of the CVC4 project. ## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ## in the top-level source directory and their institutional affiliations. diff --git a/test/unit/theory/theory_bags_normal_form_white.h b/test/unit/theory/theory_bags_normal_form_white.h index 72fc4284e..eb1676f79 100644 --- a/test/unit/theory/theory_bags_normal_form_white.h +++ b/test/unit/theory/theory_bags_normal_form_white.h @@ -2,10 +2,10 @@ /*! \file theory_bags_normal_form_white.h ** \verbatim ** Top contributors (to current version): - ** Mudathir Mohamed + ** Mudathir Mohamed, Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/test/unit/theory/theory_bags_rewriter_white.h b/test/unit/theory/theory_bags_rewriter_white.h index a58e2cdad..98e3cf887 100644 --- a/test/unit/theory/theory_bags_rewriter_white.h +++ b/test/unit/theory/theory_bags_rewriter_white.h @@ -2,10 +2,10 @@ /*! \file theory_bags_rewriter_white.h ** \verbatim ** Top contributors (to current version): - ** Mudathir Mohamed + ** Mudathir Mohamed, Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/test/unit/theory/theory_bags_type_rules_white.h b/test/unit/theory/theory_bags_type_rules_white.h index 8d1db858d..825e52669 100644 --- a/test/unit/theory/theory_bags_type_rules_white.h +++ b/test/unit/theory/theory_bags_type_rules_white.h @@ -1,11 +1,11 @@ /********************* */ -/*! \file theory_bags_type_rules_black.h +/*! \file theory_bags_type_rules_white.h ** \verbatim ** Top contributors (to current version): - ** Mudathir Mohamed + ** Mudathir Mohamed, Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/test/unit/theory/theory_sets_type_enumerator_white.h b/test/unit/theory/theory_sets_type_enumerator_white.h index 1b5ba1dcb..a100984ba 100644 --- a/test/unit/theory/theory_sets_type_enumerator_white.h +++ b/test/unit/theory/theory_sets_type_enumerator_white.h @@ -2,7 +2,7 @@ /*! \file theory_sets_type_enumerator_white.h ** \verbatim ** Top contributors (to current version): - ** Mudathir Mohamed, Andres Noetzli, Andrew Reynolds + ** Mudathir Mohamed, Andrew Reynolds, Andres Noetzli ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/test/unit/theory/theory_sets_type_rules_white.h b/test/unit/theory/theory_sets_type_rules_white.h index 00b012745..59f8186ac 100644 --- a/test/unit/theory/theory_sets_type_rules_white.h +++ b/test/unit/theory/theory_sets_type_rules_white.h @@ -2,10 +2,10 @@ /*! \file theory_sets_type_rules_white.h ** \verbatim ** Top contributors (to current version): - ** Mudathir Mohamed + ** Mudathir Mohamed, Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** diff --git a/test/unit/theory/theory_strings_skolem_cache_black.h b/test/unit/theory/theory_strings_skolem_cache_black.h index dd70dd5b9..72a9b7e64 100644 --- a/test/unit/theory/theory_strings_skolem_cache_black.h +++ b/test/unit/theory/theory_strings_skolem_cache_black.h @@ -2,7 +2,7 @@ /*! \file theory_strings_skolem_cache_black.h ** \verbatim ** Top contributors (to current version): - ** Andres Noetzli + ** Andres Noetzli, Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/test/unit/theory/theory_white.h b/test/unit/theory/theory_white.h index f69830fd8..9f23dbad6 100644 --- a/test/unit/theory/theory_white.h +++ b/test/unit/theory/theory_white.h @@ -2,7 +2,7 @@ /*! \file theory_white.h ** \verbatim ** Top contributors (to current version): - ** Tim King, Morgan Deters, Clark Barrett + ** Tim King, Andrew Reynolds, Morgan Deters ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/test/unit/util/CMakeLists.txt b/test/unit/util/CMakeLists.txt index 148ae9910..3457578df 100644 --- a/test/unit/util/CMakeLists.txt +++ b/test/unit/util/CMakeLists.txt @@ -1,7 +1,7 @@ ##################### ## CMakeLists.txt ## Top contributors (to current version): -## Aina Niemetz, Gereon Kremer, Andres Noetzli +## Aina Niemetz, Yoni Zohar, Gereon Kremer ## This file is part of the CVC4 project. ## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ## in the top-level source directory and their institutional affiliations. diff --git a/test/unit/util/bitvector_black.h b/test/unit/util/bitvector_black.h index 5b6eecc5f..417410c9e 100644 --- a/test/unit/util/bitvector_black.h +++ b/test/unit/util/bitvector_black.h @@ -2,7 +2,7 @@ /*! \file bitvector_black.h ** \verbatim ** Top contributors (to current version): - ** Andres Noetzli, Christopher L. Conway, Morgan Deters + ** Andres Noetzli, Christopher L. Conway, Aina Niemetz ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. diff --git a/test/unit/util/output_black.h b/test/unit/util/output_black.h index 00580de63..298aad812 100644 --- a/test/unit/util/output_black.h +++ b/test/unit/util/output_black.h @@ -2,7 +2,7 @@ /*! \file output_black.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Tim King, Andres Noetzli + ** Morgan Deters, Tim King, Aina Niemetz ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. |