diff options
author | Martin Brain <martin.brain@cs.ox.ac.uk> | 2014-12-03 21:29:43 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-12-03 21:58:28 -0500 |
commit | cf6bc6c57dd579b8f75b7d20922eda0eaa92b2f7 (patch) | |
tree | 582afecddf7d64953d8562ab57dd915db6cc852f /src/theory/fp | |
parent | 2121eaac7e63875f1e6ba53076535d25fd561c04 (diff) |
Floating point infrastructure.
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
Diffstat (limited to 'src/theory/fp')
-rw-r--r-- | src/theory/fp/kinds | 238 | ||||
-rw-r--r-- | src/theory/fp/options | 8 | ||||
-rw-r--r-- | src/theory/fp/options_handlers.h | 14 | ||||
-rw-r--r-- | src/theory/fp/theory_fp.cpp | 104 | ||||
-rw-r--r-- | src/theory/fp/theory_fp.h | 36 | ||||
-rw-r--r-- | src/theory/fp/theory_fp_rewriter.cpp | 478 | ||||
-rw-r--r-- | src/theory/fp/theory_fp_rewriter.h | 48 | ||||
-rw-r--r-- | src/theory/fp/theory_fp_type_rules.h | 430 |
8 files changed, 1356 insertions, 0 deletions
diff --git a/src/theory/fp/kinds b/src/theory/fp/kinds new file mode 100644 index 000000000..983d5aa5c --- /dev/null +++ b/src/theory/fp/kinds @@ -0,0 +1,238 @@ +# kinds -*- sh -*- +# +# For documentation on this file format, please refer to +# src/theory/builtin/kinds. +# + +theory THEORY_FP ::CVC4::theory::fp::TheoryFp "theory/fp/theory_fp.h" +typechecker "theory/fp/theory_fp_type_rules.h" +rewriter ::CVC4::theory::fp::TheoryFpRewriter "theory/fp/theory_fp_rewriter.h" + +properties check + +# Theory content goes here. + +# constants... +constant CONST_FLOATINGPOINT \ + ::CVC4::FloatingPoint \ + ::CVC4::FloatingPointHashFunction \ + "util/floatingpoint.h" \ + "a floating-point literal" +typerule CONST_FLOATINGPOINT ::CVC4::theory::fp::FloatingPointConstantTypeRule + + +constant CONST_ROUNDINGMODE \ + ::CVC4::RoundingMode \ + ::CVC4::RoundingModeHashFunction \ + "util/floatingpoint.h" \ + "a floating-point rounding mode" +typerule CONST_ROUNDINGMODE ::CVC4::theory::fp::RoundingModeConstantTypeRule + + + +# types... +sort ROUNDINGMODE_TYPE \ + 5 \ + well-founded \ + "NodeManager::currentNM()->mkConst<RoundingMode>(RoundingMode())" \ + "expr/node_manager.h" \ + "floating-point rounding mode" + +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" + + +# operators... +operator FLOATINGPOINT_FP 3 "construct a floating-point literal from bit vectors" +typerule FLOATINGPOINT_FP ::CVC4::theory::fp::FloatingPointFPTypeRule + + + +operator FLOATINGPOINT_EQ 2: "floating-point equality" +typerule FLOATINGPOINT_EQ ::CVC4::theory::fp::FloatingPointTestTypeRule + +operator FLOATINGPOINT_ABS 1 "floating-point absolute value" +typerule FLOATINGPOINT_ABS ::CVC4::theory::fp::FloatingPointOperationTypeRule + +operator FLOATINGPOINT_NEG 1 "floating-point negation" +typerule FLOATINGPOINT_NEG ::CVC4::theory::fp::FloatingPointOperationTypeRule + +operator FLOATINGPOINT_PLUS 3 "floating-point addition" +typerule FLOATINGPOINT_PLUS ::CVC4::theory::fp::FloatingPointRoundingOperationTypeRule + +operator FLOATINGPOINT_SUB 3 "floating-point sutraction" +typerule FLOATINGPOINT_SUB ::CVC4::theory::fp::FloatingPointRoundingOperationTypeRule + +operator FLOATINGPOINT_MULT 3 "floating-point multiply" +typerule FLOATINGPOINT_MULT ::CVC4::theory::fp::FloatingPointRoundingOperationTypeRule + +operator FLOATINGPOINT_DIV 3 "floating-point division" +typerule FLOATINGPOINT_DIV ::CVC4::theory::fp::FloatingPointRoundingOperationTypeRule + +operator FLOATINGPOINT_FMA 4 "floating-point fused multiply and add" +typerule FLOATINGPOINT_FMA ::CVC4::theory::fp::FloatingPointRoundingOperationTypeRule + +operator FLOATINGPOINT_SQRT 2 "floating-point square root" +typerule FLOATINGPOINT_SQRT ::CVC4::theory::fp::FloatingPointRoundingOperationTypeRule + +operator FLOATINGPOINT_REM 2 "floating-point remainder" +typerule FLOATINGPOINT_REM ::CVC4::theory::fp::FloatingPointOperationTypeRule + +operator FLOATINGPOINT_RTI 2 "floating-point round to integral" +typerule FLOATINGPOINT_RTI ::CVC4::theory::fp::FloatingPointRoundingOperationTypeRule + +operator FLOATINGPOINT_MIN 2 "floating-point minimum" +typerule FLOATINGPOINT_MIN ::CVC4::theory::fp::FloatingPointOperationTypeRule + +operator FLOATINGPOINT_MAX 2 "floating-point maximum" +typerule FLOATINGPOINT_MAX ::CVC4::theory::fp::FloatingPointOperationTypeRule + + +operator FLOATINGPOINT_LEQ 2 "floating-point less than or equal" +typerule FLOATINGPOINT_LEQ ::CVC4::theory::fp::FloatingPointTestTypeRule + +operator FLOATINGPOINT_LT 2 "floating-point less than" +typerule FLOATINGPOINT_LT ::CVC4::theory::fp::FloatingPointTestTypeRule + +operator FLOATINGPOINT_GEQ 2 "floating-point greater than or equal" +typerule FLOATINGPOINT_GEQ ::CVC4::theory::fp::FloatingPointTestTypeRule + +operator FLOATINGPOINT_GT 2 "floating-point greater than" +typerule FLOATINGPOINT_GT ::CVC4::theory::fp::FloatingPointTestTypeRule + + + +operator FLOATINGPOINT_ISN 1 "floating-point is normal" +typerule FLOATINGPOINT_ISN ::CVC4::theory::fp::FloatingPointTestTypeRule + +operator FLOATINGPOINT_ISSN 1 "floating-point is sub-normal" +typerule FLOATINGPOINT_ISSN ::CVC4::theory::fp::FloatingPointTestTypeRule + +operator FLOATINGPOINT_ISZ 1 "floating-point is zero" +typerule FLOATINGPOINT_ISZ ::CVC4::theory::fp::FloatingPointTestTypeRule + +operator FLOATINGPOINT_ISINF 1 "floating-point is infinite" +typerule FLOATINGPOINT_ISINF ::CVC4::theory::fp::FloatingPointTestTypeRule + +operator FLOATINGPOINT_ISNAN 1 "floating-point is NaN" +typerule FLOATINGPOINT_ISNAN ::CVC4::theory::fp::FloatingPointTestTypeRule + +operator FLOATINGPOINT_ISNEG 1 "floating-point is negative" +typerule FLOATINGPOINT_ISNEG ::CVC4::theory::fp::FloatingPointTestTypeRule + +operator FLOATINGPOINT_ISPOS 1 "floating-point is positive" +typerule FLOATINGPOINT_ISPOS ::CVC4::theory::fp::FloatingPointTestTypeRule + + + +constant FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP \ + ::CVC4::FloatingPointToFPIEEEBitVector \ + "::CVC4::FloatingPointConvertSortHashFunction<0x1>" \ + "util/floatingpoint.h" \ + "operator for to_fp from bit vector" +typerule FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP ::CVC4::theory::fp::FloatingPointParametricOpTypeRule + +parameterized FLOATINGPOINT_TO_FP_IEEE_BITVECTOR FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP 1 "convert an IEEE-754 bit vector to floating-point" +typerule FLOATINGPOINT_TO_FP_IEEE_BITVECTOR ::CVC4::theory::fp::FloatingPointToFPIEEEBitVectorTypeRule + + + +constant FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP \ + ::CVC4::FloatingPointToFPFloatingPoint \ + "::CVC4::FloatingPointConvertSortHashFunction<0x2>" \ + "util/floatingpoint.h" \ + "operator for to_fp from floating point" +typerule FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP ::CVC4::theory::fp::FloatingPointParametricOpTypeRule + +parameterized FLOATINGPOINT_TO_FP_FLOATINGPOINT FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP 2 "convert between floating-point sorts" +typerule FLOATINGPOINT_TO_FP_FLOATINGPOINT ::CVC4::theory::fp::FloatingPointToFPFloatingPointTypeRule + + + + +constant FLOATINGPOINT_TO_FP_REAL_OP \ + ::CVC4::FloatingPointToFPReal \ + "::CVC4::FloatingPointConvertSortHashFunction<0x4>" \ + "util/floatingpoint.h" \ + "operator for to_fp from real" +typerule FLOATINGPOINT_TO_FP_REAL_OP ::CVC4::theory::fp::FloatingPointParametricOpTypeRule + +parameterized FLOATINGPOINT_TO_FP_REAL FLOATINGPOINT_TO_FP_REAL_OP 2 "convert a real to floating-point" +typerule FLOATINGPOINT_TO_FP_REAL ::CVC4::theory::fp::FloatingPointToFPRealTypeRule + + + +constant FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP \ + ::CVC4::FloatingPointToFPSignedBitVector \ + "::CVC4::FloatingPointConvertSortHashFunction<0x8>" \ + "util/floatingpoint.h" \ + "operator for to_fp from signed bit vector" +typerule FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP ::CVC4::theory::fp::FloatingPointParametricOpTypeRule + +parameterized FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP 2 "convert a signed bit vector to floating-point" +typerule FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR ::CVC4::theory::fp::FloatingPointToFPSignedBitVectorTypeRule + + + +constant FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP \ + ::CVC4::FloatingPointToFPUnsignedBitVector \ + "::CVC4::FloatingPointConvertSortHashFunction<0x10>" \ + "util/floatingpoint.h" \ + "operator for to_fp from unsigned bit vector" +typerule FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP ::CVC4::theory::fp::FloatingPointParametricOpTypeRule + + +parameterized FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP 2 "convert an unsigned bit vector to floating-point" +typerule FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR ::CVC4::theory::fp::FloatingPointToFPUnsignedBitVectorTypeRule + + + +constant FLOATINGPOINT_TO_FP_GENERIC_OP \ + ::CVC4::FloatingPointToFPGeneric \ + "::CVC4::FloatingPointConvertSortHashFunction<0x11>" \ + "util/floatingpoint.h" \ + "operator for a generic to_fp" +typerule FLOATINGPOINT_TO_FP_GENERIC_OP ::CVC4::theory::fp::FloatingPointParametricOpTypeRule + + +parameterized FLOATINGPOINT_TO_FP_GENERIC FLOATINGPOINT_TO_FP_GENERIC_OP 1:2 "a generic conversion to floating-point, used in parsing only" +typerule FLOATINGPOINT_TO_FP_GENERIC ::CVC4::theory::fp::FloatingPointToFPGenericTypeRule + + + + + +constant FLOATINGPOINT_TO_UBV_OP \ + ::CVC4::FloatingPointToUBV \ + "::CVC4::FloatingPointToBVHashFunction<0x1>" \ + "util/floatingpoint.h" \ + "operator for to_ubv" +typerule FLOATINGPOINT_TO_UBV_OP ::CVC4::theory::fp::FloatingPointParametricOpTypeRule + +parameterized FLOATINGPOINT_TO_UBV FLOATINGPOINT_TO_UBV_OP 2 "convert a floating-point value to an unsigned bit vector" +typerule FLOATINGPOINT_TO_UBV ::CVC4::theory::fp::FloatingPointToUBVTypeRule + + + +constant FLOATINGPOINT_TO_SBV_OP \ + ::CVC4::FloatingPointToSBV \ + "::CVC4::FloatingPointToBVHashFunction<0x2>" \ + "util/floatingpoint.h" \ + "operator for to_sbv" +typerule FLOATINGPOINT_TO_SBV_OP ::CVC4::theory::fp::FloatingPointParametricOpTypeRule + +parameterized FLOATINGPOINT_TO_SBV FLOATINGPOINT_TO_SBV_OP 2 "convert a floating-point value to a signed bit vector" +typerule FLOATINGPOINT_TO_SBV ::CVC4::theory::fp::FloatingPointToSBVTypeRule + + +operator FLOATINGPOINT_TO_REAL 1 "floating-point to real" +typerule FLOATINGPOINT_TO_REAL ::CVC4::theory::fp::FloatingPointToRealTypeRule + + +endtheory diff --git a/src/theory/fp/options b/src/theory/fp/options new file mode 100644 index 000000000..3fee94d1d --- /dev/null +++ b/src/theory/fp/options @@ -0,0 +1,8 @@ +# +# Option specification file for CVC4 +# See src/options/base_options for a description of this file format +# + +module FP "theory/fp/options.h" Fp + +endmodule diff --git a/src/theory/fp/options_handlers.h b/src/theory/fp/options_handlers.h new file mode 100644 index 000000000..f1a86e396 --- /dev/null +++ b/src/theory/fp/options_handlers.h @@ -0,0 +1,14 @@ +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__FP__OPTIONS_HANDLERS_H +#define __CVC4__THEORY__FP__OPTIONS_HANDLERS_H + +namespace CVC4 { +namespace theory { +namespace fp { + +}/* CVC4::theory::fp namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__FP__OPTIONS_HANDLERS_H */ diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp new file mode 100644 index 000000000..6400fec38 --- /dev/null +++ b/src/theory/fp/theory_fp.cpp @@ -0,0 +1,104 @@ +#include "theory/fp/theory_fp.h" + +using namespace std; + +namespace CVC4 { +namespace theory { +namespace fp { + +namespace removeToFPGeneric { + + Node removeToFPGeneric (TNode node) { + Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_GENERIC); + + FloatingPointToFPGeneric info = node.getOperator().getConst<FloatingPointToFPGeneric>(); + + size_t children = node.getNumChildren(); + + Node op; + + if (children == 1) { + op = NodeManager::currentNM()->mkConst(FloatingPointToFPIEEEBitVector(info.t.exponent(), + info.t.significand())); + return NodeManager::currentNM()->mkNode(op, node[0]); + + } else { + Assert(children == 2); + Assert(node[0].getType().isRoundingMode()); + + TypeNode t = node[1].getType(); + + if (t.isFloatingPoint()) { + op = NodeManager::currentNM()->mkConst(FloatingPointToFPFloatingPoint(info.t.exponent(), + info.t.significand())); + } else if (t.isReal()) { + op = NodeManager::currentNM()->mkConst(FloatingPointToFPReal(info.t.exponent(), + info.t.significand())); + } else if (t.isBitVector()) { + op = NodeManager::currentNM()->mkConst(FloatingPointToFPSignedBitVector(info.t.exponent(), + info.t.significand())); + + } else { + throw TypeCheckingExceptionPrivate(node, "cannot rewrite to_fp generic due to incorrect type of second argument"); + } + + return NodeManager::currentNM()->mkNode(op, node[0], node[1]); + } + + Unreachable("to_fp generic not rewritten"); + } +} + + +/** Constructs a new instance of TheoryFp w.r.t. the provided contexts. */ +TheoryFp::TheoryFp(context::Context* c, + context::UserContext* u, + OutputChannel& out, + Valuation valuation, + const LogicInfo& logicInfo) : + Theory(THEORY_FP, c, u, out, valuation, logicInfo) { +}/* TheoryFp::TheoryFp() */ + + +Node TheoryFp::expandDefinition(LogicRequest &, Node node) { + Trace("fp-expandDefinition") << "TheoryFp::expandDefinition(): " << node << std::endl; + + if (node.getKind() == kind::FLOATINGPOINT_TO_FP_GENERIC) { + Node res(removeToFPGeneric::removeToFPGeneric(node)); + + Trace("fp-expandDefinition") << "TO_FP_GENERIC rewritten to " << res << std::endl; + + return res; + } else { + return node; + } +} + + +void TheoryFp::check(Effort level) { + if (done() && !fullEffort(level)) { + return; + } + + while(!done()) { + // Get all the assertions + Assertion assertion = get(); + TNode fact = assertion.assertion; + + Debug("fp") << "TheoryFp::check(): processing " << fact << std::endl; + + // Do the work + switch(fact.getKind()) { + + /* cases for all the theory's kinds go here... */ + + default: + Unhandled(fact.getKind()); + } + } + +}/* TheoryFp::check() */ + +}/* CVC4::theory::fp namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h new file mode 100644 index 000000000..6fb41685f --- /dev/null +++ b/src/theory/fp/theory_fp.h @@ -0,0 +1,36 @@ +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__FP__THEORY_FP_H +#define __CVC4__THEORY__FP__THEORY_FP_H + +#include "theory/theory.h" + +namespace CVC4 { +namespace theory { +namespace fp { + +class TheoryFp : public Theory { +public: + + /** Constructs a new instance of TheoryFp w.r.t. the provided contexts. */ + TheoryFp(context::Context* c, + context::UserContext* u, + OutputChannel& out, + Valuation valuation, + const LogicInfo& logicInfo); + + Node expandDefinition(LogicRequest &, Node node); + + void check(Effort); + + std::string identify() const { + return "THEORY_FP"; + } + +};/* class TheoryFp */ + +}/* CVC4::theory::fp namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__FP__THEORY_FP_H */ diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp new file mode 100644 index 000000000..0c41e8ff7 --- /dev/null +++ b/src/theory/fp/theory_fp_rewriter.cpp @@ -0,0 +1,478 @@ +/********************* */ +/*! \file theory_fp_rewriter.cpp + ** \verbatim + ** Original author: Martin Brain + ** Major contributors: + ** Minor contributors (to current version): + ** This file is part of the CVC4 project. + ** Copyright (c) 2013 University of Oxford + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Rewrite rules for floating point theories. ]] + ** + ** \todo [[ Constant folding + ** Push negations up 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.abs (fp.neg x)) --> (fp.abs x) + ** (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 + ** ]] + **/ + +#include "theory/fp/theory_fp_rewriter.h" + +#include "util/cvc4_assert.h" + +#include <algorithm> + +namespace CVC4 { +namespace theory { +namespace fp { + +namespace rewrite { + /** Rewrite rules **/ + + RewriteResponse notFP (TNode node, bool) { + Unreachable("non floating-point kind (%d) in floating point rewrite?",node.getKind()); + } + + RewriteResponse identity (TNode node, bool) { + return RewriteResponse(REWRITE_DONE, node); + } + + RewriteResponse type (TNode node, bool) { + Unreachable("sort kind (%d) found in expression?",node.getKind()); + return RewriteResponse(REWRITE_DONE, node); + } + + RewriteResponse removeDoubleNegation (TNode node, bool) { + Assert(node.getKind() == kind::FLOATINGPOINT_NEG); + if (node[0].getKind() == kind::FLOATINGPOINT_NEG) { + RewriteResponse(REWRITE_AGAIN, node[0][0]); + } + + return RewriteResponse(REWRITE_DONE, node); + } + + RewriteResponse convertSubtractionToAddition (TNode node, bool) { + Assert(node.getKind() == kind::FLOATINGPOINT_SUB); + Node negation = NodeManager::currentNM()->mkNode(kind::FLOATINGPOINT_NEG,node[2]); + Node addition = NodeManager::currentNM()->mkNode(kind::FLOATINGPOINT_PLUS,node[0],node[1],negation); + return RewriteResponse(REWRITE_DONE, addition); + } + + + /* Implies (fp.eq x x) --> (not (isNaN x)) + */ + + RewriteResponse ieeeEqToEq (TNode node, bool) { + Assert(node.getKind() == kind::FLOATINGPOINT_EQ); + NodeManager *nm = NodeManager::currentNM(); + + return RewriteResponse(REWRITE_DONE, + nm->mkNode(kind::AND, + nm->mkNode(kind::AND, + nm->mkNode(kind::NOT, nm->mkNode(kind::FLOATINGPOINT_ISNAN, node[0])), + nm->mkNode(kind::NOT, nm->mkNode(kind::FLOATINGPOINT_ISNAN, node[1]))), + nm->mkNode(kind::OR, + nm->mkNode(kind::EQUAL, node[0], node[1]), + nm->mkNode(kind::AND, + nm->mkNode(kind::FLOATINGPOINT_ISZ, node[0]), + nm->mkNode(kind::FLOATINGPOINT_ISZ, node[1]))))); + } + + + RewriteResponse geqToleq (TNode node, bool) { + Assert(node.getKind() == kind::FLOATINGPOINT_GEQ); + return RewriteResponse(REWRITE_DONE,NodeManager::currentNM()->mkNode(kind::FLOATINGPOINT_LEQ,node[1],node[0])); + } + + RewriteResponse gtTolt (TNode node, bool) { + Assert(node.getKind() == kind::FLOATINGPOINT_GT); + return RewriteResponse(REWRITE_DONE,NodeManager::currentNM()->mkNode(kind::FLOATINGPOINT_LT,node[1],node[0])); + } + + RewriteResponse removed (TNode node, bool) { + Unreachable("kind (%d) should have been removed?",node.getKind()); + return RewriteResponse(REWRITE_DONE, node); + } + + RewriteResponse variable (TNode node, bool) { + // We should only get floating point and rounding mode variables to rewrite. + TypeNode tn = node.getType(true); + Assert(tn.isFloatingPoint() || tn.isRoundingMode()); + + // Not that we do anything with them... + return RewriteResponse(REWRITE_DONE, node); + } + + RewriteResponse equal (TNode node, bool isPreRewrite) { + // We should only get equalities of floating point or rounding mode types. + Assert(node.getKind() == kind::EQUAL); + + TypeNode tn = node[0].getType(true); + + Assert(tn.isFloatingPoint() || tn.isRoundingMode()); + Assert(tn == node[1].getType(true)); // Should be ensured by the typing rules + + if (node[0] == node[1]) { + return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true)); + } else if (!isPreRewrite && (node[0] > node[1])) { + Node normal = NodeManager::currentNM()->mkNode(kind::EQUAL,node[1],node[0]); + return RewriteResponse(REWRITE_DONE, normal); + } else { + return RewriteResponse(REWRITE_DONE, node); + } + } + + RewriteResponse convertFromRealLiteral (TNode node, bool) { + Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_REAL); + + // \todo Honour the rounding mode and work for something other than doubles! + + if (node[1].getKind() == kind::CONST_RATIONAL) { + TNode op = node.getOperator(); + const FloatingPointToFPReal ¶m = op.getConst<FloatingPointToFPReal>(); + Node lit = + NodeManager::currentNM()->mkConst(FloatingPoint(param.t.exponent(), + param.t.significand(), + node[1].getConst<Rational>().getDouble())); + + return RewriteResponse(REWRITE_DONE, lit); + } else { + return RewriteResponse(REWRITE_DONE, node); + } + } + + RewriteResponse convertFromIEEEBitVectorLiteral (TNode node, bool) { + Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR); + + // \todo Handle arbitrary length bit vectors without using strings! + + if (node[0].getKind() == kind::CONST_BITVECTOR) { + TNode op = node.getOperator(); + const FloatingPointToFPIEEEBitVector ¶m = op.getConst<FloatingPointToFPIEEEBitVector>(); + const BitVector &bv = node[0].getConst<BitVector>(); + std::string bitString(bv.toString()); + + Node lit = + NodeManager::currentNM()->mkConst(FloatingPoint(param.t.exponent(), + param.t.significand(), + bitString)); + + return RewriteResponse(REWRITE_DONE, lit); + } else { + return RewriteResponse(REWRITE_DONE, node); + } + } + + RewriteResponse convertFromLiteral (TNode node, bool) { + Assert(node.getKind() == kind::FLOATINGPOINT_FP); + + // \todo Handle arbitrary length bit vectors without using strings! + + if ((node[0].getKind() == kind::CONST_BITVECTOR) && + (node[1].getKind() == kind::CONST_BITVECTOR) && + (node[2].getKind() == kind::CONST_BITVECTOR)) { + + BitVector bv(node[0].getConst<BitVector>()); + bv = bv.concat(node[1].getConst<BitVector>()); + bv = bv.concat(node[2].getConst<BitVector>()); + + std::string bitString(bv.toString()); + std::reverse(bitString.begin(), bitString.end()); + + // +1 to support the hidden bit + Node lit = + NodeManager::currentNM()->mkConst(FloatingPoint(node[1].getConst<BitVector>().getSize(), + node[2].getConst<BitVector>().getSize() + 1, + bitString)); + + return RewriteResponse(REWRITE_DONE, lit); + } else { + return RewriteResponse(REWRITE_DONE, node); + } + } + + // Note these cannot be assumed to be symmetric for +0/-0, thus no symmetry reorder + RewriteResponse compactMinMax (TNode node, bool isPreRewrite) { + Kind k = node.getKind(); + + Assert((k == kind::FLOATINGPOINT_MIN) || (k == kind::FLOATINGPOINT_MAX)); + + if (node[0] == node[1]) { + return RewriteResponse(REWRITE_DONE, node[0]); + } else { + return RewriteResponse(REWRITE_DONE, node); + } + } + + + RewriteResponse reorderFPEquality (TNode node, bool isPreRewrite) { + Assert(node.getKind() == kind::FLOATINGPOINT_EQ); + Assert(!isPreRewrite); // Likely redundant in pre-rewrite + + if (node[0] > node[1]) { + Node normal = NodeManager::currentNM()->mkNode(kind::FLOATINGPOINT_EQ,node[1],node[0]); + return RewriteResponse(REWRITE_DONE, normal); + } else { + return RewriteResponse(REWRITE_DONE, node); + } + } + + RewriteResponse reorderBinaryOperation (TNode node, bool isPreRewrite) { + Kind k = node.getKind(); + Assert((k == kind::FLOATINGPOINT_PLUS) || (k == kind::FLOATINGPOINT_MULT)); + Assert(!isPreRewrite); // Likely redundant in pre-rewrite + + if (node[1] > node[2]) { + Node normal = NodeManager::currentNM()->mkNode(k,node[0],node[2],node[1]); + return RewriteResponse(REWRITE_DONE, normal); + } else { + return RewriteResponse(REWRITE_DONE, node); + } + } + + RewriteResponse reorderFMA (TNode node, bool isPreRewrite) { + Assert(node.getKind() == kind::FLOATINGPOINT_FMA); + Assert(!isPreRewrite); // Likely redundant in pre-rewrite + + if (node[1] > node[2]) { + Node normal = NodeManager::currentNM()->mkNode(kind::FLOATINGPOINT_FMA,node[0],node[2],node[1],node[3]); + return RewriteResponse(REWRITE_DONE, normal); + } else { + return RewriteResponse(REWRITE_DONE, node); + } + } + + RewriteResponse removeSignOperations (TNode node, bool isPreRewrite) { + Assert(node.getKind() == kind::FLOATINGPOINT_ISN || + node.getKind() == kind::FLOATINGPOINT_ISSN || + node.getKind() == kind::FLOATINGPOINT_ISZ || + node.getKind() == kind::FLOATINGPOINT_ISINF || + node.getKind() == kind::FLOATINGPOINT_ISNAN); + Assert(node.getNumChildren() == 1); + + Kind childKind(node[0].getKind()); + + if ((childKind == kind::FLOATINGPOINT_NEG) || + (childKind == kind::FLOATINGPOINT_ABS)) { + + Node rewritten = NodeManager::currentNM()->mkNode(node.getKind(),node[0][0]); + return RewriteResponse(REWRITE_AGAIN, rewritten); + } else { + return RewriteResponse(REWRITE_DONE, node); + } + } + + +}; /* CVC4::theory::fp::rewrite */ + +RewriteFunction TheoryFpRewriter::preRewriteTable[kind::LAST_KIND]; +RewriteFunction TheoryFpRewriter::postRewriteTable[kind::LAST_KIND]; + + + /** + * Initialize the rewriter. + */ + void TheoryFpRewriter::init() { + + /* Set up the pre-rewrite dispatch table */ + for (unsigned i = 0; i < kind::LAST_KIND; ++i) { + preRewriteTable[i] = rewrite::notFP; + } + + /******** Constants ********/ + /* No rewriting possible for constants */ + preRewriteTable[kind::CONST_FLOATINGPOINT] = rewrite::identity; + preRewriteTable[kind::CONST_ROUNDINGMODE] = rewrite::identity; + + /******** Sorts(?) ********/ + /* These kinds should only appear in types */ + //preRewriteTable[kind::ROUNDINGMODE_TYPE] = rewrite::type; + preRewriteTable[kind::FLOATINGPOINT_TYPE] = rewrite::type; + + /******** Operations ********/ + preRewriteTable[kind::FLOATINGPOINT_FP] = rewrite::identity; + preRewriteTable[kind::FLOATINGPOINT_ABS] = rewrite::identity; + preRewriteTable[kind::FLOATINGPOINT_NEG] = rewrite::removeDoubleNegation; + preRewriteTable[kind::FLOATINGPOINT_PLUS] = rewrite::identity; + preRewriteTable[kind::FLOATINGPOINT_SUB] = rewrite::convertSubtractionToAddition; + preRewriteTable[kind::FLOATINGPOINT_MULT] = rewrite::identity; + preRewriteTable[kind::FLOATINGPOINT_DIV] = rewrite::identity; + preRewriteTable[kind::FLOATINGPOINT_FMA] = rewrite::identity; + preRewriteTable[kind::FLOATINGPOINT_SQRT] = rewrite::identity; + preRewriteTable[kind::FLOATINGPOINT_REM] = rewrite::identity; + preRewriteTable[kind::FLOATINGPOINT_RTI] = rewrite::identity; + preRewriteTable[kind::FLOATINGPOINT_MIN] = rewrite::compactMinMax; + preRewriteTable[kind::FLOATINGPOINT_MAX] = rewrite::compactMinMax; + + /******** Comparisons ********/ + preRewriteTable[kind::FLOATINGPOINT_EQ] = rewrite::ieeeEqToEq; + preRewriteTable[kind::FLOATINGPOINT_LEQ] = rewrite::identity; + preRewriteTable[kind::FLOATINGPOINT_LT] = rewrite::identity; + preRewriteTable[kind::FLOATINGPOINT_GEQ] = rewrite::geqToleq; + preRewriteTable[kind::FLOATINGPOINT_GT] = rewrite::gtTolt; + + /******** Classifications ********/ + preRewriteTable[kind::FLOATINGPOINT_ISN] = rewrite::identity; + preRewriteTable[kind::FLOATINGPOINT_ISSN] = rewrite::identity; + preRewriteTable[kind::FLOATINGPOINT_ISZ] = rewrite::identity; + preRewriteTable[kind::FLOATINGPOINT_ISINF] = rewrite::identity; + preRewriteTable[kind::FLOATINGPOINT_ISNAN] = rewrite::identity; + preRewriteTable[kind::FLOATINGPOINT_ISNEG] = rewrite::identity; + preRewriteTable[kind::FLOATINGPOINT_ISPOS] = rewrite::identity; + + /******** Conversions ********/ + preRewriteTable[kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR] = rewrite::identity; + preRewriteTable[kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT] = rewrite::identity; + preRewriteTable[kind::FLOATINGPOINT_TO_FP_REAL] = rewrite::identity; + preRewriteTable[kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR] = rewrite::identity; + preRewriteTable[kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR] = rewrite::identity; + preRewriteTable[kind::FLOATINGPOINT_TO_FP_GENERIC] = rewrite::removed; + preRewriteTable[kind::FLOATINGPOINT_TO_UBV] = rewrite::identity; + preRewriteTable[kind::FLOATINGPOINT_TO_SBV] = rewrite::identity; + preRewriteTable[kind::FLOATINGPOINT_TO_REAL] = rewrite::identity; + + /******** Variables ********/ + preRewriteTable[kind::VARIABLE] = rewrite::variable; + preRewriteTable[kind::BOUND_VARIABLE] = rewrite::variable; + + preRewriteTable[kind::EQUAL] = rewrite::equal; + + + + + /* Set up the post-rewrite dispatch table */ + for (unsigned i = 0; i < kind::LAST_KIND; ++i) { + postRewriteTable[i] = rewrite::notFP; + } + + /******** Constants ********/ + /* No rewriting possible for constants */ + postRewriteTable[kind::CONST_FLOATINGPOINT] = rewrite::identity; + postRewriteTable[kind::CONST_ROUNDINGMODE] = rewrite::identity; + + /******** Sorts(?) ********/ + /* These kinds should only appear in types */ + //postRewriteTable[kind::ROUNDINGMODE_TYPE] = rewrite::type; + postRewriteTable[kind::FLOATINGPOINT_TYPE] = rewrite::type; + + /******** Operations ********/ + postRewriteTable[kind::FLOATINGPOINT_FP] = rewrite::convertFromLiteral; + postRewriteTable[kind::FLOATINGPOINT_ABS] = rewrite::identity; + postRewriteTable[kind::FLOATINGPOINT_NEG] = rewrite::removeDoubleNegation; + postRewriteTable[kind::FLOATINGPOINT_PLUS] = rewrite::reorderBinaryOperation; + postRewriteTable[kind::FLOATINGPOINT_SUB] = rewrite::removed; + postRewriteTable[kind::FLOATINGPOINT_MULT] = rewrite::reorderBinaryOperation; + postRewriteTable[kind::FLOATINGPOINT_DIV] = rewrite::identity; + postRewriteTable[kind::FLOATINGPOINT_FMA] = rewrite::reorderFMA; + postRewriteTable[kind::FLOATINGPOINT_SQRT] = rewrite::identity; + postRewriteTable[kind::FLOATINGPOINT_REM] = rewrite::identity; + postRewriteTable[kind::FLOATINGPOINT_RTI] = rewrite::identity; + postRewriteTable[kind::FLOATINGPOINT_MIN] = rewrite::compactMinMax; + postRewriteTable[kind::FLOATINGPOINT_MAX] = rewrite::compactMinMax; + + /******** Comparisons ********/ + postRewriteTable[kind::FLOATINGPOINT_EQ] = rewrite::removed; + postRewriteTable[kind::FLOATINGPOINT_LEQ] = rewrite::identity; + postRewriteTable[kind::FLOATINGPOINT_LT] = rewrite::identity; + postRewriteTable[kind::FLOATINGPOINT_GEQ] = rewrite::removed; + postRewriteTable[kind::FLOATINGPOINT_GT] = rewrite::removed; + + /******** Classifications ********/ + postRewriteTable[kind::FLOATINGPOINT_ISN] = rewrite::removeSignOperations; + postRewriteTable[kind::FLOATINGPOINT_ISSN] = rewrite::removeSignOperations; + postRewriteTable[kind::FLOATINGPOINT_ISZ] = rewrite::removeSignOperations; + postRewriteTable[kind::FLOATINGPOINT_ISINF] = rewrite::removeSignOperations; + postRewriteTable[kind::FLOATINGPOINT_ISNAN] = rewrite::removeSignOperations; + postRewriteTable[kind::FLOATINGPOINT_ISNEG] = rewrite::identity; + postRewriteTable[kind::FLOATINGPOINT_ISPOS] = rewrite::identity; + + /******** Conversions ********/ + postRewriteTable[kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR] = rewrite::convertFromIEEEBitVectorLiteral; + postRewriteTable[kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT] = rewrite::identity; + postRewriteTable[kind::FLOATINGPOINT_TO_FP_REAL] = rewrite::convertFromRealLiteral; + postRewriteTable[kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR] = rewrite::identity; + postRewriteTable[kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR] = rewrite::identity; + postRewriteTable[kind::FLOATINGPOINT_TO_FP_GENERIC] = rewrite::removed; + postRewriteTable[kind::FLOATINGPOINT_TO_UBV] = rewrite::identity; + postRewriteTable[kind::FLOATINGPOINT_TO_SBV] = rewrite::identity; + postRewriteTable[kind::FLOATINGPOINT_TO_REAL] = rewrite::identity; + + /******** Variables ********/ + postRewriteTable[kind::VARIABLE] = rewrite::variable; + postRewriteTable[kind::BOUND_VARIABLE] = rewrite::variable; + + postRewriteTable[kind::EQUAL] = rewrite::equal; + + + } + + + + + /** + * Rewrite a node into the normal form for the theory of fp + * in pre-order (really topological order)---meaning that the + * children may not be in the normal form. This is an optimization + * for theories with cancelling terms (e.g., 0 * (big-nasty-expression) + * in arithmetic rewrites to 0 without the need to look at the big + * nasty expression). Since it's only an optimization, the + * implementation here can do nothing. + */ + + RewriteResponse TheoryFpRewriter::preRewrite(TNode node) { + Trace("fp-rewrite") << "TheoryFpRewriter::preRewrite(): " << node << std::endl; + RewriteResponse res = preRewriteTable [node.getKind()] (node, true); + if (res.node != node) { + Debug("fp-rewrite") << "TheoryFpRewriter::preRewrite(): before " << node << std::endl; + Debug("fp-rewrite") << "TheoryFpRewriter::preRewrite(): after " << res.node << std::endl; + } + return res; + } + + + /** + * Rewrite a node into the normal form for the theory of fp. + * Called in post-order (really reverse-topological order) when + * traversing the expression DAG during rewriting. This is the + * main function of the rewriter, and because of the ordering, + * it can assume its children are all rewritten already. + * + * This function can return one of three rewrite response codes + * along with the rewritten node: + * + * REWRITE_DONE indicates that no more rewriting is needed. + * REWRITE_AGAIN means that the top-level expression should be + * rewritten again, but that its children are in final form. + * REWRITE_AGAIN_FULL means that the entire returned expression + * should be rewritten again (top-down with preRewrite(), then + * bottom-up with postRewrite()). + * + * Even if this function returns REWRITE_DONE, if the returned + * expression belongs to a different theory, it will be fully + * rewritten by that theory's rewriter. + */ + + RewriteResponse TheoryFpRewriter::postRewrite(TNode node) { + Trace("fp-rewrite") << "TheoryFpRewriter::postRewrite(): " << node << std::endl; + RewriteResponse res = postRewriteTable [node.getKind()] (node, false); + if (res.node != node) { + Debug("fp-rewrite") << "TheoryFpRewriter::postRewrite(): before " << node << std::endl; + Debug("fp-rewrite") << "TheoryFpRewriter::postRewrite(): after " << res.node << std::endl; + } + return res; + } + + +}/* CVC4::theory::fp namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + diff --git a/src/theory/fp/theory_fp_rewriter.h b/src/theory/fp/theory_fp_rewriter.h new file mode 100644 index 000000000..8a8f1c933 --- /dev/null +++ b/src/theory/fp/theory_fp_rewriter.h @@ -0,0 +1,48 @@ +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__FP__THEORY_FP_REWRITER_H +#define __CVC4__THEORY__FP__THEORY_FP_REWRITER_H + +#include "theory/rewriter.h" + +namespace CVC4 { +namespace theory { +namespace fp { + +typedef RewriteResponse (*RewriteFunction) (TNode, bool); + +class TheoryFpRewriter { + protected : + static RewriteFunction preRewriteTable[kind::LAST_KIND]; + static RewriteFunction postRewriteTable[kind::LAST_KIND]; + + public: + + static RewriteResponse preRewrite(TNode node); + static RewriteResponse postRewrite(TNode node); + + + /** + * Rewrite an equality, in case special handling is required. + */ + static Node rewriteEquality(TNode equality) { + // often this will suffice + return postRewrite(equality).node; + } + + static void init(); + + /** + * Shut down the rewriter. + */ + static inline void shutdown() { + // nothing to do + } + +};/* class TheoryFpRewriter */ + +}/* CVC4::theory::fp namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__FP__THEORY_FP_REWRITER_H */ diff --git a/src/theory/fp/theory_fp_type_rules.h b/src/theory/fp/theory_fp_type_rules.h new file mode 100644 index 000000000..2c9a67984 --- /dev/null +++ b/src/theory/fp/theory_fp_type_rules.h @@ -0,0 +1,430 @@ +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__FP__THEORY_FP_TYPE_RULES_H +#define __CVC4__THEORY__FP__THEORY_FP_TYPE_RULES_H + +namespace CVC4 { +namespace theory { +namespace fp { + +#define TRACE(FUNCTION) Trace("fp-type") << FUNCTION "::computeType(" << check << "): " << n << std::endl + + +class FloatingPointConstantTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + TRACE("FloatingPointConstantTypeRule"); + + const FloatingPoint &f = n.getConst<FloatingPoint>(); + + if (check) { + if (!(validExponentSize(f.t.exponent()))) { + throw TypeCheckingExceptionPrivate(n, "constant with invalid exponent size"); + } + if (!(validSignificandSize(f.t.significand()))) { + throw TypeCheckingExceptionPrivate(n, "constant with invalid significand size"); + } + } + return nodeManager->mkFloatingPointType(f.t); + } +}; + + +class RoundingModeConstantTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + TRACE("RoundingModeConstantTypeRule"); + + // Nothing to check! + return nodeManager->roundingModeType(); + } +}; + + + +class FloatingPointFPTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + 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); + } + +}; + + +class FloatingPointTestTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + 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(); + } +}; + + +class FloatingPointOperationTypeRule { +public : + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + 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; + } +}; + + +class FloatingPointRoundingOperationTypeRule { +public : + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + 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 test applied to mixed sorts"); + } + } + } + + return firstOperand; + } +}; + +class FloatingPointParametricOpTypeRule { +public : + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + TRACE("FloatingPointParametricOpTypeRule"); + + return nodeManager->builtinOperatorType(); + } +}; + +class FloatingPointToFPIEEEBitVectorTypeRule { +public : + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + TRACE("FloatingPointToFPIEEEBitVectorTypeRule"); + + FloatingPointToFPIEEEBitVector info = n.getOperator().getConst<FloatingPointToFPIEEEBitVector>(); + + 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.t.exponent() + info.t.significand())) { + 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.t); + } +}; + + +class FloatingPointToFPFloatingPointTypeRule { +public : + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + TRACE("FloatingPointToFPFloatingPointTypeRule"); + + FloatingPointToFPFloatingPoint info = n.getOperator().getConst<FloatingPointToFPFloatingPoint>(); + + 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.t); + } +}; + + +class FloatingPointToFPRealTypeRule { +public : + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + TRACE("FloatingPointToFPRealTypeRule"); + + FloatingPointToFPReal info = n.getOperator().getConst<FloatingPointToFPReal>(); + + 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.t); + } +}; + + +class FloatingPointToFPSignedBitVectorTypeRule { +public : + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + TRACE("FloatingPointToFPSignedBitVectorTypeRule"); + + FloatingPointToFPSignedBitVector info = n.getOperator().getConst<FloatingPointToFPSignedBitVector>(); + + 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.t); + } +}; + + +class FloatingPointToFPUnsignedBitVectorTypeRule { +public : + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + TRACE("FloatingPointToFPUnsignedBitVectorTypeRule"); + + FloatingPointToFPUnsignedBitVector info = n.getOperator().getConst<FloatingPointToFPUnsignedBitVector>(); + + 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.t); + } +}; + + + +class FloatingPointToFPGenericTypeRule { +public : + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + TRACE("FloatingPointToFPGenericTypeRule"); + + FloatingPointToFPGeneric info = n.getOperator().getConst<FloatingPointToFPGeneric>(); + + 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.t); + } +}; + + + +class FloatingPointToUBVTypeRule { +public : + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + TRACE("FloatingPointToUBVTypeRule"); + + FloatingPointToUBV info = n.getOperator().getConst<FloatingPointToUBV>(); + + 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.bvs); + } +}; + + +class FloatingPointToSBVTypeRule { +public : + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + TRACE("FloatingPointToSBVTypeRule"); + + FloatingPointToSBV info = n.getOperator().getConst<FloatingPointToSBV>(); + + 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.bvs); + } +}; + + + +class FloatingPointToRealTypeRule { +public : + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + TRACE("FloatingPointToRealTypeRule"); + + if (check) { + TypeNode roundingModeType = n[0].getType(check); + + if (!roundingModeType.isRoundingMode()) { + throw TypeCheckingExceptionPrivate(n, "first argument must be a rounding mode"); + } + + TypeNode operand = n[1].getType(check); + + if (!operand.isFloatingPoint()) { + throw TypeCheckingExceptionPrivate(n, "floating-point to real applied to a non floating-point sort"); + } + } + + return nodeManager->realType(); + } +}; + + + +}/* CVC4::theory::fp namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__FP__THEORY_FP_TYPE_RULES_H */ |