This is a merge from the "theoryfixes+cdattrhash" branch. The changes

are somewhat disparate but belonged on the same branch because they were
held back from trunk all for the same reason (to keep the trunk stable
for furious bitvector development).  Dejan has now given me the go-ahead
for a merge.

=========================================
THIS COMMIT CHANGES THE THEORY INTERFACE!
=========================================

Theory constructors are expected to take an additional "Valuation*"
parameter that each Theory should send along to the base class
constructor.  The base class Theory keeps the Valuation* in a
d_valuation field for use by it and by its derived classes.
Theory::getValue() no longer takes a Valuation* (it is expected
to use d_valuation instead).  This allows other theory functions
to take advantage of getValue() for debugging or heuristic
purposes.

TODO BEFORE MERGE TO TRUNK:
****implement BitIterator find() in CDAttrHash<bool>.

Specifically:

* Added QF_BV support for SMT-LIB v2.
* Two adjustments to the theory interface as requested by Tim King:
  1. As described above.
  2. Theories now have const access to the fact queue through base
     class functions facts_begin() and facts_end(); useful for
     debugging.
* Added an "Asserted" attribute so that theories can check if something
  has been asserted or not (and therefore not propagate it).  However, this
  has been disabled for now, pending more data on the overhead of it, and
  pending discussion at the 3/25/2011 meeting.
* Do not define NDEBUG in MiniSat in assertion-enabled builds (so
  that MiniSat asserts are evaluated).
* As a result of the new MiniSat assertions, some --incremental
  regressions had to be disabled; also, some bitvectors ?!!
* Bug 71 is resolved by adding a specialization for CDAttrHash<> in the
  attribute package.
* Fixes for some warnings flagged by clang.
* System tests have arrived!  So far mainly infrastructure for having
  system tests, but there is a system test aimed at improving code
  coverage of the printer package.
* Minor other adjustments to documentation and coding to be more
  conformant to CVC4 policy.

Tests have been performed to demonstrate that these changes have no or
negligible effect on performance.  In particular, changing the
CDAttrHash<> doesn't have any real effect on performance or memory right
now, since there is only one context-dependent boolean flag (as soon
as another is added, the effect is noticeable but probably still slight).

4 files changed, 175 insertions, 25 deletions

