diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-02-26 14:59:38 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-02-26 14:59:38 -0600 |
commit | 3ef1df6e974ba572a8def512489cd9e47e9d2a2b (patch) | |
tree | 82ed16f31e9fd3d7a3356c0248b3a7a7a384864c /src/printer | |
parent | b320aa323923822a7702997bbca05e8512da55a4 (diff) |
More fixes for printing sygus commands (#3812)
Towards v1 -> v2 sygus conversion.
This makes several fixes and improvements related to printing sygus commands:
(1) The logic is extended with LIA, DT, UF internally during setDefaults instead of during parsing. This is the correct place for this extension of the logic since it should be applied regardless of the parser. 5 existing logic bugs were discovered as a result of this in regressions, which are fixed by this PR.
(2) Ensures that terms in sygus grammars are printed without letification, since this is prohibited in sygus. Notice the formulas printed by constraints need to be letified (otherwise we can't convert large lustre benchmarks). Thus, the letification threshold should determine this but always be overridden for grammar terms.
(3) Ensures final options are set for all sygus-specific commands, which follows the standards prescribed by sygus v2 (all set-* commands come before other commands).
Diffstat (limited to 'src/printer')
-rw-r--r-- | src/printer/printer.cpp | 5 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 14 | ||||
-rw-r--r-- | src/printer/sygus_print_callback.cpp | 3 |
3 files changed, 11 insertions, 11 deletions
diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index 28471de72..886be0cfa 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -84,8 +84,9 @@ 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 - toStream(out, n, -1, false, 1); + // 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 diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index e9a4d0a83..6fdbd4adb 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -1522,7 +1522,8 @@ void Smt2Printer::toStreamSygus(std::ostream& out, TNode n) const { out << "("; } - out << dt[cIndex].getSygusOp(); + // print operator without letification (the fifth argument is set to 0). + toStream(out, dt[cIndex].getSygusOp(), -1, false, 0); if (n.getNumChildren() > 0) { for (Node nc : n) @@ -1537,15 +1538,12 @@ void Smt2Printer::toStreamSygus(std::ostream& out, TNode n) const } } Node p = n.getAttribute(theory::SygusPrintProxyAttribute()); - if (!p.isNull()) + if (p.isNull()) { - out << p; - } - else - { - // cannot convert term to analog, print original - out << n; + p = n; } + // cannot convert term to analog, print original, without letification. + toStream(out, p, -1, false, 0); } static void toStream(std::ostream& out, const AssertCommand* c) diff --git a/src/printer/sygus_print_callback.cpp b/src/printer/sygus_print_callback.cpp index ae1d97c64..92a89a18e 100644 --- a/src/printer/sygus_print_callback.cpp +++ b/src/printer/sygus_print_callback.cpp @@ -78,8 +78,9 @@ void SygusExprPrintCallback::toStreamSygus(const Printer* p, sbody = sbody.substitute(vars.begin(), vars.end(), subs.begin(), subs.end()); + // print to stream without letification std::stringstream body_out; - body_out << sbody; + p->toStream(body_out, sbody, -1, false, 0); // do string substitution Assert(e.getNumChildren() == d_args.size()); |