From c8c7a075428e6193dee86e57a9ecb8af11af270c Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Mon, 3 May 2021 13:27:02 -0700 Subject: [PATCH] FP: Rewrite to_fp conversion from signed bit-vector. (#6472) SymFPU does not allow to_fp conversion from signed bv of size 1. This adds rewrites for this case. Rewrites for the constant and the non-constant cases were tested in isolation. --- src/theory/fp/theory_fp_rewriter.cpp | 99 +++++++++++++++++--------- test/regress/CMakeLists.txt | 1 + test/regress/regress0/fp/from_sbv.smt2 | 15 ++++ 3 files changed, 82 insertions(+), 33 deletions(-) create mode 100644 test/regress/regress0/fp/from_sbv.smt2 diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp index e431ffa09..74e1ff526 100644 --- a/src/theory/fp/theory_fp_rewriter.cpp +++ b/src/theory/fp/theory_fp_rewriter.cpp @@ -32,11 +32,13 @@ * - Samuel Figuer results */ +#include "theory/fp/theory_fp_rewriter.h" + #include #include "base/check.h" +#include "theory/bv/theory_bv_utils.h" #include "theory/fp/fp_converter.h" -#include "theory/fp/theory_fp_rewriter.h" namespace cvc5 { namespace theory { @@ -333,6 +335,28 @@ namespace rewrite { return RewriteResponse(REWRITE_DONE, node); } + RewriteResponse toFPSignedBV(TNode node, bool isPreRewrite) + { + Assert(!isPreRewrite); + Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR); + + /* symFPU does not allow conversions from signed bit-vector of size 1 */ + if (node[1].getType().getBitVectorSize() == 1) + { + NodeManager* nm = NodeManager::currentNM(); + Node op = nm->mkConst(FloatingPointToFPUnsignedBitVector( + node.getOperator().getConst())); + Node fromubv = nm->mkNode(op, node[0], node[1]); + return RewriteResponse( + REWRITE_AGAIN_FULL, + nm->mkNode(kind::ITE, + node[1].eqNode(bv::utils::mkOne(1)), + nm->mkNode(kind::FLOATINGPOINT_NEG, fromubv), + fromubv)); + } + return RewriteResponse(REWRITE_DONE, node); + } + }; // namespace rewrite namespace constantFold { @@ -736,15 +760,16 @@ RewriteResponse maxTotal(TNode node, bool isPreRewrite) Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_REAL); TNode op = node.getOperator(); - const FloatingPointToFPReal ¶m = op.getConst(); + const FloatingPointSize& size = + op.getConst().getSize(); RoundingMode rm(node[0].getConst()); Rational arg(node[1].getConst()); - FloatingPoint res(param.getSize(), rm, arg); + FloatingPoint res(size, rm, arg); Node lit = NodeManager::currentNM()->mkConst(res); - + return RewriteResponse(REWRITE_DONE, lit); } @@ -753,16 +778,27 @@ RewriteResponse maxTotal(TNode node, bool isPreRewrite) Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR); TNode op = node.getOperator(); - const FloatingPointToFPSignedBitVector ¶m = op.getConst(); + const FloatingPointSize& size = + op.getConst().getSize(); RoundingMode rm(node[0].getConst()); - BitVector arg(node[1].getConst()); + BitVector sbv(node[1].getConst()); - FloatingPoint res(param.getSize(), rm, arg, true); + NodeManager* nm = NodeManager::currentNM(); - Node lit = NodeManager::currentNM()->mkConst(res); - - return RewriteResponse(REWRITE_DONE, lit); + /* symFPU does not allow conversions from signed bit-vector of size 1 */ + if (sbv.getSize() == 1) + { + FloatingPoint fromubv(size, rm, sbv, false); + if (sbv.isBitSet(0)) + { + return RewriteResponse(REWRITE_DONE, nm->mkConst(fromubv.negate())); + } + return RewriteResponse(REWRITE_DONE, nm->mkConst(fromubv)); + } + + return RewriteResponse(REWRITE_DONE, + nm->mkConst(FloatingPoint(size, rm, sbv, true))); } RewriteResponse convertFromUBV(TNode node, bool isPreRewrite) @@ -770,15 +806,16 @@ RewriteResponse maxTotal(TNode node, bool isPreRewrite) Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR); TNode op = node.getOperator(); - const FloatingPointToFPUnsignedBitVector ¶m = op.getConst(); + const FloatingPointSize& size = + op.getConst().getSize(); RoundingMode rm(node[0].getConst()); BitVector arg(node[1].getConst()); - FloatingPoint res(param.getSize(), rm, arg, false); + FloatingPoint res(size, rm, arg, false); Node lit = NodeManager::currentNM()->mkConst(res); - + return RewriteResponse(REWRITE_DONE, lit); } @@ -787,13 +824,12 @@ RewriteResponse maxTotal(TNode node, bool isPreRewrite) Assert(node.getKind() == kind::FLOATINGPOINT_TO_UBV); TNode op = node.getOperator(); - const FloatingPointToUBV ¶m = op.getConst(); + const BitVectorSize& size = op.getConst().d_bv_size; RoundingMode rm(node[0].getConst()); FloatingPoint arg(node[1].getConst()); - FloatingPoint::PartialBitVector res( - arg.convertToBV(param.d_bv_size, rm, false)); + FloatingPoint::PartialBitVector res(arg.convertToBV(size, rm, false)); if (res.second) { Node lit = NodeManager::currentNM()->mkConst(res.first); @@ -809,13 +845,12 @@ RewriteResponse maxTotal(TNode node, bool isPreRewrite) Assert(node.getKind() == kind::FLOATINGPOINT_TO_SBV); TNode op = node.getOperator(); - const FloatingPointToSBV ¶m = op.getConst(); + const BitVectorSize& size = op.getConst().d_bv_size; RoundingMode rm(node[0].getConst()); FloatingPoint arg(node[1].getConst()); - FloatingPoint::PartialBitVector res( - arg.convertToBV(param.d_bv_size, rm, true)); + FloatingPoint::PartialBitVector res(arg.convertToBV(size, rm, true)); if (res.second) { Node lit = NodeManager::currentNM()->mkConst(res.first); @@ -848,7 +883,8 @@ RewriteResponse maxTotal(TNode node, bool isPreRewrite) Assert(node.getKind() == kind::FLOATINGPOINT_TO_UBV_TOTAL); TNode op = node.getOperator(); - const FloatingPointToUBVTotal ¶m = op.getConst(); + const BitVectorSize& size = + op.getConst().d_bv_size; RoundingMode rm(node[0].getConst()); FloatingPoint arg(node[1].getConst()); @@ -857,14 +893,12 @@ RewriteResponse maxTotal(TNode node, bool isPreRewrite) if (node[2].getMetaKind() == kind::metakind::CONSTANT) { BitVector partialValue(node[2].getConst()); - BitVector folded( - arg.convertToBVTotal(param.d_bv_size, rm, false, partialValue)); + BitVector folded(arg.convertToBVTotal(size, rm, false, partialValue)); Node lit = NodeManager::currentNM()->mkConst(folded); return RewriteResponse(REWRITE_DONE, lit); } else { - FloatingPoint::PartialBitVector res( - arg.convertToBV(param.d_bv_size, rm, false)); + FloatingPoint::PartialBitVector res(arg.convertToBV(size, rm, false)); if (res.second) { Node lit = NodeManager::currentNM()->mkConst(res.first); @@ -881,7 +915,8 @@ RewriteResponse maxTotal(TNode node, bool isPreRewrite) Assert(node.getKind() == kind::FLOATINGPOINT_TO_SBV_TOTAL); TNode op = node.getOperator(); - const FloatingPointToSBVTotal ¶m = op.getConst(); + const BitVectorSize& size = + op.getConst().d_bv_size; RoundingMode rm(node[0].getConst()); FloatingPoint arg(node[1].getConst()); @@ -890,14 +925,12 @@ RewriteResponse maxTotal(TNode node, bool isPreRewrite) if (node[2].getMetaKind() == kind::metakind::CONSTANT) { BitVector partialValue(node[2].getConst()); - BitVector folded( - arg.convertToBVTotal(param.d_bv_size, rm, true, partialValue)); + BitVector folded(arg.convertToBVTotal(size, rm, true, partialValue)); Node lit = NodeManager::currentNM()->mkConst(folded); return RewriteResponse(REWRITE_DONE, lit); } else { - FloatingPoint::PartialBitVector res( - arg.convertToBV(param.d_bv_size, rm, true)); + FloatingPoint::PartialBitVector res(arg.convertToBV(size, rm, true)); if (res.second) { Node lit = NodeManager::currentNM()->mkConst(res.first); @@ -1049,7 +1082,7 @@ RewriteResponse maxTotal(TNode node, bool isPreRewrite) TheoryFpRewriter::TheoryFpRewriter(context::UserContext* u) : d_fpExpDef(u) { /* Set up the pre-rewrite dispatch table */ - for (unsigned i = 0; i < kind::LAST_KIND; ++i) + for (uint32_t i = 0; i < kind::LAST_KIND; ++i) { d_preRewriteTable[i] = rewrite::notFP; } @@ -1140,7 +1173,7 @@ TheoryFpRewriter::TheoryFpRewriter(context::UserContext* u) : d_fpExpDef(u) d_preRewriteTable[kind::ROUNDINGMODE_BITBLAST] = rewrite::identity; /* Set up the post-rewrite dispatch table */ - for (unsigned i = 0; i < kind::LAST_KIND; ++i) + for (uint32_t i = 0; i < kind::LAST_KIND; ++i) { d_postRewriteTable[i] = rewrite::notFP; } @@ -1197,7 +1230,7 @@ TheoryFpRewriter::TheoryFpRewriter(context::UserContext* u) : d_fpExpDef(u) rewrite::identity; d_postRewriteTable[kind::FLOATINGPOINT_TO_FP_REAL] = rewrite::identity; d_postRewriteTable[kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR] = - rewrite::identity; + rewrite::toFPSignedBV; d_postRewriteTable[kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR] = rewrite::identity; d_postRewriteTable[kind::FLOATINGPOINT_TO_FP_GENERIC] = rewrite::identity; @@ -1228,7 +1261,7 @@ TheoryFpRewriter::TheoryFpRewriter(context::UserContext* u) : d_fpExpDef(u) d_postRewriteTable[kind::ROUNDINGMODE_BITBLAST] = rewrite::identity; /* Set up the post-rewrite constant fold table */ - for (unsigned i = 0; i < kind::LAST_KIND; ++i) + for (uint32_t i = 0; i < kind::LAST_KIND; ++i) { // Note that this is identity, not notFP // Constant folding is called after post-rewrite diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 765b12e90..685ac8b4e 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -574,6 +574,7 @@ set(regress_0_tests regress0/fp/down-cast-RNA.smt2 regress0/fp/ext-rew-test.smt2 regress0/fp/from_ubv.smt2 + regress0/fp/from_sbv.smt2 regress0/fp/issue-5524.smt2 regress0/fp/issue3536.smt2 regress0/fp/issue3582.smt2 diff --git a/test/regress/regress0/fp/from_sbv.smt2 b/test/regress/regress0/fp/from_sbv.smt2 new file mode 100644 index 000000000..226d6589c --- /dev/null +++ b/test/regress/regress0/fp/from_sbv.smt2 @@ -0,0 +1,15 @@ +; COMMAND-LINE: --fp-exp +; EXPECT: unsat +(set-logic QF_BVFP) +(declare-const x (_ BitVec 1)) +(declare-const rm RoundingMode) +(assert (or + (distinct ((_ to_fp 5 11) rm #b1) (fp #b1 #b01111 #b0000000000)) + (distinct ((_ to_fp 5 11) rm #b0) (_ +zero 5 11)) + (ite + (= x #b1) + (= ((_ to_fp 5 11) rm x) ((_ to_fp_unsigned 5 11) rm x)) + (distinct ((_ to_fp 5 11) rm x) ((_ to_fp_unsigned 5 11) rm x)) + ) + )) +(check-sat) -- 2.30.2