diff --git a/src/parser/input.h b/src/parser/input.h
index 6ed9bb441..b9123fc45 100644
--- a/src/parser/input.h
+++ b/src/parser/input.h
@@ -94,10 +94,11 @@ class CVC4_PUBLIC Input {
   InputStream *d_inputStream;
 
   /* Since we own d_inputStream and it needs to be freed, we need to prevent
-   * copy construction and assignment.
+   * copy construction and assignment.  Mark them private and do not define
+   * them.
    */
-  Input(const Input& input) { Unimplemented("Copy constructor for Input."); }
-  Input& operator=(const Input& input) { Unimplemented("operator= for Input."); }
+  Input(const Input& input) CVC4_UNUSED;
+  Input& operator=(const Input& input) CVC4_UNUSED;
 
 public:
 
diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g
index f125826d3..39d834891 100644
--- a/src/parser/smt/Smt.g
+++ b/src/parser/smt/Smt.g
@@ -595,7 +595,7 @@ ROTATE_LEFT_TOK   : 'rotate_left';
 ROTATE_RIGHT_TOK  : 'rotate_right';
 
 /**
- * Mathces a bit-vector constant of the form bv123
+ * Matches a bit-vector constant of the form bv123
  */
 BITVECTOR_BV_CONST
   : 'bv' DIGIT+
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 705eee4d4..f34279149 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** Minor contributors (to current version): mdeters, taking
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  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
@@ -27,7 +27,7 @@ options {
 @header {
 /**
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  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
@@ -321,6 +321,7 @@ term[CVC4::Expr& expr]
 @init {
   Debug("parser") << "term: " << AntlrInput::tokenText(LT(1)) << std::endl;
   Kind kind;
+  Expr op;
   std::string name;
   std::vector<Expr> args;
   SExpr sexpr;
@@ -356,18 +357,27 @@ term[CVC4::Expr& expr]
   | /* A non-built-in function application */
     LPAREN_TOK
     functionName[name,CHECK_DECLARED]
-    { args.push_back(Expr()); }
-    termList[args,expr] RPAREN_TOK
     { PARSER_STATE->checkFunction(name);
       const bool isDefinedFunction =
         PARSER_STATE->isDefinedFunction(name);
-      expr = isDefinedFunction ?
-        PARSER_STATE->getFunction(name) :
-        PARSER_STATE->getVariable(name);
-      args[0] = expr;
-      expr = MK_EXPR(isDefinedFunction ?
-                     CVC4::kind::APPLY :
-                     CVC4::kind::APPLY_UF, args); }
+      if(isDefinedFunction) {
+        expr = PARSER_STATE->getFunction(name);
+        kind = CVC4::kind::APPLY;
+      } else {
+        expr = PARSER_STATE->getVariable(name);
+        kind = CVC4::kind::APPLY_UF;
+      }
+      args.push_back(expr);
+    }
+    termList[args,expr] RPAREN_TOK
+    { Debug("parser") << "args has size " << args.size() << std::endl << "expr is " << expr << std::endl;
+      for(std::vector<Expr>::iterator i = args.begin(); i != args.end(); ++i)
+        Debug("parser") << "++ " << *i << std::endl;
+      expr = MK_EXPR(kind, args); }
+
+  | /* An indexed function application */
+    LPAREN_TOK indexedFunctionName[op] termList[args,expr] RPAREN_TOK
+    { expr = MK_EXPR(op, args); }
 
   | /* a let binding */
     LPAREN_TOK LET_TOK LPAREN_TOK
@@ -421,19 +431,62 @@ term[CVC4::Expr& expr]
       // valid GMP rational string
       expr = MK_CONST( AntlrInput::tokenToRational($DECIMAL_LITERAL) ); }
 
+  | LPAREN_TOK INDEX_TOK bvLit=SYMBOL size=INTEGER_LITERAL RPAREN_TOK
+    { if(AntlrInput::tokenText($bvLit).find("bv") == 0) {
+        expr = MK_CONST( AntlrInput::tokenToBitvector($bvLit, $size) );
+      } else {
+        PARSER_STATE->parseError("Unexpected symbol `" + AntlrInput::tokenText($bvLit) + "'");
+      }
+    }
+
   | HEX_LITERAL
     { Assert( AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0 );
-      std::string hexString = AntlrInput::tokenTextSubstr($HEX_LITERAL,2);
+      std::string hexString = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2);
       expr = MK_CONST( BitVector(hexString, 16) ); }
 
   | BINARY_LITERAL
     { Assert( AntlrInput::tokenText($BINARY_LITERAL).find("#b") == 0 );
-      std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL,2);
+      std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 2);
       expr = MK_CONST( BitVector(binString, 2) ); }
     // NOTE: Theory constants go here
   ;
 
 /**
+ * Matches a bit-vector operator (the ones parametrized by numbers)
+ */
+indexedFunctionName[CVC4::Expr& op]
+  : LPAREN_TOK INDEX_TOK
+    ( 'extract' n1=INTEGER_LITERAL n2=INTEGER_LITERAL
+      { op = MK_CONST(BitVectorExtract(AntlrInput::tokenToUnsigned($n1),
+                                       AntlrInput::tokenToUnsigned($n2))); }
+    | 'repeat' n=INTEGER_LITERAL
+      { op = MK_CONST(BitVectorRepeat(AntlrInput::tokenToUnsigned($n))); }
+    | 'zero_extend' n=INTEGER_LITERAL
+      { op = MK_CONST(BitVectorZeroExtend(AntlrInput::tokenToUnsigned($n))); }
+    | 'sign_extend' n=INTEGER_LITERAL
+      { op = MK_CONST(BitVectorSignExtend(AntlrInput::tokenToUnsigned($n))); }
+    | 'rotate_left' n=INTEGER_LITERAL
+      { op = MK_CONST(BitVectorRotateLeft(AntlrInput::tokenToUnsigned($n))); }
+    | 'rotate_right' n=INTEGER_LITERAL
+      { op = MK_CONST(BitVectorRotateRight(AntlrInput::tokenToUnsigned($n))); }
+    | badIndexedFunctionName
+   )
+    RPAREN_TOK
+  ;
+
+/**
+ * Matches an erroneous indexed function name (and args) for better
+ * error reporting.
+ */
+badIndexedFunctionName
+@declarations {
+  std::string name;
+}
+  : symbol[name,CHECK_NONE,SYM_VARIABLE] INTEGER_LITERAL+
+      { PARSER_STATE->parseError(std::string("Unknown indexed function `") + name + "'"); }
+  ;
+
+/**
  * Matches a sequence of terms and puts them into the formulas
  * vector.
  * @param formulas the vector to fill with terms
@@ -472,8 +525,40 @@ builtinOp[CVC4::Kind& kind]
   | MINUS_TOK    { $kind = CVC4::kind::MINUS; }
   | STAR_TOK     { $kind = CVC4::kind::MULT; }
   | DIV_TOK      { $kind = CVC4::kind::DIVISION; }
+
   | SELECT_TOK   { $kind = CVC4::kind::SELECT; }
   | STORE_TOK    { $kind = CVC4::kind::STORE; }
+
+  | CONCAT_TOK   { $kind = CVC4::kind::BITVECTOR_CONCAT; }
+  | BVNOT_TOK   { $kind = CVC4::kind::BITVECTOR_NOT; }
+  | BVAND_TOK   { $kind = CVC4::kind::BITVECTOR_AND; }
+  | BVOR_TOK   { $kind = CVC4::kind::BITVECTOR_OR; }
+  | BVNEG_TOK   { $kind = CVC4::kind::BITVECTOR_NEG; }
+  | BVADD_TOK   { $kind = CVC4::kind::BITVECTOR_PLUS; }
+  | BVMUL_TOK   { $kind = CVC4::kind::BITVECTOR_MULT; }
+  | BVUDIV_TOK   { $kind = CVC4::kind::BITVECTOR_UDIV; }
+  | BVUREM_TOK   { $kind = CVC4::kind::BITVECTOR_UREM; }
+  | BVSHL_TOK     { $kind = CVC4::kind::BITVECTOR_SHL; }
+  | BVLSHR_TOK     { $kind = CVC4::kind::BITVECTOR_LSHR; }
+  | BVULT_TOK     { $kind = CVC4::kind::BITVECTOR_ULT; }
+  | BVNAND_TOK     { $kind = CVC4::kind::BITVECTOR_NAND; }
+  | BVNOR_TOK     { $kind = CVC4::kind::BITVECTOR_NOR; }
+  | BVXOR_TOK     { $kind = CVC4::kind::BITVECTOR_XOR; }
+  | BVXNOR_TOK     { $kind = CVC4::kind::BITVECTOR_XNOR; }
+  | BVCOMP_TOK     { $kind = CVC4::kind::BITVECTOR_COMP; }
+  | BVSUB_TOK     { $kind = CVC4::kind::BITVECTOR_SUB; }
+  | BVSDIV_TOK     { $kind = CVC4::kind::BITVECTOR_SDIV; }
+  | BVSREM_TOK     { $kind = CVC4::kind::BITVECTOR_SREM; }
+  | BVSMOD_TOK     { $kind = CVC4::kind::BITVECTOR_SMOD; }
+  | BVASHR_TOK     { $kind = CVC4::kind::BITVECTOR_ASHR; }
+  | 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; }
+
   // NOTE: Theory operators go here
   ;
 
@@ -534,9 +619,21 @@ sortSymbol[CVC4::Type& t]
 @declarations {
   std::string name;
   std::vector<CVC4::Type> args;
+  std::vector<uint64_t> numerals;
 }
   : sortName[name,CHECK_NONE]
   	{ t = PARSER_STATE->getSort(name); }
+  | LPAREN_TOK INDEX_TOK symbol[name,CHECK_NONE,SYM_SORT] nonemptyNumeralList[numerals] RPAREN_TOK
+    {
+      if( name == "BitVec" ) {
+        if( numerals.size() != 1 ) {
+          PARSER_STATE->parseError("Illegal bitvector type.");
+        }
+        t = EXPR_MANAGER->mkBitVectorType(numerals.front());
+      } else {
+        Unhandled(name);
+      }
+    }
   | LPAREN_TOK symbol[name,CHECK_NONE,SYM_SORT] sortList[args] RPAREN_TOK
     {
       if( name == "Array" ) {
@@ -580,6 +677,16 @@ symbol[std::string& id,
       PARSER_STATE->checkDeclaration(id, check, type); }
   ;
 
+/**
+ * Matches a nonempty list of numerals.
+ * @param numerals the (empty) vector to house the numerals.
+ */
+nonemptyNumeralList[std::vector<uint64_t>& numerals]
+  : ( INTEGER_LITERAL
+      { numerals.push_back(AntlrInput::tokenToUnsigned($INTEGER_LITERAL)); }
+    )+
+  ;
+
 // Base SMT-LIB tokens
 ASSERT_TOK : 'assert';
 CHECKSAT_TOK : 'check-sat';
