diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-04 18:34:24 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-04 18:34:41 -0400 |
| commit | 90e3d3127d41348d9d3c7d7877d2d9d7e2828124 (patch) | |
| tree | ca519e08ece0fbf9bf2116e7430d84ec5678fad4 /src/printer | |
| parent | d1d052cf549f574aad25f42e66051170e43ac3a7 (diff) | |
Add operator support (resolves bug #563).
Diffstat (limited to 'src/printer')
| -rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 27 |
1 files changed, 24 insertions, 3 deletions
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 63529c2a5..77d8f14de 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -483,6 +483,27 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo op << '^'; opType = INFIX; break; + case kind::ABS: + op << "ABS"; + opType = PREFIX; + break; + case kind::IS_INTEGER: + op << "IS_INTEGER"; + opType = PREFIX; + break; + case kind::TO_INTEGER: + op << "FLOOR"; + opType = PREFIX; + break; + case kind::TO_REAL: + // ignore, there is no to-real in CVC language + toStream(out, n[0], depth, types, false); + return; + case kind::DIVISIBLE: + out << "DIVISIBLE("; + toStream(out, n[0], depth, types, false); + out << ", " << n.getOperator().getConst<Divisible>().k << ")"; + return; // BITVECTORS case kind::BITVECTOR_XOR: @@ -573,7 +594,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo opType = INFIX; break; case kind::BITVECTOR_PLUS: { - //This interprets a BITVECTOR_PLUS as a bvadd in SMT-LIB + // This interprets a BITVECTOR_PLUS as a bvadd in SMT-LIB Assert(n.getType().isBitVector()); unsigned numc = n.getNumChildren()-2; unsigned child = 0; @@ -590,7 +611,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo out << ','; toStream(out, n[child], depth, types, false); out << ','; - toStream(out, n[child+1], depth, types, false); + toStream(out, n[child + 1], depth, types, false); while (child > 0) { out << ')'; --child; @@ -627,7 +648,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo out << ','; toStream(out, n[child], depth, types, false); out << ','; - toStream(out, n[child+1], depth, types, false); + toStream(out, n[child + 1], depth, types, false); while (child > 0) { out << ')'; --child; |