Add support for fp.to_ieee_bvfp_to_ieee_bv

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: