From 441c53b1a68cc16a345eb0dc8d9956c1301ed509 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Mon, 3 May 2021 19:07:52 -0700 Subject: [PATCH] FP: Move removal of generic to_fp operations to rewriter. (#6480) --- src/theory/fp/fp_expand_defs.cpp | 48 +------------------------ src/theory/fp/theory_fp_rewriter.cpp | 43 +++++++++++++++++++++- test/regress/CMakeLists.txt | 1 + test/regress/regress0/fp/issue3582.smt2 | 1 + test/regress/regress0/fp/issue5511.smt2 | 1 + test/regress/regress0/fp/issue5734.smt2 | 7 ++++ test/regress/regress0/fp/issue6164.smt2 | 1 + 7 files changed, 54 insertions(+), 48 deletions(-) create mode 100644 test/regress/regress0/fp/issue5734.smt2 diff --git a/src/theory/fp/fp_expand_defs.cpp b/src/theory/fp/fp_expand_defs.cpp index 1fc893a30..dac0d5136 100644 --- a/src/theory/fp/fp_expand_defs.cpp +++ b/src/theory/fp/fp_expand_defs.cpp @@ -21,48 +21,6 @@ namespace cvc5 { namespace theory { namespace fp { -namespace removeToFPGeneric { - -Node removeToFPGeneric(TNode node) -{ - Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_GENERIC); - - FloatingPointToFPGeneric info = - node.getOperator().getConst(); - - size_t children = node.getNumChildren(); - - Node op; - NodeManager* nm = NodeManager::currentNM(); - - if (children == 1) - { - op = nm->mkConst(FloatingPointToFPIEEEBitVector(info)); - return nm->mkNode(op, node[0]); - } - Assert(children == 2); - Assert(node[0].getType().isRoundingMode()); - - TypeNode t = node[1].getType(); - - if (t.isFloatingPoint()) - { - op = nm->mkConst(FloatingPointToFPFloatingPoint(info)); - } - else if (t.isReal()) - { - op = nm->mkConst(FloatingPointToFPReal(info)); - } - else - { - Assert(t.isBitVector()); - op = nm->mkConst(FloatingPointToFPSignedBitVector(info)); - } - - return nm->mkNode(op, node[0], node[1]); -} -} // namespace removeToFPGeneric - FpExpandDefs::FpExpandDefs(context::UserContext* u) : @@ -251,11 +209,7 @@ TrustNode FpExpandDefs::expandDefinition(Node node) Node res = node; Kind kind = node.getKind(); - if (kind == kind::FLOATINGPOINT_TO_FP_GENERIC) - { - res = removeToFPGeneric::removeToFPGeneric(node); - } - else if (kind == kind::FLOATINGPOINT_MIN) + if (kind == kind::FLOATINGPOINT_MIN) { res = NodeManager::currentNM()->mkNode( kind::FLOATINGPOINT_MIN_TOTAL, node[0], node[1], minUF(node)); diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp index 74e1ff526..628c00c30 100644 --- a/src/theory/fp/theory_fp_rewriter.cpp +++ b/src/theory/fp/theory_fp_rewriter.cpp @@ -77,6 +77,46 @@ namespace rewrite { << ") found in expression?"; } + RewriteResponse removeToFPGeneric(TNode node, bool isPreRewrite) + { + Assert(!isPreRewrite); + Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_GENERIC); + + FloatingPointToFPGeneric info = + node.getOperator().getConst(); + + uint32_t children = node.getNumChildren(); + + Node op; + NodeManager* nm = NodeManager::currentNM(); + + if (children == 1) + { + op = nm->mkConst(FloatingPointToFPIEEEBitVector(info)); + return RewriteResponse(REWRITE_AGAIN, nm->mkNode(op, node[0])); + } + Assert(children == 2); + Assert(node[0].getType().isRoundingMode()); + + TypeNode t = node[1].getType(); + + if (t.isFloatingPoint()) + { + op = nm->mkConst(FloatingPointToFPFloatingPoint(info)); + } + else if (t.isReal()) + { + op = nm->mkConst(FloatingPointToFPReal(info)); + } + else + { + Assert(t.isBitVector()); + op = nm->mkConst(FloatingPointToFPSignedBitVector(info)); + } + + return RewriteResponse(REWRITE_AGAIN, nm->mkNode(op, node[0], node[1])); + } + RewriteResponse removeDoubleNegation(TNode node, bool isPreRewrite) { Assert(node.getKind() == kind::FLOATINGPOINT_NEG); @@ -1233,7 +1273,8 @@ TheoryFpRewriter::TheoryFpRewriter(context::UserContext* u) : d_fpExpDef(u) rewrite::toFPSignedBV; d_postRewriteTable[kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR] = rewrite::identity; - d_postRewriteTable[kind::FLOATINGPOINT_TO_FP_GENERIC] = rewrite::identity; + d_postRewriteTable[kind::FLOATINGPOINT_TO_FP_GENERIC] = + rewrite::removeToFPGeneric; d_postRewriteTable[kind::FLOATINGPOINT_TO_UBV] = rewrite::identity; d_postRewriteTable[kind::FLOATINGPOINT_TO_SBV] = rewrite::identity; d_postRewriteTable[kind::FLOATINGPOINT_TO_REAL] = rewrite::identity; diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 685ac8b4e..3f1ff1307 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -581,6 +581,7 @@ set(regress_0_tests regress0/fp/issue3619.smt2 regress0/fp/issue4277-assign-func.smt2 regress0/fp/issue5511.smt2 + regress0/fp/issue5734.smt2 regress0/fp/issue6164.smt2 regress0/fp/rti_3_5_bug.smt2 regress0/fp/simple.smt2 diff --git a/test/regress/regress0/fp/issue3582.smt2 b/test/regress/regress0/fp/issue3582.smt2 index c06cdb110..2de76b680 100644 --- a/test/regress/regress0/fp/issue3582.smt2 +++ b/test/regress/regress0/fp/issue3582.smt2 @@ -1,3 +1,4 @@ +; REQUIRES: symfpu ; EXPECT: unsat (set-logic QF_FP) (declare-fun bv () (_ BitVec 1)) diff --git a/test/regress/regress0/fp/issue5511.smt2 b/test/regress/regress0/fp/issue5511.smt2 index 911db54ee..d4393486c 100644 --- a/test/regress/regress0/fp/issue5511.smt2 +++ b/test/regress/regress0/fp/issue5511.smt2 @@ -1,3 +1,4 @@ +; REQUIRES: symfpu ; EXPECT: sat (set-logic QF_FP) (declare-fun a () (_ FloatingPoint 53 11)) diff --git a/test/regress/regress0/fp/issue5734.smt2 b/test/regress/regress0/fp/issue5734.smt2 new file mode 100644 index 000000000..2ad9ac921 --- /dev/null +++ b/test/regress/regress0/fp/issue5734.smt2 @@ -0,0 +1,7 @@ +; REQUIRES: symfpu +; EXPECT: sat +(set-logic QF_FP) +(declare-fun a () RoundingMode) +(declare-fun b () (_ FloatingPoint 8 24)) +(assert (= b (fp.add a b (fp.add a ((_ to_fp 8 24) a ((_ to_fp 8 24) a 0)) b)))) +(check-sat) diff --git a/test/regress/regress0/fp/issue6164.smt2 b/test/regress/regress0/fp/issue6164.smt2 index 3ec9f1594..056a98afc 100644 --- a/test/regress/regress0/fp/issue6164.smt2 +++ b/test/regress/regress0/fp/issue6164.smt2 @@ -1,3 +1,4 @@ +; REQUIRES: symfpu ; EXPECT: sat ; EXPECT: ((((_ to_fp 5 11) roundNearestTiesToAway (/ 1 10)) (fp #b0 #b01011 #b1001100110))) (set-logic ALL) -- 2.30.2