From 5421d1a6f3035ca76feba80dca456a09633c7230 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 18 Apr 2022 17:01:34 -0500 Subject: [PATCH] Add some missing FP symbols to LFSC (#8629) --- proofs/lfsc/signatures/theory_def.plf | 4 ++++ src/proof/lfsc/lfsc_node_converter.cpp | 30 +++++++++++++++++++++++++- 2 files changed, 33 insertions(+), 1 deletion(-) 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 LfscNodeConverter::getOperatorIndices(Kind k, Node n) indices.push_back(nm->mkConstInt(fr.getSize().significandWidth())); } break; + case FLOATINGPOINT_TO_SBV: + { + const FloatingPointToSBV& fsbv = n.getConst(); + indices.push_back(nm->mkConstInt(Rational(fsbv))); + } + break; + case FLOATINGPOINT_TO_UBV: + { + const FloatingPointToUBV& fubv = n.getConst(); + indices.push_back(nm->mkConstInt(Rational(fubv))); + } + break; + case FLOATINGPOINT_TO_SBV_TOTAL: + { + const FloatingPointToSBVTotal& fsbv = + n.getConst(); + indices.push_back(nm->mkConstInt(Rational(fsbv))); + } + break; + case FLOATINGPOINT_TO_UBV_TOTAL: + { + const FloatingPointToUBVTotal& fubv = + n.getConst(); + indices.push_back(nm->mkConstInt(Rational(fubv))); + } + break; case APPLY_TESTER: { unsigned index = DType::indexOf(n); -- 2.30.2