@@ -596,6 +703,7 @@ LET_TOK : 'let';
 ATTRIBUTE_TOK : '!';
 LPAREN_TOK : '(';
 RPAREN_TOK : ')';
+INDEX_TOK : '_';
 SET_LOGIC_TOK : 'set-logic';
 SET_INFO_TOK : 'set-info';
 GET_INFO_TOK : 'get-info';
@@ -631,6 +739,36 @@ STORE_TOK         : 'store';
 TILDE_TOK         : '~';
 XOR_TOK           : 'xor';
 
+CONCAT_TOK : 'concat';
+BVNOT_TOK : 'bvnot';
+BVAND_TOK : 'bvand';
+BVOR_TOK : 'bvor';
+BVNEG_TOK : 'bvneg';
+BVADD_TOK : 'bvadd';
+BVMUL_TOK : 'bvmul';
+BVUDIV_TOK : 'bvudiv';
+BVUREM_TOK : 'bvurem';
+BVSHL_TOK : 'bvshl';
+BVLSHR_TOK : 'bvlshr';
+BVULT_TOK : 'bvult';
+BVNAND_TOK : 'bvnand';
+BVNOR_TOK : 'bvnor';
+BVXOR_TOK : 'bvxor';
+BVXNOR_TOK : 'bvxnor';
+BVCOMP_TOK : 'bvcomp';
+BVSUB_TOK : 'bvsub';
+BVSDIV_TOK : 'bvsdiv';
+BVSREM_TOK : 'bvsrem';
+BVSMOD_TOK : 'bvsmod';
+BVASHR_TOK : 'bvashr';
+BVULE_TOK : 'bvule';
+BVUGT_TOK : 'bvugt';
+BVUGE_TOK : 'bvuge';
+BVSLT_TOK : 'bvslt';
+BVSLE_TOK : 'bvsle';
+BVSGT_TOK : 'bvsgt';
+BVSGE_TOK : 'bvsge';
+
 /**
  * Matches a symbol from the input. A symbol is a "simple" symbol or a
  * sequence of printable ASCII characters that starts and ends with | and
@@ -651,10 +789,12 @@ KEYWORD
 
 /** Matches a "simple" symbol: a non-empty sequence of letters, digits and
  * the characters + - / * = % ? ! . $ ~ & ^ < > @ that does not start with a
- * digit.
+ * digit, and is not the special reserved symbol '_'.
  */
 fragment SIMPLE_SYMBOL
