mostly CVC presentation language parsing and printing

9 files changed, 1078 insertions, 270 deletions

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 21fc0a4a1..870c77383 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -136,8 +136,8 @@ IntegerType ExprManager::integerType() const {
   return IntegerType(Type(d_nodeManager, new TypeNode(d_nodeManager->integerType())));
 }
 
-Expr ExprManager::mkExpr(Kind kind, const Expr& child1) {
-  const unsigned n = 1;
+Expr ExprManager::mkExpr(Kind kind, Expr child1) {
+  const unsigned n = 1 - (kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED ? 1 : 0);
   CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
                 "Exprs with kind %s must have at least %u children and "
                 "at most %u children (the one under construction has %u)",
@@ -152,8 +152,8 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1) {
   }
 }
 
-Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2) {
-  const unsigned n = 2;
+Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2) {
+  const unsigned n = 2 - (kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED ? 1 : 0);
   CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
                 "Exprs with kind %s must have at least %u children and "
                 "at most %u children (the one under construction has %u)",
@@ -170,9 +170,9 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2) {
   }
 }
 
-Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
-                         const Expr& child3) {
-  const unsigned n = 3;
+Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2,
+                         Expr child3) {
+  const unsigned n = 3 - (kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED ? 1 : 0);
   CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
                 "Exprs with kind %s must have at least %u children and "
                 "at most %u children (the one under construction has %u)",
@@ -190,9 +190,9 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
   }
 }
 
-Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
-                         const Expr& child3, const Expr& child4) {
-  const unsigned n = 4;
+Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2,
+                         Expr child3, Expr child4) {
+  const unsigned n = 4 - (kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED ? 1 : 0);
   CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
                 "Exprs with kind %s must have at least %u children and "
                 "at most %u children (the one under construction has %u)",
@@ -211,10 +211,10 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
   }
 }
 
-Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
-                         const Expr& child3, const Expr& child4,
-                         const Expr& child5) {
-  const unsigned n = 5;
+Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2,
+                         Expr child3, Expr child4,
+                         Expr child5) {
+  const unsigned n = 5 - (kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED ? 1 : 0);
   CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
                 "Exprs with kind %s must have at least %u children and "
                 "at most %u children (the one under construction has %u)",
@@ -235,7 +235,7 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
 }
 
 Expr ExprManager::mkExpr(Kind kind, const std::vector<Expr>& children) {
-  const unsigned n = children.size();
+  const unsigned n = children.size() - (kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED ? 1 : 0);
   CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
                 "Exprs with kind %s must have at least %u children and "
                 "at most %u children (the one under construction has %u)",
@@ -259,9 +259,141 @@ Expr ExprManager::mkExpr(Kind kind, const std::vector<Expr>& children) {
   }
 }
 
+Expr ExprManager::mkExpr(Expr opExpr) {
+  const unsigned n = 0;
+  Kind kind = kind::operatorKindToKind(opExpr.getKind());
+  CheckArgument(kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
+                "This Expr constructor is for parameterized kinds only");
+  CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
+                "Exprs with kind %s must have at least %u children and "
+                "at most %u children (the one under construction has %u)",
+                kind::kindToString(kind).c_str(),
+                minArity(kind), maxArity(kind), n);
+  NodeManagerScope nms(d_nodeManager);
+  try {
+    INC_STAT(kind);
+    return Expr(this, d_nodeManager->mkNodePtr(opExpr.getNode()));
+  } catch (const TypeCheckingExceptionPrivate& e) {
+    throw TypeCheckingException(this, &e);
+  }
+}
+
+Expr ExprManager::mkExpr(Expr opExpr, Expr child1) {
+  const unsigned n = 1;
+  Kind kind = kind::operatorKindToKind(opExpr.getKind());
+  CheckArgument(kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
+                "This Expr constructor is for parameterized kinds only");
+  CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
+                "Exprs with kind %s must have at least %u children and "
+                "at most %u children (the one under construction has %u)",
+                kind::kindToString(kind).c_str(),
+                minArity(kind), maxArity(kind), n);
+  NodeManagerScope nms(d_nodeManager);
+  try {
+    INC_STAT(kind);
+    return Expr(this, d_nodeManager->mkNodePtr(opExpr.getNode(), child1.getNode()));
+  } catch (const TypeCheckingExceptionPrivate& e) {
+    throw TypeCheckingException(this, &e);
+  }
+}
+
+Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2) {
+  const unsigned n = 2;
+  Kind kind = kind::operatorKindToKind(opExpr.getKind());
+  CheckArgument(kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
+                "This Expr constructor is for parameterized kinds only");
+  CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
+                "Exprs with kind %s must have at least %u children and "
+                "at most %u children (the one under construction has %u)",
+                kind::kindToString(kind).c_str(),
+                minArity(kind), maxArity(kind), n);
+  NodeManagerScope nms(d_nodeManager);
+  try {
+    INC_STAT(kind);
+    return Expr(this, d_nodeManager->mkNodePtr(opExpr.getNode(),
+                                               child1.getNode(),
+                                               child2.getNode()));
+  } catch (const TypeCheckingExceptionPrivate& e) {
+    throw TypeCheckingException(this, &e);
+  }
+}
+
+Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3) {
+  const unsigned n = 3;
+  Kind kind = kind::operatorKindToKind(opExpr.getKind());
+  CheckArgument(kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
+                "This Expr constructor is for parameterized kinds only");
+  CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
+                "Exprs with kind %s must have at least %u children and "
+                "at most %u children (the one under construction has %u)",
+                kind::kindToString(kind).c_str(),
+                minArity(kind), maxArity(kind), n);
+  NodeManagerScope nms(d_nodeManager);
+  try {
+    INC_STAT(kind);
+    return Expr(this, d_nodeManager->mkNodePtr(opExpr.getNode(),
+                                               child1.getNode(),
+                                               child2.getNode(),
+                                               child3.getNode()));
+  } catch (const TypeCheckingExceptionPrivate& e) {
+    throw TypeCheckingException(this, &e);
+  }
+}
+
+Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3,
+                         Expr child4) {
+  const unsigned n = 4;
+  Kind kind = kind::operatorKindToKind(opExpr.getKind());
+  CheckArgument(kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
+                "This Expr constructor is for parameterized kinds only");
+  CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
+                "Exprs with kind %s must have at least %u children and "
+                "at most %u children (the one under construction has %u)",
+                kind::kindToString(kind).c_str(),
+                minArity(kind), maxArity(kind), n);
+  NodeManagerScope nms(d_nodeManager);
+  try {
+    INC_STAT(kind);
+    return Expr(this, d_nodeManager->mkNodePtr(opExpr.getNode(),
+                                               child1.getNode(),
+                                               child2.getNode(),
+                                               child3.getNode(),
+                                               child4.getNode()));
+  } catch (const TypeCheckingExceptionPrivate& e) {
+    throw TypeCheckingException(this, &e);
+  }
+}
+
+Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3,
+                         Expr child4, Expr child5) {
+  const unsigned n = 5;
+  Kind kind = kind::operatorKindToKind(opExpr.getKind());
+  CheckArgument(kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
+                "This Expr constructor is for parameterized kinds only");
+  CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
+                "Exprs with kind %s must have at least %u children and "
+                "at most %u children (the one under construction has %u)",
+                kind::kindToString(kind).c_str(),
+                minArity(kind), maxArity(kind), n);
+  NodeManagerScope nms(d_nodeManager);
+  try {
+    INC_STAT(kind);
+    return Expr(this, d_nodeManager->mkNodePtr(opExpr.getNode(),
+                                               child1.getNode(),
+                                               child2.getNode(),
+                                               child3.getNode(),
+                                               child4.getNode(),
+                                               child5.getNode()));
+  } catch (const TypeCheckingExceptionPrivate& e) {
+    throw TypeCheckingException(this, &e);
+  }
+}
+
 Expr ExprManager::mkExpr(Expr opExpr, const std::vector<Expr>& children) {
   const unsigned n = children.size();
   Kind kind = kind::operatorKindToKind(opExpr.getKind());
+  CheckArgument(kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
+                "This Expr constructor is for parameterized kinds only");
   CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
                 "Exprs with kind %s must have at least %u children and "
                 "at most %u children (the one under construction has %u)",
@@ -286,13 +418,13 @@ Expr ExprManager::mkExpr(Expr opExpr, const std::vector<Expr>& children) {
 }
 
 /** Make a function type from domain to range. */
-FunctionType ExprManager::mkFunctionType(const Type& domain, const Type& range) {
+FunctionType ExprManager::mkFunctionType(Type domain, Type range) {
   NodeManagerScope nms(d_nodeManager);
   return FunctionType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkFunctionType(*domain.d_typeNode, *range.d_typeNode))));
 }
 
 /** Make a function type with input types from argTypes. */
