diff options
-rw-r--r-- | src/api/cvc4cpp.cpp | 2 | ||||
-rw-r--r-- | src/api/cvc4cppkind.h | 2 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 1 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 4 | ||||
-rw-r--r-- | src/theory/fp/kinds | 3 | ||||
-rw-r--r-- | src/theory/fp/theory_fp.cpp | 35 | ||||
-rw-r--r-- | src/theory/fp/theory_fp.h | 3 | ||||
-rw-r--r-- | src/theory/fp/theory_fp_type_rules.h | 31 |
8 files changed, 78 insertions, 3 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index fa727088e..1b6783f7a 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -209,6 +209,7 @@ const static std::unordered_map<Kind, CVC4::Kind, KindHashFunction> s_kinds{ {FLOATINGPOINT_TO_UBV, CVC4::Kind::FLOATINGPOINT_TO_UBV}, {FLOATINGPOINT_TO_SBV, CVC4::Kind::FLOATINGPOINT_TO_SBV}, {FLOATINGPOINT_TO_REAL, CVC4::Kind::FLOATINGPOINT_TO_REAL}, + {FLOATINGPOINT_TO_IEEE_BV, CVC4::Kind::FLOATINGPOINT_TO_IEEE_BV}, /* Arrays -------------------------------------------------------------- */ {SELECT, CVC4::Kind::SELECT}, {STORE, CVC4::Kind::STORE}, @@ -474,6 +475,7 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction> {CVC4::Kind::FLOATINGPOINT_TO_SBV_TOTAL, INTERNAL_KIND}, {CVC4::Kind::FLOATINGPOINT_TO_REAL, FLOATINGPOINT_TO_REAL}, {CVC4::Kind::FLOATINGPOINT_TO_REAL_TOTAL, INTERNAL_KIND}, + {CVC4::Kind::FLOATINGPOINT_TO_IEEE_BV, FLOATINGPOINT_TO_IEEE_BV}, /* Arrays ---------------------------------------------------------- */ {CVC4::Kind::SELECT, SELECT}, {CVC4::Kind::STORE, STORE}, diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h index f8e1fb90c..c177f01e2 100644 --- a/src/api/cvc4cppkind.h +++ b/src/api/cvc4cppkind.h @@ -1441,6 +1441,8 @@ enum CVC4_PUBLIC Kind : int32_t */ FLOATINGPOINT_TO_REAL, + FLOATINGPOINT_TO_IEEE_BV, + /* Arrays ---------------------------------------------------------------- */ /** diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 3233ee7e8..79c20e4b0 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -255,6 +255,7 @@ void Smt2::addFloatingPointOperators() { addIndexedOperator(api::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR, api::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR, "to_fp_signed"); + addOperator(api::FLOATINGPOINT_TO_IEEE_BV, "fp.to_ieee_bv"); } } diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 30c1cd0f5..323f94a39 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3038,8 +3038,8 @@ Expr SmtEngine::getValue(const Expr& ex) const // Ensure it's a constant, or a lambda (for uninterpreted functions). This // assertion only holds for models that do not have approximate values. - Assert(m->hasApproximations() || resultNode.getKind() == kind::LAMBDA - || resultNode.isConst()); + // Assert(m->hasApproximations() || resultNode.getKind() == kind::LAMBDA + // || resultNode.isConst()); if(options::abstractValues() && resultNode.getType().isArray()) { resultNode = d_private->mkAbstractValue(resultNode); diff --git a/src/theory/fp/kinds b/src/theory/fp/kinds index 49ed92dee..49ce066d9 100644 --- a/src/theory/fp/kinds +++ b/src/theory/fp/kinds @@ -302,6 +302,9 @@ typerule FLOATINGPOINT_COMPONENT_EXPONENT ::CVC4::theory::fp::FloatingPointCom operator FLOATINGPOINT_COMPONENT_SIGNIFICAND 1 "Significand component of a word-blasted floating-point number" typerule FLOATINGPOINT_COMPONENT_SIGNIFICAND ::CVC4::theory::fp::FloatingPointComponentSignificand +operator FLOATINGPOINT_TO_IEEE_BV 1 "IEEE representation of a floating-point number" +typerule FLOATINGPOINT_TO_IEEE_BV ::CVC4::theory::fp::FloatingPointToIeeeBv + operator ROUNDINGMODE_BITBLAST 1 "The bit-vector for a non-deterministic rounding mode" typerule ROUNDINGMODE_BITBLAST ::CVC4::theory::fp::RoundingModeBitBlast diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp index 2632a6f38..7e034ebf4 100644 --- a/src/theory/fp/theory_fp.cpp +++ b/src/theory/fp/theory_fp.cpp @@ -399,6 +399,7 @@ Node TheoryFp::expandDefinition(LogicRequest &lr, Node node) Trace("fp-expandDefinition") << "TheoryFp::expandDefinition(): " << node << std::endl; + NodeManager* nm = NodeManager::currentNM(); Node res = node; if (node.getKind() == kind::FLOATINGPOINT_TO_FP_GENERIC) { @@ -438,8 +439,40 @@ Node TheoryFp::expandDefinition(LogicRequest &lr, Node node) enableUF(lr); res = NodeManager::currentNM()->mkNode(kind::FLOATINGPOINT_TO_REAL_TOTAL, node[0], toRealUF(node)); + } + else if (node.getKind() == kind::FLOATINGPOINT_TO_IEEE_BV) + { + // enableUF(lr); + TypeNode fpt = node[0].getType(); + uint32_t bw = fpt.getFloatingPointExponentSize() + + fpt.getFloatingPointSignificandSize(); + TypeNode bvt = nm->mkBitVectorType(bw); + Node v = nm->mkBoundVar(bvt); + Node bvl = nm->mkNode(kind::BOUND_VAR_LIST, v); + Node cond = nm->mkNode(kind::FLOATINGPOINT_ISNAN, node[0]).negate(); + + FloatingPointToFPIEEEBitVector conv(fpt.getFloatingPointExponentSize(), + fpt.getFloatingPointSignificandSize()); + + if (d_ufFpToIeeeBvSkolems.find(fpt) == d_ufFpToIeeeBvSkolems.end()) + { + std::vector<TypeNode> args = {fpt}; + d_ufFpToIeeeBvSkolems[fpt] = nm->mkSkolem( + "fp.to_ieee_bv NaN case", bvt); // nm->mkFunctionType(args, bvt)); + } - } else { + Node body = + nm->mkNode(kind::ITE, + cond, + node[0].eqNode(nm->mkNode(nm->mkConst(conv), v)), + nm->mkNode(kind::AND, + nm->mkNode(kind::FLOATINGPOINT_ISNAN, + nm->mkNode(nm->mkConst(conv), v)), + v.eqNode(d_ufFpToIeeeBvSkolems[fpt]))); + res = nm->mkNode(kind::CHOICE, bvl, body); + } + else + { // Do nothing } diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h index ad093f924..ebe04699b 100644 --- a/src/theory/fp/theory_fp.h +++ b/src/theory/fp/theory_fp.h @@ -142,6 +142,9 @@ class TheoryFp : public Theory { bool refineAbstraction(TheoryModel* m, TNode abstract, TNode concrete); + std::unordered_map<TypeNode, Node, TypeNodeHashFunction> + d_ufFpToIeeeBvSkolems; + }; /* class TheoryFp */ } // namespace fp diff --git a/src/theory/fp/theory_fp_type_rules.h b/src/theory/fp/theory_fp_type_rules.h index 4022cc278..0665ee4fa 100644 --- a/src/theory/fp/theory_fp_type_rules.h +++ b/src/theory/fp/theory_fp_type_rules.h @@ -739,6 +739,37 @@ class FloatingPointComponentSignificand } }; +class FloatingPointToIeeeBv +{ + public: + inline static TypeNode computeType(NodeManager* nodeManager, + TNode n, + bool check) + { + TypeNode operandType = n[0].getType(check); + + if (check) + { + if (!operandType.isFloatingPoint()) + { + throw TypeCheckingExceptionPrivate(n, + "fp.to_ieee_bv applied to a non " + "floating-point sort"); + } + } + +#ifdef CVC4_USE_SYMFPU + /* As before we need to use some of sympfu. */ + FloatingPointSize fps = operandType.getConst<FloatingPointSize>(); + unsigned bw = fps.packedWidth(); +#else + unsigned bw = 1; +#endif + + return nodeManager->mkBitVectorType(bw); + } +}; + class RoundingModeBitBlast { public: |