diff options
Diffstat (limited to 'src/theory/fp')
-rw-r--r-- | src/theory/fp/fp_converter.cpp | 56 | ||||
-rw-r--r-- | src/theory/fp/fp_converter.h | 2 | ||||
-rw-r--r-- | src/theory/fp/theory_fp_rewriter.cpp | 30 | ||||
-rw-r--r-- | src/theory/fp/theory_fp_type_rules.h | 16 |
4 files changed, 36 insertions, 68 deletions
diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp index 0d088fe41..f7c58af7b 100644 --- a/src/theory/fp/fp_converter.cpp +++ b/src/theory/fp/fp_converter.cpp @@ -13,11 +13,13 @@ **/ #include "theory/fp/fp_converter.h" -#include "theory/theory.h" -// theory.h Only needed for the leaf test #include <vector> +#include "theory/theory.h" // theory.h Only needed for the leaf test +#include "util/floatingpoint.h" +#include "util/symfpu_literal.h" + #ifdef CVC4_USE_SYMFPU #include "symfpu/core/add.h" #include "symfpu/core/classify.h" @@ -919,9 +921,11 @@ Node FpConverter::convert(TNode node) if (current.getKind() == kind::CONST_FLOATINGPOINT) { /******** Constants ********/ - d_fpMap.insert(current, - symfpu::unpackedFloat<traits>( - current.getConst<FloatingPoint>().getLiteral())); + d_fpMap.insert( + current, + symfpu::unpackedFloat<traits>(current.getConst<FloatingPoint>() + .getLiteral() + ->getSymUF())); } else { @@ -1711,43 +1715,23 @@ Node FpConverter::getValue(Valuation &val, TNode var) #ifdef CVC4_USE_SYMFPU TypeNode t(var.getType()); + Assert(t.isRoundingMode() || t.isFloatingPoint()) + << "Asking for the value of a type that is not managed by the " + "floating-point theory"; + if (t.isRoundingMode()) { rmMap::const_iterator i(d_rmMap.find(var)); - if (i == d_rmMap.end()) - { - Unreachable() << "Asking for the value of an unregistered expression"; - } - else - { - Node value = rmToNode((*i).second); - return value; - } + Assert(i != d_rmMap.end()) + << "Asking for the value of an unregistered expression"; + return rmToNode((*i).second); } - else if (t.isFloatingPoint()) - { - fpMap::const_iterator i(d_fpMap.find(var)); - - if (i == d_fpMap.end()) - { - Unreachable() << "Asking for the value of an unregistered expression"; - } - else - { - Node value = ufToNode(fpt(t), (*i).second); - return value; - } - } - else - { - Unreachable() - << "Asking for the value of a type that is not managed by the " - "floating-point theory"; - } - - Unreachable() << "Unable to find value"; + fpMap::const_iterator i(d_fpMap.find(var)); + Assert(i != d_fpMap.end()) + << "Asking for the value of an unregistered expression"; + return ufToNode(fpt(t), (*i).second); #else Unimplemented() << "Conversion is dependent on SymFPU"; #endif diff --git a/src/theory/fp/fp_converter.h b/src/theory/fp/fp_converter.h index fd4434832..59e65c9e1 100644 --- a/src/theory/fp/fp_converter.h +++ b/src/theory/fp/fp_converter.h @@ -29,7 +29,7 @@ #include "expr/type.h" #include "theory/valuation.h" #include "util/bitvector.h" -#include "util/floatingpoint.h" +#include "util/floatingpoint_size.h" #include "util/hash.h" #ifdef CVC4_USE_SYMFPU diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp index 49b4e85c5..b56fa259c 100644 --- a/src/theory/fp/theory_fp_rewriter.cpp +++ b/src/theory/fp/theory_fp_rewriter.cpp @@ -887,18 +887,10 @@ namespace constantFold { switch (k) { #ifdef CVC4_USE_SYMFPU - case kind::FLOATINGPOINT_COMPONENT_NAN: - result = arg0.getLiteral().nan; - break; - case kind::FLOATINGPOINT_COMPONENT_INF: - result = arg0.getLiteral().inf; - break; - case kind::FLOATINGPOINT_COMPONENT_ZERO: - result = arg0.getLiteral().zero; - break; - case kind::FLOATINGPOINT_COMPONENT_SIGN: - result = arg0.getLiteral().sign; - break; + case kind::FLOATINGPOINT_COMPONENT_NAN: result = arg0.isNaN(); break; + case kind::FLOATINGPOINT_COMPONENT_INF: result = arg0.isInfinite(); break; + case kind::FLOATINGPOINT_COMPONENT_ZERO: result = arg0.isZero(); break; + case kind::FLOATINGPOINT_COMPONENT_SIGN: result = arg0.getSign(); break; #endif default: Unreachable() << "Unknown kind used in componentFlag"; break; } @@ -919,11 +911,11 @@ namespace constantFold { return RewriteResponse( REWRITE_DONE, #ifdef CVC4_USE_SYMFPU - NodeManager::currentNM()->mkConst((BitVector)arg0.getLiteral().exponent) + NodeManager::currentNM()->mkConst((BitVector)arg0.getExponent()) #else node #endif - ); + ); } RewriteResponse componentSignificand(TNode node, bool) @@ -932,14 +924,14 @@ namespace constantFold { FloatingPoint arg0(node[0].getConst<FloatingPoint>()); - return RewriteResponse(REWRITE_DONE, + return RewriteResponse( + REWRITE_DONE, #ifdef CVC4_USE_SYMFPU - NodeManager::currentNM()->mkConst( - (BitVector)arg0.getLiteral().significand) + NodeManager::currentNM()->mkConst((BitVector)arg0.getSignificand()) #else - node + node #endif - ); + ); } RewriteResponse roundingModeBitBlast(TNode node, bool) diff --git a/src/theory/fp/theory_fp_type_rules.h b/src/theory/fp/theory_fp_type_rules.h index 4d4f3c660..d632e80c8 100644 --- a/src/theory/fp/theory_fp_type_rules.h +++ b/src/theory/fp/theory_fp_type_rules.h @@ -19,6 +19,7 @@ // 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 @@ -693,12 +694,10 @@ class FloatingPointComponentExponent * Here we use types from floatingpoint.h which are the literal * back-end but it should't make a difference. */ FloatingPointSize fps = operandType.getConst<FloatingPointSize>(); - symfpuLiteral::CVC4FPSize format(fps); // The symfpu interface to type info - unsigned bw = FloatingPointLiteral::exponentWidth(format); + unsigned bw = FloatingPoint::getUnpackedExponentWidth(fps); #else unsigned bw = 2; #endif - return nodeManager->mkBitVectorType(bw); } }; @@ -736,12 +735,10 @@ class FloatingPointComponentSignificand #ifdef CVC4_USE_SYMFPU /* As before we need to use some of sympfu. */ FloatingPointSize fps = operandType.getConst<FloatingPointSize>(); - symfpuLiteral::CVC4FPSize format(fps); - unsigned bw = FloatingPointLiteral::significandWidth(format); + unsigned bw = FloatingPoint::getUnpackedSignificandWidth(fps); #else unsigned bw = 1; #endif - return nodeManager->mkBitVectorType(bw); } }; @@ -771,12 +768,7 @@ class RoundingModeBitBlast } } -#ifdef CVC4_USE_SYMFPU - /* Uses sympfu for the macro. */ - return nodeManager->mkBitVectorType(SYMFPU_NUMBER_OF_ROUNDING_MODES); -#else - return nodeManager->mkBitVectorType(5); -#endif + return nodeManager->mkBitVectorType(CVC4_NUM_ROUNDING_MODES); } }; |