diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-06-09 12:50:31 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-06-09 17:50:31 +0000 |
| commit | 9dc6deed6147b7a53a65d727cc7afd7b1b6c2c19 (patch) | |
| tree | 2aa8ff76f1900764d4d8a680b564ad193c729f69 /src/smt | |
| parent | cd34574f476827c11e1f0d9a33141a04b5175696 (diff) | |
Fixes related to printing tuples, define-fun commands in smt2 (#6679)
This PR fixes some initial issues with printing datatypes in smt2.
It does not yet address further issues on printing define-fun as a result of dump=raw-benchmark, which requires deeper refactoring of the implementation of the API / SmtEngine.
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/command.cpp | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 0aebee7b3..d672b79a6 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -1404,11 +1404,16 @@ void DefineFunctionCommand::toStream(std::ostream& out, size_t dag, OutputLanguage language) const { + TypeNode rangeType = termToNode(d_func).getType(); + if (rangeType.isFunction()) + { + rangeType = rangeType.getRangeType(); + } Printer::getPrinter(language)->toStreamCmdDefineFunction( out, d_func.toString(), termVectorToNodes(d_formals), - termToNode(d_func).getType().getRangeType(), + rangeType, termToNode(d_formula)); } |