From: Andrew Reynolds Date: Thu, 3 Dec 2020 16:49:08 +0000 (-0600) Subject: Refactor handling of global declarations (#5577) X-Git-Tag: cvc5-1.0.0~2511 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a0b0aebf36c2ba54edc3ae58dc8270a74560d840;p=cvc5.git Refactor handling of global declarations (#5577) This refactors how global declarations are handled in the parser. In particular, we do not push/pop user contexts in the symbol table and manager when global declarations are true, which is an equivalent behavior to declaring symbols globally. This further refactors to not use ExprManager flags, thus breaking most of the dependencies on the old API. This is work towards fixing global declarations in the smt2 parser. The parser still does not behave correctly for overloaded symbols + global declarations (e.g. see #4767), which require further refactoring. This is also work towards migrating the parser not to depend on the old API. There are a few miscellaneous things to change after this PR, but we are very close to breaking this dependency now. --- diff --git a/src/expr/symbol_manager.cpp b/src/expr/symbol_manager.cpp index f82845fe3..5fb46a5d0 100644 --- a/src/expr/symbol_manager.cpp +++ b/src/expr/symbol_manager.cpp @@ -41,9 +41,11 @@ class SymbolManager::Implementation d_declareTerms(&d_context), d_hasPushedScope(&d_context, false) { + // use an outermost push, to be able to clear all definitions + d_context.push(); } - ~Implementation() {} + ~Implementation() { d_context.pop(); } /** set expression name */ bool setExpressionName(api::Term t, const std::string& name, @@ -68,10 +70,14 @@ class SymbolManager::Implementation void addModelDeclarationTerm(api::Term t); /** reset */ void reset(); + /** reset assertions */ + void resetAssertions(); /** Push a scope in the expression names. */ void pushScope(bool isUserContext); /** Pop a scope in the expression names. */ void popScope(); + /** Have we pushed a scope (e.g. let or quantifier) in the current context? */ + bool hasPushedScope() const; private: /** The context manager for the scope maps. */ @@ -94,8 +100,8 @@ bool SymbolManager::Implementation::setExpressionName(api::Term t, const std::string& name, bool isAssertion) { - Trace("sym-manager") << "set expression name: " << t << " -> " << name - << ", isAssertion=" << isAssertion << std::endl; + Trace("sym-manager") << "SymbolManager: set expression name: " << t << " -> " + << name << ", isAssertion=" << isAssertion << std::endl; // cannot name subexpressions under quantifiers PrettyCheckArgument( !d_hasPushedScope.get(), name, "cannot name function in a scope"); @@ -185,20 +191,22 @@ std::vector SymbolManager::Implementation::getModelDeclareTerms() void SymbolManager::Implementation::addModelDeclarationSort(api::Sort s) { - Trace("sym-manager") << "addModelDeclarationSort " << s << std::endl; + Trace("sym-manager") << "SymbolManager: addModelDeclarationSort " << s + << std::endl; d_declareSorts.push_back(s); } void SymbolManager::Implementation::addModelDeclarationTerm(api::Term t) { - Trace("sym-manager") << "addModelDeclarationTerm " << t << std::endl; + Trace("sym-manager") << "SymbolManager: addModelDeclarationTerm " << t + << std::endl; d_declareTerms.push_back(t); } void SymbolManager::Implementation::pushScope(bool isUserContext) { - Trace("sym-manager") << "pushScope, isUserContext = " << isUserContext - << std::endl; + Trace("sym-manager") << "SymbolManager: pushScope, isUserContext = " + << isUserContext << std::endl; PrettyCheckArgument(!d_hasPushedScope.get() || !isUserContext, "cannot push a user context within a scope context"); d_context.push(); @@ -210,7 +218,7 @@ void SymbolManager::Implementation::pushScope(bool isUserContext) void SymbolManager::Implementation::popScope() { - Trace("sym-manager") << "popScope" << std::endl; + Trace("sym-manager") << "SymbolManager: popScope" << std::endl; if (d_context.getLevel() == 0) { throw ScopeException(); @@ -220,9 +228,31 @@ void SymbolManager::Implementation::popScope() << "d_hasPushedScope is now " << d_hasPushedScope.get() << std::endl; } +bool SymbolManager::Implementation::hasPushedScope() const +{ + return d_hasPushedScope.get(); +} + void SymbolManager::Implementation::reset() { - // clear names? + Trace("sym-manager") << "SymbolManager: reset" << std::endl; + // clear names by popping to context level 0 + while (d_context.getLevel() > 0) + { + d_context.pop(); + } + // push the outermost context + d_context.push(); +} + +void SymbolManager::Implementation::resetAssertions() +{ + Trace("sym-manager") << "SymbolManager: resetAssertions" << std::endl; + // clear names by popping to context level 1 + while (d_context.getLevel() > 1) + { + d_context.pop(); + } } // ---------------------------------------------- SymbolManager @@ -290,12 +320,27 @@ size_t SymbolManager::scopeLevel() const void SymbolManager::pushScope(bool isUserContext) { + // we do not push user contexts when global declarations is true. This + // policy applies both to the symbol table and to the symbol manager. + if (d_globalDeclarations && isUserContext) + { + return; + } d_implementation->pushScope(isUserContext); d_symtabAllocated.pushScope(); } void SymbolManager::popScope() { + // If global declarations is true, then if d_hasPushedScope is false, then + // the pop corresponds to a user context, which we did not push. Note this + // additionally relies on the fact that user contexts cannot be pushed + // within scope contexts. Hence, since we did not push the context, we + // do not pop a context here. + if (d_globalDeclarations && !d_implementation->hasPushedScope()) + { + return; + } d_symtabAllocated.popScope(); d_implementation->popScope(); } @@ -316,4 +361,10 @@ void SymbolManager::reset() d_implementation->reset(); } +void SymbolManager::resetAssertions() +{ + d_implementation->resetAssertions(); + d_symtabAllocated.resetAssertions(); +} + } // namespace CVC4 diff --git a/src/expr/symbol_manager.h b/src/expr/symbol_manager.h index 06b01da8b..fa5732854 100644 --- a/src/expr/symbol_manager.h +++ b/src/expr/symbol_manager.h @@ -130,6 +130,10 @@ class CVC4_PUBLIC SymbolManager * Reset this symbol manager, which resets the symbol table. */ void reset(); + /** + * Reset assertions for this symbol manager, which resets the symbol table. + */ + void resetAssertions(); /** Set global declarations to the value flag. */ void setGlobalDeclarations(bool flag); /** Get global declarations flag. */ diff --git a/src/expr/symbol_table.cpp b/src/expr/symbol_table.cpp index 3d01b778c..28e979b25 100644 --- a/src/expr/symbol_table.cpp +++ b/src/expr/symbol_table.cpp @@ -346,10 +346,11 @@ class SymbolTable::Implementation { d_typeMap(&d_context), d_overload_trie(&d_context) { + // use an outermost push, to be able to clear definitions not at level zero + d_context.push(); } - ~Implementation() { - } + ~Implementation() { d_context.pop(); } bool bind(const string& name, api::Term obj, bool levelZero, bool doOverload); void bindType(const string& name, api::Sort t, bool levelZero = false); @@ -368,6 +369,7 @@ class SymbolTable::Implementation { void pushScope(); size_t getLevel() const; void reset(); + void resetAssertions(); //------------------------ operator overloading /** implementation of function from header */ bool isOverloadedFunction(api::Term fun) const; @@ -411,6 +413,9 @@ bool SymbolTable::Implementation::bind(const string& name, bool doOverload) { PrettyCheckArgument(!obj.isNull(), obj, "cannot bind to a null api::Term"); + Trace("sym-table") << "SymbolTable: bind " << name + << ", levelZero=" << levelZero + << ", doOverload=" << doOverload << std::endl; if (doOverload) { if (!bindWithOverloading(name, obj)) { return false; @@ -538,7 +543,9 @@ size_t SymbolTable::Implementation::lookupArity(const string& name) { } void SymbolTable::Implementation::popScope() { - if (d_context.getLevel() == 0) { + // should not pop beyond level one + if (d_context.getLevel() == 1) + { throw ScopeException(); } d_context.pop(); @@ -551,10 +558,22 @@ size_t SymbolTable::Implementation::getLevel() const { } void SymbolTable::Implementation::reset() { + Trace("sym-table") << "SymbolTable: reset" << std::endl; this->SymbolTable::Implementation::~Implementation(); new (this) SymbolTable::Implementation(); } +void SymbolTable::Implementation::resetAssertions() +{ + Trace("sym-table") << "SymbolTable: resetAssertions" << std::endl; + // pop all contexts + while (d_context.getLevel() > 0) + { + d_context.pop(); + } + d_context.push(); +} + bool SymbolTable::Implementation::isOverloadedFunction(api::Term fun) const { return d_overload_trie.isOverloadedFunction(fun); @@ -658,5 +677,6 @@ void SymbolTable::popScope() { d_implementation->popScope(); } void SymbolTable::pushScope() { d_implementation->pushScope(); } size_t SymbolTable::getLevel() const { return d_implementation->getLevel(); } void SymbolTable::reset() { d_implementation->reset(); } +void SymbolTable::resetAssertions() { d_implementation->resetAssertions(); } } // namespace CVC4 diff --git a/src/expr/symbol_table.h b/src/expr/symbol_table.h index 0e30d6d73..b2ca745f7 100644 --- a/src/expr/symbol_table.h +++ b/src/expr/symbol_table.h @@ -172,6 +172,8 @@ class CVC4_PUBLIC SymbolTable { /** Reset everything. */ void reset(); + /** Reset assertions. */ + void resetAssertions(); //------------------------ operator overloading /** is this function overloaded? */ diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp index ef85dd1a9..46e88af8f 100644 --- a/src/parser/antlr_input.cpp +++ b/src/parser/antlr_input.cpp @@ -20,7 +20,6 @@ #include #include "base/output.h" -#include "expr/type.h" #include "parser/antlr_line_buffered_input.h" #include "parser/bounded_token_buffer.h" #include "parser/bounded_token_factory.h" diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index f174ed470..8831bfb7a 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -565,13 +565,9 @@ namespace CVC4 { #include #include "base/output.h" -#include "expr/expr.h" -#include "expr/kind.h" -#include "expr/type.h" #include "parser/antlr_input.h" #include "parser/parser.h" - #define REPEAT_COMMAND(k, CommandCtor) \ ({ \ unsigned __k = (k); \ @@ -742,13 +738,15 @@ mainCommand[std::unique_ptr* cmd] { UNSUPPORTED("POPTO_SCOPE command"); } | RESET_TOK - { cmd->reset(new ResetCommand()); + { + cmd->reset(new ResetCommand()); + // reset the state of the parser, which is independent of the symbol + // manager PARSER_STATE->reset(); } | RESET_TOK ASSERTIONS_TOK { cmd->reset(new ResetAssertionsCommand()); - PARSER_STATE->reset(); } // Datatypes can be mututally-recursive if they're in the same @@ -889,7 +887,7 @@ mainCommand[std::unique_ptr* cmd] idCommaFlag=true; })? { - func = PARSER_STATE->bindVar(id, t, ExprManager::VAR_FLAG_NONE, true); + func = PARSER_STATE->bindVar(id, t, false, true); ids.push_back(id); types.push_back(t); funcs.push_back(func); @@ -1117,8 +1115,7 @@ declareVariables[std::unique_ptr* cmd, CVC4::api::Sort& t, } else { Debug("parser") << " " << *i << " not declared" << std::endl; if(topLevel) { - api::Term func = - PARSER_STATE->bindVar(*i, t, ExprManager::VAR_FLAG_GLOBAL); + api::Term func = PARSER_STATE->bindVar(*i, t); Command* decl = new DeclareFunctionCommand(*i, func, t); seq->addCommand(decl); } else { @@ -1151,10 +1148,7 @@ declareVariables[std::unique_ptr* cmd, CVC4::api::Sort& t, ++i) { Debug("parser") << "making " << *i << " : " << t << " = " << f << std::endl; PARSER_STATE->checkDeclaration(*i, CHECK_UNDECLARED, SYM_VARIABLE); - api::Term func = PARSER_STATE->mkVar( - *i, - t, - ExprManager::VAR_FLAG_GLOBAL | ExprManager::VAR_FLAG_DEFINED); + api::Term func = SOLVER->mkConst(t, *i); PARSER_STATE->defineVar(*i, fterm); Command* decl = new DefineFunctionCommand(*i, func, formals, f, true); seq->addCommand(decl); @@ -2307,11 +2301,11 @@ datatypeDef[std::vector& datatypes] * below. */ : identifier[id,CHECK_NONE,SYM_SORT] { PARSER_STATE->pushScope(); } ( LBRACKET identifier[id2,CHECK_UNDECLARED,SYM_SORT] { - t = PARSER_STATE->mkSort(id2, ExprManager::SORT_FLAG_PLACEHOLDER); + t = PARSER_STATE->mkSort(id2); params.push_back( t ); } ( COMMA identifier[id2,CHECK_UNDECLARED,SYM_SORT] { - t = PARSER_STATE->mkSort(id2, ExprManager::SORT_FLAG_PLACEHOLDER); + t = PARSER_STATE->mkSort(id2); params.push_back( t ); } )* RBRACKET )? diff --git a/src/parser/cvc/cvc_input.cpp b/src/parser/cvc/cvc_input.cpp index 5e3510a4b..393e80e02 100644 --- a/src/parser/cvc/cvc_input.cpp +++ b/src/parser/cvc/cvc_input.cpp @@ -18,7 +18,6 @@ #include -#include "expr/expr_manager.h" #include "parser/antlr_input.h" #include "parser/parser_exception.h" #include "parser/cvc/CvcLexer.h" diff --git a/src/parser/input.cpp b/src/parser/input.cpp index 603da0e31..038fc1ef5 100644 --- a/src/parser/input.cpp +++ b/src/parser/input.cpp @@ -20,7 +20,6 @@ #include "parser/input.h" #include "base/output.h" -#include "expr/type.h" #include "parser/parser.h" #include "parser/parser_exception.h" diff --git a/src/parser/input.h b/src/parser/input.h index 19fd4db72..c05384740 100644 --- a/src/parser/input.h +++ b/src/parser/input.h @@ -25,16 +25,12 @@ #include #include "api/cvc4cpp.h" -#include "expr/expr.h" -#include "expr/expr_manager.h" #include "options/language.h" #include "parser/parser_exception.h" namespace CVC4 { class Command; -class Type; -class FunctionType; namespace parser { diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 1ca2e1c01..ab0571e53 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -25,9 +25,7 @@ #include "api/cvc4cpp.h" #include "base/output.h" -#include "expr/expr.h" #include "expr/kind.h" -#include "expr/type.h" #include "options/options.h" #include "parser/input.h" #include "parser/parser_exception.h" @@ -199,16 +197,13 @@ bool Parser::isPredicate(const std::string& name) { api::Term Parser::bindVar(const std::string& name, const api::Sort& type, - uint32_t flags, + bool levelZero, bool doOverload) { - if (d_symman->getGlobalDeclarations()) - { - flags |= ExprManager::VAR_FLAG_GLOBAL; - } + bool globalDecls = d_symman->getGlobalDeclarations(); Debug("parser") << "bindVar(" << name << ", " << type << ")" << std::endl; - api::Term expr = mkVar(name, type, flags); - defineVar(name, expr, flags & ExprManager::VAR_FLAG_GLOBAL, doOverload); + api::Term expr = d_solver->mkConst(type, name); + defineVar(name, expr, globalDecls || levelZero, doOverload); return expr; } @@ -217,7 +212,7 @@ 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); + defineVar(name, expr); return expr; } @@ -232,33 +227,14 @@ std::vector Parser::bindBoundVars( return vars; } -api::Term Parser::mkAnonymousFunction(const std::string& prefix, - const api::Sort& type, - uint32_t flags) -{ - bool globalDecls = d_symman->getGlobalDeclarations(); - if (globalDecls) - { - flags |= ExprManager::VAR_FLAG_GLOBAL; - } - stringstream name; - name << prefix << "_anon_" << ++d_anonymousFunctionCount; - return mkVar(name.str(), type, flags); -} - std::vector Parser::bindVars(const std::vector names, const api::Sort& type, - uint32_t flags, + bool levelZero, bool doOverload) { - bool globalDecls = d_symman->getGlobalDeclarations(); - if (globalDecls) - { - flags |= ExprManager::VAR_FLAG_GLOBAL; - } std::vector vars; for (unsigned i = 0; i < names.size(); ++i) { - vars.push_back(bindVar(names[i], type, flags, doOverload)); + vars.push_back(bindVar(names[i], type, levelZero, doOverload)); } return vars; } @@ -330,34 +306,29 @@ void Parser::defineParameterizedType(const std::string& name, defineType(name, params, type); } -api::Sort Parser::mkSort(const std::string& name, uint32_t flags) +api::Sort Parser::mkSort(const std::string& name) { Debug("parser") << "newSort(" << name << ")" << std::endl; - api::Sort type = d_solver->mkUninterpretedSort(name); bool globalDecls = d_symman->getGlobalDeclarations(); - defineType( - name, type, globalDecls && !(flags & ExprManager::SORT_FLAG_PLACEHOLDER)); + api::Sort type = d_solver->mkUninterpretedSort(name); + defineType(name, type, globalDecls); return type; } -api::Sort Parser::mkSortConstructor(const std::string& name, - size_t arity, - uint32_t flags) +api::Sort Parser::mkSortConstructor(const std::string& name, size_t arity) { Debug("parser") << "newSortConstructor(" << name << ", " << arity << ")" << std::endl; - api::Sort type = d_solver->mkSortConstructorSort(name, arity); bool globalDecls = d_symman->getGlobalDeclarations(); - defineType(name, - vector(arity), - type, - globalDecls && !(flags & ExprManager::SORT_FLAG_PLACEHOLDER)); + api::Sort type = d_solver->mkSortConstructorSort(name, arity); + defineType(name, vector(arity), type, globalDecls); return type; } api::Sort Parser::mkUnresolvedType(const std::string& name) { - api::Sort unresolved = mkSort(name, ExprManager::SORT_FLAG_PLACEHOLDER); + api::Sort unresolved = d_solver->mkUninterpretedSort(name); + defineType(name, unresolved); d_unresolved.insert(unresolved); return unresolved; } @@ -365,8 +336,8 @@ api::Sort Parser::mkUnresolvedType(const std::string& name) api::Sort Parser::mkUnresolvedTypeConstructor(const std::string& name, size_t arity) { - api::Sort unresolved = - mkSortConstructor(name, arity, ExprManager::SORT_FLAG_PLACEHOLDER); + api::Sort unresolved = d_solver->mkSortConstructorSort(name, arity); + defineType(name, vector(arity), unresolved); d_unresolved.insert(unresolved); return unresolved; } @@ -633,20 +604,9 @@ 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 d_solver->mkConst(type, name); -} -//!!!!!!!!!!! temporary - 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_VARIABLE: return d_symtab->isBound(name); case SYM_SORT: return d_symtab->isBoundType(name); } @@ -654,11 +614,6 @@ bool Parser::isDeclared(const std::string& name, SymbolType type) { return false; } -void Parser::reserveSymbolAtAssertionLevel(const std::string& varName) { - checkDeclaration(varName, CHECK_UNDECLARED, SYM_VARIABLE); - d_reservedSymbols.insert(varName); -} - void Parser::checkDeclaration(const std::string& varName, DeclarationCheck check, SymbolType type, @@ -769,23 +724,14 @@ size_t Parser::scopeLevel() const { return d_symman->scopeLevel(); } void Parser::pushScope(bool isUserContext) { d_symman->pushScope(isUserContext); - if (isUserContext) - { - d_assertionLevel = scopeLevel(); - } } void Parser::popScope() { d_symman->popScope(); - if (scopeLevel() < d_assertionLevel) - { - d_assertionLevel = scopeLevel(); - d_reservedSymbols.clear(); - } } -void Parser::reset() { d_symman->reset(); } +void Parser::reset() {} SymbolManager* Parser::getSymbolManager() { return d_symman; } @@ -928,11 +874,11 @@ api::Term Parser::mkStringConstant(const std::string& s) { if (language::isInputLang_smt2_6(d_solver->getOptions().getInputLanguage())) { - return api::Term(d_solver, d_solver->mkString(s, true).getExpr()); + return d_solver->mkString(s, true); } // otherwise, we must process ad-hoc escape sequences std::vector str = processAdHocStringEsc(s); - return api::Term(d_solver, d_solver->mkString(str).getExpr()); + return d_solver->mkString(str); } } /* CVC4::parser namespace */ diff --git a/src/parser/parser.h b/src/parser/parser.h index 686a0d147..31c421e2c 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -127,16 +127,6 @@ private: */ size_t d_assertionLevel; - /** - * Maintains a list of reserved symbols at the assertion level that might - * not occur in our symbol table. This is necessary to e.g. support the - * proper behavior of the :named annotation in SMT-LIBv2 when used under - * a let or a quantifier, since inside a let/quant body the declaration - * scope is that of the let/quant body, but the defined name should be - * reserved at the assertion level. - */ - std::set d_reservedSymbols; - /** How many anonymous functions we've created. */ size_t d_anonymousFunctionCount; @@ -394,11 +384,6 @@ public: SymbolType type = SYM_VARIABLE, std::string notes = ""); - /** - * Reserve a symbol at the assertion level. - */ - void reserveSymbolAtAssertionLevel(const std::string& name); - /** * Checks whether the given expression is function-like, i.e. * it expects arguments. This is checked by looking at the type @@ -410,33 +395,35 @@ public: */ void checkFunctionLike(api::Term fun); - /** Create a new CVC4 variable expression of the given type. + /** Create a new CVC4 variable expression of the given type. * - * flags specify information about the variable, e.g. whether it is global or defined - * (see enum in expr_manager_template.h). + * It is inserted at context level zero in the symbol table if levelZero is + * true, or if we are using global declarations. * * If a symbol with name already exists, * then if doOverload is true, we create overloaded operators. - * else if doOverload is false, the existing expression is shadowed by the new expression. + * else if doOverload is false, the existing expression is shadowed by the + * new expression. */ api::Term bindVar(const std::string& name, const api::Sort& type, - uint32_t flags = ExprManager::VAR_FLAG_NONE, + bool levelZero = false, bool doOverload = false); /** * Create a set of new CVC4 variable expressions of the given type. * - * flags specify information about the variable, e.g. whether it is global or defined - * (see enum in expr_manager_template.h). + * It is inserted at context level zero in the symbol table if levelZero is + * true, or if we are using global declarations. * * For each name, if a symbol with name already exists, * then if doOverload is true, we create overloaded operators. - * else if doOverload is false, the existing expression is shadowed by the new expression. + * else if doOverload is false, the existing expression is shadowed by the + * new expression. */ std::vector bindVars(const std::vector names, const api::Sort& type, - uint32_t flags = ExprManager::VAR_FLAG_NONE, + bool levelZero = false, bool doOverload = false); /** @@ -455,9 +442,6 @@ public: /** * Create a set of new CVC4 bound variable expressions of the given type. * - * flags specify information about the variable, e.g. whether it is global or defined - * (see enum in expr_manager_template.h). - * * For each name, if a symbol with name already exists, * then if doOverload is true, we create overloaded operators. * else if doOverload is false, the existing expression is shadowed by the new expression. @@ -465,18 +449,6 @@ public: std::vector bindBoundVars(const std::vector names, const api::Sort& type); - /** - * Create a new CVC4 function expression of the given type, - * appending a unique index to its name. (That's the ONLY - * difference between mkAnonymousFunction() and mkVar()). - * - * flags specify information about the variable, e.g. whether it is global or defined - * (see enum in expr_manager_template.h). - */ - api::Term mkAnonymousFunction(const std::string& prefix, - const api::Sort& type, - uint32_t flags = ExprManager::VAR_FLAG_NONE); - /** Create a new variable definition (e.g., from a let binding). * levelZero is set if the binding must be done at level 0. * If a symbol with name already exists, @@ -526,15 +498,12 @@ public: /** * Creates a new sort with the given name. */ - api::Sort mkSort(const std::string& name, - uint32_t flags = ExprManager::SORT_FLAG_NONE); + api::Sort mkSort(const std::string& name); /** * Creates a new sort constructor with the given name and arity. */ - api::Sort mkSortConstructor(const std::string& name, - size_t arity, - uint32_t flags = ExprManager::SORT_FLAG_NONE); + api::Sort mkSortConstructor(const std::string& name, size_t arity); /** * Creates a new "unresolved type," used only during parsing. @@ -667,15 +636,6 @@ public: */ api::Term applyTypeAscription(api::Term t, api::Sort s); - //!!!!!!!!!!! temporary - /** - * Make var, with flags required by the ExprManager, see ExprManager::mkVar. - */ - api::Term mkVar(const std::string& name, - const api::Sort& type, - uint32_t flags); - //!!!!!!!!!!! temporary - /** * Add an operator to the current legal set. * diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp index b9d0cb415..e68ecfe71 100644 --- a/src/parser/parser_builder.cpp +++ b/src/parser/parser_builder.cpp @@ -23,7 +23,6 @@ #include "api/cvc4cpp.h" #include "cvc/cvc.h" -#include "expr/expr_manager.h" #include "options/options.h" #include "parser/input.h" #include "parser/parser.h" diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 6eb3d8061..11ccb4935 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -103,9 +103,6 @@ namespace CVC4 { #include "api/cvc4cpp.h" #include "base/output.h" -#include "expr/expr.h" -#include "expr/kind.h" -#include "expr/type.h" #include "options/set_language.h" #include "parser/antlr_input.h" #include "parser/parser.h" @@ -294,7 +291,7 @@ command [std::unique_ptr* cmd] else { api::Term func = - PARSER_STATE->bindVar(name, t, ExprManager::VAR_FLAG_NONE, true); + PARSER_STATE->bindVar(name, t, false, true); cmd->reset(new DeclareFunctionCommand(name, func, t)); } } @@ -333,8 +330,7 @@ command [std::unique_ptr* cmd] // must not be extended with the name itself; no recursion // permitted) // we allow overloading for function definitions - api::Term func = PARSER_STATE->bindVar(name, t, - ExprManager::VAR_FLAG_DEFINED, true); + api::Term func = PARSER_STATE->bindVar(name, t, false, true); cmd->reset(new DefineFunctionCommand( name, func, terms, expr, SYM_MAN->getGlobalDeclarations())); } @@ -775,7 +771,7 @@ smt25Command[std::unique_ptr* cmd] sortSymbol[t,CHECK_DECLARED] { // allow overloading here api::Term c = - PARSER_STATE->bindVar(name, t, ExprManager::VAR_FLAG_NONE, true); + PARSER_STATE->bindVar(name, t, false, true); cmd->reset(new DeclareFunctionCommand(name, c, t)); } /* get model */ @@ -792,14 +788,16 @@ smt25Command[std::unique_ptr* cmd] /* reset: reset everything, returning solver to initial state. * Logic and options must be set again. */ | RESET_TOK - { cmd->reset(new ResetCommand()); + { + cmd->reset(new ResetCommand()); + // reset the state of the parser, which is independent of the symbol + // manager PARSER_STATE->reset(); } /* reset-assertions: reset assertions, assertion stack, declarations, * etc., but the logic and options remain as they were. */ | RESET_ASSERTIONS_TOK { cmd->reset(new ResetAssertionsCommand()); - PARSER_STATE->resetAssertions(); } | DEFINE_FUN_REC_TOK { PARSER_STATE->checkThatLogicIsSet(); } @@ -943,7 +941,7 @@ extendedCommand[std::unique_ptr* cmd] } // allow overloading api::Term func = - PARSER_STATE->bindVar(name, tt, ExprManager::VAR_FLAG_NONE, true); + PARSER_STATE->bindVar(name, tt, false, true); seq->addCommand(new DeclareFunctionCommand(name, func, tt)); sorts.clear(); } @@ -963,7 +961,7 @@ extendedCommand[std::unique_ptr* cmd] } // allow overloading api::Term func = - PARSER_STATE->bindVar(name, t, ExprManager::VAR_FLAG_NONE, true); + PARSER_STATE->bindVar(name, t, false, true); seq->addCommand(new DeclareFunctionCommand(name, func, t)); sorts.clear(); } @@ -977,8 +975,7 @@ extendedCommand[std::unique_ptr* cmd] { PARSER_STATE->checkUserSymbol(name); } term[e,e2] { - api::Term func = PARSER_STATE->bindVar(name, e.getSort(), - ExprManager::VAR_FLAG_DEFINED); + api::Term func = PARSER_STATE->bindVar(name, e.getSort()); cmd->reset(new DefineFunctionCommand( name, func, e, SYM_MAN->getGlobalDeclarations())); } @@ -1008,8 +1005,7 @@ extendedCommand[std::unique_ptr* cmd] } tt = SOLVER->mkFunctionSort(sorts, tt); } - api::Term func = PARSER_STATE->bindVar(name, tt, - ExprManager::VAR_FLAG_DEFINED); + api::Term func = PARSER_STATE->bindVar(name, tt); cmd->reset(new DefineFunctionCommand( name, func, terms, e, SYM_MAN->getGlobalDeclarations())); } @@ -1030,8 +1026,7 @@ extendedCommand[std::unique_ptr* cmd] // declare the name down here (while parsing term, signature // must not be extended with the name itself; no recursion // permitted) - api::Term func = PARSER_STATE->bindVar(name, t, - ExprManager::VAR_FLAG_DEFINED); + api::Term func = PARSER_STATE->bindVar(name, t); cmd->reset(new DefineFunctionCommand( name, func, terms, e, SYM_MAN->getGlobalDeclarations())); } @@ -1101,7 +1096,7 @@ datatypes_2_5_DefCommand[bool isCo, std::unique_ptr* cmd] LPAREN_TOK /* parametric sorts */ ( symbol[name,CHECK_UNDECLARED,SYM_SORT] { - sorts.push_back(PARSER_STATE->mkSort(name, ExprManager::SORT_FLAG_PLACEHOLDER)); + sorts.push_back(PARSER_STATE->mkSort(name)); } )* RPAREN_TOK @@ -1197,7 +1192,7 @@ datatypesDef[bool isCo, ( PAR_TOK { PARSER_STATE->pushScope(); } LPAREN_TOK ( symbol[name,CHECK_UNDECLARED,SYM_SORT] { - params.push_back( PARSER_STATE->mkSort(name, ExprManager::SORT_FLAG_PLACEHOLDER)); } + params.push_back( PARSER_STATE->mkSort(name)); } )* RPAREN_TOK { // if the arity was fixed by prelude and is not equal to the number of parameters diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 17f5661b4..2474c89c2 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -18,7 +18,7 @@ #include #include "base/check.h" -#include "expr/type.h" +#include "expr/expr.h" #include "options/options.h" #include "parser/antlr_input.h" #include "parser/parser.h" @@ -41,10 +41,9 @@ Smt2::Smt2(api::Solver* solver, d_logicSet(false), d_seenSetLogic(false) { - pushScope(true); } -Smt2::~Smt2() { popScope(); } +Smt2::~Smt2() {} void Smt2::addArithmeticOperators() { addOperator(api::PLUS, "+"); @@ -445,7 +444,7 @@ api::Term Smt2::bindDefineFunRec( api::Sort ft = mkFlatFunctionType(sorts, t, flattenVars); // allow overloading - return bindVar(fname, ft, ExprManager::VAR_FLAG_NONE, true); + return bindVar(fname, ft, false, true); } void Smt2::pushDefineFunRecScope( @@ -473,16 +472,6 @@ void Smt2::reset() { d_logic = LogicInfo(); operatorKindMap.clear(); d_lastNamedTerm = std::pair(); - this->Parser::reset(); - pushScope(true); -} - -void Smt2::resetAssertions() { - // Remove all declarations except the ones at level 0. - while (this->scopeLevel() > 0) { - this->popScope(); - } - pushScope(true); } std::unique_ptr Smt2::invConstraint( @@ -1083,6 +1072,7 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector& args) else if (p.d_kind == api::APPLY_SELECTOR && !p.d_expr.isNull()) { // tuple selector case + std::string indexString = p.d_expr.toString(); Integer x = p.d_expr.getExpr().getConst().getNumerator(); if (!x.fitsUnsignedInt()) { diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 654ff9fbf..ed329675d 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -192,8 +192,6 @@ class Smt2 : public Parser void reset() override; - void resetAssertions(); - /** * Creates a command that adds an invariant constraint. * diff --git a/src/parser/smt2/smt2_input.cpp b/src/parser/smt2/smt2_input.cpp index 99907b51a..01eaf7096 100644 --- a/src/parser/smt2/smt2_input.cpp +++ b/src/parser/smt2/smt2_input.cpp @@ -18,7 +18,6 @@ #include -#include "expr/expr_manager.h" #include "parser/input.h" #include "parser/parser.h" #include "parser/parser_exception.h" diff --git a/src/parser/smt2/sygus_input.cpp b/src/parser/smt2/sygus_input.cpp index e1365f603..729dad4ec 100644 --- a/src/parser/smt2/sygus_input.cpp +++ b/src/parser/smt2/sygus_input.cpp @@ -18,7 +18,6 @@ #include -#include "expr/expr_manager.h" #include "parser/input.h" #include "parser/parser.h" #include "parser/parser_exception.h" diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp index f80b9c3c8..23bbd443d 100644 --- a/src/parser/tptp/tptp.cpp +++ b/src/parser/tptp/tptp.cpp @@ -21,7 +21,6 @@ #include #include "api/cvc4cpp.h" -#include "expr/type.h" #include "options/options.h" #include "parser/parser.h" #include "smt/command.h" @@ -247,7 +246,7 @@ api::Term Tptp::parseOpToExpr(ParseOp& p) { api::Sort t = p.d_type == d_solver->getBooleanSort() ? p.d_type : d_unsorted; - expr = bindVar(p.d_name, t, ExprManager::VAR_FLAG_GLOBAL); // levelZero + expr = bindVar(p.d_name, t, true); // must define at level zero preemptCommand(new DeclareFunctionCommand(p.d_name, expr, t)); } return expr; @@ -291,7 +290,7 @@ api::Term Tptp::applyParseOp(ParseOp& p, std::vector& args) api::Sort t = p.d_type == d_solver->getBooleanSort() ? p.d_type : d_unsorted; t = d_solver->mkFunctionSort(sorts, t); - v = bindVar(p.d_name, t, ExprManager::VAR_FLAG_GLOBAL); // levelZero + v = bindVar(p.d_name, t, true); // must define at level zero preemptCommand(new DeclareFunctionCommand(p.d_name, v, t)); } // args might be rationals, in which case we need to create diff --git a/src/parser/tptp/tptp_input.cpp b/src/parser/tptp/tptp_input.cpp index 5634510ff..12c1a148a 100644 --- a/src/parser/tptp/tptp_input.cpp +++ b/src/parser/tptp/tptp_input.cpp @@ -19,7 +19,6 @@ #include -#include "expr/expr_manager.h" #include "parser/input.h" #include "parser/parser.h" #include "parser/parser_exception.h" diff --git a/src/smt/command.cpp b/src/smt/command.cpp index d02c1631e..cfd25fa3b 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -869,6 +869,7 @@ void ResetCommand::invoke(api::Solver* solver, SymbolManager* sm) { try { + sm->reset(); solver->getSmtEngine()->reset(); d_commandStatus = CommandSuccess::instance(); } @@ -897,6 +898,7 @@ void ResetAssertionsCommand::invoke(api::Solver* solver, SymbolManager* sm) { try { + sm->resetAssertions(); solver->resetAssertions(); d_commandStatus = CommandSuccess::instance(); }