1 /********************* */
3 ** Original author: cconway
4 ** Major contributors: dejan, mdeters
5 ** Minor contributors (to current version): none
6 ** This file is part of the CVC4 prototype.
7 ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
8 ** Courant Institute of Mathematical Sciences
10 ** See the file COPYING in the top-level source directory for licensing
13 ** Parser state implementation.
22 #include "parser_exception.h"
23 #include "expr/command.h"
24 #include "expr/expr.h"
25 #include "expr/kind.h"
26 #include "expr/type.h"
27 #include "util/output.h"
28 #include "util/Assert.h"
29 #include "parser/cvc/cvc_input.h"
30 #include "parser/smt/smt_input.h"
33 using namespace CVC4::kind
;
38 Parser::Parser(ExprManager
* exprManager
, Input
* input
) :
39 d_exprManager(exprManager
),
42 d_checksEnabled(true),
44 d_input
->setParser(this);
47 Expr
Parser::getSymbol(const std::string
& name
, SymbolType type
) {
48 Assert( isDeclared(name
, type
) );
52 case SYM_VARIABLE
: // Functions share var namespace
53 return d_declScope
.lookup(name
);
61 Expr
Parser::getVariable(const std::string
& name
) {
62 return getSymbol(name
, SYM_VARIABLE
);
66 Parser::getType(const std::string
& var_name
,
68 Assert( isDeclared(var_name
, type
) );
69 Type t
= getSymbol(var_name
,type
).getType();
73 Type
Parser::getSort(const std::string
& name
) {
74 Assert( isDeclared(name
, SYM_SORT
) );
75 Type t
= d_declScope
.lookupType(name
);
79 /* Returns true if name is bound to a boolean variable. */
80 bool Parser::isBoolean(const std::string
& name
) {
81 return isDeclared(name
, SYM_VARIABLE
) && getType(name
).isBoolean();
84 /* Returns true if name is bound to a function. */
85 bool Parser::isFunction(const std::string
& name
) {
86 return isDeclared(name
, SYM_VARIABLE
) && getType(name
).isFunction();
89 /* Returns true if name is bound to a function returning boolean. */
90 bool Parser::isPredicate(const std::string
& name
) {
91 return isDeclared(name
, SYM_VARIABLE
) && getType(name
).isPredicate();
95 Parser::mkVar(const std::string
& name
, const Type
& type
) {
96 Debug("parser") << "mkVar(" << name
<< "," << type
<< ")" << std::endl
;
97 Expr expr
= d_exprManager
->mkVar(name
, type
);
102 const std::vector
<Expr
>
103 Parser::mkVars(const std::vector
<std::string
> names
,
105 std::vector
<Expr
> vars
;
106 for(unsigned i
= 0; i
< names
.size(); ++i
) {
107 vars
.push_back(mkVar(names
[i
],type
));
113 Parser::defineVar(const std::string
& name
, const Expr
& val
) {
114 Assert(!isDeclared(name
));
115 d_declScope
.bind(name
,val
);
116 Assert(isDeclared(name
));
120 Parser::defineType(const std::string
& name
, const Type
& type
) {
121 Assert( !isDeclared(name
, SYM_SORT
) );
122 d_declScope
.bindType(name
,type
);
123 Assert( isDeclared(name
, SYM_SORT
) ) ;
127 Parser::mkSort(const std::string
& name
) {
128 Debug("parser") << "newSort(" << name
<< ")" << std::endl
;
129 Type type
= d_exprManager
->mkSort(name
);
130 defineType(name
,type
);
134 const std::vector
<Type
>
135 Parser::mkSorts(const std::vector
<std::string
>& names
) {
136 std::vector
<Type
> types
;
137 for(unsigned i
= 0; i
< names
.size(); ++i
) {
138 types
.push_back(mkSort(names
[i
]));
143 bool Parser::isDeclared(const std::string
& name
, SymbolType type
) {
146 return d_declScope
.isBound(name
);
148 return d_declScope
.isBoundType(name
);
154 void Parser::checkDeclaration(const std::string
& varName
,
155 DeclarationCheck check
,
157 throw (ParserException
) {
158 if(!d_checksEnabled
) {
164 if( !isDeclared(varName
, type
) ) {
165 parseError("Symbol " + varName
+ " not declared");
169 case CHECK_UNDECLARED
:
170 if( isDeclared(varName
, type
) ) {
171 parseError("Symbol " + varName
+ " previously declared");
183 void Parser::checkFunction(const std::string
& name
)
184 throw (ParserException
) {
185 if( d_checksEnabled
&& !isFunction(name
) ) {
186 parseError("Expecting function symbol, found '" + name
+ "'");
190 void Parser::checkArity(Kind kind
, unsigned int numArgs
)
191 throw (ParserException
) {
192 if(!d_checksEnabled
) {
196 unsigned int min
= d_exprManager
->minArity(kind
);
197 unsigned int max
= d_exprManager
->maxArity(kind
);
199 if( numArgs
< min
|| numArgs
> max
) {
202 if( numArgs
< min
) {
203 ss
<< "at least " << min
<< " ";
205 ss
<< "at most " << max
<< " ";
207 ss
<< "arguments for operator '" << kind
<< "', ";
208 ss
<< "found " << numArgs
;
209 parseError(ss
.str());
213 void Parser::checkOperator(Kind kind
, unsigned int numArgs
) throw (ParserException
) {
214 if( d_strictMode
&& d_logicOperators
.find(kind
) == d_logicOperators
.end() ) {
215 parseError( "Operator is not defined in the current logic: " + kindToString(kind
) );
217 checkArity(kind
,numArgs
);
220 void Parser::addOperator(Kind kind
) {
221 d_logicOperators
.insert(kind
);
224 Command
* Parser::nextCommand() throw(ParserException
) {
225 Debug("parser") << "nextCommand()" << std::endl
;
229 cmd
= d_input
->parseCommand();
233 } catch(ParserException
& e
) {
238 Debug("parser") << "nextCommand() => " << cmd
<< std::endl
;
242 Expr
Parser::nextExpression() throw(ParserException
) {
243 Debug("parser") << "nextExpression()" << std::endl
;
247 result
= d_input
->parseExpr();
248 if(result
.isNull()) {
251 } catch(ParserException
& e
) {
256 Debug("parser") << "nextExpression() => " << result
<< std::endl
;
261 }/* CVC4::parser namespace */
262 }/* CVC4 namespace */