diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-11-27 02:13:38 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-11-27 02:13:38 +0000 |
commit | b122cec27ca27d0b48e786191448e0053be78ed0 (patch) | |
tree | 615981d8623e830894f02fc528b173ac7461f934 /src/printer | |
parent | 3da16da97df7cd2efd4b113db3bfef8b9c138ebe (diff) |
Tuples and records merge. Resolves bug 270.
Also some fixes to parametric datatypes I found, and fixes for a handful of bugs, including some observed with --check-models --incremental on together.
(this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'src/printer')
-rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 68 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 9 |
2 files changed, 70 insertions, 7 deletions
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index f190b81bf..b3e16b38e 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -207,7 +207,6 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo out << ']'; return; break; - case kind::TUPLE: case kind::SEXPR: // no-op break; @@ -291,6 +290,14 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo break; // DATATYPES + case kind::APPLY_TYPE_ASCRIPTION: { + toStream(out, n[0], depth, types, false); + out << "::"; + TypeNode t = TypeNode::fromType(n.getOperator().getConst<AscriptionType>().getType()); + out << (t.isFunctionLike() ? t.getRangeType() : t); + } + return; + break; case kind::APPLY_CONSTRUCTOR: case kind::APPLY_SELECTOR: case kind::APPLY_TESTER: @@ -321,6 +328,49 @@ 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<TupleSelect>().getIndex(); + return; + break; + case kind::RECORD_SELECT: + toStream(out, n[0], depth, types, true); + out << '.' << n.getOperator().getConst<RecordSelect>().getField(); + return; + break; + case kind::TUPLE_UPDATE: + toStream(out, n[0], depth, types, true); + out << " WITH ." << n.getOperator().getConst<TupleUpdate>().getIndex() << " := "; + toStream(out, n[1], depth, types, true); + return; + break; + case kind::RECORD_UPDATE: + toStream(out, n[0], depth, types, true); + out << " WITH ." << n.getOperator().getConst<RecordUpdate>().getField() << " := "; + 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<Record>(); + out << "(# "; + TNode::iterator i = n.begin(); + bool first = true; + for(Record::const_iterator j = rec.begin(); j != rec.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: @@ -413,6 +463,9 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo op << ">="; opType = INFIX; break; + case kind::PARAMETRIC_DATATYPE: + out << n[0].getConst<Datatype>().getName(); + break; // BITVECTORS case kind::BITVECTOR_XOR: @@ -748,14 +801,14 @@ void CvcPrinter::toStream(std::ostream& out, Model& m, const Command* c) const t if(dynamic_cast<const DeclareTypeCommand*>(c) != NULL) { TypeNode tn = TypeNode::fromType( ((const DeclareTypeCommand*)c)->getType() ); if( tn.isSort() ){ - //print the cardinality + // print the cardinality if( tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){ out << "; cardinality of " << tn << " is " << (*tm.d_rep_set.d_type_reps.find(tn)).second.size() << std::endl; } } out << c << std::endl; if( tn.isSort() ){ - //print the representatives + // print the representatives if( tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){ for( size_t i=0; i<(*tm.d_rep_set.d_type_reps.find(tn)).second.size(); i++ ){ if( (*tm.d_rep_set.d_type_reps.find(tn)).second[i].isVar() ){ @@ -780,7 +833,7 @@ void CvcPrinter::toStream(std::ostream& out, Model& m, const Command* c) const t }else{ out << tn; } - out << " = " << tm.getValue( n ) << ";" << std::endl; + out << " = " << tm.getValue(n.toExpr()) << ";" << std::endl; /* //for table format (work in progress) @@ -916,10 +969,11 @@ static void toStream(std::ostream& out, const SimplifyCommand* c) throw() { } static void toStream(std::ostream& out, const GetValueCommand* c) throw() { - out << "% (get-value ( "; const vector<Expr>& terms = c->getTerms(); - copy(terms.begin(), terms.end(), ostream_iterator<Expr>(out, " ")); - out << " ))"; + Assert(!terms.empty()); + out << "GET_VALUE "; + copy(terms.begin(), terms.end() - 1, ostream_iterator<Expr>(out, ";\nGET_VALUE ")); + out << terms.back() << ";"; } static void toStream(std::ostream& out, const GetModelCommand* c) throw() { diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index c3fb3b782..ae589eba6 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -281,6 +281,15 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, break; // datatypes + case kind::APPLY_TYPE_ASCRIPTION: { + out << "as "; + toStream(out, n[0], toDepth < 0 ? toDepth : toDepth - 1, types); + out << ' '; + TypeNode t = TypeNode::fromType(n.getOperator().getConst<AscriptionType>().getType()); + out << (t.isFunctionLike() ? t.getRangeType() : t); + stillNeedToPrintParams = false; + } + break; case kind::APPLY_TESTER: case kind::APPLY_CONSTRUCTOR: case kind::APPLY_SELECTOR: |