summaryrefslogtreecommitdiff
path: root/src/theory/fp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/fp')
-rw-r--r--src/theory/fp/fp_converter.cpp27
-rw-r--r--src/theory/fp/fp_converter.h39
-rw-r--r--src/theory/fp/theory_fp.cpp30
-rw-r--r--src/theory/fp/theory_fp.h30
-rw-r--r--src/theory/fp/theory_fp_rewriter.cpp65
-rw-r--r--src/theory/fp/theory_fp_rewriter.h33
-rw-r--r--src/theory/fp/theory_fp_type_rules.cpp27
-rw-r--r--src/theory/fp/theory_fp_type_rules.h27
-rw-r--r--src/theory/fp/type_enumerator.h30
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"
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback