Fix parsing of BVROTR by CVC parser

This commit fixes Bugzilla bug 766 as proposed by jacobly.alt@gmail.com.

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index d443dc2bd6d040a955ed12ed5928a1d972478bb5..1b1137a9d6d7a0373106cfb47187df1c6db135ca 100644 (file)
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -1945,7 +1945,7 @@ bvTerm[CVC4::Expr& f]
     { f = MK_EXPR(MK_CONST(BitVectorRepeat(k)), f); }
     /* BV rotate right */
   | BVROTR_TOK LPAREN formula[f] COMMA k=numeral RPAREN
-    { f = MK_EXPR(MK_CONST(BitVectorSignExtend(k)), f); }
+    { f = MK_EXPR(MK_CONST(BitVectorRotateRight(k)), f); }
     /* BV rotate left */
   | BVROTL_TOK LPAREN formula[f] COMMA k=numeral RPAREN
     { f = MK_EXPR(MK_CONST(BitVectorRotateLeft(k)), f); }

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index a65a61dc761cd25070f04485a277188794aeea68..d202e78a32ad1e999995bd019d755b1ada364d87 100644 (file)
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -111,7 +111,13 @@ CVC_TESTS = \
        wiki.21.cvc \
        queries0.cvc \
        trim.cvc \
-       print_lambda.cvc 
+       print_lambda.cvc \
+       cvc3.userdoc.01.cvc \
+       cvc3.userdoc.02.cvc \
+       cvc3.userdoc.03.cvc \
+       cvc3.userdoc.04.cvc \
+       cvc3.userdoc.05.cvc \
+       cvc3.userdoc.06.cvc
 
 # Regression tests for TPTP inputs
 TPTP_TESTS =

diff --git a/test/regress/regress0/cvc3.userdoc.01.cvc b/test/regress/regress0/cvc3.userdoc.01.cvc
new file mode 100644 (file)
index 0000000..7c89de4
--- /dev/null
+++ b/test/regress/regress0/cvc3.userdoc.01.cvc
@@ -0,0 +1,31 @@
+% COMMAND-LINE: --incremental
+
+% EXPECT: valid
+QUERY 0bin0000111101010000  = 0hex0f50;
+
+% EXPECT: valid
+QUERY 0bin01@0bin0          = 0bin010;
+
+% EXPECT: valid
+QUERY 0bin0011[3:1]         = 0bin001;
+
+% EXPECT: valid
+QUERY 0bin0011 << 3         = 0bin0011000;
+
+% EXPECT: valid
+QUERY 0bin1000 >> 3         = 0bin0001;
+
+% EXPECT: valid
+QUERY SX(0bin100, 5)        = 0bin11100;
+
+% EXPECT: valid
+QUERY BVZEROEXTEND(0bin1,3) = 0bin0001;
+
+% EXPECT: valid
+QUERY BVREPEAT(0bin10,3)    = 0bin101010;
+
+% EXPECT: valid
+QUERY BVROTL(0bin101,1)     = 0bin011;
+
+% EXPECT: valid
+QUERY BVROTR(0bin101,1)     = 0bin110;

diff --git a/test/regress/regress0/cvc3.userdoc.02.cvc b/test/regress/regress0/cvc3.userdoc.02.cvc
new file mode 100644 (file)
index 0000000..b6329e9
--- /dev/null
+++ b/test/regress/regress0/cvc3.userdoc.02.cvc
@@ -0,0 +1,7 @@
+x : BITVECTOR(5);
+y : BITVECTOR(4);
+yy : BITVECTOR(3);
+
+% EXPECT: valid
+QUERY
+ BVPLUS(9, x@0bin0000, (0bin000@(~y)@0bin11))[8:4] = BVPLUS(5, x, ~(y[3:2])) ;

diff --git a/test/regress/regress0/cvc3.userdoc.03.cvc b/test/regress/regress0/cvc3.userdoc.03.cvc
new file mode 100644 (file)
index 0000000..4fc6a5f
--- /dev/null
+++ b/test/regress/regress0/cvc3.userdoc.03.cvc
@@ -0,0 +1,8 @@
+bv : BITVECTOR(10);
+a : BOOLEAN;
+
+% EXPECT: valid
+QUERY
+ 0bin01100000[5:3]=(0bin1111001@bv[0:0])[4:2]
+ AND
+ 0bin1@(IF a THEN 0bin0 ELSE 0bin1 ENDIF) = (IF a THEN 0bin110 ELSE 0bin011 ENDIF)[1:0] ;

diff --git a/test/regress/regress0/cvc3.userdoc.04.cvc b/test/regress/regress0/cvc3.userdoc.04.cvc
new file mode 100644 (file)
index 0000000..824690b
--- /dev/null
+++ b/test/regress/regress0/cvc3.userdoc.04.cvc
@@ -0,0 +1,9 @@
+x, y, z, t, q : BITVECTOR(1024);
+
+ASSERT x = ~x;
+ASSERT x&y&t&z&q = x;
+ASSERT x|y = t;
+ASSERT BVXOR(x,~x) = t;
+
+% EXPECT: valid
+QUERY  FALSE;

diff --git a/test/regress/regress0/cvc3.userdoc.05.cvc b/test/regress/regress0/cvc3.userdoc.05.cvc
new file mode 100644 (file)
index 0000000..37da96b
--- /dev/null
+++ b/test/regress/regress0/cvc3.userdoc.05.cvc
@@ -0,0 +1,14 @@
+x, y : BITVECTOR(4);
+
+ASSERT x = 0hex5;
+ASSERT y = 0bin0101;
+
+% EXPECT: valid
+QUERY
+ BVMULT(8,x,y)=BVMULT(8,y,x)
+ AND
+ NOT(BVLT(x,y))
+ AND
+ BVLE(BVSUB(8,x,y), BVPLUS(8, x, BVUMINUS(x)))
+ AND
+ x = BVSUB(4, BVUMINUS(x), BVPLUS(4, x,0hex1)) ;

diff --git a/test/regress/regress0/cvc3.userdoc.06.cvc b/test/regress/regress0/cvc3.userdoc.06.cvc
new file mode 100644 (file)
index 0000000..3801b6d
--- /dev/null
+++ b/test/regress/regress0/cvc3.userdoc.06.cvc
@@ -0,0 +1,13 @@
+% COMMAND-LINE: --incremental
+
+x, y : BITVECTOR(8);
+z, t : BITVECTOR(12);
+
+ASSERT x = 0hexff;
+ASSERT z = 0hexff0;
+
+% EXPECT: valid
+QUERY  z = x << 4;
+
+% EXPECT: valid
+QUERY (z >> 4)[7:0] = x;