From 99c42d62491307279403059690fa31be1fb3af63 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Mon, 2 May 2011 05:04:36 +0000 Subject: 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. --- src/parser/cvc/Cvc.g | 16 +++++++++++++--- src/parser/smt/Smt.g | 45 ++++++++++++++++++++++++++++++++++++++------- src/parser/smt2/Smt2.g | 32 +++++++++++++++++++++++++------- 3 files changed, 76 insertions(+), 17 deletions(-) (limited to 'src/parser') 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 #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 + #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 @@ -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 ; -- cgit v1.2.3