diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-04-12 12:31:43 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-04-12 19:31:43 +0000 |
commit | 7ec30058750611786b1b597816c8a23e28bb5812 (patch) | |
tree | e59b1de0078dc04d3a9c212cf9e6ebfd70cbb7f4 /src/theory/fp | |
parent | 7361b587e9a1b717dfa906d02f66feb6896e80dd (diff) |
Refactor and update copyright headers. (#6316)
Diffstat (limited to 'src/theory/fp')
-rw-r--r-- | src/theory/fp/fp_converter.cpp | 27 | ||||
-rw-r--r-- | src/theory/fp/fp_converter.h | 39 | ||||
-rw-r--r-- | src/theory/fp/theory_fp.cpp | 30 | ||||
-rw-r--r-- | src/theory/fp/theory_fp.h | 30 | ||||
-rw-r--r-- | src/theory/fp/theory_fp_rewriter.cpp | 65 | ||||
-rw-r--r-- | src/theory/fp/theory_fp_rewriter.h | 33 | ||||
-rw-r--r-- | src/theory/fp/theory_fp_type_rules.cpp | 27 | ||||
-rw-r--r-- | src/theory/fp/theory_fp_type_rules.h | 27 | ||||
-rw-r--r-- | src/theory/fp/type_enumerator.h | 30 |
9 files changed, 154 insertions, 154 deletions
diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp index 5b2f586ba..a62fd4894 100644 --- a/src/theory/fp/fp_converter.cpp +++ b/src/theory/fp/fp_converter.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file fp_converter.cpp - ** \verbatim - ** Top contributors (to current version): - ** Martin Brain, Mathias Preiner, Aina Niemetz - ** This file is part of the CVC4 project. - ** 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 Conversion of floating-point operations to bit-vectors using symfpu. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Martin Brain, Mathias Preiner, Aina Niemetz + * + * This file is part of the cvc5 project. + * + * 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. + * **************************************************************************** + * + * Conversion of floating-point operations to bit-vectors using symfpu. + */ #include "theory/fp/fp_converter.h" diff --git a/src/theory/fp/fp_converter.h b/src/theory/fp/fp_converter.h index 3a74627d5..146751e50 100644 --- a/src/theory/fp/fp_converter.h +++ b/src/theory/fp/fp_converter.h @@ -1,22 +1,23 @@ -/********************* */ -/*! \file fp_converter.h - ** \verbatim - ** Top contributors (to current version): - ** Martin Brain, Mathias Preiner, Aina Niemetz - ** This file is part of the CVC4 project. - ** 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 Converts floating-point nodes to bit-vector expressions. - ** - ** Uses the symfpu library to convert from floating-point operations to - ** bit-vectors and propositions allowing the theory to be solved by - ** 'bit-blasting'. - ** - ** !!! This header is not to be included in any other headers !!! - **/ +/****************************************************************************** + * Top contributors (to current version): + * Martin Brain, Mathias Preiner, Aina Niemetz + * + * This file is part of the cvc5 project. + * + * 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. + * **************************************************************************** + * + * Converts floating-point nodes to bit-vector expressions. + * + * Uses the symfpu library to convert from floating-point operations to + * bit-vectors and propositions allowing the theory to be solved by + * 'bit-blasting'. + * + * !!! This header is not to be included in any other headers !!! + */ #include "cvc4_private.h" diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp index 88d01ea20..80a5c539b 100644 --- a/src/theory/fp/theory_fp.cpp +++ b/src/theory/fp/theory_fp.cpp @@ -1,19 +1,17 @@ -/********************* */ -/*! \file theory_fp.cpp - ** \verbatim - ** Top contributors (to current version): - ** Martin Brain, Andrew Reynolds, Andres Noetzli - ** This file is part of the CVC4 project. - ** 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 [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ +/****************************************************************************** + * Top contributors (to current version): + * Martin Brain, Andrew Reynolds, Andres Noetzli + * + * This file is part of the cvc5 project. + * + * 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. + * **************************************************************************** + * + * Theory of floating-point arithmetic. + */ #include "theory/fp/theory_fp.h" diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h index 875614928..feda238e1 100644 --- a/src/theory/fp/theory_fp.h +++ b/src/theory/fp/theory_fp.h @@ -1,19 +1,17 @@ -/********************* */ -/*! \file theory_fp.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Martin Brain, Aina Niemetz - ** This file is part of the CVC4 project. - ** 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 [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Martin Brain, Aina Niemetz + * + * This file is part of the cvc5 project. + * + * 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. + * **************************************************************************** + * + * Theory of floating-point arithmetic. + */ #include "cvc4_private.h" diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp index 51d2e5bd7..64b89913a 100644 --- a/src/theory/fp/theory_fp_rewriter.cpp +++ b/src/theory/fp/theory_fp_rewriter.cpp @@ -1,35 +1,36 @@ -/********************* */ -/*! \file theory_fp_rewriter.cpp - ** \verbatim - ** Top contributors (to current version): - ** Martin Brain, Andres Noetzli, Aina Niemetz - ** Copyright (c) 2013 University of Oxford - ** This file is part of the CVC4 project. - ** 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. - ** - ** \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 - **/ +/****************************************************************************** + * Top contributors (to current version): + * Martin Brain, Andres Noetzli, Aina Niemetz + * Copyright (c) 2013 University of Oxford + * + * This file is part of the cvc5 project. + * + * 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. + * **************************************************************************** + * + * 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 + */ #include <algorithm> diff --git a/src/theory/fp/theory_fp_rewriter.h b/src/theory/fp/theory_fp_rewriter.h index 29d16e119..8c634abe2 100644 --- a/src/theory/fp/theory_fp_rewriter.h +++ b/src/theory/fp/theory_fp_rewriter.h @@ -1,19 +1,20 @@ -/********************* */ -/*! \file theory_fp_rewriter.h - ** \verbatim - ** Top contributors (to current version): - ** Andres Noetzli, Martin Brain, Mathias Preiner - ** This file is part of the CVC4 project. - ** 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 [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andres Noetzli, Martin Brain, Mathias Preiner + * + * This file is part of the cvc5 project. + * + * 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. + * **************************************************************************** + * + * [[ Add one-line brief description here ]] + * + * [[ Add lengthier description here ]] + * \todo document this file + */ #include "cvc4_private.h" diff --git a/src/theory/fp/theory_fp_type_rules.cpp b/src/theory/fp/theory_fp_type_rules.cpp index 44936c440..6beba19ad 100644 --- a/src/theory/fp/theory_fp_type_rules.cpp +++ b/src/theory/fp/theory_fp_type_rules.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file theory_fp_type_rules.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Martin Brain, Tim King - ** This file is part of the CVC4 project. - ** 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 Type rules for the theory of floating-point arithmetic. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Martin Brain, Tim King + * + * This file is part of the cvc5 project. + * + * 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. + * **************************************************************************** + * + * Type rules for the theory of floating-point arithmetic. + */ #include "theory/fp/theory_fp_type_rules.h" diff --git a/src/theory/fp/theory_fp_type_rules.h b/src/theory/fp/theory_fp_type_rules.h index c00c5f910..5c9eaf342 100644 --- a/src/theory/fp/theory_fp_type_rules.h +++ b/src/theory/fp/theory_fp_type_rules.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file theory_fp_type_rules.h - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Martin Brain, Mathias Preiner - ** This file is part of the CVC4 project. - ** 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 Type rules for the theory of floating-point arithmetic. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Martin Brain, Mathias Preiner + * + * This file is part of the cvc5 project. + * + * 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. + * **************************************************************************** + * + * Type rules for the theory of floating-point arithmetic. + */ #include "cvc4_private.h" diff --git a/src/theory/fp/type_enumerator.h b/src/theory/fp/type_enumerator.h index c97dd94cb..0d22bc62d 100644 --- a/src/theory/fp/type_enumerator.h +++ b/src/theory/fp/type_enumerator.h @@ -1,19 +1,17 @@ -/********************* */ -/*! \file type_enumerator.h - ** \verbatim - ** Top contributors (to current version): - ** 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-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 An enumerator for floating-point numbers. - ** - ** An enumerator for floating-point numbers. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Tim King, Martin Brain, Aina Niemetz + * + * This file is part of the cvc5 project. + * + * 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. + * **************************************************************************** + * + * An enumerator for floating-point numbers. + */ #include "cvc4_private.h" |