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 // more permissive in type than isFunction(), because defined
107 // functions can be zero-ary and declared functions cannot.
108 return d_declScope
.isBoundDefinedFunction(name
);
111 /* Returns true if name is bound to a function returning boolean. */
112 bool Parser::isPredicate(const std::string
& name
) {
113 return isDeclared(name
, SYM_VARIABLE
) && getType(name
).isPredicate();
117 Parser::mkVar(const std::string
& name
, const Type
& type
) {
118 Debug("parser") << "mkVar(" << name
<< ", " << type
<< ")" << std::endl
;
119 Expr expr
= d_exprManager
->mkVar(name
, type
);
120 defineVar(name
, expr
);
125 Parser::mkFunction(const std::string
& name
, const Type
& type
) {
126 Debug("parser") << "mkVar(" << name
<< ", " << type
<< ")" << std::endl
;
127 Expr expr
= d_exprManager
->mkVar(name
, type
);
128 defineFunction(name
, expr
);
132 const std::vector
<Expr
>
133 Parser::mkVars(const std::vector
<std::string
> names
,
135 std::vector
<Expr
> vars
;
136 for(unsigned i
= 0; i
< names
.size(); ++i
) {
137 vars
.push_back(mkVar(names
[i
], type
));
143 Parser::defineVar(const std::string
& name
, const Expr
& val
) {
144 d_declScope
.bind(name
, val
);
145 Assert( isDeclared(name
) );
149 Parser::defineFunction(const std::string
& name
, const Expr
& val
) {
150 d_declScope
.bindDefinedFunction(name
, val
);
151 Assert( isDeclared(name
) );
155 Parser::defineType(const std::string
& name
, const Type
& type
) {
156 d_declScope
.bindType(name
, type
);
157 Assert( isDeclared(name
, SYM_SORT
) );
161 Parser::defineType(const std::string
& name
,
162 const std::vector
<Type
>& params
,
164 d_declScope
.bindType(name
, params
, type
);
165 Assert( isDeclared(name
, SYM_SORT
) );
169 Parser::defineParameterizedType(const std::string
& name
,
170 const std::vector
<Type
>& params
,
172 if(Debug
.isOn("parser")) {
173 Debug("parser") << "defineParameterizedType(" << name
<< ", " << params
.size() << ", [";
174 if(params
.size() > 0) {
175 copy(params
.begin(), params
.end() - 1,
176 ostream_iterator
<Type
>(Debug("parser"), ", ") );
177 Debug("parser") << params
.back();
179 Debug("parser") << "], " << type
<< ")" << std::endl
;
181 defineType(name
, params
, type
);
185 Parser::mkSort(const std::string
& name
) {
186 Debug("parser") << "newSort(" << name
<< ")" << std::endl
;
187 Type type
= d_exprManager
->mkSort(name
);
188 defineType(name
, type
);
193 Parser::mkSortConstructor(const std::string
& name
, size_t arity
) {
194 Debug("parser") << "newSortConstructor(" << name
<< ", " << arity
<< ")"
196 Type type
= d_exprManager
->mkSortConstructor(name
, arity
);
197 defineType(name
, vector
<Type
>(arity
), type
);
201 const std::vector
<Type
>
202 Parser::mkSorts(const std::vector
<std::string
>& names
) {
203 std::vector
<Type
> types
;
204 for(unsigned i
= 0; i
< names
.size(); ++i
) {
205 types
.push_back(mkSort(names
[i
]));
210 bool Parser::isDeclared(const std::string
& name
, SymbolType type
) {
213 return d_declScope
.isBound(name
);
215 return d_declScope
.isBoundType(name
);
221 void Parser::checkDeclaration(const std::string
& varName
,
222 DeclarationCheck check
,
224 throw (ParserException
) {
225 if(!d_checksEnabled
) {
231 if( !isDeclared(varName
, type
) ) {
232 parseError("Symbol " + varName
+ " not declared");
236 case CHECK_UNDECLARED
:
237 if( isDeclared(varName
, type
) ) {
238 parseError("Symbol " + varName
+ " previously declared");
250 void Parser::checkFunction(const std::string
& name
)
251 throw (ParserException
) {
252 if( d_checksEnabled
&& !isFunction(name
) ) {
253 parseError("Expecting function symbol, found '" + name
+ "'");
257 void Parser::checkArity(Kind kind
, unsigned int numArgs
)
258 throw (ParserException
) {
259 if(!d_checksEnabled
) {
263 unsigned int min
= d_exprManager
->minArity(kind
);
264 unsigned int max
= d_exprManager
->maxArity(kind
);
266 if( numArgs
< min
|| numArgs
> max
) {
269 if( numArgs
< min
) {
270 ss
<< "at least " << min
<< " ";
272 ss
<< "at most " << max
<< " ";
274 ss
<< "arguments for operator '" << kind
<< "', ";
275 ss
<< "found " << numArgs
;
276 parseError(ss
.str());
280 void Parser::checkOperator(Kind kind
, unsigned int numArgs
) throw (ParserException
) {
281 if( d_strictMode
&& d_logicOperators
.find(kind
) == d_logicOperators
.end() ) {
282 parseError( "Operator is not defined in the current logic: " + kindToString(kind
) );
284 checkArity(kind
, numArgs
);
287 void Parser::addOperator(Kind kind
) {
288 d_logicOperators
.insert(kind
);
291 void Parser::preemptCommand(Command
* cmd
) {
292 d_commandQueue
.push_back(cmd
);
295 Command
* Parser::nextCommand() throw(ParserException
) {
296 Debug("parser") << "nextCommand()" << std::endl
;
298 if(!d_commandQueue
.empty()) {
299 cmd
= d_commandQueue
.front();
300 d_commandQueue
.pop_front();
307 cmd
= d_input
->parseCommand();
308 d_commandQueue
.push_back(cmd
);
309 cmd
= d_commandQueue
.front();
310 d_commandQueue
.pop_front();
314 } catch(ParserException
& e
) {
317 } catch(Exception
& e
) {
321 parseError( ss
.str() );
325 Debug("parser") << "nextCommand() => " << cmd
<< std::endl
;
329 Expr
Parser::nextExpression() throw(ParserException
) {
330 Debug("parser") << "nextExpression()" << std::endl
;
334 result
= d_input
->parseExpr();
335 if(result
.isNull()) {
338 } catch(ParserException
& e
) {
341 } catch(Exception
& e
) {
345 parseError( ss
.str() );
348 Debug("parser") << "nextExpression() => " << result
<< std::endl
;
353 }/* CVC4::parser namespace */
354 }/* CVC4 namespace */