diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-07-14 14:12:18 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-07-14 14:12:18 -0500 |
| commit | 14d32d598e9daa97cf1a29ff893caac2989baec4 (patch) | |
| tree | f37a48a15db69e6423a3149c1a2e91687b870542 /src/printer/printer.cpp | |
| parent | 455fed0b388ff9c534391eb88f8c2a336fa42f07 (diff) | |
Remove sygus print callback (#4727)
This removes sygus print callbacks, since they are no longer necessary to support the sygus v1 parser.
This involved generalizing the scope of the datatype utility sygusToBuiltin. Now, printing "as sygus" simply is accomplished by doing sygusToBuiltin conversion and then calling the printer on the builtin term.
This is required for further work towards eliminating the Expr layer.
FYI @4tXJ7f
Diffstat (limited to 'src/printer/printer.cpp')
| -rw-r--r-- | src/printer/printer.cpp | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index 5d54759b9..67dbe1036 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -69,14 +69,6 @@ unique_ptr<Printer> Printer::makePrinter(OutputLanguage lang) } } -void Printer::toStreamSygus(std::ostream& out, TNode n) const -{ - // no sygus-specific printing associated with this printer, - // just print the original term, without letification (the fifth argument is - // set to 0). - toStream(out, n, -1, false, 0); -} - void Printer::toStream(std::ostream& out, const Model& m) const { for(size_t i = 0; i < m.getNumCommands(); ++i) { |