diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-07-09 14:33:31 -0400 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-07-09 14:33:31 -0400 |
commit | b3c76399db741d8d616a75242345710dc1c1b81c (patch) | |
tree | 5f2ac2af2b52229a28d3e72f93dd2f0b89d548ed /src/printer | |
parent | e926fd162c6cee95d31044305e3b4df90b59f9fc (diff) |
sets cvc printer
Diffstat (limited to 'src/printer')
-rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 58 |
1 files changed, 58 insertions, 0 deletions
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 2548c22ab..41e87b809 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -162,6 +162,12 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo out << n.getConst<Datatype>().getName(); break; + case kind::EMPTYSET: { + out << "{} :: " << n.getConst<EmptySet>().getType(); + return; + break; + } + default: // fall back on whatever operator<< does on underlying type; we // might luck out and print something reasonable @@ -696,6 +702,58 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo return; break; + // SETS + case kind::SET_TYPE: + out << "SET OF "; + toStream(out, n[0], depth, types, false); + return; + break; + case kind::UNION: + op << '|'; + opType = INFIX; + break; + case kind::INTERSECTION: + op << '&'; + opType = INFIX; + break; + case kind::SETMINUS: + op << '-'; + opType = INFIX; + break; + case kind::SUBSET: + op << "<="; + opType = INFIX; + break; + case kind::MEMBER: + op << "IN"; + opType = INFIX; + break; + case kind::SINGLETON: + out << "{"; + toStream(out, n[0], depth, types, false); + out << "}"; + return; + break; + case kind::INSERT: { + if(bracket) { + out << '('; + } + out << '{'; + size_t i = 0; + toStream(out, n[i++], depth, types, false); + for(;i+1 < n.getNumChildren(); ++i) { + out << ", "; + toStream(out, n[i], depth, types, false); + } + out << "} | "; + toStream(out, n[i], depth, types, true); + if(bracket) { + out << ')'; + } + return; + break; + } + // Quantifiers case kind::FORALL: out << "(FORALL"; |