From 62b673a6b8444c14c169a984dd6e3fc8f685851e Mon Sep 17 00:00:00 2001 From: ajreynol Date: Mon, 15 Feb 2016 13:02:02 -0600 Subject: Eliminate most of the internal representation infrastructure for tuples and records, replace with datatypes throughout, update cvc printer for tuples/records. Minor changes to API for records and tuples. --- src/printer/cvc/cvc_printer.cpp | 115 ++++++++++++++++++++++++++-------------- 1 file changed, 76 insertions(+), 39 deletions(-) (limited to 'src/printer/cvc/cvc_printer.cpp') diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 25f958963..b525c4329 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -162,8 +162,32 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo } break; - case kind::DATATYPE_TYPE: - out << n.getConst().getName(); + case kind::DATATYPE_TYPE: { + const Datatype& dt = n.getConst(); + if( dt.isTuple() ){ + out << '['; + for (unsigned i = 0; i < dt[0].getNumArgs(); ++ i) { + if (i > 0) { + out << ", "; + } + Type t = ((SelectorType)dt[0][i].getSelector().getType()).getRangeType(); + out << t; + } + out << ']'; + }else if( dt.isRecord() ){ + out << "[# "; + for (unsigned i = 0; i < dt[0].getNumArgs(); ++ i) { + if (i > 0) { + out << ", "; + } + Type t = ((SelectorType)dt[0][i].getSelector().getType()).getRangeType(); + out << dt[0][i].getSelector() << ":" << t; + } + out << " #]"; + }else{ + out << dt.getName(); + } + } break; case kind::EMPTYSET: @@ -214,7 +238,6 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo out << " ENDIF"; return; break; - case kind::TUPLE_TYPE: case kind::SEXPR_TYPE: out << '['; for (unsigned i = 0; i < n.getNumChildren(); ++ i) { @@ -329,9 +352,48 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo } return; break; - case kind::APPLY_CONSTRUCTOR: + case kind::APPLY_CONSTRUCTOR: { + TypeNode t = n.getType(); + if( t.isTuple() ){ + //no-op + }else if( t.isRecord() ){ + const Record& rec = t.getRecord(); + out << "(# "; + TNode::iterator i = n.begin(); + bool first = true; + const Record::FieldVector& fields = rec.getFields(); + for(Record::FieldVector::const_iterator j = fields.begin(); j != fields.end(); ++i, ++j) { + if(!first) { + out << ", "; + } + out << (*j).first << " := "; + toStream(out, *i, depth, types, false); + first = false; + } + out << " #)"; + return; + }else{ + toStream(op, n.getOperator(), depth, types, false); + } + } + break; case kind::APPLY_SELECTOR: - case kind::APPLY_SELECTOR_TOTAL: + case kind::APPLY_SELECTOR_TOTAL: { + TypeNode t = n.getType(); + if( t.isTuple() ){ + toStream(out, n[0], depth, types, true); + out << '.' << Datatype::indexOf( n.getOperator().toExpr() ); + }else if( t.isRecord() ){ + toStream(out, n[0], depth, types, true); + const Record& rec = t.getRecord(); + unsigned index = Datatype::indexOf( n.getOperator().toExpr() ); + std::pair fld = rec[index]; + out << '.' << fld.first; + }else{ + toStream(op, n.getOperator(), depth, types, false); + } + } + break; case kind::APPLY_TESTER: toStream(op, n.getOperator(), depth, types, false); break; @@ -359,16 +421,6 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo out << " -> BOOLEAN"; return; break; - case kind::TUPLE_SELECT: - toStream(out, n[0], depth, types, true); - out << '.' << n.getOperator().getConst().getIndex(); - return; - break; - case kind::RECORD_SELECT: - toStream(out, n[0], depth, types, true); - out << '.' << n.getOperator().getConst().getField(); - return; - break; case kind::TUPLE_UPDATE: toStream(out, n[0], depth, types, true); out << " WITH ." << n.getOperator().getConst().getIndex() << " := "; @@ -381,28 +433,6 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo toStream(out, n[1], depth, types, true); return; break; - case kind::TUPLE: - // no-op - break; - case kind::RECORD: { - // (# _a := 2, _b := 2 #) - const Record& rec = n.getOperator().getConst(); - out << "(# "; - TNode::iterator i = n.begin(); - bool first = true; - const Record::FieldVector& fields = rec.getFields(); - for(Record::FieldVector::const_iterator j = fields.begin(); j != fields.end(); ++i, ++j) { - if(!first) { - out << ", "; - } - out << (*j).first << " := "; - toStream(out, *i, depth, types, false); - first = false; - } - out << " #)"; - return; - break; - } // ARRAYS case kind::ARRAY_TYPE: @@ -1106,8 +1136,9 @@ static void toStream(std::ostream& out, const DefineFunctionCommand* c, bool cvc static void toStream(std::ostream& out, const DeclareTypeCommand* c, bool cvc3Mode) throw() { if(c->getArity() > 0) { + //TODO? out << "ERROR: Don't know how to print parameterized type declaration " - "in CVC language:" << endl << c->toString() << endl; + "in CVC language." << endl; } else { out << c->getSymbol() << " : TYPE;"; } @@ -1229,7 +1260,13 @@ static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c, boo } firstSelector = false; const DatatypeConstructorArg& selector = *k; - out << selector.getName() << ": " << SelectorType(selector.getType()).getRangeType(); + Type t = SelectorType(selector.getType()).getRangeType(); + if( t.isDatatype() ){ + const Datatype & sdt = ((DatatypeType)t).getDatatype(); + out << selector.getName() << ": " << sdt.getName(); + }else{ + out << selector.getName() << ": " << t; + } } out << ')'; } -- cgit v1.2.3