Partial merge from datatypes-merge branch:

1. Defines a new type "DatatypeType", a type-constant that holds a Datatype, describing an inductive data type.
2. CVC language parser supports datatypes.
3. CVC language printer now functional.
4. Minor other cleanups.

No performance impact is expected outside of datatypes.  I'm verifying that that is the case with a cluster job this morning.

1 files changed, 154 insertions, 2 deletions

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index d2cf3f8b1..a048bc3b2 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
@@ -20,6 +20,8 @@
 #include "util/language.h"
 
 #include <iostream>
+#include <algorithm>
+#include <iterator>
 
 using namespace std;
 
@@ -29,7 +31,157 @@ namespace cvc {
 
 void CvcPrinter::toStream(std::ostream& out, TNode n,
                           int toDepth, bool types) const {
-  n.toStream(out, toDepth, types, language::output::LANG_AST);
+  // null
+  if(n.getKind() == kind::NULL_EXPR) {
+    out << "NULL";
+    return;
+  }
+
+  // variable
+  if(n.getMetaKind() == kind::metakind::VARIABLE) {
+    string s;
+    if(n.getAttribute(expr::VarNameAttr(), s)) {
+      out << s;
+    } else {
+      if(n.getKind() == kind::VARIABLE) {
+        out << "var_";
+      } else {
+        out << n.getKind() << '_';
+      }
+      out << n.getId();
+    }
+    if(types) {
+      // print the whole type, but not *its* type
+      out << ":";
+      n.getType().toStream(out, -1, false, language::output::LANG_CVC4);
+    }
+
+    return;
+  }
+
+  // constant
+  if(n.getMetaKind() == kind::metakind::CONSTANT) {
+    switch(n.getKind()) {
+    case kind::BITVECTOR_TYPE:
+      out << "BITVECTOR(" << n.getConst<BitVectorSize>().size << ")";
+      break;
+    case kind::CONST_BITVECTOR: {
+      const BitVector& bv = n.getConst<BitVector>();
+      const Integer& x = bv.getValue();
+      out << "0bin";
+      unsigned n = bv.getSize();
+      while(n-- > 0) {
+        out << (x.testBit(n) ? '1' : '0');
+      }
+      break;
+    }
+    case kind::CONST_BOOLEAN:
+      // the default would print "1" or "0" for bool, that's not correct
+      // for our purposes
+      out << (n.getConst<bool>() ? "TRUE" : "FALSE");
+      break;
+    case kind::CONST_RATIONAL: {
+      const Rational& rat = n.getConst<Rational>();
+      out << '(' << rat.getNumerator() << '/' << rat.getDenominator() << ')';
+      break;
+    }
+    case kind::BUILTIN:
+      switch(Kind k = n.getConst<Kind>()) {
+      case kind::EQUAL: out << '='; break;
+      case kind::PLUS: out << '+'; break;
+      case kind::MULT: out << '*'; break;
+      case kind::MINUS:
+      case kind::UMINUS: out << '-'; break;
+      case kind::DIVISION: out << '/'; break;
+      case kind::LT: out << '<'; break;
+      case kind::LEQ: out << "<="; break;
+      case kind::GT: out << '>'; break;
+      case kind::GEQ: out << ">="; break;
+      case kind::IMPLIES: out << "=>"; break;
+      case kind::IFF: out << "<=>"; break;
+      default:
+        out << k;
+      }
+      break;
+    default:
+      // fall back on whatever operator<< does on underlying type; we
+      // might luck out and be SMT-LIB v2 compliant
+      kind::metakind::NodeValueConstPrinter::toStream(out, n);
+    }
+
+    return;
+  } else if(n.getMetaKind() == kind::metakind::PARAMETERIZED) {
+    out << n.getOperator();
+    if(n.getNumChildren() > 0) {
+      out << '(';
+      if(n.getNumChildren() > 1) {
+        copy(n.begin(), n.end() - 1, ostream_iterator<TNode>(out, ", "));
+      }
+      out << n[n.getNumChildren() - 1] << ')';
+    }
+    return;
+  } else if(n.getMetaKind() == kind::metakind::OPERATOR) {
+    switch(Kind k = n.getKind()) {
+    case kind::FUNCTION_TYPE:
+    case kind::CONSTRUCTOR_TYPE:
+    case kind::SELECTOR_TYPE:
+    case kind::TESTER_TYPE:
+      if(n.getNumChildren() > 0) {
+        copy(n.begin(), n.end() - 1, ostream_iterator<TNode>(out, " -> "));
+        out << n[n.getNumChildren() - 1];
+      }
+      break;
+
+    case kind::ARRAY_TYPE:
+      out << "ARRAY " << n[0] << " OF " << n[1];
+      break;
+    case kind::SELECT:
+      out << n[0] << '[' << n[1] << ']';
+      break;
+    case kind::STORE:
+      out << n[0] << " WITH [" << n[1] << "] = " << n[2];
+      break;
+
+    case kind::TUPLE_TYPE:
+      out << '[';
+      copy(n.begin(), n.end() - 1, ostream_iterator<TNode>(out, ","));
+      out << n[n.getNumChildren() - 1];
+      out << ']';
+      break;
+    case kind::TUPLE:
+      out << "( ";
+      copy(n.begin(), n.end() - 1, ostream_iterator<TNode>(out, ", "));
+      out << n[n.getNumChildren() - 1];
+      out << " )";
+      break;
+
+    case kind::ITE:
+      out << "IF " << n[0] << " THEN " << n[1] << " ELSE " << n[2];
+      break;
+
+    default:
+      if(k == kind::NOT && n[0].getKind() == kind::EQUAL) {
+        // collapse NOT-over-EQUAL
+        out << n[0][0] << " /= " << n[0][1];
+      } else if(n.getNumChildren() == 2) {
+        // infix operator
+        out << n[0] << ' ' << n.getOperator() << ' ' << n[1];
+      } else {
+        // prefix operator
+        out << n.getOperator() << ' ';
+        if(n.getNumChildren() > 0) {
+          if(n.getNumChildren() > 1) {
+            copy(n.begin(), n.end() - 1, ostream_iterator<TNode>(out, " "));
+          }
+          out << n[n.getNumChildren() - 1];
+        }
+      }
+    }
+    return;
+  }
+
+  Unhandled();
+
 }/* CvcPrinter::toStream() */
 
 }/* CVC4::printer::cvc namespace */