diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2020-06-02 09:09:15 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-06-02 09:09:15 -0700 |
commit | 50edf184492d20f4acb7b8d82f3843f3146f77d5 (patch) | |
tree | 2a1bbdbd59dc7aefca114b108c646eb6f2dd933e /src/parser/parser.cpp | |
parent | b826fc8ae95fc13c4e2be45e39961199392a4dda (diff) |
New C++ API: Keep reference to solver object in non-solver objects. (#4549)
This is in preparation for adding guards to ensure that sort and term
arguments belong to the same solver.
Diffstat (limited to 'src/parser/parser.cpp')
-rw-r--r-- | src/parser/parser.cpp | 55 |
1 files changed, 28 insertions, 27 deletions
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index c860d14c7..b24f9ae9d 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -82,14 +82,9 @@ api::Term 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(); + assert(type == SYM_VARIABLE); + // Functions share var namespace + return api::Term(d_solver, d_symtab->lookup(name)); } api::Term Parser::getVariable(const std::string& name) @@ -166,7 +161,7 @@ api::Sort Parser::getSort(const std::string& name) { checkDeclaration(name, CHECK_DECLARED, SYM_SORT); assert(isDeclared(name, SYM_SORT)); - api::Sort t = api::Sort(d_symtab->lookupType(name)); + api::Sort t = api::Sort(d_solver, d_symtab->lookupType(name)); return t; } @@ -175,8 +170,8 @@ api::Sort Parser::getSort(const std::string& name, { checkDeclaration(name, CHECK_DECLARED, SYM_SORT); assert(isDeclared(name, SYM_SORT)); - api::Sort t = - api::Sort(d_symtab->lookupType(name, api::sortVectorToTypes(params))); + api::Sort t = api::Sort( + d_solver, d_symtab->lookupType(name, api::sortVectorToTypes(params))); return t; } @@ -237,7 +232,8 @@ std::vector<api::Term> Parser::bindBoundVars( std::vector<api::Term> vars; for (std::pair<std::string, api::Sort>& i : sortedVarNames) { - vars.push_back(bindBoundVar(i.first, i.second.getType())); + vars.push_back( + bindBoundVar(i.first, api::Sort(d_solver, i.second.getType()))); } return vars; } @@ -251,7 +247,7 @@ api::Term Parser::mkAnonymousFunction(const std::string& prefix, } stringstream name; name << prefix << "_anon_" << ++d_anonymousFunctionCount; - return mkVar(name.str(), type.getType(), flags); + return mkVar(name.str(), api::Sort(d_solver, type.getType()), flags); } std::vector<api::Term> Parser::bindVars(const std::vector<std::string> names, @@ -334,7 +330,8 @@ void Parser::defineParameterizedType(const std::string& name, api::Sort Parser::mkSort(const std::string& name, uint32_t flags) { Debug("parser") << "newSort(" << name << ")" << std::endl; - api::Sort type = d_solver->getExprManager()->mkSort(name, flags); + api::Sort type = + api::Sort(d_solver, d_solver->getExprManager()->mkSort(name, flags)); defineType( name, type, @@ -348,8 +345,9 @@ api::Sort Parser::mkSortConstructor(const std::string& name, { Debug("parser") << "newSortConstructor(" << name << ", " << arity << ")" << std::endl; - api::Sort type = - d_solver->getExprManager()->mkSortConstructor(name, arity, flags); + api::Sort type = api::Sort( + d_solver, + d_solver->getExprManager()->mkSortConstructor(name, arity, flags)); defineType( name, vector<api::Sort>(arity), @@ -379,8 +377,10 @@ api::Sort Parser::mkUnresolvedTypeConstructor( { Debug("parser") << "newSortConstructor(P)(" << name << ", " << params.size() << ")" << std::endl; - api::Sort unresolved = d_solver->getExprManager()->mkSortConstructor( - name, params.size(), ExprManager::SORT_FLAG_PLACEHOLDER); + api::Sort unresolved = + api::Sort(d_solver, + d_solver->getExprManager()->mkSortConstructor( + name, params.size(), ExprManager::SORT_FLAG_PLACEHOLDER)); defineType(name, params, unresolved); api::Sort t = getSort(name, params); d_unresolved.insert(unresolved); @@ -588,11 +588,12 @@ api::Term Parser::applyTypeAscription(api::Term t, api::Sort s) Expr e = t.getExpr(); const DatatypeConstructor& dtc = Datatype::datatypeOf(e)[Datatype::indexOf(e)]; - t = api::Term(em->mkExpr( - kind::APPLY_TYPE_ASCRIPTION, - em->mkConst( - AscriptionType(dtc.getSpecializedConstructorType(s.getType()))), - e)); + t = api::Term( + d_solver, + em->mkExpr(kind::APPLY_TYPE_ASCRIPTION, + em->mkConst(AscriptionType( + dtc.getSpecializedConstructorType(s.getType()))), + e)); } // the type of t does not match the sort s by design (constructor type // vs datatype type), thus we use an alternative check here. @@ -624,7 +625,7 @@ api::Term Parser::mkVar(const std::string& name, uint32_t flags) { return api::Term( - d_solver->getExprManager()->mkVar(name, type.getType(), flags)); + d_solver, d_solver->getExprManager()->mkVar(name, type.getType(), flags)); } //!!!!!!!!!!! temporary @@ -892,16 +893,16 @@ std::vector<unsigned> Parser::processAdHocStringEsc(const std::string& s) return str; } -Expr Parser::mkStringConstant(const std::string& s) +api::Term Parser::mkStringConstant(const std::string& s) { ExprManager* em = d_solver->getExprManager(); if (language::isInputLang_smt2_6(em->getOptions().getInputLanguage())) { - return d_solver->mkString(s, true).getExpr(); + return api::Term(d_solver, d_solver->mkString(s, true).getExpr()); } // otherwise, we must process ad-hoc escape sequences std::vector<unsigned> str = processAdHocStringEsc(s); - return d_solver->mkString(str).getExpr(); + return api::Term(d_solver, d_solver->mkString(str).getExpr()); } } /* CVC4::parser namespace */ |