-FunctionType ExprManager::mkFunctionType(const std::vector<Type>& argTypes, const Type& range) {
+FunctionType ExprManager::mkFunctionType(const std::vector<Type>& argTypes, Type range) {
   NodeManagerScope nms(d_nodeManager);
   Assert( argTypes.size() >= 1 );
   std::vector<TypeNode> argTypeNodes;
@@ -436,7 +568,7 @@ SortConstructorType ExprManager::mkSortConstructor(const std::string& name,
  * @param check whether we should check the type as we compute it
  * (default: false)
  */
-Type ExprManager::getType(const Expr& e, bool check) throw (TypeCheckingException) {
+Type ExprManager::getType(Expr e, bool check) throw (TypeCheckingException) {
   NodeManagerScope nms(d_nodeManager);
   Type t;
   try {
@@ -448,7 +580,7 @@ Type ExprManager::getType(const Expr& e, bool check) throw (TypeCheckingExceptio
   return t;
 }
 
-Expr ExprManager::mkVar(const std::string& name, const Type& type) {
+Expr ExprManager::mkVar(const std::string& name, Type type) {
   NodeManagerScope nms(d_nodeManager);
   Node* n = d_nodeManager->mkVarPtr(name, *type.d_typeNode);
   Debug("nm") << "set " << name << " on " << *n << std::endl;
@@ -456,7 +588,7 @@ Expr ExprManager::mkVar(const std::string& name, const Type& type) {
   return Expr(this, n);
 }
 
-Expr ExprManager::mkVar(const Type& type) {
+Expr ExprManager::mkVar(Type type) {
   NodeManagerScope nms(d_nodeManager);
   INC_STAT_VAR(type);
   return Expr(this, d_nodeManager->mkVarPtr(*type.d_typeNode));
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 415d05878..31ce7855a 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -127,7 +127,7 @@ public:
    * @param child1 kind the kind of expression
    * @return the expression
    */
-  Expr mkExpr(Kind kind, const Expr& child1);
+  Expr mkExpr(Kind kind, Expr child1);
 
   /**
    * Make a binary expression of a given kind (AND, PLUS, ...).
@@ -136,7 +136,7 @@ public:
    * @param child2 the second child of the new expression
    * @return the expression
    */
-  Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2);
+  Expr mkExpr(Kind kind, Expr child1, Expr child2);
 
   /**
    * Make a 3-ary expression of a given kind (AND, PLUS, ...).
@@ -146,8 +146,7 @@ public:
    * @param child3 the third child of the new expression
    * @return the expression
    */
-  Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2,
-              const Expr& child3);
+  Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3);
 
   /**
    * Make a 4-ary expression of a given kind (AND, PLUS, ...).
@@ -158,8 +157,7 @@ public:
    * @param child4 the fourth child of the new expression
    * @return the expression
    */
-  Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2,
-              const Expr& child3, const Expr& child4);
+  Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4);
 
   /**
    * Make a 5-ary expression of a given kind (AND, PLUS, ...).
@@ -171,11 +169,13 @@ public:
    * @param child5 the fifth child of the new expression
    * @return the expression
    */
-  Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2,
-              const Expr& child3, const Expr& child4, const Expr& child5);
+  Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4,
+              Expr child5);
 
   /**
-   * Make an n-ary expression of given kind given a vector of it's children
+   * Make an n-ary expression of given kind given a vector of its
+   * children
+   *
    * @param kind the kind of expression to build
    * @param children the subexpressions
    * @return the n-ary expression
@@ -183,8 +183,73 @@ public:
   Expr mkExpr(Kind kind, const std::vector<Expr>& children);
 
   /**
-   * Make an n-ary expression of given tre operator to appply and a vector of
-   * it's children
+   * Make a nullary parameterized expression with the given operator.
+   *
+   * @param opExpr the operator expression
+   * @return the nullary expression
+   */
+  Expr mkExpr(Expr opExpr);
+
+  /**
+   * Make a unary parameterized expression with the given operator.
+   *
+   * @param opExpr the operator expression
+   * @param child1 the subexpression
+   * @return the unary expression
+   */
+  Expr mkExpr(Expr opExpr, Expr child1);
+
+  /**
+   * Make a binary parameterized expression with the given operator.
+   *
+   * @param opExpr the operator expression
+   * @param child1 the first subexpression
+   * @param child2 the second subexpression
+   * @return the binary expression
+   */
+  Expr mkExpr(Expr opExpr, Expr child1, Expr child2);
+
+  /**
+   * Make a ternary parameterized expression with the given operator.
+   *
+   * @param opExpr the operator expression
+   * @param child1 the first subexpression
+   * @param child2 the second subexpression
+   * @param child3 the third subexpression
+   * @return the ternary expression
+   */
+  Expr mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3);
+
+  /**
+   * Make a quaternary parameterized expression with the given operator.
+   *
+   * @param opExpr the operator expression
+   * @param child1 the first subexpression
+   * @param child2 the second subexpression
+   * @param child3 the third subexpression
+   * @param child4 the fourth subexpression
+   * @return the quaternary expression
+   */
+  Expr mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3, Expr child4);
+
+  /**
+   * Make a quinary parameterized expression with the given operator.
+   *
+   * @param opExpr the operator expression
+   * @param child1 the first subexpression
+   * @param child2 the second subexpression
+   * @param child3 the third subexpression
+   * @param child4 the fourth subexpression
+   * @param child5 the fifth subexpression
+   * @return the quinary expression
+   */
+  Expr mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3, Expr child4,
+              Expr child5);
+
+  /**
+   * Make an n-ary expression of given operator to apply and a vector
+   * of its children
+   *
    * @param opExpr the operator expression
    * @param children the subexpressions
    * @return the n-ary expression
@@ -210,13 +275,13 @@ public:
 
 
   /** Make a function type from domain to range. */
-  FunctionType mkFunctionType(const Type& domain, const Type& range);
+  FunctionType mkFunctionType(Type domain, Type range);
 
   /**
    * Make a function type with input types from argTypes.
    * <code>argTypes</code> must have at least one element.
    */
-  FunctionType mkFunctionType(const std::vector<Type>& argTypes, const Type& range);
+  FunctionType mkFunctionType(const std::vector<Type>& argTypes, Type range);
 
   /**
    * Make a function type with input types from
@@ -279,12 +344,12 @@ public:
                                         size_t arity) const;
 
   /** Get the type of an expression */
-  Type getType(const Expr& e, bool check = false)
+  Type getType(Expr e, bool check = false)
     throw (TypeCheckingException);
 
   // variables are special, because duplicates are permitted
-  Expr mkVar(const std::string& name, const Type& type);
-  Expr mkVar(const Type& type);
+  Expr mkVar(const std::string& name, Type type);
+  Expr mkVar(Type type);
 
   /** Returns the minimum arity of the given kind. */
   static unsigned minArity(Kind kind);
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 7f7d37a52..94b7e5c40 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -303,7 +303,35 @@ public:
   template <bool ref_count>
   Node* mkNodePtr(Kind kind, const std::vector<NodeTemplate<ref_count> >& children);
 
-  /** Create a node by applying an operator to the children */
+  /** Create a node (with no children) by operator. */
+  Node mkNode(TNode opNode);
+  Node* mkNodePtr(TNode opNode);
+
+  /** Create a node with one child by operator. */
+  Node mkNode(TNode opNode, TNode child1);
+  Node* mkNodePtr(TNode opNode, TNode child1);
+
+  /** Create a node with two children by operator. */
+  Node mkNode(TNode opNode, TNode child1, TNode child2);
+  Node* mkNodePtr(TNode opNode, TNode child1, TNode child2);
+
+  /** Create a node with three children by operator. */
+  Node mkNode(TNode opNode, TNode child1, TNode child2, TNode child3);
+  Node* mkNodePtr(TNode opNode, TNode child1, TNode child2, TNode child3);
+
+  /** Create a node with four children by operator. */
+  Node mkNode(TNode opNode, TNode child1, TNode child2, TNode child3,
+              TNode child4);
+  Node* mkNodePtr(TNode opNode, TNode child1, TNode child2, TNode child3,
+              TNode child4);
+
+  /** Create a node with five children by operator. */
+  Node mkNode(TNode opNode, TNode child1, TNode child2, TNode child3,
+              TNode child4, TNode child5);
+  Node* mkNodePtr(TNode opNode, TNode child1, TNode child2, TNode child3,
+              TNode child4, TNode child5);
+
+  /** Create a node by applying an operator to the children. */
   template <bool ref_count>
   Node mkNode(TNode opNode, const std::vector<NodeTemplate<ref_count> >& children);
   template <bool ref_count>
@@ -1021,6 +1049,85 @@ inline Node* NodeManager::mkNodePtr(Kind kind,
   return nb.constructNodePtr();
 }
 
