1 /********************* */
4 ** Original author: Morgan Deters
5 ** Major contributors: Christopher L. Conway
6 ** Minor contributors (to current version): Tim King, Dejan Jovanovic, Francois Bobot, Andrew Reynolds
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2013 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** information.\endverbatim
12 ** \brief Parser state implementation.
14 ** Parser state implementation.
24 #include "parser/input.h"
25 #include "parser/parser.h"
26 #include "parser/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 "options/options.h"
35 using namespace CVC4::kind
;
40 Parser::Parser(ExprManager
* exprManager
, Input
* input
, bool strictMode
, bool parseOnly
) :
41 d_exprManager(exprManager
),
44 d_symtab(&d_symtabAllocated
),
46 d_anonymousFunctionCount(0),
48 d_checksEnabled(true),
49 d_strictMode(strictMode
),
50 d_parseOnly(parseOnly
),
51 d_canIncludeFile(true) {
52 d_input
->setParser(*this);
55 Expr
Parser::getSymbol(const std::string
& name
, SymbolType type
) {
56 checkDeclaration(name
, CHECK_DECLARED
, type
);
57 assert( isDeclared(name
, type
) );
59 if(type
== SYM_VARIABLE
) {
60 // Functions share var namespace
61 return d_symtab
->lookup(name
);
64 assert(false);//Unhandled(type);
69 Expr
Parser::getVariable(const std::string
& name
) {
70 return getSymbol(name
, SYM_VARIABLE
);
73 Expr
Parser::getFunction(const std::string
& name
) {
74 return getSymbol(name
, SYM_VARIABLE
);
77 Type
Parser::getType(const std::string
& var_name
,
79 checkDeclaration(var_name
, CHECK_DECLARED
, type
);
80 assert( isDeclared(var_name
, type
) );
81 Type t
= getSymbol(var_name
, type
).getType();
85 Type
Parser::getSort(const std::string
& name
) {
86 checkDeclaration(name
, CHECK_DECLARED
, SYM_SORT
);
87 assert( isDeclared(name
, SYM_SORT
) );
88 Type t
= d_symtab
->lookupType(name
);
92 Type
Parser::getSort(const std::string
& name
,
93 const std::vector
<Type
>& params
) {
94 checkDeclaration(name
, CHECK_DECLARED
, SYM_SORT
);
95 assert( isDeclared(name
, SYM_SORT
) );
96 Type t
= d_symtab
->lookupType(name
, params
);
100 size_t Parser::getArity(const std::string
& sort_name
){
101 checkDeclaration(sort_name
, CHECK_DECLARED
, SYM_SORT
);
102 assert( isDeclared(sort_name
, SYM_SORT
) );
103 return d_symtab
->lookupArity(sort_name
);
106 /* Returns true if name is bound to a boolean variable. */
107 bool Parser::isBoolean(const std::string
& name
) {
108 return isDeclared(name
, SYM_VARIABLE
) && getType(name
).isBoolean();
111 /* Returns true if name is bound to a function-like thing (function,
112 * constructor, tester, or selector). */
113 bool Parser::isFunctionLike(const std::string
& name
) {
114 if(!isDeclared(name
, SYM_VARIABLE
)) {
117 Type type
= getType(name
);
118 return type
.isFunction() || type
.isConstructor() ||
119 type
.isTester() || type
.isSelector();
122 /* Returns true if name is bound to a defined function. */
123 bool Parser::isDefinedFunction(const std::string
& name
) {
124 // more permissive in type than isFunction(), because defined
125 // functions can be zero-ary and declared functions cannot.
126 return d_symtab
->isBoundDefinedFunction(name
);
129 /* Returns true if the Expr is a defined function. */
130 bool Parser::isDefinedFunction(Expr func
) {
131 // more permissive in type than isFunction(), because defined
132 // functions can be zero-ary and declared functions cannot.
133 return d_symtab
->isBoundDefinedFunction(func
);
136 /* Returns true if name is bound to a function returning boolean. */
137 bool Parser::isPredicate(const std::string
& name
) {
138 return isDeclared(name
, SYM_VARIABLE
) && getType(name
).isPredicate();
142 Parser::mkVar(const std::string
& name
, const Type
& type
, uint32_t flags
) {
143 Debug("parser") << "mkVar(" << name
<< ", " << type
<< ")" << std::endl
;
144 Expr expr
= d_exprManager
->mkVar(name
, type
, flags
);
145 defineVar(name
, expr
, flags
& ExprManager::VAR_FLAG_GLOBAL
);
150 Parser::mkBoundVar(const std::string
& name
, const Type
& type
) {
151 Debug("parser") << "mkVar(" << name
<< ", " << type
<< ")" << std::endl
;
152 Expr expr
= d_exprManager
->mkBoundVar(name
, type
);
153 defineVar(name
, expr
, false);
158 Parser::mkFunction(const std::string
& name
, const Type
& type
, uint32_t flags
) {
159 Debug("parser") << "mkVar(" << name
<< ", " << type
<< ")" << std::endl
;
160 Expr expr
= d_exprManager
->mkVar(name
, type
, flags
);
161 defineFunction(name
, expr
, flags
& ExprManager::VAR_FLAG_GLOBAL
);
166 Parser::mkAnonymousFunction(const std::string
& prefix
, const Type
& type
, uint32_t flags
) {
168 name
<< prefix
<< "_anon_" << ++d_anonymousFunctionCount
;
169 return d_exprManager
->mkVar(name
.str(), type
, flags
);
173 Parser::mkVars(const std::vector
<std::string
> names
, const Type
& type
, uint32_t flags
) {
174 std::vector
<Expr
> vars
;
175 for(unsigned i
= 0; i
< names
.size(); ++i
) {
176 vars
.push_back(mkVar(names
[i
], type
, flags
));
182 Parser::mkBoundVars(const std::vector
<std::string
> names
, const Type
& type
) {
183 std::vector
<Expr
> vars
;
184 for(unsigned i
= 0; i
< names
.size(); ++i
) {
185 vars
.push_back(mkBoundVar(names
[i
], type
));
191 Parser::defineVar(const std::string
& name
, const Expr
& val
, bool levelZero
) {
192 Debug("parser") << "defineVar( " << name
<< " := " << val
<< ")" << std::endl
;;
193 d_symtab
->bind(name
, val
, levelZero
);
194 assert( isDeclared(name
) );
198 Parser::defineFunction(const std::string
& name
, const Expr
& val
, bool levelZero
) {
199 d_symtab
->bindDefinedFunction(name
, val
, levelZero
);
200 assert( isDeclared(name
) );
204 Parser::defineType(const std::string
& name
, const Type
& type
) {
205 d_symtab
->bindType(name
, type
);
206 assert( isDeclared(name
, SYM_SORT
) );
210 Parser::defineType(const std::string
& name
,
211 const std::vector
<Type
>& params
,
213 d_symtab
->bindType(name
, params
, type
);
214 assert( isDeclared(name
, SYM_SORT
) );
218 Parser::defineParameterizedType(const std::string
& name
,
219 const std::vector
<Type
>& params
,
221 if(Debug
.isOn("parser")) {
222 Debug("parser") << "defineParameterizedType(" << name
<< ", " << params
.size() << ", [";
223 if(params
.size() > 0) {
224 copy(params
.begin(), params
.end() - 1,
225 ostream_iterator
<Type
>(Debug("parser"), ", ") );
226 Debug("parser") << params
.back();
228 Debug("parser") << "], " << type
<< ")" << std::endl
;
230 defineType(name
, params
, type
);
234 Parser::mkSort(const std::string
& name
) {
235 Debug("parser") << "newSort(" << name
<< ")" << std::endl
;
236 Type type
= d_exprManager
->mkSort(name
);
237 defineType(name
, type
);
242 Parser::mkSortConstructor(const std::string
& name
, size_t arity
) {
243 Debug("parser") << "newSortConstructor(" << name
<< ", " << arity
<< ")"
245 SortConstructorType type
= d_exprManager
->mkSortConstructor(name
, arity
);
246 defineType(name
, vector
<Type
>(arity
), type
);
250 SortType
Parser::mkUnresolvedType(const std::string
& name
) {
251 SortType unresolved
= mkSort(name
);
252 d_unresolved
.insert(unresolved
);
257 Parser::mkUnresolvedTypeConstructor(const std::string
& name
,
259 SortConstructorType unresolved
= mkSortConstructor(name
, arity
);
260 d_unresolved
.insert(unresolved
);
265 Parser::mkUnresolvedTypeConstructor(const std::string
& name
,
266 const std::vector
<Type
>& params
) {
267 Debug("parser") << "newSortConstructor(P)(" << name
<< ", " << params
.size() << ")"
269 SortConstructorType unresolved
= d_exprManager
->mkSortConstructor(name
, params
.size());
270 defineType(name
, params
, unresolved
);
271 Type t
= getSort( name
, params
);
272 d_unresolved
.insert(unresolved
);
276 bool Parser::isUnresolvedType(const std::string
& name
) {
277 if(!isDeclared(name
, SYM_SORT
)) {
280 return d_unresolved
.find(getSort(name
)) != d_unresolved
.end();
283 std::vector
<DatatypeType
>
284 Parser::mkMutualDatatypeTypes(const std::vector
<Datatype
>& datatypes
) {
287 std::vector
<DatatypeType
> types
=
288 d_exprManager
->mkMutualDatatypeTypes(datatypes
, d_unresolved
);
290 assert(datatypes
.size() == types
.size());
292 for(unsigned i
= 0; i
< datatypes
.size(); ++i
) {
293 DatatypeType t
= types
[i
];
294 const Datatype
& dt
= t
.getDatatype();
295 const std::string
& name
= dt
.getName();
296 Debug("parser-idt") << "define " << name
<< " as " << t
<< std::endl
;
297 if(isDeclared(name
, SYM_SORT
)) {
298 throw ParserException(name
+ " already declared");
300 if( t
.isParametric() ) {
301 std::vector
< Type
> paramTypes
= t
.getParamTypes();
302 defineType(name
, paramTypes
, t
);
306 for(Datatype::const_iterator j
= dt
.begin(),
310 const DatatypeConstructor
& ctor
= *j
;
311 Expr::printtypes::Scope
pts(Debug("parser-idt"), true);
312 Expr constructor
= ctor
.getConstructor();
313 Debug("parser-idt") << "+ define " << constructor
<< std::endl
;
314 string constructorName
= ctor
.getName();
315 if(isDeclared(constructorName
, SYM_VARIABLE
)) {
316 throw ParserException(constructorName
+ " already declared");
318 defineVar(constructorName
, constructor
);
319 Expr tester
= ctor
.getTester();
320 Debug("parser-idt") << "+ define " << tester
<< std::endl
;
321 string testerName
= ctor
.getTesterName();
322 if(isDeclared(testerName
, SYM_VARIABLE
)) {
323 throw ParserException(testerName
+ " already declared");
325 defineVar(testerName
, tester
);
326 for(DatatypeConstructor::const_iterator k
= ctor
.begin(),
330 Expr selector
= (*k
).getSelector();
331 Debug("parser-idt") << "+++ define " << selector
<< std::endl
;
332 string selectorName
= (*k
).getName();
333 if(isDeclared(selectorName
, SYM_VARIABLE
)) {
334 throw ParserException(selectorName
+ " already declared");
336 defineVar(selectorName
, selector
);
341 // These are no longer used, and the ExprManager would have
342 // complained of a bad substitution if anything is left unresolved.
343 // Clear out the set.
344 d_unresolved
.clear();
347 } catch(IllegalArgumentException
& ie
) {
348 throw ParserException(ie
.getMessage());
352 bool Parser::isDeclared(const std::string
& name
, SymbolType type
) {
355 return d_reservedSymbols
.find(name
) != d_reservedSymbols
.end() || d_symtab
->isBound(name
);
357 return d_symtab
->isBoundType(name
);
359 assert(false);//Unhandled(type);
363 void Parser::reserveSymbolAtAssertionLevel(const std::string
& varName
) {
364 checkDeclaration(varName
, CHECK_UNDECLARED
, SYM_VARIABLE
);
365 d_reservedSymbols
.insert(varName
);
368 void Parser::checkDeclaration(const std::string
& varName
,
369 DeclarationCheck check
,
372 throw(ParserException
) {
373 if(!d_checksEnabled
) {
379 if( !isDeclared(varName
, type
) ) {
380 parseError("Symbol " + varName
+ " not declared as a " +
381 (type
== SYM_VARIABLE
? "variable" : "type") +
382 (notes
.size() == 0 ? notes
: "\n" + notes
));
386 case CHECK_UNDECLARED
:
387 if( isDeclared(varName
, type
) ) {
388 parseError("Symbol " + varName
+ " previously declared as a " +
389 (type
== SYM_VARIABLE
? "variable" : "type") +
390 (notes
.size() == 0 ? notes
: "\n" + notes
));
398 assert(false);//Unhandled(check);
402 void Parser::checkFunctionLike(const std::string
& name
) throw(ParserException
) {
403 if(d_checksEnabled
&& !isFunctionLike(name
)) {
404 parseError("Expecting function-like symbol, found '" + name
+ "'");
408 void Parser::checkArity(Kind kind
, unsigned numArgs
)
409 throw(ParserException
) {
410 if(!d_checksEnabled
) {
414 unsigned min
= d_exprManager
->minArity(kind
);
415 unsigned max
= d_exprManager
->maxArity(kind
);
417 if( numArgs
< min
|| numArgs
> max
) {
420 if( numArgs
< min
) {
421 ss
<< "at least " << min
<< " ";
423 ss
<< "at most " << max
<< " ";
425 ss
<< "arguments for operator '" << kind
<< "', ";
426 ss
<< "found " << numArgs
;
427 parseError(ss
.str());
431 void Parser::checkOperator(Kind kind
, unsigned numArgs
) throw(ParserException
) {
432 if( d_strictMode
&& d_logicOperators
.find(kind
) == d_logicOperators
.end() ) {
433 parseError( "Operator is not defined in the current logic: " + kindToString(kind
) );
435 checkArity(kind
, numArgs
);
438 void Parser::addOperator(Kind kind
) {
439 d_logicOperators
.insert(kind
);
442 void Parser::preemptCommand(Command
* cmd
) {
443 d_commandQueue
.push_back(cmd
);
446 Command
* Parser::nextCommand() throw(ParserException
) {
447 Debug("parser") << "nextCommand()" << std::endl
;
449 if(!d_commandQueue
.empty()) {
450 cmd
= d_commandQueue
.front();
451 d_commandQueue
.pop_front();
452 setDone(cmd
== NULL
);
455 cmd
= d_input
->parseCommand();
456 d_commandQueue
.push_back(cmd
);
457 cmd
= d_commandQueue
.front();
458 d_commandQueue
.pop_front();
459 setDone(cmd
== NULL
);
460 } catch(ParserException
& e
) {
463 } catch(exception
& e
) {
465 parseError(e
.what());
468 Debug("parser") << "nextCommand() => " << cmd
<< std::endl
;
472 Expr
Parser::nextExpression() throw(ParserException
) {
473 Debug("parser") << "nextExpression()" << std::endl
;
477 result
= d_input
->parseExpr();
478 setDone(result
.isNull());
479 } catch(ParserException
& e
) {
482 } catch(exception
& e
) {
484 parseError(e
.what());
487 Debug("parser") << "nextExpression() => " << result
<< std::endl
;
491 void Parser::attributeNotSupported(const std::string
& attr
) {
492 if(d_attributesWarnedAbout
.find(attr
) == d_attributesWarnedAbout
.end()) {
494 ss
<< "warning: Attribute " << attr
<< " not supported (ignoring this and all following uses)";
495 d_input
->warning(ss
.str());
496 d_attributesWarnedAbout
.insert(attr
);
500 }/* CVC4::parser namespace */
501 }/* CVC4 namespace */