namespace CVC4 {
namespace parser {
-Parser::Parser(ExprManager* exprManager, Input* input, bool strictMode, bool parseOnly) :
- d_exprManager(exprManager),
- d_resourceManager(d_exprManager->getResourceManager()),
- d_input(input),
- d_symtabAllocated(),
- d_symtab(&d_symtabAllocated),
- d_assertionLevel(0),
- d_globalDeclarations(false),
- d_anonymousFunctionCount(0),
- d_done(false),
- d_checksEnabled(true),
- d_strictMode(strictMode),
- d_parseOnly(parseOnly),
- d_canIncludeFile(true),
- d_logicIsForced(false),
- d_forcedLogic() {
+Parser::Parser(ExprManager* exprManager, Input* input, bool strictMode,
+ bool parseOnly)
+ : d_exprManager(exprManager),
+ d_resourceManager(d_exprManager->getResourceManager()),
+ d_input(input),
+ d_symtabAllocated(),
+ d_symtab(&d_symtabAllocated),
+ d_assertionLevel(0),
+ d_globalDeclarations(false),
+ d_anonymousFunctionCount(0),
+ d_done(false),
+ d_checksEnabled(true),
+ d_strictMode(strictMode),
+ d_parseOnly(parseOnly),
+ d_canIncludeFile(true),
+ d_logicIsForced(false),
+ d_forcedLogic() {
d_input->setParser(*this);
}
Expr Parser::getSymbol(const std::string& name, SymbolType type) {
checkDeclaration(name, CHECK_DECLARED, type);
- assert( isDeclared(name, type) );
+ assert(isDeclared(name, type));
- if(type == SYM_VARIABLE) {
+ if (type == SYM_VARIABLE) {
// Functions share var namespace
return d_symtab->lookup(name);
}
- assert(false);//Unhandled(type);
+ assert(false); // Unhandled(type);
return Expr();
}
-
Expr Parser::getVariable(const std::string& name) {
return getSymbol(name, SYM_VARIABLE);
}
return getSymbol(name, SYM_VARIABLE);
}
-Type Parser::getType(const std::string& var_name,
- SymbolType type) {
+Type Parser::getType(const std::string& var_name, SymbolType type) {
checkDeclaration(var_name, CHECK_DECLARED, type);
- assert( isDeclared(var_name, 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) );
+ 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) {
+Type Parser::getSort(const std::string& name, const std::vector<Type>& params) {
checkDeclaration(name, CHECK_DECLARED, SYM_SORT);
- assert( isDeclared(name, 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){
+size_t Parser::getArity(const std::string& sort_name) {
checkDeclaration(sort_name, CHECK_DECLARED, SYM_SORT);
- assert( isDeclared(sort_name, SYM_SORT) );
+ assert(isDeclared(sort_name, SYM_SORT));
return d_symtab->lookupArity(sort_name);
}
/* 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)) {
+ if (!isDeclared(name, SYM_VARIABLE)) {
return false;
}
Type type = getType(name);
- return type.isFunction() || type.isConstructor() ||
- type.isTester() || type.isSelector();
+ return type.isFunction() || type.isConstructor() || type.isTester() ||
+ type.isSelector();
}
/* Returns true if name is bound to a defined function. */
return isDeclared(name, SYM_VARIABLE) && getType(name).isPredicate();
}
-Expr
-Parser::mkVar(const std::string& name, const Type& type, uint32_t flags) {
- if(d_globalDeclarations) {
+Expr Parser::mkVar(const std::string& name, const Type& type, uint32_t flags) {
+ if (d_globalDeclarations) {
flags |= ExprManager::VAR_FLAG_GLOBAL;
}
Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl;
return expr;
}
-Expr
-Parser::mkBoundVar(const std::string& name, const Type& type) {
+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, uint32_t flags) {
- if(d_globalDeclarations) {
+Expr Parser::mkFunction(const std::string& name, const Type& type,
+ uint32_t flags) {
+ if (d_globalDeclarations) {
flags |= ExprManager::VAR_FLAG_GLOBAL;
}
Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl;
return expr;
}
-Expr
-Parser::mkAnonymousFunction(const std::string& prefix, const Type& type, uint32_t flags) {
- if(d_globalDeclarations) {
+Expr Parser::mkAnonymousFunction(const std::string& prefix, const Type& type,
+ uint32_t flags) {
+ if (d_globalDeclarations) {
flags |= ExprManager::VAR_FLAG_GLOBAL;
}
stringstream name;
return d_exprManager->mkVar(name.str(), type, flags);
}
-std::vector<Expr>
-Parser::mkVars(const std::vector<std::string> names, const Type& type, uint32_t flags) {
- if(d_globalDeclarations) {
+std::vector<Expr> Parser::mkVars(const std::vector<std::string> names,
+ const Type& type, uint32_t flags) {
+ if (d_globalDeclarations) {
flags |= ExprManager::VAR_FLAG_GLOBAL;
}
std::vector<Expr> vars;
- for(unsigned i = 0; i < names.size(); ++i) {
+ for (unsigned i = 0; i < names.size(); ++i) {
vars.push_back(mkVar(names[i], type, flags));
}
return vars;
}
-std::vector<Expr>
-Parser::mkBoundVars(const std::vector<std::string> names, const Type& type) {
+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) {
+ 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 << ")" << std::endl;;
+void Parser::defineVar(const std::string& name, const Expr& val,
+ bool levelZero) {
+ Debug("parser") << "defineVar( " << name << " := " << val << ")" << std::endl;
d_symtab->bind(name, val, levelZero);
- assert( isDeclared(name) );
+ assert(isDeclared(name));
}
-void
-Parser::defineFunction(const std::string& name, const Expr& val, bool levelZero) {
+void Parser::defineFunction(const std::string& name, const Expr& val,
+ bool levelZero) {
d_symtab->bindDefinedFunction(name, val, levelZero);
- assert( isDeclared(name) );
+ assert(isDeclared(name));
}
-void
-Parser::defineType(const std::string& name, const Type& type) {
+void Parser::defineType(const std::string& name, const Type& type) {
d_symtab->bindType(name, type);
- assert( isDeclared(name, SYM_SORT) );
+ assert(isDeclared(name, SYM_SORT));
}
-void
-Parser::defineType(const std::string& name,
- const std::vector<Type>& params,
- const Type& type) {
+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) );
+ 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) {
+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"), ", ") );
+ ostream_iterator<Type>(Debug("parser"), ", "));
Debug("parser") << params.back();
}
Debug("parser") << "], " << type << ")" << std::endl;
defineType(name, params, type);
}
-SortType
-Parser::mkSort(const std::string& name, uint32_t flags) {
- if(d_globalDeclarations) {
+SortType Parser::mkSort(const std::string& name, uint32_t flags) {
+ if (d_globalDeclarations) {
flags |= ExprManager::VAR_FLAG_GLOBAL;
}
Debug("parser") << "newSort(" << name << ")" << std::endl;
return type;
}
-SortConstructorType
-Parser::mkSortConstructor(const std::string& name, size_t arity) {
+SortConstructorType Parser::mkSortConstructor(const std::string& name,
+ size_t arity) {
Debug("parser") << "newSortConstructor(" << name << ", " << arity << ")"
<< std::endl;
SortConstructorType type = d_exprManager->mkSortConstructor(name, arity);
return unresolved;
}
-SortConstructorType
-Parser::mkUnresolvedTypeConstructor(const std::string& name,
- size_t arity) {
+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());
+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 );
+ Type t = getSort(name, params);
d_unresolved.insert(unresolved);
return unresolved;
}
bool Parser::isUnresolvedType(const std::string& name) {
- if(!isDeclared(name, SYM_SORT)) {
+ if (!isDeclared(name, SYM_SORT)) {
return false;
}
return d_unresolved.find(getSort(name)) != d_unresolved.end();
}
-std::vector<DatatypeType>
-Parser::mkMutualDatatypeTypes(std::vector<Datatype>& datatypes) {
-
+std::vector<DatatypeType> Parser::mkMutualDatatypeTypes(
+ std::vector<Datatype>& datatypes) {
try {
std::vector<DatatypeType> types =
- d_exprManager->mkMutualDatatypeTypes(datatypes, d_unresolved);
+ d_exprManager->mkMutualDatatypeTypes(datatypes, d_unresolved);
assert(datatypes.size() == types.size());
- for(unsigned i = 0; i < datatypes.size(); ++i) {
+ 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)) {
+ if (isDeclared(name, SYM_SORT)) {
throw ParserException(name + " already declared");
}
- if( t.isParametric() ) {
- std::vector< Type > paramTypes = t.getParamTypes();
- defineType(name, paramTypes, t );
+ 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) {
+ for (Datatype::const_iterator j = dt.begin(), j_end = dt.end();
+ j != j_end; ++j) {
const DatatypeConstructor& ctor = *j;
expr::ExprPrintTypes::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)) {
+ 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)) {
+ 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) {
+ 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)) {
+ if (isDeclared(selectorName, SYM_VARIABLE)) {
throw ParserException(selectorName + " already declared");
}
defineVar(selectorName, selector);
// complained of a bad substitution if anything is left unresolved.
// Clear out the set.
d_unresolved.clear();
-
- //throw exception if any datatype is not well-founded
- for(unsigned i = 0; i < datatypes.size(); ++i) {
+
+ // throw exception if any datatype is not well-founded
+ for (unsigned i = 0; i < datatypes.size(); ++i) {
const Datatype& dt = types[i].getDatatype();
- if( !dt.isCodatatype() && !dt.isWellFounded() ){
+ if (!dt.isCodatatype() && !dt.isWellFounded()) {
throw ParserException(dt.getName() + " is not well-founded");
}
}
-
+
return types;
- } catch(IllegalArgumentException& ie) {
+ } catch (IllegalArgumentException& ie) {
throw ParserException(ie.getMessage());
}
}
bool Parser::isDeclared(const std::string& name, SymbolType type) {
- switch(type) {
- case SYM_VARIABLE:
- return d_reservedSymbols.find(name) != d_reservedSymbols.end() || d_symtab->isBound(name);
- case SYM_SORT:
- return d_symtab->isBoundType(name);
+ switch (type) {
+ case SYM_VARIABLE:
+ return d_reservedSymbols.find(name) != d_reservedSymbols.end() ||
+ d_symtab->isBound(name);
+ case SYM_SORT:
+ return d_symtab->isBoundType(name);
}
- assert(false);//Unhandled(type);
+ assert(false); // Unhandled(type);
return false;
}
}
void Parser::checkDeclaration(const std::string& varName,
- DeclarationCheck check,
- SymbolType type,
- std::string notes)
- throw(ParserException) {
- if(!d_checksEnabled) {
+ DeclarationCheck check, SymbolType type,
+ std::string notes) 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") +
- (notes.size() == 0 ? notes : "\n" + notes));
- }
- break;
+ switch (check) {
+ case CHECK_DECLARED:
+ if (!isDeclared(varName, type)) {
+ parseError("Symbol '" + varName + "' not declared as a " +
+ (type == SYM_VARIABLE ? "variable" : "type") +
+ (notes.size() == 0 ? notes : "\n" + notes));
+ }
+ break;
- case CHECK_UNDECLARED:
- if( isDeclared(varName, type) ) {
- parseError("Symbol '" + varName + "' previously declared as a " +
- (type == SYM_VARIABLE ? "variable" : "type") +
- (notes.size() == 0 ? notes : "\n" + notes));
- }
- break;
+ case CHECK_UNDECLARED:
+ if (isDeclared(varName, type)) {
+ parseError("Symbol '" + varName + "' previously declared as a " +
+ (type == SYM_VARIABLE ? "variable" : "type") +
+ (notes.size() == 0 ? notes : "\n" + notes));
+ }
+ break;
- case CHECK_NONE:
- break;
+ case CHECK_NONE:
+ break;
- default:
- assert(false);//Unhandled(check);
+ default:
+ assert(false); // Unhandled(check);
}
}
void Parser::checkFunctionLike(const std::string& name) throw(ParserException) {
- if(d_checksEnabled && !isFunctionLike(name)) {
+ if (d_checksEnabled && !isFunctionLike(name)) {
parseError("Expecting function-like symbol, found '" + name + "'");
}
}
-void Parser::checkArity(Kind kind, unsigned numArgs)
- throw(ParserException) {
- if(!d_checksEnabled) {
+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 ) {
+ if (numArgs < min || numArgs > max) {
stringstream ss;
ss << "Expecting ";
- if( numArgs < min ) {
+ if (numArgs < min) {
ss << "at least " << min << " ";
} else {
ss << "at most " << max << " ";
}
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) );
+ if (d_strictMode && d_logicOperators.find(kind) == d_logicOperators.end()) {
+ parseError("Operator is not defined in the current logic: " +
+ kindToString(kind));
}
checkArity(kind, numArgs);
}
-void Parser::addOperator(Kind kind) {
- d_logicOperators.insert(kind);
-}
+void Parser::addOperator(Kind kind) { d_logicOperators.insert(kind); }
-void Parser::preemptCommand(Command* cmd) {
- d_commandQueue.push_back(cmd);
-}
+void Parser::preemptCommand(Command* cmd) { d_commandQueue.push_back(cmd); }
-Command* Parser::nextCommand() throw(ParserException, UnsafeInterruptException) {
+Command* Parser::nextCommand() throw(ParserException,
+ UnsafeInterruptException) {
Debug("parser") << "nextCommand()" << std::endl;
Command* cmd = NULL;
- if(!d_commandQueue.empty()) {
+ if (!d_commandQueue.empty()) {
cmd = d_commandQueue.front();
d_commandQueue.pop_front();
setDone(cmd == NULL);
cmd = d_commandQueue.front();
d_commandQueue.pop_front();
setDone(cmd == NULL);
- } catch(ParserException& e) {
+ } catch (ParserException& e) {
setDone();
throw;
- } catch(exception& e) {
+ } catch (exception& e) {
setDone();
parseError(e.what());
}
}
Debug("parser") << "nextCommand() => " << cmd << std::endl;
- if (cmd != NULL &&
- dynamic_cast<SetOptionCommand*>(cmd) == NULL &&
- dynamic_cast<QuitCommand*>(cmd) == NULL)
- {
+ if (cmd != NULL && dynamic_cast<SetOptionCommand*>(cmd) == NULL &&
+ dynamic_cast<QuitCommand*>(cmd) == NULL) {
// don't count set-option commands as to not get stuck in an infinite
// loop of resourcing out
const Options& options = d_exprManager->getOptions();
const Options& options = d_exprManager->getOptions();
d_resourceManager->spendResource(options.getParseStep());
Expr result;
- if(!done()) {
+ if (!done()) {
try {
result = d_input->parseExpr();
setDone(result.isNull());
- } catch(ParserException& e) {
+ } catch (ParserException& e) {
setDone();
throw;
- } catch(exception& e) {
+ } catch (exception& e) {
setDone();
parseError(e.what());
}
}
void Parser::attributeNotSupported(const std::string& attr) {
- if(d_attributesWarnedAbout.find(attr) == d_attributesWarnedAbout.end()) {
+ if (d_attributesWarnedAbout.find(attr) == d_attributesWarnedAbout.end()) {
stringstream ss;
- ss << "warning: Attribute '" << attr << "' not supported (ignoring this and all following uses)";
+ 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 */
+} /* CVC4::parser namespace */
+} /* CVC4 namespace */
projects / cvc5.git / commitdiff