diff options
Diffstat (limited to 'src/theory/fp/fp_expand_defs.cpp')
| -rw-r--r-- | src/theory/fp/fp_expand_defs.cpp | 17 |
1 files changed, 7 insertions, 10 deletions
diff --git a/src/theory/fp/fp_expand_defs.cpp b/src/theory/fp/fp_expand_defs.cpp index 4e9803bf7..34cc1ed5d 100644 --- a/src/theory/fp/fp_expand_defs.cpp +++ b/src/theory/fp/fp_expand_defs.cpp @@ -260,22 +260,23 @@ TrustNode FpExpandDefs::expandDefinition(Node node) << "FpExpandDefs::expandDefinition(): " << node << std::endl; Node res = node; + Kind kind = node.getKind(); - if (node.getKind() == kind::FLOATINGPOINT_TO_FP_GENERIC) + if (kind == kind::FLOATINGPOINT_TO_FP_GENERIC) { res = removeToFPGeneric::removeToFPGeneric(node); } - else if (node.getKind() == kind::FLOATINGPOINT_MIN) + else if (kind == kind::FLOATINGPOINT_MIN) { res = NodeManager::currentNM()->mkNode( kind::FLOATINGPOINT_MIN_TOTAL, node[0], node[1], minUF(node)); } - else if (node.getKind() == kind::FLOATINGPOINT_MAX) + else if (kind == kind::FLOATINGPOINT_MAX) { res = NodeManager::currentNM()->mkNode( kind::FLOATINGPOINT_MAX_TOTAL, node[0], node[1], maxUF(node)); } - else if (node.getKind() == kind::FLOATINGPOINT_TO_UBV) + else if (kind == kind::FLOATINGPOINT_TO_UBV) { FloatingPointToUBV info = node.getOperator().getConst<FloatingPointToUBV>(); FloatingPointToUBVTotal newInfo(info); @@ -287,7 +288,7 @@ TrustNode FpExpandDefs::expandDefinition(Node node) node[1], toUBVUF(node)); } - else if (node.getKind() == kind::FLOATINGPOINT_TO_SBV) + else if (kind == kind::FLOATINGPOINT_TO_SBV) { FloatingPointToSBV info = node.getOperator().getConst<FloatingPointToSBV>(); FloatingPointToSBVTotal newInfo(info); @@ -299,15 +300,11 @@ TrustNode FpExpandDefs::expandDefinition(Node node) node[1], toSBVUF(node)); } - else if (node.getKind() == kind::FLOATINGPOINT_TO_REAL) + else if (kind == kind::FLOATINGPOINT_TO_REAL) { res = NodeManager::currentNM()->mkNode( kind::FLOATINGPOINT_TO_REAL_TOTAL, node[0], toRealUF(node)); } - else - { - // Do nothing - } if (res != node) { |