diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-16 11:37:53 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-16 11:38:09 -0500 |
commit | 966f38dc17ee316fdb069ec2a427c4f79f1f73b2 (patch) | |
tree | 1a1b60435daffa8b59eea589ef04c26b50f8a724 /src/printer | |
parent | 594301e6f2893ebe9baba5083ff084933b1e9da9 (diff) |
Parsing support for SMT LIB 2.6. Minor fixes for printing datatypes. Fix for mkGroundTerm for parametric datatypes. Minor change to run_regression to allow regressions to override input language. Minor refactoring to Cvc.g.
Diffstat (limited to 'src/printer')
-rw-r--r-- | src/printer/printer.cpp | 3 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 97 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.h | 1 |
3 files changed, 71 insertions, 30 deletions
diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index c715312c1..a8a84c06f 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -43,6 +43,9 @@ Printer* Printer::makePrinter(OutputLanguage lang) throw() { case LANG_SMTLIB_V2_5: return new printer::smt2::Smt2Printer(); + + case LANG_SMTLIB_V2_6: + return new printer::smt2::Smt2Printer(printer::smt2::smt2_6_variant); case LANG_TPTP: return new printer::tptp::TptpPrinter(); diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 2b7da63f7..08eaf610a 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -671,11 +671,17 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, tmp.replace(pos, 8, "::"); } out << tmp; - }else if( n.getKind()==kind::APPLY_TESTER ){ + }else if( n.getKind()==kind::APPLY_TESTER ){ unsigned cindex = Datatype::indexOf(n.getOperator().toExpr()); const Datatype& dt = Datatype::datatypeOf(n.getOperator().toExpr()); - out << "is-"; - toStream(out, Node::fromExpr(dt[cindex].getConstructor()), toDepth < 0 ? toDepth : toDepth - 1, types); + if( d_variant==smt2_6_variant ){ + out << "(_ is "; + toStream(out, Node::fromExpr(dt[cindex].getConstructor()), toDepth < 0 ? toDepth : toDepth - 1, types); + out << ")"; + }else{ + out << "is-"; + toStream(out, Node::fromExpr(dt[cindex].getConstructor()), toDepth < 0 ? toDepth : toDepth - 1, types); + } }else{ toStream(out, n.getOperator(), toDepth < 0 ? toDepth : toDepth - 1, types); } @@ -1018,7 +1024,7 @@ void Smt2Printer::toStream(std::ostream& out, const Command* c, tryToStream<GetInfoCommand>(out, c) || tryToStream<SetOptionCommand>(out, c) || tryToStream<GetOptionCommand>(out, c) || - tryToStream<DatatypeDeclarationCommand>(out, c) || + tryToStream<DatatypeDeclarationCommand>(out, c, d_variant) || tryToStream<CommentCommand>(out, c, d_variant) || tryToStream<EmptyCommand>(out, c) || tryToStream<EchoCommand>(out, c, d_variant)) { @@ -1102,9 +1108,12 @@ void Smt2Printer::toStream(std::ostream& out, const Model& m, const Command* c) const std::map< TypeNode, std::vector< Node > >& type_reps = tm.d_rep_set.d_type_reps; std::map< TypeNode, std::vector< Node > >::const_iterator tn_iterator = type_reps.find( tn ); - if( options::modelUninterpDtEnum() && tn.isSort() && tn_iterator != type_reps.end() ){ - out << "(declare-datatypes () ((" << dynamic_cast<const DeclareTypeCommand*>(c)->getSymbol() << " "; - + if( options::modelUninterpDtEnum() && tn.isSort() && tn_iterator != type_reps.end() ){ + if(d_variant == smt2_6_variant) { + out << "(declare-datatypes ((" << dynamic_cast<const DeclareTypeCommand*>(c)->getSymbol() << " 0)) ("; + }else{ + out << "(declare-datatypes () ((" << dynamic_cast<const DeclareTypeCommand*>(c)->getSymbol() << " "; + } for( size_t i=0, N = tn_iterator->second.size(); i < N; i++ ){ out << "(" << (*tn_iterator).second[i] << ")"; } @@ -1457,32 +1466,60 @@ static void toStream(std::ostream& out, const GetOptionCommand* c) throw() { out << "(get-option :" << c->getFlag() << ")"; } -static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) throw() { +static void toStream(std::ostream& out, const Datatype & d) { + for(Datatype::const_iterator ctor = d.begin(), ctor_end = d.end(); + ctor != ctor_end; ++ctor){ + if( ctor!=d.begin() ) out << " "; + out << "(" << maybeQuoteSymbol(ctor->getName()); + + for(DatatypeConstructor::const_iterator arg = ctor->begin(), arg_end = ctor->end(); + arg != arg_end; ++arg){ + out << " (" << arg->getSelector() << " " + << static_cast<SelectorType>(arg->getType()).getRangeType() << ")"; + } + out << ")"; + } +} + +static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c, Variant v) throw() { const vector<DatatypeType>& datatypes = c->getDatatypes(); - out << "(declare-datatypes () ("; - for(vector<DatatypeType>::const_iterator i = datatypes.begin(), - i_end = datatypes.end(); - i != i_end; - ++i) { - - const Datatype & d = i->getDatatype(); - - out << "(" << maybeQuoteSymbol(d.getName()) << " "; - for(Datatype::const_iterator ctor = d.begin(), ctor_end = d.end(); - ctor != ctor_end; ++ctor){ - if( ctor!=d.begin() ) out << " "; - out << "(" << maybeQuoteSymbol(ctor->getName()); - - for(DatatypeConstructor::const_iterator arg = ctor->begin(), arg_end = ctor->end(); - arg != arg_end; ++arg){ - out << " (" << arg->getSelector() << " " - << static_cast<SelectorType>(arg->getType()).getRangeType() << ")"; - } - out << ")"; + out << "(declare-"; + Assert( !datatypes.empty() ); + if( datatypes[0].getDatatype().isCodatatype() ){ + out << "co"; + } + out << "datatypes"; + if(v == smt2_6_variant) { + out << " ("; + for(vector<DatatypeType>::const_iterator i = datatypes.begin(), + i_end = datatypes.end(); + i != i_end; ++i) { + const Datatype & d = i->getDatatype(); + out << "(" << maybeQuoteSymbol(d.getName()); + out << " " << d.getNumParameters() << ")"; } - out << ")" << endl; + out << ") "; + for(vector<DatatypeType>::const_iterator i = datatypes.begin(), + i_end = datatypes.end(); + i != i_end; ++i) { + const Datatype & d = i->getDatatype(); + out << "("; + toStream( out, d ); + out << ")" << endl; + } + }else{ + out << " () ("; + for(vector<DatatypeType>::const_iterator i = datatypes.begin(), + i_end = datatypes.end(); + i != i_end; ++i) { + const Datatype & d = i->getDatatype(); + out << "(" << maybeQuoteSymbol(d.getName()) << " "; + toStream( out, d ); + out << ")" << endl; + } + out << ")"; } - out << "))"; + out << ")"; } static void toStream(std::ostream& out, const CommentCommand* c, Variant v) throw() { diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h index 0354a5738..d73f11b59 100644 --- a/src/printer/smt2/smt2_printer.h +++ b/src/printer/smt2/smt2_printer.h @@ -30,6 +30,7 @@ namespace smt2 { enum Variant { no_variant, smt2_0_variant, // old-style 2.0 syntax, when it makes a difference + smt2_6_variant, // new-style 2.6 syntax, when it makes a difference z3str_variant, // old-style 2.0 and also z3str syntax sygus_variant // variant for sygus };/* enum Variant */ |