From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Wed, 3 Oct 2018 01:10:54 +0000 (-0700)
Subject: Allow (_ to_fp ...) in strict parsing mode (#2566)
X-Git-Tag: cvc5-1.0.0~4471
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c48dd01b92f4704c99ca6833b94759dee42106a8;p=cvc5.git

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 c3a107bdf..c4046b7c2 100644
--- 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 ecd98ddc2..fd4026dc0 100644
--- 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 394263f48..deb4ad647 100644
--- 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
index 000000000..8652a5c33
--- /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)