diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-10-03 13:12:11 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-10-03 13:12:17 -0400 |
commit | eb63fdb37b2784d6d4340402cd0ee00ceb8f5041 (patch) | |
tree | 762648416161edb6b939334aefa9c75349073e95 /src/printer | |
parent | bd05758bc141f0b922916b63089e7e8748f8da31 (diff) |
More array constants and parsing: better error messages, extend to CVC presentation language.
Diffstat (limited to 'src/printer')
-rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 9b3e83578..2d89d3aff 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -168,6 +168,13 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo break; } + case kind::STORE_ALL: { + const ArrayStoreAll& asa = n.getConst<ArrayStoreAll>(); + out << "ARRAY(" << asa.getType().getIndexType() << " OF " + << asa.getType().getConstituentType() << ") : " << asa.getExpr(); + break; + } + default: // fall back on whatever operator<< does on underlying type; we // might luck out and print something reasonable |