From bcf90d561a60ebce1417950fd570e95199061111 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 2 Mar 2022 15:11:05 -0600 Subject: [PATCH] Eliminate CDHashMap::insertAtContextLevelZero (#8173) This method unnecessarily complicates the usage of CDHashMap. It had one usage in the current code, for dealing with global declarations. However, this was an entirely artificial use case, as one should properly manage scopes when this option is true (i.e. global-declarations simply disables user-level scoping in the symbol table). It also simplifies the symbol table so that it doesn't automatically push a global outermost scope. Instead, this scope is pushed when the logic is declared, so that background symbols are correctly added at level 0. Fixes #4767. --- src/context/cdhashmap.h | 59 ++++----------------------- src/context/cdhashset.h | 4 -- src/context/cdinsert_hashmap.h | 59 +++++++-------------------- src/expr/symbol_manager.cpp | 6 ++- src/expr/symbol_table.cpp | 48 +++++++--------------- src/expr/symbol_table.h | 10 +---- src/parser/parser.cpp | 35 ++++++---------- src/parser/parser.h | 18 +------- src/parser/smt2/Smt2.g | 8 ++-- src/parser/smt2/smt2.cpp | 34 ++++++++------- src/parser/tptp/tptp.cpp | 37 +++++++++++------ src/parser/tptp/tptp.h | 9 ++++ test/unit/context/cdhashmap_black.cpp | 27 ++++-------- 13 files changed, 120 insertions(+), 234 deletions(-) diff --git a/src/context/cdhashmap.h b/src/context/cdhashmap.h index d765905d6..63b166d61 100644 --- a/src/context/cdhashmap.h +++ b/src/context/cdhashmap.h @@ -203,28 +203,16 @@ class CDOhash_map : public ContextObj CDOhash_map(Context* context, CDHashMap* map, const Key& key, - const Data& data, - bool atLevelZero = false) + const Data& data) : ContextObj(false, context), d_value(key, data), d_map(NULL) { - if (atLevelZero) - { - // "Initializing" map insertion: this entry will never be - // removed from the map, it's inserted at level 0 as an - // "initializing" element. See - // CDHashMap<>::insertAtContextLevelZero(). - mutable_data() = data; - } - else - { - // Normal map insertion: first makeCurrent(), then set the data - // and then, later, the map. Order is important; we can't - // initialize d_map in the constructor init list above, because - // we want the restore of d_map to NULL to signal us to remove - // the element from the map. + // Normal map insertion: first makeCurrent(), then set the data + // and then, later, the map. Order is important; we can't + // initialize d_map in the constructor init list above, because + // we want the restore of d_map to NULL to signal us to remove + // the element from the map. - set(data); - } + set(data); d_map = map; CDOhash_map*& first = d_map->d_first; @@ -379,39 +367,6 @@ class CDHashMap : public ContextObj return res.second; } - /** - * Version of insert() for CDHashMap<> that inserts data value d at - * context level zero. This is a special escape hatch for inserting - * "initializing" data into the map. Imagine something happens at a - * deep context level L that causes insertion into a map, such that - * the object should have an "initializing" value v1 below context - * level L, and a "current" value v2 at context level L. Then you - * can (assuming key k): - * - * map.insertAtContextLevelZero(k, v1); - * map.insert(k, v2); - * - * The justification for this "escape hatch" has to do with - * variables and assignments in theories (e.g., in arithmetic). - * Let's say you introduce a new variable x at some deep decision - * level (thanks to lazy registration, or a splitting lemma, or - * whatever). x might be mapped to something, but for theory - * implementation simplicity shouldn't disappear from the map on - * backjump; rather, it can take another (legal) value, or a special - * value to indicate it needs to be recomputed. - * - * It is an error (checked via AlwaysAssert()) to - * insertAtContextLevelZero() a key that already is in the map. - */ - void insertAtContextLevelZero(const Key& k, const Data& d) - { - AlwaysAssert(d_map.find(k) == d_map.end()); - - Element* obj = - new (true) Element(d_context, this, k, d, true /* atLevelZero */); - d_map.insert(std::make_pair(k, obj)); - } - // FIXME: no erase(), too much hassle to implement efficiently... using value_type = typename CDOhash_map::value_type; diff --git a/src/context/cdhashset.h b/src/context/cdhashset.h index b7e3b8ed5..cd57d8f76 100644 --- a/src/context/cdhashset.h +++ b/src/context/cdhashset.h @@ -149,10 +149,6 @@ public: return super::key_end(); } - void insertAtContextLevelZero(const V& v) { - return super::insertAtContextLevelZero(v, true); - } - }; /* class CDHashSet */ } // namespace context diff --git a/src/context/cdinsert_hashmap.h b/src/context/cdinsert_hashmap.h index b383fe931..2d4906ea4 100644 --- a/src/context/cdinsert_hashmap.h +++ b/src/context/cdinsert_hashmap.h @@ -28,7 +28,6 @@ * - Use insert_safe if you want to check if the element has been inserted * and only insert if it has not yet been. * - Does not accept TNodes as keys. - * - Supports insertAtContextLevelZero() if the element is not in the map. */ #include @@ -191,22 +190,13 @@ private: /** For restores, we need to keep track of the previous size. */ size_t d_size; - /** - * To support insertAtContextLevelZero() and restores, - * we have called d_insertMap->d_pushFront(). - */ - size_t d_pushFronts; - /** * Private copy constructor used only by save(). d_insertMap is * not copied: only the base class information and - * d_size and d_pushFronts are needed in restore. + * d_size are needed in restore. */ - CDInsertHashMap(const CDInsertHashMap& l) : - ContextObj(l), - d_insertMap(NULL), - d_size(l.d_size), - d_pushFronts(l.d_pushFronts) + CDInsertHashMap(const CDInsertHashMap& l) + : ContextObj(l), d_insertMap(nullptr), d_size(l.d_size) { Debug("CDInsertHashMap") << "copy ctor: " << this << " from " << &l @@ -232,12 +222,12 @@ private: return data; } protected: - /** - * Implementation of mandatory ContextObj method restore: - * restore to the previous size taking into account the number - * of new pushFront calls have happened since saving. - * The d_insertMap is untouched and d_pushFronts is also kept. - */ + /** + * Implementation of mandatory ContextObj method restore: + * restore to the previous size taking into account the number + * of new pushFront calls have happened since saving. + * The d_insertMap is untouched. + */ void restore(ContextObj* data) override { Debug("CDInsertHashMap") @@ -245,12 +235,9 @@ protected: << " data == " << data << " d_insertMap == " << this->d_insertMap << std::endl; size_t oldSize = ((CDInsertHashMap*)data)->d_size; - size_t oldPushFronts = - ((CDInsertHashMap*)data)->d_pushFronts; - Assert(oldPushFronts <= d_pushFronts); // The size to restore to. - size_t restoreSize = oldSize + (d_pushFronts - oldPushFronts); + size_t restoreSize = oldSize; d_insertMap->pop_to_size(restoreSize); d_size = restoreSize; Assert(d_insertMap->size() == d_size); @@ -263,13 +250,11 @@ public: /** * Main constructor: d_insertMap starts as an empty map, with the size is 0 */ - CDInsertHashMap(Context* context) : - ContextObj(context), - d_insertMap(new IHM()), - d_size(0), - d_pushFronts(0){ - Assert(d_insertMap->size() == d_size); - } + CDInsertHashMap(Context* context) + : ContextObj(context), d_insertMap(new IHM()), d_size(0) + { + Assert(d_insertMap->size() == d_size); + } /** * Destructor: delete the d_insertMap @@ -328,20 +313,6 @@ public: } } - /** - * Version of insert() for CDMap<> that inserts data value d at - * context level zero. - * - * It is an error to insertAtContextLevelZero() - * a key that already is in the map. - */ - void insertAtContextLevelZero(const Key& k, const Data& d){ - makeCurrent(); - ++d_size; - ++d_pushFronts; - d_insertMap->push_front(k, d); - } - /** Returns true if k is a mapped key in the context. */ bool contains(const Key& k) const { return d_insertMap->contains(k); diff --git a/src/expr/symbol_manager.cpp b/src/expr/symbol_manager.cpp index 240e043c6..aaadeeede 100644 --- a/src/expr/symbol_manager.cpp +++ b/src/expr/symbol_manager.cpp @@ -417,6 +417,7 @@ const std::string& SymbolManager::getLastSynthName() const void SymbolManager::reset() { + // reset resets the symbol table even when global declarations are true d_symtabAllocated.reset(); d_implementation->reset(); } @@ -424,7 +425,10 @@ void SymbolManager::reset() void SymbolManager::resetAssertions() { d_implementation->resetAssertions(); - d_symtabAllocated.resetAssertions(); + if (!d_globalDeclarations) + { + d_symtabAllocated.resetAssertions(); + } } } // namespace cvc5 diff --git a/src/expr/symbol_table.cpp b/src/expr/symbol_table.cpp index 762120b5b..c74548d97 100644 --- a/src/expr/symbol_table.cpp +++ b/src/expr/symbol_table.cpp @@ -342,18 +342,15 @@ 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() { d_context.pop(); } + ~Implementation() {} - bool bind(const string& name, api::Term obj, bool levelZero, bool doOverload); - void bindType(const string& name, api::Sort t, bool levelZero = false); + bool bind(const string& name, api::Term obj, bool doOverload); + void bindType(const string& name, api::Sort t); void bindType(const string& name, const vector& params, - api::Sort t, - bool levelZero = false); + api::Sort t); bool isBound(const string& name) const; bool isBoundType(const string& name) const; api::Term lookup(const string& name) const; @@ -405,23 +402,18 @@ class SymbolTable::Implementation { bool SymbolTable::Implementation::bind(const string& name, api::Term obj, - bool levelZero, 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; } } - if (levelZero) { - d_exprMap.insertAtContextLevelZero(name, obj); - } else { d_exprMap.insert(name, obj); - } + return true; } @@ -440,21 +432,14 @@ api::Term SymbolTable::Implementation::lookup(const string& name) const } } -void SymbolTable::Implementation::bindType(const string& name, - api::Sort t, - bool levelZero) +void SymbolTable::Implementation::bindType(const string& name, api::Sort t) { - if (levelZero) { - d_typeMap.insertAtContextLevelZero(name, make_pair(vector(), t)); - } else { d_typeMap.insert(name, make_pair(vector(), t)); - } } void SymbolTable::Implementation::bindType(const string& name, const vector& params, - api::Sort t, - bool levelZero) + api::Sort t) { if (Debug.isOn("sort")) { Debug("sort") << "bindType(" << name << ", ["; @@ -466,11 +451,8 @@ void SymbolTable::Implementation::bindType(const string& name, } Debug("sort") << "], " << t << ")" << endl; } - if (levelZero) { - d_typeMap.insertAtContextLevelZero(name, make_pair(params, t)); - } else { + d_typeMap.insert(name, make_pair(params, t)); - } } bool SymbolTable::Implementation::isBoundType(const string& name) const { @@ -542,7 +524,7 @@ size_t SymbolTable::Implementation::lookupArity(const string& name) { void SymbolTable::Implementation::popScope() { // should not pop beyond level one - if (d_context.getLevel() == 1) + if (d_context.getLevel() == 0) { throw ScopeException(); } @@ -627,23 +609,21 @@ SymbolTable::SymbolTable() : d_implementation(new SymbolTable::Implementation()) SymbolTable::~SymbolTable() {} bool SymbolTable::bind(const string& name, api::Term obj, - bool levelZero, bool doOverload) { - return d_implementation->bind(name, obj, levelZero, doOverload); + return d_implementation->bind(name, obj, doOverload); } -void SymbolTable::bindType(const string& name, api::Sort t, bool levelZero) +void SymbolTable::bindType(const string& name, api::Sort t) { - d_implementation->bindType(name, t, levelZero); + d_implementation->bindType(name, t); } void SymbolTable::bindType(const string& name, const vector& params, - api::Sort t, - bool levelZero) + api::Sort t) { - d_implementation->bindType(name, params, t, levelZero); + d_implementation->bindType(name, params, t); } bool SymbolTable::isBound(const string& name) const diff --git a/src/expr/symbol_table.h b/src/expr/symbol_table.h index ddf26f9da..e4a39a8ca 100644 --- a/src/expr/symbol_table.h +++ b/src/expr/symbol_table.h @@ -66,14 +66,12 @@ class CVC5_EXPORT SymbolTable * * @param name an identifier * @param obj the expression to bind to name - * @param levelZero set if the binding must be done at level 0 * @param doOverload set if the binding can overload the function name. * * Returns false if the binding was invalid. */ bool bind(const std::string& name, api::Term obj, - bool levelZero = false, bool doOverload = false); /** @@ -85,9 +83,8 @@ class CVC5_EXPORT SymbolTable * * @param name an identifier * @param t the type to bind to name - * @param levelZero set if the binding must be done at level 0 */ - void bindType(const std::string& name, api::Sort t, bool levelZero = false); + void bindType(const std::string& name, api::Sort t); /** * Bind a type to a name in the current scope. If name @@ -99,13 +96,10 @@ class CVC5_EXPORT SymbolTable * @param name an identifier * @param params the parameters to the type * @param t the type to bind to name - * @param levelZero true to bind it globally (default is to bind it - * locally within the current scope) */ void bindType(const std::string& name, const std::vector& params, - api::Sort t, - bool levelZero = false); + api::Sort t); /** * Check whether a name is bound to an expression with bind(). diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 580c74f0f..6c04a3ad6 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -202,13 +202,11 @@ bool Parser::isPredicate(const std::string& name) { api::Term Parser::bindVar(const std::string& name, const api::Sort& type, - bool levelZero, bool doOverload) { - bool globalDecls = d_symman->getGlobalDeclarations(); Debug("parser") << "bindVar(" << name << ", " << type << ")" << std::endl; api::Term expr = d_solver->mkConst(type, name); - defineVar(name, expr, globalDecls || levelZero, doOverload); + defineVar(name, expr, doOverload); return expr; } @@ -234,12 +232,11 @@ std::vector Parser::bindBoundVars( std::vector Parser::bindVars(const std::vector names, const api::Sort& type, - bool levelZero, bool doOverload) { std::vector vars; for (unsigned i = 0; i < names.size(); ++i) { - vars.push_back(bindVar(names[i], type, levelZero, doOverload)); + vars.push_back(bindVar(names[i], type, doOverload)); } return vars; } @@ -256,11 +253,10 @@ std::vector Parser::bindBoundVars( 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, doOverload)) { std::stringstream ss; ss << "Cannot bind " << name << " to symbol of type " << val.getSort(); @@ -272,7 +268,6 @@ void Parser::defineVar(const std::string& name, void Parser::defineType(const std::string& name, const api::Sort& type, - bool levelZero, bool skipExisting) { if (skipExisting && isDeclared(name, SYM_SORT)) @@ -280,16 +275,15 @@ void Parser::defineType(const std::string& name, Assert(d_symtab->lookupType(name) == type); return; } - d_symtab->bindType(name, type, levelZero); + d_symtab->bindType(name, type); Assert(isDeclared(name, SYM_SORT)); } void Parser::defineType(const std::string& name, const std::vector& params, - const api::Sort& type, - bool levelZero) + const api::Sort& type) { - d_symtab->bindType(name, params, type, levelZero); + d_symtab->bindType(name, params, type); Assert(isDeclared(name, SYM_SORT)); } @@ -314,9 +308,8 @@ void Parser::defineParameterizedType(const std::string& name, api::Sort Parser::mkSort(const std::string& name) { Debug("parser") << "newSort(" << name << ")" << std::endl; - bool globalDecls = d_symman->getGlobalDeclarations(); api::Sort type = d_solver->mkUninterpretedSort(name); - defineType(name, type, globalDecls); + defineType(name, type); return type; } @@ -324,9 +317,8 @@ api::Sort Parser::mkSortConstructor(const std::string& name, size_t arity) { Debug("parser") << "newSortConstructor(" << name << ", " << arity << ")" << std::endl; - bool globalDecls = d_symman->getGlobalDeclarations(); api::Sort type = d_solver->mkSortConstructorSort(name, arity); - defineType(name, vector(arity), type, globalDecls); + defineType(name, vector(arity), type); return type; } @@ -383,7 +375,6 @@ std::vector Parser::bindMutualDatatypeTypes( d_solver->mkDatatypeSorts(datatypes, d_unresolved); Assert(datatypes.size() == types.size()); - bool globalDecls = d_symman->getGlobalDeclarations(); for (unsigned i = 0; i < datatypes.size(); ++i) { api::Sort t = types[i]; @@ -396,11 +387,11 @@ std::vector Parser::bindMutualDatatypeTypes( if (t.isParametricDatatype()) { std::vector paramTypes = t.getDatatypeParamSorts(); - defineType(name, paramTypes, t, globalDecls); + defineType(name, paramTypes, t); } else { - defineType(name, t, globalDecls); + defineType(name, t); } std::unordered_set< std::string > consNames; std::unordered_set< std::string > selNames; @@ -414,7 +405,7 @@ std::vector Parser::bindMutualDatatypeTypes( if(!doOverload) { checkDeclaration(constructorName, CHECK_UNDECLARED); } - defineVar(constructorName, constructor, globalDecls, doOverload); + defineVar(constructorName, constructor, doOverload); consNames.insert(constructorName); }else{ throw ParserException(constructorName + " already declared in this datatype"); @@ -428,7 +419,7 @@ std::vector Parser::bindMutualDatatypeTypes( { checkDeclaration(testerName, CHECK_UNDECLARED); } - defineVar(testerName, tester, globalDecls, doOverload); + defineVar(testerName, tester, doOverload); } for (size_t k = 0, nargs = ctor.getNumSelectors(); k < nargs; k++) { @@ -440,7 +431,7 @@ std::vector Parser::bindMutualDatatypeTypes( if(!doOverload) { checkDeclaration(selectorName, CHECK_UNDECLARED); } - defineVar(selectorName, selector, globalDecls, doOverload); + defineVar(selectorName, selector, doOverload); selNames.insert(selectorName); }else{ throw ParserException(selectorName + " already declared in this datatype"); diff --git a/src/parser/parser.h b/src/parser/parser.h index 43edbf299..6781fc4f9 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -389,9 +389,6 @@ public: void checkFunctionLike(api::Term fun); /** Create a new cvc5 variable expression of the given type. - * - * 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. @@ -400,15 +397,11 @@ public: */ api::Term bindVar(const std::string& name, const api::Sort& type, - bool levelZero = false, bool doOverload = false); /** * Create a set of new cvc5 variable expressions of the given type. * - * 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 @@ -416,7 +409,6 @@ public: */ std::vector bindVars(const std::vector names, const api::Sort& type, - bool levelZero = false, bool doOverload = false); /** @@ -444,7 +436,6 @@ public: const api::Sort& type); /** 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, * then if doOverload is true, we create overloaded operators. * else if doOverload is false, the existing expression is shadowed by the @@ -452,7 +443,6 @@ public: */ void defineVar(const std::string& name, const api::Term& val, - bool levelZero = false, bool doOverload = false); /** @@ -460,15 +450,12 @@ public: * * @param name The name of the type * @param type The type that should be associated with the name - * @param levelZero If true, the type definition is considered global and - * cannot be removed by popping the user context * @param skipExisting If true, the type definition is ignored if the same * symbol has already been defined. It is assumed that * the definition is the exact same as the existing one. */ void defineType(const std::string& name, const api::Sort& type, - bool levelZero = false, bool skipExisting = false); /** @@ -477,13 +464,10 @@ public: * @param name The name of the type * @param params The type parameters * @param type The type that should be associated with the name - * @param levelZero If true, the type definition is considered global and - * cannot be removed by poppoing the user context */ void defineType(const std::string& name, const std::vector& params, - const api::Sort& type, - bool levelZero = false); + const api::Sort& type); /** Create a new type definition (e.g., from an SMT-LIBv2 define-sort). */ void defineParameterizedType(const std::string& name, diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index e19a78c84..355a3469e 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -287,7 +287,7 @@ command [std::unique_ptr* cmd] else { api::Term func = - PARSER_STATE->bindVar(name, t, false, true); + PARSER_STATE->bindVar(name, t, true); cmd->reset(new DeclareFunctionCommand(name, func, t)); } } @@ -781,7 +781,7 @@ smt25Command[std::unique_ptr* cmd] "version 2.0"); } api::Term c = - PARSER_STATE->bindVar(name, t, false, true); + PARSER_STATE->bindVar(name, t, true); cmd->reset(new DeclareFunctionCommand(name, c, t)); } /* get model */ @@ -947,7 +947,7 @@ extendedCommand[std::unique_ptr* cmd] } // allow overloading api::Term func = - PARSER_STATE->bindVar(name, tt, false, true); + PARSER_STATE->bindVar(name, tt, true); seq->addCommand(new DeclareFunctionCommand(name, func, tt)); sorts.clear(); } @@ -967,7 +967,7 @@ extendedCommand[std::unique_ptr* cmd] } // allow overloading api::Term func = - PARSER_STATE->bindVar(name, t, false, true); + PARSER_STATE->bindVar(name, t, true); seq->addCommand(new DeclareFunctionCommand(name, func, t)); sorts.clear(); } diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 0f0e3060c..ec83dff0b 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -277,9 +277,9 @@ void Smt2::addSepOperators() { void Smt2::addCoreSymbols() { - defineType("Bool", d_solver->getBooleanSort(), true, true); - defineVar("true", d_solver->mkTrue(), true, true); - defineVar("false", d_solver->mkFalse(), true, true); + defineType("Bool", d_solver->getBooleanSort(), true); + defineVar("true", d_solver->mkTrue(), true); + defineVar("false", d_solver->mkFalse(), true); addOperator(api::AND, "and"); addOperator(api::DISTINCT, "distinct"); addOperator(api::EQUAL, "="); @@ -410,7 +410,7 @@ api::Term Smt2::bindDefineFunRec( api::Sort ft = mkFlatFunctionType(sorts, t, flattenVars); // allow overloading - return bindVar(fname, ft, false, true); + return bindVar(fname, ft, true); } void Smt2::pushDefineFunRecScope( @@ -513,7 +513,7 @@ Command* Smt2::setLogic(std::string name, bool fromCommand) if(d_logic.isTheoryEnabled(theory::THEORY_ARITH)) { if(d_logic.areIntegersUsed()) { - defineType("Int", d_solver->getIntegerSort(), true, true); + defineType("Int", d_solver->getIntegerSort(), true); addArithmeticOperators(); if (!strictModeEnabled() || !d_logic.isLinear()) { @@ -526,7 +526,7 @@ Command* Smt2::setLogic(std::string name, bool fromCommand) if (d_logic.areRealsUsed()) { - defineType("Real", d_solver->getRealSort(), true, true); + defineType("Real", d_solver->getRealSort(), true); addArithmeticOperators(); addOperator(api::DIVISION, "/"); if (!strictModeEnabled()) @@ -577,7 +577,7 @@ Command* Smt2::setLogic(std::string name, bool fromCommand) if(d_logic.isTheoryEnabled(theory::THEORY_DATATYPES)) { const std::vector types; - defineType("Tuple", d_solver->mkTupleSort(types), true, true); + defineType("Tuple", d_solver->mkTupleSort(types), true); addDatatypesOperators(); } @@ -632,9 +632,9 @@ Command* Smt2::setLogic(std::string name, bool fromCommand) addOperator(api::TABLE_PRODUCT, "table.product"); } if(d_logic.isTheoryEnabled(theory::THEORY_STRINGS)) { - defineType("String", d_solver->getStringSort(), true, true); - defineType("RegLan", d_solver->getRegExpSort(), true, true); - defineType("Int", d_solver->getIntegerSort(), true, true); + defineType("String", d_solver->getStringSort(), true); + defineType("RegLan", d_solver->getRegExpSort(), true); + defineType("Int", d_solver->getIntegerSort(), true); defineVar("re.none", d_solver->mkRegexpNone()); defineVar("re.allchar", d_solver->mkRegexpAllchar()); @@ -651,11 +651,11 @@ Command* Smt2::setLogic(std::string name, bool fromCommand) } if (d_logic.isTheoryEnabled(theory::THEORY_FP)) { - defineType("RoundingMode", d_solver->getRoundingModeSort(), true, true); - defineType("Float16", d_solver->mkFloatingPointSort(5, 11), true, true); - defineType("Float32", d_solver->mkFloatingPointSort(8, 24), true, true); - defineType("Float64", d_solver->mkFloatingPointSort(11, 53), true, true); - defineType("Float128", d_solver->mkFloatingPointSort(15, 113), true, true); + defineType("RoundingMode", d_solver->getRoundingModeSort(), true); + defineType("Float16", d_solver->mkFloatingPointSort(5, 11), true); + defineType("Float32", d_solver->mkFloatingPointSort(8, 24), true); + defineType("Float64", d_solver->mkFloatingPointSort(11, 53), true); + defineType("Float128", d_solver->mkFloatingPointSort(15, 113), true); defineVar("RNE", d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_EVEN)); defineVar("roundNearestTiesToEven", @@ -681,6 +681,10 @@ Command* Smt2::setLogic(std::string name, bool fromCommand) addSepOperators(); } + // builtin symbols of the logic are declared at context level zero, hence + // we push the outermost scope here + pushScope(true); + std::string logic = sygus() ? d_logic.getLogicString() : name; if (!fromCommand) { diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp index b8f25c66e..37ef05f7f 100644 --- a/src/parser/tptp/tptp.cpp +++ b/src/parser/tptp/tptp.cpp @@ -240,20 +240,34 @@ api::Term Tptp::parseOpToExpr(ParseOp& p) // if it has a kind, it's a builtin one and this function should not have been // called Assert(p.d_kind == api::NULL_EXPR); - if (isDeclared(p.d_name)) - { // already appeared - expr = getVariable(p.d_name); - } - else + expr = isTptpDeclared(p.d_name); + if (expr.isNull()) { api::Sort t = p.d_type == d_solver->getBooleanSort() ? p.d_type : d_unsorted; - expr = bindVar(p.d_name, t, true); // must define at level zero + expr = bindVar(p.d_name, t); // must define at level zero + d_auxSymbolTable[p.d_name] = expr; preemptCommand(new DeclareFunctionCommand(p.d_name, expr, t)); } return expr; } +api::Term Tptp::isTptpDeclared(const std::string& name) +{ + if (isDeclared(name)) + { // already appeared + return getVariable(name); + } + std::unordered_map::iterator it = + d_auxSymbolTable.find(name); + if (it != d_auxSymbolTable.end()) + { + return it->second; + } + // otherwise null + return api::Term(); +} + api::Term Tptp::applyParseOp(ParseOp& p, std::vector& args) { if (Debug.isOn("parser")) @@ -281,18 +295,15 @@ api::Term Tptp::applyParseOp(ParseOp& p, std::vector& args) if (p.d_kind == api::NULL_EXPR) { // A non-built-in function application, get the expression - api::Term v; - if (isDeclared(p.d_name)) - { // already appeared - v = getVariable(p.d_name); - } - else + api::Term v = isTptpDeclared(p.d_name); + if (v.isNull()) { std::vector sorts(args.size(), d_unsorted); 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, true); // must define at level zero + v = bindVar(p.d_name, t); // must define at level zero + d_auxSymbolTable[p.d_name] = v; 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.h b/src/parser/tptp/tptp.h index 2167a6c38..f765bfb2f 100644 --- a/src/parser/tptp/tptp.h +++ b/src/parser/tptp/tptp.h @@ -183,6 +183,8 @@ class Tptp : public Parser { private: void addArithmeticOperators(); + /** is the name declared, if so, return the term for that name */ + api::Term isTptpDeclared(const std::string& name); // In CNF variable are implicitly binded // d_freevar collect them @@ -194,6 +196,13 @@ class Tptp : public Parser { // The set of expression that already have a bridge std::unordered_set d_r_converted; std::unordered_map d_distinct_objects; + /** + * TPTP automatically declares symbols as they are parsed inline. This + * requires using an auxiliary symbol table for such symbols. This must be + * independent of the main symbol table which is aware of quantifier + * scopes. + */ + std::unordered_map d_auxSymbolTable; std::vector< pANTLR3_INPUT_STREAM > d_in_created; diff --git a/test/unit/context/cdhashmap_black.cpp b/test/unit/context/cdhashmap_black.cpp index c4d744914..a4060e1f8 100644 --- a/test/unit/context/cdhashmap_black.cpp +++ b/test/unit/context/cdhashmap_black.cpp @@ -75,11 +75,10 @@ TEST_F(TestContextBlackCDHashMap, simple_sequence) d_context->push(); ASSERT_TRUE(elements_are(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}})); - map.insertAtContextLevelZero(23, 317); map.insert(1, 45); ASSERT_TRUE( - elements_are(map, {{1, 45}, {3, 4}, {5, 6}, {9, 8}, {23, 317}})); + elements_are(map, {{1, 45}, {3, 4}, {5, 6}, {9, 8}})); map.insert(23, 324); ASSERT_TRUE( @@ -88,15 +87,15 @@ TEST_F(TestContextBlackCDHashMap, simple_sequence) } ASSERT_TRUE( - elements_are(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}, {23, 317}})); + elements_are(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}})); d_context->pop(); } - ASSERT_TRUE(elements_are(map, {{3, 4}, {5, 6}, {9, 8}, {23, 317}})); + ASSERT_TRUE(elements_are(map, {{3, 4}, {5, 6}, {9, 8}})); d_context->pop(); } - ASSERT_TRUE(elements_are(map, {{3, 4}, {23, 317}})); + ASSERT_TRUE(elements_are(map, {{3, 4}})); } TEST_F(TestContextBlackCDHashMap, simple_sequence_fewer_finds) @@ -155,15 +154,9 @@ TEST_F(TestContextBlackCDHashMap, insert_at_context_level_zero) ASSERT_TRUE(elements_are(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}})); - map.insertAtContextLevelZero(23, 317); - ASSERT_TRUE( - elements_are(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}, {23, 317}})); + elements_are(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}})); - ASSERT_DEATH(map.insertAtContextLevelZero(23, 317), - "insertAtContextLevelZero"); - ASSERT_DEATH(map.insertAtContextLevelZero(23, 472), - "insertAtContextLevelZero"); map.insert(23, 472); ASSERT_TRUE( @@ -174,8 +167,6 @@ TEST_F(TestContextBlackCDHashMap, insert_at_context_level_zero) ASSERT_TRUE( elements_are(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}, {23, 472}})); - ASSERT_DEATH(map.insertAtContextLevelZero(23, 0), - "insertAtContextLevelZero"); map.insert(23, 1024); ASSERT_TRUE( @@ -187,19 +178,15 @@ TEST_F(TestContextBlackCDHashMap, insert_at_context_level_zero) d_context->pop(); } - ASSERT_TRUE(elements_are(map, {{3, 4}, {5, 6}, {9, 8}, {23, 317}})); + ASSERT_TRUE(elements_are(map, {{3, 4}, {5, 6}, {9, 8}})); - ASSERT_DEATH(map.insertAtContextLevelZero(23, 0), - "insertAtContextLevelZero"); map.insert(23, 477); ASSERT_TRUE(elements_are(map, {{3, 4}, {5, 6}, {9, 8}, {23, 477}})); d_context->pop(); } - ASSERT_DEATH(map.insertAtContextLevelZero(23, 0), "insertAtContextLevelZero"); - - ASSERT_TRUE(elements_are(map, {{3, 4}, {23, 317}})); + ASSERT_TRUE(elements_are(map, {{3, 4}})); } } // namespace test } // namespace cvc5 -- 2.30.2