diff options
| author | Alex Ozdemir <aozdemir@hmc.edu> | 2021-08-03 18:41:04 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-08-04 01:41:04 +0000 |
| commit | 81544bb6de5b21db7ed5e41d56277105bbea103d (patch) | |
| tree | 8f90aeeae2638938902fe4e0d679da15b1565d5c /src/api/cpp/cvc5.cpp | |
| parent | 19c382b8666492fa8818444c7f2ee907da3d9479 (diff) | |
Add IEEE-BV-to-FP to external-to-internal mapping in C++ API (#6951)
Without this, you can't make terms with that kind.
Diffstat (limited to 'src/api/cpp/cvc5.cpp')
| -rw-r--r-- | src/api/cpp/cvc5.cpp | 2 |
1 files changed, 2 insertions, 0 deletions
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}, |