diff options
author | Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> | 2020-08-04 15:23:54 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-08-04 15:23:54 -0500 |
commit | 24a40040a4a5f88f96eada87e46323ace729f06a (patch) | |
tree | e2d74981a9f0d2ceb8bc973c619c71a3e099f2fe /src/printer | |
parent | 0cbcf1f835f74c304e2ac3884143b7df9c7f75b6 (diff) |
Modify the smt2 parser to use the Sygus grammar. (#4829)
Diffstat (limited to 'src/printer')
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 28 |
1 files changed, 15 insertions, 13 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index d6b304a78..45cc2426c 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -2071,33 +2071,32 @@ static void toStream(std::ostream& out, const SynthFunCommand* c) { out << '(' << c->getCommandName() << ' ' << CVC4::quoteSymbol(c->getSymbol()) << ' '; - Type type = c->getFunction().getType(); - const std::vector<Expr>& vars = c->getVars(); - Assert(!type.isFunction() || !vars.empty()); + const std::vector<api::Term>& vars = c->getVars(); out << '('; - if (type.isFunction()) + if (!vars.empty()) { // print variable list - std::vector<Expr>::const_iterator i = vars.begin(), i_end = vars.end(); - Assert(i != i_end); - out << '(' << *i << ' ' << i->getType() << ')'; + std::vector<api::Term>::const_iterator i = vars.begin(), i_end = vars.end(); + out << '(' << *i << ' ' << i->getSort() << ')'; ++i; while (i != i_end) { - out << " (" << *i << ' ' << i->getType() << ')'; + out << " (" << *i << ' ' << i->getSort() << ')'; ++i; } - FunctionType ft = type; - type = ft.getRangeType(); } out << ')'; // if not invariant-to-synthesize, print return type if (!c->isInv()) { - out << ' ' << type; + out << ' ' << c->getSort(); } + out << '\n'; // print grammar, if any - toStreamSygusGrammar(out, c->getSygusType()); + if (c->getGrammar() != nullptr) + { + out << *c->getGrammar(); + } out << ')'; } @@ -2152,7 +2151,10 @@ static void toStream(std::ostream& out, const GetAbductCommand* c) out << c->getConjecture(); // print grammar, if any - toStreamSygusGrammar(out, c->getGrammarType()); + if (c->getGrammar() != nullptr) + { + out << *c->getGrammar(); + } out << ')'; } |