fixing the cvc bv parser and typechecker

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 40f35093f93885434c49f5114e098c367be1e0a2..7b1d1640af00c1d295380e3a3fee28e6807e8c1b 100644 (file)
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -549,6 +549,16 @@ using namespace CVC4::parser;
 #define MK_CONST EXPR_MANAGER->mkConst
 #define UNSUPPORTED PARSER_STATE->unimplementedFeature
 
+#define ENSURE_BV_SIZE(k, f)                                   \
+{                                                              \
+  unsigned size = BitVectorType(f.getType()).getSize();        \
+  if(k > size) {                                               \
+    f = MK_EXPR(MK_CONST(BitVectorZeroExtend(k - size)), f);   \
+  } else if (k < size) {                                       \
+    f = MK_EXPR(MK_CONST(BitVectorExtract(k - 1, 0)), f);      \
+  }                                                            \
+}                                            
+
 }/* @parser::postinclude */
 
 /**
@@ -1705,6 +1715,7 @@ postfixTerm[CVC4::Expr& f]
 bvTerm[CVC4::Expr& f]
 @init {
   Expr f2;
+  std::vector<Expr> args;
 }
     /* BV xor */
   : BVXOR_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
@@ -1722,43 +1733,36 @@ bvTerm[CVC4::Expr& f]
   | BVUMINUS_TOK LPAREN formula[f] RPAREN
     { f = MK_EXPR(CVC4::kind::BITVECTOR_NEG, f); }
     /* BV addition */
-  | BVPLUS_TOK LPAREN k=numeral COMMA formula[f]
-    ( COMMA formula[f2] { f = MK_EXPR(CVC4::kind::BITVECTOR_PLUS, f, f2); } )+ RPAREN
-    { unsigned size = BitVectorType(f.getType()).getSize();
-      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(k - 1, 0)), f);
+  | BVPLUS_TOK LPAREN k=numeral COMMA formula[f] { args.push_back(f); }
+    ( COMMA formula[f2] { args.push_back(f2); } )+ RPAREN 
+    {
+      if (k <= 0) {
+        PARSER_STATE->parseError("BVPLUS(k,_,_) must have k > 0");
+      }      
+      for (unsigned i = 0; i < args.size(); ++ i) {
+        ENSURE_BV_SIZE(k, args[i]);
       }
+      f = MK_EXPR(CVC4::kind::BITVECTOR_PLUS, args);
     }
     /* BV subtraction */
   | BVSUB_TOK LPAREN k=numeral COMMA formula[f] COMMA formula[f2] RPAREN
-    { f = MK_EXPR(CVC4::kind::BITVECTOR_SUB, f, f2);
-      if(k == 0) {
+    {       
+      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(k - 1, 0)), f);
-      }
+      }      
+      ENSURE_BV_SIZE(k, f);
+      ENSURE_BV_SIZE(k, f2);
+      f = MK_EXPR(CVC4::kind::BITVECTOR_SUB, f, f2);
     }
     /* BV multiplication */
   | BVMULT_TOK LPAREN k=numeral COMMA formula[f] COMMA formula[f2] RPAREN
-    { f = MK_EXPR(CVC4::kind::BITVECTOR_MULT, f, f2);
-      if(k == 0) {
+    { 
+      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(k - 1, 0)), f);
-      }
+      ENSURE_BV_SIZE(k, f);
+      ENSURE_BV_SIZE(k, f2);
+      f = MK_EXPR(CVC4::kind::BITVECTOR_MULT, f, f2);
     }
     /* BV unsigned division */
   | BVUDIV_TOK LPAREN formula[f] COMMA formula[f2] RPAREN

diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds
index 65500fe91d05a95bfb90f596e1c6f4f60367ea3f..9dc2e66bbacf81833b8342df28b0686f7a83a0ab 100644 (file)
--- a/src/theory/bv/kinds
+++ b/src/theory/bv/kinds
@@ -128,10 +128,10 @@ typerule BITVECTOR_XNOR ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
 
 typerule BITVECTOR_COMP ::CVC4::theory::bv::BitVectorCompRule
 
-typerule BITVECTOR_MULT ::CVC4::theory::bv::BitVectorArithRule
-typerule BITVECTOR_PLUS ::CVC4::theory::bv::BitVectorArithRule
-typerule BITVECTOR_SUB ::CVC4::theory::bv::BitVectorArithRule
-typerule BITVECTOR_NEG ::CVC4::theory::bv::BitVectorArithRule
+typerule BITVECTOR_MULT ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_PLUS ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_SUB ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_NEG ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
 
 typerule BITVECTOR_UDIV ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
 typerule BITVECTOR_UREM ::CVC4::theory::bv::BitVectorFixedWidthTypeRule

diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h
index 91b3a0e5da402da6e584226115c84827ecf023c2..8d8c31fa1e7d1bab87de50c9f054535aa5a76021 100644 (file)
--- a/src/theory/bv/theory_bv_type_rules.h
+++ b/src/theory/bv/theory_bv_type_rules.h
@@ -72,25 +72,6 @@ public:
   }
 };
 
-class BitVectorArithRule {
-public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate, AssertionException) {
-    unsigned maxWidth = 0;
-    TNode::iterator it = n.begin();
-    TNode::iterator it_end = n.end();
-    // TODO: optimize unary neg
-    for (; it != it_end; ++ it) {
-      TypeNode t = (*it).getType(check);
-      if (check && !t.isBitVector()) {
-        throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms");
-      }
-      maxWidth = std::max( maxWidth, t.getBitVectorSize() );
-    }
-    return nodeManager->mkBitVectorType(maxWidth);
-  }
-};
-
 class BitVectorFixedWidthTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)

diff --git a/test/regress/regress0/bv/Makefile.am b/test/regress/regress0/bv/Makefile.am
index 86b59ab04220a6865575f031a1893be55b901ae0..43702b6806768cb5eae6314b9f2293b6d90d5ca9 100644 (file)
--- a/test/regress/regress0/bv/Makefile.am
+++ b/test/regress/regress0/bv/Makefile.am
@@ -92,7 +92,7 @@ SMT_TESTS = \
 SMT2_TESTS =
 
 # Regression tests for PL inputs
-CVC_TESTS = bvsimple.cvc
+CVC_TESTS = bvsimple.cvc sizecheck.cvc
 
 # Regression tests derived from bug reports
 BUG_TESTS = \

diff --git a/test/regress/regress0/bv/sizecheck.cvc b/test/regress/regress0/bv/sizecheck.cvc
new file mode 100644 (file)
index 0000000..e9326d9
--- /dev/null
+++ b/test/regress/regress0/bv/sizecheck.cvc
@@ -0,0 +1,7 @@
+x : BITVECTOR(10);
+y : BITVECTOR(12);
+
+ASSERT (0bin0001000000000000 = BVPLUS(16, x, y));
+CHECKSAT;
+% EXPECT: sat
+% EXIT: 10