1 /********************* */
4 ** Original author: dejan
5 ** Major contributors: cconway, mdeters
6 ** Minor contributors (to current version): bobot, ajreynol
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009-2012 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.
23 #include "parser/input.h"
24 #include "parser/parser.h"
25 #include "parser/parser_exception.h"
26 #include "expr/command.h"
27 #include "expr/expr.h"
28 #include "expr/kind.h"
29 #include "expr/type.h"
30 #include "util/output.h"
31 #include "options/options.h"
34 using namespace CVC4::kind
;
39 Parser::Parser(ExprManager
* exprManager
, Input
* input
, bool strictMode
, bool parseOnly
) :
40 d_exprManager(exprManager
),
43 d_symtab(&d_symtabAllocated
),
44 d_anonymousFunctionCount(0),
46 d_checksEnabled(true),
47 d_strictMode(strictMode
),
48 d_parseOnly(parseOnly
) {
49 d_input
->setParser(*this);
52 Expr
Parser::getSymbol(const std::string
& name
, SymbolType type
) {
53 checkDeclaration(name
, CHECK_DECLARED
, type
);
54 assert( isDeclared(name
, type
) );
56 if(type
== SYM_VARIABLE
) {
57 // Functions share var namespace
58 return d_symtab
->lookup(name
);
61 assert(false);//Unhandled(type);
66 Expr
Parser::getVariable(const std::string
& name
) {
67 return getSymbol(name
, SYM_VARIABLE
);
70 Expr
Parser::getFunction(const std::string
& name
) {
71 return getSymbol(name
, SYM_VARIABLE
);
74 Type
Parser::getType(const std::string
& var_name
,
76 checkDeclaration(var_name
, CHECK_DECLARED
, type
);
77 assert( isDeclared(var_name
, type
) );
78 Type t
= getSymbol(var_name
, type
).getType();
82 Type
Parser::getSort(const std::string
& name
) {
83 checkDeclaration(name
, CHECK_DECLARED
, SYM_SORT
);
84 assert( isDeclared(name
, SYM_SORT
) );
85 Type t
= d_symtab
->lookupType(name
);
89 Type
Parser::getSort(const std::string
& name
,
90 const std::vector
<Type
>& params
) {
91 checkDeclaration(name
, CHECK_DECLARED
, SYM_SORT
);
92 assert( isDeclared(name
, SYM_SORT
) );
93 Type t
= d_symtab
->lookupType(name
, params
);
97 size_t Parser::getArity(const std::string
& sort_name
){
98 checkDeclaration(sort_name
, CHECK_DECLARED
, SYM_SORT
);
99 assert( isDeclared(sort_name
, SYM_SORT
) );
100 return d_symtab
->lookupArity(sort_name
);
103 /* Returns true if name is bound to a boolean variable. */
104 bool Parser::isBoolean(const std::string
& name
) {
105 return isDeclared(name
, SYM_VARIABLE
) && getType(name
).isBoolean();
108 /* Returns true if name is bound to a function-like thing (function,
109 * constructor, tester, or selector). */
110 bool Parser::isFunctionLike(const std::string
& name
) {
111 if(!isDeclared(name
, SYM_VARIABLE
)) {
114 Type type
= getType(name
);
115 return type
.isFunction() || type
.isConstructor() ||
116 type
.isTester() || type
.isSelector();
119 /* Returns true if name is bound to a defined function. */
120 bool Parser::isDefinedFunction(const std::string
& name
) {
121 // more permissive in type than isFunction(), because defined
122 // functions can be zero-ary and declared functions cannot.
123 return d_symtab
->isBoundDefinedFunction(name
);
126 /* Returns true if the Expr is a defined function. */
127 bool Parser::isDefinedFunction(Expr func
) {
128 // more permissive in type than isFunction(), because defined
129 // functions can be zero-ary and declared functions cannot.
130 return d_symtab
->isBoundDefinedFunction(func
);
133 /* Returns true if name is bound to a function returning boolean. */
134 bool Parser::isPredicate(const std::string
& name
) {
135 return isDeclared(name
, SYM_VARIABLE
) && getType(name
).isPredicate();
139 Parser::mkVar(const std::string
& name
, const Type
& type
,
141 Debug("parser") << "mkVar(" << name
<< ", " << type
<< ", " << levelZero
<< ")" << std::endl
;
142 Expr expr
= d_exprManager
->mkVar(name
, type
, levelZero
);
143 defineVar(name
, expr
, levelZero
);
148 Parser::mkBoundVar(const std::string
& name
, const Type
& type
) {
149 Debug("parser") << "mkVar(" << name
<< ", " << type
<< ")" << std::endl
;
150 Expr expr
= d_exprManager
->mkBoundVar(name
, type
);
151 defineVar(name
, expr
, false);
156 Parser::mkFunction(const std::string
& name
, const Type
& type
,
158 Debug("parser") << "mkVar(" << name
<< ", " << type
<< ")" << std::endl
;
159 Expr expr
= d_exprManager
->mkVar(name
, type
, levelZero
);
160 defineFunction(name
, expr
, levelZero
);
165 Parser::mkAnonymousFunction(const std::string
& prefix
, const Type
& type
) {
167 name
<< prefix
<< "_anon_" << ++d_anonymousFunctionCount
;
168 return mkFunction(name
.str(), type
);
172 Parser::mkVars(const std::vector
<std::string
> names
,
175 std::vector
<Expr
> vars
;
176 for(unsigned i
= 0; i
< names
.size(); ++i
) {
177 vars
.push_back(mkVar(names
[i
], type
, levelZero
));
183 Parser::defineVar(const std::string
& name
, const Expr
& val
,
185 Debug("parser") << "defineVar( " << name
<< " := " << val
<< " , " << levelZero
<< ")" << std::endl
;;
186 d_symtab
->bind(name
, val
, levelZero
);
187 assert( isDeclared(name
) );
191 Parser::defineFunction(const std::string
& name
, const Expr
& val
,
193 d_symtab
->bindDefinedFunction(name
, val
, levelZero
);
194 assert( isDeclared(name
) );
198 Parser::defineType(const std::string
& name
, const Type
& type
) {
199 d_symtab
->bindType(name
, type
);
200 assert( isDeclared(name
, SYM_SORT
) );
204 Parser::defineType(const std::string
& name
,
205 const std::vector
<Type
>& params
,
207 d_symtab
->bindType(name
, params
, type
);
208 assert( isDeclared(name
, SYM_SORT
) );
212 Parser::defineParameterizedType(const std::string
& name
,
213 const std::vector
<Type
>& params
,
215 if(Debug
.isOn("parser")) {
216 Debug("parser") << "defineParameterizedType(" << name
<< ", " << params
.size() << ", [";
217 if(params
.size() > 0) {
218 copy(params
.begin(), params
.end() - 1,
219 ostream_iterator
<Type
>(Debug("parser"), ", ") );
220 Debug("parser") << params
.back();
222 Debug("parser") << "], " << type
<< ")" << std::endl
;
224 defineType(name
, params
, type
);
228 Parser::mkSort(const std::string
& name
) {
229 Debug("parser") << "newSort(" << name
<< ")" << std::endl
;
230 Type type
= d_exprManager
->mkSort(name
);
231 defineType(name
, type
);
236 Parser::mkSortConstructor(const std::string
& name
, size_t arity
) {
237 Debug("parser") << "newSortConstructor(" << name
<< ", " << arity
<< ")"
239 SortConstructorType type
= d_exprManager
->mkSortConstructor(name
, arity
);
240 defineType(name
, vector
<Type
>(arity
), type
);
244 SortType
Parser::mkUnresolvedType(const std::string
& name
) {
245 SortType unresolved
= mkSort(name
);
246 d_unresolved
.insert(unresolved
);
251 Parser::mkUnresolvedTypeConstructor(const std::string
& name
,
253 SortConstructorType unresolved
= mkSortConstructor(name
, arity
);
254 d_unresolved
.insert(unresolved
);
259 Parser::mkUnresolvedTypeConstructor(const std::string
& name
,
260 const std::vector
<Type
>& params
) {
261 Debug("parser") << "newSortConstructor(P)(" << name
<< ", " << params
.size() << ")"
263 SortConstructorType unresolved
= d_exprManager
->mkSortConstructor(name
, params
.size());
264 defineType(name
, params
, unresolved
);
265 Type t
= getSort( name
, params
);
266 d_unresolved
.insert(unresolved
);
270 bool Parser::isUnresolvedType(const std::string
& name
) {
271 if(!isDeclared(name
, SYM_SORT
)) {
274 return d_unresolved
.find(getSort(name
)) != d_unresolved
.end();
277 std::vector
<DatatypeType
>
278 Parser::mkMutualDatatypeTypes(const std::vector
<Datatype
>& datatypes
) {
280 std::vector
<DatatypeType
> types
=
281 d_exprManager
->mkMutualDatatypeTypes(datatypes
, d_unresolved
);
283 assert(datatypes
.size() == types
.size());
285 for(unsigned i
= 0; i
< datatypes
.size(); ++i
) {
286 DatatypeType t
= types
[i
];
287 const Datatype
& dt
= t
.getDatatype();
288 const std::string
& name
= dt
.getName();
289 Debug("parser-idt") << "define " << name
<< " as " << t
<< std::endl
;
290 if(isDeclared(name
, SYM_SORT
)) {
291 throw ParserException(name
+ " already declared");
293 if( t
.isParametric() ) {
294 std::vector
< Type
> paramTypes
= t
.getParamTypes();
295 defineType(name
, paramTypes
, t
);
299 for(Datatype::const_iterator j
= dt
.begin(),
303 const DatatypeConstructor
& ctor
= *j
;
304 Expr::printtypes::Scope
pts(Debug("parser-idt"), true);
305 Expr constructor
= ctor
.getConstructor();
306 Debug("parser-idt") << "+ define " << constructor
<< std::endl
;
307 string constructorName
= ctor
.getName();
308 if(isDeclared(constructorName
, SYM_VARIABLE
)) {
309 throw ParserException(constructorName
+ " already declared");
311 defineVar(constructorName
, constructor
);
312 Expr tester
= ctor
.getTester();
313 Debug("parser-idt") << "+ define " << tester
<< std::endl
;
314 string testerName
= ctor
.getTesterName();
315 if(isDeclared(testerName
, SYM_VARIABLE
)) {
316 throw ParserException(testerName
+ " already declared");
318 defineVar(testerName
, tester
);
319 for(DatatypeConstructor::const_iterator k
= ctor
.begin(),
323 Expr selector
= (*k
).getSelector();
324 Debug("parser-idt") << "+++ define " << selector
<< std::endl
;
325 string selectorName
= (*k
).getName();
326 if(isDeclared(selectorName
, SYM_VARIABLE
)) {
327 throw ParserException(selectorName
+ " already declared");
329 defineVar(selectorName
, selector
);
334 // These are no longer used, and the ExprManager would have
335 // complained of a bad substitution if anything is left unresolved.
336 // Clear out the set.
337 d_unresolved
.clear();
342 bool Parser::isDeclared(const std::string
& name
, SymbolType type
) {
345 return d_symtab
->isBound(name
);
347 return d_symtab
->isBoundType(name
);
349 assert(false);//Unhandled(type);
353 void Parser::checkDeclaration(const std::string
& varName
,
354 DeclarationCheck check
,
356 throw(ParserException
) {
357 if(!d_checksEnabled
) {
363 if( !isDeclared(varName
, type
) ) {
364 parseError("Symbol " + varName
+ " not declared as a " +
365 (type
== SYM_VARIABLE
? "variable" : "type"));
369 case CHECK_UNDECLARED
:
370 if( isDeclared(varName
, type
) ) {
371 parseError("Symbol " + varName
+ " previously declared as a " +
372 (type
== SYM_VARIABLE
? "variable" : "type"));
380 assert(false);//Unhandled(check);
384 void Parser::checkFunctionLike(const std::string
& name
) throw(ParserException
) {
385 if(d_checksEnabled
&& !isFunctionLike(name
)) {
386 parseError("Expecting function-like symbol, found '" + name
+ "'");
390 void Parser::checkArity(Kind kind
, unsigned numArgs
)
391 throw(ParserException
) {
392 if(!d_checksEnabled
) {
396 unsigned min
= d_exprManager
->minArity(kind
);
397 unsigned max
= d_exprManager
->maxArity(kind
);
399 if( numArgs
< min
|| numArgs
> max
) {
402 if( numArgs
< min
) {
403 ss
<< "at least " << min
<< " ";
405 ss
<< "at most " << max
<< " ";
407 ss
<< "arguments for operator '" << kind
<< "', ";
408 ss
<< "found " << numArgs
;
409 parseError(ss
.str());
413 void Parser::checkOperator(Kind kind
, unsigned numArgs
) throw(ParserException
) {
414 if( d_strictMode
&& d_logicOperators
.find(kind
) == d_logicOperators
.end() ) {
415 parseError( "Operator is not defined in the current logic: " + kindToString(kind
) );
417 checkArity(kind
, numArgs
);
420 void Parser::addOperator(Kind kind
) {
421 d_logicOperators
.insert(kind
);
424 void Parser::preemptCommand(Command
* cmd
) {
425 d_commandQueue
.push_back(cmd
);
428 Command
* Parser::nextCommand() throw(ParserException
) {
429 Debug("parser") << "nextCommand()" << std::endl
;
431 if(!d_commandQueue
.empty()) {
432 cmd
= d_commandQueue
.front();
433 d_commandQueue
.pop_front();
440 cmd
= d_input
->parseCommand();
441 d_commandQueue
.push_back(cmd
);
442 cmd
= d_commandQueue
.front();
443 d_commandQueue
.pop_front();
447 } catch(ParserException
& e
) {
450 } catch(Exception
& e
) {
453 // set the language of the stream, otherwise if it contains
454 // Exprs or Types it prints in the AST language
455 OutputLanguage outlang
=
456 language::toOutputLanguage(d_input
->getLanguage());
457 ss
<< Expr::setlanguage(outlang
) << e
;
458 parseError( ss
.str() );
462 Debug("parser") << "nextCommand() => " << cmd
<< std::endl
;
466 Expr
Parser::nextExpression() throw(ParserException
) {
467 Debug("parser") << "nextExpression()" << std::endl
;
471 result
= d_input
->parseExpr();
472 if(result
.isNull()) {
475 } catch(ParserException
& e
) {
478 } catch(Exception
& e
) {
482 parseError( ss
.str() );
485 Debug("parser") << "nextExpression() => " << result
<< std::endl
;
490 }/* CVC4::parser namespace */
491 }/* CVC4 namespace */