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.
25 #include "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 "util/Assert.h"
32 #include "parser/cvc/cvc_input.h"
33 #include "parser/smt/smt_input.h"
36 using namespace CVC4::kind
;
41 Parser::Parser(ExprManager
* exprManager
, Input
* input
, bool strictMode
) :
42 d_exprManager(exprManager
),
45 d_checksEnabled(true),
46 d_strictMode(strictMode
) {
47 d_input
->setParser(*this);
50 Expr
Parser::getSymbol(const std::string
& name
, SymbolType type
) {
51 Assert( isDeclared(name
, type
) );
55 case SYM_VARIABLE
: // Functions share var namespace
56 return d_declScope
.lookup(name
);
64 Expr
Parser::getVariable(const std::string
& name
) {
65 return getSymbol(name
, SYM_VARIABLE
);
69 Parser::getType(const std::string
& var_name
,
71 Assert( isDeclared(var_name
, type
) );
72 Type t
= getSymbol(var_name
,type
).getType();
76 Type
Parser::getSort(const std::string
& name
) {
77 Assert( isDeclared(name
, SYM_SORT
) );
78 Type t
= d_declScope
.lookupType(name
);
82 /* Returns true if name is bound to a boolean variable. */
83 bool Parser::isBoolean(const std::string
& name
) {
84 return isDeclared(name
, SYM_VARIABLE
) && getType(name
).isBoolean();
87 /* Returns true if name is bound to a function. */
88 bool Parser::isFunction(const std::string
& name
) {
89 return isDeclared(name
, SYM_VARIABLE
) && getType(name
).isFunction();
92 /* Returns true if name is bound to a function returning boolean. */
93 bool Parser::isPredicate(const std::string
& name
) {
94 return isDeclared(name
, SYM_VARIABLE
) && getType(name
).isPredicate();
98 Parser::mkVar(const std::string
& name
, const Type
& type
) {
99 Debug("parser") << "mkVar(" << name
<< "," << type
<< ")" << std::endl
;
100 Expr expr
= d_exprManager
->mkVar(name
, type
);
101 defineVar(name
,expr
);
105 const std::vector
<Expr
>
106 Parser::mkVars(const std::vector
<std::string
> names
,
108 std::vector
<Expr
> vars
;
109 for(unsigned i
= 0; i
< names
.size(); ++i
) {
110 vars
.push_back(mkVar(names
[i
],type
));
116 Parser::defineVar(const std::string
& name
, const Expr
& val
) {
117 d_declScope
.bind(name
,val
);
118 Assert(isDeclared(name
));
122 Parser::defineType(const std::string
& name
, const Type
& type
) {
123 d_declScope
.bindType(name
,type
);
124 Assert( isDeclared(name
, SYM_SORT
) ) ;
128 Parser::mkSort(const std::string
& name
) {
129 Debug("parser") << "newSort(" << name
<< ")" << std::endl
;
130 Type type
= d_exprManager
->mkSort(name
);
131 defineType(name
,type
);
135 const std::vector
<Type
>
136 Parser::mkSorts(const std::vector
<std::string
>& names
) {
137 std::vector
<Type
> types
;
138 for(unsigned i
= 0; i
< names
.size(); ++i
) {
139 types
.push_back(mkSort(names
[i
]));
144 bool Parser::isDeclared(const std::string
& name
, SymbolType type
) {
147 return d_declScope
.isBound(name
);
149 return d_declScope
.isBoundType(name
);
155 void Parser::checkDeclaration(const std::string
& varName
,
156 DeclarationCheck check
,
158 throw (ParserException
) {
159 if(!d_checksEnabled
) {
165 if( !isDeclared(varName
, type
) ) {
166 parseError("Symbol " + varName
+ " not declared");
170 case CHECK_UNDECLARED
:
171 if( isDeclared(varName
, type
) ) {
172 parseError("Symbol " + varName
+ " previously declared");
184 void Parser::checkFunction(const std::string
& name
)
185 throw (ParserException
) {
186 if( d_checksEnabled
&& !isFunction(name
) ) {
187 parseError("Expecting function symbol, found '" + name
+ "'");
191 void Parser::checkArity(Kind kind
, unsigned int numArgs
)
192 throw (ParserException
) {
193 if(!d_checksEnabled
) {
197 unsigned int min
= d_exprManager
->minArity(kind
);
198 unsigned int max
= d_exprManager
->maxArity(kind
);
200 if( numArgs
< min
|| numArgs
> max
) {
203 if( numArgs
< min
) {
204 ss
<< "at least " << min
<< " ";
206 ss
<< "at most " << max
<< " ";
208 ss
<< "arguments for operator '" << kind
<< "', ";
209 ss
<< "found " << numArgs
;
210 parseError(ss
.str());
214 void Parser::checkOperator(Kind kind
, unsigned int numArgs
) throw (ParserException
) {
215 if( d_strictMode
&& d_logicOperators
.find(kind
) == d_logicOperators
.end() ) {
216 parseError( "Operator is not defined in the current logic: " + kindToString(kind
) );
218 checkArity(kind
,numArgs
);
221 void Parser::addOperator(Kind kind
) {
222 d_logicOperators
.insert(kind
);
225 Command
* Parser::nextCommand() throw(ParserException
) {
226 Debug("parser") << "nextCommand()" << std::endl
;
230 cmd
= d_input
->parseCommand();
234 } catch(ParserException
& e
) {
239 Debug("parser") << "nextCommand() => " << cmd
<< std::endl
;
243 Expr
Parser::nextExpression() throw(ParserException
) {
244 Debug("parser") << "nextExpression()" << std::endl
;
248 result
= d_input
->parseExpr();
249 if(result
.isNull()) {
252 } catch(ParserException
& e
) {
257 Debug("parser") << "nextExpression() => " << result
<< std::endl
;
262 }/* CVC4::parser namespace */
263 }/* CVC4 namespace */