* make Model class private (as discussed at meeting today)

* fix minor issue with s-expr parsing in CVC and SMT grammars
* other minor things

(this commit was certified error- and warning-free by the test-and-commit script.)

2 files changed, 20 insertions, 14 deletions

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 22459037d..40f35093f 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -320,7 +320,7 @@ Kind getOperatorKind(int type, bool& negate) {
   case INTDIV_TOK: return kind::INTS_DIVISION;
   case MOD_TOK: return kind::INTS_MODULUS;
   case DIV_TOK: return kind::DIVISION;
-  case EXP_TOK: break;
+  case EXP_TOK: return kind::POW;
 
     // bvBinop
   case CONCAT_TOK: return kind::BITVECTOR_CONCAT;
@@ -570,8 +570,9 @@ parseCommand returns [CVC4::Command* cmd = NULL]
     { std::string s = AntlrInput::tokenText($IDENTIFIER);
       if(s == "benchmark") {
         PARSER_STATE->parseError("In CVC4 presentation language mode, but SMT-LIBv1 format detected.  Use --lang smt1 for SMT-LIBv1 support.");
-      } else if(s == "set" || s == "get") {
-        PARSER_STATE->parseError("In CVC4 presentation language mode, but SMT-LIBv2 format detected.  Use --lang smt2 for SMT-LIBv2 support.");
+      } else if(s == "set" || s == "get" || s == "declare" ||
+                s == "define" || s == "assert") {
+        PARSER_STATE->parseError("In CVC4 presentation language mode, but SMT-LIB format detected.  Use --lang smt for SMT-LIB support.");
       } else {
         PARSER_STATE->parseError("A CVC4 presentation language command cannot begin with a parenthesis; expected command name.");
       }
@@ -782,7 +783,9 @@ simpleSymbolicExpr[CVC4::SExpr& sexpr]
   CVC4::Rational r;
 }
   : INTEGER_LITERAL
-    { sexpr = SExpr(AntlrInput::tokenToInteger($INTEGER_LITERAL)); }
+    { sexpr = SExpr(Integer(AntlrInput::tokenText($INTEGER_LITERAL))); }
+  | MINUS_TOK INTEGER_LITERAL
+    { sexpr = SExpr(-Integer(AntlrInput::tokenText($INTEGER_LITERAL))); }
   | DECIMAL_LITERAL
     { sexpr = SExpr(AntlrInput::tokenToRational($DECIMAL_LITERAL)); }
   | HEX_LITERAL
@@ -1784,15 +1787,15 @@ bvTerm[CVC4::Expr& f]
     /* BV sign extension */
   | SX_TOK LPAREN formula[f] COMMA k=numeral RPAREN
     { unsigned n = BitVectorType(f.getType()).getSize();
-      // Sign extension in TheoryBitVector is defined as in SMT-LIBv2
+      // Sign extension in TheoryBitVector is defined as in SMT-LIB
       // which is different than in the CVC language
       // SX(BITVECTOR(k), n) in CVC language extends to n bits
-      // In SMT-LIBv2, such a thing expands to k + n bits
+      // In SMT-LIB, such a thing expands to k + n bits
       f = MK_EXPR(MK_CONST(BitVectorSignExtend(k - n)), f); }
     /* BV zero extension */
   | BVZEROEXTEND_TOK LPAREN formula[f] COMMA k=numeral RPAREN
     { unsigned n = BitVectorType(f.getType()).getSize();
-      // Zero extension in TheoryBitVector is defined as in SMT-LIBv2
+      // Zero extension in TheoryBitVector is defined as in SMT-LIB
       // which is the same as in CVC3, but different than SX!
       // SX(BITVECTOR(k), n) in CVC language extends to n bits
       // BVZEROEXTEND(BITVECTOR(k), n) in CVC language extends to k + n bits
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index dbefc0305..a49ae35c5 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -5,7 +5,7 @@
  ** Major contributors: mdeters
  ** Minor contributors (to current version): taking
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012  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
@@ -34,7 +34,7 @@ options {
 @header {
 /**
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012  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
@@ -124,8 +124,9 @@ namespace CVC4 {
 using namespace CVC4;
 using namespace CVC4::parser;
 
-/* These need to be macros so they can refer to the PARSER macro, which will be defined
- * by ANTLR *after* this section. (If they were functions, PARSER would be undefined.) */
+/* These need to be macros so they can refer to the PARSER macro, which
+ * will be defined by ANTLR *after* this section. (If they were functions,
+ * PARSER would be undefined.) */
 #undef PARSER_STATE
 #define PARSER_STATE ((Smt2*)PARSER->super)
 #undef EXPR_MANAGER
@@ -140,7 +141,8 @@ using namespace CVC4::parser;
 
 /**
  * Parses an expression.
- * @return the parsed expression, or the Null Expr if we've reached the end of the input
+ * @return the parsed expression, or the Null Expr if we've reached the
+ * end of the input
  */
 parseExpr returns [CVC4::parser::smt2::myExpr expr]
 @declarations {
@@ -160,7 +162,8 @@ parseCommand returns [CVC4::Command* cmd = NULL]
   ;
 
 /**
- * Parse the internal portion of the command, ignoring the surrounding parentheses.
+ * Parse the internal portion of the command, ignoring the surrounding
+ * parentheses.
  */
 command returns [CVC4::Command* cmd = NULL]
 @declarations {
@@ -631,7 +634,7 @@ simpleSymbolicExpr[CVC4::SExpr& sexpr]
   std::string s;
 }
   : INTEGER_LITERAL
-    { sexpr = SExpr(AntlrInput::tokenToInteger($INTEGER_LITERAL)); }
+    { sexpr = SExpr(Integer(AntlrInput::tokenText($INTEGER_LITERAL))); }
   | DECIMAL_LITERAL
     { sexpr = SExpr(AntlrInput::tokenToRational($DECIMAL_LITERAL)); }
   | str[s]