From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 18 Apr 2022 22:01:34 +0000 (-0500)
Subject: Add some missing FP symbols to LFSC (#8629)
X-Git-Tag: cvc5-1.0.1~250
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5421d1a6f3035ca76feba80dca456a09633c7230;p=cvc5.git

Add some missing FP symbols to LFSC (#8629)
---

diff --git a/proofs/lfsc/signatures/theory_def.plf b/proofs/lfsc/signatures/theory_def.plf
index 361493537..eb2c34991 100644
--- a/proofs/lfsc/signatures/theory_def.plf
+++ b/proofs/lfsc/signatures/theory_def.plf
@@ -424,6 +424,10 @@
 (define to_fp_ieee_bv (# x mpz (# y mpz (# z term (apply (f_to_fp_ieee_bv x y) z)))))
 (declare f_to_fp_bv (! i mpz (! j mpz term)))
 (define to_fp_bv (# x mpz (# y mpz (# z term (apply (f_to_fp_bv x y) z)))))
+(declare f_fp.to_ubv_total (! i mpz term))
+(define fp.to_ubv_total (# x mpz (# z term (# w term (# u term (apply (apply (apply (f_fp.to_ubv_total x) z) w) u))))))
+(declare f_fp.to_sbv_total (! i mpz term))
+(define fp.to_sbv_total (# x mpz (# z term (# w term (# u term (apply (apply (apply (f_fp.to_sbv_total x) z) w) u))))))
 ; rounding modes
 (declare roundNearestTiesToEven term)
 (declare roundNearestTiesToAway term)
diff --git a/src/proof/lfsc/lfsc_node_converter.cpp b/src/proof/lfsc/lfsc_node_converter.cpp
index fcbf6cea0..563e7809b 100644
--- a/src/proof/lfsc/lfsc_node_converter.cpp
+++ b/src/proof/lfsc/lfsc_node_converter.cpp
@@ -883,7 +883,9 @@ bool LfscNodeConverter::isIndexedOperatorKind(Kind k)
          || k == FLOATINGPOINT_TO_FP_FROM_FP
          || k == FLOATINGPOINT_TO_FP_FROM_IEEE_BV
          || k == FLOATINGPOINT_TO_FP_FROM_SBV
-         || k == FLOATINGPOINT_TO_FP_FROM_REAL || k == APPLY_UPDATER
+         || k == FLOATINGPOINT_TO_FP_FROM_REAL || k == FLOATINGPOINT_TO_SBV
+         || k == FLOATINGPOINT_TO_UBV || k == FLOATINGPOINT_TO_SBV_TOTAL
+         || k == FLOATINGPOINT_TO_UBV_TOTAL || k == APPLY_UPDATER
          || k == APPLY_TESTER;
 }
 
@@ -965,6 +967,32 @@ std::vector<Node> LfscNodeConverter::getOperatorIndices(Kind k, Node n)
       indices.push_back(nm->mkConstInt(fr.getSize().significandWidth()));
     }
     break;
+    case FLOATINGPOINT_TO_SBV:
+    {
+      const FloatingPointToSBV& fsbv = n.getConst<FloatingPointToSBV>();
+      indices.push_back(nm->mkConstInt(Rational(fsbv)));
+    }
+    break;
+    case FLOATINGPOINT_TO_UBV:
+    {
+      const FloatingPointToUBV& fubv = n.getConst<FloatingPointToUBV>();
+      indices.push_back(nm->mkConstInt(Rational(fubv)));
+    }
+    break;
+    case FLOATINGPOINT_TO_SBV_TOTAL:
+    {
+      const FloatingPointToSBVTotal& fsbv =
+          n.getConst<FloatingPointToSBVTotal>();
+      indices.push_back(nm->mkConstInt(Rational(fsbv)));
+    }
+    break;
+    case FLOATINGPOINT_TO_UBV_TOTAL:
+    {
+      const FloatingPointToUBVTotal& fubv =
+          n.getConst<FloatingPointToUBVTotal>();
+      indices.push_back(nm->mkConstInt(Rational(fubv)));
+    }
+    break;
     case APPLY_TESTER:
     {
       unsigned index = DType::indexOf(n);