-/********************* -*- C++ -*- */
-/** parser.cpp
+/********************* */
+/*! \file parser.cpp
+ ** \verbatim
+ ** Original author: dejan
+ ** Major contributors: cconway, mdeters
+ ** Minor contributors (to current version): bobot, ajreynol
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
+ ** Copyright (c) 2009-2012 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
- ** information.
+ ** information.\endverbatim
**
- ** Parser implementation.
+ ** \brief Parser state implementation.
+ **
+ ** Parser state implementation.
**/
#include <iostream>
#include <fstream>
+#include <sstream>
+#include <iterator>
+#include <stdint.h>
+#include <cassert>
-#include "parser.h"
-#include "util/command.h"
-#include "util/Assert.h"
-#include "parser_exception.h"
-#include "parser/antlr_parser.h"
-#include "parser/smt/generated/AntlrSmtParser.hpp"
-#include "parser/smt/generated/AntlrSmtLexer.hpp"
-#include "parser/cvc/generated/AntlrCvcParser.hpp"
-#include "parser/cvc/generated/AntlrCvcLexer.hpp"
+#include "parser/input.h"
+#include "parser/parser.h"
+#include "parser/parser_exception.h"
+#include "expr/command.h"
+#include "expr/expr.h"
+#include "expr/kind.h"
+#include "expr/type.h"
+#include "util/output.h"
+#include "options/options.h"
using namespace std;
+using namespace CVC4::kind;
namespace CVC4 {
namespace parser {
-Parser::Parser(ExprManager* em) :
- d_expr_manager(em), d_done(false) {
+Parser::Parser(ExprManager* exprManager, Input* input, bool strictMode, bool parseOnly) :
+ d_exprManager(exprManager),
+ d_input(input),
+ d_symtabAllocated(),
+ d_symtab(&d_symtabAllocated),
+ d_anonymousFunctionCount(0),
+ d_done(false),
+ d_checksEnabled(true),
+ d_strictMode(strictMode),
+ d_parseOnly(parseOnly) {
+ d_input->setParser(*this);
}
-void Parser::setDone(bool done) {
- d_done = done;
+Expr Parser::getSymbol(const std::string& name, SymbolType type) {
+ checkDeclaration(name, CHECK_DECLARED, type);
+ assert( isDeclared(name, type) );
+
+ if(type == SYM_VARIABLE) {
+ // Functions share var namespace
+ return d_symtab->lookup(name);
+ }
+
+ assert(false);//Unhandled(type);
+ return Expr();
}
-bool Parser::done() const {
- return d_done;
+
+Expr Parser::getVariable(const std::string& name) {
+ return getSymbol(name, SYM_VARIABLE);
}
-Command* SmtParser::parseNextCommand() throw (ParserException) {
- Command* cmd = 0;
- if(!done()) {
- try {
- cmd = d_antlr_parser->benchmark();
- setDone();
- } catch(antlr::ANTLRException& e) {
- setDone();
- throw ParserException(e.toString());
+Expr Parser::getFunction(const std::string& name) {
+ return getSymbol(name, SYM_VARIABLE);
+}
+
+Type Parser::getType(const std::string& var_name,
+ SymbolType type) {
+ checkDeclaration(var_name, CHECK_DECLARED, type);
+ assert( isDeclared(var_name, type) );
+ Type t = getSymbol(var_name, type).getType();
+ return t;
+}
+
+Type Parser::getSort(const std::string& name) {
+ checkDeclaration(name, CHECK_DECLARED, SYM_SORT);
+ assert( isDeclared(name, SYM_SORT) );
+ Type t = d_symtab->lookupType(name);
+ return t;
+}
+
+Type Parser::getSort(const std::string& name,
+ const std::vector<Type>& params) {
+ checkDeclaration(name, CHECK_DECLARED, SYM_SORT);
+ assert( isDeclared(name, SYM_SORT) );
+ Type t = d_symtab->lookupType(name, params);
+ return t;
+}
+
+size_t Parser::getArity(const std::string& sort_name){
+ checkDeclaration(sort_name, CHECK_DECLARED, SYM_SORT);
+ assert( isDeclared(sort_name, SYM_SORT) );
+ return d_symtab->lookupArity(sort_name);
+}
+
+/* Returns true if name is bound to a boolean variable. */
+bool Parser::isBoolean(const std::string& name) {
+ return isDeclared(name, SYM_VARIABLE) && getType(name).isBoolean();
+}
+
+/* Returns true if name is bound to a function-like thing (function,
+ * constructor, tester, or selector). */
+bool Parser::isFunctionLike(const std::string& name) {
+ if(!isDeclared(name, SYM_VARIABLE)) {
+ return false;
+ }
+ Type type = getType(name);
+ return type.isFunction() || type.isConstructor() ||
+ type.isTester() || type.isSelector();
+}
+
+/* Returns true if name is bound to a defined function. */
+bool Parser::isDefinedFunction(const std::string& name) {
+ // more permissive in type than isFunction(), because defined
+ // functions can be zero-ary and declared functions cannot.
+ return d_symtab->isBoundDefinedFunction(name);
+}
+
+/* Returns true if the Expr is a defined function. */
+bool Parser::isDefinedFunction(Expr func) {
+ // more permissive in type than isFunction(), because defined
+ // functions can be zero-ary and declared functions cannot.
+ return d_symtab->isBoundDefinedFunction(func);
+}
+
+/* Returns true if name is bound to a function returning boolean. */
+bool Parser::isPredicate(const std::string& name) {
+ return isDeclared(name, SYM_VARIABLE) && getType(name).isPredicate();
+}
+
+Expr
+Parser::mkVar(const std::string& name, const Type& type,
+ bool levelZero) {
+ Debug("parser") << "mkVar(" << name << ", " << type << ", " << levelZero << ")" << std::endl;
+ Expr expr = d_exprManager->mkVar(name, type, levelZero);
+ defineVar(name, expr, levelZero);
+ return expr;
+}
+
+Expr
+Parser::mkBoundVar(const std::string& name, const Type& type) {
+ Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl;
+ Expr expr = d_exprManager->mkBoundVar(name, type);
+ defineVar(name, expr, false);
+ return expr;
+}
+
+Expr
+Parser::mkFunction(const std::string& name, const Type& type,
+ bool levelZero) {
+ Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl;
+ Expr expr = d_exprManager->mkVar(name, type, levelZero);
+ defineFunction(name, expr, levelZero);
+ return expr;
+}
+
+Expr
+Parser::mkAnonymousFunction(const std::string& prefix, const Type& type) {
+ stringstream name;
+ name << prefix << "_anon_" << ++d_anonymousFunctionCount;
+ return mkFunction(name.str(), type);
+}
+
+std::vector<Expr>
+Parser::mkVars(const std::vector<std::string> names,
+ const Type& type,
+ bool levelZero) {
+ std::vector<Expr> vars;
+ for(unsigned i = 0; i < names.size(); ++i) {
+ vars.push_back(mkVar(names[i], type, levelZero));
+ }
+ return vars;
+}
+
+std::vector<Expr>
+Parser::mkBoundVars(const std::vector<std::string> names,
+ const Type& type) {
+ std::vector<Expr> vars;
+ for(unsigned i = 0; i < names.size(); ++i) {
+ vars.push_back(mkBoundVar(names[i], type));
+ }
+ return vars;
+}
+
+void
+Parser::defineVar(const std::string& name, const Expr& val,
+ bool levelZero) {
+ Debug("parser") << "defineVar( " << name << " := " << val << " , " << levelZero << ")" << std::endl;;
+ d_symtab->bind(name, val, levelZero);
+ assert( isDeclared(name) );
+}
+
+void
+Parser::defineFunction(const std::string& name, const Expr& val,
+ bool levelZero) {
+ d_symtab->bindDefinedFunction(name, val, levelZero);
+ assert( isDeclared(name) );
+}
+
+void
+Parser::defineType(const std::string& name, const Type& type) {
+ d_symtab->bindType(name, type);
+ assert( isDeclared(name, SYM_SORT) );
+}
+
+void
+Parser::defineType(const std::string& name,
+ const std::vector<Type>& params,
+ const Type& type) {
+ d_symtab->bindType(name, params, type);
+ assert( isDeclared(name, SYM_SORT) );
+}
+
+void
+Parser::defineParameterizedType(const std::string& name,
+ const std::vector<Type>& params,
+ const Type& type) {
+ if(Debug.isOn("parser")) {
+ Debug("parser") << "defineParameterizedType(" << name << ", " << params.size() << ", [";
+ if(params.size() > 0) {
+ copy(params.begin(), params.end() - 1,
+ ostream_iterator<Type>(Debug("parser"), ", ") );
+ Debug("parser") << params.back();
}
+ Debug("parser") << "], " << type << ")" << std::endl;
}
- return cmd;
+ defineType(name, params, type);
}
-Expr SmtParser::parseNextExpression() throw (ParserException) {
- Expr result;
- if (!done()) {
- try {
- result = d_antlr_parser->an_formula();
- } catch(antlr::ANTLRException& e) {
- setDone();
- throw ParserException(e.toString());
+SortType
+Parser::mkSort(const std::string& name) {
+ Debug("parser") << "newSort(" << name << ")" << std::endl;
+ Type type = d_exprManager->mkSort(name);
+ defineType(name, type);
+ return type;
+}
+
+SortConstructorType
+Parser::mkSortConstructor(const std::string& name, size_t arity) {
+ Debug("parser") << "newSortConstructor(" << name << ", " << arity << ")"
+ << std::endl;
+ SortConstructorType type = d_exprManager->mkSortConstructor(name, arity);
+ defineType(name, vector<Type>(arity), type);
+ return type;
+}
+
+SortType Parser::mkUnresolvedType(const std::string& name) {
+ SortType unresolved = mkSort(name);
+ d_unresolved.insert(unresolved);
+ return unresolved;
+}
+
+SortConstructorType
+Parser::mkUnresolvedTypeConstructor(const std::string& name,
+ size_t arity) {
+ SortConstructorType unresolved = mkSortConstructor(name, arity);
+ d_unresolved.insert(unresolved);
+ return unresolved;
+}
+
+SortConstructorType
+Parser::mkUnresolvedTypeConstructor(const std::string& name,
+ const std::vector<Type>& params) {
+ Debug("parser") << "newSortConstructor(P)(" << name << ", " << params.size() << ")"
+ << std::endl;
+ SortConstructorType unresolved = d_exprManager->mkSortConstructor(name, params.size());
+ defineType(name, params, unresolved);
+ Type t = getSort( name, params );
+ d_unresolved.insert(unresolved);
+ return unresolved;
+}
+
+bool Parser::isUnresolvedType(const std::string& name) {
+ if(!isDeclared(name, SYM_SORT)) {
+ return false;
+ }
+ return d_unresolved.find(getSort(name)) != d_unresolved.end();
+}
+
+std::vector<DatatypeType>
+Parser::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) {
+
+ try {
+ std::vector<DatatypeType> types =
+ d_exprManager->mkMutualDatatypeTypes(datatypes, d_unresolved);
+
+ assert(datatypes.size() == types.size());
+
+ for(unsigned i = 0; i < datatypes.size(); ++i) {
+ DatatypeType t = types[i];
+ const Datatype& dt = t.getDatatype();
+ const std::string& name = dt.getName();
+ Debug("parser-idt") << "define " << name << " as " << t << std::endl;
+ if(isDeclared(name, SYM_SORT)) {
+ throw ParserException(name + " already declared");
+ }
+ if( t.isParametric() ) {
+ std::vector< Type > paramTypes = t.getParamTypes();
+ defineType(name, paramTypes, t );
+ } else {
+ defineType(name, t);
+ }
+ for(Datatype::const_iterator j = dt.begin(),
+ j_end = dt.end();
+ j != j_end;
+ ++j) {
+ const DatatypeConstructor& ctor = *j;
+ Expr::printtypes::Scope pts(Debug("parser-idt"), true);
+ Expr constructor = ctor.getConstructor();
+ Debug("parser-idt") << "+ define " << constructor << std::endl;
+ string constructorName = ctor.getName();
+ if(isDeclared(constructorName, SYM_VARIABLE)) {
+ throw ParserException(constructorName + " already declared");
+ }
+ defineVar(constructorName, constructor);
+ Expr tester = ctor.getTester();
+ Debug("parser-idt") << "+ define " << tester << std::endl;
+ string testerName = ctor.getTesterName();
+ if(isDeclared(testerName, SYM_VARIABLE)) {
+ throw ParserException(testerName + " already declared");
+ }
+ defineVar(testerName, tester);
+ for(DatatypeConstructor::const_iterator k = ctor.begin(),
+ k_end = ctor.end();
+ k != k_end;
+ ++k) {
+ Expr selector = (*k).getSelector();
+ Debug("parser-idt") << "+++ define " << selector << std::endl;
+ string selectorName = (*k).getName();
+ if(isDeclared(selectorName, SYM_VARIABLE)) {
+ throw ParserException(selectorName + " already declared");
+ }
+ defineVar(selectorName, selector);
+ }
+ }
}
+
+ // These are no longer used, and the ExprManager would have
+ // complained of a bad substitution if anything is left unresolved.
+ // Clear out the set.
+ d_unresolved.clear();
+
+ return types;
+ } catch(IllegalArgumentException& ie) {
+ throw ParserException(ie.getMessage());
+ }
+}
+
+bool Parser::isDeclared(const std::string& name, SymbolType type) {
+ switch(type) {
+ case SYM_VARIABLE:
+ return d_symtab->isBound(name);
+ case SYM_SORT:
+ return d_symtab->isBoundType(name);
+ }
+ assert(false);//Unhandled(type);
+ return false;
+}
+
+void Parser::checkDeclaration(const std::string& varName,
+ DeclarationCheck check,
+ SymbolType type)
+ throw(ParserException) {
+ if(!d_checksEnabled) {
+ return;
+ }
+
+ switch(check) {
+ case CHECK_DECLARED:
+ if( !isDeclared(varName, type) ) {
+ parseError("Symbol " + varName + " not declared as a " +
+ (type == SYM_VARIABLE ? "variable" : "type"));
+ }
+ break;
+
+ case CHECK_UNDECLARED:
+ if( isDeclared(varName, type) ) {
+ parseError("Symbol " + varName + " previously declared as a " +
+ (type == SYM_VARIABLE ? "variable" : "type"));
+ }
+ break;
+
+ case CHECK_NONE:
+ break;
+
+ default:
+ assert(false);//Unhandled(check);
}
- return result;
}
-SmtParser::~SmtParser() {
- delete d_antlr_parser;
- delete d_antlr_lexer;
+void Parser::checkFunctionLike(const std::string& name) throw(ParserException) {
+ if(d_checksEnabled && !isFunctionLike(name)) {
+ parseError("Expecting function-like symbol, found '" + name + "'");
+ }
}
-SmtParser::SmtParser(ExprManager* em, istream& input) :
- Parser(em) {
- d_antlr_lexer = new AntlrSmtLexer(input);
- d_antlr_parser = new AntlrSmtParser(*d_antlr_lexer);
- d_antlr_parser->setExpressionManager(d_expr_manager);
+void Parser::checkArity(Kind kind, unsigned numArgs)
+ throw(ParserException) {
+ if(!d_checksEnabled) {
+ return;
+ }
+
+ unsigned min = d_exprManager->minArity(kind);
+ unsigned max = d_exprManager->maxArity(kind);
+
+ if( numArgs < min || numArgs > max ) {
+ stringstream ss;
+ ss << "Expecting ";
+ if( numArgs < min ) {
+ ss << "at least " << min << " ";
+ } else {
+ ss << "at most " << max << " ";
+ }
+ ss << "arguments for operator '" << kind << "', ";
+ ss << "found " << numArgs;
+ parseError(ss.str());
+ }
}
-SmtParser::SmtParser(ExprManager*em, const char* file_name) :
- Parser(em), d_input(file_name) {
- if(!d_input) {
- throw ParserException(string("File not found or inaccessible: ") + file_name);
+void Parser::checkOperator(Kind kind, unsigned numArgs) throw(ParserException) {
+ if( d_strictMode && d_logicOperators.find(kind) == d_logicOperators.end() ) {
+ parseError( "Operator is not defined in the current logic: " + kindToString(kind) );
}
- d_antlr_lexer = new AntlrSmtLexer(d_input);
- d_antlr_lexer->setFilename(file_name);
- d_antlr_parser = new AntlrSmtParser(*d_antlr_lexer);
- d_antlr_parser->setExpressionManager(d_expr_manager);
- d_antlr_parser->setFilename(file_name);
+ checkArity(kind, numArgs);
}
-Command* CvcParser::parseNextCommand() throw (ParserException) {
- Command* cmd = 0;
- if(!done()) {
+void Parser::addOperator(Kind kind) {
+ d_logicOperators.insert(kind);
+}
+
+void Parser::preemptCommand(Command* cmd) {
+ d_commandQueue.push_back(cmd);
+}
+
+Command* Parser::nextCommand() throw(ParserException) {
+ Debug("parser") << "nextCommand()" << std::endl;
+ Command* cmd = NULL;
+ if(!d_commandQueue.empty()) {
+ cmd = d_commandQueue.front();
+ d_commandQueue.pop_front();
+ setDone(cmd == NULL);
+ } else {
try {
- cmd = d_antlr_parser->command();
- if (cmd == 0) {
- setDone();
- cmd = new EmptyCommand("EOF");
- }
- } catch(antlr::ANTLRException& e) {
+ cmd = d_input->parseCommand();
+ d_commandQueue.push_back(cmd);
+ cmd = d_commandQueue.front();
+ d_commandQueue.pop_front();
+ setDone(cmd == NULL);
+ } catch(ParserException& e) {
+ setDone();
+ throw;
+ } catch(exception& e) {
setDone();
- throw ParserException(e.toString());
+ parseError(e.what());
}
}
+ Debug("parser") << "nextCommand() => " << cmd << std::endl;
return cmd;
}
-Expr CvcParser::parseNextExpression() throw (ParserException) {
+Expr Parser::nextExpression() throw(ParserException) {
+ Debug("parser") << "nextExpression()" << std::endl;
Expr result;
- if (!done()) {
+ if(!done()) {
try {
- result = d_antlr_parser->formula();
- } catch(antlr::ANTLRException& e) {
+ result = d_input->parseExpr();
+ setDone(result.isNull());
+ } catch(ParserException& e) {
setDone();
- throw ParserException(e.toString());
+ throw;
+ } catch(exception& e) {
+ setDone();
+ parseError(e.what());
}
}
+ Debug("parser") << "nextExpression() => " << result << std::endl;
return result;
}
-CvcParser::~CvcParser() {
- delete d_antlr_parser;
- delete d_antlr_lexer;
-}
-
-CvcParser::CvcParser(ExprManager* em, istream& input) :
- Parser(em) {
- d_antlr_lexer = new AntlrCvcLexer(input);
- d_antlr_parser = new AntlrCvcParser(*d_antlr_lexer);
- d_antlr_parser->setExpressionManager(d_expr_manager);
-}
-
-CvcParser::CvcParser(ExprManager*em, const char* file_name) :
- Parser(em), d_input(file_name) {
- if(!d_input) {
- throw ParserException(string("File not found or inaccessible: ") + file_name);
+void Parser::attributeNotSupported(const std::string& attr) {
+ if(d_attributesWarnedAbout.find(attr) == d_attributesWarnedAbout.end()) {
+ stringstream ss;
+ ss << "warning: Attribute " << attr << " not supported (ignoring this and all following uses)";
+ d_input->warning(ss.str());
+ d_attributesWarnedAbout.insert(attr);
}
- d_antlr_lexer = new AntlrCvcLexer(d_input);
- d_antlr_lexer->setFilename(file_name);
- d_antlr_parser = new AntlrCvcParser(*d_antlr_lexer);
- d_antlr_parser->setExpressionManager(d_expr_manager);
- d_antlr_parser->setFilename(file_name);
}
-
}/* CVC4::parser namespace */
}/* CVC4 namespace */
-
projects / cvc5.git / blobdiff