-  : (ALPHA | SYMBOL_CHAR) (ALPHA | DIGIT | SYMBOL_CHAR)*
+  : (ALPHA | SYMBOL_CHAR) (ALPHA | DIGIT | SYMBOL_CHAR)+
+  | ALPHA
+  | SYMBOL_CHAR_NOUNDERSCORE
   ;
 
 /**
@@ -703,14 +843,14 @@ DECIMAL_LITERAL
 /**
  * Matches a hexadecimal constant.
  */
- HEX_LITERAL
+HEX_LITERAL
   : '#x' HEX_DIGIT+
   ;
 
 /**
  * Matches a binary constant.
  */
- BINARY_LITERAL
+BINARY_LITERAL
   : '#b' ('0' | '1')+
   ;
 
@@ -730,7 +870,6 @@ COMMENT
   : ';' (~('\n' | '\r'))* { SKIP(); }
   ;
 
-
 /**
  * Matches any letter ('a'-'z' and 'A'-'Z').
  */
@@ -750,11 +889,15 @@ fragment HEX_DIGIT : DIGIT | 'a'..'f' | 'A'..'F';
 /**
  * Matches the characters that may appear in a "symbol" (i.e., an identifier)
  */
-fragment SYMBOL_CHAR
-  : '+' | '-' | '/' | '*' | '=' | '%' | '?' | '!' | '.' | '$' | '_' | '~'
+fragment SYMBOL_CHAR_NOUNDERSCORE
+  : '+' | '-' | '/' | '*' | '=' | '%' | '?' | '!' | '.' | '$' | '~'
   | '&' | '^' | '<' | '>' | '@'
   ;
 
+fragment SYMBOL_CHAR
+  : SYMBOL_CHAR_NOUNDERSCORE | '_'
+  ;
+
 /**
  * Matches an allowed escaped character.
  */
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index e41e0e26a..03b901164 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -82,6 +82,9 @@ void Smt2::addTheory(Theory theory) {
     addArithmeticOperators();
     break;
 
+  case THEORY_BITVECTORS:
+    break;
+
   default:
     Unhandled(theory);
   }
@@ -134,6 +137,10 @@ void Smt2::setLogic(const std::string& name) {
     addOperator(kind::APPLY_UF);
     break;
 
+  case Smt::QF_BV:
+    addTheory(THEORY_BITVECTORS);
+    break;
+
   case Smt::AUFLIA:
   case Smt::AUFLIRA:
   case Smt::AUFNIRA:
@@ -141,7 +148,6 @@ void Smt2::setLogic(const std::string& name) {
   case Smt::UFNIA:
   case Smt::QF_AUFBV:
   case Smt::QF_AUFLIA:
-  case Smt::QF_BV:
     Unhandled(name);
   }
 }