diff options
| author | François Bobot <francois@bobot.eu> | 2012-04-06 22:51:27 +0000 |
|---|---|---|
| committer | François Bobot <francois@bobot.eu> | 2012-04-06 22:51:27 +0000 |
| commit | 889853e225687dfef36b15ca1dccf74682e0fd66 (patch) | |
| tree | 598f1960f24db5ded582a14efec49c5aeb9488ac /src/printer/cvc | |
| parent | 7237456b4e2e5a119feacf98f52ec9e55d7a62a5 (diff) | |
* Smt2 printer for datatypes
* Fix DefineFunctionCommand when a constant is defined
Diffstat (limited to 'src/printer/cvc')
| -rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index a3d15f822..857513fa3 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -140,6 +140,10 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo } break; + case kind::DATATYPE_TYPE: + out << n.getConst<Datatype>().getName(); + break; + default: Warning() << "Constant printing not implemented for the case of " << n.getKind() << endl; out << n.getKind(); |