smt parser for bit-vectors

7 files changed, 219 insertions, 16 deletions

diff --git a/src/expr/builtin_kinds b/src/expr/builtin_kinds
index 1c24b045c..5ce38f5fd 100644
--- a/src/expr/builtin_kinds
+++ b/src/expr/builtin_kinds
@@ -130,8 +130,8 @@ operator FUNCTION_TYPE 2: "function type"
 variable SORT_TYPE "sort type"
 
 constant BITVECTOR_TYPE \
-	unsigned \
-	::CVC4::UnsignedHashStrategy \
+	::CVC4::BitVectorSize \
+	"::CVC4::UnsignedHashStrategy< ::CVC4::BitVectorSize >" \
 	"util/bitvector.h" \
 	"bit-vector type" 
 	
\ No newline at end of file
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 8243bd6da..5cb19bc89 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -634,7 +634,7 @@ inline TypeNode NodeManager::kindType() {
 }
 
 inline TypeNode NodeManager::bitVectorType(unsigned size) {
-  return TypeNode(mkTypeConst<unsigned>(kind::BITVECTOR_TYPE));
+  return TypeNode(mkTypeConst<BitVectorSize>(BitVectorSize(size)));
 }
 
 /** Make a function type from domain to range. */
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index b935c837e..da16000ce 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -74,13 +74,13 @@ bool TypeNode::isBitVector() const {
 
 /** Is this a bit-vector type of size <code>size</code> */
 bool TypeNode::isBitVector(unsigned size) const {
-  return getKind() == kind::BITVECTOR_TYPE && getConst<unsigned>() == size;
+  return getKind() == kind::BITVECTOR_TYPE && getConst<BitVectorSize>() == size;
 }
 
 /** Get the size of this bit-vector type */
 unsigned TypeNode::getBitVectorSize() const {
   Assert(isBitVector());
-  return getConst<unsigned>();
+  return getConst<BitVectorSize>();
 }
 
 
diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h
index 1d6f5f790..441d2a0b3 100644
--- a/src/parser/antlr_input.h
+++ b/src/parser/antlr_input.h
@@ -134,6 +134,8 @@ public:
 
   /** Retrieve the text associated with a token. */
   inline static std::string tokenText(pANTLR3_COMMON_TOKEN token);
+  /** Retrieve an unsigned from the text of a token */
+  inline static unsigned tokenToUnsigned( pANTLR3_COMMON_TOKEN token );
   /** Retrieve an Integer from the text of a token */
   inline static Integer tokenToInteger( pANTLR3_COMMON_TOKEN token );
   /** Retrieve a Rational from the text of a token */
@@ -180,6 +182,15 @@ std::string AntlrInput::tokenText(pANTLR3_COMMON_TOKEN token) {
   return txt;
 }
 
+unsigned AntlrInput::tokenToUnsigned(pANTLR3_COMMON_TOKEN token) {
+  unsigned result;
+  std::stringstream ss;
+  ss << tokenText(token);
+  ss >> result;
+  return result;
+}
+
+
 Integer AntlrInput::tokenToInteger(pANTLR3_COMMON_TOKEN token) {
   Integer i( tokenText(token) );
   return i;
diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g
index bc2ecb661..dde5d26eb 100644
--- a/src/parser/smt/Smt.g
+++ b/src/parser/smt/Smt.g
@@ -94,7 +94,8 @@ setLogic(Parser *parser, const std::string& name) {
     parser->mkSort("U");
   } else if(name == "QF_LRA"){
     parser->defineType("Real", parser->getExprManager()->realType());
-  } else{
+  } else if(name == "QF_BV"){
+  } else {
     // NOTE: Theory types go here
     Unhandled(name);
   }
@@ -270,6 +271,7 @@ builtinOp[CVC4::Kind& kind]
   | IFF_TOK      { $kind = CVC4::kind::IFF;     }
   | EQUAL_TOK    { $kind = CVC4::kind::EQUAL;   }
   | DISTINCT_TOK { $kind = CVC4::kind::DISTINCT; }
+    // NOTE: Theory operators go here
   | GREATER_THAN_TOK
                  { $kind = CVC4::kind::GT; }
   | GREATER_THAN_TOK EQUAL_TOK
@@ -283,7 +285,35 @@ builtinOp[CVC4::Kind& kind]
   | TILDE_TOK    { $kind = CVC4::kind::UMINUS; }
   | MINUS_TOK    { $kind = CVC4::kind::MINUS; }
   // Bit-vectors
-    // NOTE: Theory operators go here
+  | CONCAT_TOK   { $kind = CVC4::kind::BITVECTOR_CONCAT; }
+  | BVAND_TOK    { $kind = CVC4::kind::BITVECTOR_AND;    } 
+  | BVOR_TOK     { $kind = CVC4::kind::BITVECTOR_OR;     }   
+  | BVXOR_TOK    { $kind = CVC4::kind::BITVECTOR_XOR;    }
+  | BVNOT_TOK    { $kind = CVC4::kind::BITVECTOR_NOT;    }
+  | BVNAND_TOK   { $kind = CVC4::kind::BITVECTOR_NAND;   }
+  | BVNOR_TOK    { $kind = CVC4::kind::BITVECTOR_NOR;    }
+  | BVXNOR_TOK   { $kind = CVC4::kind::BITVECTOR_XNOR;   }
+  | BVCOMP_TOK   { $kind = CVC4::kind::BITVECTOR_COMP;   }
+  | BVMUL_TOK    { $kind = CVC4::kind::BITVECTOR_MULT;   }
+  | BVADD_TOK    { $kind = CVC4::kind::BITVECTOR_PLUS;   }
+  | BVSUB_TOK    { $kind = CVC4::kind::BITVECTOR_SUB;    }
+  | BVNEG_TOK    { $kind = CVC4::kind::BITVECTOR_NEG;    }
+  | BVUDIV_TOK   { $kind = CVC4::kind::BITVECTOR_UDIV;   }
+  | BVUREM_TOK   { $kind = CVC4::kind::BITVECTOR_UREM;   }
+  | BVSDIV_TOK   { $kind = CVC4::kind::BITVECTOR_SDIV;   } 
+  | BVSREM_TOK   { $kind = CVC4::kind::BITVECTOR_SREM;   }
+  | BVSMOD_TOK   { $kind = CVC4::kind::BITVECTOR_SMOD;   }
+  | BVSHL_TOK    { $kind = CVC4::kind::BITVECTOR_SHL;    }
+  | BVLSHR_TOK   { $kind = CVC4::kind::BITVECTOR_LSHR;   }
+  | BVASHR_TOK   { $kind = CVC4::kind::BITVECTOR_ASHR;   }
+  | BVULT_TOK    { $kind = CVC4::kind::BITVECTOR_ULT;    }
+  | BVULE_TOK    { $kind = CVC4::kind::BITVECTOR_ULE;    }
+  | BVUGT_TOK    { $kind = CVC4::kind::BITVECTOR_UGT;    }
+  | BVUGE_TOK    { $kind = CVC4::kind::BITVECTOR_UGE;    }
+  | BVSLT_TOK    { $kind = CVC4::kind::BITVECTOR_SLT;    }
+  | BVSLE_TOK    { $kind = CVC4::kind::BITVECTOR_SLE;    }
+  | BVSGT_TOK    { $kind = CVC4::kind::BITVECTOR_SGT;    }
+  | BVSGE_TOK    { $kind = CVC4::kind::BITVECTOR_SGE;    }
     /* TODO: lt, gt, plus, minus, etc. */
   ;
 
@@ -292,6 +322,25 @@ builtinOp[CVC4::Kind& kind]
  */
 parameterizedOperator[CVC4::Expr& op] 
   : functionSymbol[op]
+  | bitVectorOperator[op]
+  ;
+
+/**
+ * Matches a bit-vector operator (the ones parametrized by numbers)
+ */
+bitVectorOperator[CVC4::Expr& op]
+  : EXTRACT_TOK '[' n1 = NUMERAL_TOK ':' n2 = NUMERAL_TOK ']'
+    { op = MK_CONST(BitVectorExtract(AntlrInput::tokenToUnsigned($n1), AntlrInput::tokenToUnsigned($n2))); }
+  | REPEAT_TOK '[' n = NUMERAL_TOK ']' 
+    { op = MK_CONST(BitVectorRepeat(AntlrInput::tokenToUnsigned($n))); }
+  | ZERO_EXTEND_TOK '[' n = NUMERAL_TOK ']'
+    { op = MK_CONST(BitVectorZeroExtend(AntlrInput::tokenToUnsigned($n))); }
+  | SIGN_EXTEND_TOK '[' n = NUMERAL_TOK ']'
+    { op = MK_CONST(BitVectorSignExtend(AntlrInput::tokenToUnsigned($n))); }
+  | ROTATE_LEFT_TOK '[' n = NUMERAL_TOK ']'
+    { op = MK_CONST(BitVectorRotateLeft(AntlrInput::tokenToUnsigned($n))); }
+  | ROTATE_RIGHT_TOK '[' n = NUMERAL_TOK ']'
+    { op = MK_CONST(BitVectorRotateRight(AntlrInput::tokenToUnsigned($n))); }  
   ;
 
 /**
@@ -319,7 +368,7 @@ functionSymbol[CVC4::Expr& fun]
 }
   : functionName[name,CHECK_DECLARED]
     { PARSER_STATE->checkFunction(name);
-      fun = PARSER_STATE->getVariable(name); }
+      fun = PARSER_STATE->getVariable(name); }  
   ;
   
 /**
@@ -394,6 +443,9 @@ sortSymbol returns [CVC4::Type t]
 }
   : sortName[name,CHECK_NONE] 
   	{ $t = PARSER_STATE->getSort(name); }
+  | BITVECTOR_TOK '[' NUMERAL_TOK ']' {
+  	$t = EXPR_MANAGER->bitVectorType(AntlrInput::tokenToUnsigned($NUMERAL_TOK));
+  }
   ;
 
 /**
@@ -503,6 +555,43 @@ STAR_TOK          : '*';
 TILDE_TOK         : '~';
 XOR_TOK           : 'xor';
 
+// Bitvector tokens 
+BITVECTOR_TOK     : 'BitVec';
+CONCAT_TOK        : 'concat';
+EXTRACT_TOK       : 'extract';
+BVAND_TOK         : 'bvand';
+BVOR_TOK          : 'bvor';
+BVXOR_TOK         : 'bvxor';
+BVNOT_TOK         : 'bvnot';
+BVNAND_TOK        : 'bvnand';
+BVNOR_TOK         : 'bvnor';
+BVXNOR_TOK        : 'bvxnor';
+BVCOMP_TOK        : 'bvcomp';
+BVMUL_TOK         : 'bvmul';
+BVADD_TOK         : 'bvadd';
+BVSUB_TOK         : 'bvsub';
+BVNEG_TOK         : 'bvneg';
+BVUDIV_TOK        : 'bvudiv';
+BVUREM_TOK        : 'bvurem';
+BVSDIV_TOK        : 'bvsdiv';
+BVSREM_TOK        : 'bvsrem';
+BVSMOD_TOK        : 'bvsmod';
+BVSHL_TOK         : 'bvshl';
+BVLSHR_TOK        : 'bvlshr';
+BVASHR_TOK        : 'bvashr';
+BVULT_TOK         : 'bvult';
+BVULE_TOK         : 'bvule';
+BVUGT_TOK         : 'bvugt';
+BVUGE_TOK         : 'bvuge';
+BVSLT_TOK         : 'bvslt';
+BVSLE_TOK         : 'bvsle';
+BVSGT_TOK         : 'bvsgt';
+BVSGE_TOK         : 'bvsge';
+REPEAT_TOK        : 'repeat';
+ZERO_EXTEND_TOK   : 'zero_extend';
+SIGN_EXTEND_TOK   : 'sign_extend';
+ROTATE_LEFT_TOK   : 'rotate_left';
+ROTATE_RIGHT_TOK  : 'rotate_right';
 
 /**
  * Matches an identifier from the input. An identifier is a sequence of letters,
diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds
index aeb425474..ba8fc4efd 100644
--- a/src/theory/bv/kinds
+++ b/src/theory/bv/kinds
@@ -6,21 +6,81 @@
 
 theory ::CVC4::theory::bv::TheoryBV "theory_bv.h"
 
-constant CONST_BITVECTOR \
+constant BITVECTOR_CONST \
     ::CVC4::BitVector \
     ::CVC4::BitVectorHashStrategy \
     "util/bitvector.h" \
     "a fixed-width bit-vector constant"
     
 operator BITVECTOR_CONCAT 2 "bit-vector concatenation"
+operator BITVECTOR_AND 2 "bitwise and"
+operator BITVECTOR_OR 2 "bitwise or"      
+operator BITVECTOR_XOR 2 "bitwise xor"      
+operator BITVECTOR_NOT 2 "bitwise not"
+operator BITVECTOR_NAND 2 "bitwise nand"
+operator BITVECTOR_NOR 2 "bitwise nor"
+operator BITVECTOR_XNOR 2 "bitwise xnor"
+operator BITVECTOR_COMP 2 "equality comparison (returns one bit)"
+operator BITVECTOR_MULT 2 "bit-vector multiplication"
+operator BITVECTOR_PLUS 2 "bit-vector addition"
+operator BITVECTOR_SUB 2 "bit-vector subtraction"
+operator BITVECTOR_NEG 1 "bit-vector unary negation"
+operator BITVECTOR_UDIV 2 "bit-vector unsigned division, truncating towards 0 (undefined if divisor is 0)"    
+operator BITVECTOR_UREM 2 "bit-vector unsigned remainder from truncating division (undefined if divisor is 0)"    
+operator BITVECTOR_SDIV 2 "bit-vector 2's complement signed division"
+operator BITVECTOR_SREM 2 "bit-vector 2's complement signed remainder (sign follows dividend)"
+operator BITVECTOR_SMOD 2 "bit-vector 2's complement signed remainder (sign follows divisor)"
+operator BITVECTOR_SHL 2 "bit-vector left shift"
+operator BITVECTOR_LSHR 2 "bit-vector logical shift right"
+operator BITVECTOR_ASHR 2 "bit-vector arithmetic shift right"
+operator BITVECTOR_ULT 2 "bit-vector unsigned less than"
+operator BITVECTOR_ULE 2 "bit-vector unsigned less than or equal"
+operator BITVECTOR_UGT 2 "bit-vector unsigned greater than"
+operator BITVECTOR_UGE 2 "bit-vector unsigned greater than or equal"
+operator BITVECTOR_SLT 2 "bit-vector signed less than"
+operator BITVECTOR_SLE 2 "bit-vector signed less than or equal"
+operator BITVECTOR_SGT 2 "bit-vector signed greater than"
+operator BITVECTOR_SGE 2 "signed greater than or equal"
+
 constant BITVECTOR_EXTRACT_OP \
 	::CVC4::BitVectorExtract \
 	::CVC4::BitVectorExtractHashStrategy \
 	"util/bitvector.h" \
 	"operator for the bit-vector extract"
-	
-parameterized BITVECTOR_EXTRACT BITVECTOR_EXTRACT_OP 2 "disequality"
 
+constant BITVECTOR_REPEAT_OP \
+	::CVC4::BitVectorRepeat \
+	"::CVC4::UnsignedHashStrategy< ::CVC4::BitVectorRepeat >" \
+	"util/bitvector.h" \
+	"operator for the bit-vector repeat"
+
+constant BITVECTOR_ZERO_EXTEND_OP \
+	::CVC4::BitVectorZeroExtend \
+	"::CVC4::UnsignedHashStrategy< ::CVC4::BitVectorZeroExtend >" \
+	"util/bitvector.h" \
+	"operator for the bit-vector zero-extend"
+
+constant BITVECTOR_SIGN_EXTEND_OP \
+	::CVC4::BitVectorSignExtend \
+	"::CVC4::UnsignedHashStrategy< ::CVC4::BitVectorSignExtend >" \
+	"util/bitvector.h" \
+	"operator for the bit-vector sign-extend"
 
+constant BITVECTOR_ROTATE_LEFT_OP \
+	::CVC4::BitVectorRotateLeft \
+	"::CVC4::UnsignedHashStrategy< ::CVC4::BitVectorRotateLeft >" \
+	"util/bitvector.h" \
+	"operator for the bit-vector rotate left"
 
-    
\ No newline at end of file
+constant BITVECTOR_ROTATE_RIGHT_OP \
+	::CVC4::BitVectorRotateRight \
+	"::CVC4::UnsignedHashStrategy< ::CVC4::BitVectorRotateRight >" \
+	"util/bitvector.h" \
+	"operator for the bit-vector rotate right"
+	
+parameterized BITVECTOR_EXTRACT BITVECTOR_EXTRACT_OP 1 "bit-vector extract"
+parameterized BITVECTOR_REPEAT BITVECTOR_REPEAT_OP 1 "bit-vector repeat"
+parameterized BITVECTOR_ZERO_EXTEND BITVECTOR_ZERO_EXTEND_OP 1 "bit-vector zero-extend"
+parameterized BITVECTOR_SIGN_EXTEND BITVECTOR_SIGN_EXTEND_OP 1 "bit-vector sign-extend"
+parameterized BITVECTOR_ROTATE_LEFT BITVECTOR_ROTATE_LEFT_OP 1 "bit-vector rotate left"
+parameterized BITVECTOR_ROTATE_RIGHT BITVECTOR_ROTATE_RIGHT_OP 1 "bit-vector rotate right"
diff --git a/src/util/bitvector.h b/src/util/bitvector.h
index e1c0131d9..1ab13230b 100644
--- a/src/util/bitvector.h
+++ b/src/util/bitvector.h
@@ -105,6 +105,9 @@ struct BitVectorExtract  {
   /** The low bit of the range for this extract */
   unsigned low;
 
+  BitVectorExtract(unsigned high, unsigned low)
+  : high(high), low(low) {}
+
   bool operator == (const BitVectorExtract& extract) const {
     return high == extract.high && low == extract.low;
   }
@@ -122,11 +125,51 @@ public:
   }
 };
 
-/**
- * Hash function for the unsigned integers.
- */
+struct BitVectorSize {
+  unsigned size;
+  BitVectorSize(unsigned size)
+  : size(size) {}
+  operator unsigned () const { return size; }
+};
+
+struct BitVectorRepeat {
+  unsigned repeatAmount;
+  BitVectorRepeat(unsigned repeatAmount)
+  : repeatAmount(repeatAmount) {}
+  operator unsigned () const { return repeatAmount; }
+};
+
+struct BitVectorZeroExtend {
+  unsigned zeroExtendAmount;
+  BitVectorZeroExtend(unsigned zeroExtendAmount)
+  : zeroExtendAmount(zeroExtendAmount) {}
+  operator unsigned () const { return zeroExtendAmount; }
+};
+
+struct BitVectorSignExtend {
+  unsigned signExtendAmount;
+  BitVectorSignExtend(unsigned signExtendAmount)
+  : signExtendAmount(signExtendAmount) {}
+  operator unsigned () const { return signExtendAmount; }
+};
+
+struct BitVectorRotateLeft {
+  unsigned rotateLeftAmount;
+  BitVectorRotateLeft(unsigned rotateLeftAmount)
+  : rotateLeftAmount(rotateLeftAmount) {}
+  operator unsigned () const { return rotateLeftAmount; }
+};
+
+struct BitVectorRotateRight {
+  unsigned rotateRightAmount;
+  BitVectorRotateRight(unsigned rotateRightAmount)
+  : rotateRightAmount(rotateRightAmount) {}
+  operator unsigned () const { return rotateRightAmount; }
+};
+
+template <typename T>
 struct UnsignedHashStrategy {
-  static inline size_t hash(unsigned x) {
+  static inline size_t hash(const T& x) {
     return (size_t)x;
   }
 };