From 77d0bec48a745e3c4acd65085f9c59bdfceed6c0 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 6 Apr 2022 13:43:33 -0500
Subject: [PATCH] Fixes for LFSC printing and signatures (#8579)

Ensures we recognize some internal FP symbols, adds a missing string operator, fixes seq.unit operator printing (required for CONG over seq.unit), fix for 0-ary tuple printing.
---
 proofs/lfsc/signatures/theory_def.plf  | 25 +++++++++++++++++++++++--
 src/proof/lfsc/lfsc_node_converter.cpp |  2 +-
 src/proof/lfsc/lfsc_printer.cpp        |  7 ++++++-
 3 files changed, 30 insertions(+), 4 deletions(-)

diff --git a/proofs/lfsc/signatures/theory_def.plf b/proofs/lfsc/signatures/theory_def.plf
index 5170932f7..361493537 100644
--- a/proofs/lfsc/signatures/theory_def.plf
+++ b/proofs/lfsc/signatures/theory_def.plf
@@ -190,6 +190,8 @@
 (define str.< (# x term (# y term (apply (apply f_str.< x) y))))
 (declare f_str.<= term)
 (define str.<= (# x term (# y term (apply (apply f_str.<= x) y))))
+(declare f_str.replace_all term)
+(define str.replace_all (# x term (# y term (# z term (apply (apply (apply f_str.replace_all x) y) z)))))
 (declare f_str.indexof_re term)
 (define str.indexof_re (# x term (# y term (# z term (apply (apply (apply f_str.indexof_re x) y) z)))))
 (declare f_str.replace_re term)
@@ -339,6 +341,12 @@
 (define bitOf (# b mpz (# x term (apply (f_bitOf b) x))))
 (declare f_BITVECTOR_EAGER_ATOM term)
 (define BITVECTOR_EAGER_ATOM (# x term (apply f_BITVECTOR_EAGER_ATOM x)))
+(declare f_BITVECTOR_ITE term)
+(define BITVECTOR_ITE (# x term (# y term (# z term (apply (apply (apply f_BITVECTOR_ITE x) y) z)))))
+(declare f_BITVECTOR_SLTBV term)
+(define BITVECTOR_SLTBV (# x term (# y term (apply (apply f_BITVECTOR_SLTBV x) y))))
+(declare f_BITVECTOR_ULTBV term)
+(define BITVECTOR_ULTBV (# x term (# y term (apply (apply f_BITVECTOR_ULTBV x) y))))
 ; The empty bitvector, which is used as the null terminator of bvconcat chains
 (declare emptybv term)
 
@@ -412,8 +420,8 @@
 (define to_fp_real (# x mpz (# y mpz (# z term (# w term (apply (apply (f_to_fp_real x y) z) w))))))
 (declare f_to_fp_sbv (! i mpz (! j mpz term)))
 (define to_fp_sbv (# x mpz (# y mpz (# z term (# w term (apply (apply (f_to_fp_sbv x y) z) w))))))
-(declare f_to_fp_generic (! i mpz (! j mpz term)))
-(define to_fp_generic (# x mpz (# y mpz (# z term (# w term (apply (apply (f_to_fp_generic x y) z) w))))))
+(declare f_to_fp_ieee_bv (! i mpz (! j mpz term)))
+(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)))))
 ; rounding modes
@@ -422,6 +430,19 @@
 (declare roundTowardPositive term)
 (declare roundTowardNegative term)
 (declare roundTowardZero term)
+; internally generated terms
+(declare f_EXPONENT term)
+(define EXPONENT (# x term (apply f_EXPONENT x)))
+(declare f_SIGN term)
+(define SIGN (# x term (apply f_SIGN x)))
+(declare f_SIGNIFICAND term)
+(define SIGNIFICAND (# x term (apply f_SIGNIFICAND x)))
+(declare f_ZERO term)
+(define ZERO (# x term (apply f_ZERO x)))
+(declare f_INF term)
+(define INF (# x term (apply f_INF x)))
+(declare f_NAN term)
+(define NAN (# x term (apply f_NAN x)))
 
 ;; ---- Sets
 (declare set.empty (! s sort term))
diff --git a/src/proof/lfsc/lfsc_node_converter.cpp b/src/proof/lfsc/lfsc_node_converter.cpp
index 2dd5619b0..7388c46a0 100644
--- a/src/proof/lfsc/lfsc_node_converter.cpp
+++ b/src/proof/lfsc/lfsc_node_converter.cpp
@@ -1101,7 +1101,7 @@ Node LfscNodeConverter::getOperatorOfTerm(Node n, bool macroApply)
         opName << getNameForUserNameOf(dt[cindex][index].getSelector());
       }
     }
-    else if (k == SET_SINGLETON || k == BAG_MAKE)
+    else if (k == SET_SINGLETON || k == BAG_MAKE || k == SEQ_UNIT)
     {
       if (!macroApply)
       {
diff --git a/src/proof/lfsc/lfsc_printer.cpp b/src/proof/lfsc/lfsc_printer.cpp
index 4448a4b2f..e41813ee3 100644
--- a/src/proof/lfsc/lfsc_printer.cpp
+++ b/src/proof/lfsc/lfsc_printer.cpp
@@ -258,7 +258,12 @@ void LfscPrinter::printTypeDefinition(
       if (tupleArityProcessed.find(arity) == tupleArityProcessed.end())
       {
         tupleArityProcessed.insert(arity);
-        os << "(declare Tuple_" << arity << " ";
+        os << "(declare Tuple";
+        if (arity>0)
+        {
+          os << "_" << arity;
+        }
+        os << " ";
         std::stringstream tcparen;
         for (size_t j = 0, nargs = cons.getNumArgs(); j < nargs; j++)
         {
-- 
2.30.2