+// for operators
+inline Node NodeManager::mkNode(TNode opNode) {
+  NodeBuilder<1> nb(this, kind::operatorKindToKind(opNode.getKind()));
+  nb << opNode;
+  return nb.constructNode();
+}
+
+inline Node* NodeManager::mkNodePtr(TNode opNode) {
+  NodeBuilder<1> nb(this, kind::operatorKindToKind(opNode.getKind()));
+  nb << opNode;
+  return nb.constructNodePtr();
+}
+
+inline Node NodeManager::mkNode(TNode opNode, TNode child1) {
+  NodeBuilder<2> nb(this, kind::operatorKindToKind(opNode.getKind()));
+  nb << opNode << child1;
+  return nb.constructNode();
+}
+
+inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1) {
+  NodeBuilder<2> nb(this, kind::operatorKindToKind(opNode.getKind()));
+  nb << opNode << child1;
+  return nb.constructNodePtr();
+}
+
+inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2) {
+  NodeBuilder<3> nb(this, kind::operatorKindToKind(opNode.getKind()));
+  nb << opNode << child1 << child2;
+  return nb.constructNode();
+}
+
+inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2) {
+  NodeBuilder<3> nb(this, kind::operatorKindToKind(opNode.getKind()));
+  nb << opNode << child1 << child2;
+  return nb.constructNodePtr();
+}
+
+inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2,
+                                TNode child3) {
+  NodeBuilder<4> nb(this, kind::operatorKindToKind(opNode.getKind()));
+  nb << opNode << child1 << child2 << child3;
+  return nb.constructNode();
+}
+
+inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2,
+                                TNode child3) {
+  NodeBuilder<4> nb(this, kind::operatorKindToKind(opNode.getKind()));
+  nb << opNode << child1 << child2 << child3;
+  return nb.constructNodePtr();
+}
+
+inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2,
+                                TNode child3, TNode child4) {
+  NodeBuilder<5> nb(this, kind::operatorKindToKind(opNode.getKind()));
+  nb << opNode << child1 << child2 << child3 << child4;
+  return nb.constructNode();
+}
+
+inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2,
+                                TNode child3, TNode child4) {
+  NodeBuilder<5> nb(this, kind::operatorKindToKind(opNode.getKind()));
+  nb << opNode << child1 << child2 << child3 << child4;
+  return nb.constructNodePtr();
+}
+
+inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2,
+                                TNode child3, TNode child4, TNode child5) {
+  NodeBuilder<6> nb(this, kind::operatorKindToKind(opNode.getKind()));
+  nb << opNode << child1 << child2 << child3 << child4 << child5;
+  return nb.constructNode();
+}
+
+inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2,
+                                    TNode child3, TNode child4, TNode child5) {
+  NodeBuilder<6> nb(this, kind::operatorKindToKind(opNode.getKind()));
+  nb << opNode << child1 << child2 << child3 << child4 << child5;
+  return nb.constructNodePtr();
+}
+
 // N-ary version for operators
 template <bool ref_count>
 inline Node NodeManager::mkNode(TNode opNode,
@@ -1034,8 +1141,8 @@ inline Node NodeManager::mkNode(TNode opNode,
 
 template <bool ref_count>
 inline Node* NodeManager::mkNodePtr(TNode opNode,
-                                const std::vector<NodeTemplate<ref_count> >&
-                                children) {
+                                    const std::vector<NodeTemplate<ref_count> >&
+                                    children) {
   NodeBuilder<> nb(this, kind::operatorKindToKind(opNode.getKind()));
   nb << opNode;
   nb.append(children);
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 33e576a32..96a8346b0 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -24,6 +24,323 @@ options {
   k = 2;
 }
 
+tokens {
+  // Keywords
+
+  AND_TOK = 'AND';
+  ASSERT_TOK = 'ASSERT';
+  BOOLEAN_TOK = 'BOOLEAN';
+  CHECKSAT_TOK = 'CHECKSAT';
+  ECHO_TOK = 'ECHO';
+  ELSEIF_TOK = 'ELSIF';
+  ELSE_TOK = 'ELSE';
+  ENDIF_TOK = 'ENDIF';
+  FALSE_TOK = 'FALSE';
+  IF_TOK = 'IF';
+  IN_TOK = 'IN';
+  INT_TOK = 'INT';
+  LET_TOK = 'LET';
+  NOT_TOK = 'NOT';
+  OPTION_TOK = 'OPTION';
+  OR_TOK = 'OR';
+  POPTO_TOK = 'POPTO';
+  POP_TOK = 'POP';
+  PRINT_TOK = 'PRINT';
+  PUSH_TOK = 'PUSH';
+  QUERY_TOK = 'QUERY';
+  REAL_TOK = 'REAL';
+  THEN_TOK = 'THEN';
+  TRUE_TOK = 'TRUE';
+  TYPE_TOK = 'TYPE';
+  XOR_TOK = 'XOR';
+
+  DATATYPE_TOK = 'DATATYPE';
+  END_TOK = 'END';
+
+  ARRAY_TOK = 'ARRAY';
+  OF_TOK = 'OF';
+  WITH_TOK = 'WITH';
+
+  FORALL_TOK = 'FORALL';
+  EXISTS_TOK = 'EXISTS';
+
+  // Symbols
+
+  COLON = ':';
+  COMMA = ',';
+  LPAREN = '(';
+  RPAREN = ')';
+  LBRACE = '{';
+  RBRACE = '}';
+  LBRACKET = '[';
+  RBRACKET = ']';
+  SEMICOLON = ';';
+  BAR = '|';
+  DOT = '.';
+
+  SQHASH = '[#';
+  HASHSQ = '#]';
+  PARENHASH = '(#';
+  HASHPAREN = '#)';
+
+  // Operators
+
+  ARROW_TOK = '->';
+  DIV_TOK = '/';
+  EQUAL_TOK = '=';
+  DISEQUAL_TOK = '/=';
+  EXP_TOK = '^';
+  GT_TOK = '>';
+  GEQ_TOK = '>=';
+  IFF_TOK = '<=>';
+  IMPLIES_TOK = '=>';
+  LT_TOK = '<';
+  LEQ_TOK = '<=';
+  MINUS_TOK = '-';
+  PLUS_TOK = '+';
+  STAR_TOK = '*';
+  ASSIGN_TOK = ':=';
+  MOD_TOK = 'MOD';
+  INTDIV_TOK = 'DIV';
+  FLOOR_TOK = 'FLOOR';
+
+  //IS_INTEGER_TOK = 'IS_INTEGER';
+
+  // Bitvectors
+
+  BITVECTOR_TOK = 'BITVECTOR';
+  LEFTSHIFT_TOK = '<<';
+  RIGHTSHIFT_TOK = '>>';
+  BVPLUS_TOK = 'BVPLUS';
+  BVSUB_TOK = 'BVSUB';
+  BVUDIV_TOK = 'BVUDIV';
+  BVSDIV_TOK = 'BVSDIV';
+  BVUREM_TOK = 'BVUREM';
+  BVSREM_TOK = 'BVSREM';
+  BVSMOD_TOK = 'BVSMOD';
+  BVSHL_TOK = 'BVSHL';
+  BVASHR_TOK = 'BVASHR';
+  BVLSHR_TOK = 'BVLSHR';
+  BVUMINUS_TOK = 'BVUMINUS';
+  BVMULT_TOK = 'BVMULT';
+  BVNEG_TOK = '~';
+  BVAND_TOK = '&';
+  BVXOR_TOK = 'BVXOR';
+  BVNAND_TOK = 'BVNAND';
+  BVNOR_TOK = 'BVNOR';
+  BVCOMP_TOK = 'BVCOMP';
+  BVXNOR_TOK = 'BVXNOR';
+  CONCAT_TOK = '@';
+  BVTOINT_TOK = 'BVTOINT';
+  INTTOBV_TOK = 'INTTOBV';
+  BOOLEXTRACT_TOK = 'BOOLEXTRACT';
+  BVLT_TOK = 'BVLT';
+  BVGT_TOK = 'BVGT';
+  BVLE_TOK = 'BVLE';
+  BVGE_TOK = 'BVGE';
+  SX_TOK = 'SX';
+  BVZEROEXTEND_TOK = 'BVZEROEXTEND';
+  BVREPEAT_TOK = 'BVREPEAT';
+  BVROTL_TOK = 'BVROTL';
+  BVROTR_TOK = 'BVROTR';
+  BVSLT_TOK = 'BVSLT';
+  BVSGT_TOK = 'BVSGT';
+  BVSLE_TOK = 'BVSLE';
+  BVSGE_TOK = 'BVSGE';
+}
+
+@parser::members {
+
+// Idea and code guidance from Sam Harwell,
+// http://www.antlr.org/wiki/display/ANTLR3/Operator+precedence+parser
+
+bool isRightToLeft(int type) {
+  // return true here for any operators that are right-to-left associative
+  switch(type) {
+  case IMPLIES_TOK: return true;
+  default: return false;
+  }
+}
+
+int getOperatorPrecedence(int type) {
+  switch(type) {
+  case BITVECTOR_TOK: return 1;
+  case DOT:
+  case LPAREN:
+  case LBRACE: return 2;
+  case LBRACKET: return 3;
+  case ARROW_TOK: return 4;
+  //case IS_INTEGER_TOK: return 5;
+  case BVSLT_TOK:
+  case BVSLE_TOK:
+  case BVSGT_TOK:
+  case BVSGE_TOK: return 6;
+  case BVLT_TOK:
+  case BVLE_TOK:
+  case BVGT_TOK:
+  case BVGE_TOK: return 7;
+  case LEFTSHIFT_TOK:
+  case RIGHTSHIFT_TOK: return 8;
+  case SX_TOK:
+  case BVZEROEXTEND_TOK:
+  case BVREPEAT_TOK:
+  case BVROTL_TOK:
+  case BVROTR_TOK: return 9;
+  case BVUDIV_TOK:
+  case BVSDIV_TOK:
+  case BVUREM_TOK:
+  case BVSREM_TOK:
+  case BVSMOD_TOK:
+  case BVSHL_TOK:
+  case BVASHR_TOK:
+  case BVLSHR_TOK: return 10;
+  case BVUMINUS_TOK:
+  case BVPLUS_TOK:
+  case BVSUB_TOK: return 11;
+  case BVNEG_TOK: return 12;
+  case BVXNOR_TOK: return 13;
+  case BVNOR_TOK:
+  case BVCOMP_TOK: return 14;
+  case BVNAND_TOK: return 15;
+  case BVXOR_TOK: return 16;
+  case BVAND_TOK: return 17;
+  case BAR: return 18;
+  case CONCAT_TOK: return 19;
+//case UMINUS_TOK: return 20;
+  case WITH_TOK: return 21;
+  case EXP_TOK: return 22;
+  case STAR_TOK:
+  case INTDIV_TOK:
+  case DIV_TOK:
+  case MOD_TOK: return 23;
+  case PLUS_TOK:
+  case MINUS_TOK: return 24;
+  case LEQ_TOK:
+  case LT_TOK:
+  case GEQ_TOK:
+  case GT_TOK:
+  case FLOOR_TOK: return 25;
+  case EQUAL_TOK:
+  case DISEQUAL_TOK: return 26;
+  case NOT_TOK: return 27;
+  case AND_TOK: return 28;
+  case OR_TOK:
+  case XOR_TOK: return 29;
+  case IMPLIES_TOK: return 30;// right-to-left
+  case IFF_TOK: return 31;
+  case FORALL_TOK:
+  case EXISTS_TOK: return 32;
+  case ASSIGN_TOK:
+  case IN_TOK: return 33;
+
+  default:
+    Unhandled(CvcParserTokenNames[type]);
+  }
+}
+
+Kind getOperatorKind(int type, bool& negate) {
+  negate = false;
+
+  switch(type) {
+    // booleanBinop
+  case IFF_TOK: return kind::IFF;
+  case IMPLIES_TOK: return kind::IMPLIES;
+  case OR_TOK: return kind::OR;
+  case XOR_TOK: return kind::XOR;
+  case AND_TOK: return kind::AND;
+
+    // comparisonBinop
+  case EQUAL_TOK: return kind::EQUAL;
+  case DISEQUAL_TOK: negate = true; return kind::EQUAL;
+  case GT_TOK: return kind::GT;
+  case GEQ_TOK: return kind::GEQ;
+  case LT_TOK: return kind::LT;
+  case LEQ_TOK: return kind::LEQ;
+
+    // arithmeticBinop
+  case PLUS_TOK: return kind::PLUS;
+  case MINUS_TOK: return kind::MINUS;
+  case STAR_TOK: return kind::MULT;
+  case INTDIV_TOK: Unhandled(CvcParserTokenNames[type]);
+  case DIV_TOK: return kind::DIVISION;
+  case EXP_TOK: Unhandled(CvcParserTokenNames[type]);
+
+    // concatBitwiseBinop
+  case CONCAT_TOK: return kind::BITVECTOR_CONCAT;
+  case BAR: return kind::BITVECTOR_OR;
+  case BVAND_TOK: return kind::BITVECTOR_AND;
+
+  default:
+    Unhandled(CvcParserTokenNames[type]);
+  }
+}
+
+unsigned findPivot(const std::vector<unsigned>& operators,
+                   unsigned startIndex, unsigned stopIndex) {
+  unsigned pivot = startIndex;
+  unsigned pivotRank = getOperatorPrecedence(operators[pivot]);
+  /*Debug("prec") << "initial pivot at " << pivot
+                << "(" << CvcParserTokenNames[operators[pivot]] << ") "
+                << "level " << pivotRank << std::endl;*/
+  for(unsigned i = startIndex + 1; i <= stopIndex; ++i) {
+    unsigned current = getOperatorPrecedence(operators[i]);
+    bool rtl = isRightToLeft(operators[i]);
+    if(current > pivotRank || (current == pivotRank && !rtl)) {
+      /*Debug("prec") << "new pivot at " << i
+                    << "(" << CvcParserTokenNames[operators[i]] << ") "
+                    << "level " << current << " rtl == " << rtl << std::endl;*/
+      pivot = i;
+      pivotRank = current;
+    }
+  }
+  return pivot;
+}
+
+Expr createPrecedenceTree(ExprManager* em,
+                          const std::vector<CVC4::Expr>& expressions,
+                          const std::vector<unsigned>& operators,
+                          unsigned startIndex, unsigned stopIndex) {
+  Assert(expressions.size() == operators.size() + 1);
+  Assert(startIndex < expressions.size());
+  Assert(stopIndex < expressions.size());
+  Assert(startIndex <= stopIndex);
+
+  if(stopIndex == startIndex) {
+    return expressions[startIndex];
+  }
+
+  unsigned pivot = findPivot(operators, startIndex, stopIndex - 1);
+  //Debug("prec") << "pivot[" << startIndex << "," << stopIndex - 1 << "] at " << pivot << std::endl;
+  bool negate;
+  Expr e = em->mkExpr(getOperatorKind(operators[pivot], negate),
+                      createPrecedenceTree(em, expressions, operators, startIndex, pivot),
+                      createPrecedenceTree(em, expressions, operators, pivot + 1, stopIndex));
+  return negate ? em->mkExpr(kind::NOT, e) : e;
+}
+
+Expr createPrecedenceTree(ExprManager* em,
+                          const std::vector<CVC4::Expr>& expressions,
+                          const std::vector<unsigned>& operators) {
+  if(Debug.isOn("prec") && operators.size() > 1) {
+    for(unsigned i = 0; i < expressions.size(); ++i) {
+      Debug("prec") << expressions[i];
+      if(operators.size() > i) {
+        Debug("prec") << ' ' << CvcParserTokenNames[operators[i]] << ' ';
+      }
+    }
+    Debug("prec") << std::endl;
+  }
+
+  Expr e = createPrecedenceTree(em, expressions, operators, 0, expressions.size() - 1);
+  if(Debug.isOn("prec") && operators.size() > 1) {
+    Expr::setlanguage::Scope ls(Debug("prec"), language::output::LANG_AST);
+    Debug("prec") << "=> " << e << std::endl;
+  }
+  return e;
+}
+
+}/* @parser::members */
+
 @header {
 /**
  ** This file is part of the CVC4 prototype.
@@ -178,21 +495,41 @@ declaration[CVC4::Command*& cmd]
   Debug("parser-extra") << "declaration: " << AntlrInput::tokenText(LT(1)) << std::endl;
 }
   : // FIXME: These could be type or function declarations, if that matters.
-    identifierList[ids, CHECK_UNDECLARED, SYM_VARIABLE] COLON declType[t,ids] SEMICOLON
-    { cmd = new DeclarationCommand(ids,t); }
+    identifierList[ids, CHECK_UNDECLARED, SYM_VARIABLE] COLON declType[t, ids] SEMICOLON
+    { cmd = new DeclarationCommand(ids, t); }
   ;
 
 /** Match the right-hand side of a declaration. Returns the type. */
 declType[CVC4::Type& t, std::vector<std::string>& idList]
 @init {
+  Expr f;
   Debug("parser-extra") << "declType: " << AntlrInput::tokenText(LT(1)) << std::endl;
 }
   : /* A sort declaration (e.g., "T : TYPE") */
     TYPE_TOK
     { PARSER_STATE->mkSorts(idList);
       t = EXPR_MANAGER->kindType(); }
+  | /* A type alias */
+    TYPE_TOK EQUAL_TOK type[t]
+    { for(std::vector<std::string>::const_iterator i = idList.begin();
+          i != idList.end();
+          ++i) {
+        PARSER_STATE->defineType(*i, t);
+      }
+      t = EXPR_MANAGER->kindType(); }
   | /* A variable declaration */
-    type[t] { PARSER_STATE->mkVars(idList,t); }
+    type[t] ( EQUAL_TOK formula[f] )?
+    { if(f.isNull()) {
+        PARSER_STATE->mkVars(idList, t);
+      } else {
+        for(std::vector<std::string>::const_iterator i = idList.begin(),
+              i_end = idList.end();
+            i != i_end;
+            ++i) {
+          PARSER_STATE->defineFunction(*i, f);
+        }
+      }
+    }
   ;
 
 /**
@@ -206,16 +543,16 @@ type[CVC4::Type& t]
   Debug("parser-extra") << "type: " << AntlrInput::tokenText(LT(1)) << std::endl;
 }
   : /* Simple type */
-    baseType[t]
+    bitvectorType[t]
   | /* Single-parameter function type */
     baseType[t] ARROW_TOK baseType[t2]
-    { t = EXPR_MANAGER->mkFunctionType(t,t2); }
+    { t = EXPR_MANAGER->mkFunctionType(t, t2); }
   | /* Multi-parameter function type */
     LPAREN baseType[t]
     { typeList.push_back(t); }
-    (COMMA baseType[t] { typeList.push_back(t); } )+
+    ( COMMA baseType[t] { typeList.push_back(t); } )*
     RPAREN ARROW_TOK baseType[t]
-    { t = EXPR_MANAGER->mkFunctionType(typeList,t); }
+    { t = EXPR_MANAGER->mkFunctionType(typeList, t); }
   ;
 
 /**
@@ -247,6 +584,24 @@ identifier[std::string& id,
   ;
 
 /**
+ * Matches a bitvector type.
+ */
+bitvectorType[CVC4::Type& t]
+  : arrayType[t]
+  | BITVECTOR_TOK LPAREN INTEGER_LITERAL RPAREN
+    { t = EXPR_MANAGER->mkBitVectorType(AntlrInput::tokenToUnsigned($INTEGER_LITERAL)); }
+  ;
+
+arrayType[CVC4::Type& t]
+@init {
+  Type t2;
+}
+  : baseType[t]
+  | ARRAY_TOK baseType[t] OF_TOK baseType[t2]
+    { t = EXPR_MANAGER->mkArrayType(t, t2); }
+  ;
+
+/**
  * Matches a type (which MUST be already declared).
  *
  * @return the type identifier
@@ -262,9 +617,7 @@ baseType[CVC4::Type& t]
  * CHECK_DECLARED and the type is not declared, an exception is
  * thrown.
  *
- * @return the type identifier
- *
- * @TODO parse more types
+ * @return the type identifier in 't', and the id (where applicable) in 'id'
  */
 maybeUndefinedBaseType[CVC4::Type& t,
                        CVC4::parser::DeclarationCheck check] returns [CVC4::parser::cvc::mystring id]
@@ -336,7 +689,7 @@ letBinding[CVC4::Expr& f]
     letDecls
     IN_TOK letBinding[f]
     { PARSER_STATE->popScope(); }
-  | iffFormula[f]
+  | booleanFormula[f]
   ;
 
 /**
@@ -359,193 +712,305 @@ letDecl
     { PARSER_STATE->defineVar(name, e); }
   ;
 
-/**
- * Matches a Boolean IFF formula (right-associative)
- */
-iffFormula[CVC4::Expr& f]
+booleanFormula[CVC4::Expr& f]
 @init {
-  Expr e;
-  Debug("parser-extra") << "<=> formula: " << AntlrInput::tokenText(LT(1)) << std::endl;
+  std::vector<CVC4::Expr> expressions;
+  std::vector<unsigned> operators;
+  unsigned op;
+  unsigned notCount = 0;
 }
-  : impliesFormula[f]
-    ( IFF_TOK
-    	iffFormula[e]
-        { f = MK_EXPR(CVC4::kind::IFF, f, e); }
-    )?
+  : ( NOT_TOK { ++notCount; } )* comparison[f]
+    { while(notCount > 0) {
+        --notCount;
+        f = EXPR_MANAGER->mkExpr(kind::NOT, f);
+      }
+      expressions.push_back(f); }
+    ( booleanBinop[op] ( NOT_TOK { ++notCount; } )* comparison[f]
+      { operators.push_back(op);
+        while(notCount > 0) {
+          --notCount;
+          f = EXPR_MANAGER->mkExpr(kind::NOT, f);
+        }
+        expressions.push_back(f);
+      }
+    )*
+    { f = createPrecedenceTree(EXPR_MANAGER, expressions, operators); }
   ;
 
-/**
- * Matches a Boolean IMPLIES formula (right-associative)
- */
-impliesFormula[CVC4::Expr& f]
+booleanBinop[unsigned& op]
 @init {
-  Expr e;
-  Debug("parser-extra") << "=> Formula: " << AntlrInput::tokenText(LT(1)) << std::endl;
+  op = LT(1)->getType(LT(1));
 }
-  : orFormula[f]
-    ( IMPLIES_TOK impliesFormula[e]
-        { f = MK_EXPR(CVC4::kind::IMPLIES, f, e); }
-    )?
+  : IFF_TOK
+  | IMPLIES_TOK
+  | OR_TOK
+  | XOR_TOK
+  | AND_TOK
   ;
 
-/**
- * Matches a Boolean OR formula (left-associative)
- */
-orFormula[CVC4::Expr& f]
+comparison[CVC4::Expr& f]
 @init {
-  std::vector<Expr> exprs;
-  Debug("parser-extra") << "OR Formula: " << AntlrInput::tokenText(LT(1)) << std::endl;
+  std::vector<CVC4::Expr> expressions;
+  std::vector<unsigned> operators;
+  unsigned op;
 }
-  : xorFormula[f]
-      ( OR_TOK  { exprs.push_back(f); }
-        xorFormula[f] { exprs.push_back(f); } )*
-    {
-      if( exprs.size() > 0 ) {
-        f = MK_EXPR(CVC4::kind::OR, exprs);
-      }
-    }
+  : term[f] { expressions.push_back(f); }
+    ( comparisonBinop[op] term[f]
+      { operators.push_back(op); expressions.push_back(f); } )*
+    { f = createPrecedenceTree(EXPR_MANAGER, expressions, operators); }
   ;
 
-/**
- * Matches a Boolean XOR formula (left-associative)
- */
-xorFormula[CVC4::Expr& f]
+comparisonBinop[unsigned& op]
 @init {
-  Expr e;
-  Debug("parser-extra") << "XOR formula: " << AntlrInput::tokenText(LT(1)) << std::endl;
+  op = LT(1)->getType(LT(1));
 }
-  : andFormula[f]
-    ( XOR_TOK andFormula[e]
-      { f = MK_EXPR(CVC4::kind::XOR,f, e); }
-    )*
+  : EQUAL_TOK
+  | DISEQUAL_TOK
+  | GT_TOK
+  | GEQ_TOK
+  | LT_TOK
+  | LEQ_TOK
   ;
 
-/**
- * Matches a Boolean AND formula (left-associative)
- */
-andFormula[CVC4::Expr& f]
+term[CVC4::Expr& f]
 @init {
-  std::vector<Expr> exprs;
-  Debug("parser-extra") << "AND Formula: " << AntlrInput::tokenText(LT(1)) << std::endl;
+  std::vector<CVC4::Expr> expressions;
+  std::vector<unsigned> operators;
+  unsigned op;
 }
-  : notFormula[f]
-    ( AND_TOK { exprs.push_back(f); }
-      notFormula[f] { exprs.push_back(f); } )*
-    {
-      if( exprs.size() > 0 ) {
-        f = MK_EXPR(CVC4::kind::AND, exprs);
-      }
-    }
+  : storeTerm[f] { expressions.push_back(f); }
+    ( arithmeticBinop[op] storeTerm[f] { operators.push_back(op); expressions.push_back(f); } )*
+    { f = createPrecedenceTree(EXPR_MANAGER, expressions, operators); }
   ;
 
-/**
- * Parses a NOT formula.
- * @return the expression representing the formula
- */
-notFormula[CVC4::Expr& f]
+arithmeticBinop[unsigned& op]
 @init {
-  Debug("parser-extra") << "NOT formula: " << AntlrInput::tokenText(LT(1)) << std::endl;
+  op = LT(1)->getType(LT(1));
 }
-  : /* negation */
-    NOT_TOK notFormula[f]
-    { f = MK_EXPR(CVC4::kind::NOT, f); }
-  | /* a boolean atom */
-    comparisonFormula[f]
+  : PLUS_TOK
+  | MINUS_TOK
+  | STAR_TOK
+  | INTDIV_TOK
+  | DIV_TOK
+  | EXP_TOK
   ;
 
-/** Parses a comparison formula (non-associative).
-    NOTE: equality should technically have higher precedence than
-    greater-than, less-than, etc., but I don't think this will ever
-    be relevant in a well-typed formula.
-*/
-comparisonFormula[CVC4::Expr& f]
+/** Parses an array store term. */
+storeTerm[CVC4::Expr& f]
 @init {
-  Expr e;
-  Kind op;
-  bool negate;
-  Debug("parser-extra") << "predicate formula: " << AntlrInput::tokenText(LT(1)) << std::endl;
-}
-  : plusTerm[f]
-    ( ( EQUAL_TOK { op = CVC4::kind::EQUAL; negate = false; }
-      | DISEQUAL_TOK { op = CVC4::kind::EQUAL; negate = true; }
-      | GT_TOK { op = CVC4::kind::GT; negate = false; }
-      | GEQ_TOK { op = CVC4::kind::GEQ; negate = false; }
-      | LT_TOK { op = CVC4::kind::LT; negate = false; }
-      | LEQ_TOK { op = CVC4::kind::LEQ; negate = false; })
-      plusTerm[e]
-      { f = MK_EXPR(op, f, e);
-        if(negate) {
-          f = MK_EXPR(CVC4::kind::NOT, f);
-        }
+  Expr f2, f3;
+}
+  : uminusTerm[f] ( WITH_TOK
+    LBRACKET formula[f2] RBRACKET ASSIGN_TOK uminusTerm[f3]
+    { f = MK_EXPR(CVC4::kind::STORE, f, f2, f3); }
+    ( COMMA LBRACKET formula[f2] RBRACKET ASSIGN_TOK uminusTerm[f3]
+      { f = MK_EXPR(CVC4::kind::STORE, f, f2, f3); } )* )*
+  ;
+
+/** Parses a unary minus term. */
+uminusTerm[CVC4::Expr& f]
+@init {
+  unsigned minusCount = 0;
+}
+  : /* Unary minus */
+//    (MINUS_TOK { ++minusCount; })* concatBitwiseTerm[f]
+    (MINUS_TOK { ++minusCount; })+ concatBitwiseTerm[f]
+    { while(minusCount > 0) { --minusCount; f = MK_EXPR(CVC4::kind::UMINUS, f); } }
+  | concatBitwiseTerm[f]
+  ;
+
+/** Parses bitvectors. */
+
+concatBitwiseTerm[CVC4::Expr& f]
+@init {
+  std::vector<CVC4::Expr> expressions;
+  std::vector<unsigned> operators;
+  unsigned op;
+}
+  : bitwiseXorTerm[f] { expressions.push_back(f); }
+    ( concatBitwiseBinop[op] bitwiseXorTerm[f] { operators.push_back(op); expressions.push_back(f); } )*
+    { f = createPrecedenceTree(EXPR_MANAGER, expressions, operators); }
+  ;
+concatBitwiseBinop[unsigned& op]
+@init {
+  op = LT(1)->getType(LT(1));
+}
+  : CONCAT_TOK
+  | BAR
+  | BVAND_TOK
+  ;
+
+bitwiseXorTerm[CVC4::Expr& f]
+@init {
+  Expr f2;
+}
+  : /* BV xor */
+    BVXOR_TOK LPAREN formula[f] COMMA formula[f] RPAREN
+    { f = MK_EXPR(CVC4::kind::BITVECTOR_XOR, f, f2); }
+  | BVNAND_TOK LPAREN formula[f] COMMA formula[f] RPAREN
+    { f = MK_EXPR(CVC4::kind::BITVECTOR_NAND, f, f2); }
+  | BVNOR_TOK LPAREN formula[f] COMMA formula[f] RPAREN
+    { f = MK_EXPR(CVC4::kind::BITVECTOR_NOR, f, f2); }
+  | BVCOMP_TOK LPAREN formula[f] COMMA formula[f] RPAREN
+    { f = MK_EXPR(CVC4::kind::BITVECTOR_COMP, f, f2); }
+  | BVXNOR_TOK LPAREN formula[f] COMMA formula[f] RPAREN
+    { f = MK_EXPR(CVC4::kind::BITVECTOR_XNOR, f, f2); }
+  | bvNegTerm[f]
+  ;
+bvNegTerm[CVC4::Expr& f]
+  : /* BV neg */
+    BVNEG_TOK bvNegTerm[f]
+    { f = MK_EXPR(CVC4::kind::BITVECTOR_NOT, f); }
+  | bvUminusTerm[f]
+  ;
+bvUminusTerm[CVC4::Expr& f]
+@init {
+  Expr f2;
+}
+  : /* BV unary minus */
+    BVUMINUS_TOK LPAREN formula[f] RPAREN
+    { f = MK_EXPR(CVC4::kind::BITVECTOR_NEG, f); }
+  | BVPLUS_TOK LPAREN INTEGER_LITERAL COMMA formula[f]
+    ( COMMA formula[f2] { f = MK_EXPR(CVC4::kind::BITVECTOR_PLUS, f, f2); } )+ RPAREN
+    { unsigned size = BitVectorType(f.getType()).getSize();
+      unsigned k = AntlrInput::tokenToUnsigned($INTEGER_LITERAL);
+      if(k == 0) {
+        PARSER_STATE->parseError("BVPLUS(k,_,_,...) must have k > 0");
       }
-    )?
+      if(k > size) {
+        f = MK_EXPR(MK_CONST(BitVectorZeroExtend(k)), f);
+      } else if(k < size) {
+        f = MK_EXPR(MK_CONST(BitVectorExtract(0, k - 1)), f);
+      }
+    }
+  | BVSUB_TOK LPAREN INTEGER_LITERAL COMMA formula[f] COMMA formula[f2] RPAREN
+    { f = MK_EXPR(CVC4::kind::BITVECTOR_SUB, f, f2);
+      unsigned k = AntlrInput::tokenToUnsigned($INTEGER_LITERAL);
+      if(k == 0) {
+        PARSER_STATE->parseError("BVSUB(k,_,_) must have k > 0");
+      }
+      unsigned size = BitVectorType(f.getType()).getSize();
+      if(k > size) {
+        f = MK_EXPR(MK_CONST(BitVectorZeroExtend(k)), f);
+      } else if(k < size) {
+        f = MK_EXPR(MK_CONST(BitVectorExtract(0, k - 1)), f);
+      }
+    }
+  | BVMULT_TOK LPAREN INTEGER_LITERAL COMMA formula[f] COMMA formula[f2] RPAREN
+    { MK_EXPR(CVC4::kind::BITVECTOR_MULT, f, f2);
+      unsigned k = AntlrInput::tokenToUnsigned($INTEGER_LITERAL);
+      if(k == 0) {
+        PARSER_STATE->parseError("BVMULT(k,_,_) must have k > 0");
+      }
+      unsigned size = BitVectorType(f.getType()).getSize();
+      if(k > size) {
+        f = MK_EXPR(MK_CONST(BitVectorZeroExtend(k)), f);
+      } else if(k < size) {
+        f = MK_EXPR(MK_CONST(BitVectorExtract(0, k - 1)), f);
+      }
+    }
+  | BVUDIV_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
+    { f = MK_EXPR(CVC4::kind::BITVECTOR_UDIV, f, f2); }
+  | BVSDIV_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
+    { f = MK_EXPR(CVC4::kind::BITVECTOR_SDIV, f, f2); }
+  | BVUREM_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
+    { f = MK_EXPR(CVC4::kind::BITVECTOR_UREM, f, f2); }
+  | BVSREM_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
+    { f = MK_EXPR(CVC4::kind::BITVECTOR_SREM, f, f2); }
+  | BVSMOD_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
+    { f = MK_EXPR(CVC4::kind::BITVECTOR_SMOD, f, f2); }
+  | BVSHL_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
+    { f = MK_EXPR(CVC4::kind::BITVECTOR_SHL, f, f2); }
+  | BVASHR_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
+    { f = MK_EXPR(CVC4::kind::BITVECTOR_ASHR, f, f2); }
+  | BVLSHR_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
+    { f = MK_EXPR(CVC4::kind::BITVECTOR_LSHR, f, f2); }
+  | SX_TOK LPAREN formula[f] COMMA INTEGER_LITERAL RPAREN
+    { unsigned k = AntlrInput::tokenToUnsigned($INTEGER_LITERAL);
+      f = MK_EXPR(MK_CONST(BitVectorSignExtend(k)), f); }
+  | BVZEROEXTEND_TOK LPAREN formula[f] COMMA INTEGER_LITERAL RPAREN
+    { unsigned k = AntlrInput::tokenToUnsigned($INTEGER_LITERAL);
+      f = MK_EXPR(MK_CONST(BitVectorSignExtend(k)), f); }
+  | BVREPEAT_TOK LPAREN formula[f] COMMA INTEGER_LITERAL RPAREN
+    { unsigned k = AntlrInput::tokenToUnsigned($INTEGER_LITERAL);
+      f = MK_EXPR(MK_CONST(BitVectorRepeat(k)), f); }
+  | BVROTR_TOK LPAREN formula[f] COMMA INTEGER_LITERAL RPAREN
+    { unsigned k = AntlrInput::tokenToUnsigned($INTEGER_LITERAL);
+      f = MK_EXPR(MK_CONST(BitVectorSignExtend(k)), f); }
+  | BVROTL_TOK LPAREN formula[f] COMMA INTEGER_LITERAL RPAREN
+    { unsigned k = AntlrInput::tokenToUnsigned($INTEGER_LITERAL);
+      f = MK_EXPR(MK_CONST(BitVectorRotateLeft(k)), f); }
+  | bvShiftTerm[f]
   ;
 
-/** Parses a plus/minus term (left-associative).
-    TODO: This won't take advantage of n-ary PLUS's. */
-plusTerm[CVC4::Expr& f]
+bvShiftTerm[CVC4::Expr& f]
 @init {
-  Expr e;
-  Kind op;
-  std::vector<Expr> exprs;
-  Debug("parser-extra") << "plus term: " << AntlrInput::tokenText(LT(1)) << std::endl;
-}
-  : multTerm[f]
-    ( ( PLUS_TOK { op = CVC4::kind::PLUS; }
-      | MINUS_TOK { op = CVC4::kind::MINUS; } )
-      multTerm[e]
-      { f = MK_EXPR(op, f, e); }
-    )*
+  std::vector<CVC4::Expr> expressions;
+  std::vector<unsigned> operators;
+  unsigned op;
+}
+  : bvComparison[f]
+    ( ( LEFTSHIFT_TOK | RIGHTSHIFT_TOK) INTEGER_LITERAL
+      { unsigned k = AntlrInput::tokenToUnsigned($INTEGER_LITERAL);
+        f = MK_EXPR(MK_CONST(BitVectorRotateLeft(k)), f); }
+    )?
   ;
 
-/** Parses a multiply/divide term (left-associative).
-    TODO: This won't take advantage of n-ary MULT's. */
-multTerm[CVC4::Expr& f]
+bvComparison[CVC4::Expr& f]
 @init {
-  Expr e;
-  Kind op;
-  Debug("parser-extra") << "multiplication term: " << AntlrInput::tokenText(LT(1)) << std::endl;
-}
-  : expTerm[f]
-    ( ( STAR_TOK { op = CVC4::kind::MULT; }
-      | DIV_TOK { op = CVC4::kind::DIVISION; } )
-      expTerm[e]
-      { f = MK_EXPR(op, f, e); }
-    )*
+  Expr f2;
+}
+  : /* BV comparison */
+    BVLT_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
+    { f = MK_EXPR(CVC4::kind::BITVECTOR_ULT, f, f2); }
+  | BVLE_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
+    { f = MK_EXPR(CVC4::kind::BITVECTOR_ULE, f, f2); }
+  | BVGT_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
+    { f = MK_EXPR(CVC4::kind::BITVECTOR_UGT, f, f2); }
+  | BVGE_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
+    { f = MK_EXPR(CVC4::kind::BITVECTOR_UGE, f, f2); }
+  | BVSLT_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
+    { f = MK_EXPR(CVC4::kind::BITVECTOR_SLT, f, f2); }
+  | BVSLE_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
+    { f = MK_EXPR(CVC4::kind::BITVECTOR_SLE, f, f2); }
+  | BVSGT_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
+    { f = MK_EXPR(CVC4::kind::BITVECTOR_SGT, f, f2); }
+  | BVSGE_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
+    { f = MK_EXPR(CVC4::kind::BITVECTOR_SGE, f, f2); }
+  /*
+  | IS_INTEGER_TOK LPAREN formula[f] RPAREN
+    { f = MK_EXPR(CVC4::kind::BITVECTOR_IS_INTEGER, f); }
+  */
+  | selectExtractTerm[f]
   ;
 
-/**
- * Parses an exponential term (left-associative).
- * NOTE that the exponent must be a nonnegative integer constant
- * (for now).
- */
-expTerm[CVC4::Expr& f]
+/** Parses an array select. */
+selectExtractTerm[CVC4::Expr& f]
 @init {
-  Expr e;
-  Debug("parser-extra") << "exponential term: " << AntlrInput::tokenText(LT(1)) << std::endl;
-}
-  : unaryTerm[f]
-    ( EXP_TOK INTEGER_LITERAL
-      { Integer n = AntlrInput::tokenToInteger($INTEGER_LITERAL);
-        if(n == 0) {
-          f = MK_CONST( Integer(1) );
-        } else if(n == 1) {
-          /* f remains the same */
-        } else {
-          std::vector<Expr> v;
-          for(Integer i = 0; i < n; i = i + 1) {
-            v.push_back(f);
+  Expr f2;
+  bool extract;
+}
+  : /* array select / bitvector extract */
+    simpleTerm[f]
+    ( { extract = false; }
+      LBRACKET formula[f2] ( COLON INTEGER_LITERAL { extract = true; } )? RBRACKET
+      { if(extract) {
+          if(f2.getKind() != kind::CONST_INTEGER) {
+            PARSER_STATE->parseError("bitvector extraction requires [INTEGER_LITERAL:INTEGER_LITERAL] range");
           }
-          f = MK_EXPR(CVC4::kind::MULT, v);
+          unsigned k1 = f2.getConst<Integer>().getLong();
+          unsigned k2 = AntlrInput::tokenToUnsigned($INTEGER_LITERAL);
+          f = MK_EXPR(MK_CONST(BitVectorExtract(k1, k2)), f);
+        } else {
+          f = MK_EXPR(CVC4::kind::SELECT, f, f2);
         }
       }
     )*
+
   ;
 
-/**
- * Parses a unary term.
- */
-unaryTerm[CVC4::Expr& f]
+/** Parses a simple term. */
+simpleTerm[CVC4::Expr& f]
 @init {
   std::string name;
   std::vector<Expr> args;
@@ -574,18 +1039,22 @@ unaryTerm[CVC4::Expr& f]
   | /* if-then-else */
     iteTerm[f]
 
-  | /* Unary minus */
-    MINUS_TOK unaryTerm[f] { f = MK_EXPR(CVC4::kind::UMINUS, f); }
-
   | /* parenthesized sub-formula */
     LPAREN formula[f] RPAREN
 
     /* constants */
   | TRUE_TOK  { f = MK_CONST(true); }
   | FALSE_TOK { f = MK_CONST(false); }
-
   | INTEGER_LITERAL { f = MK_CONST( AntlrInput::tokenToInteger($INTEGER_LITERAL) ); }
   | DECIMAL_LITERAL { f = MK_CONST( AntlrInput::tokenToRational($DECIMAL_LITERAL) ); }
+  | HEX_LITERAL
+    { Assert( AntlrInput::tokenText($HEX_LITERAL).find("0hex") == 0 );
+      std::string hexString = AntlrInput::tokenTextSubstr($HEX_LITERAL, 4);
+      f = MK_CONST( BitVector(hexString, 16) ); }
+  | BINARY_LITERAL
+    { Assert( AntlrInput::tokenText($BINARY_LITERAL).find("0bin") == 0 );
+      std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 4);
+      f = MK_CONST( BitVector(binString, 2) ); }
 
   | /* variable */
     identifier[name,CHECK_DECLARED,SYM_VARIABLE]
@@ -653,7 +1122,7 @@ datatypeDef[std::vector<CVC4::Datatype>& datatypes]
   : identifier[id,CHECK_UNDECLARED,SYM_SORT]
     { datatypes.push_back(Datatype(id)); }
     EQUAL_TOK constructorDef[datatypes.back()]
-    ( BAR_TOK constructorDef[datatypes.back()] )*
+    ( BAR constructorDef[datatypes.back()] )*
   ;
 
 /**
@@ -689,7 +1158,13 @@ selector[CVC4::Datatype::Constructor& ctor]
   std::string id;
   Type type;
 }
-  : identifier[id,CHECK_UNDECLARED,SYM_SORT] COLON maybeUndefinedBaseType[type,CHECK_NONE]
+  : identifier[id,CHECK_UNDECLARED,SYM_SORT] COLON
+    maybeUndefinedBaseType[type,CHECK_NONE]
+    // TODO: this doesn't permit datatype fields of ARRAY or BITVECTOR
+    // type.  This will be problematic, since, after all, you could
+    // have something nasty like this:
+    //
+    //   DATATYPE list = cons(car:ARRAY list OF list, cdr:list) | nil END;
     { if(type.isNull()) {
         ctor.addArg(id, Datatype::UnresolvedType($maybeUndefinedBaseType.id));
       } else {
@@ -699,70 +1174,6 @@ selector[CVC4::Datatype::Constructor& ctor]
     }
   ;
 
-// Keywords
-
-AND_TOK : 'AND';
-ASSERT_TOK : 'ASSERT';
-BOOLEAN_TOK : 'BOOLEAN';
-CHECKSAT_TOK : 'CHECKSAT';
-ECHO_TOK : 'ECHO';
-ELSEIF_TOK : 'ELSIF';
-ELSE_TOK : 'ELSE';
-ENDIF_TOK : 'ENDIF';
-FALSE_TOK : 'FALSE';
-IF_TOK : 'IF';
-IN_TOK : 'IN';
-INT_TOK : 'INT';
-LET_TOK : 'LET';
-NOT_TOK : 'NOT';
-OPTION_TOK : 'OPTION';
-OR_TOK : 'OR';
-POPTO_TOK : 'POPTO';
-POP_TOK : 'POP';
-PRINT_TOK : 'PRINT';
-PUSH_TOK : 'PUSH';
-QUERY_TOK : 'QUERY';
-REAL_TOK : 'REAL';
-THEN_TOK : 'THEN';
-TRUE_TOK : 'TRUE';
-TYPE_TOK : 'TYPE';
-XOR_TOK : 'XOR';
-
-DATATYPE_TOK : 'DATATYPE';
-END_TOK : 'END';
-BAR_TOK : '|';
-
-ARRAY_TOK : 'ARRAY';
-OF_TOK : 'OF';
-WITH_TOK : 'WITH';
-
-BITVECTOR_TOK : 'BITVECTOR';
-
-// Symbols
-
-COLON : ':';
-COMMA : ',';
-LPAREN : '(';
-RPAREN : ')';
-SEMICOLON : ';';
-
-// Operators
-
-ARROW_TOK : '->';
-DIV_TOK : '/';
-EQUAL_TOK : '=';
-DISEQUAL_TOK : '/=';
-EXP_TOK : '^';
-GT_TOK : '>';
-GEQ_TOK : '>=';
-IFF_TOK : '<=>';
-IMPLIES_TOK : '=>';
-LT_TOK : '<';
-LEQ_TOK : '<=';
-MINUS_TOK : '-';
-PLUS_TOK : '+';
-STAR_TOK : '*';
-
 /**
  * Matches an identifier from the input. An identifier is a sequence of letters,
  * digits and "_", "'", "." symbols, starting with a letter.
@@ -780,6 +1191,20 @@ INTEGER_LITERAL: DIGIT+;
 DECIMAL_LITERAL: DIGIT+ '.' DIGIT+;
 
 /**
+ * Matches a hexadecimal constant.
+ */
+HEX_LITERAL
+  : '0hex' HEX_DIGIT+
+  ;
+
+/**
+ * Matches a binary constant.
+ */
+BINARY_LITERAL
+  : '0bin' ('0' | '1')+
+  ;
+
+/**
  * Matches a double quoted string literal. Escaping is supported, and
  * escape character '\' has to be escaped.
  */
@@ -795,6 +1220,8 @@ fragment ALPHA : 'a'..'z' | 'A'..'Z';
  */
 fragment DIGIT : '0'..'9';
 
+fragment HEX_DIGIT : DIGIT | 'a'..'f' | 'A'..'F';
+
 /**
  * Matches and skips whitespace in the input and ignores it.
  */
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index a5a633e48..d27abc735 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -448,6 +448,7 @@ term[CVC4::Expr& expr]
     { Assert( AntlrInput::tokenText($BINARY_LITERAL).find("#b") == 0 );
       std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 2);
       expr = MK_CONST( BitVector(binString, 2) ); }
+
     // NOTE: Theory constants go here
   ;
 
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index a048bc3b2..c3253d05a 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -99,6 +99,39 @@ void CvcPrinter::toStream(std::ostream& out, TNode n,
       case kind::GEQ: out << ">="; break;
       case kind::IMPLIES: out << "=>"; break;
       case kind::IFF: out << "<=>"; break;
+
+        // names are slightly different than the kind
+      case kind::BITVECTOR_PLUS: out << "BVPLUS"; break;
+      case kind::BITVECTOR_SUB: out << "BVSUB"; break;
+      case kind::BITVECTOR_XOR: out << "BVXOR"; break;
+      case kind::BITVECTOR_NAND: out << "BVNAND"; break;
+      case kind::BITVECTOR_NOR: out << "BVNOR"; break;
+      case kind::BITVECTOR_XNOR: out << "BVXNOR"; break;
+      case kind::BITVECTOR_COMP: out << "BVCOMP"; break;
+      case kind::BITVECTOR_MULT: out << "BVMULT"; break;
+      case kind::BITVECTOR_UDIV: out << "BVUDIV"; break;
+      case kind::BITVECTOR_UREM: out << "BVUREM"; break;
+      case kind::BITVECTOR_SDIV: out << "BVSDIV"; break;
+      case kind::BITVECTOR_SREM: out << "BVSREM"; break;
+      case kind::BITVECTOR_SMOD: out << "BVSMOD"; break;
+      case kind::BITVECTOR_SHL: out << "BVSHL"; break;
+      case kind::BITVECTOR_LSHR: out << "BVLSHR"; break;
+      case kind::BITVECTOR_ASHR: out << "BVASHR"; break;
+      case kind::BITVECTOR_ULT: out << "BVLT"; break;
+      case kind::BITVECTOR_ULE: out << "BVLE"; break;
+      case kind::BITVECTOR_UGT: out << "BVGT"; break;
+      case kind::BITVECTOR_UGE: out << "BVGE"; break;
+      case kind::BITVECTOR_SLT: out << "BVSLT"; break;
+      case kind::BITVECTOR_SLE: out << "BVSLE"; break;
+      case kind::BITVECTOR_SGT: out << "BVSGT"; break;
+      case kind::BITVECTOR_SGE: out << "BVSGE"; break;
+      case kind::BITVECTOR_NEG: out << "BVUMINUS"; break;
+
+      case kind::BITVECTOR_NOT: out << "~"; break;
+      case kind::BITVECTOR_AND: out << "&"; break;
+      case kind::BITVECTOR_OR: out << "|"; break;
+      case kind::BITVECTOR_CONCAT: out << "@"; break;
+
       default:
         out << k;
       }
@@ -159,6 +192,38 @@ void CvcPrinter::toStream(std::ostream& out, TNode n,
       out << "IF " << n[0] << " THEN " << n[1] << " ELSE " << n[2];
       break;
 
+    // these are prefix
+    case kind::BITVECTOR_PLUS:
+    case kind::BITVECTOR_SUB:
+    case kind::BITVECTOR_XOR:
+    case kind::BITVECTOR_NAND:
+    case kind::BITVECTOR_NOR:
+    case kind::BITVECTOR_XNOR:
+    case kind::BITVECTOR_COMP:
+    case kind::BITVECTOR_MULT:
+    case kind::BITVECTOR_UDIV:
+    case kind::BITVECTOR_UREM:
+    case kind::BITVECTOR_SDIV:
+    case kind::BITVECTOR_SREM:
+    case kind::BITVECTOR_SMOD:
+    case kind::BITVECTOR_SHL:
+    case kind::BITVECTOR_LSHR:
+    case kind::BITVECTOR_ASHR:
+    case kind::BITVECTOR_ULT:
+    case kind::BITVECTOR_ULE:
+    case kind::BITVECTOR_UGT:
+    case kind::BITVECTOR_UGE:
+    case kind::BITVECTOR_SLT:
+    case kind::BITVECTOR_SLE:
+    case kind::BITVECTOR_SGT:
+    case kind::BITVECTOR_SGE:
+      out << n.getOperator() << '(' << n[0] << ',' << n[1] << ')';
+      break;
+
+    case kind::BITVECTOR_EXTRACT:
+      out << n[0] << '[' << n.getOperator().getConst<BitVectorExtract>() << ']';
+      break;
+
     default:
       if(k == kind::NOT && n[0].getKind() == kind::EQUAL) {
         // collapse NOT-over-EQUAL
diff --git a/test/regress/regress0/precedence/or-xor.cvc b/test/regress/regress0/precedence/or-xor.cvc
index 4e19be584..3252647a2 100644
--- a/test/regress/regress0/precedence/or-xor.cvc
+++ b/test/regress/regress0/precedence/or-xor.cvc
@@ -3,5 +3,6 @@
 
 A, B, C: BOOLEAN;
 
-QUERY (A OR B XOR C) <=> (A OR (B XOR C));
+QUERY ((A OR B XOR C) <=> ((A OR B) XOR C))
+  AND ((A XOR B OR C) <=> ((A XOR B) OR C));
 % EXIT: 20
diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h
index af9b7bd0f..dbc8e2281 100644
--- a/test/unit/parser/parser_black.h
+++ b/test/unit/parser/parser_black.h
@@ -2,10 +2,10 @@
 /*! \file parser_black.h
  ** \verbatim
  ** Original author: cconway
- ** Major contributors: none
- ** Minor contributors (to current version): mdeters
+ ** Major contributors: mdeters
+ ** 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
@@ -206,7 +206,12 @@ public:
     tryGoodInput("a, b : BOOLEAN;");
     tryGoodInput("a, b : BOOLEAN; QUERY (a => b) AND a => b;");
     tryGoodInput("T, U : TYPE; f : T -> U; x : T; y : U; CHECKSAT f(x) = y;");
+    tryGoodInput("T : TYPE = BOOLEAN; x : T; CHECKSAT x;");
+    tryGoodInput("a : ARRAY INT OF REAL; ASSERT (a WITH [1] := 0.0)[1] = a[0];");
+    tryGoodInput("b : BITVECTOR(3); ASSERT b = 0bin101;");
+    tryGoodInput("T : TYPE = BOOLEAN; x : T; CHECKSAT x;");
     tryGoodInput("T : TYPE; x, y : T; a : BOOLEAN; QUERY (IF a THEN x ELSE y ENDIF) = x;");
+    tryGoodInput("CHECKSAT 0bin0000 /= 0hex7;");
     tryGoodInput("%% nothing but a comment");
     tryGoodInput("% a comment\nASSERT TRUE; %a command\n% another comment");
   }
@@ -219,6 +224,7 @@ public:
     tryBadInput("a, b : boolean;"); // lowercase boolean isn't a type
     tryBadInput("0x : INT;"); // 0x isn't an identifier
     tryBadInput("a, b : BOOLEAN\nQUERY (a => b) AND a => b;"); // no semicolon after decl
+    tryBadInput("ASSERT 0bin012 /= 0hex0;"); // bad binary literal
     tryBadInput("a : BOOLEAN; a: BOOLEAN;"); // double decl
     tryBadInput("a, b: BOOLEAN; QUERY a(b);"); // non-function used as function
   }
diff --git a/test/unit/util/datatype_black.h b/test/unit/util/datatype_black.h
index d0de68e33..991d71364 100644
--- a/test/unit/util/datatype_black.h
+++ b/test/unit/util/datatype_black.h
@@ -54,6 +54,10 @@ public:
     cout << nat << std::endl;
     DatatypeType natType = d_em->mkDatatypeType(nat);
     cout << natType << std::endl;
+
+    Expr ctor = natType.getDatatype()[1].getConstructor();
+    Expr apply = d_em->mkExpr(kind::APPLY_CONSTRUCTOR, ctor);
+    cout << apply << std::endl;
   }
 
   void testTree() {