** \verbatim
** Original author: dejan
** Major contributors: cconway, mdeters
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): bobot, ajreynol
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011 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.\endverbatim
**
#include <iostream>
#include <fstream>
+#include <sstream>
#include <iterator>
#include <stdint.h>
+#include <cassert>
-#include "input.h"
-#include "parser.h"
-#include "parser_exception.h"
+#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 "util/options.h"
-#include "util/Assert.h"
-#include "parser/cvc/cvc_input.h"
-#include "parser/smt/smt_input.h"
+#include "options/options.h"
using namespace std;
using namespace CVC4::kind;
Parser::Parser(ExprManager* exprManager, Input* input, bool strictMode, bool parseOnly) :
d_exprManager(exprManager),
d_input(input),
- d_declScopeAllocated(),
- d_declScope(&d_declScopeAllocated),
+ d_symtabAllocated(),
+ d_symtab(&d_symtabAllocated),
d_anonymousFunctionCount(0),
d_done(false),
d_checksEnabled(true),
}
Expr Parser::getSymbol(const std::string& name, SymbolType type) {
- Assert( isDeclared(name, type) );
+ checkDeclaration(name, CHECK_DECLARED, type);
+ assert( isDeclared(name, type) );
- switch( type ) {
-
- case SYM_VARIABLE: // Functions share var namespace
- return d_declScope->lookup(name);
-
- default:
- Unhandled(type);
+ if(type == SYM_VARIABLE) {
+ // Functions share var namespace
+ return d_symtab->lookup(name);
}
+
+ assert(false);//Unhandled(type);
+ return Expr();
}
Type Parser::getType(const std::string& var_name,
SymbolType type) {
- Assert( isDeclared(var_name, 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) {
- Assert( isDeclared(name, SYM_SORT) );
- Type t = d_declScope->lookupType(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) {
- Assert( isDeclared(name, SYM_SORT) );
- Type t = d_declScope->lookupType(name, 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){
- Assert( isDeclared(sort_name, SYM_SORT) );
- return d_declScope->lookupArity(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::isDefinedFunction(const std::string& name) {
// more permissive in type than isFunction(), because defined
// functions can be zero-ary and declared functions cannot.
- return d_declScope->isBoundDefinedFunction(name);
+ 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_declScope->isBoundDefinedFunction(func);
+ return d_symtab->isBoundDefinedFunction(func);
}
/* Returns true if name is bound to a function returning boolean. */
}
Expr
-Parser::mkVar(const std::string& name, const Type& type) {
+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->mkVar(name, type);
- defineVar(name, expr);
+ Expr expr = d_exprManager->mkBoundVar(name, type);
+ defineVar(name, expr, false);
return expr;
}
Expr
-Parser::mkFunction(const std::string& name, const Type& type) {
+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);
- defineFunction(name, expr);
+ 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 << ':' << ++d_anonymousFunctionCount;
+ name << prefix << "_anon_" << ++d_anonymousFunctionCount;
return mkFunction(name.str(), type);
}
std::vector<Expr>
Parser::mkVars(const std::vector<std::string> names,
- const Type& type) {
+ 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(mkVar(names[i], type));
+ vars.push_back(mkBoundVar(names[i], type));
}
return vars;
}
void
-Parser::defineVar(const std::string& name, const Expr& val) {
- d_declScope->bind(name, val);
- Assert( isDeclared(name) );
+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) {
- d_declScope->bindDefinedFunction(name, val);
- Assert( isDeclared(name) );
+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_declScope->bindType(name, type);
- Assert( isDeclared(name, SYM_SORT) );
+ 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_declScope->bindType(name, params, type);
- Assert( isDeclared(name, SYM_SORT) );
+ d_symtab->bindType(name, params, type);
+ assert( isDeclared(name, SYM_SORT) );
}
void
return type;
}
-std::vector<SortType>
-Parser::mkSorts(const std::vector<std::string>& names) {
- std::vector<SortType> types;
- for(unsigned i = 0; i < names.size(); ++i) {
- types.push_back(mkSort(names[i]));
- }
- return types;
-}
-
SortType Parser::mkUnresolvedType(const std::string& name) {
SortType unresolved = mkSort(name);
d_unresolved.insert(unresolved);
}
SortConstructorType
-Parser::mkUnresolvedTypeConstructor(const std::string& name,
+Parser::mkUnresolvedTypeConstructor(const std::string& name,
size_t arity) {
- SortConstructorType unresolved = mkSortConstructor(name,arity);
+ SortConstructorType unresolved = mkSortConstructor(name, arity);
d_unresolved.insert(unresolved);
return unresolved;
}
SortConstructorType
-Parser::mkUnresolvedTypeConstructor(const std::string& name,
+Parser::mkUnresolvedTypeConstructor(const std::string& name,
const std::vector<Type>& params) {
Debug("parser") << "newSortConstructor(P)(" << name << ", " << params.size() << ")"
<< std::endl;
std::vector<DatatypeType>
Parser::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) {
- std::vector<DatatypeType> types =
- d_exprManager->mkMutualDatatypeTypes(datatypes, d_unresolved);
+ try {
+ std::vector<DatatypeType> types =
+ d_exprManager->mkMutualDatatypeTypes(datatypes, d_unresolved);
- Assert(datatypes.size() == types.size());
+ 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 Datatype::Constructor& ctor = *j;
- Expr::printtypes::Scope pts(Debug("parser-idt"), true);
- Expr constructor = ctor.getConstructor();
- Debug("parser-idt") << "+ define " << constructor << std::endl;
- string constructorName = constructor.toString();
- if(isDeclared(constructorName, SYM_VARIABLE)) {
- throw ParserException(constructorName + " already declared");
+ 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");
}
- defineVar(constructorName, constructor);
- Expr tester = ctor.getTester();
- Debug("parser-idt") << "+ define " << tester << std::endl;
- string testerName = tester.toString();
- if(isDeclared(testerName, SYM_VARIABLE)) {
- throw ParserException(testerName + " already declared");
+ if( t.isParametric() ) {
+ std::vector< Type > paramTypes = t.getParamTypes();
+ defineType(name, paramTypes, t );
+ } else {
+ defineType(name, t);
}
- defineVar(testerName, tester);
- for(Datatype::Constructor::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 = selector.toString();
- if(isDeclared(selectorName, SYM_VARIABLE)) {
- throw ParserException(selectorName + " already declared");
+ 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);
}
- 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();
+ // 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;
+ 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_declScope->isBound(name);
+ return d_symtab->isBound(name);
case SYM_SORT:
- return d_declScope->isBoundType(name);
- default:
- Unhandled(type);
+ return d_symtab->isBoundType(name);
}
+ assert(false);//Unhandled(type);
+ return false;
}
void Parser::checkDeclaration(const std::string& varName,
switch(check) {
case CHECK_DECLARED:
if( !isDeclared(varName, type) ) {
- parseError("Symbol " + varName + " not declared as a " + (type == SYM_VARIABLE ? "variable" : "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"));
+ parseError("Symbol " + varName + " previously declared as a " +
+ (type == SYM_VARIABLE ? "variable" : "type"));
}
break;
break;
default:
- Unhandled(check);
+ assert(false);//Unhandled(check);
}
}
if(!d_commandQueue.empty()) {
cmd = d_commandQueue.front();
d_commandQueue.pop_front();
- if(cmd == NULL) {
- setDone();
- }
+ setDone(cmd == NULL);
} else {
- if(!done()) {
- try {
- cmd = d_input->parseCommand();
- d_commandQueue.push_back(cmd);
- cmd = d_commandQueue.front();
- d_commandQueue.pop_front();
- if(cmd == NULL) {
- setDone();
- }
- } catch(ParserException& e) {
- setDone();
- throw;
- } catch(Exception& e) {
- setDone();
- stringstream ss;
- // set the language of the stream, otherwise if it contains
- // Exprs or Types it prints in the AST language
- OutputLanguage outlang =
- language::toOutputLanguage(d_input->getLanguage());
- ss << Expr::setlanguage(outlang) << e;
- parseError( ss.str() );
- }
+ try {
+ 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();
+ parseError(e.what());
}
}
Debug("parser") << "nextCommand() => " << cmd << std::endl;
if(!done()) {
try {
result = d_input->parseExpr();
- if(result.isNull()) {
- setDone();
- }
+ setDone(result.isNull());
} catch(ParserException& e) {
setDone();
throw;
- } catch(Exception& e) {
+ } catch(exception& e) {
setDone();
- stringstream ss;
- ss << e;
- parseError( ss.str() );
+ parseError(e.what());
}
}
Debug("parser") << "nextExpression() => " << result << std::endl;
return result;
}
+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);
+ }
+}
}/* CVC4::parser namespace */
}/* CVC4 namespace */
projects / cvc5.git / blobdiff