summaryrefslogtreecommitdiff
path: root/src/parser
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser')
-rw-r--r--src/parser/cvc/Cvc.g210
-rw-r--r--src/parser/input.h8
-rw-r--r--src/parser/parser.cpp70
-rw-r--r--src/parser/parser.h15
-rw-r--r--src/parser/smt/Smt.g8
-rw-r--r--src/parser/smt2/Smt2.g8
6 files changed, 258 insertions, 61 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 0a05271e2..33e576a32 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -2,10 +2,10 @@
/*! \file Cvc.g
** \verbatim
** Original author: cconway
- ** Major contributors: none
- ** Minor contributors (to current version): dejan, mdeters
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): dejan
** 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
@@ -37,7 +37,7 @@ options {
@lexer::includes {
/** This suppresses warnings about the redefinition of token symbols between different
- * parsers. The redefinitions should be harmless as long as no client: (a) #include's
+ * parsers. The redefinitions should be harmless as long as no client: (a) #include's
* the lexer headers for two grammars AND (b) uses the token symbol definitions. */
#pragma GCC system_header
@@ -56,6 +56,26 @@ options {
namespace CVC4 {
class Expr;
}/* CVC4 namespace */
+
+namespace CVC4 {
+ namespace parser {
+ namespace cvc {
+ /**
+ * This class is just here to get around an unfortunate bit of Antlr.
+ * We use strings below as return values from rules, which require
+ * them to be constructible by a uintptr_t. So we derive the string
+ * class to provide just such a conversion.
+ */
+ class mystring : public std::string {
+ public:
+ mystring(const std::string& s) : std::string(s) {}
+ mystring(uintptr_t) : std::string() {}
+ mystring() : std::string() {}
+ };/* class mystring */
+ }/* CVC4::parser::cvc namespace */
+ }/* CVC4::parser namespace */
+}/* CVC4 namespace */
+
}
@parser::postinclude {
@@ -72,7 +92,7 @@ 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.) */
-#undef PARSER_STATE
+#undef PARSER_STATE
#define PARSER_STATE ((Parser*)PARSER->super)
#undef EXPR_MANAGER
#define EXPR_MANAGER PARSER_STATE->getExprManager()
@@ -109,6 +129,8 @@ command returns [CVC4::Command* cmd = 0]
Expr f;
SExpr sexpr;
std::string s;
+ Type t;
+ std::vector<CVC4::Datatype> dts;
Debug("parser-extra") << "command: " << AntlrInput::tokenText(LT(1)) << std::endl;
}
: ASSERT_TOK formula[f] SEMICOLON { cmd = new AssertCommand(f); }
@@ -119,6 +141,13 @@ command returns [CVC4::Command* cmd = 0]
{ cmd = new SetOptionCommand(AntlrInput::tokenText($STRING_LITERAL), sexpr); }
| PUSH_TOK SEMICOLON { cmd = new PushCommand(); }
| POP_TOK SEMICOLON { cmd = new PopCommand(); }
+ // Datatypes can be mututally-recursive if they're in the same
+ // definition block, separated by a comma. So we parse everything
+ // and then ask the ExprManager to resolve everything in one go.
+ | DATATYPE_TOK datatypeDef[dts]
+ ( COMMA datatypeDef[dts] )*
+ END_TOK SEMICOLON
+ { cmd = new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts)); }
| declaration[cmd]
| EOF
;
@@ -159,8 +188,8 @@ declType[CVC4::Type& t, std::vector<std::string>& idList]
Debug("parser-extra") << "declType: " << AntlrInput::tokenText(LT(1)) << std::endl;
}
: /* A sort declaration (e.g., "T : TYPE") */
- TYPE_TOK
- { PARSER_STATE->mkSorts(idList);
+ TYPE_TOK
+ { PARSER_STATE->mkSorts(idList);
t = EXPR_MANAGER->kindType(); }
| /* A variable declaration */
type[t] { PARSER_STATE->mkVars(idList,t); }
@@ -179,7 +208,7 @@ type[CVC4::Type& t]
: /* Simple type */
baseType[t]
| /* Single-parameter function type */
- baseType[t] ARROW_TOK baseType[t2]
+ baseType[t] ARROW_TOK baseType[t2]
{ t = EXPR_MANAGER->mkFunctionType(t,t2); }
| /* Multi-parameter function type */
LPAREN baseType[t]
@@ -218,34 +247,62 @@ identifier[std::string& id,
;
/**
- * Matches a type.
- * TODO: parse more types
+ * Matches a type (which MUST be already declared).
+ *
+ * @return the type identifier
*/
baseType[CVC4::Type& t]
+ : maybeUndefinedBaseType[t,CHECK_DECLARED]
+ ;
+
+/**
+ * Matches a type (which may not be declared yet). Returns the
+ * identifier. If the type is declared, returns the Type in the 't'
+ * parameter; otherwise a null Type is returned in 't'. If 'check' is
+ * CHECK_DECLARED and the type is not declared, an exception is
+ * thrown.
+ *
+ * @return the type identifier
+ *
+ * @TODO parse more types
+ */
+maybeUndefinedBaseType[CVC4::Type& t,
+ CVC4::parser::DeclarationCheck check] returns [CVC4::parser::cvc::mystring id]
@init {
- std::string id;
Debug("parser-extra") << "base type: " << AntlrInput::tokenText(LT(1)) << std::endl;
+ AssertArgument(check == CHECK_DECLARED || check == CHECK_NONE,
+ check, "CVC parser: can't use CHECK_UNDECLARED with maybeUndefinedBaseType[]");
}
- : BOOLEAN_TOK { t = EXPR_MANAGER->booleanType(); }
- | INT_TOK { t = EXPR_MANAGER->integerType(); }
- | REAL_TOK { t = EXPR_MANAGER->realType(); }
- | typeSymbol[t]
+ : BOOLEAN_TOK { t = EXPR_MANAGER->booleanType(); id = AntlrInput::tokenText($BOOLEAN_TOK); }
+ | INT_TOK { t = EXPR_MANAGER->integerType(); id = AntlrInput::tokenText($INT_TOK); }
+ | REAL_TOK { t = EXPR_MANAGER->realType(); id = AntlrInput::tokenText($REAL_TOK); }
+ | typeSymbol[t,check]
+ { id = $typeSymbol.id; }
;
/**
- * Matches a type identifier
+ * Matches a type identifier. Returns the identifier. If the type is
+ * declared, returns the Type in the 't' parameter; otherwise a null
+ * Type is returned in 't'. If 'check' is CHECK_DECLARED and the type
+ * is not declared, an exception is thrown.
+ *
+ * @return the type identifier
*/
-typeSymbol[CVC4::Type& t]
+typeSymbol[CVC4::Type& t,
+ CVC4::parser::DeclarationCheck check] returns [CVC4::parser::cvc::mystring id]
@init {
- std::string id;
Debug("parser-extra") << "type symbol: " << AntlrInput::tokenText(LT(1)) << std::endl;
}
- : identifier[id,CHECK_DECLARED,SYM_SORT]
- { t = PARSER_STATE->getSort(id); }
+ : identifier[id,check,SYM_SORT]
+ { bool isNew = (check == CHECK_UNDECLARED || check == CHECK_NONE) &&
+ !PARSER_STATE->isDeclared(id, SYM_SORT);
+ t = isNew ? Type() : PARSER_STATE->getSort(id);
+ }
;
/**
* Matches a CVC4 formula.
+ *
* @return the expression representing the formula
*/
formula[CVC4::Expr& formula]
@@ -311,7 +368,7 @@ iffFormula[CVC4::Expr& f]
Debug("parser-extra") << "<=> formula: " << AntlrInput::tokenText(LT(1)) << std::endl;
}
: impliesFormula[f]
- ( IFF_TOK
+ ( IFF_TOK
iffFormula[e]
{ f = MK_EXPR(CVC4::kind::IFF, f, e); }
)?
@@ -371,7 +428,7 @@ andFormula[CVC4::Expr& f]
std::vector<Expr> exprs;
Debug("parser-extra") << "AND Formula: " << AntlrInput::tokenText(LT(1)) << std::endl;
}
- : notFormula[f]
+ : notFormula[f]
( AND_TOK { exprs.push_back(f); }
notFormula[f] { exprs.push_back(f); } )*
{
@@ -412,9 +469,9 @@ comparisonFormula[CVC4::Expr& f]
( ( EQUAL_TOK { op = CVC4::kind::EQUAL; negate = false; }
| DISEQUAL_TOK { op = CVC4::kind::EQUAL; negate = true; }
| GT_TOK { op = CVC4::kind::GT; negate = false; }
- | GEQ_TOK { op = CVC4::kind::GEQ; negate = false; }
+ | GEQ_TOK { op = CVC4::kind::GEQ; negate = false; }
| LT_TOK { op = CVC4::kind::LT; negate = false; }
- | LEQ_TOK { op = CVC4::kind::LEQ; negate = false; })
+ | LEQ_TOK { op = CVC4::kind::LEQ; negate = false; })
plusTerm[e]
{ f = MK_EXPR(op, f, e);
if(negate) {
@@ -424,7 +481,7 @@ comparisonFormula[CVC4::Expr& f]
)?
;
-/** Parses a plus/minus term (left-associative).
+/** Parses a plus/minus term (left-associative).
TODO: This won't take advantage of n-ary PLUS's. */
plusTerm[CVC4::Expr& f]
@init {
@@ -435,13 +492,13 @@ plusTerm[CVC4::Expr& f]
}
: multTerm[f]
( ( PLUS_TOK { op = CVC4::kind::PLUS; }
- | MINUS_TOK { op = CVC4::kind::MINUS; } )
+ | MINUS_TOK { op = CVC4::kind::MINUS; } )
multTerm[e]
{ f = MK_EXPR(op, f, e); }
)*
;
-/** Parses a multiply/divide term (left-associative).
+/** Parses a multiply/divide term (left-associative).
TODO: This won't take advantage of n-ary MULT's. */
multTerm[CVC4::Expr& f]
@init {
@@ -451,7 +508,7 @@ multTerm[CVC4::Expr& f]
}
: expTerm[f]
( ( STAR_TOK { op = CVC4::kind::MULT; }
- | DIV_TOK { op = CVC4::kind::DIVISION; } )
+ | DIV_TOK { op = CVC4::kind::DIVISION; } )
expTerm[e]
{ f = MK_EXPR(op, f, e); }
)*
@@ -494,18 +551,29 @@ unaryTerm[CVC4::Expr& f]
std::vector<Expr> args;
Debug("parser-extra") << "term: " << AntlrInput::tokenText(LT(1)) << std::endl;
}
- : /* function application */
- // { isFunction(AntlrInput::tokenText(LT(1))) }?
+ : /* function/constructor application */
functionSymbol[f]
{ args.push_back( f ); }
LPAREN formulaList[args] RPAREN
// TODO: check arity
- { f = MK_EXPR(CVC4::kind::APPLY_UF, args); }
+ { Type t = f.getType();
+ if( t.isFunction() ) {
+ f = MK_EXPR(CVC4::kind::APPLY_UF, args);
+ } else if( t.isConstructor() ) {
+ Debug("parser-idt") << "apply constructor: " << name.c_str() << " " << args.size() << std::endl;
+ f = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, args);
+ } else if( t.isSelector() ) {
+ Debug("parser-idt") << "apply selector: " << name.c_str() << " " << args.size() << std::endl;
+ f = MK_EXPR(CVC4::kind::APPLY_SELECTOR, args);
+ } else if( t.isTester() ) {
+ Debug("parser-idt") << "apply tester: " << name.c_str() << " " << args.size() << std::endl;
+ f = MK_EXPR(CVC4::kind::APPLY_TESTER, args);
+ }
+ }
| /* if-then-else */
iteTerm[f]
-
| /* Unary minus */
MINUS_TOK unaryTerm[f] { f = MK_EXPR(CVC4::kind::UMINUS, f); }
@@ -517,10 +585,17 @@ unaryTerm[CVC4::Expr& f]
| FALSE_TOK { f = MK_CONST(false); }
| INTEGER_LITERAL { f = MK_CONST( AntlrInput::tokenToInteger($INTEGER_LITERAL) ); }
+ | DECIMAL_LITERAL { f = MK_CONST( AntlrInput::tokenToRational($DECIMAL_LITERAL) ); }
| /* variable */
identifier[name,CHECK_DECLARED,SYM_VARIABLE]
- { f = PARSER_STATE->getVariable(name); }
+ { f = PARSER_STATE->getVariable(name);
+ // datatypes: 0-ary constructors
+ if( PARSER_STATE->getType(name).isConstructor() ){
+ args.push_back( f );
+ f = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, args);
+ }
+ }
;
/**
@@ -546,7 +621,7 @@ iteElseTerm[CVC4::Expr& f]
std::vector<Expr> args;
Debug("parser-extra") << "else: " << AntlrInput::tokenText(LT(1)) << std::endl;
}
- : ELSE_TOK formula[f]
+ : ELSE_TOK formula[f]
| ELSEIF_TOK iteCondition = formula[f] { args.push_back(f); }
THEN_TOK iteThen = formula[f] { args.push_back(f); }
iteElse = iteElseTerm[f] { args.push_back(f); }
@@ -564,10 +639,65 @@ functionSymbol[CVC4::Expr& f]
std::string name;
}
: identifier[name,CHECK_DECLARED,SYM_VARIABLE]
- { PARSER_STATE->checkFunction(name);
+ { PARSER_STATE->checkFunctionLike(name);
f = PARSER_STATE->getVariable(name); }
;
+/**
+ * Parses a datatype definition
+ */
+datatypeDef[std::vector<CVC4::Datatype>& datatypes]
+@init {
+ std::string id;
+}
+ : identifier[id,CHECK_UNDECLARED,SYM_SORT]
+ { datatypes.push_back(Datatype(id)); }
+ EQUAL_TOK constructorDef[datatypes.back()]
+ ( BAR_TOK constructorDef[datatypes.back()] )*
+ ;
+
+/**
+ * Parses a constructor defintion for type
+ */
+constructorDef[CVC4::Datatype& type]
+@init {
+ std::string id;
+ CVC4::Datatype::Constructor* ctor;
+}
+ : identifier[id,CHECK_UNDECLARED,SYM_SORT]
+ {
+ // make the tester
+ std::string testerId("is_");
+ testerId.append(id);
+ PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_SORT);
+ ctor = new CVC4::Datatype::Constructor(id, testerId);
+ }
+ ( LPAREN
+ selector[*ctor]
+ ( COMMA selector[*ctor] )*
+ RPAREN
+ )?
+ { // make the constructor
+ type.addConstructor(*ctor);
+ Debug("parser-idt") << "constructor: " << id.c_str() << std::endl;
+ delete ctor;
+ }
+ ;
+
+selector[CVC4::Datatype::Constructor& ctor]
+@init {
+ std::string id;
+ Type type;
+}
+ : identifier[id,CHECK_UNDECLARED,SYM_SORT] COLON maybeUndefinedBaseType[type,CHECK_NONE]
+ { if(type.isNull()) {
+ ctor.addArg(id, Datatype::UnresolvedType($maybeUndefinedBaseType.id));
+ } else {
+ ctor.addArg(id, type);
+ }
+ Debug("parser-idt") << "selector: " << id.c_str() << std::endl;
+ }
+ ;
// Keywords
@@ -598,6 +728,16 @@ TRUE_TOK : 'TRUE';
TYPE_TOK : 'TYPE';
XOR_TOK : 'XOR';
+DATATYPE_TOK : 'DATATYPE';
+END_TOK : 'END';
+BAR_TOK : '|';
+
+ARRAY_TOK : 'ARRAY';
+OF_TOK : 'OF';
+WITH_TOK : 'WITH';
+
+BITVECTOR_TOK : 'BITVECTOR';
+
// Symbols
COLON : ':';
diff --git a/src/parser/input.h b/src/parser/input.h
index b9123fc45..71b2faeae 100644
--- a/src/parser/input.h
+++ b/src/parser/input.h
@@ -2,10 +2,10 @@
/*! \file input.h
** \verbatim
** Original author: cconway
- ** Major contributors: none
- ** Minor contributors (to current version): mdeters
+ ** Major contributors: mdeters
+ ** 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)
+ ** 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
@@ -179,7 +179,7 @@ protected:
/** Set the Parser object for this input. */
virtual void setParser(Parser& parser) = 0;
-};
+};/* class Input */
}/* CVC4::parser namespace */
}/* CVC4 namespace */
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 0ebccf720..c8a9876d5 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -72,8 +72,7 @@ Expr Parser::getFunction(const std::string& name) {
return getSymbol(name, SYM_VARIABLE);
}
-Type
-Parser::getType(const std::string& var_name,
+Type Parser::getType(const std::string& var_name,
SymbolType type) {
Assert( isDeclared(var_name, type) );
Type t = getSymbol(var_name, type).getType();
@@ -98,9 +97,15 @@ bool Parser::isBoolean(const std::string& name) {
return isDeclared(name, SYM_VARIABLE) && getType(name).isBoolean();
}
-/* Returns true if name is bound to a function. */
-bool Parser::isFunction(const std::string& name) {
- return isDeclared(name, SYM_VARIABLE) && getType(name).isFunction();
+/* Returns true if name is bound to a function-like thing (function,
+ * constructor, tester, or selector). */
+bool Parser::isFunctionLike(const std::string& name) {
+ if(!isDeclared(name, SYM_VARIABLE)) {
+ return false;
+ }
+ Type type = getType(name);
+ return type.isFunction() || type.isConstructor() ||
+ type.isTester() || type.isSelector();
}
/* Returns true if name is bound to a defined function. */
@@ -200,7 +205,7 @@ Parser::mkSortConstructor(const std::string& name, size_t arity) {
return type;
}
-const std::vector<Type>
+std::vector<Type>
Parser::mkSorts(const std::vector<std::string>& names) {
std::vector<Type> types;
for(unsigned i = 0; i < names.size(); ++i) {
@@ -209,6 +214,53 @@ Parser::mkSorts(const std::vector<std::string>& names) {
return types;
}
+std::vector<DatatypeType>
+Parser::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) {
+ std::vector<DatatypeType> types =
+ d_exprManager->mkMutualDatatypeTypes(datatypes);
+ Assert(datatypes.size() == types.size());
+ for(unsigned i = 0; i < datatypes.size(); ++i) {
+ DatatypeType t = types[i];
+ const Datatype& dt = t.getDatatype();
+ Debug("parser-idt") << "define " << dt.getName() << " as " << t << std::endl;
+ defineType(dt.getName(), t);
+ for(Datatype::const_iterator j = dt.begin(),
+ j_end = dt.end();
+ j != j_end;
+ ++j) {
+ const Datatype::Constructor& ctor = *j;
+ Expr::printtypes::Scope pts(Debug("parser-idt"), true);
+ Expr constructor = ctor.getConstructor();
+ Debug("parser-idt") << "+ define " << constructor << std::endl;
+ string constructorName = constructor.toString();
+ if(isDeclared(constructorName, SYM_VARIABLE)) {
+ throw ParserException(constructorName + " already declared");
+ }
+ defineVar(constructorName, constructor);
+ Expr tester = ctor.getTester();
+ Debug("parser-idt") << "+ define " << tester << std::endl;
+ string testerName = tester.toString();
+ if(isDeclared(testerName, SYM_VARIABLE)) {
+ throw ParserException(testerName + " already declared");
+ }
+ defineVar(testerName, tester);
+ for(Datatype::Constructor::const_iterator k = ctor.begin(),
+ k_end = ctor.end();
+ k != k_end;
+ ++k) {
+ Expr selector = (*k).getSelector();
+ Debug("parser-idt") << "+++ define " << selector << std::endl;
+ string selectorName = selector.toString();
+ if(isDeclared(selectorName, SYM_VARIABLE)) {
+ throw ParserException(selectorName + " already declared");
+ }
+ defineVar(selectorName, selector);
+ }
+ }
+ }
+ return types;
+}
+
bool Parser::isDeclared(const std::string& name, SymbolType type) {
switch(type) {
case SYM_VARIABLE:
@@ -249,10 +301,10 @@ void Parser::checkDeclaration(const std::string& varName,
}
}
-void Parser::checkFunction(const std::string& name)
+void Parser::checkFunctionLike(const std::string& name)
throw (ParserException) {
- if( d_checksEnabled && !isFunction(name) ) {
- parseError("Expecting function symbol, found '" + name + "'");
+ if( d_checksEnabled && !isFunctionLike(name) ) {
+ parseError("Expecting function-like symbol, found '" + name + "'");
}
}
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 15fe5126c..718b862ab 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -263,7 +263,7 @@ public:
* @throws ParserException if checks are enabled and name is not
* bound to a function
*/
- void checkFunction(const std::string& name) throw (ParserException);
+ void checkFunctionLike(const std::string& name) throw (ParserException);
/**
* Check that <code>kind</code> can accept <code>numArgs</code> arguments.
@@ -337,8 +337,13 @@ public:
/**
* Creates new sorts with the given names (all of arity 0).
*/
- const std::vector<Type>
- mkSorts(const std::vector<std::string>& names);
+ std::vector<Type> mkSorts(const std::vector<std::string>& names);
+
+ /**
+ * Create sorts of mutually-recursive datatypes.
+ */
+ std::vector<DatatypeType>
+ mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes);
/**
* Add an operator to the current legal set.
@@ -357,8 +362,8 @@ public:
/** Is the symbol bound to a boolean variable? */
bool isBoolean(const std::string& name);
- /** Is the symbol bound to a function? */
- bool isFunction(const std::string& name);
+ /** Is the symbol bound to a function (or function-like thing)? */
+ bool isFunctionLike(const std::string& name);
/** Is the symbol bound to a defined function? */
bool isDefinedFunction(const std::string& name);
diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g
index 39d834891..96ac46bf1 100644
--- a/src/parser/smt/Smt.g
+++ b/src/parser/smt/Smt.g
@@ -2,10 +2,10 @@
/*! \file Smt.g
** \verbatim
** Original author: cconway
- ** Major contributors: dejan
- ** Minor contributors (to current version): mdeters, taking
+ ** Major contributors: mdeters, dejan
+ ** Minor contributors (to current version): 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
@@ -365,7 +365,7 @@ functionSymbol[CVC4::Expr& fun]
std::string name;
}
: functionName[name,CHECK_DECLARED]
- { PARSER_STATE->checkFunction(name);
+ { PARSER_STATE->checkFunctionLike(name);
fun = PARSER_STATE->getVariable(name); }
;
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index f34279149..a5a633e48 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -2,8 +2,8 @@
/*! \file Smt2.g
** \verbatim
** Original author: cconway
- ** Major contributors: none
- ** Minor contributors (to current version): mdeters, taking
+ ** 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)
** Courant Institute of Mathematical Sciences
@@ -357,7 +357,7 @@ term[CVC4::Expr& expr]
| /* A non-built-in function application */
LPAREN_TOK
functionName[name,CHECK_DECLARED]
- { PARSER_STATE->checkFunction(name);
+ { PARSER_STATE->checkFunctionLike(name);
const bool isDefinedFunction =
PARSER_STATE->isDefinedFunction(name);
if(isDefinedFunction) {
@@ -578,7 +578,7 @@ functionSymbol[CVC4::Expr& fun]
std::string name;
}
: functionName[name,CHECK_DECLARED]
- { PARSER_STATE->checkFunction(name);
+ { PARSER_STATE->checkFunctionLike(name);
fun = PARSER_STATE->getVariable(name); }
;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback