diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2020-12-02 19:55:00 -0800 |
|---|---|---|
| committer | Aina Niemetz <aina.niemetz@gmail.com> | 2020-12-02 19:55:00 -0800 |
| commit | 92e9feab5f417fbbd3ac07d47fe9b6b49f5c4168 (patch) | |
| tree | c7c533d12e91b68d350d5dcc5e77441a831f69a9 /src/theory | |
| parent | 3a8e2f4e52f4debfb8eb6fb9c49934a66d742ec9 (diff) | |
Update copyright headers.
Diffstat (limited to 'src/theory')
143 files changed, 197 insertions, 180 deletions
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. |