3b7b322cac7f4db8b706e78524c8ff9fbc7cf5f3
1 /********************* */
3 ** Original author: dejan
4 ** Major contributors: mdeters, cconway
5 ** Minor contributors (to current version): none
6 ** This file is part of the CVC4 prototype.
7 ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
8 ** Courant Institute of Mathematical Sciences
10 ** See the file COPYING in the top-level source directory for licensing
13 ** Parser implementation.
21 #include "expr/command.h"
22 #include "expr/expr.h"
23 #include "expr/kind.h"
24 #include "expr/type.h"
25 #include "util/output.h"
26 #include "util/Assert.h"
27 #include "parser/parser_exception.h"
28 #include "parser/cvc/cvc_input.h"
29 #include "parser/smt/smt_input.h"
32 using namespace CVC4::kind
;
37 void Input::setDone(bool done
) {
41 bool Input::done() const {
45 Command
* Input::parseNextCommand() throw (ParserException
) {
46 Debug("parser") << "parseNextCommand()" << std::endl
;
50 cmd
= doParseCommand();
54 } catch(ParserException
& e
) {
56 throw ParserException(e
.toString());
59 Debug("parser") << "parseNextCommand() => " << cmd
<< std::endl
;
63 Expr
Input::parseNextExpression() throw (ParserException
) {
64 Debug("parser") << "parseNextExpression()" << std::endl
;
68 result
= doParseExpr();
71 } catch(ParserException
& e
) {
73 throw ParserException(e
.toString());
76 Debug("parser") << "parseNextExpression() => " << result
<< std::endl
;
83 Input::Input(ExprManager
* exprManager
, const std::string
& filename
) :
84 d_exprManager(exprManager
),
87 d_checksEnabled(true) {
90 Input
* Input::newFileParser(ExprManager
* em
, InputLanguage lang
,
91 const std::string
& filename
, bool useMmap
) {
97 parser
= new CvcInput(em
,filename
,useMmap
);
100 parser
= new SmtInput(em
,filename
,useMmap
);
111 Parser* Parser::getNewParser(ExprManager* em, InputLanguage lang,
112 istream& input, string filename) {
113 antlr::CharBuffer* inputBuffer = new CharBuffer(input);
114 return getNewParser(em, lang, inputBuffer, filename);
119 Parser* Parser::getNewParser(ExprManager* em, InputLanguage lang,
120 std::istream& input, const std::string& name) {
125 antlrLexer = new AntlrCvcLexer(*inputBuffer);
126 antlrParser = new AntlrCvcParser(*antlrLexer);
130 parser = new Smt(em,input,name);
134 Unhandled("Unknown Input language!");
140 Input
* Input::newStringParser(ExprManager
* em
, InputLanguage lang
,
141 const std::string
& input
, const std::string
& name
) {
146 parser
= new CvcInput(em
,input
,name
);
150 parser
= new SmtInput(em
,input
,name
);
159 Expr
Input::getSymbol(const std::string
& name
, SymbolType type
) {
160 Assert( isDeclared(name
, type
) );
165 case SYM_VARIABLE
: // Functions share var namespace
166 return d_varSymbolTable
.getObject(name
);
174 Expr
Input::getVariable(const std::string
& name
) {
175 return getSymbol(name
, SYM_VARIABLE
);
179 Input::getType(const std::string
& var_name
,
181 Assert( isDeclared(var_name
, type
) );
182 Type
* t
= getSymbol(var_name
,type
).getType();
186 Type
* Input::getSort(const std::string
& name
) {
187 Assert( isDeclared(name
, SYM_SORT
) );
188 Type
* t
= d_sortTable
.getObject(name
);
192 /* Returns true if name is bound to a boolean variable. */
193 bool Input::isBoolean(const std::string
& name
) {
194 return isDeclared(name
, SYM_VARIABLE
) && getType(name
)->isBoolean();
197 /* Returns true if name is bound to a function. */
198 bool Input::isFunction(const std::string
& name
) {
199 return isDeclared(name
, SYM_VARIABLE
) && getType(name
)->isFunction();
202 /* Returns true if name is bound to a function returning boolean. */
203 bool Input::isPredicate(const std::string
& name
) {
204 return isDeclared(name
, SYM_VARIABLE
) && getType(name
)->isPredicate();
208 Input::mkVar(const std::string
& name
, Type
* type
) {
209 Debug("parser") << "mkVar(" << name
<< "," << *type
<< ")" << std::endl
;
210 Expr expr
= d_exprManager
->mkVar(type
, name
);
211 defineVar(name
,expr
);
215 const std::vector
<Expr
>
216 Input::mkVars(const std::vector
<std::string
> names
,
218 std::vector
<Expr
> vars
;
219 for(unsigned i
= 0; i
< names
.size(); ++i
) {
220 vars
.push_back(mkVar(names
[i
], type
));
226 Input::defineVar(const std::string
& name
, const Expr
& val
) {
227 Assert(!isDeclared(name
));
228 d_varSymbolTable
.bindName(name
,val
);
229 Assert(isDeclared(name
));
233 Input::undefineVar(const std::string
& name
) {
234 Assert(isDeclared(name
));
235 d_varSymbolTable
.unbindName(name
);
236 Assert(!isDeclared(name
));
240 Input::setLogic(const std::string
& name
) {
241 if( name
== "QF_UF" ) {
249 Input::newSort(const std::string
& name
) {
250 Debug("parser") << "newSort(" << name
<< ")" << std::endl
;
251 Assert( !isDeclared(name
, SYM_SORT
) ) ;
252 Type
* type
= d_exprManager
->mkSort(name
);
253 d_sortTable
.bindName(name
, type
);
254 Assert( isDeclared(name
, SYM_SORT
) ) ;
258 const std::vector
<Type
*>
259 Input::newSorts(const std::vector
<std::string
>& names
) {
260 std::vector
<Type
*> types
;
261 for(unsigned i
= 0; i
< names
.size(); ++i
) {
262 types
.push_back(newSort(names
[i
]));
267 bool Input::isDeclared(const std::string
& name
, SymbolType type
) {
270 return d_varSymbolTable
.isBound(name
);
272 return d_sortTable
.isBound(name
);
278 void Input::checkDeclaration(const std::string
& varName
,
279 DeclarationCheck check
,
281 throw (ParserException
) {
282 if(!d_checksEnabled
) {
288 if( !isDeclared(varName
, type
) ) {
289 parseError("Symbol " + varName
+ " not declared");
293 case CHECK_UNDECLARED
:
294 if( isDeclared(varName
, type
) ) {
295 parseError("Symbol " + varName
+ " previously declared");
307 void Input::checkFunction(const std::string
& name
)
308 throw (ParserException
) {
309 if( d_checksEnabled
&& !isFunction(name
) ) {
310 parseError("Expecting function symbol, found '" + name
+ "'");
314 void Input::checkArity(Kind kind
, unsigned int numArgs
)
315 throw (ParserException
) {
316 if(!d_checksEnabled
) {
320 unsigned int min
= d_exprManager
->minArity(kind
);
321 unsigned int max
= d_exprManager
->maxArity(kind
);
323 if( numArgs
< min
|| numArgs
> max
) {
326 if( numArgs
< min
) {
327 ss
<< "at least " << min
<< " ";
329 ss
<< "at most " << max
<< " ";
331 ss
<< "arguments for operator '" << kind
<< "', ";
332 ss
<< "found " << numArgs
;
333 parseError(ss
.str());
337 void Input::enableChecks() {
338 d_checksEnabled
= true;
341 void Input::disableChecks() {
342 d_checksEnabled
= false;
346 }/* CVC4::parser namespace */
347 }/* CVC4 namespace */