diff options
Diffstat (limited to 'src/parser/parser.cpp')
| -rw-r--r-- | src/parser/parser.cpp | 323 |
1 files changed, 173 insertions, 150 deletions
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index eae9636a2..55a52e8d6 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -83,7 +83,8 @@ ExprManager* Parser::getExprManager() const api::Solver* Parser::getSolver() const { return d_solver; } -Expr Parser::getSymbol(const std::string& name, SymbolType type) { +api::Term Parser::getSymbol(const std::string& name, SymbolType type) +{ checkDeclaration(name, CHECK_DECLARED, type); assert(isDeclared(name, type)); @@ -96,23 +97,28 @@ Expr Parser::getSymbol(const std::string& name, SymbolType type) { return Expr(); } -Expr Parser::getVariable(const std::string& name) { +api::Term Parser::getVariable(const std::string& name) +{ return getSymbol(name, SYM_VARIABLE); } -Expr Parser::getFunction(const std::string& name) { +api::Term Parser::getFunction(const std::string& name) +{ return getSymbol(name, SYM_VARIABLE); } -Expr Parser::getExpressionForName(const std::string& name) { - Type t; +api::Term Parser::getExpressionForName(const std::string& name) +{ + api::Sort t; return getExpressionForNameAndType(name, t); } -Expr Parser::getExpressionForNameAndType(const std::string& name, Type t) { +api::Term Parser::getExpressionForNameAndType(const std::string& name, + api::Sort t) +{ assert(isDeclared(name)); // first check if the variable is declared and not overloaded - Expr expr = getVariable(name); + api::Term expr = getVariable(name); if(expr.isNull()) { // the variable is overloaded, try with type if the type exists if(!t.isNull()) { @@ -128,47 +134,52 @@ Expr Parser::getExpressionForNameAndType(const std::string& name, Type t) { } // now, post-process the expression assert( !expr.isNull() ); - Type te = expr.getType(); - if (te.isConstructor() && ConstructorType(te).getArity() == 0) + api::Sort te = expr.getSort(); + if (te.isConstructor() && te.getConstructorArity() == 0) { // nullary constructors have APPLY_CONSTRUCTOR kind with no children - expr = getExprManager()->mkExpr(CVC4::kind::APPLY_CONSTRUCTOR, expr); + expr = d_solver->mkTerm(api::APPLY_CONSTRUCTOR, expr); } return expr; } -Kind Parser::getKindForFunction(Expr fun) { - Type t = fun.getType(); +api::Kind Parser::getKindForFunction(api::Term fun) +{ + api::Sort t = fun.getSort(); if (t.isFunction()) { - return APPLY_UF; + return api::APPLY_UF; } else if (t.isConstructor()) { - return APPLY_CONSTRUCTOR; + return api::APPLY_CONSTRUCTOR; } else if (t.isSelector()) { - return APPLY_SELECTOR; + return api::APPLY_SELECTOR; } else if (t.isTester()) { - return APPLY_TESTER; + return api::APPLY_TESTER; } - return UNDEFINED_KIND; + return api::UNDEFINED_KIND; } -Type Parser::getSort(const std::string& name) { +api::Sort Parser::getSort(const std::string& name) +{ checkDeclaration(name, CHECK_DECLARED, SYM_SORT); assert(isDeclared(name, SYM_SORT)); - Type t = d_symtab->lookupType(name); + api::Sort t = api::Sort(d_symtab->lookupType(name)); return t; } -Type Parser::getSort(const std::string& name, const std::vector<Type>& params) { +api::Sort Parser::getSort(const std::string& name, + const std::vector<api::Sort>& params) +{ checkDeclaration(name, CHECK_DECLARED, SYM_SORT); assert(isDeclared(name, SYM_SORT)); - Type t = d_symtab->lookupType(name, params); + api::Sort t = + api::Sort(d_symtab->lookupType(name, api::sortVectorToTypes(params))); return t; } @@ -180,122 +191,142 @@ size_t Parser::getArity(const std::string& sort_name) { /* Returns true if name is bound to a boolean variable. */ bool Parser::isBoolean(const std::string& name) { - Expr expr = getVariable(name); - return !expr.isNull() && expr.getType().isBoolean(); + api::Term expr = getVariable(name); + return !expr.isNull() && expr.getSort().isBoolean(); } -bool Parser::isFunctionLike(Expr fun) { +bool Parser::isFunctionLike(api::Term fun) +{ if(fun.isNull()) { return false; } - Type type = fun.getType(); + api::Sort type = fun.getSort(); return type.isFunction() || type.isConstructor() || type.isTester() || type.isSelector(); } /* Returns true if name is bound to a function returning boolean. */ bool Parser::isPredicate(const std::string& name) { - Expr expr = getVariable(name); - return !expr.isNull() && expr.getType().isPredicate(); + api::Term expr = getVariable(name); + return !expr.isNull() && expr.getSort().isPredicate(); } -Expr Parser::mkVar(const std::string& name, const Type& type, uint32_t flags, bool doOverload) { +api::Term Parser::bindVar(const std::string& name, + const api::Sort& type, + uint32_t flags, + bool doOverload) +{ if (d_globalDeclarations) { flags |= ExprManager::VAR_FLAG_GLOBAL; } - Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl; - Expr expr = getExprManager()->mkVar(name, type, flags); + Debug("parser") << "bindVar(" << name << ", " << type << ")" << std::endl; + api::Term expr = mkVar(name, type, flags); defineVar(name, expr, flags & ExprManager::VAR_FLAG_GLOBAL, doOverload); return expr; } -Expr Parser::mkBoundVar(const std::string& name, const Type& type) { - Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl; - Expr expr = getExprManager()->mkBoundVar(name, type); +api::Term Parser::bindBoundVar(const std::string& name, const api::Sort& type) +{ + Debug("parser") << "bindBoundVar(" << name << ", " << type << ")" + << std::endl; + api::Term expr = d_solver->mkVar(type, name); defineVar(name, expr, false); return expr; } -std::vector<Expr> Parser::mkBoundVars( - std::vector<std::pair<std::string, Type> >& sortedVarNames) +std::vector<api::Term> Parser::bindBoundVars( + std::vector<std::pair<std::string, api::Sort> >& sortedVarNames) { - std::vector<Expr> vars; - for (std::pair<std::string, CVC4::Type>& i : sortedVarNames) + std::vector<api::Term> vars; + for (std::pair<std::string, api::Sort>& i : sortedVarNames) { - vars.push_back(mkBoundVar(i.first, i.second)); + vars.push_back(bindBoundVar(i.first, i.second.getType())); } return vars; } -Expr Parser::mkAnonymousFunction(const std::string& prefix, const Type& type, - uint32_t flags) { +api::Term Parser::mkAnonymousFunction(const std::string& prefix, + const api::Sort& type, + uint32_t flags) +{ if (d_globalDeclarations) { flags |= ExprManager::VAR_FLAG_GLOBAL; } stringstream name; name << prefix << "_anon_" << ++d_anonymousFunctionCount; - return getExprManager()->mkVar(name.str(), type, flags); + return mkVar(name.str(), type.getType(), flags); } -std::vector<Expr> Parser::mkVars(const std::vector<std::string> names, - const Type& type, uint32_t flags, bool doOverload) { +std::vector<api::Term> Parser::bindVars(const std::vector<std::string> names, + const api::Sort& type, + uint32_t flags, + bool doOverload) +{ if (d_globalDeclarations) { flags |= ExprManager::VAR_FLAG_GLOBAL; } - std::vector<Expr> vars; + std::vector<api::Term> vars; for (unsigned i = 0; i < names.size(); ++i) { - vars.push_back(mkVar(names[i], type, flags, doOverload)); + vars.push_back(bindVar(names[i], type, flags, doOverload)); } return vars; } -std::vector<Expr> Parser::mkBoundVars(const std::vector<std::string> names, - const Type& type) { - std::vector<Expr> vars; +std::vector<api::Term> Parser::bindBoundVars( + const std::vector<std::string> names, const api::Sort& type) +{ + std::vector<api::Term> vars; for (unsigned i = 0; i < names.size(); ++i) { - vars.push_back(mkBoundVar(names[i], type)); + vars.push_back(bindBoundVar(names[i], type)); } return vars; } -void Parser::defineVar(const std::string& name, const Expr& val, - bool levelZero, bool doOverload) { +void Parser::defineVar(const std::string& name, + const api::Term& val, + bool levelZero, + bool doOverload) +{ Debug("parser") << "defineVar( " << name << " := " << val << ")" << std::endl; - if (!d_symtab->bind(name, val, levelZero, doOverload)) { + if (!d_symtab->bind(name, val.getExpr(), levelZero, doOverload)) + { std::stringstream ss; - ss << "Cannot bind " << name << " to symbol of type " << val.getType(); + ss << "Cannot bind " << name << " to symbol of type " << val.getSort(); ss << ", maybe the symbol has already been defined?"; - parseError(ss.str()); + parseError(ss.str()); } assert(isDeclared(name)); } void Parser::defineType(const std::string& name, - const Type& type, + const api::Sort& type, bool levelZero) { - d_symtab->bindType(name, type, levelZero); + d_symtab->bindType(name, type.getType(), levelZero); assert(isDeclared(name, SYM_SORT)); } void Parser::defineType(const std::string& name, - const std::vector<Type>& params, - const Type& type, + const std::vector<api::Sort>& params, + const api::Sort& type, bool levelZero) { - d_symtab->bindType(name, params, type, levelZero); + d_symtab->bindType( + name, api::sortVectorToTypes(params), type.getType(), levelZero); assert(isDeclared(name, SYM_SORT)); } void Parser::defineParameterizedType(const std::string& name, - const std::vector<Type>& params, - const Type& type) { + const std::vector<api::Sort>& params, + const api::Sort& 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"), ", ")); + copy(params.begin(), + params.end() - 1, + ostream_iterator<api::Sort>(Debug("parser"), ", ")); Debug("parser") << params.back(); } Debug("parser") << "], " << type << ")" << std::endl; @@ -303,9 +334,10 @@ void Parser::defineParameterizedType(const std::string& name, defineType(name, params, type); } -SortType Parser::mkSort(const std::string& name, uint32_t flags) { +api::Sort Parser::mkSort(const std::string& name, uint32_t flags) +{ Debug("parser") << "newSort(" << name << ")" << std::endl; - Type type = getExprManager()->mkSort(name, flags); + api::Sort type = getExprManager()->mkSort(name, flags); defineType( name, type, @@ -313,44 +345,46 @@ SortType Parser::mkSort(const std::string& name, uint32_t flags) { return type; } -SortConstructorType Parser::mkSortConstructor(const std::string& name, - size_t arity, - uint32_t flags) +api::Sort Parser::mkSortConstructor(const std::string& name, + size_t arity, + uint32_t flags) { Debug("parser") << "newSortConstructor(" << name << ", " << arity << ")" << std::endl; - SortConstructorType type = - getExprManager()->mkSortConstructor(name, arity, flags); + api::Sort type = getExprManager()->mkSortConstructor(name, arity, flags); defineType( name, - vector<Type>(arity), + vector<api::Sort>(arity), type, d_globalDeclarations && !(flags & ExprManager::SORT_FLAG_PLACEHOLDER)); return type; } -SortType Parser::mkUnresolvedType(const std::string& name) { - SortType unresolved = mkSort(name, ExprManager::SORT_FLAG_PLACEHOLDER); +api::Sort Parser::mkUnresolvedType(const std::string& name) +{ + api::Sort unresolved = mkSort(name, ExprManager::SORT_FLAG_PLACEHOLDER); d_unresolved.insert(unresolved); return unresolved; } -SortConstructorType Parser::mkUnresolvedTypeConstructor(const std::string& name, - size_t arity) { - SortConstructorType unresolved = +api::Sort Parser::mkUnresolvedTypeConstructor(const std::string& name, + size_t arity) +{ + api::Sort unresolved = mkSortConstructor(name, arity, ExprManager::SORT_FLAG_PLACEHOLDER); d_unresolved.insert(unresolved); return unresolved; } -SortConstructorType Parser::mkUnresolvedTypeConstructor( - const std::string& name, const std::vector<Type>& params) { +api::Sort Parser::mkUnresolvedTypeConstructor( + const std::string& name, const std::vector<api::Sort>& params) +{ Debug("parser") << "newSortConstructor(P)(" << name << ", " << params.size() << ")" << std::endl; - SortConstructorType unresolved = getExprManager()->mkSortConstructor( + api::Sort unresolved = getExprManager()->mkSortConstructor( name, params.size(), ExprManager::SORT_FLAG_PLACEHOLDER); defineType(name, params, unresolved); - Type t = getSort(name, params); + api::Sort t = getSort(name, params); d_unresolved.insert(unresolved); return unresolved; } @@ -366,32 +400,41 @@ std::vector<DatatypeType> Parser::mkMutualDatatypeTypes( std::vector<Datatype>& datatypes, bool doOverload, uint32_t flags) { try { - std::vector<DatatypeType> types = - getExprManager()->mkMutualDatatypeTypes(datatypes, d_unresolved, flags); + std::set<Type> tset = api::sortSetToTypes(d_unresolved); + std::vector<DatatypeType> dtypes = + getExprManager()->mkMutualDatatypeTypes(datatypes, tset, flags); + std::vector<api::Sort> types; + for (unsigned i = 0, dtsize = dtypes.size(); i < dtsize; i++) + { + types.push_back(api::Sort(dtypes[i])); + } assert(datatypes.size() == types.size()); for (unsigned i = 0; i < datatypes.size(); ++i) { - DatatypeType t = types[i]; - const Datatype& dt = t.getDatatype(); + api::Sort t = types[i]; + const api::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(); + if (t.isParametricDatatype()) + { + std::vector<api::Sort> paramTypes = t.getDatatypeParamSorts(); defineType(name, paramTypes, t, d_globalDeclarations); - } else { + } + else + { defineType(name, t, d_globalDeclarations); } std::unordered_set< std::string > consNames; std::unordered_set< std::string > selNames; - for (Datatype::const_iterator j = dt.begin(), j_end = dt.end(); - j != j_end; ++j) { - const DatatypeConstructor& ctor = *j; + for (size_t j = 0, ncons = dt.getNumConstructors(); j < ncons; j++) + { + const api::DatatypeConstructor& ctor = dt[j]; expr::ExprPrintTypes::Scope pts(Debug("parser-idt"), true); - Expr constructor = ctor.getConstructor(); + api::Term constructor = ctor.getConstructorTerm(); Debug("parser-idt") << "+ define " << constructor << std::endl; string constructorName = ctor.getName(); if(consNames.find(constructorName)==consNames.end()) { @@ -404,19 +447,19 @@ std::vector<DatatypeType> Parser::mkMutualDatatypeTypes( }else{ throw ParserException(constructorName + " already declared in this datatype"); } - Expr tester = ctor.getTester(); + api::Term tester = ctor.getTesterTerm(); Debug("parser-idt") << "+ define " << tester << std::endl; string testerName = ctor.getTesterName(); if(!doOverload) { checkDeclaration(testerName, CHECK_UNDECLARED); } defineVar(testerName, tester, d_globalDeclarations, doOverload); - for (DatatypeConstructor::const_iterator k = ctor.begin(), - k_end = ctor.end(); - k != k_end; ++k) { - Expr selector = (*k).getSelector(); + for (size_t k = 0, nargs = ctor.getNumSelectors(); k < nargs; k++) + { + const api::DatatypeSelector& sel = ctor[k]; + api::Term selector = sel.getSelectorTerm(); Debug("parser-idt") << "+++ define " << selector << std::endl; - string selectorName = (*k).getName(); + string selectorName = sel.getName(); if(selNames.find(selectorName)==selNames.end()) { if(!doOverload) { checkDeclaration(selectorName, CHECK_UNDECLARED); @@ -437,45 +480,49 @@ std::vector<DatatypeType> Parser::mkMutualDatatypeTypes( // throw exception if any datatype is not well-founded for (unsigned i = 0; i < datatypes.size(); ++i) { - const Datatype& dt = types[i].getDatatype(); + const api::Datatype& dt = types[i].getDatatype(); if (!dt.isCodatatype() && !dt.isWellFounded()) { throw ParserException(dt.getName() + " is not well-founded"); } } - - return types; + std::vector<DatatypeType> retTypes; + for (unsigned i = 0, ntypes = types.size(); i < ntypes; i++) + { + retTypes.push_back(DatatypeType(types[i].getType())); + } + return retTypes; } catch (IllegalArgumentException& ie) { throw ParserException(ie.getMessage()); } } -Type Parser::mkFlatFunctionType(std::vector<Type>& sorts, - Type range, - std::vector<Expr>& flattenVars) +api::Sort Parser::mkFlatFunctionType(std::vector<api::Sort>& sorts, + api::Sort range, + std::vector<api::Term>& flattenVars) { if (range.isFunction()) { - std::vector<Type> domainTypes = - (static_cast<FunctionType>(range)).getArgTypes(); + std::vector<api::Sort> domainTypes = range.getFunctionDomainSorts(); for (unsigned i = 0, size = domainTypes.size(); i < size; i++) { sorts.push_back(domainTypes[i]); // the introduced variable is internal (not parsable) std::stringstream ss; ss << "__flatten_var_" << i; - Expr v = getExprManager()->mkBoundVar(ss.str(), domainTypes[i]); + api::Term v = d_solver->mkVar(domainTypes[i], ss.str()); flattenVars.push_back(v); } - range = static_cast<FunctionType>(range).getRangeType(); + range = range.getFunctionCodomainSort(); } if (sorts.empty()) { return range; } - return getExprManager()->mkFunctionType(sorts, range); + return d_solver->mkFunctionSort(sorts, range); } -Type Parser::mkFlatFunctionType(std::vector<Type>& sorts, Type range) +api::Sort Parser::mkFlatFunctionType(std::vector<api::Sort>& sorts, + api::Sort range) { if (sorts.empty()) { @@ -485,7 +532,7 @@ Type Parser::mkFlatFunctionType(std::vector<Type>& sorts, Type range) if (Debug.isOn("parser")) { Debug("parser") << "mkFlatFunctionType: range " << range << " and domains "; - for (Type t : sorts) + for (api::Sort t : sorts) { Debug("parser") << " " << t; } @@ -493,19 +540,18 @@ Type Parser::mkFlatFunctionType(std::vector<Type>& sorts, Type range) } while (range.isFunction()) { - std::vector<Type> domainTypes = - static_cast<FunctionType>(range).getArgTypes(); + std::vector<api::Sort> domainTypes = range.getFunctionDomainSorts(); sorts.insert(sorts.end(), domainTypes.begin(), domainTypes.end()); - range = static_cast<FunctionType>(range).getRangeType(); + range = range.getFunctionCodomainSort(); } - return getExprManager()->mkFunctionType(sorts, range); + return d_solver->mkFunctionSort(sorts, range); } -Expr Parser::mkHoApply(Expr expr, std::vector<Expr>& args) +api::Term Parser::mkHoApply(api::Term expr, const std::vector<api::Term>& args) { for (unsigned i = 0; i < args.size(); i++) { - expr = getExprManager()->mkExpr(HO_APPLY, expr, args[i]); + expr = d_solver->mkTerm(api::HO_APPLY, expr, args[i]); } return expr; } @@ -581,6 +627,15 @@ api::Term Parser::applyTypeAscription(api::Term t, api::Sort s) return t; } +//!!!!!!!!!!! temporary +api::Term Parser::mkVar(const std::string& name, + const api::Sort& type, + uint32_t flags) +{ + return api::Term(getExprManager()->mkVar(name, type.getType(), flags)); +} +//!!!!!!!!!!! temporary + bool Parser::isDeclared(const std::string& name, SymbolType type) { switch (type) { case SYM_VARIABLE: @@ -632,7 +687,7 @@ void Parser::checkDeclaration(const std::string& varName, } } -void Parser::checkFunctionLike(Expr fun) +void Parser::checkFunctionLike(api::Term fun) { if (d_checksEnabled && !isFunctionLike(fun)) { stringstream ss; @@ -643,39 +698,7 @@ void Parser::checkFunctionLike(Expr fun) } } -void Parser::checkArity(Kind kind, unsigned numArgs) -{ - if (!d_checksEnabled) { - return; - } - - unsigned min = getExprManager()->minArity(kind); - unsigned max = getExprManager()->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()); - } -} - -void Parser::checkOperator(Kind kind, unsigned numArgs) -{ - 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(api::Kind kind) { d_logicOperators.insert(kind); } void Parser::preemptCommand(Command* cmd) { d_commandQueue.push_back(cmd); } Command* Parser::nextCommand() |