more work on CVC language

3 files changed, 47 insertions, 21 deletions

diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index bcc96637f..48cf4ea93 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -155,9 +155,7 @@ void QueryCommand::printResult(std::ostream& out) const {
 }
 
 void QueryCommand::toStream(std::ostream& out) const {
-  out << "Query(";
-  d_expr.printAst(out, 0);
-  out << ")";
+  out << "Query(" << d_expr << ')';
 }
 
 /* class CommandSequence */
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 96a8346b0..30866eddb 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -597,7 +597,7 @@ arrayType[CVC4::Type& t]
   Type t2;
 }
   : baseType[t]
-  | ARRAY_TOK baseType[t] OF_TOK baseType[t2]
+  | ARRAY_TOK bitvectorType[t] OF_TOK bitvectorType[t2]
     { t = EXPR_MANAGER->mkArrayType(t, t2); }
   ;
 
@@ -927,10 +927,14 @@ bvUminusTerm[CVC4::Expr& f]
     { 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); }
+      unsigned n = BitVectorType(f.getType()).getSize();
+      // sign extension in TheoryBitVector is defined as in SMT-LIBv2
+      f = MK_EXPR(MK_CONST(BitVectorSignExtend(k - n)), f); }
   | BVZEROEXTEND_TOK LPAREN formula[f] COMMA INTEGER_LITERAL RPAREN
     { unsigned k = AntlrInput::tokenToUnsigned($INTEGER_LITERAL);
-      f = MK_EXPR(MK_CONST(BitVectorSignExtend(k)), f); }
+      unsigned n = BitVectorType(f.getType()).getSize();
+      // also zero extension
+      f = MK_EXPR(MK_CONST(BitVectorZeroExtend(k - n)), f); }
   | BVREPEAT_TOK LPAREN formula[f] COMMA INTEGER_LITERAL RPAREN
     { unsigned k = AntlrInput::tokenToUnsigned($INTEGER_LITERAL);
       f = MK_EXPR(MK_CONST(BitVectorRepeat(k)), f); }
@@ -945,14 +949,19 @@ bvUminusTerm[CVC4::Expr& f]
 
 bvShiftTerm[CVC4::Expr& f]
 @init {
-  std::vector<CVC4::Expr> expressions;
-  std::vector<unsigned> operators;
-  unsigned op;
+  bool left = false;
 }
   : bvComparison[f]
-    ( ( LEFTSHIFT_TOK | RIGHTSHIFT_TOK) INTEGER_LITERAL
+    ( (LEFTSHIFT_TOK { left = true; } | RIGHTSHIFT_TOK) INTEGER_LITERAL
       { unsigned k = AntlrInput::tokenToUnsigned($INTEGER_LITERAL);
-        f = MK_EXPR(MK_CONST(BitVectorRotateLeft(k)), f); }
+        if(left) {
+          f = MK_EXPR(kind::BITVECTOR_CONCAT, f, MK_CONST(BitVector(k)));
+        } else {
+          unsigned n = BitVectorType(f.getType()).getSize();
+          f = MK_EXPR(kind::BITVECTOR_CONCAT, MK_CONST(BitVector(k)),
+                      MK_EXPR(MK_CONST(BitVectorExtract(n - 1, k)), f));
+        }
+      }
     )?
   ;
 
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index c3253d05a..97f434e9b 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -144,13 +144,36 @@ void CvcPrinter::toStream(std::ostream& out, TNode n,
 
     return;
   } else if(n.getMetaKind() == kind::metakind::PARAMETERIZED) {
-    out << n.getOperator();
-    if(n.getNumChildren() > 0) {
-      out << '(';
-      if(n.getNumChildren() > 1) {
-        copy(n.begin(), n.end() - 1, ostream_iterator<TNode>(out, ", "));
+    switch(n.getKind()) {
+    case kind::BITVECTOR_EXTRACT:
+      out << n[0] << n.getOperator().getConst<BitVectorExtract>();
+      break;
+    case kind::BITVECTOR_REPEAT:
+      out << "BVREPEAT(" << n[0] << "," << n.getOperator() << ')';
+      break;
+    case kind::BITVECTOR_ZERO_EXTEND:
+      out << "BVZEROEXTEND(" << n[0] << "," << n.getOperator() << ')';
+      break;
+    case kind::BITVECTOR_SIGN_EXTEND:
+      out << "SX(" << n[0] << "," << n.getOperator() << ')';
+      break;
+    case kind::BITVECTOR_ROTATE_LEFT:
+      out << "BVROTL(" << n[0] << "," << n.getOperator() << ')';
+      break;
+    case kind::BITVECTOR_ROTATE_RIGHT:
+      out << "BVROTR(" << n[0] << "," << n.getOperator() << ')';
+      break;
+
+
+    default:
+      out << n.getOperator();
+      if(n.getNumChildren() > 0) {
+        out << '(';
+        if(n.getNumChildren() > 1) {
+          copy(n.begin(), n.end() - 1, ostream_iterator<TNode>(out, ", "));
+        }
+        out << n[n.getNumChildren() - 1] << ')';
       }
-      out << n[n.getNumChildren() - 1] << ')';
     }
     return;
   } else if(n.getMetaKind() == kind::metakind::OPERATOR) {
@@ -220,10 +243,6 @@ void CvcPrinter::toStream(std::ostream& out, TNode n,
       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