From: yoni206 <yoni206@users.noreply.github.com>
Date: Thu, 17 Sep 2020 03:34:40 +0000 (-0700)
Subject: Dumping internal define-funs with no arguments (#5077)
X-Git-Tag: cvc5-1.0.0~2849
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=14041ad14583f670bc03d5eef6535544d86fc9fc;p=cvc5.git

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 265b35b3e..2cd8297d6 100644
--- 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 9e1480852..c6f3b85f5 100644
--- 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
index 000000000..22665d54c
--- /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)