Update copyright headers to 2021. (#6081)

8 files changed, 26 insertions, 25 deletions

diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp
index 036e1c798..60d229215 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, Mathias Preiner, Aina Niemetz
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their 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 8b5f7905f..8f02cc115 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, Mathias Preiner, Aina Niemetz
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their 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 e9b59fdae..c783620a7 100644
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Martin Brain, Andrew Reynolds, Andres Noetzli
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their 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 bd6e70ff1..2283756f6 100644
--- a/src/theory/fp/theory_fp.h
+++ b/src/theory/fp/theory_fp.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Andrew Reynolds, Martin Brain, Aina Niemetz
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their 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 763ca662c..d4d47731d 100644
--- a/src/theory/fp/theory_fp_rewriter.cpp
+++ b/src/theory/fp/theory_fp_rewriter.cpp
@@ -5,29 +5,30 @@
  **   Martin Brain, Andres Noetzli, Aina Niemetz
  ** Copyright (c) 2013  University of Oxford
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
  ** in the top-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 [[ Rewrite rules for floating point theories. ]]
+ ** \brief Rewrite rules for floating point theories.
  **
- ** \todo [[ Single argument constant propagate / simplify
-             Push negations through arithmetic operators (include max and min? maybe not due to +0/-0)
- **          classifications to normal tests (maybe)
- **          (= x (fp.neg x)) --> (isNaN x)
- **          (fp.eq x (fp.neg x)) --> (isZero x)   (previous and reorganise should be sufficient)
- **          (fp.eq x const) --> various = depending on const
- **          (fp.isPositive (fp.neg x)) --> (fp.isNegative x)
- **          (fp.isNegative (fp.neg x)) --> (fp.isPositive x)
- **          (fp.isPositive (fp.abs x)) --> (not (isNaN x))
- **          (fp.isNegative (fp.abs x)) --> false
- **          A -> castA --> A
- **          A -> castB -> castC  -->  A -> castC if A <= B <= C
- **          A -> castB -> castA  -->  A if A <= B
- **          promotion converts can ignore rounding mode
- **          Samuel Figuer results
- **       ]]
+ ** \todo - Single argument constant propagate / simplify
+ **       - Push negations through arithmetic operators (include max and min?
+ **         maybe not due to +0/-0)
+ **       - classifications to normal tests (maybe)
+ **       - (= x (fp.neg x)) --> (isNaN x)
+ **       - (fp.eq x (fp.neg x)) --> (isZero x) (previous and reorganise
+ **             should be sufficient)
+ **       - (fp.eq x const) --> various = depending on const
+ **       - (fp.isPositive (fp.neg x)) --> (fp.isNegative x)
+ **       - (fp.isNegative (fp.neg x)) --> (fp.isPositive x)
+ **       - (fp.isPositive (fp.abs x)) --> (not (isNaN x))
+ **       - (fp.isNegative (fp.abs x)) --> false
+ **       - A -> castA --> A
+ **       - A -> castB -> castC  -->  A -> castC if A <= B <= C
+ **       - A -> castB -> castA  -->  A if A <= B
+ **       - promotion converts can ignore rounding mode
+ **       - Samuel Figuer results
  **/
 
 #include <algorithm>
diff --git a/src/theory/fp/theory_fp_rewriter.h b/src/theory/fp/theory_fp_rewriter.h
index 1232e9c75..5591246b4 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):
  **   Andres Noetzli, Martin Brain, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their 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 f09f1b449..32c718654 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, Aina Niemetz
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their 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 79322a314..01145472d 100644
--- a/src/theory/fp/type_enumerator.h
+++ b/src/theory/fp/type_enumerator.h
@@ -5,7 +5,7 @@
  **   Tim King, Martin Brain, Aina Niemetz
  ** Copyright (c) 2009-2015  New York University and The University of Iowa
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim