Adding bit-vector constants in SMT2

7 files changed, 166 insertions, 30 deletions

diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h
index f52467ad9..38fe1bce8 100644
--- a/src/parser/antlr_input.h
+++ b/src/parser/antlr_input.h
@@ -29,6 +29,7 @@
 #include "expr/expr.h"
 #include "expr/expr_manager.h"
 #include "util/Assert.h"
+#include "util/bitvector.h"
 #include "util/integer.h"
 #include "util/rational.h"
 
@@ -148,8 +149,6 @@ public:
   static Integer tokenToInteger( pANTLR3_COMMON_TOKEN token );
   /** Retrieve a Rational from the text of a token */
   static Rational tokenToRational(pANTLR3_COMMON_TOKEN token);
-  /** Retrive a Bitvector from the text of a token */
-//  static Bitvector tokenToBitvector(pANTLR3_COMMON_TOKEN token, int base);
 
 protected:
   /** Create an input. This input takes ownership of the given input stream,
@@ -201,8 +200,7 @@ inline unsigned AntlrInput::tokenToUnsigned(pANTLR3_COMMON_TOKEN token) {
 }
 
 inline Integer AntlrInput::tokenToInteger(pANTLR3_COMMON_TOKEN token) {
-  Integer i( tokenText(token) );
-  return i;
+  return Integer( tokenText(token) );
 }
 
 inline Rational AntlrInput::tokenToRational(pANTLR3_COMMON_TOKEN token) {
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 01cc99c3d..d788a2c3f 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -241,8 +241,9 @@ Expr Parser::nextExpression() throw(ParserException) {
   if(!done()) {
     try {
       result = d_input->parseExpr();
-      if(result.isNull())
+      if(result.isNull()) {
         setDone();
+      }
     } catch(ParserException& e) {
       setDone();
       throw;
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 19997cdd0..4f65fa5e7 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -259,6 +259,14 @@ term[CVC4::Expr& expr]
   | RATIONAL
     { // FIXME: This doesn't work because an SMT rational is not a valid GMP rational string
       expr = MK_CONST( AntlrInput::tokenToRational($RATIONAL) ); }
+  | HEX_LITERAL
+    { std::string hexString = AntlrInput::tokenText($HEX_LITERAL);
+      AlwaysAssert( hexString.find("#x") == 0 );
+      expr = MK_CONST( BitVector(hexString.erase(0,2), 16) ); }
+  | BINARY_LITERAL
+    { std::string binString = AntlrInput::tokenText($BINARY_LITERAL);
+      AlwaysAssert( binString.find("#b") == 0 );
+      expr = MK_CONST( BitVector(binString.erase(0,2), 2) ); }
     // NOTE: Theory constants go here
   ;
 
@@ -352,15 +360,6 @@ sortSymbol[CVC4::Type& t]
   ;
 
 /**
- * Matches the status of the benchmark, one of 'sat', 'unsat' or 'unknown'.
- */
-benchmarkStatus[ CVC4::BenchmarkStatus& status ]
-  : SAT_TOK       { $status = SMT_SATISFIABLE;    }
-  | UNSAT_TOK     { $status = SMT_UNSATISFIABLE;  }
-  | UNKNOWN_TOK   { $status = SMT_UNKNOWN;        }
-  ;
-
-/**
  * Matches an symbol and sets the string reference parameter id.
  * @param id string to hold the symbol
  * @param check what kinds of check to do on the symbol
@@ -459,17 +458,38 @@ WHITESPACE
   ;
 
 /**
- * Matches a numeral from the input (non-empty sequence of digits).
+ * Matches an integer constant from the input (non-empty sequence of digits).
+ * This is a bit looser than what the standard allows, because it accepts 
+ * leading zeroes. 
  */
 NUMERAL
   : DIGIT+
   ;
 
+/**
+  * Matches a rational constant from the input. This is a bit looser
+  * than what the standard allows, because it accepts leading zeroes. 
+  */
 RATIONAL
   : DIGIT+ '.' DIGIT+
   ;
 
 /**
+ * Matches a hexadecimal constant.
+ */
+ HEX_LITERAL
+  : '#x' HEX_DIGIT+
+  ;
+
+/**
+ * Matches a binary constant.
+ */
+ BINARY_LITERAL
+  : '#b' ('0' | '1')+
+  ;
+
+
+/**
  * Matches a double quoted string literal. Escaping is supported, and escape
  * character '\' has to be escaped.
  */
@@ -499,6 +519,8 @@ ALPHA
  */
 fragment DIGIT : '0'..'9';
 
+fragment HEX_DIGIT : DIGIT | 'a'..'f' | 'A'..'F';
+
 /** Matches the characters that may appear in a "symbol" (i.e., an identifier) 
  */
 fragment SYMBOL_CHAR 
diff --git a/src/util/bitvector.h b/src/util/bitvector.h
index 2d01189c5..4f6038a81 100644
--- a/src/util/bitvector.h
+++ b/src/util/bitvector.h
@@ -8,9 +8,12 @@
 #ifndef __CVC4__BITVECTOR_H_
 #define __CVC4__BITVECTOR_H_
 
-#include <string>
 #include <iostream>
+#include "util/Assert.h"
 #include "util/gmp_util.h"
+#include "util/integer.h"
+
+using namespace std;
 
 namespace CVC4 {
 
@@ -19,9 +22,9 @@ class BitVector {
 private:
 
   unsigned d_size;
-  mpz_class d_value;
+  Integer d_value;
 
-  BitVector(unsigned size, const mpz_class& val) : d_size(size), d_value(val) {}
+  BitVector(unsigned size, const Integer& val) : d_size(size), d_value(val) {}
 
 public:
 
@@ -37,8 +40,7 @@ public:
   BitVector(unsigned size, const BitVector& q)
   : d_size(size), d_value(q.d_value) {}
 
-  BitVector(const std::string& num, unsigned base = 2)
-  : d_size(1), d_value(0) {}
+  BitVector(const std::string& num, unsigned base = 2);
 
   ~BitVector() {}
 
@@ -80,11 +82,20 @@ public:
   }
 
   size_t hash() const {
-    return gmpz_hash(d_value.get_mpz_t());
+    return d_value.hash();
   }
 
   std::string toString(unsigned int base = 2) const {
-    return d_value.get_str(base);
+    std::string str = d_value.toString(base);
+    if( base == 2 && d_size > str.size() ) {
+      std::string zeroes;
+      for( unsigned int i=0; i < d_size - str.size(); ++i ) {
+        zeroes.append("0");
+      }
+      return zeroes + str;
+    } else {
+      return str;
+    }
   }
 
   unsigned getSize() const {
@@ -92,6 +103,38 @@ public:
   }
 };
 
+inline BitVector::BitVector(const std::string& num, unsigned base) {
+  AlwaysAssert( base == 2 || base == 16 );
+
+  if( base == 2 ) {
+    d_size = num.size();
+//    d_value = Integer(num,2);
+/*
+    for( string::const_iterator it = num.begin(); it != num.end(); ++it ) {
+      if( *it != '0' || *it != '1' ) {
+        IllegalArgument(num, "BitVector argument is not a binary string.");
+      }
+      z = (Integer(2) * z) + (*it == '1');
+      d_value = mpz_class(z.get_mpz());
+    }
+*/
+  } else if( base == 16 ) {
+    d_size = num.size() * 4;
+//    // Use a stream to decode the hex string
+//    stringstream ss;
+//    ss.setf(ios::hex, ios::basefield);
+//    ss << num;
+//    ss >> z;
+//    d_value = mpz_class(z);
+//    break;
+  } else {
+    Unreachable("Unsupported base in BitVector(std::string&, unsigned int).");
+  }
+
+  d_value = Integer(num,base);
+}
+
+
 /**
  * Hash function for the BitVector constants.
  */
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index 666d1c285..2ec5122f3 100644
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -21,6 +21,7 @@ UNIT_TESTS = \
 	theory/theory_black \
 	theory/theory_uf_white \
 	util/assert_white \
+	util/bitvector_black \
 	util/configuration_black \
 	util/output_black \
 	util/exception_black \
diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h
index da636353e..b4044b96f 100644
--- a/test/unit/parser/parser_black.h
+++ b/test/unit/parser/parser_black.h
@@ -174,7 +174,9 @@ const string goodSmt2Exprs[] = {
     "(ite a (f x) y)",
     "1",
     "0",
-    "1.5"
+    "1.5",
+    "#xfab09c7",
+    "#b0001011"
 };
 
 const int numGoodSmt2Exprs = sizeof(goodSmt2Exprs) / sizeof(string);
@@ -205,7 +207,11 @@ const string badSmt2Exprs[] = {
     "(if_then_else a (f x) y)", // no if_then_else in v2
     "(a b)", // using non-function as function
     ".5", // rational constants must have integer prefix
-    "1." // rational constants must have fractional suffix
+    "1.", // rational constants must have fractional suffix
+    "#x", // hex constants must have at least one digit
+    "#b", // ditto binary constants
+    "#xg0f",
+    "#b9"
 };
 
 const int numBadSmt2Exprs = sizeof(badSmt2Exprs) / sizeof(string);
@@ -271,7 +277,7 @@ class ParserBlack : public CxxTest::TestSuite {
       TS_ASSERT_THROWS
         ( while(parser.nextCommand());
           cout << "\nBad input succeeded:\n" << badInputs[i] << endl;,
-          ParserException );
+          const ParserException& );
 //      Debug.off("parser");
       delete input;
     }
@@ -299,13 +305,21 @@ class ParserBlack : public CxxTest::TestSuite {
         TS_ASSERT( e.isNull() );
         delete input;
       } catch (Exception& e) {
-        cout << "\nGood expr failed:\n" << goodBooleanExprs[i] << endl;
-        cout << e;
+        cout << endl
+             << "Good expr failed." << endl
+             << "Input: <<" << goodBooleanExprs[i] << ">>" << endl
+             << "Output: <<" << e << ">>" << endl;
         throw;
       }
     }
   }
 
+  /* NOTE: The check implemented here may fail if a bad expression expression string
+   * has a prefix that is parseable as a good expression. E.g., the bad SMT v2 expression
+   * "#b10@@@@@@" will actually return the bit-vector 10 and ignore the tail of the
+   * input. It's more trouble than it's worth to check that the whole input was
+   * consumed here, so just be careful to avoid valid prefixes in tests.
+   */
   void tryBadExprs(InputLanguage d_lang, const string badBooleanExprs[], int numExprs) {
     //Debug.on("parser");
     for(int i = 0; i < numExprs; ++i) {
@@ -318,9 +332,12 @@ class ParserBlack : public CxxTest::TestSuite {
       setupContext(parser);
       TS_ASSERT( !parser.done() );
       TS_ASSERT_THROWS
-        ( parser.nextExpression();
-          cout << "\nBad expr succeeded: " << badBooleanExprs[i] << endl;,
-          ParserException );
+        ( Expr e = parser.nextExpression();
+          cout << endl
+               << "Bad expr succeeded." << endl
+               << "Input: <<" << badBooleanExprs[i] << ">>" << endl
+               << "Output: <<" << e << ">>" << endl;,
+          const ParserException& );
       delete input;
     }
     //Debug.off("parser");
diff --git a/test/unit/util/bitvector_black.h b/test/unit/util/bitvector_black.h
new file mode 100644
index 000000000..f35107af0
--- /dev/null
+++ b/test/unit/util/bitvector_black.h
@@ -0,0 +1,54 @@
+/*********************                                                        */
+/** integer_black.h
+ ** Original author: taking
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** Black box testing of CVC4::Integer.
+ **/
+
+#include <cxxtest/TestSuite.h>
+#include <sstream>
+
+#include "util/bitvector.h"
+
+using namespace CVC4;
+using namespace std;
+
+class BitVectorBlack : public CxxTest::TestSuite {
+
+
+public:
+
+  void testStringConstructor() {
+    BitVector b1("0101",2);
+    TS_ASSERT_EQUALS( 4, b1.getSize() );
+    TS_ASSERT_EQUALS( "0101", b1.toString() );
+    TS_ASSERT_EQUALS( "5", b1.toString(10) );
+    TS_ASSERT_EQUALS( "5", b1.toString(16) );
+
+    BitVector b2("000001", 2);
+    TS_ASSERT_EQUALS( 6, b2.getSize() );
+    TS_ASSERT_EQUALS( "000001", b2.toString() );
+    TS_ASSERT_EQUALS( "1", b2.toString(10) );
+    TS_ASSERT_EQUALS( "1", b2.toString(16) );
+
+    BitVector b3("7f", 16);
+    TS_ASSERT_EQUALS( 8, b3.getSize() );
+    TS_ASSERT_EQUALS( "01111111", b3.toString() );
+    TS_ASSERT_EQUALS( "127", b3.toString(10) );
+    TS_ASSERT_EQUALS( "7f", b3.toString(16) );
+
+    BitVector b4("01a", 16);
+    TS_ASSERT_EQUALS( 12, b4.getSize() );
+    TS_ASSERT_EQUALS( "000000011010", b4.toString() );
+    TS_ASSERT_EQUALS( "26", b4.toString(10) );
+    TS_ASSERT_EQUALS( "1a", b4.toString(16) );
+  }
+};