1 /********************* */
4 ** Original author: dejan
5 ** Major contributors: mdeters, cconway
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
9 ** Courant Institute of Mathematical Sciences
10 ** New York University
11 ** See the file COPYING in the top-level source directory for licensing
12 ** information.\endverbatim
14 ** \brief Parser state implementation.
16 ** Parser state implementation.
26 #include "parser_exception.h"
27 #include "expr/command.h"
28 #include "expr/expr.h"
29 #include "expr/kind.h"
30 #include "expr/type.h"
31 #include "util/output.h"
32 #include "util/Assert.h"
33 #include "parser/cvc/cvc_input.h"
34 #include "parser/smt/smt_input.h"
37 using namespace CVC4::kind
;
42 Parser::Parser(ExprManager
* exprManager
, Input
* input
, bool strictMode
) :
43 d_exprManager(exprManager
),
46 d_checksEnabled(true),
47 d_strictMode(strictMode
) {
48 d_input
->setParser(*this);
51 Expr
Parser::getSymbol(const std::string
& name
, SymbolType type
) {
52 Assert( isDeclared(name
, type
) );
56 case SYM_VARIABLE
: // Functions share var namespace
57 return d_declScope
.lookup(name
);
65 Expr
Parser::getVariable(const std::string
& name
) {
66 return getSymbol(name
, SYM_VARIABLE
);
69 Expr
Parser::getFunction(const std::string
& name
) {
70 return getSymbol(name
, SYM_VARIABLE
);
74 Parser::getType(const std::string
& var_name
,
76 Assert( isDeclared(var_name
, type
) );
77 Type t
= getSymbol(var_name
, type
).getType();
81 Type
Parser::getSort(const std::string
& name
) {
82 Assert( isDeclared(name
, SYM_SORT
) );
83 Type t
= d_declScope
.lookupType(name
);
87 Type
Parser::getSort(const std::string
& name
,
88 const std::vector
<Type
>& params
) {
89 Assert( isDeclared(name
, SYM_SORT
) );
90 Type t
= d_declScope
.lookupType(name
, params
);
94 /* Returns true if name is bound to a boolean variable. */
95 bool Parser::isBoolean(const std::string
& name
) {
96 return isDeclared(name
, SYM_VARIABLE
) && getType(name
).isBoolean();
99 /* Returns true if name is bound to a function. */
100 bool Parser::isFunction(const std::string
& name
) {
101 return isDeclared(name
, SYM_VARIABLE
) && getType(name
).isFunction();
104 /* Returns true if name is bound to a defined function. */
105 bool Parser::isDefinedFunction(const std::string
& name
) {
106 return isFunction(name
) && d_declScope
.isBoundDefinedFunction(name
);
109 /* Returns true if name is bound to a function returning boolean. */
110 bool Parser::isPredicate(const std::string
& name
) {
111 return isDeclared(name
, SYM_VARIABLE
) && getType(name
).isPredicate();
115 Parser::mkVar(const std::string
& name
, const Type
& type
) {
116 Debug("parser") << "mkVar(" << name
<< ", " << type
<< ")" << std::endl
;
117 Expr expr
= d_exprManager
->mkVar(name
, type
);
118 defineVar(name
, expr
);
123 Parser::mkFunction(const std::string
& name
, const Type
& type
) {
124 Debug("parser") << "mkVar(" << name
<< ", " << type
<< ")" << std::endl
;
125 Expr expr
= d_exprManager
->mkVar(name
, type
);
126 defineFunction(name
, expr
);
130 const std::vector
<Expr
>
131 Parser::mkVars(const std::vector
<std::string
> names
,
133 std::vector
<Expr
> vars
;
134 for(unsigned i
= 0; i
< names
.size(); ++i
) {
135 vars
.push_back(mkVar(names
[i
], type
));
141 Parser::defineVar(const std::string
& name
, const Expr
& val
) {
142 d_declScope
.bind(name
, val
);
143 Assert( isDeclared(name
) );
147 Parser::defineFunction(const std::string
& name
, const Expr
& val
) {
148 d_declScope
.bindDefinedFunction(name
, val
);
149 Assert( isDeclared(name
) );
153 Parser::defineType(const std::string
& name
, const Type
& type
) {
154 d_declScope
.bindType(name
, type
);
155 Assert( isDeclared(name
, SYM_SORT
) );
159 Parser::defineType(const std::string
& name
,
160 const std::vector
<Type
>& params
,
162 d_declScope
.bindType(name
, params
, type
);
163 Assert( isDeclared(name
, SYM_SORT
) );
167 Parser::defineParameterizedType(const std::string
& name
,
168 const std::vector
<Type
>& params
,
170 if(Debug
.isOn("parser")) {
171 Debug("parser") << "defineParameterizedType(" << name
<< ", " << params
.size() << ", [";
172 if(params
.size() > 0) {
173 copy(params
.begin(), params
.end() - 1,
174 ostream_iterator
<Type
>(Debug("parser"), ", ") );
175 Debug("parser") << params
.back();
177 Debug("parser") << "], " << type
<< ")" << std::endl
;
179 defineType(name
, params
, type
);
183 Parser::mkSort(const std::string
& name
) {
184 Debug("parser") << "newSort(" << name
<< ")" << std::endl
;
185 Type type
= d_exprManager
->mkSort(name
);
186 defineType(name
, type
);
191 Parser::mkSortConstructor(const std::string
& name
, size_t arity
) {
192 Debug("parser") << "newSortConstructor(" << name
<< ", " << arity
<< ")"
194 Type type
= d_exprManager
->mkSortConstructor(name
, arity
);
195 defineType(name
, vector
<Type
>(arity
), type
);
199 const std::vector
<Type
>
200 Parser::mkSorts(const std::vector
<std::string
>& names
) {
201 std::vector
<Type
> types
;
202 for(unsigned i
= 0; i
< names
.size(); ++i
) {
203 types
.push_back(mkSort(names
[i
]));
208 bool Parser::isDeclared(const std::string
& name
, SymbolType type
) {
211 return d_declScope
.isBound(name
);
213 return d_declScope
.isBoundType(name
);
219 void Parser::checkDeclaration(const std::string
& varName
,
220 DeclarationCheck check
,
222 throw (ParserException
) {
223 if(!d_checksEnabled
) {
229 if( !isDeclared(varName
, type
) ) {
230 parseError("Symbol " + varName
+ " not declared");
234 case CHECK_UNDECLARED
:
235 if( isDeclared(varName
, type
) ) {
236 parseError("Symbol " + varName
+ " previously declared");
248 void Parser::checkFunction(const std::string
& name
)
249 throw (ParserException
) {
250 if( d_checksEnabled
&& !isFunction(name
) ) {
251 parseError("Expecting function symbol, found '" + name
+ "'");
255 void Parser::checkArity(Kind kind
, unsigned int numArgs
)
256 throw (ParserException
) {
257 if(!d_checksEnabled
) {
261 unsigned int min
= d_exprManager
->minArity(kind
);
262 unsigned int max
= d_exprManager
->maxArity(kind
);
264 if( numArgs
< min
|| numArgs
> max
) {
267 if( numArgs
< min
) {
268 ss
<< "at least " << min
<< " ";
270 ss
<< "at most " << max
<< " ";
272 ss
<< "arguments for operator '" << kind
<< "', ";
273 ss
<< "found " << numArgs
;
274 parseError(ss
.str());
278 void Parser::checkOperator(Kind kind
, unsigned int numArgs
) throw (ParserException
) {
279 if( d_strictMode
&& d_logicOperators
.find(kind
) == d_logicOperators
.end() ) {
280 parseError( "Operator is not defined in the current logic: " + kindToString(kind
) );
282 checkArity(kind
, numArgs
);
285 void Parser::addOperator(Kind kind
) {
286 d_logicOperators
.insert(kind
);
289 Command
* Parser::nextCommand() throw(ParserException
) {
290 Debug("parser") << "nextCommand()" << std::endl
;
294 cmd
= d_input
->parseCommand();
298 } catch(ParserException
& e
) {
301 } catch(Exception
& e
) {
305 parseError( ss
.str() );
308 Debug("parser") << "nextCommand() => " << cmd
<< std::endl
;
312 Expr
Parser::nextExpression() throw(ParserException
) {
313 Debug("parser") << "nextExpression()" << std::endl
;
317 result
= d_input
->parseExpr();
318 if(result
.isNull()) {
321 } catch(ParserException
& e
) {
324 } catch(Exception
& e
) {
328 parseError( ss
.str() );
331 Debug("parser") << "nextExpression() => " << result
<< std::endl
;
336 }/* CVC4::parser namespace */
337 }/* CVC4 namespace */