Minor fixes to various parts of CVC4, including the removal of the uintptr_t constructors for Type and Expr (which existed due to ANTLR limitations). These issues are now handled (as a hack, due to said limitations) in the parser rather than the CVC4 core.

3 files changed, 76 insertions, 17 deletions

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 8df9ea6a0..af0024156 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -433,6 +433,7 @@ Expr addNots(ExprManager* em, size_t n, Expr e) {
 
 @parser::includes {
 
+#include <stdint.h>
 #include "expr/command.h"
 #include "parser/parser.h"
 #include "util/subrange_bound.h"
@@ -440,9 +441,7 @@ Expr addNots(ExprManager* em, size_t n, Expr e) {
 
 namespace CVC4 {
   class Expr;
-}/* CVC4 namespace */
 
-namespace CVC4 {
   namespace parser {
     namespace cvc {
       /**
@@ -469,6 +468,17 @@ namespace CVC4 {
         mySubrangeBound(const Integer& i) : CVC4::SubrangeBound(i) {}
         mySubrangeBound(const SubrangeBound& b) : CVC4::SubrangeBound(b) {}
       };/* class mySubrangeBound */
+
+      /**
+       * Just exists to give us the uintptr_t construction that
+       * ANTLR requires.
+       */
+      struct myExpr : public CVC4::Expr {
+        myExpr() : CVC4::Expr() {}
+        myExpr(uintptr_t) : CVC4::Expr() {}
+        myExpr(const Expr& e) : CVC4::Expr(e) {}
+        myExpr(const myExpr& e) : CVC4::Expr(e) {}
+      };/* struct myExpr */
     }/* CVC4::parser::cvc namespace */
   }/* CVC4::parser namespace */
 }/* CVC4 namespace */
@@ -521,7 +531,7 @@ using namespace CVC4::parser;
  * Parses an expression.
  * @return the parsed expression
  */
-parseExpr returns [CVC4::Expr expr]
+parseExpr returns [CVC4::parser::cvc::myExpr expr]
   : formula[expr]
   | EOF
   ;
diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g
index e964c020a..0cceb53e4 100644
--- a/src/parser/smt/Smt.g
+++ b/src/parser/smt/Smt.g
@@ -29,7 +29,7 @@ options {
   // Note that CVC4's BoundedTokenBuffer requires a fixed k !
   // If you change this k, change it also in smt_input.cpp !
   k = 2;
-}
+}/* options */
 
 @header {
 /**
@@ -40,7 +40,7 @@ options {
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **/
-}
+}/* @header */
 
 @lexer::includes {
 /** This suppresses warnings about the redefinition of token symbols between
@@ -58,19 +58,50 @@ options {
 #define ANTLR3_INLINE_INPUT_ASCII
 
 #include "parser/antlr_tracing.h"
-}
+}/* @lexer::includes */
 
 @parser::includes {
+
+#include <stdint.h>
+
 #include "expr/command.h"
 #include "parser/parser.h"
 #include "parser/antlr_tracing.h"
 
 namespace CVC4 {
   class Expr;
+
+  namespace parser {
+    namespace smt {
+      /**
+       * Just exists to provide the uintptr_t constructor that ANTLR
+       * requires.
+       */
+      struct myExpr : public CVC4::Expr {
+        myExpr() : CVC4::Expr() {}
+        myExpr(void*) : CVC4::Expr() {}
+        myExpr(const Expr& e) : CVC4::Expr(e) {}
+        myExpr(const myExpr& e) : CVC4::Expr(e) {}
+      };/* struct myExpr */
+
+      /**
+       * Just exists to provide the uintptr_t constructor that ANTLR
+       * requires.
+       */
+      struct myType : public CVC4::Type {
+        myType() : CVC4::Type() {}
+        myType(void*) : CVC4::Type() {}
+        myType(const Type& t) : CVC4::Type(t) {}
+        myType(const myType& t) : CVC4::Type(t) {}
+      };/* struct myType */
+    }/* CVC4::parser::smt namespace */
+  }/* CVC4::parser namespace */
 }/* CVC4 namespace */
-}
+
+}/* @parser::includes */
 
 @parser::postinclude {
+
 #include "expr/expr.h"
 #include "expr/kind.h"
 #include "expr/type.h"
@@ -96,14 +127,14 @@ using namespace CVC4::parser;
 #undef MK_CONST
 #define MK_CONST EXPR_MANAGER->mkConst
 
-}
+}/* @parser::postinclude */
 
 
 /**
  * Parses an expression.
  * @return the parsed expression
  */
-parseExpr returns [CVC4::Expr expr]
+parseExpr returns [CVC4::parser::smt::myExpr expr]
   : annotatedFormula[expr]
   | EOF
   ;
@@ -445,7 +476,7 @@ sortName[std::string& name, CVC4::parser::DeclarationCheck check]
   : identifier[name,check,SYM_SORT]
   ;
 
-sortSymbol returns [CVC4::Type t]
+sortSymbol returns [CVC4::parser::smt::myType t]
 @declarations {
   std::string name;
 }
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 17ea1611d..a8dfbfeab 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -29,7 +29,7 @@ options {
   // Note that CVC4's BoundedTokenBuffer requires a fixed k !
   // If you change this k, change it also in smt2_input.cpp !
   k = 2;
-}
+}/* options */
 
 @header {
 /**
@@ -40,7 +40,7 @@ options {
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **/
-}
+}/* @header */
 
 @lexer::includes {
 
@@ -59,7 +59,8 @@ options {
 #define ANTLR3_INLINE_INPUT_ASCII
 
 #include "parser/antlr_tracing.h"
-}
+
+}/* @lexer::includes */
 
 @lexer::postinclude {
 #include <stdint.h>
@@ -73,7 +74,7 @@ using namespace CVC4::parser;
 
 #undef PARSER_STATE
 #define PARSER_STATE ((Smt2*)LEXER->super)
-}
+}/* @lexer::postinclude */
 
 @parser::includes {
 #include "expr/command.h"
@@ -81,10 +82,27 @@ using namespace CVC4::parser;
 
 namespace CVC4 {
   class Expr;
+
+  namespace parser {
+    namespace smt2 {
+      /**
+       * Just exists to provide the uintptr_t constructor that ANTLR
+       * requires.
+       */
+      struct myExpr : public CVC4::Expr {
+        myExpr() : CVC4::Expr() {}
+        myExpr(void*) : CVC4::Expr() {}
+        myExpr(const Expr& e) : CVC4::Expr(e) {}
+        myExpr(const myExpr& e) : CVC4::Expr(e) {}
+      };/* struct myExpr */
+    }/* CVC4::parser::smt2 namespace */
+  }/* CVC4::parser namespace */
 }/* CVC4 namespace */
-}
+
+}/* @parser::includes */
 
 @parser::postinclude {
+
 #include "expr/expr.h"
 #include "expr/kind.h"
 #include "expr/type.h"
@@ -110,13 +128,13 @@ using namespace CVC4::parser;
 #undef MK_CONST
 #define MK_CONST EXPR_MANAGER->mkConst
 
-}
+}/* parser::postinclude */
 
 /**
  * Parses an expression.
  * @return the parsed expression, or the Null Expr if we've reached the end of the input
  */
-parseExpr returns [CVC4::Expr expr]
+parseExpr returns [CVC4::parser::smt2::myExpr expr]
   : term[expr]
   | EOF
   ;