Dumping internal define-funs with no arguments (#5077)

Currently, --dump=assertions:... fails if a define-fun command is executed internally (an example for this can be found here.

The failure occurs because the printer expects a range type whenever a define-fun command is executed. However, when this command is used for 0-ary functions (variables), the getter for the range fails.

This PR fixes this by asking for a range only if the type is indeed a function. Otherwise, the original type is printed.

A test that currently fails but passes with this PR is included.

diff --git a/src/smt/node_command.cpp b/src/smt/node_command.cpp
index 265b35b3ea774a5d8c6216e15fb44dbf784162e9..2cd8297d6bc50e01a9dd413c8fe49961fc7ebb46 100644 (file)
--- a/src/smt/node_command.cpp
+++ b/src/smt/node_command.cpp
@@ -164,11 +164,14 @@ void DefineFunctionNodeCommand::toStream(std::ostream& out,
                                          size_t dag,
                                          OutputLanguage language) const
 {
+  TypeNode tn = d_fun.getType();
+  bool hasRange =
+      (tn.isFunction() || tn.isConstructor() || tn.isSelector());
   Printer::getPrinter(language)->toStreamCmdDefineFunction(
       out,
       d_fun.toString(),
       d_formals,
-      d_fun.getType().getRangeType(),
+      (hasRange ? d_fun.getType().getRangeType() : tn),
       d_formula);
 }
 

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 9e1480852ef5b4771e698aee29c417f6b8e3045b..c6f3b85f581b7971c32caf8c0526eee746d0b41f 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -673,6 +673,7 @@ set(regress_0_tests
   regress0/preprocess/preprocess_13.cvc
   regress0/preprocess/preprocess_14.cvc
   regress0/preprocess/preprocess_15.cvc
+  regress0/print_define_fun_internal.smt2
   regress0/print_lambda.cvc
   regress0/print_model.cvc
   regress0/printer/bv_consts_bin.smt2

diff --git a/test/regress/regress0/print_define_fun_internal.smt2 b/test/regress/regress0/print_define_fun_internal.smt2
new file mode 100644 (file)
index 0000000..22665d5
--- /dev/null
+++ b/test/regress/regress0/print_define_fun_internal.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --solve-real-as-int --dump=assertions:post-real-to-int
+; EXIT: 0
+; SCRUBBER: grep -v -E '.*'
+(set-logic QF_NRA)
+(declare-fun a () Real)
+(declare-fun b () Real)
+(assert (= (* a a) 4))
+(assert (= (* b b) 0))
+(assert (= (+ (* a a) (* b b)) 4))
+(check-sat)