Allow (_ to_fp ...) in strict parsing mode (#2566)

When parsing with `--strict-parsing`, we are checking whether the
operators that we encounter have been explicitly added to the
`d_logicOperators` set in the `Parser` class. We did not do that for the
indexed operator `(_ to_fp ...)` (which is represented by the kind
`FLOATINGPOINT_TO_FP_GENERIC`). This commit adds the operator.

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index c3a107bdf77b055d70ba8ae998a57d2ad95bcbbc..c4046b7c21a7c4158cb64b53711c5967c112e384 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -188,6 +188,7 @@ void Smt2::addFloatingPointOperators() {
   addOperator(kind::FLOATINGPOINT_ISPOS, "fp.isPositive");
   addOperator(kind::FLOATINGPOINT_TO_REAL, "fp.to_real");
 
+  Parser::addOperator(kind::FLOATINGPOINT_TO_FP_GENERIC);
   Parser::addOperator(kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR);
   Parser::addOperator(kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT);
   Parser::addOperator(kind::FLOATINGPOINT_TO_FP_REAL);

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index ecd98ddc2e8317d977c534a2c2b23e3991825aa6..fd4026dc061696e5168e89fc2762d0b1844069bd 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -520,6 +520,7 @@ set(regress_0_tests
   regress0/parser/shadow_fun_symbol_nirat.smt2
   regress0/parser/strings20.smt2
   regress0/parser/strings25.smt2
+  regress0/parser/to_fp.smt2
   regress0/precedence/and-not.cvc
   regress0/precedence/and-xor.cvc
   regress0/precedence/bool-cmp.cvc

diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 394263f48147948412e71ba68b2c943ef8825c20..deb4ad647ded140c902d4570acfa2e7122ba1f3d 100644 (file)
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -528,6 +528,7 @@ REG0_TESTS = \
        regress0/parser/shadow_fun_symbol_nirat.smt2 \
        regress0/parser/strings20.smt2 \
        regress0/parser/strings25.smt2 \
+       regress0/parser/to_fp.smt2 \
        regress0/precedence/and-not.cvc \
        regress0/precedence/and-xor.cvc \
        regress0/precedence/bool-cmp.cvc \

diff --git a/test/regress/regress0/parser/to_fp.smt2 b/test/regress/regress0/parser/to_fp.smt2
new file mode 100644 (file)
index 0000000..8652a5c
--- /dev/null
+++ b/test/regress/regress0/parser/to_fp.smt2
@@ -0,0 +1,10 @@
+; REQUIRES: symfpu
+; COMMAND-LINE: --strict-parsing
+; EXPECT: sat
+(set-logic QF_FP)
+(declare-fun |c::main::main::3::div@1!0&0#1| () (_ FloatingPoint 8 24))
+(assert (not (fp.eq ((_ to_fp 11 53)
+                     roundNearestTiesToEven
+                     |c::main::main::3::div@1!0&0#1|)
+              (fp #b0 #b00000000000 #x0000000000000))))
+(check-sat)