diff options
| author | yoni206 <yoni206@users.noreply.github.com> | 2020-09-16 20:34:40 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-16 22:34:40 -0500 |
| commit | 14041ad14583f670bc03d5eef6535544d86fc9fc (patch) | |
| tree | f81b8503c7e0eae4431535241de2acd37f2f0fa6 /src/smt/node_command.cpp | |
| parent | 70bfc4f67bcad32fa1b9b581b71b3a2d70e14d7e (diff) | |
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.
Diffstat (limited to 'src/smt/node_command.cpp')
| -rw-r--r-- | src/smt/node_command.cpp | 5 |
1 files changed, 4 insertions, 1 deletions
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); } |