diff options
author | Arjun Viswanathan <arjun-viswanathan@uiowa.edu> | 2017-12-27 21:43:35 -0600 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-12-27 21:43:35 -0600 |
commit | 2731897b5f9ed46c66e3bdf20cde47ef43923a9c (patch) | |
tree | a95d36fdeb9c6a0d5dbc41ef4dc7bafdcb6e81b3 /src/printer/smt2/smt2_printer.cpp | |
parent | 3b7f04092f55b263b1f89fa2c2517821013ff5fe (diff) |
Rel smt parser (#1446)
Diffstat (limited to 'src/printer/smt2/smt2_printer.cpp')
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 237 |
1 files changed, 153 insertions, 84 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index c13c519ae..54fc10719 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -252,11 +252,32 @@ void Smt2Printer::toStream(std::ostream& out, } case kind::DATATYPE_TYPE: + { + const Datatype& dt = (NodeManager::currentNM()->getDatatypeForIndex( + n.getConst<DatatypeIndexConstant>().getIndex())); + if (dt.isTuple()) + { + unsigned int n = dt[0].getNumArgs(); + if (n == 0) + { + out << "Tuple"; + } + else + { + out << "(Tuple"; + for (unsigned int i = 0; i < n; i++) + { + out << " " << dt[0][i].getRangeType(); + } + out << ")"; + } + } + else { - const Datatype & dt = (NodeManager::currentNM()->getDatatypeForIndex( n.getConst< DatatypeIndexConstant >().getIndex() )); out << maybeQuoteSymbol(dt.getName()); } break; + } case kind::UNINTERPRETED_CONSTANT: { const UninterpretedConstant& uc = n.getConst<UninterpretedConstant>(); @@ -549,6 +570,11 @@ void Smt2Printer::toStream(std::ostream& out, case kind::INTERSECTION: case kind::SETMINUS: case kind::SUBSET: + case kind::CARD: + case kind::JOIN: + case kind::PRODUCT: + case kind::TRANSPOSE: + case kind::TCLOSURE: parametricTypeChildren = true; out << smtKindString(k) << " "; break; @@ -624,80 +650,103 @@ void Smt2Printer::toStream(std::ostream& out, return; } break; - case kind::APPLY_CONSTRUCTOR: typeChildren = true; - case kind::APPLY_TESTER: - case kind::APPLY_SELECTOR: - case kind::APPLY_SELECTOR_TOTAL: - case kind::PARAMETRIC_DATATYPE: - break; - //separation logic - case kind::SEP_EMP: - case kind::SEP_PTO: - case kind::SEP_STAR: - case kind::SEP_WAND:out << smtKindString(k) << " "; break; + case kind::APPLY_CONSTRUCTOR: + { + typeChildren = true; + const Datatype& dt = Datatype::datatypeOf(n.getOperator().toExpr()); + if (dt.isTuple()) + { + stillNeedToPrintParams = false; + out << "mkTuple" << ( dt[0].getNumArgs()==0 ? "" : " "); + } + } + + case kind::APPLY_TESTER: + case kind::APPLY_SELECTOR: + case kind::APPLY_SELECTOR_TOTAL: + case kind::PARAMETRIC_DATATYPE: break; - case kind::SEP_NIL:out << "(as sep.nil " << n.getType() << ")";break; + // separation logic + case kind::SEP_EMP: + case kind::SEP_PTO: + case kind::SEP_STAR: + case kind::SEP_WAND: out << smtKindString(k) << " "; break; - // quantifiers - case kind::FORALL: - case kind::EXISTS: - if( k==kind::FORALL ){ - out << "forall "; - }else{ - out << "exists "; - } - for( unsigned i=0; i<2; i++) { - out << n[i] << " "; - if( i==0 && n.getNumChildren()==3 ){ - out << "(! "; + case kind::SEP_NIL: + out << "(as sep.nil " << n.getType() << ")"; + break; + + // quantifiers + case kind::FORALL: + case kind::EXISTS: + if (k == kind::FORALL) + { + out << "forall "; + } + else + { + out << "exists "; + } + for (unsigned i = 0; i < 2; i++) + { + out << n[i] << " "; + if (i == 0 && n.getNumChildren() == 3) + { + out << "(! "; + } + } + if (n.getNumChildren() == 3) + { + out << n[2]; + out << ")"; } - } - if( n.getNumChildren()==3 ){ - out << n[2]; out << ")"; - } - out << ")"; - return; - break; - case kind::BOUND_VAR_LIST: - // the left parenthesis is already printed (before the switch) - for(TNode::iterator i = n.begin(), iend = n.end(); - i != iend; ) { - out << '('; - toStream(out, *i, toDepth < 0 ? toDepth : toDepth - 1, types, 0); - out << ' '; - out << (*i).getType(); - // The following code do stange things - // (*i).getType().toStream(out, toDepth < 0 ? toDepth : toDepth - 1, - // false, language::output::LANG_SMTLIB_V2_5); - out << ')'; - if(++i != iend) { + return; + break; + case kind::BOUND_VAR_LIST: + // the left parenthesis is already printed (before the switch) + for (TNode::iterator i = n.begin(), iend = n.end(); i != iend;) + { + out << '('; + toStream(out, *i, toDepth < 0 ? toDepth : toDepth - 1, types, 0); out << ' '; + out << (*i).getType(); + // The following code do stange things + // (*i).getType().toStream(out, toDepth < 0 ? toDepth : toDepth - 1, + // false, language::output::LANG_SMTLIB_V2_5); + out << ')'; + if (++i != iend) + { + out << ' '; + } } - } - out << ')'; - return; - case kind::INST_PATTERN: - break; - case kind::INST_PATTERN_LIST: - for(unsigned i=0; i<n.getNumChildren(); i++) { - if( n[i].getKind()==kind::INST_ATTRIBUTE ){ - if( n[i][0].getAttribute(theory::FunDefAttribute()) ){ - out << ":fun-def"; + out << ')'; + return; + case kind::INST_PATTERN: break; + case kind::INST_PATTERN_LIST: + for (unsigned i = 0; i < n.getNumChildren(); i++) + { + if (n[i].getKind() == kind::INST_ATTRIBUTE) + { + if (n[i][0].getAttribute(theory::FunDefAttribute())) + { + out << ":fun-def"; + } + } + else + { + out << ":pattern " << n[i]; } - }else{ - out << ":pattern " << n[i]; } - } - return; - break; + return; + break; - default: - // fall back on however the kind prints itself; this probably - // won't be SMT-LIB v2 compliant, but it will be clear from the - // output that support for the kind needs to be added here. - out << n.getKind() << ' '; + default: + // fall back on however the kind prints itself; this probably + // won't be SMT-LIB v2 compliant, but it will be clear from the + // output that support for the kind needs to be added here. + out << n.getKind() << ' '; } if( n.getMetaKind() == kind::metakind::PARAMETERIZED && stillNeedToPrintParams ) { @@ -917,6 +966,12 @@ static string smtKindString(Kind k) case kind::SINGLETON: return "singleton"; case kind::INSERT: return "insert"; case kind::COMPLEMENT: return "complement"; + case kind::CARD: return "card"; + case kind::JOIN: return "join"; + case kind::PRODUCT: return "product"; + case kind::TRANSPOSE: return "transpose"; + case kind::TCLOSURE: + return "tclosure"; // fp theory case kind::FLOATINGPOINT_FP: return "fp"; @@ -1326,7 +1381,11 @@ void Smt2Printer::toStream(std::ostream& out, } */ } else { - out << c << endl; + DatatypeDeclarationCommand* c1 = (DatatypeDeclarationCommand*)c; + const vector<DatatypeType>& datatypes = c1->getDatatypes(); + if (!datatypes[0].isTuple()) { + out << c << endl; + } } } @@ -1762,38 +1821,48 @@ static void toStream(std::ostream& out, { const vector<DatatypeType>& datatypes = c->getDatatypes(); out << "(declare-"; - Assert( !datatypes.empty() ); - if( datatypes[0].getDatatype().isCodatatype() ){ + Assert(!datatypes.empty()); + if (datatypes[0].getDatatype().isCodatatype()) + { out << "co"; } out << "datatypes"; - if(v == smt2_6_variant) { + 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(); + 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 << ") ("; - for(vector<DatatypeType>::const_iterator i = datatypes.begin(), - i_end = datatypes.end(); - i != i_end; ++i) { - const Datatype & d = i->getDatatype(); + 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 ); + toStream(out, d); out << ")" << endl; } out << ")"; - }else{ + } + else + { out << " () ("; - for(vector<DatatypeType>::const_iterator i = datatypes.begin(), - i_end = datatypes.end(); - i != i_end; ++i) { - const Datatype & d = i->getDatatype(); + 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 ); + toStream(out, d); out << ")" << endl; } out << ")"; |