1 /********************* */
4 ** Original author: dejan
5 ** Major contributors: cconway, mdeters
6 ** Minor contributors (to current version): ajreynol
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.
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"
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
),
47 d_symtab(&d_symtabAllocated
),
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 checkDeclaration(name
, CHECK_DECLARED
, type
);
58 Assert( isDeclared(name
, type
) );
62 case SYM_VARIABLE
: // Functions share var namespace
63 return d_symtab
->lookup(name
);
71 Expr
Parser::getVariable(const std::string
& name
) {
72 return getSymbol(name
, SYM_VARIABLE
);
75 Expr
Parser::getFunction(const std::string
& name
) {
76 return getSymbol(name
, SYM_VARIABLE
);
79 Type
Parser::getType(const std::string
& var_name
,
81 checkDeclaration(var_name
, CHECK_DECLARED
, type
);
82 Assert( isDeclared(var_name
, type
) );
83 Type t
= getSymbol(var_name
, type
).getType();
87 Type
Parser::getSort(const std::string
& name
) {
88 checkDeclaration(name
, CHECK_DECLARED
, SYM_SORT
);
89 Assert( isDeclared(name
, SYM_SORT
) );
90 Type t
= d_symtab
->lookupType(name
);
94 Type
Parser::getSort(const std::string
& name
,
95 const std::vector
<Type
>& params
) {
96 checkDeclaration(name
, CHECK_DECLARED
, SYM_SORT
);
97 Assert( isDeclared(name
, SYM_SORT
) );
98 Type t
= d_symtab
->lookupType(name
, params
);
102 size_t Parser::getArity(const std::string
& sort_name
){
103 checkDeclaration(sort_name
, CHECK_DECLARED
, SYM_SORT
);
104 Assert( isDeclared(sort_name
, SYM_SORT
) );
105 return d_symtab
->lookupArity(sort_name
);
108 /* Returns true if name is bound to a boolean variable. */
109 bool Parser::isBoolean(const std::string
& name
) {
110 return isDeclared(name
, SYM_VARIABLE
) && getType(name
).isBoolean();
113 /* Returns true if name is bound to a function-like thing (function,
114 * constructor, tester, or selector). */
115 bool Parser::isFunctionLike(const std::string
& name
) {
116 if(!isDeclared(name
, SYM_VARIABLE
)) {
119 Type type
= getType(name
);
120 return type
.isFunction() || type
.isConstructor() ||
121 type
.isTester() || type
.isSelector();
124 /* Returns true if name is bound to a defined function. */
125 bool Parser::isDefinedFunction(const std::string
& name
) {
126 // more permissive in type than isFunction(), because defined
127 // functions can be zero-ary and declared functions cannot.
128 return d_symtab
->isBoundDefinedFunction(name
);
131 /* Returns true if the Expr is a defined function. */
132 bool Parser::isDefinedFunction(Expr func
) {
133 // more permissive in type than isFunction(), because defined
134 // functions can be zero-ary and declared functions cannot.
135 return d_symtab
->isBoundDefinedFunction(func
);
138 /* Returns true if name is bound to a function returning boolean. */
139 bool Parser::isPredicate(const std::string
& name
) {
140 return isDeclared(name
, SYM_VARIABLE
) && getType(name
).isPredicate();
144 Parser::mkVar(const std::string
& name
, const Type
& type
,
146 Debug("parser") << "mkVar(" << name
<< ", " << type
<< ")" << std::endl
;
147 Expr expr
= d_exprManager
->mkVar(name
, type
);
148 defineVar(name
, expr
, levelZero
);
153 Parser::mkBoundVar(const std::string
& name
, const Type
& type
) {
154 Debug("parser") << "mkVar(" << name
<< ", " << type
<< ")" << std::endl
;
155 Expr expr
= d_exprManager
->mkBoundVar(name
, type
);
156 defineVar(name
, expr
, false);
161 Parser::mkFunction(const std::string
& name
, const Type
& type
,
163 Debug("parser") << "mkVar(" << name
<< ", " << type
<< ")" << std::endl
;
164 Expr expr
= d_exprManager
->mkVar(name
, type
);
165 defineFunction(name
, expr
, levelZero
);
170 Parser::mkAnonymousFunction(const std::string
& prefix
, const Type
& type
) {
172 name
<< prefix
<< ':' << ++d_anonymousFunctionCount
;
173 return mkFunction(name
.str(), type
);
177 Parser::mkVars(const std::vector
<std::string
> names
,
180 std::vector
<Expr
> vars
;
181 for(unsigned i
= 0; i
< names
.size(); ++i
) {
182 vars
.push_back(mkVar(names
[i
], type
, levelZero
));
188 Parser::defineVar(const std::string
& name
, const Expr
& val
,
190 Debug("parser") << "defineVar( " << name
<< " := " << val
<< " , " << levelZero
<< ")" << std::endl
;;
191 d_symtab
->bind(name
, val
, levelZero
);
192 Assert( isDeclared(name
) );
196 Parser::defineFunction(const std::string
& name
, const Expr
& val
,
198 d_symtab
->bindDefinedFunction(name
, val
, levelZero
);
199 Assert( isDeclared(name
) );
203 Parser::defineType(const std::string
& name
, const Type
& type
) {
204 d_symtab
->bindType(name
, type
);
205 Assert( isDeclared(name
, SYM_SORT
) );
209 Parser::defineType(const std::string
& name
,
210 const std::vector
<Type
>& params
,
212 d_symtab
->bindType(name
, params
, type
);
213 Assert( isDeclared(name
, SYM_SORT
) );
217 Parser::defineParameterizedType(const std::string
& name
,
218 const std::vector
<Type
>& params
,
220 if(Debug
.isOn("parser")) {
221 Debug("parser") << "defineParameterizedType(" << name
<< ", " << params
.size() << ", [";
222 if(params
.size() > 0) {
223 copy(params
.begin(), params
.end() - 1,
224 ostream_iterator
<Type
>(Debug("parser"), ", ") );
225 Debug("parser") << params
.back();
227 Debug("parser") << "], " << type
<< ")" << std::endl
;
229 defineType(name
, params
, type
);
233 Parser::mkSort(const std::string
& name
) {
234 Debug("parser") << "newSort(" << name
<< ")" << std::endl
;
235 Type type
= d_exprManager
->mkSort(name
);
236 defineType(name
, type
);
241 Parser::mkSortConstructor(const std::string
& name
, size_t arity
) {
242 Debug("parser") << "newSortConstructor(" << name
<< ", " << arity
<< ")"
244 SortConstructorType type
= d_exprManager
->mkSortConstructor(name
, arity
);
245 defineType(name
, vector
<Type
>(arity
), type
);
249 SortType
Parser::mkUnresolvedType(const std::string
& name
) {
250 SortType unresolved
= mkSort(name
);
251 d_unresolved
.insert(unresolved
);
256 Parser::mkUnresolvedTypeConstructor(const std::string
& name
,
258 SortConstructorType unresolved
= mkSortConstructor(name
, arity
);
259 d_unresolved
.insert(unresolved
);
264 Parser::mkUnresolvedTypeConstructor(const std::string
& name
,
265 const std::vector
<Type
>& params
) {
266 Debug("parser") << "newSortConstructor(P)(" << name
<< ", " << params
.size() << ")"
268 SortConstructorType unresolved
= d_exprManager
->mkSortConstructor(name
, params
.size());
269 defineType(name
, params
, unresolved
);
270 Type t
= getSort( name
, params
);
271 d_unresolved
.insert(unresolved
);
275 bool Parser::isUnresolvedType(const std::string
& name
) {
276 if(!isDeclared(name
, SYM_SORT
)) {
279 return d_unresolved
.find(getSort(name
)) != d_unresolved
.end();
282 std::vector
<DatatypeType
>
283 Parser::mkMutualDatatypeTypes(const std::vector
<Datatype
>& datatypes
) {
285 std::vector
<DatatypeType
> types
=
286 d_exprManager
->mkMutualDatatypeTypes(datatypes
, d_unresolved
);
288 Assert(datatypes
.size() == types
.size());
290 for(unsigned i
= 0; i
< datatypes
.size(); ++i
) {
291 DatatypeType t
= types
[i
];
292 const Datatype
& dt
= t
.getDatatype();
293 const std::string
& name
= dt
.getName();
294 Debug("parser-idt") << "define " << name
<< " as " << t
<< std::endl
;
295 if(isDeclared(name
, SYM_SORT
)) {
296 throw ParserException(name
+ " already declared");
298 if( t
.isParametric() ) {
299 std::vector
< Type
> paramTypes
= t
.getParamTypes();
300 defineType(name
, paramTypes
, t
);
304 for(Datatype::const_iterator j
= dt
.begin(),
308 const DatatypeConstructor
& ctor
= *j
;
309 Expr::printtypes::Scope
pts(Debug("parser-idt"), true);
310 Expr constructor
= ctor
.getConstructor();
311 Debug("parser-idt") << "+ define " << constructor
<< std::endl
;
312 string constructorName
= ctor
.getName();
313 if(isDeclared(constructorName
, SYM_VARIABLE
)) {
314 throw ParserException(constructorName
+ " already declared");
316 defineVar(constructorName
, constructor
);
317 Expr tester
= ctor
.getTester();
318 Debug("parser-idt") << "+ define " << tester
<< std::endl
;
319 string testerName
= ctor
.getTesterName();
320 if(isDeclared(testerName
, SYM_VARIABLE
)) {
321 throw ParserException(testerName
+ " already declared");
323 defineVar(testerName
, tester
);
324 for(DatatypeConstructor::const_iterator k
= ctor
.begin(),
328 Expr selector
= (*k
).getSelector();
329 Debug("parser-idt") << "+++ define " << selector
<< std::endl
;
330 string selectorName
= (*k
).getName();
331 if(isDeclared(selectorName
, SYM_VARIABLE
)) {
332 throw ParserException(selectorName
+ " already declared");
334 defineVar(selectorName
, selector
);
339 // These are no longer used, and the ExprManager would have
340 // complained of a bad substitution if anything is left unresolved.
341 // Clear out the set.
342 d_unresolved
.clear();
347 DatatypeType
Parser::mkRecordType(const std::vector
< std::pair
<std::string
, Type
> >& typeIds
) {
348 DatatypeType
& dtt
= d_recordTypes
[typeIds
];
350 Datatype
dt("__cvc4_record");
351 Debug("datatypes") << "make new record_ctor" << std::endl
;
352 DatatypeConstructor
c("__cvc4_record_ctor");
353 for(std::vector
< std::pair
<std::string
, Type
> >::const_iterator i
= typeIds
.begin(); i
!= typeIds
.end(); ++i
) {
354 c
.addArg((*i
).first
, (*i
).second
);
356 dt
.addConstructor(c
);
357 dtt
= d_exprManager
->mkDatatypeType(dt
);
359 Debug("datatypes") << "use old record_ctor" << std::endl
;
364 DatatypeType
Parser::mkTupleType(const std::vector
<Type
>& types
) {
365 DatatypeType
& dtt
= d_tupleTypes
[types
];
367 Datatype
dt("__cvc4_tuple");
368 DatatypeConstructor
c("__cvc4_tuple_ctor");
369 for(std::vector
<Type
>::const_iterator i
= types
.begin(); i
!= types
.end(); ++i
) {
370 c
.addArg("__cvc4_tuple_stor", *i
);
372 dt
.addConstructor(c
);
373 dtt
= d_exprManager
->mkDatatypeType(dt
);
378 bool Parser::isDeclared(const std::string
& name
, SymbolType type
) {
381 return d_symtab
->isBound(name
);
383 return d_symtab
->isBoundType(name
);
389 void Parser::checkDeclaration(const std::string
& varName
,
390 DeclarationCheck check
,
392 throw(ParserException
) {
393 if(!d_checksEnabled
) {
399 if( !isDeclared(varName
, type
) ) {
400 parseError("Symbol " + varName
+ " not declared as a " +
401 (type
== SYM_VARIABLE
? "variable" : "type"));
405 case CHECK_UNDECLARED
:
406 if( isDeclared(varName
, type
) ) {
407 parseError("Symbol " + varName
+ " previously declared as a " +
408 (type
== SYM_VARIABLE
? "variable" : "type"));
420 void Parser::checkFunctionLike(const std::string
& name
) throw(ParserException
) {
421 if(d_checksEnabled
&& !isFunctionLike(name
)) {
422 parseError("Expecting function-like symbol, found '" + name
+ "'");
426 void Parser::checkArity(Kind kind
, unsigned numArgs
)
427 throw(ParserException
) {
428 if(!d_checksEnabled
) {
432 unsigned min
= d_exprManager
->minArity(kind
);
433 unsigned max
= d_exprManager
->maxArity(kind
);
435 if( numArgs
< min
|| numArgs
> max
) {
438 if( numArgs
< min
) {
439 ss
<< "at least " << min
<< " ";
441 ss
<< "at most " << max
<< " ";
443 ss
<< "arguments for operator '" << kind
<< "', ";
444 ss
<< "found " << numArgs
;
445 parseError(ss
.str());
449 void Parser::checkOperator(Kind kind
, unsigned numArgs
) throw(ParserException
) {
450 if( d_strictMode
&& d_logicOperators
.find(kind
) == d_logicOperators
.end() ) {
451 parseError( "Operator is not defined in the current logic: " + kindToString(kind
) );
453 checkArity(kind
, numArgs
);
456 void Parser::addOperator(Kind kind
) {
457 d_logicOperators
.insert(kind
);
460 void Parser::preemptCommand(Command
* cmd
) {
461 d_commandQueue
.push_back(cmd
);
464 Command
* Parser::nextCommand() throw(ParserException
) {
465 Debug("parser") << "nextCommand()" << std::endl
;
467 if(!d_commandQueue
.empty()) {
468 cmd
= d_commandQueue
.front();
469 d_commandQueue
.pop_front();
476 cmd
= d_input
->parseCommand();
477 d_commandQueue
.push_back(cmd
);
478 cmd
= d_commandQueue
.front();
479 d_commandQueue
.pop_front();
483 } catch(ParserException
& e
) {
486 } catch(Exception
& e
) {
489 // set the language of the stream, otherwise if it contains
490 // Exprs or Types it prints in the AST language
491 OutputLanguage outlang
=
492 language::toOutputLanguage(d_input
->getLanguage());
493 ss
<< Expr::setlanguage(outlang
) << e
;
494 parseError( ss
.str() );
498 Debug("parser") << "nextCommand() => " << cmd
<< std::endl
;
502 Expr
Parser::nextExpression() throw(ParserException
) {
503 Debug("parser") << "nextExpression()" << std::endl
;
507 result
= d_input
->parseExpr();
508 if(result
.isNull()) {
511 } catch(ParserException
& e
) {
514 } catch(Exception
& e
) {
518 parseError( ss
.str() );
521 Debug("parser") << "nextExpression() => " << result
<< std::endl
;
526 }/* CVC4::parser namespace */
527 }/* CVC4 namespace */