diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-05-04 11:46:31 -0500 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-05-04 09:46:31 -0700 |
commit | 410eb892bd779a7544cace62fa2b447b8188e238 (patch) | |
tree | c34d8671243bd5024fe7ad214a7ffac06a3bd595 /src | |
parent | cbfcc24f0da280e21de5118cc2c0c6a18a71a629 (diff) |
Do not print tuples. (#1874)
Diffstat (limited to 'src')
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 5d2b8972d..96bee9724 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -1441,10 +1441,7 @@ void Smt2Printer::toStream(std::ostream& out, else if (const DatatypeDeclarationCommand* datatype_declaration_command = dynamic_cast<const DatatypeDeclarationCommand*>(command)) { - if (!datatype_declaration_command->getDatatypes()[0].isTuple()) - { - out << command << endl; - } + toStream(out, datatype_declaration_command, -1, false, 1); } else { @@ -1903,8 +1900,14 @@ static void toStream(std::ostream& out, Variant v) { const vector<DatatypeType>& datatypes = c->getDatatypes(); - out << "(declare-"; Assert(!datatypes.empty()); + if (datatypes[0].getDatatype().isTuple()) + { + // not necessary to print tuples + Assert(datatypes.size() == 1); + return; + } + out << "(declare-"; if (datatypes[0].getDatatype().isCodatatype()) { out << "co"; |