From de14432ebd850dab001bb860db102e86ec734f97 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 25 Nov 2020 10:46:41 -0600 Subject: Use symbol manager for printing responses get-model (#5516) This makes symbol manager be in charge of determining which sorts and terms to print in response to get-model. This eliminates the need for the parser to call ExprManager::mkVar (and similar methods) with custom flags. This requires significant simplifications to the printers for models, where instead of a NodeCommand, we take a Sort or Term to print in the model. This is one of the last remaining steps for migrating the parser to the new API. The next step will be to remove a lot of the internal infrastructure for managing expression names, commands to print in models, node commands, node listeners, etc. --- src/parser/parser.cpp | 15 ++++----------- 1 file changed, 4 insertions(+), 11 deletions(-) (limited to 'src/parser/parser.cpp') diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 1fc995fd6..1ca2e1c01 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -333,8 +333,7 @@ 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 = - api::Sort(d_solver, d_solver->getExprManager()->mkSort(name, flags)); + api::Sort type = d_solver->mkUninterpretedSort(name); bool globalDecls = d_symman->getGlobalDeclarations(); defineType( name, type, globalDecls && !(flags & ExprManager::SORT_FLAG_PLACEHOLDER)); @@ -347,9 +346,7 @@ api::Sort Parser::mkSortConstructor(const std::string& name, { Debug("parser") << "newSortConstructor(" << name << ", " << arity << ")" << std::endl; - api::Sort type = api::Sort( - d_solver, - d_solver->getExprManager()->mkSortConstructor(name, arity, flags)); + api::Sort type = d_solver->mkSortConstructorSort(name, arity); bool globalDecls = d_symman->getGlobalDeclarations(); defineType(name, vector(arity), @@ -379,10 +376,7 @@ api::Sort Parser::mkUnresolvedTypeConstructor( { Debug("parser") << "newSortConstructor(P)(" << name << ", " << params.size() << ")" << std::endl; - api::Sort unresolved = - api::Sort(d_solver, - d_solver->getExprManager()->mkSortConstructor( - name, params.size(), ExprManager::SORT_FLAG_PLACEHOLDER)); + api::Sort unresolved = d_solver->mkSortConstructorSort(name, params.size()); defineType(name, params, unresolved); api::Sort t = getSort(name, params); d_unresolved.insert(unresolved); @@ -644,8 +638,7 @@ api::Term Parser::mkVar(const std::string& name, const api::Sort& type, uint32_t flags) { - return api::Term( - d_solver, d_solver->getExprManager()->mkVar(name, type.getType(), flags)); + return d_solver->mkConst(type, name); } //!!!!!!!!!!! temporary -- cgit v1.2.3