mostly CVC presentation language parsing and printing

1 files changed, 654 insertions, 227 deletions

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.
  */