diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2018-06-26 12:34:59 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2018-06-26 12:34:59 -0500 |
| commit | 1d9f4830351c05299392b246292e9498296d7e7f (patch) | |
| tree | 4e8f906272977bb7e12a186ba641d01546218606 /src/theory | |
| parent | e47677a72a1e2638062a2c2adf42081e0e7488b2 (diff) | |
| parent | 48cccffd5fac5cb5ed436ba1457b444185f267fb (diff) | |
Merge branch 'master' of https://github.com/CVC4/CVC4 into sygusComp2018-2
Diffstat (limited to 'src/theory')
378 files changed, 676 insertions, 674 deletions
diff --git a/src/theory/arith/approx_simplex.cpp b/src/theory/arith/approx_simplex.cpp index 07cb6aca6..bc7efdaf7 100644 --- a/src/theory/arith/approx_simplex.cpp +++ b/src/theory/arith/approx_simplex.cpp @@ -2,9 +2,9 @@ /*! \file approx_simplex.cpp ** \verbatim ** Top contributors (to current version): - ** Tim King, Morgan Deters, Paul Meng + ** Tim King, Andres Noetzli, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/approx_simplex.h b/src/theory/arith/approx_simplex.h index eb95190bf..a0982169d 100644 --- a/src/theory/arith/approx_simplex.h +++ b/src/theory/arith/approx_simplex.h @@ -2,9 +2,9 @@ /*! \file approx_simplex.h ** \verbatim ** Top contributors (to current version): - ** Tim King, Morgan Deters, Paul Meng + ** Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/arith_ite_utils.cpp b/src/theory/arith/arith_ite_utils.cpp index c67af2a5d..a683d2bbb 100644 --- a/src/theory/arith/arith_ite_utils.cpp +++ b/src/theory/arith/arith_ite_utils.cpp @@ -2,9 +2,9 @@ /*! \file arith_ite_utils.cpp ** \verbatim ** Top contributors (to current version): - ** Tim King, Morgan Deters, Paul Meng + ** Tim King, Kshitij Bansal ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/arith_ite_utils.h b/src/theory/arith/arith_ite_utils.h index e2d0d2baf..69801919f 100644 --- a/src/theory/arith/arith_ite_utils.h +++ b/src/theory/arith/arith_ite_utils.h @@ -2,9 +2,9 @@ /*! \file arith_ite_utils.h ** \verbatim ** Top contributors (to current version): - ** Tim King, Morgan Deters, Paul Meng + ** Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/arith_msum.cpp b/src/theory/arith/arith_msum.cpp index c56587901..f08b4c0ba 100644 --- a/src/theory/arith/arith_msum.cpp +++ b/src/theory/arith/arith_msum.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/arith_msum.h b/src/theory/arith/arith_msum.h index 652a395cc..195db38c9 100644 --- a/src/theory/arith/arith_msum.h +++ b/src/theory/arith/arith_msum.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index 355aa7b0f..c3327e620 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -2,9 +2,9 @@ /*! \file arith_rewriter.cpp ** \verbatim ** Top contributors (to current version): - ** Tim King, Morgan Deters, Dejan Jovanovic + ** Tim King, Andrew Reynolds, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/arith_rewriter.h b/src/theory/arith/arith_rewriter.h index a4472d6c3..7d137bdfd 100644 --- a/src/theory/arith/arith_rewriter.h +++ b/src/theory/arith/arith_rewriter.h @@ -2,9 +2,9 @@ /*! \file arith_rewriter.h ** \verbatim ** Top contributors (to current version): - ** Tim King, Dejan Jovanovic, Morgan Deters + ** Dejan Jovanovic, Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp index 478f0f94c..ed68df89c 100644 --- a/src/theory/arith/arith_static_learner.cpp +++ b/src/theory/arith/arith_static_learner.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Dejan Jovanovic, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/arith_static_learner.h b/src/theory/arith/arith_static_learner.h index cca4b2285..2318da25d 100644 --- a/src/theory/arith/arith_static_learner.h +++ b/src/theory/arith/arith_static_learner.h @@ -2,9 +2,9 @@ /*! \file arith_static_learner.h ** \verbatim ** Top contributors (to current version): - ** Tim King, Morgan Deters, Paul Meng + ** Tim King, Dejan Jovanovic, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/arith_utilities.h b/src/theory/arith/arith_utilities.h index 30db4ec42..14c7fcefe 100644 --- a/src/theory/arith/arith_utilities.h +++ b/src/theory/arith/arith_utilities.h @@ -2,9 +2,9 @@ /*! \file arith_utilities.h ** \verbatim ** Top contributors (to current version): - ** Tim King, Morgan Deters, Paul Meng + ** Tim King, Andrew Reynolds, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/arithvar.cpp b/src/theory/arith/arithvar.cpp index d63dc6fca..8ac72276d 100644 --- a/src/theory/arith/arithvar.cpp +++ b/src/theory/arith/arithvar.cpp @@ -2,9 +2,9 @@ /*! \file arithvar.cpp ** \verbatim ** Top contributors (to current version): - ** Tim King, Morgan Deters, Paul Meng + ** Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/arithvar.h b/src/theory/arith/arithvar.h index d1f71803f..cb1fb7b5f 100644 --- a/src/theory/arith/arithvar.h +++ b/src/theory/arith/arithvar.h @@ -2,9 +2,9 @@ /*! \file arithvar.h ** \verbatim ** Top contributors (to current version): - ** Tim King, Paul Meng + ** Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/arithvar_node_map.h b/src/theory/arith/arithvar_node_map.h index 62a8301e7..0606eb65d 100644 --- a/src/theory/arith/arithvar_node_map.h +++ b/src/theory/arith/arithvar_node_map.h @@ -2,9 +2,9 @@ /*! \file arithvar_node_map.h ** \verbatim ** Top contributors (to current version): - ** Tim King, Morgan Deters, Paul Meng + ** Tim King, Morgan Deters, Dejan Jovanovic ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/attempt_solution_simplex.cpp b/src/theory/arith/attempt_solution_simplex.cpp index fe6755951..025571650 100644 --- a/src/theory/arith/attempt_solution_simplex.cpp +++ b/src/theory/arith/attempt_solution_simplex.cpp @@ -2,9 +2,9 @@ /*! \file attempt_solution_simplex.cpp ** \verbatim ** Top contributors (to current version): - ** Tim King, Morgan Deters, Paul Meng + ** Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/attempt_solution_simplex.h b/src/theory/arith/attempt_solution_simplex.h index fa65214e7..7e5b41936 100644 --- a/src/theory/arith/attempt_solution_simplex.h +++ b/src/theory/arith/attempt_solution_simplex.h @@ -2,9 +2,9 @@ /*! \file attempt_solution_simplex.h ** \verbatim ** Top contributors (to current version): - ** Tim King, Paul Meng, Morgan Deters + ** Tim King, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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_counts.h b/src/theory/arith/bound_counts.h index 70ddc2bfa..7debbad13 100644 --- a/src/theory/arith/bound_counts.h +++ b/src/theory/arith/bound_counts.h @@ -2,9 +2,9 @@ /*! \file bound_counts.h ** \verbatim ** Top contributors (to current version): - ** Tim King, Morgan Deters, Paul Meng + ** Tim King, Morgan Deters, Clark Barrett ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/callbacks.cpp b/src/theory/arith/callbacks.cpp index 73aa5c34e..86240b949 100644 --- a/src/theory/arith/callbacks.cpp +++ b/src/theory/arith/callbacks.cpp @@ -2,9 +2,9 @@ /*! \file callbacks.cpp ** \verbatim ** Top contributors (to current version): - ** Tim King, Morgan Deters, Paul Meng + ** Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/callbacks.h b/src/theory/arith/callbacks.h index f84550dcc..8b79ff659 100644 --- a/src/theory/arith/callbacks.h +++ b/src/theory/arith/callbacks.h @@ -2,9 +2,9 @@ /*! \file callbacks.h ** \verbatim ** Top contributors (to current version): - ** Tim King, Morgan Deters, Paul Meng + ** Tim King, Mathias Preiner, Clark Barrett ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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 f6e702f5b..d4a59b4b0 100644 --- a/src/theory/arith/congruence_manager.cpp +++ b/src/theory/arith/congruence_manager.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Paul Meng, Dejan Jovanovic ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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.h b/src/theory/arith/congruence_manager.h index 5085dc841..278c79a2f 100644 --- a/src/theory/arith/congruence_manager.h +++ b/src/theory/arith/congruence_manager.h @@ -2,9 +2,9 @@ /*! \file congruence_manager.h ** \verbatim ** Top contributors (to current version): - ** Tim King, Paul Meng, Morgan Deters + ** Tim King, Paul Meng, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/constraint.cpp b/src/theory/arith/constraint.cpp index 15f82d82b..f5c3eac08 100644 --- a/src/theory/arith/constraint.cpp +++ b/src/theory/arith/constraint.cpp @@ -2,9 +2,9 @@ /*! \file constraint.cpp ** \verbatim ** Top contributors (to current version): - ** Tim King, Morgan Deters, Paul Meng + ** Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/constraint.h b/src/theory/arith/constraint.h index 25f838567..5eef9663e 100644 --- a/src/theory/arith/constraint.h +++ b/src/theory/arith/constraint.h @@ -2,9 +2,9 @@ /*! \file constraint.h ** \verbatim ** Top contributors (to current version): - ** Tim King, Paul Meng, Morgan Deters + ** Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/constraint_forward.h b/src/theory/arith/constraint_forward.h index 80a0fa0a4..b08b572be 100644 --- a/src/theory/arith/constraint_forward.h +++ b/src/theory/arith/constraint_forward.h @@ -2,9 +2,9 @@ /*! \file constraint_forward.h ** \verbatim ** Top contributors (to current version): - ** Tim King, Paul Meng + ** Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/cut_log.cpp b/src/theory/arith/cut_log.cpp index 08fe0bc1e..dcdadd76f 100644 --- a/src/theory/arith/cut_log.cpp +++ b/src/theory/arith/cut_log.cpp @@ -2,9 +2,9 @@ /*! \file cut_log.cpp ** \verbatim ** Top contributors (to current version): - ** Tim King, Morgan Deters, Paul Meng + ** Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/cut_log.h b/src/theory/arith/cut_log.h index 7d41666e7..6650e6680 100644 --- a/src/theory/arith/cut_log.h +++ b/src/theory/arith/cut_log.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Morgan Deters, Kshitij Bansal ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/delta_rational.cpp b/src/theory/arith/delta_rational.cpp index 7a94674d6..758f8af4a 100644 --- a/src/theory/arith/delta_rational.cpp +++ b/src/theory/arith/delta_rational.cpp @@ -2,9 +2,9 @@ /*! \file delta_rational.cpp ** \verbatim ** Top contributors (to current version): - ** Tim King, Morgan Deters, Paul Meng + ** Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/delta_rational.h b/src/theory/arith/delta_rational.h index 5e4b2c3a8..9a8e4586e 100644 --- a/src/theory/arith/delta_rational.h +++ b/src/theory/arith/delta_rational.h @@ -2,9 +2,9 @@ /*! \file delta_rational.h ** \verbatim ** Top contributors (to current version): - ** Tim King, Morgan Deters, Dejan Jovanovic + ** Tim King, Dejan Jovanovic, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/dio_solver.cpp b/src/theory/arith/dio_solver.cpp index 744bc769e..718034f62 100644 --- a/src/theory/arith/dio_solver.cpp +++ b/src/theory/arith/dio_solver.cpp @@ -2,9 +2,9 @@ /*! \file dio_solver.cpp ** \verbatim ** Top contributors (to current version): - ** Tim King, Morgan Deters, Paul Meng + ** Tim King, Morgan Deters, Dejan Jovanovic ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/dio_solver.h b/src/theory/arith/dio_solver.h index 367ea8faa..aeb82a82b 100644 --- a/src/theory/arith/dio_solver.h +++ b/src/theory/arith/dio_solver.h @@ -2,9 +2,9 @@ /*! \file dio_solver.h ** \verbatim ** Top contributors (to current version): - ** Tim King, Morgan Deters, Paul Meng + ** Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/dual_simplex.cpp b/src/theory/arith/dual_simplex.cpp index ccab94221..1f855b1dd 100644 --- a/src/theory/arith/dual_simplex.cpp +++ b/src/theory/arith/dual_simplex.cpp @@ -2,9 +2,9 @@ /*! \file dual_simplex.cpp ** \verbatim ** Top contributors (to current version): - ** Tim King, Paul Meng, Morgan Deters + ** Tim King, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/dual_simplex.h b/src/theory/arith/dual_simplex.h index 10d18170e..56eaf9a50 100644 --- a/src/theory/arith/dual_simplex.h +++ b/src/theory/arith/dual_simplex.h @@ -2,9 +2,9 @@ /*! \file dual_simplex.h ** \verbatim ** Top contributors (to current version): - ** Tim King, Paul Meng, Morgan Deters + ** Tim King, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/error_set.cpp b/src/theory/arith/error_set.cpp index 0bd283252..d5b86143d 100644 --- a/src/theory/arith/error_set.cpp +++ b/src/theory/arith/error_set.cpp @@ -2,9 +2,9 @@ /*! \file error_set.cpp ** \verbatim ** Top contributors (to current version): - ** Tim King, Paul Meng, Morgan Deters + ** Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/error_set.h b/src/theory/arith/error_set.h index e09a85aaf..2eb2b60d2 100644 --- a/src/theory/arith/error_set.h +++ b/src/theory/arith/error_set.h @@ -2,9 +2,9 @@ /*! \file error_set.h ** \verbatim ** Top contributors (to current version): - ** Tim King, Paul Meng, Morgan Deters + ** Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/fc_simplex.cpp b/src/theory/arith/fc_simplex.cpp index db40f3580..198c22e77 100644 --- a/src/theory/arith/fc_simplex.cpp +++ b/src/theory/arith/fc_simplex.cpp @@ -2,9 +2,9 @@ /*! \file fc_simplex.cpp ** \verbatim ** Top contributors (to current version): - ** Tim King, Paul Meng, Morgan Deters + ** Tim King, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/fc_simplex.h b/src/theory/arith/fc_simplex.h index a93fa88e8..9fa666f95 100644 --- a/src/theory/arith/fc_simplex.h +++ b/src/theory/arith/fc_simplex.h @@ -2,9 +2,9 @@ /*! \file fc_simplex.h ** \verbatim ** Top contributors (to current version): - ** Tim King, Morgan Deters, Paul Meng + ** Tim King, Morgan Deters, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/infer_bounds.cpp b/src/theory/arith/infer_bounds.cpp index e9a85d7d7..501b3507c 100644 --- a/src/theory/arith/infer_bounds.cpp +++ b/src/theory/arith/infer_bounds.cpp @@ -2,9 +2,9 @@ /*! \file infer_bounds.cpp ** \verbatim ** Top contributors (to current version): - ** Tim King, Paul Meng + ** Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/infer_bounds.h b/src/theory/arith/infer_bounds.h index 720b5704d..8a48cb8bc 100644 --- a/src/theory/arith/infer_bounds.h +++ b/src/theory/arith/infer_bounds.h @@ -2,9 +2,9 @@ /*! \file infer_bounds.h ** \verbatim ** Top contributors (to current version): - ** Tim King, Paul Meng + ** Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/linear_equality.cpp b/src/theory/arith/linear_equality.cpp index c97ed9714..e424c714e 100644 --- a/src/theory/arith/linear_equality.cpp +++ b/src/theory/arith/linear_equality.cpp @@ -2,9 +2,9 @@ /*! \file linear_equality.cpp ** \verbatim ** Top contributors (to current version): - ** Tim King, Paul Meng + ** Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/linear_equality.h b/src/theory/arith/linear_equality.h index 0f2862a72..531b52c3a 100644 --- a/src/theory/arith/linear_equality.h +++ b/src/theory/arith/linear_equality.h @@ -2,9 +2,9 @@ /*! \file linear_equality.h ** \verbatim ** Top contributors (to current version): - ** Tim King, Paul Meng, Clark Barrett + ** Tim King, Mathias Preiner, Clark Barrett ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/matrix.cpp b/src/theory/arith/matrix.cpp index 2817a1dca..5da2ab2f6 100644 --- a/src/theory/arith/matrix.cpp +++ b/src/theory/arith/matrix.cpp @@ -2,9 +2,9 @@ /*! \file matrix.cpp ** \verbatim ** Top contributors (to current version): - ** Tim King, Paul Meng + ** Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/matrix.h b/src/theory/arith/matrix.h index eda5b9dac..ef045ea37 100644 --- a/src/theory/arith/matrix.h +++ b/src/theory/arith/matrix.h @@ -2,9 +2,9 @@ /*! \file matrix.h ** \verbatim ** Top contributors (to current version): - ** Tim King, Paul Meng, Morgan Deters + ** Tim King, Mathias Preiner, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp index fa1c01b88..98c426339 100644 --- a/src/theory/arith/nonlinear_extension.cpp +++ b/src/theory/arith/nonlinear_extension.cpp @@ -2,9 +2,9 @@ /*! \file nonlinear_extension.cpp ** \verbatim ** Top contributors (to current version): - ** Tim King, Andrew Reynolds, Andres Noetzli + ** Andrew Reynolds, Tim King, Aina Niemetz ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/nonlinear_extension.h b/src/theory/arith/nonlinear_extension.h index 08cd570c4..d3698aa94 100644 --- a/src/theory/arith/nonlinear_extension.h +++ b/src/theory/arith/nonlinear_extension.h @@ -2,9 +2,9 @@ /*! \file nonlinear_extension.h ** \verbatim ** Top contributors (to current version): - ** Tim King + ** Andrew Reynolds, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/normal_form.cpp b/src/theory/arith/normal_form.cpp index 76782d8a5..12bf90f2e 100644 --- a/src/theory/arith/normal_form.cpp +++ b/src/theory/arith/normal_form.cpp @@ -2,9 +2,9 @@ /*! \file normal_form.cpp ** \verbatim ** Top contributors (to current version): - ** Tim King, Morgan Deters, Paul Meng + ** Tim King, Andrew Reynolds, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/normal_form.h b/src/theory/arith/normal_form.h index ba740146b..b4d9e9f13 100644 --- a/src/theory/arith/normal_form.h +++ b/src/theory/arith/normal_form.h @@ -2,9 +2,9 @@ /*! \file normal_form.h ** \verbatim ** Top contributors (to current version): - ** Tim King, Morgan Deters, Paul Meng + ** Tim King, Morgan Deters, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/partial_model.cpp b/src/theory/arith/partial_model.cpp index 8d4e8c5f9..4364b730a 100644 --- a/src/theory/arith/partial_model.cpp +++ b/src/theory/arith/partial_model.cpp @@ -2,9 +2,9 @@ /*! \file partial_model.cpp ** \verbatim ** Top contributors (to current version): - ** Tim King, Morgan Deters, Paul Meng + ** Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/partial_model.h b/src/theory/arith/partial_model.h index 47a1c2d42..9e8a51b9f 100644 --- a/src/theory/arith/partial_model.h +++ b/src/theory/arith/partial_model.h @@ -2,9 +2,9 @@ /*! \file partial_model.h ** \verbatim ** Top contributors (to current version): - ** Tim King, Morgan Deters, Paul Meng + ** Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/simplex.cpp b/src/theory/arith/simplex.cpp index a7c5a1ac1..4ee613f4c 100644 --- a/src/theory/arith/simplex.cpp +++ b/src/theory/arith/simplex.cpp @@ -2,9 +2,9 @@ /*! \file simplex.cpp ** \verbatim ** Top contributors (to current version): - ** Tim King, Morgan Deters, Paul Meng + ** Tim King, Andres Noetzli, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/simplex.h b/src/theory/arith/simplex.h index bd983e0bf..477e0c1fe 100644 --- a/src/theory/arith/simplex.h +++ b/src/theory/arith/simplex.h @@ -2,9 +2,9 @@ /*! \file simplex.h ** \verbatim ** Top contributors (to current version): - ** Tim King, Morgan Deters, Paul Meng + ** Tim King, Morgan Deters, Clark Barrett ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/simplex_update.cpp b/src/theory/arith/simplex_update.cpp index e5bcfa612..634d17a55 100644 --- a/src/theory/arith/simplex_update.cpp +++ b/src/theory/arith/simplex_update.cpp @@ -2,9 +2,9 @@ /*! \file simplex_update.cpp ** \verbatim ** Top contributors (to current version): - ** Tim King, Paul Meng + ** Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/simplex_update.h b/src/theory/arith/simplex_update.h index 70c9a5998..f823be36c 100644 --- a/src/theory/arith/simplex_update.h +++ b/src/theory/arith/simplex_update.h @@ -2,9 +2,9 @@ /*! \file simplex_update.h ** \verbatim ** Top contributors (to current version): - ** Tim King, Paul Meng, Morgan Deters + ** Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/soi_simplex.cpp b/src/theory/arith/soi_simplex.cpp index 60c7ed56f..43ea51384 100644 --- a/src/theory/arith/soi_simplex.cpp +++ b/src/theory/arith/soi_simplex.cpp @@ -2,9 +2,9 @@ /*! \file soi_simplex.cpp ** \verbatim ** Top contributors (to current version): - ** Tim King, Morgan Deters, Paul Meng + ** Tim King, Morgan Deters, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/soi_simplex.h b/src/theory/arith/soi_simplex.h index 54a47ac4d..68af680d0 100644 --- a/src/theory/arith/soi_simplex.h +++ b/src/theory/arith/soi_simplex.h @@ -2,9 +2,9 @@ /*! \file soi_simplex.h ** \verbatim ** Top contributors (to current version): - ** Tim King, Paul Meng, Morgan Deters + ** Tim King, Morgan Deters, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/tableau.cpp b/src/theory/arith/tableau.cpp index 080104118..e0f5fc9e3 100644 --- a/src/theory/arith/tableau.cpp +++ b/src/theory/arith/tableau.cpp @@ -2,9 +2,9 @@ /*! \file tableau.cpp ** \verbatim ** Top contributors (to current version): - ** Tim King, Morgan Deters, Paul Meng + ** Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/tableau.h b/src/theory/arith/tableau.h index caf360153..338baea7f 100644 --- a/src/theory/arith/tableau.h +++ b/src/theory/arith/tableau.h @@ -2,9 +2,9 @@ /*! \file tableau.h ** \verbatim ** Top contributors (to current version): - ** Tim King, Morgan Deters, Paul Meng + ** Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/tableau_sizes.cpp b/src/theory/arith/tableau_sizes.cpp index 6d7b2e7da..d7434529e 100644 --- a/src/theory/arith/tableau_sizes.cpp +++ b/src/theory/arith/tableau_sizes.cpp @@ -2,9 +2,9 @@ /*! \file tableau_sizes.cpp ** \verbatim ** Top contributors (to current version): - ** Tim King, Morgan Deters, Paul Meng + ** Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/tableau_sizes.h b/src/theory/arith/tableau_sizes.h index da6f0f828..228ce06b8 100644 --- a/src/theory/arith/tableau_sizes.h +++ b/src/theory/arith/tableau_sizes.h @@ -2,9 +2,9 @@ /*! \file tableau_sizes.h ** \verbatim ** Top contributors (to current version): - ** Tim King, Morgan Deters, Paul Meng + ** Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 1390cbee6..9a36f5eab 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -2,9 +2,9 @@ /*! \file theory_arith.cpp ** \verbatim ** Top contributors (to current version): - ** Tim King, Morgan Deters, Dejan Jovanovic + ** Tim King, Dejan Jovanovic, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/theory_arith.h b/src/theory/arith/theory_arith.h index 4f3a13b4d..195cb1883 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Morgan Deters, Dejan Jovanovic ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 0ae506b25..81bf91992 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Andrew Reynolds, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index af0012304..78cc2ac04 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -2,9 +2,9 @@ /*! \file theory_arith_private.h ** \verbatim ** Top contributors (to current version): - ** Tim King, Martin Brain, Andrew Reynolds + ** Tim King, Andrew Reynolds, Martin Brain ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/theory_arith_private_forward.h b/src/theory/arith/theory_arith_private_forward.h index f52a80e68..4bd242037 100644 --- a/src/theory/arith/theory_arith_private_forward.h +++ b/src/theory/arith/theory_arith_private_forward.h @@ -2,9 +2,9 @@ /*! \file theory_arith_private_forward.h ** \verbatim ** Top contributors (to current version): - ** Tim King, Morgan Deters, Paul Meng + ** Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h index d783882f4..2e998010c 100644 --- a/src/theory/arith/theory_arith_type_rules.h +++ b/src/theory/arith/theory_arith_type_rules.h @@ -2,9 +2,9 @@ /*! \file theory_arith_type_rules.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Dejan Jovanovic, Christopher L. Conway + ** Dejan Jovanovic, Morgan Deters, Christopher L. Conway ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/type_enumerator.h b/src/theory/arith/type_enumerator.h index dad4ad4eb..ab0dff020 100644 --- a/src/theory/arith/type_enumerator.h +++ b/src/theory/arith/type_enumerator.h @@ -2,9 +2,9 @@ /*! \file type_enumerator.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Paul Meng, Tim King + ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/arrays/array_info.cpp b/src/theory/arrays/array_info.cpp index fc86e00de..406ae5329 100644 --- a/src/theory/arrays/array_info.cpp +++ b/src/theory/arrays/array_info.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Morgan Deters, Clark Barrett, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/arrays/array_info.h b/src/theory/arrays/array_info.h index 5955fb4e4..ec0e1765a 100644 --- a/src/theory/arrays/array_info.h +++ b/src/theory/arrays/array_info.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Morgan Deters, Clark Barrett, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/arrays/array_proof_reconstruction.cpp b/src/theory/arrays/array_proof_reconstruction.cpp index 29dfe9b47..e0f3b03be 100644 --- a/src/theory/arrays/array_proof_reconstruction.cpp +++ b/src/theory/arrays/array_proof_reconstruction.cpp @@ -2,9 +2,9 @@ /*! \file array_proof_reconstruction.cpp ** \verbatim ** Top contributors (to current version): - ** Guy Katz + ** Guy Katz, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/arrays/array_proof_reconstruction.h b/src/theory/arrays/array_proof_reconstruction.h index 1b06dc524..7132b2f3e 100644 --- a/src/theory/arrays/array_proof_reconstruction.h +++ b/src/theory/arrays/array_proof_reconstruction.h @@ -2,9 +2,9 @@ /*! \file array_proof_reconstruction.h ** \verbatim ** Top contributors (to current version): - ** Paul Meng + ** Paul Meng, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/arrays/static_fact_manager.cpp b/src/theory/arrays/static_fact_manager.cpp index a3f1ae929..d7758d00c 100644 --- a/src/theory/arrays/static_fact_manager.cpp +++ b/src/theory/arrays/static_fact_manager.cpp @@ -2,9 +2,9 @@ /*! \file static_fact_manager.cpp ** \verbatim ** Top contributors (to current version): - ** Clark Barrett, Paul Meng, Tim King + ** Clark Barrett, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/arrays/static_fact_manager.h b/src/theory/arrays/static_fact_manager.h index deefb02cf..1f3c3d1df 100644 --- a/src/theory/arrays/static_fact_manager.h +++ b/src/theory/arrays/static_fact_manager.h @@ -2,9 +2,9 @@ /*! \file static_fact_manager.h ** \verbatim ** Top contributors (to current version): - ** Clark Barrett, Paul Meng, Morgan Deters + ** Clark Barrett, Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 9a51a1f43..c98c36f13 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Clark Barrett, Morgan Deters, Guy Katz ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 70cb574a8..aca4cbcb9 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -2,9 +2,9 @@ /*! \file theory_arrays.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Clark Barrett, Dejan Jovanovic + ** Morgan Deters, Clark Barrett, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/arrays/theory_arrays_rewriter.cpp b/src/theory/arrays/theory_arrays_rewriter.cpp index c9ceae857..eaf7b5ff9 100644 --- a/src/theory/arrays/theory_arrays_rewriter.cpp +++ b/src/theory/arrays/theory_arrays_rewriter.cpp @@ -2,9 +2,9 @@ /*! \file theory_arrays_rewriter.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Paul Meng + ** Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h index 04d199971..d17c4d4ab 100644 --- a/src/theory/arrays/theory_arrays_rewriter.h +++ b/src/theory/arrays/theory_arrays_rewriter.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Clark Barrett, Morgan Deters, Dejan Jovanovic ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/arrays/theory_arrays_type_rules.h b/src/theory/arrays/theory_arrays_type_rules.h index 85d3683b3..171a03555 100644 --- a/src/theory/arrays/theory_arrays_type_rules.h +++ b/src/theory/arrays/theory_arrays_type_rules.h @@ -2,9 +2,9 @@ /*! \file theory_arrays_type_rules.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Clark Barrett, Paul Meng + ** Morgan Deters, Clark Barrett, Christopher L. Conway ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/arrays/type_enumerator.h b/src/theory/arrays/type_enumerator.h index 2202c69bc..f9a88f2ae 100644 --- a/src/theory/arrays/type_enumerator.h +++ b/src/theory/arrays/type_enumerator.h @@ -2,9 +2,9 @@ /*! \file type_enumerator.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Clark Barrett, Andrew Reynolds + ** Clark Barrett, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/arrays/union_find.cpp b/src/theory/arrays/union_find.cpp index 73bedf6fc..f919f9260 100644 --- a/src/theory/arrays/union_find.cpp +++ b/src/theory/arrays/union_find.cpp @@ -2,9 +2,9 @@ /*! \file union_find.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Paul Meng, Tim King + ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/arrays/union_find.h b/src/theory/arrays/union_find.h index 3028eaf17..617c9a1ba 100644 --- a/src/theory/arrays/union_find.h +++ b/src/theory/arrays/union_find.h @@ -2,9 +2,9 @@ /*! \file union_find.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Paul Meng + ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/assertion.cpp b/src/theory/assertion.cpp index 8c9de809c..bef29131e 100644 --- a/src/theory/assertion.cpp +++ b/src/theory/assertion.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/assertion.h b/src/theory/assertion.h index 2a5e71adc..c9748f8c8 100644 --- a/src/theory/assertion.h +++ b/src/theory/assertion.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/atom_requests.cpp b/src/theory/atom_requests.cpp index 5605a6754..85c7907bb 100644 --- a/src/theory/atom_requests.cpp +++ b/src/theory/atom_requests.cpp @@ -2,9 +2,9 @@ /*! \file atom_requests.cpp ** \verbatim ** Top contributors (to current version): - ** Dejan Jovanovic, Morgan Deters, Paul Meng + ** Dejan Jovanovic, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/atom_requests.h b/src/theory/atom_requests.h index f36d23dc9..678a0f3f0 100644 --- a/src/theory/atom_requests.h +++ b/src/theory/atom_requests.h @@ -2,9 +2,9 @@ /*! \file atom_requests.h ** \verbatim ** Top contributors (to current version): - ** Dejan Jovanovic, Morgan Deters, Paul Meng + ** Dejan Jovanovic, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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 11b6185ab..aa87b65ba 100644 --- a/src/theory/booleans/circuit_propagator.cpp +++ b/src/theory/booleans/circuit_propagator.cpp @@ -2,9 +2,9 @@ /*! \file circuit_propagator.cpp ** \verbatim ** Top contributors (to current version): - ** Dejan Jovanovic, Morgan Deters, Paul Meng + ** Dejan Jovanovic, Morgan Deters, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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.h b/src/theory/booleans/circuit_propagator.h index 7c60505a5..94ea95793 100644 --- a/src/theory/booleans/circuit_propagator.h +++ b/src/theory/booleans/circuit_propagator.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Morgan Deters, Dejan Jovanovic, Clark Barrett ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp index afe673449..3c6801f28 100644 --- a/src/theory/booleans/theory_bool.cpp +++ b/src/theory/booleans/theory_bool.cpp @@ -2,9 +2,9 @@ /*! \file theory_bool.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Dejan Jovanovic, Andrew Reynolds + ** Morgan Deters, Andrew Reynolds, Dejan Jovanovic ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/theory_bool.h b/src/theory/booleans/theory_bool.h index cd9a9f904..b81ed50f1 100644 --- a/src/theory/booleans/theory_bool.h +++ b/src/theory/booleans/theory_bool.h @@ -2,9 +2,9 @@ /*! \file theory_bool.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Paul Meng, Tim King + ** Morgan Deters, Tim King, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp index 8373f636b..28f86da7a 100644 --- a/src/theory/booleans/theory_bool_rewriter.cpp +++ b/src/theory/booleans/theory_bool_rewriter.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Dejan Jovanovic, Kshitij Bansal ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/theory_bool_rewriter.h b/src/theory/booleans/theory_bool_rewriter.h index d5b2aba21..11c7b16a2 100644 --- a/src/theory/booleans/theory_bool_rewriter.h +++ b/src/theory/booleans/theory_bool_rewriter.h @@ -2,9 +2,9 @@ /*! \file theory_bool_rewriter.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Dejan Jovanovic, Paul Meng + ** Dejan Jovanovic, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/theory_bool_type_rules.h b/src/theory/booleans/theory_bool_type_rules.h index 405748324..7498b7de4 100644 --- a/src/theory/booleans/theory_bool_type_rules.h +++ b/src/theory/booleans/theory_bool_type_rules.h @@ -2,9 +2,9 @@ /*! \file theory_bool_type_rules.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Dejan Jovanovic, Christopher L. Conway + ** Dejan Jovanovic, Morgan Deters, Christopher L. Conway ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/type_enumerator.h b/src/theory/booleans/type_enumerator.h index ac0435442..2e00f22ce 100644 --- a/src/theory/booleans/type_enumerator.h +++ b/src/theory/booleans/type_enumerator.h @@ -2,9 +2,9 @@ /*! \file type_enumerator.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Paul Meng, Andrew Reynolds + ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp index 5f3f1c843..ec22eb3f6 100644 --- a/src/theory/builtin/theory_builtin.cpp +++ b/src/theory/builtin/theory_builtin.cpp @@ -2,9 +2,9 @@ /*! \file theory_builtin.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Paul Meng + ** Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h index 14a38660b..c987941f6 100644 --- a/src/theory/builtin/theory_builtin.h +++ b/src/theory/builtin/theory_builtin.h @@ -2,9 +2,9 @@ /*! \file theory_builtin.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Paul Meng, Tim King + ** Morgan Deters, Tim King, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/builtin/theory_builtin_rewriter.cpp b/src/theory/builtin/theory_builtin_rewriter.cpp index b0e3aeb6f..3228d55f6 100644 --- a/src/theory/builtin/theory_builtin_rewriter.cpp +++ b/src/theory/builtin/theory_builtin_rewriter.cpp @@ -2,9 +2,9 @@ /*! \file theory_builtin_rewriter.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Dejan Jovanovic, Paul Meng + ** Andrew Reynolds, Dejan Jovanovic, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/builtin/theory_builtin_rewriter.h b/src/theory/builtin/theory_builtin_rewriter.h index d729e5687..79ae825e9 100644 --- a/src/theory/builtin/theory_builtin_rewriter.h +++ b/src/theory/builtin/theory_builtin_rewriter.h @@ -2,9 +2,9 @@ /*! \file theory_builtin_rewriter.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Dejan Jovanovic, Paul Meng + ** Andrew Reynolds, Dejan Jovanovic, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index 56017f829..bd3e5faa4 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -2,9 +2,9 @@ /*! \file theory_builtin_type_rules.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Dejan Jovanovic, Christopher L. Conway + ** Morgan Deters, Andrew Reynolds, Dejan Jovanovic ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/builtin/type_enumerator.cpp b/src/theory/builtin/type_enumerator.cpp index 6884d41d9..7a088bd8d 100644 --- a/src/theory/builtin/type_enumerator.cpp +++ b/src/theory/builtin/type_enumerator.cpp @@ -2,9 +2,9 @@ /*! \file type_enumerator.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/builtin/type_enumerator.h b/src/theory/builtin/type_enumerator.h index e7258d27a..bea3b7c18 100644 --- a/src/theory/builtin/type_enumerator.h +++ b/src/theory/builtin/type_enumerator.h @@ -2,9 +2,9 @@ /*! \file type_enumerator.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Andrew Reynolds, Paul Meng + ** Andrew Reynolds, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/bv/abstraction.cpp b/src/theory/bv/abstraction.cpp index f0c1d5488..081590810 100644 --- a/src/theory/bv/abstraction.cpp +++ b/src/theory/bv/abstraction.cpp @@ -2,7 +2,7 @@ /*! \file abstraction.cpp ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean, Aina Niemetz, Guy Katz + ** Liana Hadarean, Aina Niemetz, Mathias Preiner ** This file is part of the CVC4 project. ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. @@ -667,7 +667,7 @@ Node AbstractionModule::substituteArguments(TNode signature, TNode apply, unsign } if (signature.getNumChildren() == 0) { - Assert(signature.getKind() != kind::metakind::VARIABLE); + Assert(signature.getMetaKind() != kind::metakind::VARIABLE); seen[signature] = signature; return signature; } diff --git a/src/theory/bv/abstraction.h b/src/theory/bv/abstraction.h index cc78a550a..a6bc5f12f 100644 --- a/src/theory/bv/abstraction.h +++ b/src/theory/bv/abstraction.h @@ -2,9 +2,9 @@ /*! \file abstraction.h ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean, Guy Katz, Tim King + ** Liana Hadarean, Tim King, Guy Katz ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/bv/bitblast/aig_bitblaster.cpp b/src/theory/bv/bitblast/aig_bitblaster.cpp index 80930866f..f2417deb6 100644 --- a/src/theory/bv/bitblast/aig_bitblaster.cpp +++ b/src/theory/bv/bitblast/aig_bitblaster.cpp @@ -2,9 +2,9 @@ /*! \file aig_bitblaster.cpp ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean, Andrew Reynolds, Tim King + ** Liana Hadarean, Mathias Preiner, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/bv/bitblast/aig_bitblaster.h b/src/theory/bv/bitblast/aig_bitblaster.h index dea2d0429..bd624bf92 100644 --- a/src/theory/bv/bitblast/aig_bitblaster.h +++ b/src/theory/bv/bitblast/aig_bitblaster.h @@ -2,7 +2,7 @@ /*! \file aig_bitblaster.h ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean, Tim King, Aina Niemetz + ** Mathias Preiner ** This file is part of the CVC4 project. ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. diff --git a/src/theory/bv/bitblast/bitblast_strategies_template.h b/src/theory/bv/bitblast/bitblast_strategies_template.h index 3c8b7bddc..c081b87cf 100644 --- a/src/theory/bv/bitblast/bitblast_strategies_template.h +++ b/src/theory/bv/bitblast/bitblast_strategies_template.h @@ -2,7 +2,7 @@ /*! \file bitblast_strategies_template.h ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean, Aina Niemetz, Clark Barrett + ** Liana Hadarean, Aina Niemetz, Tim King ** This file is part of the CVC4 project. ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. diff --git a/src/theory/bv/bitblast/bitblast_utils.h b/src/theory/bv/bitblast/bitblast_utils.h index a2991c529..731ffb3dd 100644 --- a/src/theory/bv/bitblast/bitblast_utils.h +++ b/src/theory/bv/bitblast/bitblast_utils.h @@ -2,9 +2,9 @@ /*! \file bitblast_utils.h ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean, Paul Meng, Andrew Reynolds + ** Liana Hadarean, Mathias Preiner, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/bv/bitblast/bitblaster.h b/src/theory/bv/bitblast/bitblaster.h index f9c444b45..9e2dac2f3 100644 --- a/src/theory/bv/bitblast/bitblaster.h +++ b/src/theory/bv/bitblast/bitblaster.h @@ -2,9 +2,9 @@ /*! \file bitblaster.h ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean, Tim King, Clark Barrett + ** Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/bv/bitblast/eager_bitblaster.cpp b/src/theory/bv/bitblast/eager_bitblaster.cpp index 08776e60d..7b12c3465 100644 --- a/src/theory/bv/bitblast/eager_bitblaster.cpp +++ b/src/theory/bv/bitblast/eager_bitblaster.cpp @@ -2,7 +2,7 @@ /*! \file eager_bitblaster.cpp ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean, Tim King, Aina Niemetz + ** Liana Hadarean, Mathias Preiner, Tim King ** This file is part of the CVC4 project. ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. diff --git a/src/theory/bv/bitblast/eager_bitblaster.h b/src/theory/bv/bitblast/eager_bitblaster.h index bea275c67..fbf1a4ddb 100644 --- a/src/theory/bv/bitblast/eager_bitblaster.h +++ b/src/theory/bv/bitblast/eager_bitblaster.h @@ -2,7 +2,7 @@ /*! \file eager_bitblaster.h ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean, Tim King, Aina Niemetz + ** Mathias Preiner, Andres Noetzli ** This file is part of the CVC4 project. ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. diff --git a/src/theory/bv/bitblast/lazy_bitblaster.cpp b/src/theory/bv/bitblast/lazy_bitblaster.cpp index 539d40384..a50916413 100644 --- a/src/theory/bv/bitblast/lazy_bitblaster.cpp +++ b/src/theory/bv/bitblast/lazy_bitblaster.cpp @@ -2,7 +2,7 @@ /*! \file lazy_bitblaster.cpp ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean, Aina Niemetz, Tim King + ** Liana Hadarean, Aina Niemetz, Mathias Preiner ** This file is part of the CVC4 project. ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. diff --git a/src/theory/bv/bitblast/lazy_bitblaster.h b/src/theory/bv/bitblast/lazy_bitblaster.h index 97fef1e50..5e16b743a 100644 --- a/src/theory/bv/bitblast/lazy_bitblaster.h +++ b/src/theory/bv/bitblast/lazy_bitblaster.h @@ -2,7 +2,7 @@ /*! \file lazy_bitblaster.h ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean, Tim King, Aina Niemetz + ** Mathias Preiner ** This file is part of the CVC4 project. ** Copyright (c) 2009-2018 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_eager_solver.cpp b/src/theory/bv/bv_eager_solver.cpp index f1af28d04..27dccfde0 100644 --- a/src/theory/bv/bv_eager_solver.cpp +++ b/src/theory/bv/bv_eager_solver.cpp @@ -2,9 +2,9 @@ /*! \file bv_eager_solver.cpp ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean, Paul Meng, Tim King + ** Liana Hadarean, Tim King, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/bv/bv_eager_solver.h b/src/theory/bv/bv_eager_solver.h index 856de530d..2754bdd3b 100644 --- a/src/theory/bv/bv_eager_solver.h +++ b/src/theory/bv/bv_eager_solver.h @@ -2,9 +2,9 @@ /*! \file bv_eager_solver.h ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean, Paul Meng, Tim King + ** Liana Hadarean, Tim King, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/bv/bv_inequality_graph.cpp b/src/theory/bv/bv_inequality_graph.cpp index 12d415cad..3d1ce4f27 100644 --- a/src/theory/bv/bv_inequality_graph.cpp +++ b/src/theory/bv/bv_inequality_graph.cpp @@ -2,7 +2,7 @@ /*! \file bv_inequality_graph.cpp ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean, Aina Niemetz, Paul Meng + ** Liana Hadarean, Aina Niemetz, Morgan Deters ** This file is part of the CVC4 project. ** Copyright (c) 2009-2018 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_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h index deba84631..e1f2fbf7c 100644 --- a/src/theory/bv/bv_inequality_graph.h +++ b/src/theory/bv/bv_inequality_graph.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Liana Hadarean, Tim King, Clark Barrett ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/bv/bv_quick_check.cpp b/src/theory/bv/bv_quick_check.cpp index 44e87e368..cc007bef4 100644 --- a/src/theory/bv/bv_quick_check.cpp +++ b/src/theory/bv/bv_quick_check.cpp @@ -2,7 +2,7 @@ /*! \file bv_quick_check.cpp ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean, Tim King, Aina Niemetz + ** Liana Hadarean, Tim King, Morgan Deters ** This file is part of the CVC4 project. ** Copyright (c) 2009-2018 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_quick_check.h b/src/theory/bv/bv_quick_check.h index d941d018f..ec4eb9f4f 100644 --- a/src/theory/bv/bv_quick_check.h +++ b/src/theory/bv/bv_quick_check.h @@ -2,9 +2,9 @@ /*! \file bv_quick_check.h ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean, Paul Meng, Morgan Deters + ** Liana Hadarean, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h index 63dd53407..3166401aa 100644 --- a/src/theory/bv/bv_subtheory.h +++ b/src/theory/bv/bv_subtheory.h @@ -2,9 +2,9 @@ /*! \file bv_subtheory.h ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean, Dejan Jovanovic, Andrew Reynolds + ** Liana Hadarean, Tim King, Dejan Jovanovic ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/bv/bv_subtheory_algebraic.h b/src/theory/bv/bv_subtheory_algebraic.h index c963f15d7..09d958f25 100644 --- a/src/theory/bv/bv_subtheory_algebraic.h +++ b/src/theory/bv/bv_subtheory_algebraic.h @@ -2,9 +2,9 @@ /*! \file bv_subtheory_algebraic.h ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean, Paul Meng, Morgan Deters + ** Liana Hadarean, Mathias Preiner, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h index ca9f472c2..350baae41 100644 --- a/src/theory/bv/bv_subtheory_bitblast.h +++ b/src/theory/bv/bv_subtheory_bitblast.h @@ -2,9 +2,9 @@ /*! \file bv_subtheory_bitblast.h ** \verbatim ** Top contributors (to current version): - ** Dejan Jovanovic, Liana Hadarean, Tim King + ** Liana Hadarean, Dejan Jovanovic, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp index 7b12b3d53..d648997cb 100644 --- a/src/theory/bv/bv_subtheory_core.cpp +++ b/src/theory/bv/bv_subtheory_core.cpp @@ -2,7 +2,7 @@ /*! \file bv_subtheory_core.cpp ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean, Andrew Reynolds, Aina Niemetz + ** Liana Hadarean, Aina Niemetz, Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2018 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_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h index 05c9535c3..2ef18e613 100644 --- a/src/theory/bv/bv_subtheory_core.h +++ b/src/theory/bv/bv_subtheory_core.h @@ -2,9 +2,9 @@ /*! \file bv_subtheory_core.h ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean, Andrew Reynolds, Tim King + ** Liana Hadarean, Mathias Preiner, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp index 970b0331b..41ee74e8d 100644 --- a/src/theory/bv/bv_subtheory_inequality.cpp +++ b/src/theory/bv/bv_subtheory_inequality.cpp @@ -2,7 +2,7 @@ /*! \file bv_subtheory_inequality.cpp ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean, Andrew Reynolds, Aina Niemetz + ** Liana Hadarean, Aina Niemetz, Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2018 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_subtheory_inequality.h b/src/theory/bv/bv_subtheory_inequality.h index 620cd075b..06c39754f 100644 --- a/src/theory/bv/bv_subtheory_inequality.h +++ b/src/theory/bv/bv_subtheory_inequality.h @@ -2,9 +2,9 @@ /*! \file bv_subtheory_inequality.h ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean, Andrew Reynolds, Morgan Deters + ** Liana Hadarean, Morgan Deters, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/bv/slicer.h b/src/theory/bv/slicer.h index dc8d333c4..e6ddfb93c 100644 --- a/src/theory/bv/slicer.h +++ b/src/theory/bv/slicer.h @@ -2,9 +2,9 @@ /*! \file slicer.h ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean, Paul Meng, Tim King + ** Liana Hadarean, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 638715ae4..3b434f143 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -2,7 +2,7 @@ /*! \file theory_bv.cpp ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean, Aina Niemetz, Andrew Reynolds + ** Liana Hadarean, Andrew Reynolds, Aina Niemetz ** This file is part of the CVC4 project. ** Copyright (c) 2009-2018 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 603823ff0..c48708126 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -2,9 +2,9 @@ /*! \file theory_bv.h ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean, Morgan Deters, Dejan Jovanovic + ** Liana Hadarean, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h index c6fa42ab0..25f9eccbb 100644 --- a/src/theory/bv/theory_bv_rewrite_rules.h +++ b/src/theory/bv/theory_bv_rewrite_rules.h @@ -2,9 +2,9 @@ /*! \file theory_bv_rewrite_rules.h ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean, Dejan Jovanovic, Morgan Deters + ** Liana Hadarean, Dejan Jovanovic, Clark Barrett ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/bv/theory_bv_rewrite_rules_core.h b/src/theory/bv/theory_bv_rewrite_rules_core.h index 5b8eaea60..34d8cbab1 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_core.h +++ b/src/theory/bv/theory_bv_rewrite_rules_core.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Dejan Jovanovic, Liana Hadarean, Clark Barrett ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index c05e67947..aca44aa37 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -2,9 +2,9 @@ /*! \file theory_bv_rewriter.cpp ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean, Clark Barrett, Morgan Deters + ** Liana Hadarean, Dejan Jovanovic, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h index 4fe4f4708..aa771fc94 100644 --- a/src/theory/bv/theory_bv_rewriter.h +++ b/src/theory/bv/theory_bv_rewriter.h @@ -2,9 +2,9 @@ /*! \file theory_bv_rewriter.h ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean, Morgan Deters, Dejan Jovanovic + ** Liana Hadarean, Dejan Jovanovic, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h index 957d15ec4..817099752 100644 --- a/src/theory/bv/theory_bv_type_rules.h +++ b/src/theory/bv/theory_bv_type_rules.h @@ -2,9 +2,9 @@ /*! \file theory_bv_type_rules.h ** \verbatim ** Top contributors (to current version): - ** Tim King, Dejan Jovanovic, Morgan Deters + ** Dejan Jovanovic, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp index e6d879838..7c5a68259 100644 --- a/src/theory/bv/theory_bv_utils.cpp +++ b/src/theory/bv/theory_bv_utils.cpp @@ -2,7 +2,7 @@ /*! \file theory_bv_utils.cpp ** \verbatim ** Top contributors (to current version): - ** Aina Niemetz, Tim King, Liana Hadarean + ** Aina Niemetz, Tim King, Mathias Preiner ** This file is part of the CVC4 project. ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. diff --git a/src/theory/bv/type_enumerator.h b/src/theory/bv/type_enumerator.h index dd65fc08f..fdf7dfbd3 100644 --- a/src/theory/bv/type_enumerator.h +++ b/src/theory/bv/type_enumerator.h @@ -2,9 +2,9 @@ /*! \file type_enumerator.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Paul Meng, Tim King + ** Morgan Deters, Tim King, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/care_graph.h b/src/theory/care_graph.h index 870d3f4be..d81cd8389 100644 --- a/src/theory/care_graph.h +++ b/src/theory/care_graph.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp index 90f0494d8..443cd0bd0 100644 --- a/src/theory/datatypes/datatypes_rewriter.cpp +++ b/src/theory/datatypes/datatypes_rewriter.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index ed504e6bf..b99c5fb53 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -2,9 +2,9 @@ /*! \file datatypes_rewriter.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, Paul Meng + ** Andrew Reynolds, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp index 0036d4fbc..36f3e987c 100644 --- a/src/theory/datatypes/datatypes_sygus.cpp +++ b/src/theory/datatypes/datatypes_sygus.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/datatypes_sygus.h b/src/theory/datatypes/datatypes_sygus.h index ed39cef18..071fa0ef6 100644 --- a/src/theory/datatypes/datatypes_sygus.h +++ b/src/theory/datatypes/datatypes_sygus.h @@ -2,9 +2,9 @@ /*! \file datatypes_sygus.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Paul Meng, Tim King + ** Andrew Reynolds, Tim King, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 1897ae2b5..e3b48a4da 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index a27fd5543..e3a375b87 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -2,9 +2,9 @@ /*! \file theory_datatypes.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, Tim King + ** Andrew Reynolds, Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h index 94a99d46e..140ebe158 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.h +++ b/src/theory/datatypes/theory_datatypes_type_rules.h @@ -2,9 +2,9 @@ /*! \file theory_datatypes_type_rules.h ** \verbatim ** Top contributors (to current version): - ** Tim King, Morgan Deters, Andrew Reynolds + ** Andrew Reynolds, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/type_enumerator.cpp b/src/theory/datatypes/type_enumerator.cpp index a3d205a12..4a69a9442 100644 --- a/src/theory/datatypes/type_enumerator.cpp +++ b/src/theory/datatypes/type_enumerator.cpp @@ -2,9 +2,9 @@ /*! \file type_enumerator.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King + ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/type_enumerator.h b/src/theory/datatypes/type_enumerator.h index 462d6306e..13d590508 100644 --- a/src/theory/datatypes/type_enumerator.h +++ b/src/theory/datatypes/type_enumerator.h @@ -2,9 +2,9 @@ /*! \file type_enumerator.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, Andres Noetzli + ** Andrew Reynolds, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/example/ecdata.cpp b/src/theory/example/ecdata.cpp index 427146429..4089ad45d 100644 --- a/src/theory/example/ecdata.cpp +++ b/src/theory/example/ecdata.cpp @@ -2,9 +2,9 @@ /*! \file ecdata.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Paul Meng + ** Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/example/ecdata.h b/src/theory/example/ecdata.h index 9c93f4710..7c62f9833 100644 --- a/src/theory/example/ecdata.h +++ b/src/theory/example/ecdata.h @@ -2,9 +2,9 @@ /*! \file ecdata.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Paul Meng + ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/example/theory_uf_tim.cpp b/src/theory/example/theory_uf_tim.cpp index da87058fe..fa329f1d5 100644 --- a/src/theory/example/theory_uf_tim.cpp +++ b/src/theory/example/theory_uf_tim.cpp @@ -2,9 +2,9 @@ /*! \file theory_uf_tim.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Paul Meng + ** Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/example/theory_uf_tim.h b/src/theory/example/theory_uf_tim.h index a62d9fbe5..ccdab9d35 100644 --- a/src/theory/example/theory_uf_tim.h +++ b/src/theory/example/theory_uf_tim.h @@ -2,9 +2,9 @@ /*! \file theory_uf_tim.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Paul Meng + ** Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp index 464aa497e..a82e74a0d 100644 --- a/src/theory/fp/fp_converter.cpp +++ b/src/theory/fp/fp_converter.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Martin Brain ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/fp/fp_converter.h b/src/theory/fp/fp_converter.h index 5a7b839aa..018f3ee66 100644 --- a/src/theory/fp/fp_converter.h +++ b/src/theory/fp/fp_converter.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Martin Brain ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp index af7e0437f..364df3890 100644 --- a/src/theory/fp/theory_fp.cpp +++ b/src/theory/fp/theory_fp.cpp @@ -2,9 +2,9 @@ /*! \file theory_fp.cpp ** \verbatim ** Top contributors (to current version): - ** Martin Brain, Tim King, Paul Meng + ** Martin Brain, Andrew Reynolds, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/fp/theory_fp.h b/src/theory/fp/theory_fp.h index 832fc6442..3d13cc63f 100644 --- a/src/theory/fp/theory_fp.h +++ b/src/theory/fp/theory_fp.h @@ -2,9 +2,9 @@ /*! \file theory_fp.h ** \verbatim ** Top contributors (to current version): - ** Martin Brain, Paul Meng, Tim King + ** Martin Brain, Mathias Preiner, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp index 574f2e0f0..148536126 100644 --- a/src/theory/fp/theory_fp_rewriter.cpp +++ b/src/theory/fp/theory_fp_rewriter.cpp @@ -2,10 +2,10 @@ /*! \file theory_fp_rewriter.cpp ** \verbatim ** Top contributors (to current version): - ** Martin Brain, Paul Meng, Tim King + ** Martin Brain, Clark Barrett, Andrew Reynolds ** Copyright (c) 2013 University of Oxford ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/fp/theory_fp_rewriter.h b/src/theory/fp/theory_fp_rewriter.h index 56492f921..e39a95615 100644 --- a/src/theory/fp/theory_fp_rewriter.h +++ b/src/theory/fp/theory_fp_rewriter.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Martin Brain, Paul Meng ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/fp/theory_fp_type_rules.h b/src/theory/fp/theory_fp_type_rules.h index 9589715d2..7b155aa58 100644 --- a/src/theory/fp/theory_fp_type_rules.h +++ b/src/theory/fp/theory_fp_type_rules.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Martin Brain, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/fp/type_enumerator.h b/src/theory/fp/type_enumerator.h index 4b243c224..96a61f207 100644 --- a/src/theory/fp/type_enumerator.h +++ b/src/theory/fp/type_enumerator.h @@ -1,13 +1,14 @@ /********************* */ /*! \file type_enumerator.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: Martin Brain - ** Minor contributors (to current version): none - ** This file is part of the CVC4 project. + ** Top contributors (to current version): + ** Tim King, Martin Brain ** Copyright (c) 2009-2015 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 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 An enumerator for floating-point numbers. ** diff --git a/src/theory/idl/idl_assertion.cpp b/src/theory/idl/idl_assertion.cpp index 7738c6c2f..8b5758f5a 100644 --- a/src/theory/idl/idl_assertion.cpp +++ b/src/theory/idl/idl_assertion.cpp @@ -2,9 +2,9 @@ /*! \file idl_assertion.cpp ** \verbatim ** Top contributors (to current version): - ** Dejan Jovanovic, Morgan Deters, Paul Meng + ** Dejan Jovanovic, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/idl/idl_assertion.h b/src/theory/idl/idl_assertion.h index e70e2d4b8..6804945f3 100644 --- a/src/theory/idl/idl_assertion.h +++ b/src/theory/idl/idl_assertion.h @@ -2,9 +2,9 @@ /*! \file idl_assertion.h ** \verbatim ** Top contributors (to current version): - ** Dejan Jovanovic, Morgan Deters, Paul Meng + ** Dejan Jovanovic, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/idl/idl_assertion_db.cpp b/src/theory/idl/idl_assertion_db.cpp index 55ef29bbc..150d0814a 100644 --- a/src/theory/idl/idl_assertion_db.cpp +++ b/src/theory/idl/idl_assertion_db.cpp @@ -2,9 +2,9 @@ /*! \file idl_assertion_db.cpp ** \verbatim ** Top contributors (to current version): - ** Dejan Jovanovic, Morgan Deters, Paul Meng + ** Dejan Jovanovic, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/idl/idl_assertion_db.h b/src/theory/idl/idl_assertion_db.h index a89c8e483..8d7edc87c 100644 --- a/src/theory/idl/idl_assertion_db.h +++ b/src/theory/idl/idl_assertion_db.h @@ -2,9 +2,9 @@ /*! \file idl_assertion_db.h ** \verbatim ** Top contributors (to current version): - ** Dejan Jovanovic, Morgan Deters, Paul Meng + ** Dejan Jovanovic, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/idl/idl_model.cpp b/src/theory/idl/idl_model.cpp index 5096c1197..98a7ed7c2 100644 --- a/src/theory/idl/idl_model.cpp +++ b/src/theory/idl/idl_model.cpp @@ -2,9 +2,9 @@ /*! \file idl_model.cpp ** \verbatim ** Top contributors (to current version): - ** Dejan Jovanovic, Morgan Deters, Paul Meng + ** Dejan Jovanovic, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/idl/idl_model.h b/src/theory/idl/idl_model.h index e4a9f05ef..a58c2d79c 100644 --- a/src/theory/idl/idl_model.h +++ b/src/theory/idl/idl_model.h @@ -2,9 +2,9 @@ /*! \file idl_model.h ** \verbatim ** Top contributors (to current version): - ** Dejan Jovanovic, Morgan Deters, Paul Meng + ** Dejan Jovanovic, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/idl/theory_idl.cpp b/src/theory/idl/theory_idl.cpp index 60d04fe4d..ab87cb1a9 100644 --- a/src/theory/idl/theory_idl.cpp +++ b/src/theory/idl/theory_idl.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Dejan Jovanovic, Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/idl/theory_idl.h b/src/theory/idl/theory_idl.h index 7b05fc890..17f19ca4a 100644 --- a/src/theory/idl/theory_idl.h +++ b/src/theory/idl/theory_idl.h @@ -2,9 +2,9 @@ /*! \file theory_idl.h ** \verbatim ** Top contributors (to current version): - ** Dejan Jovanovic, Morgan Deters, Paul Meng + ** Dejan Jovanovic, Mathias Preiner, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/interrupted.h b/src/theory/interrupted.h index d53ee9d54..8ab6f0ba7 100644 --- a/src/theory/interrupted.h +++ b/src/theory/interrupted.h @@ -2,9 +2,9 @@ /*! \file interrupted.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Paul Meng, Tim King + ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/ite_utilities.cpp b/src/theory/ite_utilities.cpp index cf273a88a..40a58cf57 100644 --- a/src/theory/ite_utilities.cpp +++ b/src/theory/ite_utilities.cpp @@ -2,9 +2,9 @@ /*! \file ite_utilities.cpp ** \verbatim ** Top contributors (to current version): - ** Tim King, Morgan Deters, Kshitij Bansal + ** Tim King, Morgan Deters, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/ite_utilities.h b/src/theory/ite_utilities.h index 7fb3eae41..bfce390eb 100644 --- a/src/theory/ite_utilities.h +++ b/src/theory/ite_utilities.h @@ -2,9 +2,9 @@ /*! \file ite_utilities.h ** \verbatim ** Top contributors (to current version): - ** Tim King, Paul Meng, Morgan Deters + ** Tim King, Paul Meng, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/logic_info.cpp b/src/theory/logic_info.cpp index f2c6df0b6..7d41ff5e6 100644 --- a/src/theory/logic_info.cpp +++ b/src/theory/logic_info.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Morgan Deters, Tim King, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/logic_info.h b/src/theory/logic_info.h index 5eac6a3da..2edc049c6 100644 --- a/src/theory/logic_info.h +++ b/src/theory/logic_info.h @@ -2,9 +2,9 @@ /*! \file logic_info.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Tim King, Paul Meng + ** Morgan Deters, Andrew Reynolds, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/output_channel.h b/src/theory/output_channel.h index 317795f0d..fb0a92cc2 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -2,9 +2,9 @@ /*! \file output_channel.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Liana Hadarean, Tim King + ** Morgan Deters, Tim King, Liana Hadarean ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/alpha_equivalence.cpp b/src/theory/quantifiers/alpha_equivalence.cpp index ff32bbcb7..f9b9e909b 100644 --- a/src/theory/quantifiers/alpha_equivalence.cpp +++ b/src/theory/quantifiers/alpha_equivalence.cpp @@ -2,9 +2,9 @@ /*! \file alpha_equivalence.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King + ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/alpha_equivalence.h b/src/theory/quantifiers/alpha_equivalence.h index 3c04393d2..0e48bb349 100644 --- a/src/theory/quantifiers/alpha_equivalence.h +++ b/src/theory/quantifiers/alpha_equivalence.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Paul Meng ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/anti_skolem.cpp b/src/theory/quantifiers/anti_skolem.cpp index 1303b7627..7fa8b2ff3 100644 --- a/src/theory/quantifiers/anti_skolem.cpp +++ b/src/theory/quantifiers/anti_skolem.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/anti_skolem.h b/src/theory/quantifiers/anti_skolem.h index 6967c6c42..162140ff1 100644 --- a/src/theory/quantifiers/anti_skolem.h +++ b/src/theory/quantifiers/anti_skolem.h @@ -2,9 +2,9 @@ /*! \file anti_skolem.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King + ** Andrew Reynolds, Tim King, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/bv_inverter.h b/src/theory/quantifiers/bv_inverter.h index 2d9e04281..ad16a2ed9 100644 --- a/src/theory/quantifiers/bv_inverter.h +++ b/src/theory/quantifiers/bv_inverter.h @@ -2,7 +2,7 @@ /*! \file bv_inverter.h ** \verbatim ** Top contributors (to current version): - ** Mathias Preiner, Andrew Reynolds, Aina Niemetz + ** Andrew Reynolds, Mathias Preiner, Aina Niemetz ** This file is part of the CVC4 project. ** Copyright (c) 2009-2018 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/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index b18ebcdce..102a6327b 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/cegqi/ceg_instantiator.h b/src/theory/quantifiers/cegqi/ceg_instantiator.h index e7deb6a1a..537d8d74f 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.h @@ -2,9 +2,9 @@ /*! \file ceg_instantiator.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King + ** Andrew Reynolds, Tim King, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/cegqi/ceg_t_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp index cf09cfa55..a54382130 100644 --- a/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp @@ -2,9 +2,9 @@ /*! \file ceg_t_instantiator.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Mathias Preiner, Aina Niemetz ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/cegqi/ceg_t_instantiator.h b/src/theory/quantifiers/cegqi/ceg_t_instantiator.h index eee6747ec..306b65cc3 100644 --- a/src/theory/quantifiers/cegqi/ceg_t_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_t_instantiator.h @@ -2,9 +2,9 @@ /*! \file ceg_t_instantiator.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Tim King, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/cegqi/inst_strategy_cbqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp index 678d87156..615968704 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/cegqi/inst_strategy_cbqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h index 3445c3f9f..236904ef2 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h @@ -2,9 +2,9 @@ /*! \file inst_strategy_cbqi.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, Tim King + ** Andrew Reynolds, Tim King, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index 807a7a58c..ad278f8c5 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -2,9 +2,9 @@ /*! \file conjecture_generator.cpp ** \verbatim ** Top contributors (to current version): - ** Clark Barrett, Andrew Reynolds, Tim King + ** Andrew Reynolds, Tim King, Dejan Jovanovic ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h index 8a6339a85..b0363c59b 100644 --- a/src/theory/quantifiers/conjecture_generator.h +++ b/src/theory/quantifiers/conjecture_generator.h @@ -2,9 +2,9 @@ /*! \file conjecture_generator.h ** \verbatim ** Top contributors (to current version): - ** Clark Barrett, Paul Meng, Andrew Reynolds + ** Andrew Reynolds, Mathias Preiner, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/dynamic_rewrite.cpp b/src/theory/quantifiers/dynamic_rewrite.cpp index 00e527aba..352d6892f 100644 --- a/src/theory/quantifiers/dynamic_rewrite.cpp +++ b/src/theory/quantifiers/dynamic_rewrite.cpp @@ -1,10 +1,10 @@ /********************* */ -/*! \file dynamic_rewriter.cpp +/*! \file dynamic_rewrite.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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 @@ -24,8 +24,7 @@ namespace theory { namespace quantifiers { DynamicRewriter::DynamicRewriter(const std::string& name, QuantifiersEngine* qe) - : d_qe(qe), - d_equalityEngine(qe->getUserContext(), "DynamicRewriter::" + name, true), + : d_equalityEngine(qe->getUserContext(), "DynamicRewriter::" + name, true), d_rewrites(qe->getUserContext()) { d_equalityEngine.addFunctionKind(kind::APPLY_UF); diff --git a/src/theory/quantifiers/dynamic_rewrite.h b/src/theory/quantifiers/dynamic_rewrite.h index 56f591470..0c115d8a1 100644 --- a/src/theory/quantifiers/dynamic_rewrite.h +++ b/src/theory/quantifiers/dynamic_rewrite.h @@ -1,10 +1,10 @@ /********************* */ -/*! \file dynamic_rewriter.h +/*! \file dynamic_rewrite.h ** \verbatim ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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 @@ -65,8 +65,6 @@ class DynamicRewriter bool areEqual(Node a, Node b); private: - /** pointer to the quantifiers engine */ - QuantifiersEngine* d_qe; /** index over argument types to function skolems * * The purpose of this trie is to associate a class of interpreted operator diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp index ea5e8592d..96719cc0f 100644 --- a/src/theory/quantifiers/ematching/candidate_generator.cpp +++ b/src/theory/quantifiers/ematching/candidate_generator.cpp @@ -2,9 +2,9 @@ /*! \file candidate_generator.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, Tim King + ** Andrew Reynolds, Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/ematching/candidate_generator.h b/src/theory/quantifiers/ematching/candidate_generator.h index 4662d7c4c..dc188062f 100644 --- a/src/theory/quantifiers/ematching/candidate_generator.h +++ b/src/theory/quantifiers/ematching/candidate_generator.h @@ -2,9 +2,9 @@ /*! \file candidate_generator.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Andrew Reynolds, Clark Barrett + ** Andrew Reynolds, Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp index fad6334b8..2fcfa19d9 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.cpp +++ b/src/theory/quantifiers/ematching/ho_trigger.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/ematching/ho_trigger.h b/src/theory/quantifiers/ematching/ho_trigger.h index 85bb09086..8840c949f 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.h +++ b/src/theory/quantifiers/ematching/ho_trigger.h @@ -2,9 +2,9 @@ /*! \file ho_trigger.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Tim King, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp index 3ceefcd90..6fd9ae418 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp @@ -2,9 +2,9 @@ /*! \file inst_match_generator.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, Tim King + ** Andrew Reynolds, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/ematching/inst_match_generator.h b/src/theory/quantifiers/ematching/inst_match_generator.h index 2e7e3c90c..abf269f3e 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.h +++ b/src/theory/quantifiers/ematching/inst_match_generator.h @@ -2,9 +2,9 @@ /*! \file inst_match_generator.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Andrew Reynolds, Tim King + ** Andrew Reynolds, Tim King, Clark Barrett ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp index c2c1425f0..3f2dc7cc6 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp @@ -2,9 +2,9 @@ /*! \file inst_strategy_e_matching.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, Tim King + ** Andrew Reynolds, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/ematching/inst_strategy_e_matching.h b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h index eba49fa9a..a8d53cf4b 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h @@ -2,9 +2,9 @@ /*! \file inst_strategy_e_matching.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Andrew Reynolds, Tim King + ** Morgan Deters, Andrew Reynolds, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp index bd95b316d..2aa8af53d 100644 --- a/src/theory/quantifiers/ematching/instantiation_engine.cpp +++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/ematching/instantiation_engine.h b/src/theory/quantifiers/ematching/instantiation_engine.h index e4cb986da..c94320b74 100644 --- a/src/theory/quantifiers/ematching/instantiation_engine.h +++ b/src/theory/quantifiers/ematching/instantiation_engine.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp index 3928cf485..1fce68de0 100644 --- a/src/theory/quantifiers/ematching/trigger.cpp +++ b/src/theory/quantifiers/ematching/trigger.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/ematching/trigger.h b/src/theory/quantifiers/ematching/trigger.h index 28d227bf7..bbd7c386b 100644 --- a/src/theory/quantifiers/ematching/trigger.h +++ b/src/theory/quantifiers/ematching/trigger.h @@ -2,9 +2,9 @@ /*! \file trigger.h ** \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-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/equality_infer.cpp b/src/theory/quantifiers/equality_infer.cpp index a5cbef746..f4a4a34a7 100644 --- a/src/theory/quantifiers/equality_infer.cpp +++ b/src/theory/quantifiers/equality_infer.cpp @@ -2,9 +2,9 @@ /*! \file equality_infer.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King + ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/equality_infer.h b/src/theory/quantifiers/equality_infer.h index 5a3f2e4d5..49d208d99 100644 --- a/src/theory/quantifiers/equality_infer.h +++ b/src/theory/quantifiers/equality_infer.h @@ -2,9 +2,9 @@ /*! \file equality_infer.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King + ** Andrew Reynolds, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp index 86878b9ca..1d582f597 100644 --- a/src/theory/quantifiers/equality_query.cpp +++ b/src/theory/quantifiers/equality_query.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/equality_query.h b/src/theory/quantifiers/equality_query.h index 0b28f53c6..a9a3cb185 100644 --- a/src/theory/quantifiers/equality_query.h +++ b/src/theory/quantifiers/equality_query.h @@ -2,9 +2,9 @@ /*! \file equality_query.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp index 4a4cf80ac..48933eff6 100644 --- a/src/theory/quantifiers/extended_rewrite.cpp +++ b/src/theory/quantifiers/extended_rewrite.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/extended_rewrite.h b/src/theory/quantifiers/extended_rewrite.h index 27d030eaf..00228e27c 100644 --- a/src/theory/quantifiers/extended_rewrite.h +++ b/src/theory/quantifiers/extended_rewrite.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index e608b25b3..e844b4eca 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -2,9 +2,9 @@ /*! \file first_order_model.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, Tim King + ** Andrew Reynolds, Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index db2f97b16..cf6ee003d 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -2,9 +2,9 @@ /*! \file first_order_model.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, Paul Meng + ** Andrew Reynolds, Tim King, Paul Meng ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/fmf/ambqi_builder.cpp b/src/theory/quantifiers/fmf/ambqi_builder.cpp index 52ce4407a..5def5fc95 100644 --- a/src/theory/quantifiers/fmf/ambqi_builder.cpp +++ b/src/theory/quantifiers/fmf/ambqi_builder.cpp @@ -2,9 +2,9 @@ /*! \file ambqi_builder.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Andrew Reynolds, Tim King + ** Andrew Reynolds, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/fmf/ambqi_builder.h b/src/theory/quantifiers/fmf/ambqi_builder.h index 914da14b4..b052e0985 100644 --- a/src/theory/quantifiers/fmf/ambqi_builder.h +++ b/src/theory/quantifiers/fmf/ambqi_builder.h @@ -2,9 +2,9 @@ /*! \file ambqi_builder.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Tim King, Andrew Reynolds + ** Andrew Reynolds, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index b493d6a0c..ae1e3df32 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h index 93b6436d5..c6293f1fe 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.h +++ b/src/theory/quantifiers/fmf/bounded_integers.h @@ -2,9 +2,9 @@ /*! \file bounded_integers.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Andrew Reynolds, Tim King + ** Andrew Reynolds, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp index 9e77a31c1..b4e9aa1e9 100644 --- a/src/theory/quantifiers/fmf/full_model_check.cpp +++ b/src/theory/quantifiers/fmf/full_model_check.cpp @@ -2,9 +2,9 @@ /*! \file full_model_check.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Andrew Reynolds, Tim King + ** Andrew Reynolds, Tim King, Kshitij Bansal ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/fmf/full_model_check.h b/src/theory/quantifiers/fmf/full_model_check.h index 852f96e4c..c28910700 100644 --- a/src/theory/quantifiers/fmf/full_model_check.h +++ b/src/theory/quantifiers/fmf/full_model_check.h @@ -2,9 +2,9 @@ /*! \file full_model_check.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Andrew Reynolds, Tim King + ** Andrew Reynolds, Morgan Deters, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp index 055bee231..cc542f0c3 100644 --- a/src/theory/quantifiers/fmf/model_builder.cpp +++ b/src/theory/quantifiers/fmf/model_builder.cpp @@ -2,9 +2,9 @@ /*! \file model_builder.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King + ** Andrew Reynolds, Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/fmf/model_builder.h b/src/theory/quantifiers/fmf/model_builder.h index 5af1e3451..b08537e9f 100644 --- a/src/theory/quantifiers/fmf/model_builder.h +++ b/src/theory/quantifiers/fmf/model_builder.h @@ -2,9 +2,9 @@ /*! \file model_builder.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, Tim King + ** Andrew Reynolds, Tim King, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp index 3f3c21907..b3d9af953 100644 --- a/src/theory/quantifiers/fmf/model_engine.cpp +++ b/src/theory/quantifiers/fmf/model_engine.cpp @@ -2,9 +2,9 @@ /*! \file model_engine.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, Tim King + ** Andrew Reynolds, Morgan Deters, Kshitij Bansal ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/fmf/model_engine.h b/src/theory/quantifiers/fmf/model_engine.h index 6412ea81b..a11115f33 100644 --- a/src/theory/quantifiers/fmf/model_engine.h +++ b/src/theory/quantifiers/fmf/model_engine.h @@ -2,9 +2,9 @@ /*! \file model_engine.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Andrew Reynolds, Tim King + ** Morgan Deters, Andrew Reynolds, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/fun_def_process.cpp b/src/theory/quantifiers/fun_def_process.cpp index 49a19aeda..fcd0838ef 100644 --- a/src/theory/quantifiers/fun_def_process.cpp +++ b/src/theory/quantifiers/fun_def_process.cpp @@ -2,9 +2,9 @@ /*! \file fun_def_process.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Paul Meng + ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/fun_def_process.h b/src/theory/quantifiers/fun_def_process.h index a4e0bdfa3..b59c6199a 100644 --- a/src/theory/quantifiers/fun_def_process.h +++ b/src/theory/quantifiers/fun_def_process.h @@ -2,9 +2,9 @@ /*! \file fun_def_process.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Paul Meng + ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/global_negate.cpp b/src/theory/quantifiers/global_negate.cpp index 01925ec43..0670b5c5b 100644 --- a/src/theory/quantifiers/global_negate.cpp +++ b/src/theory/quantifiers/global_negate.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/global_negate.h b/src/theory/quantifiers/global_negate.h index 814b0014c..f5d92c478 100644 --- a/src/theory/quantifiers/global_negate.h +++ b/src/theory/quantifiers/global_negate.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp index da16010cd..091c3b673 100644 --- a/src/theory/quantifiers/inst_match.cpp +++ b/src/theory/quantifiers/inst_match.cpp @@ -2,9 +2,9 @@ /*! \file inst_match.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, Tim King + ** Andrew Reynolds, Morgan Deters, Clark Barrett ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h index ce438861c..86138feb3 100644 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Morgan Deters, Francois Bobot ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/inst_match_trie.cpp b/src/theory/quantifiers/inst_match_trie.cpp index 12844eacb..aba4a3b5e 100644 --- a/src/theory/quantifiers/inst_match_trie.cpp +++ b/src/theory/quantifiers/inst_match_trie.cpp @@ -1,10 +1,10 @@ /********************* */ -/*! \file inst_match.cpp +/*! \file inst_match_trie.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, Tim King + ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/inst_match_trie.h b/src/theory/quantifiers/inst_match_trie.h index e33bf5997..50df50786 100644 --- a/src/theory/quantifiers/inst_match_trie.h +++ b/src/theory/quantifiers/inst_match_trie.h @@ -1,10 +1,10 @@ /********************* */ -/*! \file inst_match.h +/*! \file inst_match_trie.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, Francois Bobot + ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/inst_propagator.cpp b/src/theory/quantifiers/inst_propagator.cpp index f97413026..392e092b8 100644 --- a/src/theory/quantifiers/inst_propagator.cpp +++ b/src/theory/quantifiers/inst_propagator.cpp @@ -2,9 +2,9 @@ /*! \file inst_propagator.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/inst_propagator.h b/src/theory/quantifiers/inst_propagator.h index e0c72c9fa..dc1bf6908 100644 --- a/src/theory/quantifiers/inst_propagator.h +++ b/src/theory/quantifiers/inst_propagator.h @@ -2,9 +2,9 @@ /*! \file inst_propagator.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp index 743e7ccc8..9d70d0d4b 100644 --- a/src/theory/quantifiers/inst_strategy_enumerative.cpp +++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/inst_strategy_enumerative.h b/src/theory/quantifiers/inst_strategy_enumerative.h index 51c0c1d0c..be0f452e4 100644 --- a/src/theory/quantifiers/inst_strategy_enumerative.h +++ b/src/theory/quantifiers/inst_strategy_enumerative.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index 323776ddb..eab05f454 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h index 18a06dc3d..62e0ddb55 100644 --- a/src/theory/quantifiers/instantiate.h +++ b/src/theory/quantifiers/instantiate.h @@ -2,9 +2,9 @@ /*! \file instantiate.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/lazy_trie.cpp b/src/theory/quantifiers/lazy_trie.cpp index 33d8adaa1..35049b8ba 100644 --- a/src/theory/quantifiers/lazy_trie.cpp +++ b/src/theory/quantifiers/lazy_trie.cpp @@ -2,7 +2,7 @@ /*! \file lazy_trie.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Haniel Barbosa + ** Haniel Barbosa ** This file is part of the CVC4 project. ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. diff --git a/src/theory/quantifiers/lazy_trie.h b/src/theory/quantifiers/lazy_trie.h index 3585247c6..156f1abde 100644 --- a/src/theory/quantifiers/lazy_trie.h +++ b/src/theory/quantifiers/lazy_trie.h @@ -2,7 +2,7 @@ /*! \file lazy_trie.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Haniel Barbosa + ** Haniel Barbosa ** This file is part of the CVC4 project. ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. diff --git a/src/theory/quantifiers/local_theory_ext.cpp b/src/theory/quantifiers/local_theory_ext.cpp index c76d97255..93b220ea9 100644 --- a/src/theory/quantifiers/local_theory_ext.cpp +++ b/src/theory/quantifiers/local_theory_ext.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Paul Meng ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/local_theory_ext.h b/src/theory/quantifiers/local_theory_ext.h index 2390eb40c..63e810645 100644 --- a/src/theory/quantifiers/local_theory_ext.h +++ b/src/theory/quantifiers/local_theory_ext.h @@ -2,9 +2,9 @@ /*! \file local_theory_ext.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King + ** Andrew Reynolds, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp index a90227577..d88f8eec9 100644 --- a/src/theory/quantifiers/macros.cpp +++ b/src/theory/quantifiers/macros.cpp @@ -2,9 +2,9 @@ /*! \file macros.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, Tim King + ** Andrew Reynolds, Tim King, Kshitij Bansal ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/macros.h b/src/theory/quantifiers/macros.h index bd6a96cc0..b36be7aec 100644 --- a/src/theory/quantifiers/macros.h +++ b/src/theory/quantifiers/macros.h @@ -2,9 +2,9 @@ /*! \file macros.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Andrew Reynolds, Tim King + ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index efc2f3064..f7521ff4a 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -2,9 +2,9 @@ /*! \file quant_conflict_find.cpp ** \verbatim ** Top contributors (to current version): - ** Clark Barrett, Andrew Reynolds, Tim King + ** Andrew Reynolds, Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index 77ea530ae..507d929a7 100644 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -2,9 +2,9 @@ /*! \file quant_conflict_find.h ** \verbatim ** Top contributors (to current version): - ** Clark Barrett, Andrew Reynolds, Tim King + ** Andrew Reynolds, Tim King, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/quant_epr.cpp b/src/theory/quantifiers/quant_epr.cpp index 187466aaa..eedea6767 100644 --- a/src/theory/quantifiers/quant_epr.cpp +++ b/src/theory/quantifiers/quant_epr.cpp @@ -2,9 +2,9 @@ /*! \file quant_epr.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, Tim King + ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/quant_epr.h b/src/theory/quantifiers/quant_epr.h index f191da68e..07569a09b 100644 --- a/src/theory/quantifiers/quant_epr.h +++ b/src/theory/quantifiers/quant_epr.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/quant_relevance.cpp b/src/theory/quantifiers/quant_relevance.cpp index 1f814263f..b9e4d0650 100644 --- a/src/theory/quantifiers/quant_relevance.cpp +++ b/src/theory/quantifiers/quant_relevance.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/quant_relevance.h b/src/theory/quantifiers/quant_relevance.h index 0650b1c42..75ae32318 100644 --- a/src/theory/quantifiers/quant_relevance.h +++ b/src/theory/quantifiers/quant_relevance.h @@ -2,9 +2,9 @@ /*! \file quant_relevance.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp index da6b0a6b4..fb5492eb3 100644 --- a/src/theory/quantifiers/quant_split.cpp +++ b/src/theory/quantifiers/quant_split.cpp @@ -2,9 +2,9 @@ /*! \file quant_split.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King + ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/quant_split.h b/src/theory/quantifiers/quant_split.h index 94bfa0f20..6a752fe3f 100644 --- a/src/theory/quantifiers/quant_split.h +++ b/src/theory/quantifiers/quant_split.h @@ -2,9 +2,9 @@ /*! \file quant_split.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King + ** Andrew Reynolds, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index ccc6e99a8..b1b34fb98 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -2,9 +2,9 @@ /*! \file quant_util.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, Tim King + ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index 874baa482..bb3bd68e3 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -2,9 +2,9 @@ /*! \file quant_util.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, Tim King + ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp index 0e8dfc9f4..e8e93dc0f 100644 --- a/src/theory/quantifiers/quantifiers_attributes.cpp +++ b/src/theory/quantifiers/quantifiers_attributes.cpp @@ -2,9 +2,9 @@ /*! \file quantifiers_attributes.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, Paul Meng + ** Andrew Reynolds, Paul Meng, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h index fcb519712..16de5fd2e 100644 --- a/src/theory/quantifiers/quantifiers_attributes.h +++ b/src/theory/quantifiers/quantifiers_attributes.h @@ -2,9 +2,9 @@ /*! \file quantifiers_attributes.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Paul Meng, Andrew Reynolds + ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index c3dcdf6dc..4799de09d 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index 2fbcc2641..bd0192d9e 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -2,9 +2,9 @@ /*! \file quantifiers_rewriter.h ** \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-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp index e38f76994..849e73822 100644 --- a/src/theory/quantifiers/relevant_domain.cpp +++ b/src/theory/quantifiers/relevant_domain.cpp @@ -2,9 +2,9 @@ /*! \file relevant_domain.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, Tim King + ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h index a138e4e21..78fe23890 100644 --- a/src/theory/quantifiers/relevant_domain.h +++ b/src/theory/quantifiers/relevant_domain.h @@ -2,9 +2,9 @@ /*! \file relevant_domain.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Andrew Reynolds, Tim King + ** Andrew Reynolds, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp index 7f78eb049..ed9666d80 100644 --- a/src/theory/quantifiers/rewrite_engine.cpp +++ b/src/theory/quantifiers/rewrite_engine.cpp @@ -2,9 +2,9 @@ /*! \file rewrite_engine.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, Tim King + ** Andrew Reynolds, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/rewrite_engine.h b/src/theory/quantifiers/rewrite_engine.h index 03cf0c996..febcc0126 100644 --- a/src/theory/quantifiers/rewrite_engine.h +++ b/src/theory/quantifiers/rewrite_engine.h @@ -2,9 +2,9 @@ /*! \file rewrite_engine.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Andrew Reynolds, Tim King + ** Andrew Reynolds, Mathias Preiner, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/single_inv_partition.cpp b/src/theory/quantifiers/single_inv_partition.cpp index 0a0dac4ba..40c191ca2 100644 --- a/src/theory/quantifiers/single_inv_partition.cpp +++ b/src/theory/quantifiers/single_inv_partition.cpp @@ -2,9 +2,9 @@ /*! \file single_inv_partition.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King + ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/single_inv_partition.h b/src/theory/quantifiers/single_inv_partition.h index f346285fa..588b1fde8 100644 --- a/src/theory/quantifiers/single_inv_partition.h +++ b/src/theory/quantifiers/single_inv_partition.h @@ -2,9 +2,9 @@ /*! \file single_inv_partition.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King + ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp index 555058d98..2f12c000c 100644 --- a/src/theory/quantifiers/skolemize.cpp +++ b/src/theory/quantifiers/skolemize.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/skolemize.h b/src/theory/quantifiers/skolemize.h index c3fb1da29..5605c8c5f 100644 --- a/src/theory/quantifiers/skolemize.h +++ b/src/theory/quantifiers/skolemize.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/sygus/ce_guided_conjecture.cpp b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp index dfbd5fb3e..e3afd2c6e 100644 --- a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp @@ -2,9 +2,9 @@ /*! \file ce_guided_conjecture.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Tim King, Haniel Barbosa ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/sygus/ce_guided_conjecture.h b/src/theory/quantifiers/sygus/ce_guided_conjecture.h index a874ad048..0b6f0e1a8 100644 --- a/src/theory/quantifiers/sygus/ce_guided_conjecture.h +++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.h @@ -2,9 +2,9 @@ /*! \file ce_guided_conjecture.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King + ** Andrew Reynolds, Tim King, Haniel Barbosa ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/sygus/ce_guided_instantiation.cpp b/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp index 031507c11..f877bcefd 100644 --- a/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/sygus/ce_guided_instantiation.h b/src/theory/quantifiers/sygus/ce_guided_instantiation.h index e461a08d5..502244d25 100644 --- a/src/theory/quantifiers/sygus/ce_guided_instantiation.h +++ b/src/theory/quantifiers/sygus/ce_guided_instantiation.h @@ -2,9 +2,9 @@ /*! \file ce_guided_instantiation.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King + ** Andrew Reynolds, Mathias Preiner, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp index 5fc22b002..9588757fa 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/sygus/ce_guided_single_inv.h b/src/theory/quantifiers/sygus/ce_guided_single_inv.h index e19d749ad..0fa5c1204 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.h +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.h @@ -2,9 +2,9 @@ /*! \file ce_guided_single_inv.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King + ** Andrew Reynolds, Tim King, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/sygus/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp index 5abed96e6..695ef25c2 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp @@ -2,9 +2,9 @@ /*! \file ce_guided_single_inv_sol.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Paul Meng, Tim King + ** Andrew Reynolds, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/sygus/ce_guided_single_inv_sol.h b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h index 4f85fe14f..9059531d5 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h @@ -2,9 +2,9 @@ /*! \file ce_guided_single_inv_sol.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Paul Meng + ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index fcb81ce5f..37ee01370 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -2,9 +2,9 @@ /*! \file cegis.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Haniel Barbosa ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h index 856219b73..f094b9490 100644 --- a/src/theory/quantifiers/sygus/cegis.h +++ b/src/theory/quantifiers/sygus/cegis.h @@ -2,9 +2,9 @@ /*! \file cegis.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Haniel Barbosa, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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 @@ -42,7 +42,7 @@ class Cegis : public SygusModule { public: Cegis(QuantifiersEngine* qe, CegConjecture* p); - ~Cegis() {} + ~Cegis() override {} /** initialize */ virtual bool initialize(Node n, const std::vector<Node>& candidates, diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index 07e4c887d..5ad4cec11 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -2,7 +2,7 @@ /*! \file cegis_unif.cpp ** \verbatim ** Top contributors (to current version): - ** Haniel Barbosa, Andrew Reynolds + ** Andrew Reynolds, Haniel Barbosa ** This file is part of the CVC4 project. ** Copyright (c) 2009-2018 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/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h index a0e5006b9..530f68c8b 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.h +++ b/src/theory/quantifiers/sygus/cegis_unif.h @@ -2,7 +2,7 @@ /*! \file cegis_unif.h ** \verbatim ** Top contributors (to current version): - ** Haniel Barbosa, Andrew Reynolds + ** Andrew Reynolds, Haniel Barbosa, Andres Noetzli ** This file is part of the CVC4 project. ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. @@ -200,7 +200,7 @@ class CegisUnif : public Cegis { public: CegisUnif(QuantifiersEngine* qe, CegConjecture* p); - ~CegisUnif(); + ~CegisUnif() override; /** Retrieves enumerators for constructing solutions * * Non-unification candidates have themselves as enumerators, while for diff --git a/src/theory/quantifiers/sygus/sygus_explain.cpp b/src/theory/quantifiers/sygus/sygus_explain.cpp index a942da909..ddf52001e 100644 --- a/src/theory/quantifiers/sygus/sygus_explain.cpp +++ b/src/theory/quantifiers/sygus/sygus_explain.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/sygus/sygus_explain.h b/src/theory/quantifiers/sygus/sygus_explain.h index aa28d4693..4efc171d3 100644 --- a/src/theory/quantifiers/sygus/sygus_explain.h +++ b/src/theory/quantifiers/sygus/sygus_explain.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index c0f285c7e..efffa046f 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -2,9 +2,9 @@ /*! \file sygus_grammar_cons.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Haniel Barbosa ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/sygus/sygus_grammar_cons.h b/src/theory/quantifiers/sygus/sygus_grammar_cons.h index 9c2d76733..c99c431ea 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/sygus/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp index 435530f46..8a415cc10 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp @@ -2,9 +2,9 @@ /*! \file sygus_grammar_norm.cpp ** \verbatim ** Top contributors (to current version): - ** Haniel Barbosa + ** Haniel Barbosa, Andrew Reynolds, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/sygus/sygus_grammar_norm.h b/src/theory/quantifiers/sygus/sygus_grammar_norm.h index f72a83e5a..a0f81dcf3 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_norm.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.h @@ -2,9 +2,9 @@ /*! \file sygus_grammar_norm.h ** \verbatim ** Top contributors (to current version): - ** Haniel Barbosa + ** Haniel Barbosa, Tim King, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/sygus/sygus_grammar_red.cpp b/src/theory/quantifiers/sygus/sygus_grammar_red.cpp index 939788e4d..24aa74c9e 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_red.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_red.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/sygus/sygus_grammar_red.h b/src/theory/quantifiers/sygus/sygus_grammar_red.h index d0484aa57..ce83402c9 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_red.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_red.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/sygus/sygus_invariance.cpp b/src/theory/quantifiers/sygus/sygus_invariance.cpp index 277a443c5..9f215f9d4 100644 --- a/src/theory/quantifiers/sygus/sygus_invariance.cpp +++ b/src/theory/quantifiers/sygus/sygus_invariance.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/sygus/sygus_invariance.h b/src/theory/quantifiers/sygus/sygus_invariance.h index d9ff98c2a..09b40c2dd 100644 --- a/src/theory/quantifiers/sygus/sygus_invariance.h +++ b/src/theory/quantifiers/sygus/sygus_invariance.h @@ -2,9 +2,9 @@ /*! \file sygus_invariance.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Tim King, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/sygus/sygus_module.cpp b/src/theory/quantifiers/sygus/sygus_module.cpp index 11747830d..b36fe4281 100644 --- a/src/theory/quantifiers/sygus/sygus_module.cpp +++ b/src/theory/quantifiers/sygus/sygus_module.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/sygus/sygus_module.h b/src/theory/quantifiers/sygus/sygus_module.h index b01f8e1d0..52b6aea0a 100644 --- a/src/theory/quantifiers/sygus/sygus_module.h +++ b/src/theory/quantifiers/sygus/sygus_module.h @@ -2,9 +2,9 @@ /*! \file sygus_module.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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 @@ -49,7 +49,7 @@ class SygusModule { public: SygusModule(QuantifiersEngine* qe, CegConjecture* p); - ~SygusModule() {} + virtual ~SygusModule() {} /** initialize * * n is the "base instantiation" of the deep-embedding version of the diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp index 7c7659fde..3061c4035 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.cpp +++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp @@ -1,10 +1,10 @@ /********************* */ -/*! \file ce_guided_pbe.cpp +/*! \file sygus_pbe.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Haniel Barbosa, Aina Niemetz ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/sygus/sygus_pbe.h b/src/theory/quantifiers/sygus/sygus_pbe.h index dc61f459b..49d853248 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.h +++ b/src/theory/quantifiers/sygus/sygus_pbe.h @@ -1,10 +1,10 @@ /********************* */ -/*! \file ce_guided_pbe.h +/*! \file sygus_pbe.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Haniel Barbosa ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/sygus/sygus_process_conj.cpp b/src/theory/quantifiers/sygus/sygus_process_conj.cpp index ef530e722..76e484549 100644 --- a/src/theory/quantifiers/sygus/sygus_process_conj.cpp +++ b/src/theory/quantifiers/sygus/sygus_process_conj.cpp @@ -2,9 +2,9 @@ /*! \file sygus_process_conj.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/sygus/sygus_process_conj.h b/src/theory/quantifiers/sygus/sygus_process_conj.h index 0b9a25532..b16118b2e 100644 --- a/src/theory/quantifiers/sygus/sygus_process_conj.h +++ b/src/theory/quantifiers/sygus/sygus_process_conj.h @@ -2,9 +2,9 @@ /*! \file sygus_process_conj.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/sygus/sygus_unif.cpp b/src/theory/quantifiers/sygus/sygus_unif.cpp index 76ca94e05..d0f156811 100644 --- a/src/theory/quantifiers/sygus/sygus_unif.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif.cpp @@ -2,9 +2,9 @@ /*! \file sygus_unif.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Haniel Barbosa ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/sygus/sygus_unif.h b/src/theory/quantifiers/sygus/sygus_unif.h index a19f8e41b..dd6922351 100644 --- a/src/theory/quantifiers/sygus/sygus_unif.h +++ b/src/theory/quantifiers/sygus/sygus_unif.h @@ -2,9 +2,9 @@ /*! \file sygus_unif.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Haniel Barbosa ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp index 111e76a47..8436dd1b4 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp @@ -2,9 +2,9 @@ /*! \file sygus_unif_io.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Haniel Barbosa ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/sygus/sygus_unif_io.h b/src/theory/quantifiers/sygus/sygus_unif_io.h index bdfe344ca..a499ba284 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.h +++ b/src/theory/quantifiers/sygus/sygus_unif_io.h @@ -2,9 +2,9 @@ /*! \file sygus_unif_io.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Haniel Barbosa ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/sygus/sygus_unif_strat.cpp b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp index f23e4318a..0f14eebac 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp @@ -2,9 +2,9 @@ /*! \file sygus_unif_strat.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Haniel Barbosa ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/sygus/sygus_unif_strat.h b/src/theory/quantifiers/sygus/sygus_unif_strat.h index 7431136ac..eea0be944 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_strat.h +++ b/src/theory/quantifiers/sygus/sygus_unif_strat.h @@ -2,9 +2,9 @@ /*! \file sygus_unif_strat.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Haniel Barbosa, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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 @@ -93,6 +93,8 @@ std::ostream& operator<<(std::ostream& os, StrategyType st); class UnifContext { public: + virtual ~UnifContext() {} + /** Get the current role * * In a particular context when constructing solutions in synthesis by diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index 14941520f..4c1dcc39a 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -2,9 +2,9 @@ /*! \file term_database_sygus.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Haniel Barbosa, Aina Niemetz ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h index a51de1b1f..efb7d162e 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.h +++ b/src/theory/quantifiers/sygus/term_database_sygus.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/sygus_inference.cpp b/src/theory/quantifiers/sygus_inference.cpp index dc6ca56a4..fe5761e03 100644 --- a/src/theory/quantifiers/sygus_inference.cpp +++ b/src/theory/quantifiers/sygus_inference.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/sygus_inference.h b/src/theory/quantifiers/sygus_inference.h index cdd5a1008..414103fc7 100644 --- a/src/theory/quantifiers/sygus_inference.h +++ b/src/theory/quantifiers/sygus_inference.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp index c1daa9288..c290c027a 100644 --- a/src/theory/quantifiers/sygus_sampler.cpp +++ b/src/theory/quantifiers/sygus_sampler.cpp @@ -2,9 +2,9 @@ /*! \file sygus_sampler.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Haniel Barbosa ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/sygus_sampler.h b/src/theory/quantifiers/sygus_sampler.h index 5e0a24dd2..fcd35613b 100644 --- a/src/theory/quantifiers/sygus_sampler.h +++ b/src/theory/quantifiers/sygus_sampler.h @@ -2,9 +2,9 @@ /*! \file sygus_sampler.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Tim King, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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 @@ -278,6 +278,8 @@ class SygusSampler : public LazyTrieEvaluator class NotifyMatch { public: + virtual ~NotifyMatch() {} + /** * A notification that s is equal to n * { vars -> subs }. This function * should return false if we do not wish to be notified of further matches. diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 54c19378a..482acacc2 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -2,9 +2,9 @@ /*! \file term_database.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Francois Bobot, Tim King + ** Andrew Reynolds, Tim King, Francois Bobot ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 3268e79d6..e9dd371df 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/term_enumeration.cpp b/src/theory/quantifiers/term_enumeration.cpp index 67ee88c07..58558d302 100644 --- a/src/theory/quantifiers/term_enumeration.cpp +++ b/src/theory/quantifiers/term_enumeration.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/term_enumeration.h b/src/theory/quantifiers/term_enumeration.h index a96718800..cede77dbe 100644 --- a/src/theory/quantifiers/term_enumeration.h +++ b/src/theory/quantifiers/term_enumeration.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp index 9b04ce9b5..5bf284dff 100644 --- a/src/theory/quantifiers/term_util.cpp +++ b/src/theory/quantifiers/term_util.cpp @@ -2,9 +2,9 @@ /*! \file term_util.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Paul Meng, Yoni Zohar ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h index 2880713af..6a5e33f75 100644 --- a/src/theory/quantifiers/term_util.h +++ b/src/theory/quantifiers/term_util.h @@ -2,9 +2,9 @@ /*! \file term_util.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 79b7d9a99..8cf8a7042 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Morgan Deters, Andrew Reynolds, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index b82dccd73..2eb3f70be 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Morgan Deters, Tim King, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers/theory_quantifiers_type_rules.h b/src/theory/quantifiers/theory_quantifiers_type_rules.h index 16600e006..bac3ca58f 100644 --- a/src/theory/quantifiers/theory_quantifiers_type_rules.h +++ b/src/theory/quantifiers/theory_quantifiers_type_rules.h @@ -2,9 +2,9 @@ /*! \file theory_quantifiers_type_rules.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, Paul Meng + ** Morgan Deters, Andrew Reynolds, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 97e02f2c0..1fa3514c8 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -2,9 +2,9 @@ /*! \file quantifiers_engine.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-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 70a4ede0c..56fe06257 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -2,9 +2,9 @@ /*! \file quantifiers_engine.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, Tim King + ** Andrew Reynolds, Morgan Deters, Haniel Barbosa ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/rep_set.cpp b/src/theory/rep_set.cpp index 04c39c897..7fa22e418 100644 --- a/src/theory/rep_set.cpp +++ b/src/theory/rep_set.cpp @@ -2,9 +2,9 @@ /*! \file rep_set.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, Tim King + ** Andrew Reynolds, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/rep_set.h b/src/theory/rep_set.h index a75918b5a..29cca462a 100644 --- a/src/theory/rep_set.h +++ b/src/theory/rep_set.h @@ -2,9 +2,9 @@ /*! \file rep_set.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Andrew Reynolds, Tim King + ** Andrew Reynolds, Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/rewriter.cpp b/src/theory/rewriter.cpp index d13003581..6319e1196 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -2,9 +2,9 @@ /*! \file rewriter.cpp ** \verbatim ** Top contributors (to current version): - ** Dejan Jovanovic, Morgan Deters, Liana Hadarean + ** Dejan Jovanovic, Liana Hadarean, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/rewriter.h b/src/theory/rewriter.h index ba8b12fb6..eda5dcf26 100644 --- a/src/theory/rewriter.h +++ b/src/theory/rewriter.h @@ -2,9 +2,9 @@ /*! \file rewriter.h ** \verbatim ** Top contributors (to current version): - ** Dejan Jovanovic, Morgan Deters, Paul Meng + ** Dejan Jovanovic, Morgan Deters, Liana Hadarean ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/rewriter_attributes.h b/src/theory/rewriter_attributes.h index 60fa3a417..7fb6dbfaa 100644 --- a/src/theory/rewriter_attributes.h +++ b/src/theory/rewriter_attributes.h @@ -2,9 +2,9 @@ /*! \file rewriter_attributes.h ** \verbatim ** Top contributors (to current version): - ** Dejan Jovanovic, Morgan Deters, Paul Meng + ** Dejan Jovanovic, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/rewriter_tables_template.h b/src/theory/rewriter_tables_template.h index 9ea9a9695..f34972781 100644 --- a/src/theory/rewriter_tables_template.h +++ b/src/theory/rewriter_tables_template.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Dejan Jovanovic, Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index fd64a4ae6..90c033c94 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Tim King, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/sep/theory_sep.h b/src/theory/sep/theory_sep.h index 9f3134f84..df384739d 100644 --- a/src/theory/sep/theory_sep.h +++ b/src/theory/sep/theory_sep.h @@ -2,9 +2,9 @@ /*! \file theory_sep.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Mathias Preiner, Tim King + ** Andrew Reynolds, Tim King, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/sep/theory_sep_rewriter.cpp b/src/theory/sep/theory_sep_rewriter.cpp index 513eada3f..4d0885dc2 100644 --- a/src/theory/sep/theory_sep_rewriter.cpp +++ b/src/theory/sep/theory_sep_rewriter.cpp @@ -2,9 +2,9 @@ /*! \file theory_sep_rewriter.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Mathias Preiner + ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/sep/theory_sep_rewriter.h b/src/theory/sep/theory_sep_rewriter.h index 61b2ee36a..e867bc0e9 100644 --- a/src/theory/sep/theory_sep_rewriter.h +++ b/src/theory/sep/theory_sep_rewriter.h @@ -2,9 +2,9 @@ /*! \file theory_sep_rewriter.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Mathias Preiner + ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/sep/theory_sep_type_rules.h b/src/theory/sep/theory_sep_type_rules.h index 0e0373586..f5a59c41c 100644 --- a/src/theory/sep/theory_sep_type_rules.h +++ b/src/theory/sep/theory_sep_type_rules.h @@ -2,9 +2,9 @@ /*! \file theory_sep_type_rules.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Mathias Preiner + ** Andrew Reynolds, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/sets/normal_form.h b/src/theory/sets/normal_form.h index bb715ff8c..16a32d989 100644 --- a/src/theory/sets/normal_form.h +++ b/src/theory/sets/normal_form.h @@ -2,9 +2,9 @@ /*! \file normal_form.h ** \verbatim ** Top contributors (to current version): - ** Kshitij Bansal, Tim King, Andrew Reynolds + ** Kshitij Bansal, Andrew Reynolds, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/sets/rels_utils.h b/src/theory/sets/rels_utils.h index d179c447e..39175bf0f 100644 --- a/src/theory/sets/rels_utils.h +++ b/src/theory/sets/rels_utils.h @@ -2,9 +2,9 @@ /*! \file rels_utils.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Mathias Preiner + ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp index 9fcf3c089..162ebb757 100644 --- a/src/theory/sets/theory_sets.cpp +++ b/src/theory/sets/theory_sets.cpp @@ -2,9 +2,9 @@ /*! \file theory_sets.cpp ** \verbatim ** Top contributors (to current version): - ** Kshitij Bansal, Andrew Reynolds, Paul Meng + ** Kshitij Bansal, Andrew Reynolds, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/sets/theory_sets.h b/src/theory/sets/theory_sets.h index a246903a1..7ccda3dad 100644 --- a/src/theory/sets/theory_sets.h +++ b/src/theory/sets/theory_sets.h @@ -2,9 +2,9 @@ /*! \file theory_sets.h ** \verbatim ** Top contributors (to current version): - ** Kshitij Bansal, Paul Meng, Andrew Reynolds + ** Kshitij Bansal, Tim King, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 93fca2324..7b5244a04 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Kshitij Bansal, Paul Meng ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index e708ad539..57a7aaf65 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -2,9 +2,9 @@ /*! \file theory_sets_private.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Kshitij Bansal, Paul Meng + ** Andrew Reynolds, Kshitij Bansal, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp index beb5e946c..1637695e2 100644 --- a/src/theory/sets/theory_sets_rels.cpp +++ b/src/theory/sets/theory_sets_rels.cpp @@ -2,9 +2,9 @@ /*! \file theory_sets_rels.cpp ** \verbatim ** Top contributors (to current version): - ** Paul Meng, Andrew Reynolds, Mathias Preiner + ** Paul Meng, Andrew Reynolds, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h index d6e52a308..e2807112d 100644 --- a/src/theory/sets/theory_sets_rels.h +++ b/src/theory/sets/theory_sets_rels.h @@ -2,9 +2,9 @@ /*! \file theory_sets_rels.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Paul Meng, Mathias Preiner + ** Andrew Reynolds, Paul Meng, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp index 084ca6c96..17f001a55 100644 --- a/src/theory/sets/theory_sets_rewriter.cpp +++ b/src/theory/sets/theory_sets_rewriter.cpp @@ -2,9 +2,9 @@ /*! \file theory_sets_rewriter.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Paul Meng, Kshitij Bansal + ** Kshitij Bansal, Andrew Reynolds, Paul Meng ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/sets/theory_sets_rewriter.h b/src/theory/sets/theory_sets_rewriter.h index 5cf0f8e19..c506f19a5 100644 --- a/src/theory/sets/theory_sets_rewriter.h +++ b/src/theory/sets/theory_sets_rewriter.h @@ -2,9 +2,9 @@ /*! \file theory_sets_rewriter.h ** \verbatim ** Top contributors (to current version): - ** Kshitij Bansal, Paul Meng + ** Kshitij Bansal ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/sets/theory_sets_type_enumerator.h b/src/theory/sets/theory_sets_type_enumerator.h index 87a0485ae..65a614f9a 100644 --- a/src/theory/sets/theory_sets_type_enumerator.h +++ b/src/theory/sets/theory_sets_type_enumerator.h @@ -2,9 +2,9 @@ /*! \file theory_sets_type_enumerator.h ** \verbatim ** Top contributors (to current version): - ** Kshitij Bansal, Tim King, Morgan Deters + ** Kshitij Bansal, Tim King, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h index dcac963b0..8cbb62883 100644 --- a/src/theory/sets/theory_sets_type_rules.h +++ b/src/theory/sets/theory_sets_type_rules.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Kshitij Bansal, Andrew Reynolds, Paul Meng ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp index 0b4deafb5..ca10314e8 100644 --- a/src/theory/shared_terms_database.cpp +++ b/src/theory/shared_terms_database.cpp @@ -2,9 +2,9 @@ /*! \file shared_terms_database.cpp ** \verbatim ** Top contributors (to current version): - ** Dejan Jovanovic, Morgan Deters, Clark Barrett + ** Dejan Jovanovic, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/shared_terms_database.h b/src/theory/shared_terms_database.h index bc4db97ee..5389c021f 100644 --- a/src/theory/shared_terms_database.h +++ b/src/theory/shared_terms_database.h @@ -2,9 +2,9 @@ /*! \file shared_terms_database.h ** \verbatim ** Top contributors (to current version): - ** Dejan Jovanovic, Morgan Deters, Andrew Reynolds + ** Dejan Jovanovic, Morgan Deters, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/sort_inference.cpp b/src/theory/sort_inference.cpp index 7a059771f..96e1e3a38 100644 --- a/src/theory/sort_inference.cpp +++ b/src/theory/sort_inference.cpp @@ -2,9 +2,9 @@ /*! \file sort_inference.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Paul Meng, Morgan Deters + ** Andrew Reynolds, Paul Meng, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/sort_inference.h b/src/theory/sort_inference.h index c4d898dac..6daf6157a 100644 --- a/src/theory/sort_inference.h +++ b/src/theory/sort_inference.h @@ -2,9 +2,9 @@ /*! \file sort_inference.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Andrew Reynolds, Paul Meng + ** Andrew Reynolds, Paul Meng, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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_operation.cpp b/src/theory/strings/regexp_operation.cpp index f9db44102..0eccc72c7 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -2,9 +2,9 @@ /*! \file regexp_operation.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Tianyi Liang, Andrew Reynolds + ** Tianyi Liang, Tim King, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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_operation.h b/src/theory/strings/regexp_operation.h index 4a0ce150c..04ac11549 100644 --- a/src/theory/strings/regexp_operation.h +++ b/src/theory/strings/regexp_operation.h @@ -2,9 +2,9 @@ /*! \file regexp_operation.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Tianyi Liang, Tim King + ** Tianyi Liang, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index cd99a0d33..e81968843 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -2,9 +2,9 @@ /*! \file theory_strings.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tianyi Liang, Tim King + ** Andrew Reynolds, Tianyi Liang, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/theory_strings.h b/src/theory/strings/theory_strings.h index bc60eecdf..6e638e445 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -2,9 +2,9 @@ /*! \file theory_strings.h ** \verbatim ** Top contributors (to current version): - ** Tianyi Liang, Andrew Reynolds, Tim King + ** Andrew Reynolds, Tianyi Liang, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index fac7fccf2..dfab0dd83 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -2,9 +2,9 @@ /*! \file theory_strings_preprocess.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tianyi Liang, Morgan Deters + ** Andrew Reynolds, Tianyi Liang, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h index d342cba72..78e92cd51 100644 --- a/src/theory/strings/theory_strings_preprocess.h +++ b/src/theory/strings/theory_strings_preprocess.h @@ -2,9 +2,9 @@ /*! \file theory_strings_preprocess.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Andrew Reynolds, Tim King + ** Tianyi Liang, Andrew Reynolds, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index fa706b245..f0fc939a1 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -2,9 +2,9 @@ /*! \file theory_strings_rewriter.cpp ** \verbatim ** Top contributors (to current version): - ** Tianyi Liang, Andrew Reynolds, Tim King + ** Andrew Reynolds, Tianyi Liang, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/theory_strings_rewriter.h b/src/theory/strings/theory_strings_rewriter.h index 59842dd53..74d219e50 100644 --- a/src/theory/strings/theory_strings_rewriter.h +++ b/src/theory/strings/theory_strings_rewriter.h @@ -2,9 +2,9 @@ /*! \file theory_strings_rewriter.h ** \verbatim ** Top contributors (to current version): - ** Tianyi Liang, Andrew Reynolds, Tim King + ** Andrew Reynolds, Andres Noetzli, Tianyi Liang ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h index e9e87f29a..a9ced55f3 100644 --- a/src/theory/strings/theory_strings_type_rules.h +++ b/src/theory/strings/theory_strings_type_rules.h @@ -2,9 +2,9 @@ /*! \file theory_strings_type_rules.h ** \verbatim ** Top contributors (to current version): - ** Tianyi Liang, Paul Meng, Morgan Deters + ** Tianyi Liang, Tim King, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/type_enumerator.h b/src/theory/strings/type_enumerator.h index b1904f53f..30d6c798e 100644 --- a/src/theory/strings/type_enumerator.h +++ b/src/theory/strings/type_enumerator.h @@ -2,9 +2,9 @@ /*! \file type_enumerator.h ** \verbatim ** Top contributors (to current version): - ** Tianyi Liang, Paul Meng, Andres Noetzli + ** Tianyi Liang, Tim King, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/substitutions.cpp b/src/theory/substitutions.cpp index ffb1cd1cb..2585d1ee3 100644 --- a/src/theory/substitutions.cpp +++ b/src/theory/substitutions.cpp @@ -2,9 +2,9 @@ /*! \file substitutions.cpp ** \verbatim ** Top contributors (to current version): - ** Clark Barrett, Dejan Jovanovic, Morgan Deters + ** Dejan Jovanovic, Clark Barrett, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/substitutions.h b/src/theory/substitutions.h index 2a2531887..6d6875ba3 100644 --- a/src/theory/substitutions.h +++ b/src/theory/substitutions.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Morgan Deters, Dejan Jovanovic, Clark Barrett ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp index eae5578cf..fdab93375 100644 --- a/src/theory/term_registration_visitor.cpp +++ b/src/theory/term_registration_visitor.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Dejan Jovanovic, Andrew Reynolds, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/term_registration_visitor.h b/src/theory/term_registration_visitor.h index 2a84a7995..b12cef064 100644 --- a/src/theory/term_registration_visitor.h +++ b/src/theory/term_registration_visitor.h @@ -2,9 +2,9 @@ /*! \file term_registration_visitor.h ** \verbatim ** Top contributors (to current version): - ** Dejan Jovanovic, Morgan Deters, Paul Meng + ** Dejan Jovanovic, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/theory.cpp b/src/theory/theory.cpp index 34d16eb61..584ccfe00 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Andrew Reynolds, Dejan Jovanovic ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/theory.h b/src/theory/theory.h index 5a8e56378..f5bf068d2 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Morgan Deters, Dejan Jovanovic, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/theory_engine.h b/src/theory/theory_engine.h index 8926e0593..25520c1cc 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -2,9 +2,9 @@ /*! \file theory_engine.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Dejan Jovanovic, Andrew Reynolds + ** Dejan Jovanovic, Morgan Deters, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/theory_model.cpp b/src/theory/theory_model.cpp index 0258e65cc..42818d581 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -2,9 +2,9 @@ /*! \file theory_model.cpp ** \verbatim ** Top contributors (to current version): - ** Clark Barrett, Andrew Reynolds, Morgan Deters + ** Andrew Reynolds, Clark Barrett, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/theory_model.h b/src/theory/theory_model.h index cee39b542..ac0d686de 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -2,9 +2,9 @@ /*! \file theory_model.h ** \verbatim ** Top contributors (to current version): - ** Clark Barrett, Morgan Deters, Andrew Reynolds + ** Andrew Reynolds, Tim King, Clark Barrett ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp index 5024d17ac..bcc4f7eaf 100644 --- a/src/theory/theory_model_builder.cpp +++ b/src/theory/theory_model_builder.cpp @@ -2,9 +2,9 @@ /*! \file theory_model_builder.cpp ** \verbatim ** Top contributors (to current version): - ** Clark Barrett, Andrew Reynolds, Morgan Deters + ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/theory_model_builder.h b/src/theory/theory_model_builder.h index 5b4a2d983..68e8c6b49 100644 --- a/src/theory/theory_model_builder.h +++ b/src/theory/theory_model_builder.h @@ -1,10 +1,10 @@ /********************* */ -/*! \file theory_model.h +/*! \file theory_model_builder.h ** \verbatim ** Top contributors (to current version): - ** Clark Barrett, Morgan Deters, Andrew Reynolds + ** Andrew Reynolds, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/theory_registrar.h b/src/theory/theory_registrar.h index 2514ccce0..10b90e522 100644 --- a/src/theory/theory_registrar.h +++ b/src/theory/theory_registrar.h @@ -2,9 +2,9 @@ /*! \file theory_registrar.h ** \verbatim ** Top contributors (to current version): - ** Tim King, Morgan Deters, Paul Meng + ** Tim King, Liana Hadarean, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/theory_test_utils.h b/src/theory/theory_test_utils.h index 8c2355cf4..8ebb367ab 100644 --- a/src/theory/theory_test_utils.h +++ b/src/theory/theory_test_utils.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Morgan Deters, Liana Hadarean ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/theory_traits_template.h b/src/theory/theory_traits_template.h index 5fbf10e93..e046da408 100644 --- a/src/theory/theory_traits_template.h +++ b/src/theory/theory_traits_template.h @@ -2,9 +2,9 @@ /*! \file theory_traits_template.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Dejan Jovanovic, Paul Meng + ** Dejan Jovanovic, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/type_enumerator.h b/src/theory/type_enumerator.h index 736a65ade..58961646c 100644 --- a/src/theory/type_enumerator.h +++ b/src/theory/type_enumerator.h @@ -2,9 +2,9 @@ /*! \file type_enumerator.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Andrew Reynolds, Tim King + ** Morgan Deters, Tim King, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/type_enumerator_template.cpp b/src/theory/type_enumerator_template.cpp index 3daf449fb..14f3e9e87 100644 --- a/src/theory/type_enumerator_template.cpp +++ b/src/theory/type_enumerator_template.cpp @@ -2,9 +2,9 @@ /*! \file type_enumerator_template.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Paul Meng, Tim King + ** Morgan Deters, Tim King, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/type_set.cpp b/src/theory/type_set.cpp index e7caa667b..95c672f69 100644 --- a/src/theory/type_set.cpp +++ b/src/theory/type_set.cpp @@ -2,9 +2,9 @@ /*! \file type_set.cpp ** \verbatim ** Top contributors (to current version): - ** Clark Barrett, Andrew Reynolds, Morgan Deters + ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/type_set.h b/src/theory/type_set.h index 2d9be97be..633c8b04d 100644 --- a/src/theory/type_set.h +++ b/src/theory/type_set.h @@ -2,9 +2,9 @@ /*! \file type_set.h ** \verbatim ** Top contributors (to current version): - ** Clark Barrett, Morgan Deters, Andrew Reynolds + ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index a9142c4ef..bd2fe9f9f 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Dejan Jovanovic, Guy Katz, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 2d757cb28..15abf7251 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Dejan Jovanovic, Morgan Deters, Guy Katz ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/uf/equality_engine_types.h b/src/theory/uf/equality_engine_types.h index 7cf25e8f6..724ab423c 100644 --- a/src/theory/uf/equality_engine_types.h +++ b/src/theory/uf/equality_engine_types.h @@ -2,9 +2,9 @@ /*! \file equality_engine_types.h ** \verbatim ** Top contributors (to current version): - ** Dejan Jovanovic, Andrew Reynolds, Paul Meng + ** Dejan Jovanovic, Andres Noetzli, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/uf/symmetry_breaker.cpp b/src/theory/uf/symmetry_breaker.cpp index 8a1c30ba6..0313fabab 100644 --- a/src/theory/uf/symmetry_breaker.cpp +++ b/src/theory/uf/symmetry_breaker.cpp @@ -2,9 +2,9 @@ /*! \file symmetry_breaker.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Liana Hadarean, Paul Meng + ** Morgan Deters, Liana Hadarean, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/uf/symmetry_breaker.h b/src/theory/uf/symmetry_breaker.h index bc729bcbf..434ddd93b 100644 --- a/src/theory/uf/symmetry_breaker.h +++ b/src/theory/uf/symmetry_breaker.h @@ -2,9 +2,9 @@ /*! \file symmetry_breaker.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Liana Hadarean, Paul Meng + ** Morgan Deters, Liana Hadarean, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 851f43582..653b89d7b 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -2,9 +2,9 @@ /*! \file theory_uf.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Andrew Reynolds, Dejan Jovanovic + ** Andrew Reynolds, Morgan Deters, Dejan Jovanovic ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 790968360..9221f64ac 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -2,9 +2,9 @@ /*! \file theory_uf.h ** \verbatim ** Top contributors (to current version): - ** Dejan Jovanovic, Morgan Deters, Tim King + ** Andrew Reynolds, Dejan Jovanovic, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp index b524f90c4..8c994217d 100644 --- a/src/theory/uf/theory_uf_model.cpp +++ b/src/theory/uf/theory_uf_model.cpp @@ -2,9 +2,9 @@ /*! \file theory_uf_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-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/uf/theory_uf_model.h b/src/theory/uf/theory_uf_model.h index 9cfffed16..0fc0421b6 100644 --- a/src/theory/uf/theory_uf_model.h +++ b/src/theory/uf/theory_uf_model.h @@ -2,9 +2,9 @@ /*! \file theory_uf_model.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Andrew Reynolds, Paul Meng + ** Andrew Reynolds, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/uf/theory_uf_rewriter.h b/src/theory/uf/theory_uf_rewriter.h index eff46d23a..3eb59e5fc 100644 --- a/src/theory/uf/theory_uf_rewriter.h +++ b/src/theory/uf/theory_uf_rewriter.h @@ -2,9 +2,9 @@ /*! \file theory_uf_rewriter.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Dejan Jovanovic, Paul Meng + ** Andrew Reynolds, Morgan Deters, Dejan Jovanovic ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index 0e3f9c7a2..6161710f2 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h index ecbfd9a87..5108e7ba1 100644 --- a/src/theory/uf/theory_uf_strong_solver.h +++ b/src/theory/uf/theory_uf_strong_solver.h @@ -2,9 +2,9 @@ /*! \file theory_uf_strong_solver.h ** \verbatim ** Top contributors (to current version): - ** Tim King, Andrew Reynolds, Morgan Deters + ** Morgan Deters, Andrew Reynolds, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h index e0e199288..2dbfae388 100644 --- a/src/theory/uf/theory_uf_type_rules.h +++ b/src/theory/uf/theory_uf_type_rules.h @@ -2,9 +2,9 @@ /*! \file theory_uf_type_rules.h ** \verbatim ** Top contributors (to current version): - ** Tim King, Morgan Deters, Andrew Reynolds + ** Andrew Reynolds, Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/unconstrained_simplifier.cpp b/src/theory/unconstrained_simplifier.cpp index 6c2c791cf..41529760b 100644 --- a/src/theory/unconstrained_simplifier.cpp +++ b/src/theory/unconstrained_simplifier.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Clark Barrett, Tim King, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/unconstrained_simplifier.h b/src/theory/unconstrained_simplifier.h index 04c32f408..b13311e2a 100644 --- a/src/theory/unconstrained_simplifier.h +++ b/src/theory/unconstrained_simplifier.h @@ -2,9 +2,9 @@ /*! \file unconstrained_simplifier.h ** \verbatim ** Top contributors (to current version): - ** Clark Barrett, Paul Meng, Tim King + ** Clark Barrett, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/valuation.cpp b/src/theory/valuation.cpp index 0056fb22f..62b3fc196 100644 --- a/src/theory/valuation.cpp +++ b/src/theory/valuation.cpp @@ -2,9 +2,9 @@ /*! \file valuation.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Dejan Jovanovic, Andrew Reynolds + ** Dejan Jovanovic, Morgan Deters, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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/valuation.h b/src/theory/valuation.h index 160a7b970..93b33cfdf 100644 --- a/src/theory/valuation.h +++ b/src/theory/valuation.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Morgan Deters, Dejan Jovanovic, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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 |