From 480df3b40de9650387c5fceb9aee39311753e3ab Mon Sep 17 00:00:00 2001 From: Martin Date: Wed, 20 Sep 2017 02:30:24 +0100 Subject: [PATCH] Add FP type enumerator and cardinality computer (#1104) --- src/Makefile.am | 1 + src/theory/fp/kinds | 23 ++++- src/theory/fp/theory_fp_type_rules.h | 36 +++++++- src/theory/fp/type_enumerator.h | 128 +++++++++++++++++++++++++++ 4 files changed, 182 insertions(+), 6 deletions(-) create mode 100644 src/theory/fp/type_enumerator.h diff --git a/src/Makefile.am b/src/Makefile.am index 974f599e4..da8558527 100644 --- 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 a1b28d885..61a291b53 100644 --- 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 8dddf5065..54205315f 100644 --- 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(); + + /* + * 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 index 000000000..265199694 --- /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 { + + 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(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 { + + RoundingMode rm; + bool enumerationComplete; + +public: + + RoundingModeEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw(AssertionException) : + TypeEnumeratorBase(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 */ -- 2.30.2