more work on CVC language

diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index bcc96637faf9b7cd7ed2d3c2a3c58f1187f65944..48cf4ea938f3d1fb492504d8e2b906c9aaacf01e 100644 (file)
--- 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 96a8346b00cdbfce72db0289c5c90dd0b1303281..30866eddb9aa70a94818e5e20b8c396400cbe250 100644 (file)
--- 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 c3253d05a563f3c0929dcdd2dc509047c999dab8..97f434e9b98bbfd8bb5b7e11e5908f58269f520e 100644 (file)
--- 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

diff --git a/test/regress/regress0/bv/Makefile.am b/test/regress/regress0/bv/Makefile.am
index dd4246e1620588b6e0dd0195e1c070842ed95485..92db8d453b10284aba88cd7084ac5515e7726f33 100644 (file)
--- a/test/regress/regress0/bv/Makefile.am
+++ b/test/regress/regress0/bv/Makefile.am
@@ -14,12 +14,13 @@ SMT_TESTS =
 SMT2_TESTS = 
 
 # Regression tests for PL inputs
-CVC_TESTS = 
+CVC_TESTS = bvsimple.cvc
 
 # Regression tests derived from bug reports
 BUG_TESTS = 
 
 TESTS =        $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS)
 
-EXTRA_DIST = $(TESTS)
+EXTRA_DIST = $(TESTS) \
+       test00.smt
 

diff --git a/test/regress/regress0/bv/bvsimple.cvc b/test/regress/regress0/bv/bvsimple.cvc
new file mode 100644 (file)
index 0000000..f1cb8ff
--- /dev/null
+++ b/test/regress/regress0/bv/bvsimple.cvc
@@ -0,0 +1,21 @@
+% EXPECT: valid
+% EXIT: 20
+
+% Some tests from the CVC3 user manual.
+% http://www.cs.nyu.edu/acsys/cvc3/doc/user_doc.html
+
+QUERY
+( 0bin01@0bin0 = 0bin010 ) AND
+( 0bin1000 >> 3 = 0bin0001 ) AND
+( 0bin0011 << 3 = 0bin0011000 ) AND
+( 0bin1000 >> 3 = 0bin0001 ) AND
+
+TRUE
+
+% these not working yet..
+%( BVZEROEXTEND(0bin100, 5) = 0bin00100 ) AND
+%( SX(0bin100, 5) = 0bin11100 ) AND
+%
+%( BVZEROEXTEND(0bin100, 3) = 0bin100 ) AND
+%( SX(0bin100, 3) = 0bin100 )
+;