From: Alex Ozdemir <aozdemir@hmc.edu>
Date: Wed, 4 Aug 2021 01:41:04 +0000 (-0700)
Subject: Add IEEE-BV-to-FP to external-to-internal mapping in C++ API (#6951)
X-Git-Tag: cvc5-1.0.0~1415
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=81544bb6de5b21db7ed5e41d56277105bbea103d;p=cvc5.git

Add IEEE-BV-to-FP to external-to-internal mapping in C++ API (#6951)

Without this, you can't make terms with that kind.
---

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 69aa720ea..22690fe49 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -241,6 +241,8 @@ const static std::unordered_map<Kind, cvc5::Kind> s_kinds{
     {FLOATINGPOINT_ISPOS, cvc5::Kind::FLOATINGPOINT_ISPOS},
     {FLOATINGPOINT_TO_FP_FLOATINGPOINT,
      cvc5::Kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT},
+    {FLOATINGPOINT_TO_FP_IEEE_BITVECTOR,
+     cvc5::Kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR},
     {FLOATINGPOINT_TO_FP_REAL, cvc5::Kind::FLOATINGPOINT_TO_FP_REAL},
     {FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR,
      cvc5::Kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR},