From: Aina Niemetz Date: Wed, 31 Mar 2021 00:27:13 +0000 (-0700) Subject: FP: Move implementation of type rules from header to .cpp file. (#6241) X-Git-Tag: cvc5-1.0.0~2005 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4e1c3c1c12103ef5d3f2cb3d873247bb66716287;p=cvc5.git FP: Move implementation of type rules from header to .cpp file. (#6241) --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 41a6a0df5..645cf3c79 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -622,6 +622,7 @@ libcvc4_add_sources( theory/fp/theory_fp_rewriter.cpp theory/fp/theory_fp_rewriter.h theory/fp/theory_fp_type_rules.h + theory/fp/theory_fp_type_rules.cpp theory/fp/type_enumerator.h theory/interrupted.h theory/inference_id.cpp diff --git a/src/theory/fp/theory_fp_type_rules.cpp b/src/theory/fp/theory_fp_type_rules.cpp new file mode 100644 index 000000000..165c9b924 --- /dev/null +++ b/src/theory/fp/theory_fp_type_rules.cpp @@ -0,0 +1,815 @@ +/********************* */ +/*! \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. + **/ + +#include "theory/fp/theory_fp_type_rules.h" + +// This is only needed for checking that components are only applied to leaves. +#include "theory/theory.h" +#include "util/roundingmode.h" + +namespace CVC4 { +namespace theory { +namespace fp { + +#define TRACE(FUNCTION) \ + Trace("fp-type") << FUNCTION "::computeType(" << check << "): " << n \ + << std::endl + +TypeNode FloatingPointConstantTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + TRACE("FloatingPointConstantTypeRule"); + + const FloatingPoint& f = n.getConst(); + + if (check) + { + if (!(validExponentSize(f.getSize().exponentWidth()))) + { + throw TypeCheckingExceptionPrivate(n, + "constant with invalid exponent size"); + } + if (!(validSignificandSize(f.getSize().significandWidth()))) + { + throw TypeCheckingExceptionPrivate( + n, "constant with invalid significand size"); + } + } + return nodeManager->mkFloatingPointType(f.getSize()); +} + +TypeNode RoundingModeConstantTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + TRACE("RoundingModeConstantTypeRule"); + + // Nothing to check! + return nodeManager->roundingModeType(); +} + +TypeNode FloatingPointFPTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + TRACE("FloatingPointFPTypeRule"); + + TypeNode signType = n[0].getType(check); + TypeNode exponentType = n[1].getType(check); + TypeNode significandType = n[2].getType(check); + + if (!signType.isBitVector() || !exponentType.isBitVector() + || !significandType.isBitVector()) + { + throw TypeCheckingExceptionPrivate(n, + "arguments to fp must be bit vectors"); + } + + uint32_t signBits = signType.getBitVectorSize(); + uint32_t exponentBits = exponentType.getBitVectorSize(); + uint32_t significandBits = significandType.getBitVectorSize(); + + if (check) + { + if (signBits != 1) + { + throw TypeCheckingExceptionPrivate( + n, "sign bit vector in fp must be 1 bit long"); + } + else if (!(validExponentSize(exponentBits))) + { + throw TypeCheckingExceptionPrivate( + n, "exponent bit vector in fp is an invalid size"); + } + else if (!(validSignificandSize(significandBits))) + { + throw TypeCheckingExceptionPrivate( + n, "significand bit vector in fp is an invalid size"); + } + } + + // The +1 is for the implicit hidden bit + return nodeManager->mkFloatingPointType(exponentBits, significandBits + 1); +} + +TypeNode FloatingPointTestTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + TRACE("FloatingPointTestTypeRule"); + + if (check) + { + TypeNode firstOperand = n[0].getType(check); + + if (!firstOperand.isFloatingPoint()) + { + throw TypeCheckingExceptionPrivate( + n, "floating-point test applied to a non floating-point sort"); + } + + size_t children = n.getNumChildren(); + for (size_t i = 1; i < children; ++i) + { + if (!(n[i].getType(check) == firstOperand)) + { + throw TypeCheckingExceptionPrivate( + n, "floating-point test applied to mixed sorts"); + } + } + } + + return nodeManager->booleanType(); +} + +TypeNode FloatingPointOperationTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + TRACE("FloatingPointOperationTypeRule"); + + TypeNode firstOperand = n[0].getType(check); + + if (check) + { + if (!firstOperand.isFloatingPoint()) + { + throw TypeCheckingExceptionPrivate( + n, "floating-point operation applied to a non floating-point sort"); + } + + size_t children = n.getNumChildren(); + for (size_t i = 1; i < children; ++i) + { + if (!(n[i].getType(check) == firstOperand)) + { + throw TypeCheckingExceptionPrivate( + n, "floating-point test applied to mixed sorts"); + } + } + } + + return firstOperand; +} + +TypeNode FloatingPointRoundingOperationTypeRule::computeType( + NodeManager* nodeManager, TNode n, bool check) +{ + TRACE("FloatingPointRoundingOperationTypeRule"); + + if (check) + { + TypeNode roundingModeType = n[0].getType(check); + + if (!roundingModeType.isRoundingMode()) + { + throw TypeCheckingExceptionPrivate( + n, "first argument must be a rounding mode"); + } + } + + TypeNode firstOperand = n[1].getType(check); + + if (check) + { + if (!firstOperand.isFloatingPoint()) + { + throw TypeCheckingExceptionPrivate( + n, "floating-point operation applied to a non floating-point sort"); + } + + size_t children = n.getNumChildren(); + for (size_t i = 2; i < children; ++i) + { + if (!(n[i].getType(check) == firstOperand)) + { + throw TypeCheckingExceptionPrivate( + n, "floating-point operation applied to mixed sorts"); + } + } + } + + return firstOperand; +} + +TypeNode FloatingPointPartialOperationTypeRule::computeType( + NodeManager* nodeManager, TNode n, bool check) +{ + TRACE("FloatingPointOperationTypeRule"); + AlwaysAssert(n.getNumChildren() > 0); + + TypeNode firstOperand = n[0].getType(check); + + if (check) + { + if (!firstOperand.isFloatingPoint()) + { + throw TypeCheckingExceptionPrivate( + n, "floating-point operation applied to a non floating-point sort"); + } + + const size_t children = n.getNumChildren(); + for (size_t i = 1; i < children - 1; ++i) + { + if (n[i].getType(check) != firstOperand) + { + throw TypeCheckingExceptionPrivate( + n, "floating-point partial operation applied to mixed sorts"); + } + } + + TypeNode UFValueType = n[children - 1].getType(check); + + if (!(UFValueType.isBitVector()) || !(UFValueType.getBitVectorSize() == 1)) + { + throw TypeCheckingExceptionPrivate( + n, + "floating-point partial operation final argument must be a " + "bit-vector of length 1"); + } + } + + return firstOperand; +} + +TypeNode FloatingPointParametricOpTypeRule::computeType( + NodeManager* nodeManager, TNode n, bool check) +{ + TRACE("FloatingPointParametricOpTypeRule"); + + return nodeManager->builtinOperatorType(); +} + +TypeNode FloatingPointToFPIEEEBitVectorTypeRule::computeType( + NodeManager* nodeManager, TNode n, bool check) +{ + TRACE("FloatingPointToFPIEEEBitVectorTypeRule"); + AlwaysAssert(n.getNumChildren() == 1); + + FloatingPointToFPIEEEBitVector info = + n.getOperator().getConst(); + + if (check) + { + TypeNode operandType = n[0].getType(check); + + if (!(operandType.isBitVector())) + { + throw TypeCheckingExceptionPrivate(n, + "conversion to floating-point from " + "bit vector used with sort other " + "than bit vector"); + } + else if (!(operandType.getBitVectorSize() + == info.getSize().exponentWidth() + + info.getSize().significandWidth())) + { + throw TypeCheckingExceptionPrivate( + n, + "conversion to floating-point from bit vector used with bit vector " + "length that does not match floating point parameters"); + } + } + + return nodeManager->mkFloatingPointType(info.getSize()); +} + +TypeNode FloatingPointToFPFloatingPointTypeRule::computeType( + NodeManager* nodeManager, TNode n, bool check) +{ + TRACE("FloatingPointToFPFloatingPointTypeRule"); + AlwaysAssert(n.getNumChildren() == 2); + + FloatingPointToFPFloatingPoint info = + n.getOperator().getConst(); + + if (check) + { + TypeNode roundingModeType = n[0].getType(check); + + if (!roundingModeType.isRoundingMode()) + { + throw TypeCheckingExceptionPrivate( + n, "first argument must be a rounding mode"); + } + + TypeNode operandType = n[1].getType(check); + + if (!(operandType.isFloatingPoint())) + { + throw TypeCheckingExceptionPrivate(n, + "conversion to floating-point from " + "floating-point used with sort " + "other than floating-point"); + } + } + + return nodeManager->mkFloatingPointType(info.getSize()); +} + +TypeNode FloatingPointToFPRealTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + TRACE("FloatingPointToFPRealTypeRule"); + AlwaysAssert(n.getNumChildren() == 2); + + FloatingPointToFPReal info = + n.getOperator().getConst(); + + if (check) + { + TypeNode roundingModeType = n[0].getType(check); + + if (!roundingModeType.isRoundingMode()) + { + throw TypeCheckingExceptionPrivate( + n, "first argument must be a rounding mode"); + } + + TypeNode operandType = n[1].getType(check); + + if (!(operandType.isReal())) + { + throw TypeCheckingExceptionPrivate(n, + "conversion to floating-point from " + "real used with sort other than " + "real"); + } + } + + return nodeManager->mkFloatingPointType(info.getSize()); +} + +TypeNode FloatingPointToFPSignedBitVectorTypeRule::computeType( + NodeManager* nodeManager, TNode n, bool check) +{ + TRACE("FloatingPointToFPSignedBitVectorTypeRule"); + AlwaysAssert(n.getNumChildren() == 2); + + FloatingPointToFPSignedBitVector info = + n.getOperator().getConst(); + + if (check) + { + TypeNode roundingModeType = n[0].getType(check); + + if (!roundingModeType.isRoundingMode()) + { + throw TypeCheckingExceptionPrivate( + n, "first argument must be a rounding mode"); + } + + TypeNode operandType = n[1].getType(check); + + if (!(operandType.isBitVector())) + { + throw TypeCheckingExceptionPrivate(n, + "conversion to floating-point from " + "signed bit vector used with sort " + "other than bit vector"); + } + } + + return nodeManager->mkFloatingPointType(info.getSize()); +} + +TypeNode FloatingPointToFPUnsignedBitVectorTypeRule::computeType( + NodeManager* nodeManager, TNode n, bool check) +{ + TRACE("FloatingPointToFPUnsignedBitVectorTypeRule"); + AlwaysAssert(n.getNumChildren() == 2); + + FloatingPointToFPUnsignedBitVector info = + n.getOperator().getConst(); + + if (check) + { + TypeNode roundingModeType = n[0].getType(check); + + if (!roundingModeType.isRoundingMode()) + { + throw TypeCheckingExceptionPrivate( + n, "first argument must be a rounding mode"); + } + + TypeNode operandType = n[1].getType(check); + + if (!(operandType.isBitVector())) + { + throw TypeCheckingExceptionPrivate(n, + "conversion to floating-point from " + "unsigned bit vector used with sort " + "other than bit vector"); + } + } + + return nodeManager->mkFloatingPointType(info.getSize()); +} + +TypeNode FloatingPointToFPGenericTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + TRACE("FloatingPointToFPGenericTypeRule"); + + FloatingPointToFPGeneric info = + n.getOperator().getConst(); + + if (check) + { + /* As this is a generic kind intended only for parsing, + * the checking here is light. For better checking, use + * expandDefinitions first. + */ + + size_t children = n.getNumChildren(); + for (size_t i = 0; i < children; ++i) + { + n[i].getType(check); + } + } + + return nodeManager->mkFloatingPointType(info.getSize()); +} + +TypeNode FloatingPointToUBVTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + TRACE("FloatingPointToUBVTypeRule"); + AlwaysAssert(n.getNumChildren() == 2); + + FloatingPointToUBV info = n.getOperator().getConst(); + + if (check) + { + TypeNode roundingModeType = n[0].getType(check); + + if (!roundingModeType.isRoundingMode()) + { + throw TypeCheckingExceptionPrivate( + n, "first argument must be a rounding mode"); + } + + TypeNode operandType = n[1].getType(check); + + if (!(operandType.isFloatingPoint())) + { + throw TypeCheckingExceptionPrivate(n, + "conversion to unsigned bit vector " + "used with a sort other than " + "floating-point"); + } + } + + return nodeManager->mkBitVectorType(info.d_bv_size); +} + +TypeNode FloatingPointToSBVTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + TRACE("FloatingPointToSBVTypeRule"); + AlwaysAssert(n.getNumChildren() == 2); + + FloatingPointToSBV info = n.getOperator().getConst(); + + if (check) + { + TypeNode roundingModeType = n[0].getType(check); + + if (!roundingModeType.isRoundingMode()) + { + throw TypeCheckingExceptionPrivate( + n, "first argument must be a rounding mode"); + } + + TypeNode operandType = n[1].getType(check); + + if (!(operandType.isFloatingPoint())) + { + throw TypeCheckingExceptionPrivate(n, + "conversion to signed bit vector " + "used with a sort other than " + "floating-point"); + } + } + + return nodeManager->mkBitVectorType(info.d_bv_size); +} + +TypeNode FloatingPointToUBVTotalTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + TRACE("FloatingPointToUBVTotalTypeRule"); + AlwaysAssert(n.getNumChildren() == 3); + + FloatingPointToUBVTotal info = + n.getOperator().getConst(); + + if (check) + { + TypeNode roundingModeType = n[0].getType(check); + + if (!roundingModeType.isRoundingMode()) + { + throw TypeCheckingExceptionPrivate( + n, "first argument must be a rounding mode"); + } + + TypeNode operandType = n[1].getType(check); + + if (!(operandType.isFloatingPoint())) + { + throw TypeCheckingExceptionPrivate( + n, + "conversion to unsigned bit vector total" + "used with a sort other than " + "floating-point"); + } + + TypeNode defaultValueType = n[2].getType(check); + + if (!(defaultValueType.isBitVector()) + || !(defaultValueType.getBitVectorSize() == info)) + { + throw TypeCheckingExceptionPrivate( + n, + "conversion to unsigned bit vector total" + "needs a bit vector of the same length" + "as last argument"); + } + } + + return nodeManager->mkBitVectorType(info.d_bv_size); +} + +TypeNode FloatingPointToSBVTotalTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + TRACE("FloatingPointToSBVTotalTypeRule"); + AlwaysAssert(n.getNumChildren() == 3); + + FloatingPointToSBVTotal info = + n.getOperator().getConst(); + + if (check) + { + TypeNode roundingModeType = n[0].getType(check); + + if (!roundingModeType.isRoundingMode()) + { + throw TypeCheckingExceptionPrivate( + n, "first argument must be a rounding mode"); + } + + TypeNode operandType = n[1].getType(check); + + if (!(operandType.isFloatingPoint())) + { + throw TypeCheckingExceptionPrivate(n, + "conversion to signed bit vector " + "used with a sort other than " + "floating-point"); + } + + TypeNode defaultValueType = n[2].getType(check); + + if (!(defaultValueType.isBitVector()) + || !(defaultValueType.getBitVectorSize() == info)) + { + throw TypeCheckingExceptionPrivate(n, + "conversion to signed bit vector total" + "needs a bit vector of the same length" + "as last argument"); + } + } + + return nodeManager->mkBitVectorType(info.d_bv_size); +} + +TypeNode FloatingPointToRealTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + TRACE("FloatingPointToRealTypeRule"); + AlwaysAssert(n.getNumChildren() == 1); + + if (check) + { + TypeNode operandType = n[0].getType(check); + + if (!operandType.isFloatingPoint()) + { + throw TypeCheckingExceptionPrivate( + n, "floating-point to real applied to a non floating-point sort"); + } + } + + return nodeManager->realType(); +} + +TypeNode FloatingPointToRealTotalTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + TRACE("FloatingPointToRealTotalTypeRule"); + AlwaysAssert(n.getNumChildren() == 2); + + if (check) + { + TypeNode operandType = n[0].getType(check); + + if (!operandType.isFloatingPoint()) + { + throw TypeCheckingExceptionPrivate( + n, + "floating-point to real total applied to a non floating-point sort"); + } + + TypeNode defaultValueType = n[1].getType(check); + + if (!defaultValueType.isReal()) + { + throw TypeCheckingExceptionPrivate( + n, "floating-point to real total needs a real second argument"); + } + } + + return nodeManager->realType(); +} + +TypeNode FloatingPointComponentBit::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + TRACE("FloatingPointComponentBit"); + + if (check) + { + TypeNode operandType = n[0].getType(check); + + if (!operandType.isFloatingPoint()) + { + throw TypeCheckingExceptionPrivate(n, + "floating-point bit component " + "applied to a non floating-point " + "sort"); + } + if (!(Theory::isLeafOf(n[0], THEORY_FP) + || n[0].getKind() == kind::FLOATINGPOINT_TO_FP_REAL)) + { + throw TypeCheckingExceptionPrivate(n, + "floating-point bit component " + "applied to a non leaf / to_fp leaf " + "node"); + } + } + + return nodeManager->mkBitVectorType(1); +} + +TypeNode FloatingPointComponentExponent::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + TRACE("FloatingPointComponentExponent"); + + TypeNode operandType = n[0].getType(check); + + if (check) + { + if (!operandType.isFloatingPoint()) + { + throw TypeCheckingExceptionPrivate(n, + "floating-point exponent component " + "applied to a non floating-point " + "sort"); + } + if (!(Theory::isLeafOf(n[0], THEORY_FP) + || n[0].getKind() == kind::FLOATINGPOINT_TO_FP_REAL)) + { + throw TypeCheckingExceptionPrivate(n, + "floating-point exponent component " + "applied to a non leaf / to_fp " + "node"); + } + } + +#ifdef CVC4_USE_SYMFPU + /* Need to create some symfpu objects as the size of bit-vector + * that is needed for this component is dependent on the encoding + * used (i.e. whether subnormals are forcibly normalised or not). + * Here we use types from floatingpoint.h which are the literal + * back-end but it should't make a difference. */ + FloatingPointSize fps = operandType.getConst(); + uint32_t bw = FloatingPoint::getUnpackedExponentWidth(fps); +#else + uint32_t bw = 2; +#endif + return nodeManager->mkBitVectorType(bw); +} + +TypeNode FloatingPointComponentSignificand::computeType( + NodeManager* nodeManager, TNode n, bool check) +{ + TRACE("FloatingPointComponentSignificand"); + + TypeNode operandType = n[0].getType(check); + + if (check) + { + if (!operandType.isFloatingPoint()) + { + throw TypeCheckingExceptionPrivate(n, + "floating-point significand " + "component applied to a non " + "floating-point sort"); + } + if (!(Theory::isLeafOf(n[0], THEORY_FP) + || n[0].getKind() == kind::FLOATINGPOINT_TO_FP_REAL)) + { + throw TypeCheckingExceptionPrivate(n, + "floating-point significand " + "component applied to a non leaf / " + "to_fp node"); + } + } + +#ifdef CVC4_USE_SYMFPU + /* As before we need to use some of sympfu. */ + FloatingPointSize fps = operandType.getConst(); + uint32_t bw = FloatingPoint::getUnpackedSignificandWidth(fps); +#else + uint32_t bw = 1; +#endif + return nodeManager->mkBitVectorType(bw); +} + +TypeNode RoundingModeBitBlast::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + TRACE("RoundingModeBitBlast"); + + if (check) + { + TypeNode operandType = n[0].getType(check); + + if (!operandType.isRoundingMode()) + { + throw TypeCheckingExceptionPrivate( + n, "rounding mode bit-blast applied to a non rounding-mode sort"); + } + if (!Theory::isLeafOf(n[0], THEORY_FP)) + { + throw TypeCheckingExceptionPrivate( + n, "rounding mode bit-blast applied to a non leaf node"); + } + } + + return nodeManager->mkBitVectorType(CVC4_NUM_ROUNDING_MODES); +} + +Cardinality CardinalityComputer::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.significandWidth()); + Integer exponentValues = Integer(2).pow(fps.exponentWidth()); + exponentValues -= Integer(1); + + return Integer(5) + exponentValues * significandValues; +} + +} // namespace fp +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/fp/theory_fp_type_rules.h b/src/theory/fp/theory_fp_type_rules.h index ab193d7ba..aef2d0a50 100644 --- a/src/theory/fp/theory_fp_type_rules.h +++ b/src/theory/fp/theory_fp_type_rules.h @@ -2,813 +2,233 @@ /*! \file theory_fp_type_rules.h ** \verbatim ** Top contributors (to current version): - ** Martin Brain, Tim King, Aina Niemetz + ** 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 [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file + ** \brief Type rules for the theory of floating-point arithmetic. **/ #include "cvc4_private.h" -// This is only needed for checking that components are only applied to leaves. -#include "theory/theory.h" -#include "util/roundingmode.h" - #ifndef CVC4__THEORY__FP__THEORY_FP_TYPE_RULES_H #define CVC4__THEORY__FP__THEORY_FP_TYPE_RULES_H +#include "expr/node.h" +#include "expr/type_node.h" + namespace CVC4 { + +class NodeManager; + namespace theory { namespace fp { -#define TRACE(FUNCTION) \ - Trace("fp-type") << FUNCTION "::computeType(" << check << "): " << n \ - << std::endl - -class FloatingPointConstantTypeRule { +/** Type rule for floating-point values. */ +class FloatingPointConstantTypeRule +{ public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, - bool check) { - TRACE("FloatingPointConstantTypeRule"); - - const FloatingPoint& f = n.getConst(); - - if (check) - { - if (!(validExponentSize(f.getSize().exponentWidth()))) - { - throw TypeCheckingExceptionPrivate( - n, "constant with invalid exponent size"); - } - if (!(validSignificandSize(f.getSize().significandWidth()))) - { - throw TypeCheckingExceptionPrivate( - n, "constant with invalid significand size"); - } - } - return nodeManager->mkFloatingPointType(f.getSize()); - } + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; -class RoundingModeConstantTypeRule { +/** Type rule for roundingmode values. */ +class RoundingModeConstantTypeRule +{ public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, - bool check) { - TRACE("RoundingModeConstantTypeRule"); - - // Nothing to check! - return nodeManager->roundingModeType(); - } + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; -class FloatingPointFPTypeRule { +/** Type rule for (fp ...) operator. */ +class FloatingPointFPTypeRule +{ public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, - bool check) { - TRACE("FloatingPointFPTypeRule"); - - TypeNode signType = n[0].getType(check); - TypeNode exponentType = n[1].getType(check); - TypeNode significandType = n[2].getType(check); - - if (!signType.isBitVector() || !exponentType.isBitVector() || - !significandType.isBitVector()) { - throw TypeCheckingExceptionPrivate(n, - "arguments to fp must be bit vectors"); - } - - unsigned signBits = signType.getBitVectorSize(); - unsigned exponentBits = exponentType.getBitVectorSize(); - unsigned significandBits = significandType.getBitVectorSize(); - - if (check) { - if (signBits != 1) { - throw TypeCheckingExceptionPrivate( - n, "sign bit vector in fp must be 1 bit long"); - } else if (!(validExponentSize(exponentBits))) { - throw TypeCheckingExceptionPrivate( - n, "exponent bit vector in fp is an invalid size"); - } else if (!(validSignificandSize(significandBits))) { - throw TypeCheckingExceptionPrivate( - n, "significand bit vector in fp is an invalid size"); - } - } - - // The +1 is for the implicit hidden bit - return nodeManager->mkFloatingPointType(exponentBits, significandBits + 1); - } + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; -class FloatingPointTestTypeRule { +/** + * Type rule for floating-point predicates to check if all arguments are + * floating-points of the same sort. + */ +class FloatingPointTestTypeRule +{ public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, - bool check) { - TRACE("FloatingPointTestTypeRule"); - - if (check) { - TypeNode firstOperand = n[0].getType(check); - - if (!firstOperand.isFloatingPoint()) { - throw TypeCheckingExceptionPrivate( - n, "floating-point test applied to a non floating-point sort"); - } - - size_t children = n.getNumChildren(); - for (size_t i = 1; i < children; ++i) { - if (!(n[i].getType(check) == firstOperand)) { - throw TypeCheckingExceptionPrivate( - n, "floating-point test applied to mixed sorts"); - } - } - } - - return nodeManager->booleanType(); - } + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; -class FloatingPointOperationTypeRule { +/** + * Type rule for floating-point operators which expect that all operands are + * floating-points to check if all operands are floating-points of the same + * sort. + */ +class FloatingPointOperationTypeRule +{ public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, - bool check) { - TRACE("FloatingPointOperationTypeRule"); - - TypeNode firstOperand = n[0].getType(check); - - if (check) { - if (!firstOperand.isFloatingPoint()) { - throw TypeCheckingExceptionPrivate( - n, "floating-point operation applied to a non floating-point sort"); - } - - size_t children = n.getNumChildren(); - for (size_t i = 1; i < children; ++i) { - if (!(n[i].getType(check) == firstOperand)) { - throw TypeCheckingExceptionPrivate( - n, "floating-point test applied to mixed sorts"); - } - } - } - - return firstOperand; - } + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; -class FloatingPointRoundingOperationTypeRule { +/** + * Type rule for floating-point operators which expect a roundingmode as first + * operand and floating-points for the remaining operands. Checks if the + * floating-point operands are of the same sort. + */ +class FloatingPointRoundingOperationTypeRule +{ public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, - bool check) { - TRACE("FloatingPointRoundingOperationTypeRule"); - - if (check) { - TypeNode roundingModeType = n[0].getType(check); - - if (!roundingModeType.isRoundingMode()) { - throw TypeCheckingExceptionPrivate( - n, "first argument must be a rounding mode"); - } - } - - TypeNode firstOperand = n[1].getType(check); - - if (check) { - if (!firstOperand.isFloatingPoint()) { - throw TypeCheckingExceptionPrivate( - n, "floating-point operation applied to a non floating-point sort"); - } - - size_t children = n.getNumChildren(); - for (size_t i = 2; i < children; ++i) { - if (!(n[i].getType(check) == firstOperand)) { - throw TypeCheckingExceptionPrivate( - n, "floating-point operation applied to mixed sorts"); - } - } - } - - return firstOperand; - } + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; -class FloatingPointPartialOperationTypeRule { +/** + * Type rule for floating-point partial operators (min, max) which expect that + * all operands are floating-points to check if all operands are + * floating-points of the same sort. + */ +class FloatingPointPartialOperationTypeRule +{ public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, - bool check) { - TRACE("FloatingPointOperationTypeRule"); - AlwaysAssert(n.getNumChildren() > 0); - - TypeNode firstOperand = n[0].getType(check); - - if (check) { - if (!firstOperand.isFloatingPoint()) { - throw TypeCheckingExceptionPrivate( - n, "floating-point operation applied to a non floating-point sort"); - } - - const size_t children = n.getNumChildren(); - for (size_t i = 1; i < children - 1; ++i) { - if (n[i].getType(check) != firstOperand) { - throw TypeCheckingExceptionPrivate( - n, "floating-point partial operation applied to mixed sorts"); - } - } - - TypeNode UFValueType = n[children - 1].getType(check); - - if (!(UFValueType.isBitVector()) || - !(UFValueType.getBitVectorSize() == 1)) { - throw TypeCheckingExceptionPrivate( - n, "floating-point partial operation final argument must be a bit-vector of length 1"); - } - } - - return firstOperand; - } + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; - -class FloatingPointParametricOpTypeRule { +/** + * Type rule for floating-point parametric operators (to_fp, to_fp_unsigned) + * which expect that all operands are floating-points to check if all operands + * are floating-points of the same sort. + */ +class FloatingPointParametricOpTypeRule +{ public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, - bool check) { - TRACE("FloatingPointParametricOpTypeRule"); - - return nodeManager->builtinOperatorType(); - } + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; +/** Type rule for floating-point to_fp conversion from IEEE bit-vector. */ class FloatingPointToFPIEEEBitVectorTypeRule { public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, - bool check) { - TRACE("FloatingPointToFPIEEEBitVectorTypeRule"); - AlwaysAssert(n.getNumChildren() == 1); - - FloatingPointToFPIEEEBitVector info = - n.getOperator().getConst(); - - if (check) { - TypeNode operandType = n[0].getType(check); - - if (!(operandType.isBitVector())) - { - throw TypeCheckingExceptionPrivate(n, - "conversion to floating-point from " - "bit vector used with sort other " - "than bit vector"); - } - else if (!(operandType.getBitVectorSize() - == info.getSize().exponentWidth() - + info.getSize().significandWidth())) - { - throw TypeCheckingExceptionPrivate( - n, - "conversion to floating-point from bit vector used with bit vector " - "length that does not match floating point parameters"); - } - } - - return nodeManager->mkFloatingPointType(info.getSize()); - } + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; +/** Type rule for floating-point to_fp conversion from floating-point. */ class FloatingPointToFPFloatingPointTypeRule { public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, - bool check) { - TRACE("FloatingPointToFPFloatingPointTypeRule"); - AlwaysAssert(n.getNumChildren() == 2); - - FloatingPointToFPFloatingPoint info = - n.getOperator().getConst(); - - if (check) { - TypeNode roundingModeType = n[0].getType(check); - - if (!roundingModeType.isRoundingMode()) { - throw TypeCheckingExceptionPrivate( - n, "first argument must be a rounding mode"); - } - - TypeNode operandType = n[1].getType(check); - - if (!(operandType.isFloatingPoint())) { - throw TypeCheckingExceptionPrivate(n, - "conversion to floating-point from " - "floating-point used with sort " - "other than floating-point"); - } - } - - return nodeManager->mkFloatingPointType(info.getSize()); - } + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; +/** Type rule for floating-point to_fp conversion from real. */ class FloatingPointToFPRealTypeRule { public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, - bool check) { - TRACE("FloatingPointToFPRealTypeRule"); - AlwaysAssert(n.getNumChildren() == 2); - - FloatingPointToFPReal info = - n.getOperator().getConst(); - - if (check) { - TypeNode roundingModeType = n[0].getType(check); - - if (!roundingModeType.isRoundingMode()) { - throw TypeCheckingExceptionPrivate( - n, "first argument must be a rounding mode"); - } - - TypeNode operandType = n[1].getType(check); - - if (!(operandType.isReal())) { - throw TypeCheckingExceptionPrivate(n, - "conversion to floating-point from " - "real used with sort other than " - "real"); - } - } - - return nodeManager->mkFloatingPointType(info.getSize()); - } + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; +/** Type rule for floating-point to_fp conversion from signed bit-vector. */ class FloatingPointToFPSignedBitVectorTypeRule { public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, - bool check) { - TRACE("FloatingPointToFPSignedBitVectorTypeRule"); - AlwaysAssert(n.getNumChildren() == 2); - - FloatingPointToFPSignedBitVector info = - n.getOperator().getConst(); - - if (check) { - TypeNode roundingModeType = n[0].getType(check); - - if (!roundingModeType.isRoundingMode()) { - throw TypeCheckingExceptionPrivate( - n, "first argument must be a rounding mode"); - } - - TypeNode operandType = n[1].getType(check); - - if (!(operandType.isBitVector())) { - throw TypeCheckingExceptionPrivate(n, - "conversion to floating-point from " - "signed bit vector used with sort " - "other than bit vector"); - } - } - - return nodeManager->mkFloatingPointType(info.getSize()); - } + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; +/** Type rule for floating-point to_fp conversion from unsigned bit-vector. */ class FloatingPointToFPUnsignedBitVectorTypeRule { public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, - bool check) { - TRACE("FloatingPointToFPUnsignedBitVectorTypeRule"); - AlwaysAssert(n.getNumChildren() == 2); - - FloatingPointToFPUnsignedBitVector info = - n.getOperator().getConst(); - - if (check) { - TypeNode roundingModeType = n[0].getType(check); - - if (!roundingModeType.isRoundingMode()) { - throw TypeCheckingExceptionPrivate( - n, "first argument must be a rounding mode"); - } - - TypeNode operandType = n[1].getType(check); - - if (!(operandType.isBitVector())) { - throw TypeCheckingExceptionPrivate(n, - "conversion to floating-point from " - "unsigned bit vector used with sort " - "other than bit vector"); - } - } - - return nodeManager->mkFloatingPointType(info.getSize()); - } + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; +/** Generic type rule for floating-point to_fp conversion. */ class FloatingPointToFPGenericTypeRule { public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, - bool check) { - TRACE("FloatingPointToFPGenericTypeRule"); - - FloatingPointToFPGeneric info = - n.getOperator().getConst(); - - if (check) { - /* As this is a generic kind intended only for parsing, - * the checking here is light. For better checking, use - * expandDefinitions first. - */ - - size_t children = n.getNumChildren(); - for (size_t i = 0; i < children; ++i) { - n[i].getType(check); - } - } - - return nodeManager->mkFloatingPointType(info.getSize()); - } + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; -class FloatingPointToUBVTypeRule { +/** Type rule for conversion from floating-point to unsigned bit-vector. */ +class FloatingPointToUBVTypeRule +{ public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, - bool check) { - TRACE("FloatingPointToUBVTypeRule"); - AlwaysAssert(n.getNumChildren() == 2); - - FloatingPointToUBV info = n.getOperator().getConst(); - - if (check) { - TypeNode roundingModeType = n[0].getType(check); - - if (!roundingModeType.isRoundingMode()) { - throw TypeCheckingExceptionPrivate( - n, "first argument must be a rounding mode"); - } - - TypeNode operandType = n[1].getType(check); - - if (!(operandType.isFloatingPoint())) { - throw TypeCheckingExceptionPrivate(n, - "conversion to unsigned bit vector " - "used with a sort other than " - "floating-point"); - } - } - - return nodeManager->mkBitVectorType(info.d_bv_size); - } + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; -class FloatingPointToSBVTypeRule { +/** Type rule for conversion from floating-point to signed bit-vector. */ +class FloatingPointToSBVTypeRule +{ public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, - bool check) { - TRACE("FloatingPointToSBVTypeRule"); - AlwaysAssert(n.getNumChildren() == 2); - - FloatingPointToSBV info = n.getOperator().getConst(); - - if (check) { - TypeNode roundingModeType = n[0].getType(check); - - if (!roundingModeType.isRoundingMode()) { - throw TypeCheckingExceptionPrivate( - n, "first argument must be a rounding mode"); - } - - TypeNode operandType = n[1].getType(check); - - if (!(operandType.isFloatingPoint())) { - throw TypeCheckingExceptionPrivate(n, - "conversion to signed bit vector " - "used with a sort other than " - "floating-point"); - } - } - - return nodeManager->mkBitVectorType(info.d_bv_size); - } + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; -class FloatingPointToUBVTotalTypeRule { +/** + * Type rule for conversion from floating-point to unsigned bit-vector (total + * version). + */ +class FloatingPointToUBVTotalTypeRule +{ public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, - bool check) { - TRACE("FloatingPointToUBVTotalTypeRule"); - AlwaysAssert(n.getNumChildren() == 3); - - FloatingPointToUBVTotal info = n.getOperator().getConst(); - - if (check) { - TypeNode roundingModeType = n[0].getType(check); - - if (!roundingModeType.isRoundingMode()) { - throw TypeCheckingExceptionPrivate( - n, "first argument must be a rounding mode"); - } - - TypeNode operandType = n[1].getType(check); - - if (!(operandType.isFloatingPoint())) { - throw TypeCheckingExceptionPrivate(n, - "conversion to unsigned bit vector total" - "used with a sort other than " - "floating-point"); - } - - TypeNode defaultValueType = n[2].getType(check); - - if (!(defaultValueType.isBitVector()) || - !(defaultValueType.getBitVectorSize() == info)) { - throw TypeCheckingExceptionPrivate(n, - "conversion to unsigned bit vector total" - "needs a bit vector of the same length" - "as last argument"); - } - } - - return nodeManager->mkBitVectorType(info.d_bv_size); - } + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; -class FloatingPointToSBVTotalTypeRule { +/** + * Type rule for conversion from floating-point to signed bit-vector (total + * version). + */ +class FloatingPointToSBVTotalTypeRule +{ public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, - bool check) { - TRACE("FloatingPointToSBVTotalTypeRule"); - AlwaysAssert(n.getNumChildren() == 3); - - FloatingPointToSBVTotal info = n.getOperator().getConst(); - - if (check) { - TypeNode roundingModeType = n[0].getType(check); - - if (!roundingModeType.isRoundingMode()) { - throw TypeCheckingExceptionPrivate( - n, "first argument must be a rounding mode"); - } - - TypeNode operandType = n[1].getType(check); - - if (!(operandType.isFloatingPoint())) { - throw TypeCheckingExceptionPrivate(n, - "conversion to signed bit vector " - "used with a sort other than " - "floating-point"); - } - - TypeNode defaultValueType = n[2].getType(check); - - if (!(defaultValueType.isBitVector()) || - !(defaultValueType.getBitVectorSize() == info)) { - throw TypeCheckingExceptionPrivate(n, - "conversion to signed bit vector total" - "needs a bit vector of the same length" - "as last argument"); - } - } - - return nodeManager->mkBitVectorType(info.d_bv_size); - } + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; -class FloatingPointToRealTypeRule { +/** Type rule for conversion from floating-point to real. */ +class FloatingPointToRealTypeRule +{ public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, - bool check) { - TRACE("FloatingPointToRealTypeRule"); - AlwaysAssert(n.getNumChildren() == 1); - - if (check) { - TypeNode operandType = n[0].getType(check); - - if (!operandType.isFloatingPoint()) { - throw TypeCheckingExceptionPrivate( - n, "floating-point to real applied to a non floating-point sort"); - } - } - - return nodeManager->realType(); - } + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; -class FloatingPointToRealTotalTypeRule { +/** Type rule for conversion from floating-point to real (total version). */ +class FloatingPointToRealTotalTypeRule +{ public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, - bool check) { - TRACE("FloatingPointToRealTotalTypeRule"); - AlwaysAssert(n.getNumChildren() == 2); - - if (check) { - TypeNode operandType = n[0].getType(check); - - if (!operandType.isFloatingPoint()) { - throw TypeCheckingExceptionPrivate( - n, "floating-point to real total applied to a non floating-point sort"); - } - - TypeNode defaultValueType = n[1].getType(check); - - if (!defaultValueType.isReal()) { - throw TypeCheckingExceptionPrivate( - n, "floating-point to real total needs a real second argument"); - } - - } - - return nodeManager->realType(); - } + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; +/** Type rule for floating-point components of bit-width 1. */ class FloatingPointComponentBit { public: - inline static TypeNode computeType(NodeManager* nodeManager, - TNode n, - bool check) - { - TRACE("FloatingPointComponentBit"); - - if (check) - { - TypeNode operandType = n[0].getType(check); - - if (!operandType.isFloatingPoint()) - { - throw TypeCheckingExceptionPrivate(n, - "floating-point bit component " - "applied to a non floating-point " - "sort"); - } - if (!(Theory::isLeafOf(n[0], THEORY_FP) - || n[0].getKind() == kind::FLOATINGPOINT_TO_FP_REAL)) - { - throw TypeCheckingExceptionPrivate(n, - "floating-point bit component " - "applied to a non leaf / to_fp leaf " - "node"); - } - } - - return nodeManager->mkBitVectorType(1); - } + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; +/** Type rule for floating-point exponent component. */ class FloatingPointComponentExponent { public: - inline static TypeNode computeType(NodeManager* nodeManager, - TNode n, - bool check) - { - TRACE("FloatingPointComponentExponent"); - - TypeNode operandType = n[0].getType(check); - - if (check) - { - if (!operandType.isFloatingPoint()) - { - throw TypeCheckingExceptionPrivate(n, - "floating-point exponent component " - "applied to a non floating-point " - "sort"); - } - if (!(Theory::isLeafOf(n[0], THEORY_FP) - || n[0].getKind() == kind::FLOATINGPOINT_TO_FP_REAL)) - { - throw TypeCheckingExceptionPrivate(n, - "floating-point exponent component " - "applied to a non leaf / to_fp " - "node"); - } - } - -#ifdef CVC4_USE_SYMFPU - /* Need to create some symfpu objects as the size of bit-vector - * that is needed for this component is dependent on the encoding - * used (i.e. whether subnormals are forcibly normalised or not). - * Here we use types from floatingpoint.h which are the literal - * back-end but it should't make a difference. */ - FloatingPointSize fps = operandType.getConst(); - unsigned bw = FloatingPoint::getUnpackedExponentWidth(fps); -#else - unsigned bw = 2; -#endif - return nodeManager->mkBitVectorType(bw); - } + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; +/** Type rule for floating-point significand component. */ class FloatingPointComponentSignificand { public: - inline static TypeNode computeType(NodeManager* nodeManager, - TNode n, - bool check) - { - TRACE("FloatingPointComponentSignificand"); - - TypeNode operandType = n[0].getType(check); - - if (check) - { - if (!operandType.isFloatingPoint()) - { - throw TypeCheckingExceptionPrivate(n, - "floating-point significand " - "component applied to a non " - "floating-point sort"); - } - if (!(Theory::isLeafOf(n[0], THEORY_FP) - || n[0].getKind() == kind::FLOATINGPOINT_TO_FP_REAL)) - { - throw TypeCheckingExceptionPrivate(n, - "floating-point significand " - "component applied to a non leaf / " - "to_fp node"); - } - } - -#ifdef CVC4_USE_SYMFPU - /* As before we need to use some of sympfu. */ - FloatingPointSize fps = operandType.getConst(); - unsigned bw = FloatingPoint::getUnpackedSignificandWidth(fps); -#else - unsigned bw = 1; -#endif - return nodeManager->mkBitVectorType(bw); - } + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; +/** Type rule for the ROUNDINGMODE_BITBLAST operator. */ class RoundingModeBitBlast { public: - inline static TypeNode computeType(NodeManager* nodeManager, - TNode n, - bool check) - { - TRACE("RoundingModeBitBlast"); - - if (check) - { - TypeNode operandType = n[0].getType(check); - - if (!operandType.isRoundingMode()) - { - throw TypeCheckingExceptionPrivate( - n, "rounding mode bit-blast applied to a non rounding-mode sort"); - } - if (!Theory::isLeafOf(n[0], THEORY_FP)) - { - throw TypeCheckingExceptionPrivate( - n, "rounding mode bit-blast applied to a non leaf node"); - } - } - - return nodeManager->mkBitVectorType(CVC4_NUM_ROUNDING_MODES); - } + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; -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.significandWidth()); - Integer exponentValues = Integer(2).pow(fps.exponentWidth()); - exponentValues -= Integer(1); - - return Integer(5) + exponentValues * significandValues; - } -};/* class CardinalityComputer */ - - - +/** Cardinality computation for floating-point sorts. */ +class CardinalityComputer +{ + public: + static Cardinality computeCardinality(TypeNode type); +}; -}/* CVC4::theory::fp namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace fp +} // namespace theory +} // namespace CVC4 -#endif /* CVC4__THEORY__FP__THEORY_FP_TYPE_RULES_H */ +#endif