1 /********************* */
4 ** Original author: dejan
5 ** Major contributors: cconway, mdeters
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009, 2010, 2011 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/options.h"
33 #include "util/Assert.h"
34 #include "parser/cvc/cvc_input.h"
35 #include "parser/smt/smt_input.h"
38 using namespace CVC4::kind
;
43 Parser::Parser(ExprManager
* exprManager
, Input
* input
, bool strictMode
, bool parseOnly
) :
44 d_exprManager(exprManager
),
46 d_declScopeAllocated(),
47 d_declScope(&d_declScopeAllocated
),
48 d_anonymousFunctionCount(0),
50 d_checksEnabled(true),
51 d_strictMode(strictMode
),
52 d_parseOnly(parseOnly
) {
53 d_input
->setParser(*this);
56 Expr
Parser::getSymbol(const std::string
& name
, SymbolType type
) {
57 Assert( isDeclared(name
, type
) );
61 case SYM_VARIABLE
: // Functions share var namespace
62 return d_declScope
->lookup(name
);
70 Expr
Parser::getVariable(const std::string
& name
) {
71 return getSymbol(name
, SYM_VARIABLE
);
74 Expr
Parser::getFunction(const std::string
& name
) {
75 return getSymbol(name
, SYM_VARIABLE
);
78 Type
Parser::getType(const std::string
& var_name
,
80 Assert( isDeclared(var_name
, type
) );
81 Type t
= getSymbol(var_name
, type
).getType();
85 Type
Parser::getSort(const std::string
& name
) {
86 Assert( isDeclared(name
, SYM_SORT
) );
87 Type t
= d_declScope
->lookupType(name
);
91 Type
Parser::getSort(const std::string
& name
,
92 const std::vector
<Type
>& params
) {
93 Assert( isDeclared(name
, SYM_SORT
) );
94 Type t
= d_declScope
->lookupType(name
, params
);
98 /* Returns true if name is bound to a boolean variable. */
99 bool Parser::isBoolean(const std::string
& name
) {
100 return isDeclared(name
, SYM_VARIABLE
) && getType(name
).isBoolean();
103 /* Returns true if name is bound to a function-like thing (function,
104 * constructor, tester, or selector). */
105 bool Parser::isFunctionLike(const std::string
& name
) {
106 if(!isDeclared(name
, SYM_VARIABLE
)) {
109 Type type
= getType(name
);
110 return type
.isFunction() || type
.isConstructor() ||
111 type
.isTester() || type
.isSelector();
114 /* Returns true if name is bound to a defined function. */
115 bool Parser::isDefinedFunction(const std::string
& name
) {
116 // more permissive in type than isFunction(), because defined
117 // functions can be zero-ary and declared functions cannot.
118 return d_declScope
->isBoundDefinedFunction(name
);
121 /* Returns true if the Expr is a defined function. */
122 bool Parser::isDefinedFunction(Expr func
) {
123 // more permissive in type than isFunction(), because defined
124 // functions can be zero-ary and declared functions cannot.
125 return d_declScope
->isBoundDefinedFunction(func
);
128 /* Returns true if name is bound to a function returning boolean. */
129 bool Parser::isPredicate(const std::string
& name
) {
130 return isDeclared(name
, SYM_VARIABLE
) && getType(name
).isPredicate();
134 Parser::mkVar(const std::string
& name
, const Type
& type
) {
135 Debug("parser") << "mkVar(" << name
<< ", " << type
<< ")" << std::endl
;
136 Expr expr
= d_exprManager
->mkVar(name
, type
);
137 defineVar(name
, expr
);
142 Parser::mkFunction(const std::string
& name
, const Type
& type
) {
143 Debug("parser") << "mkVar(" << name
<< ", " << type
<< ")" << std::endl
;
144 Expr expr
= d_exprManager
->mkVar(name
, type
);
145 defineFunction(name
, expr
);
150 Parser::mkAnonymousFunction(const std::string
& prefix
, const Type
& type
) {
152 name
<< prefix
<< ':' << ++d_anonymousFunctionCount
;
153 return mkFunction(name
.str(), type
);
157 Parser::mkVars(const std::vector
<std::string
> names
,
159 std::vector
<Expr
> vars
;
160 for(unsigned i
= 0; i
< names
.size(); ++i
) {
161 vars
.push_back(mkVar(names
[i
], type
));
167 Parser::defineVar(const std::string
& name
, const Expr
& val
) {
168 d_declScope
->bind(name
, val
);
169 Assert( isDeclared(name
) );
173 Parser::defineFunction(const std::string
& name
, const Expr
& val
) {
174 d_declScope
->bindDefinedFunction(name
, val
);
175 Assert( isDeclared(name
) );
179 Parser::defineType(const std::string
& name
, const Type
& type
) {
180 d_declScope
->bindType(name
, type
);
181 Assert( isDeclared(name
, SYM_SORT
) );
185 Parser::defineType(const std::string
& name
,
186 const std::vector
<Type
>& params
,
188 d_declScope
->bindType(name
, params
, type
);
189 Assert( isDeclared(name
, SYM_SORT
) );
193 Parser::defineParameterizedType(const std::string
& name
,
194 const std::vector
<Type
>& params
,
196 if(Debug
.isOn("parser")) {
197 Debug("parser") << "defineParameterizedType(" << name
<< ", " << params
.size() << ", [";
198 if(params
.size() > 0) {
199 copy(params
.begin(), params
.end() - 1,
200 ostream_iterator
<Type
>(Debug("parser"), ", ") );
201 Debug("parser") << params
.back();
203 Debug("parser") << "], " << type
<< ")" << std::endl
;
205 defineType(name
, params
, type
);
209 Parser::mkSort(const std::string
& name
) {
210 Debug("parser") << "newSort(" << name
<< ")" << std::endl
;
211 Type type
= d_exprManager
->mkSort(name
);
212 defineType(name
, type
);
217 Parser::mkSortConstructor(const std::string
& name
, size_t arity
) {
218 Debug("parser") << "newSortConstructor(" << name
<< ", " << arity
<< ")"
220 SortConstructorType type
= d_exprManager
->mkSortConstructor(name
, arity
);
221 defineType(name
, vector
<Type
>(arity
), type
);
225 std::vector
<SortType
>
226 Parser::mkSorts(const std::vector
<std::string
>& names
) {
227 std::vector
<SortType
> types
;
228 for(unsigned i
= 0; i
< names
.size(); ++i
) {
229 types
.push_back(mkSort(names
[i
]));
234 SortType
Parser::mkUnresolvedType(const std::string
& name
) {
235 SortType unresolved
= mkSort(name
);
236 d_unresolved
.insert(unresolved
);
240 bool Parser::isUnresolvedType(const std::string
& name
) {
241 if(!isDeclared(name
, SYM_SORT
)) {
244 return d_unresolved
.find(getSort(name
)) != d_unresolved
.end();
247 std::vector
<DatatypeType
>
248 Parser::mkMutualDatatypeTypes(const std::vector
<Datatype
>& datatypes
) {
250 std::vector
<DatatypeType
> types
=
251 d_exprManager
->mkMutualDatatypeTypes(datatypes
, d_unresolved
);
253 Assert(datatypes
.size() == types
.size());
255 for(unsigned i
= 0; i
< datatypes
.size(); ++i
) {
256 DatatypeType t
= types
[i
];
257 const Datatype
& dt
= t
.getDatatype();
258 const std::string
& name
= dt
.getName();
259 Debug("parser-idt") << "define " << name
<< " as " << t
<< std::endl
;
260 if(isDeclared(name
, SYM_SORT
)) {
261 throw ParserException(name
+ " already declared");
264 for(Datatype::const_iterator j
= dt
.begin(),
268 const Datatype::Constructor
& ctor
= *j
;
269 Expr::printtypes::Scope
pts(Debug("parser-idt"), true);
270 Expr constructor
= ctor
.getConstructor();
271 Debug("parser-idt") << "+ define " << constructor
<< std::endl
;
272 string constructorName
= constructor
.toString();
273 if(isDeclared(constructorName
, SYM_VARIABLE
)) {
274 throw ParserException(constructorName
+ " already declared");
276 defineVar(constructorName
, constructor
);
277 Expr tester
= ctor
.getTester();
278 Debug("parser-idt") << "+ define " << tester
<< std::endl
;
279 string testerName
= tester
.toString();
280 if(isDeclared(testerName
, SYM_VARIABLE
)) {
281 throw ParserException(testerName
+ " already declared");
283 defineVar(testerName
, tester
);
284 for(Datatype::Constructor::const_iterator k
= ctor
.begin(),
288 Expr selector
= (*k
).getSelector();
289 Debug("parser-idt") << "+++ define " << selector
<< std::endl
;
290 string selectorName
= selector
.toString();
291 if(isDeclared(selectorName
, SYM_VARIABLE
)) {
292 throw ParserException(selectorName
+ " already declared");
294 defineVar(selectorName
, selector
);
299 // These are no longer used, and the ExprManager would have
300 // complained of a bad substitution if anything is left unresolved.
301 // Clear out the set.
302 d_unresolved
.clear();
307 bool Parser::isDeclared(const std::string
& name
, SymbolType type
) {
310 return d_declScope
->isBound(name
);
312 return d_declScope
->isBoundType(name
);
318 void Parser::checkDeclaration(const std::string
& varName
,
319 DeclarationCheck check
,
321 throw(ParserException
) {
322 if(!d_checksEnabled
) {
328 if( !isDeclared(varName
, type
) ) {
329 parseError("Symbol " + varName
+ " not declared as a " + (type
== SYM_VARIABLE
? "variable" : "type"));
333 case CHECK_UNDECLARED
:
334 if( isDeclared(varName
, type
) ) {
335 parseError("Symbol " + varName
+ " previously declared as a " + (type
== SYM_VARIABLE
? "variable" : "type"));
347 void Parser::checkFunctionLike(const std::string
& name
) throw(ParserException
) {
348 if(d_checksEnabled
&& !isFunctionLike(name
)) {
349 parseError("Expecting function-like symbol, found '" + name
+ "'");
353 void Parser::checkArity(Kind kind
, unsigned numArgs
)
354 throw(ParserException
) {
355 if(!d_checksEnabled
) {
359 unsigned min
= d_exprManager
->minArity(kind
);
360 unsigned max
= d_exprManager
->maxArity(kind
);
362 if( numArgs
< min
|| numArgs
> max
) {
365 if( numArgs
< min
) {
366 ss
<< "at least " << min
<< " ";
368 ss
<< "at most " << max
<< " ";
370 ss
<< "arguments for operator '" << kind
<< "', ";
371 ss
<< "found " << numArgs
;
372 parseError(ss
.str());
376 void Parser::checkOperator(Kind kind
, unsigned numArgs
) throw(ParserException
) {
377 if( d_strictMode
&& d_logicOperators
.find(kind
) == d_logicOperators
.end() ) {
378 parseError( "Operator is not defined in the current logic: " + kindToString(kind
) );
380 checkArity(kind
, numArgs
);
383 void Parser::addOperator(Kind kind
) {
384 d_logicOperators
.insert(kind
);
387 void Parser::preemptCommand(Command
* cmd
) {
388 d_commandQueue
.push_back(cmd
);
391 Command
* Parser::nextCommand() throw(ParserException
) {
392 Debug("parser") << "nextCommand()" << std::endl
;
394 if(!d_commandQueue
.empty()) {
395 cmd
= d_commandQueue
.front();
396 d_commandQueue
.pop_front();
403 cmd
= d_input
->parseCommand();
404 d_commandQueue
.push_back(cmd
);
405 cmd
= d_commandQueue
.front();
406 d_commandQueue
.pop_front();
410 } catch(ParserException
& e
) {
413 } catch(Exception
& e
) {
416 // set the language of the stream, otherwise if it contains
417 // Exprs or Types it prints in the AST language
418 OutputLanguage outlang
=
419 language::toOutputLanguage(d_input
->getLanguage());
420 ss
<< Expr::setlanguage(outlang
) << e
;
421 parseError( ss
.str() );
425 Debug("parser") << "nextCommand() => " << cmd
<< std::endl
;
429 Expr
Parser::nextExpression() throw(ParserException
) {
430 Debug("parser") << "nextExpression()" << std::endl
;
434 result
= d_input
->parseExpr();
435 if(result
.isNull()) {
438 } catch(ParserException
& e
) {
441 } catch(Exception
& e
) {
445 parseError( ss
.str() );
448 Debug("parser") << "nextExpression() => " << result
<< std::endl
;
453 }/* CVC4::parser namespace */
454 }/* CVC4 namespace */