Add FP type enumerator and cardinality computer (#1104)

diff --git a/src/Makefile.am b/src/Makefile.am
index 974f599e4be78b9c9a25d2976b1353c47c97c674..da8558527f3a9207dcf4736f1380ee4c463594a1 100644 (file)
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -329,6 +329,7 @@ libcvc4_la_SOURCES = \
        theory/fp/theory_fp_rewriter.cpp \
        theory/fp/theory_fp_rewriter.h \
        theory/fp/theory_fp_type_rules.h \
+       theory/fp/type_enumerator.h \
        theory/idl/idl_assertion.cpp \
        theory/idl/idl_assertion.h \
        theory/idl/idl_assertion_db.cpp \

diff --git a/src/theory/fp/kinds b/src/theory/fp/kinds
index a1b28d885be5f96a6f107583fb5413392ced4d1d..61a291b536423774d31f9c2ea6b376414272787c 100644 (file)
--- a/src/theory/fp/kinds
+++ b/src/theory/fp/kinds
@@ -38,14 +38,31 @@ sort ROUNDINGMODE_TYPE \
     "expr/node_manager.h" \
     "floating-point rounding mode"
 
+enumerator ROUNDINGMODE_TYPE \
+    "::CVC4::theory::fp::RoundingModeEnumerator" \
+    "theory/fp/type_enumerator.h"
+
+
+
 constant FLOATINGPOINT_TYPE \
     ::CVC4::FloatingPointSize \
     ::CVC4::FloatingPointSizeHashFunction \
     "util/floatingpoint.h" \
     "floating-point type"
-#cardinality FLOATINGPOINT_TYPE "function" "header"
-#enumerator FLOATINGPOINT_TYPE "function" "header"
-#well-founded FLOATINGPOINT_TYPE true "function" "header"
+
+cardinality FLOATINGPOINT_TYPE \
+    "::CVC4::theory::fp::CardinalityComputer::computeCardinality(%TYPE%)" \
+    "theory/fp/theory_fp_type_rules.h"
+
+enumerator FLOATINGPOINT_TYPE \
+    "::CVC4::theory::fp::FloatingPointEnumerator" \
+    "theory/fp/type_enumerator.h"
+
+well-founded FLOATINGPOINT_TYPE \
+    true \
+    "(*CVC4::theory::TypeEnumerator(%TYPE%))" \
+    "theory/type_enumerator.h"
+
 
 
 # operators...

diff --git a/src/theory/fp/theory_fp_type_rules.h b/src/theory/fp/theory_fp_type_rules.h
index 8dddf50659e4dd0aa6e75b9b9303c18bbf07dd64..54205315fb25d0981a55c49ffdaa01ae26450412 100644 (file)
--- a/src/theory/fp/theory_fp_type_rules.h
+++ b/src/theory/fp/theory_fp_type_rules.h
@@ -464,8 +464,38 @@ class FloatingPointToRealTypeRule {
   }
 };
 
-} /* CVC4::theory::fp namespace */
-} /* CVC4::theory namespace */
-} /* CVC4 namespace */
+
+class CardinalityComputer {
+public:
+  inline static Cardinality computeCardinality(TypeNode type) {
+    Assert(type.getKind() == kind::FLOATINGPOINT_TYPE);
+
+    FloatingPointSize fps = type.getConst<FloatingPointSize>();
+
+    /*
+     * 1                    NaN
+     * 2*1                  Infinities
+     * 2*1                  Zeros
+     * 2*2^(s-1)            Subnormal
+     * 2*((2^e)-2)*2^(s-1)  Normal
+     *
+     *  = 1 + 2*2 + 2*((2^e)-1)*2^(s-1)
+     *  =       5 + ((2^e)-1)*2^s
+     */
+
+    Integer significandValues = Integer(2).pow(fps.significand());
+    Integer exponentValues = Integer(2).pow(fps.exponent());
+    exponentValues -= Integer(1);
+
+    return Integer(5) + exponentValues * significandValues;
+  }
+};/* class CardinalityComputer */
+
+
+
+
+}/* CVC4::theory::fp namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
 
 #endif /* __CVC4__THEORY__FP__THEORY_FP_TYPE_RULES_H */

diff --git a/src/theory/fp/type_enumerator.h b/src/theory/fp/type_enumerator.h
new file mode 100644 (file)
index 0000000..2651996
--- /dev/null
+++ b/src/theory/fp/type_enumerator.h
@@ -0,0 +1,128 @@
+/*********************                                                        */
+/*! \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.
+ ** 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
+ **
+ ** \brief An enumerator for floating-point numbers.
+ **
+ ** An enumerator for floating-point numbers.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__FP__TYPE_ENUMERATOR_H
+#define __CVC4__THEORY__FP__TYPE_ENUMERATOR_H
+
+#include "util/floatingpoint.h"
+#include "util/bitvector.h"
+#include "theory/type_enumerator.h"
+#include "expr/type_node.h"
+#include "expr/kind.h"
+
+namespace CVC4 {
+namespace theory {
+namespace fp {
+
+class FloatingPointEnumerator : public TypeEnumeratorBase<FloatingPointEnumerator> {
+
+  unsigned e;
+  unsigned s;
+  BitVector state;
+  bool enumerationComplete;
+
+protected :
+
+  FloatingPoint createFP (void) const {
+    // Rotate the LSB into the sign so that NaN is the last value
+    BitVector value = state.logicalRightShift(1) | state.leftShift(state.getSize() - 1);
+    
+    return FloatingPoint(e, s, value);
+  }
+
+
+public:
+
+  FloatingPointEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw(AssertionException) :
+    TypeEnumeratorBase<FloatingPointEnumerator>(type),
+      e(type.getFloatingPointExponentSize()),
+      s(type.getFloatingPointSignificandSize()),
+      state(e + s, 0U),
+      enumerationComplete(false) 
+    {}
+
+
+  Node operator*() throw(NoMoreValuesException) {
+    if (enumerationComplete) {
+      throw NoMoreValuesException(getType());
+    }
+    return NodeManager::currentNM()->mkConst(createFP());
+  }
+
+  FloatingPointEnumerator& operator++() throw() {
+    FloatingPoint current(createFP());
+
+    if (current.isNaN()) {
+      enumerationComplete = true;
+    } else {
+      state = state + BitVector(state.getSize(), 1U);
+    }
+
+    return *this;
+  }
+
+  bool isFinished() throw() {
+    return enumerationComplete;
+  }
+
+};/* FloatingPointEnumerator */
+
+class RoundingModeEnumerator : public TypeEnumeratorBase<RoundingModeEnumerator> {
+
+  RoundingMode rm;
+  bool enumerationComplete;
+
+public:
+
+  RoundingModeEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw(AssertionException) :
+    TypeEnumeratorBase<RoundingModeEnumerator>(type),
+      rm(roundNearestTiesToEven),
+      enumerationComplete(false)
+    {}
+
+
+  Node operator*() throw(NoMoreValuesException) {
+    if (enumerationComplete) {
+      throw NoMoreValuesException(getType());
+    }
+    return NodeManager::currentNM()->mkConst(rm);
+  }
+
+  RoundingModeEnumerator& operator++() throw() {
+    switch (rm) {
+    case roundNearestTiesToEven : rm = roundTowardPositive; break;
+    case roundTowardPositive : rm = roundTowardNegative; break;
+    case roundTowardNegative : rm = roundTowardZero; break;
+    case roundTowardZero : rm = roundNearestTiesToAway; break;
+    case roundNearestTiesToAway : enumerationComplete = true; break;
+    default : Unreachable("Unknown rounding mode?"); break;
+    }
+    return *this;
+  }
+
+  bool isFinished() throw() {
+    return enumerationComplete;
+  }
+
+};/* RoundingModeEnumerator */
+
+}/* CVC4::theory::fp namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__FP__TYPE_ENUMERATOR_H */