diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-03-08 23:27:03 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-03-09 07:27:03 +0000 |
commit | b302cb1f92aae1c0954c86065469e5c2b7206e74 (patch) | |
tree | f2b4cad1effdfe8041f00f23b6fe255b0c4004bb /src/theory/fp | |
parent | 86ce1c18f8ea7a397a8b12405a196b126e82b648 (diff) |
Update copyright headers to 2021. (#6081)
Diffstat (limited to 'src/theory/fp')
-rw-r--r-- | src/theory/fp/fp_converter.cpp | 2 | ||||
-rw-r--r-- | src/theory/fp/fp_converter.h | 2 | ||||
-rw-r--r-- | src/theory/fp/theory_fp.cpp | 2 | ||||
-rw-r--r-- | src/theory/fp/theory_fp.h | 2 | ||||
-rw-r--r-- | src/theory/fp/theory_fp_rewriter.cpp | 37 | ||||
-rw-r--r-- | src/theory/fp/theory_fp_rewriter.h | 2 | ||||
-rw-r--r-- | src/theory/fp/theory_fp_type_rules.h | 2 | ||||
-rw-r--r-- | src/theory/fp/type_enumerator.h | 2 |
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 |