From: Andres Noetzli Date: Mon, 27 Jun 2022 22:28:27 +0000 (-0700) Subject: Move `SymbolManager` and `SymbolTable` to parser (#8910) X-Git-Tag: cvc5-1.0.1~30 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=55d024accae4abf992c9585961bd0765d9eef2ab;p=cvc5.git Move `SymbolManager` and `SymbolTable` to parser (#8910) This moves `SymbolManager` and `SymbolTable` to the parser. To do so, it modifies headers in the `context` package to be public to the parser (changes `cvc5_private.h` to `cvc5parser_public.h`), because they are shared between the parser and the main library. --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 4150c9646..5b88c64b8 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -56,6 +56,18 @@ libcvc5_add_sources( options/options_handler.h options/options_listener.h options/options_public.h + # !!! TEMPORARY !!! + # We currently add the symbol manager and the symbol table to both libcvc5 + # and libcvc5parser as a stopgap solution, because the command infrastructure + # is still in libcvc5. Once PR #8893 is merged, they can be removed from + # libcvc5. We have to add them to libcvc5 because linking a DLL for Windows + # requires all symbols to be present. Concretely, because of the commands, we + # need the symbols for the symbol manager/table to link libcvc5. + parser/api/cpp/symbol_manager.cpp + parser/api/cpp/symbol_manager.h + parser/symbol_table.cpp + parser/symbol_table.h + # !!! /TEMPORARY !!! preprocessing/assertion_pipeline.cpp preprocessing/assertion_pipeline.h preprocessing/learned_literal_manager.cpp diff --git a/src/context/cdhashmap.h b/src/context/cdhashmap.h index c590097ca..1fc1761b9 100644 --- a/src/context/cdhashmap.h +++ b/src/context/cdhashmap.h @@ -78,7 +78,7 @@ * possible. */ -#include "cvc5_private.h" +#include "cvc5parser_public.h" #ifndef CVC5__CONTEXT__CDHASHMAP_H #define CVC5__CONTEXT__CDHASHMAP_H diff --git a/src/context/cdhashset.h b/src/context/cdhashset.h index d9605b902..5497a51fe 100644 --- a/src/context/cdhashset.h +++ b/src/context/cdhashset.h @@ -13,7 +13,7 @@ * Context-dependent set class. */ -#include "cvc5_private.h" +#include "cvc5parser_public.h" #ifndef CVC5__CONTEXT__CDHASHSET_H #define CVC5__CONTEXT__CDHASHSET_H diff --git a/src/context/cdinsert_hashmap.h b/src/context/cdinsert_hashmap.h index 7415a0a56..387f9e986 100644 --- a/src/context/cdinsert_hashmap.h +++ b/src/context/cdinsert_hashmap.h @@ -30,6 +30,11 @@ * - Does not accept TNodes as keys. */ +#include "cvc5parser_public.h" + +#ifndef CVC5__CONTEXT__CDINSERT_HASHMAP_H +#define CVC5__CONTEXT__CDINSERT_HASHMAP_H + #include #include #include @@ -39,12 +44,15 @@ #include "base/output.h" #include "context/cdinsert_hashmap_forward.h" #include "context/context.h" -#include "cvc5_private.h" -#include "expr/node.h" -#pragma once +namespace cvc5 { -namespace cvc5::context { +namespace internal { +template +class NodeTemplate; +} + +namespace context { template > class InsertHashMap { @@ -347,7 +355,8 @@ public: };/* class CDInsertHashMap<> */ template -class CDInsertHashMap : public ContextObj +class CDInsertHashMap, Data, HashFcn> + : public ContextObj { /* CDInsertHashMap is challenging to get working with TNode. * Consider using CDHashMap instead. @@ -364,4 +373,7 @@ class CDInsertHashMap : public ContextObj "Cannot create a CDInsertHashMap with TNode keys"); }; -} // namespace cvc5::context +} // namespace context +} // namespace cvc5 + +#endif diff --git a/src/context/cdlist.h b/src/context/cdlist.h index 5bff83265..dde9a1198 100644 --- a/src/context/cdlist.h +++ b/src/context/cdlist.h @@ -15,7 +15,7 @@ * simply shortened. */ -#include "cvc5_private.h" +#include "cvc5parser_public.h" #ifndef CVC5__CONTEXT__CDLIST_H #define CVC5__CONTEXT__CDLIST_H diff --git a/src/context/cdo.h b/src/context/cdo.h index 4f33e99c0..4af7f68b5 100644 --- a/src/context/cdo.h +++ b/src/context/cdo.h @@ -13,7 +13,7 @@ * A context-dependent object. */ -#include "cvc5_private.h" +#include "cvc5parser_public.h" #ifndef CVC5__CONTEXT__CDO_H #define CVC5__CONTEXT__CDO_H diff --git a/src/context/context.h b/src/context/context.h index 1aa4bb0bc..76b8b12a9 100644 --- a/src/context/context.h +++ b/src/context/context.h @@ -13,7 +13,7 @@ * Context class and context manager. */ -#include "cvc5_private.h" +#include "cvc5parser_public.h" #ifndef CVC5__CONTEXT__CONTEXT_H #define CVC5__CONTEXT__CONTEXT_H @@ -62,8 +62,8 @@ std::ostream& operator<<(std::ostream&, const Scope&); * ContextMemoryManager. A copy is stored in each Scope object for quick * access. */ -class Context { - +class CVC5_EXPORT Context +{ /** * Pointer to the ContextMemoryManager for this Context. */ @@ -192,8 +192,7 @@ public: */ void addNotifyObjPost(ContextNotifyObj* pCNO); -};/* class Context */ - +}; /* class Context */ /** * A UserContext is different from a Context only because it's used for @@ -421,7 +420,8 @@ class Scope { * argument as the special constructor in this class (and pass it * on to all ContextObj instances). */ -class ContextObj { +class CVC5_EXPORT ContextObj +{ /** * Pointer to Scope in which this object was last modified. */ @@ -647,7 +647,7 @@ class ContextObj { */ void enqueueToGarbageCollect(); -};/* class ContextObj */ +}; /* class ContextObj */ /** * For more flexible context-dependent behavior than that provided by diff --git a/src/context/context_mm.h b/src/context/context_mm.h index 4c063553f..55cc04bb6 100644 --- a/src/context/context_mm.h +++ b/src/context/context_mm.h @@ -15,7 +15,7 @@ * Designed for use by ContextManager. */ -#include "cvc5_private.h" +#include "cvc5parser_public.h" #ifndef CVC5__CONTEXT__CONTEXT_MM_H #define CVC5__CONTEXT__CONTEXT_MM_H @@ -25,6 +25,8 @@ #endif #include +#include "cvc5_export.h" + namespace cvc5::context { #ifndef CVC5_DEBUG_CONTEXT_MEMORY_MANAGER @@ -39,8 +41,8 @@ namespace cvc5::context { * releases the new region and restores the top region from the stack. * */ -class ContextMemoryManager { - +class CVC5_EXPORT ContextMemoryManager +{ /** * Memory in regions is allocated in chunks. This is the chunk size */ @@ -146,7 +148,7 @@ class ContextMemoryManager { */ void pop(); -};/* class ContextMemoryManager */ +}; /* class ContextMemoryManager */ #else /* CVC5_DEBUG_CONTEXT_MEMORY_MANAGER */ diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index 9462b7cdf..c26b683c2 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -72,10 +72,6 @@ libcvc5_add_sources( skolem_manager.h subtype_elim_node_converter.cpp subtype_elim_node_converter.h - symbol_manager.cpp - symbol_manager.h - symbol_table.cpp - symbol_table.h term_canonize.cpp term_canonize.h term_context.cpp diff --git a/src/expr/symbol_manager.cpp b/src/expr/symbol_manager.cpp deleted file mode 100644 index 3e8cf3207..000000000 --- a/src/expr/symbol_manager.cpp +++ /dev/null @@ -1,439 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Andrew Reynolds, Mathias Preiner, Andres Noetzli - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * The symbol manager. - */ - -#include "expr/symbol_manager.h" - -#include "context/cdhashmap.h" -#include "context/cdhashset.h" -#include "context/cdlist.h" -#include "context/cdo.h" - -using namespace cvc5::context; - -namespace cvc5 { - -// ---------------------------------------------- SymbolManager::Implementation - -class SymbolManager::Implementation -{ - using TermStringMap = - CDHashMap>; - using TermSet = CDHashSet>; - using SortList = CDList; - using TermList = CDList; - - public: - Implementation() - : d_context(), - d_names(&d_context), - d_namedAsserts(&d_context), - d_declareSorts(&d_context), - d_declareTerms(&d_context), - d_funToSynth(&d_context), - d_hasPushedScope(&d_context, false), - d_lastSynthName(&d_context) - { - // use an outermost push, to be able to clear all definitions - d_context.push(); - } - - ~Implementation() { d_context.pop(); } - /** set expression name */ - NamingResult setExpressionName(cvc5::Term t, - const std::string& name, - bool isAssertion = false); - /** get expression name */ - bool getExpressionName(cvc5::Term t, - std::string& name, - bool isAssertion = false) const; - /** get expression names */ - void getExpressionNames(const std::vector& ts, - std::vector& names, - bool areAssertions = false) const; - /** get expression names */ - std::map getExpressionNames( - bool areAssertions) const; - /** get model declare sorts */ - std::vector getModelDeclareSorts() const; - /** get model declare terms */ - std::vector getModelDeclareTerms() const; - /** get functions to synthesize */ - std::vector getFunctionsToSynthesize() const; - /** Add declared sort to the list of model declarations. */ - void addModelDeclarationSort(cvc5::Sort s); - /** Add declared term to the list of model declarations. */ - void addModelDeclarationTerm(cvc5::Term t); - /** Add function to the list of functions to synthesize. */ - void addFunctionToSynthesize(cvc5::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; - /** Set the last abduct-to-synthesize had the given name. */ - void setLastSynthName(const std::string& name); - /** Get the name of the last abduct-to-synthesize */ - const std::string& getLastSynthName() const; - - private: - /** The context manager for the scope maps. */ - Context d_context; - /** Map terms to names */ - TermStringMap d_names; - /** The set of terms with assertion names */ - TermSet d_namedAsserts; - /** Declared sorts (for model printing) */ - SortList d_declareSorts; - /** Declared terms (for model printing) */ - TermList d_declareTerms; - /** Functions to synthesize (for response to check-synth) */ - TermList d_funToSynth; - /** - * Have we pushed a scope (e.g. a let or quantifier) in the current context? - */ - CDO d_hasPushedScope; - /** The last abduct or interpolant to synthesize name */ - CDO d_lastSynthName; -}; - -NamingResult SymbolManager::Implementation::setExpressionName( - cvc5::Term t, const std::string& name, bool isAssertion) -{ - Trace("sym-manager") << "SymbolManager: set expression name: " << t << " -> " - << name << ", isAssertion=" << isAssertion << std::endl; - if (d_hasPushedScope.get()) - { - // cannot name subexpressions under binders - return NamingResult::ERROR_IN_BINDER; - } - - if (isAssertion) - { - d_namedAsserts.insert(t); - } - if (d_names.find(t) != d_names.end()) - { - // already named assertion - return NamingResult::ERROR_ALREADY_NAMED; - } - d_names[t] = name; - return NamingResult::SUCCESS; -} - -bool SymbolManager::Implementation::getExpressionName(cvc5::Term t, - std::string& name, - bool isAssertion) const -{ - TermStringMap::const_iterator it = d_names.find(t); - if (it == d_names.end()) - { - return false; - } - if (isAssertion) - { - // must be an assertion name - if (d_namedAsserts.find(t) == d_namedAsserts.end()) - { - return false; - } - } - name = (*it).second; - return true; -} - -void SymbolManager::Implementation::getExpressionNames( - const std::vector& ts, - std::vector& names, - bool areAssertions) const -{ - for (const cvc5::Term& t : ts) - { - std::string name; - if (getExpressionName(t, name, areAssertions)) - { - names.push_back(name); - } - } -} - -std::map -SymbolManager::Implementation::getExpressionNames(bool areAssertions) const -{ - std::map emap; - for (TermStringMap::const_iterator it = d_names.begin(), - itend = d_names.end(); - it != itend; - ++it) - { - cvc5::Term t = (*it).first; - if (areAssertions && d_namedAsserts.find(t) == d_namedAsserts.end()) - { - continue; - } - emap[t] = (*it).second; - } - return emap; -} - -std::vector SymbolManager::Implementation::getModelDeclareSorts() - const -{ - std::vector declareSorts(d_declareSorts.begin(), - d_declareSorts.end()); - return declareSorts; -} - -std::vector SymbolManager::Implementation::getModelDeclareTerms() - const -{ - std::vector declareTerms(d_declareTerms.begin(), - d_declareTerms.end()); - return declareTerms; -} - -std::vector -SymbolManager::Implementation::getFunctionsToSynthesize() const -{ - return std::vector(d_funToSynth.begin(), d_funToSynth.end()); -} - -void SymbolManager::Implementation::addModelDeclarationSort(cvc5::Sort s) -{ - Trace("sym-manager") << "SymbolManager: addModelDeclarationSort " << s - << std::endl; - d_declareSorts.push_back(s); -} - -void SymbolManager::Implementation::addModelDeclarationTerm(cvc5::Term t) -{ - Trace("sym-manager") << "SymbolManager: addModelDeclarationTerm " << t - << std::endl; - d_declareTerms.push_back(t); -} - -void SymbolManager::Implementation::addFunctionToSynthesize(cvc5::Term f) -{ - Trace("sym-manager") << "SymbolManager: addFunctionToSynthesize " << f - << std::endl; - d_funToSynth.push_back(f); -} - -void SymbolManager::Implementation::pushScope(bool isUserContext) -{ - 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(); - if (!isUserContext) - { - d_hasPushedScope = true; - } -} - -void SymbolManager::Implementation::popScope() -{ - Trace("sym-manager") << "SymbolManager: popScope" << std::endl; - if (d_context.getLevel() == 0) - { - throw internal::ScopeException(); - } - d_context.pop(); - Trace("sym-manager-debug") - << "d_hasPushedScope is now " << d_hasPushedScope.get() << std::endl; -} - -bool SymbolManager::Implementation::hasPushedScope() const -{ - return d_hasPushedScope.get(); -} - -void SymbolManager::Implementation::setLastSynthName(const std::string& name) -{ - d_lastSynthName = name; -} - -const std::string& SymbolManager::Implementation::getLastSynthName() const -{ - return d_lastSynthName.get(); -} - -void SymbolManager::Implementation::reset() -{ - 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 - -SymbolManager::SymbolManager(cvc5::Solver* s) - : d_solver(s), - d_implementation(new SymbolManager::Implementation()), - d_globalDeclarations(false) -{ -} - -SymbolManager::~SymbolManager() {} - -internal::SymbolTable* SymbolManager::getSymbolTable() -{ - return &d_symtabAllocated; -} - -NamingResult SymbolManager::setExpressionName(cvc5::Term t, - const std::string& name, - bool isAssertion) -{ - return d_implementation->setExpressionName(t, name, isAssertion); -} - -bool SymbolManager::getExpressionName(cvc5::Term t, - std::string& name, - bool isAssertion) const -{ - return d_implementation->getExpressionName(t, name, isAssertion); -} - -void SymbolManager::getExpressionNames(const std::vector& ts, - std::vector& names, - bool areAssertions) const -{ - return d_implementation->getExpressionNames(ts, names, areAssertions); -} - -std::map SymbolManager::getExpressionNames( - bool areAssertions) const -{ - return d_implementation->getExpressionNames(areAssertions); -} -std::vector SymbolManager::getModelDeclareSorts() const -{ - return d_implementation->getModelDeclareSorts(); -} -std::vector SymbolManager::getModelDeclareTerms() const -{ - return d_implementation->getModelDeclareTerms(); -} - -std::vector SymbolManager::getFunctionsToSynthesize() const -{ - return d_implementation->getFunctionsToSynthesize(); -} - -void SymbolManager::addModelDeclarationSort(cvc5::Sort s) -{ - d_implementation->addModelDeclarationSort(s); -} - -void SymbolManager::addModelDeclarationTerm(cvc5::Term t) -{ - d_implementation->addModelDeclarationTerm(t); -} - -void SymbolManager::addFunctionToSynthesize(cvc5::Term f) -{ - d_implementation->addFunctionToSynthesize(f); -} - -size_t SymbolManager::scopeLevel() const -{ - return d_symtabAllocated.getLevel(); -} - -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(); -} - -void SymbolManager::setGlobalDeclarations(bool flag) -{ - d_globalDeclarations = flag; -} - -bool SymbolManager::getGlobalDeclarations() const -{ - return d_globalDeclarations; -} - -void SymbolManager::setLastSynthName(const std::string& name) -{ - d_implementation->setLastSynthName(name); -} - -const std::string& SymbolManager::getLastSynthName() const -{ - return d_implementation->getLastSynthName(); -} - -void SymbolManager::reset() -{ - // reset resets the symbol table even when global declarations are true - d_symtabAllocated.reset(); - d_implementation->reset(); -} - -void SymbolManager::resetAssertions() -{ - d_implementation->resetAssertions(); - if (!d_globalDeclarations) - { - d_symtabAllocated.resetAssertions(); - } -} - -} // namespace cvc5 diff --git a/src/expr/symbol_manager.h b/src/expr/symbol_manager.h deleted file mode 100644 index 3fbb3375c..000000000 --- a/src/expr/symbol_manager.h +++ /dev/null @@ -1,194 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Andrew Reynolds, Mathias Preiner, Andres Noetzli - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * The symbol manager. - */ - -#include "cvc5_public.h" - -#ifndef CVC5__EXPR__SYMBOL_MANAGER_H -#define CVC5__EXPR__SYMBOL_MANAGER_H - -#include -#include -#include - -#include "api/cpp/cvc5.h" -#include "cvc5_export.h" -#include "expr/symbol_table.h" - -namespace cvc5 { - -/** Represents the result of a call to `setExpressionName()`. */ -enum class NamingResult -{ - /** The expression name was set successfully. */ - SUCCESS, - /** The expression already has a name. */ - ERROR_ALREADY_NAMED, - /** The expression is in a binder. */ - ERROR_IN_BINDER -}; - -/** - * Symbol manager, which manages: - * (1) The symbol table used by the parser, - * (2) Information related to the (! ... :named s) feature in SMT-LIB version 2. - * - * Like SymbolTable, this class currently lives in src/expr/ since it uses - * context-dependent data structures. - */ -class CVC5_EXPORT SymbolManager -{ - public: - SymbolManager(cvc5::Solver* s); - ~SymbolManager(); - /** Get the underlying symbol table */ - internal::SymbolTable* getSymbolTable(); - //---------------------------- named expressions - /** Set name of term t to name - * - * @param t The term to name - * @param name The given name - * @param isAssertion Whether t is being given a name in an assertion - * context. In particular, this is true if and only if there was an assertion - * command of the form (assert (! t :named name)). - * @return true if the name was set. This method may return false if t - * already has a name. - */ - NamingResult setExpressionName(cvc5::Term t, - const std::string& name, - bool isAssertion = false); - /** Get name for term t - * - * @param t The term - * @param name The argument to update with the name of t - * @param isAssertion Whether we only wish to get the assertion name of t - * @return true if t has a name. If so, name is updated to that name. - * Otherwise, name is unchanged. - */ - bool getExpressionName(cvc5::Term t, - std::string& name, - bool isAssertion = false) const; - /** - * Convert list of terms to list of names. This adds to names the names of - * all terms in ts that has names. Terms that do not have names are not - * included. - * - * Notice that we do not distinguish what terms among those in ts have names. - * If the caller of this method wants more fine-grained information about what - * specific terms had names, then use the more fine grained interface above, - * per term. - * - * @param ts The terms - * @param names The name list - * @param areAssertions Whether we only wish to include assertion names - */ - void getExpressionNames(const std::vector& ts, - std::vector& names, - bool areAssertions = false) const; - /** - * Get a mapping of all expression names. - * - * @param areAssertions Whether we only wish to include assertion names - * @return the mapping containing all expression names. - */ - std::map getExpressionNames( - bool areAssertions = false) const; - /** - * @return The sorts we have declared that should be printed in the model. - */ - std::vector getModelDeclareSorts() const; - /** - * @return The terms we have declared that should be printed in the model. - */ - std::vector getModelDeclareTerms() const; - /** - * @return The functions we have declared that should be printed in a response - * to check-synth. - */ - std::vector getFunctionsToSynthesize() const; - /** - * Add declared sort to the list of model declarations. - */ - void addModelDeclarationSort(cvc5::Sort s); - /** - * Add declared term to the list of model declarations. - */ - void addModelDeclarationTerm(cvc5::Term t); - /** - * Add a function to synthesize. This ensures the solution for f is printed - * in a successful response to check-synth. - */ - void addFunctionToSynthesize(cvc5::Term f); - - //---------------------------- end named expressions - /** - * Get the scope level of the symbol table. - */ - size_t scopeLevel() const; - /** - * Push a scope in the symbol table. - * - * @param isUserContext If true, this push is denoting a push of the user - * context, e.g. via an smt2 push/pop command. Otherwise, this push is - * due to a let/quantifier binding. - */ - void pushScope(bool isUserContext); - /** - * Pop a scope in the symbol table. - */ - void popScope(); - /** - * 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. */ - bool getGlobalDeclarations() const; - /** - * Set the last abduct or interpolant to synthesize had the given name. This - * is required since e.g. get-abduct-next must know the name of the - * abduct-to-synthesize to print its result. For example, the sequence: - * (get-abduct A ) - * (get-abduct-next) - * The latter command must know the symbol "A". - */ - void setLastSynthName(const std::string& name); - /** Get the name of the last abduct or interpolant to synthesize */ - const std::string& getLastSynthName() const; - - private: - /** The API Solver object. */ - cvc5::Solver* d_solver; - /** - * The declaration scope that is "owned" by this symbol manager. - */ - internal::SymbolTable d_symtabAllocated; - /** The implementation of the symbol manager */ - class Implementation; - std::unique_ptr d_implementation; - /** - * Whether the global declarations option is enabled. This corresponds to the - * SMT-LIB option :global-declarations. By default, its value is false. - */ - bool d_globalDeclarations; -}; - -} // namespace cvc5 - -#endif /* CVC5__EXPR__SYMBOL_MANAGER_H */ diff --git a/src/expr/symbol_table.cpp b/src/expr/symbol_table.cpp deleted file mode 100644 index b3977f12e..000000000 --- a/src/expr/symbol_table.cpp +++ /dev/null @@ -1,655 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Andrew Reynolds, Mathias Preiner, Tim King - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * Convenience class for scoping variable and type declarations - * (implementation). - */ - -#include "expr/symbol_table.h" - -#include -#include -#include -#include - -#include "api/cpp/cvc5.h" -#include "context/cdhashmap.h" -#include "context/cdhashset.h" -#include "context/context.h" - -namespace cvc5::internal { - -using context::CDHashMap; -using context::CDHashSet; -using context::Context; -using std::copy; -using std::endl; -using std::ostream_iterator; -using std::pair; -using std::string; -using std::vector; - -/** Overloaded type trie. - * - * This data structure stores a trie of expressions with - * the same name, and must be distinguished by their argument types. - * It is context-dependent. - * - * Using the argument allowFunVariants, - * it may either be configured to allow function variants or not, - * where a function variant is function that expects the same - * argument types as another. - * - * For example, the following definitions introduce function - * variants for the symbol f: - * - * 1. (declare-fun f (Int) Int) and - * (declare-fun f (Int) Bool) - * - * 2. (declare-fun f (Int) Int) and - * (declare-fun f (Int) Int) - * - * 3. (declare-datatypes ((Tup 0)) ((f (data Int)))) and - * (declare-fun f (Int) Tup) - * - * 4. (declare-datatypes ((Tup 0)) ((mkTup (f Int)))) and - * (declare-fun f (Tup) Bool) - * - * If function variants is set to true, we allow function variants - * but not function redefinition. In examples 2 and 3, f is - * declared twice as a symbol of identical argument and range - * types. We never accept these definitions. However, we do - * allow examples 1 and 4 above when allowFunVariants is true. - * - * For 0-argument functions (constants), we always allow - * function variants. That is, we always accept these examples: - * - * 5. (declare-fun c () Int) - * (declare-fun c () Bool) - * - * 6. (declare-datatypes ((Enum 0)) ((c))) - * (declare-fun c () Int) - * - * and always reject constant redefinition such as: - * - * 7. (declare-fun c () Int) - * (declare-fun c () Int) - * - * 8. (declare-datatypes ((Enum 0)) ((c))) and - * (declare-fun c () Enum) - */ -class OverloadedTypeTrie { - public: - OverloadedTypeTrie(Context* c, bool allowFunVariants = false) - : d_overloaded_symbols( - new (true) CDHashSet>(c)), - d_allowFunctionVariants(allowFunVariants) - { - } - ~OverloadedTypeTrie() { d_overloaded_symbols->deleteSelf(); } - - /** is this function overloaded? */ - bool isOverloadedFunction(cvc5::Term fun) const; - - /** Get overloaded constant for type. - * If possible, it returns a defined symbol with name - * that has type t. Otherwise returns null expression. - */ - cvc5::Term getOverloadedConstantForType(const std::string& name, - cvc5::Sort t) const; - - /** - * If possible, returns a defined function for a name - * and a vector of expected argument types. Otherwise returns - * null expression. - */ - cvc5::Term getOverloadedFunctionForTypes( - const std::string& name, const std::vector& argTypes) const; - /** called when obj is bound to name, and prev_bound_obj was already bound to - * name Returns false if the binding is invalid. - */ - bool bind(const string& name, cvc5::Term prev_bound_obj, cvc5::Term obj); - - private: - /** Marks expression obj with name as overloaded. - * Adds relevant information to the type arg trie data structure. - * It returns false if there is already an expression bound to that name - * whose type expects the same arguments as the type of obj but is not - * identical to the type of obj. For example, if we declare : - * - * (declare-datatypes () ((List (cons (hd Int) (tl List)) (nil)))) - * (declare-fun cons (Int List) List) - * - * cons : constructor_type( Int, List, List ) - * cons : function_type( Int, List, List ) - * - * These are put in the same place in the trie but do not have identical type, - * hence we return false. - */ - bool markOverloaded(const string& name, cvc5::Term obj); - /** the null expression */ - cvc5::Term d_nullTerm; - // The (context-independent) trie storing that maps expected argument - // vectors to symbols. All expressions stored in d_symbols are only - // interpreted as active if they also appear in the context-dependent - // set d_overloaded_symbols. - class TypeArgTrie { - public: - // children of this node - std::map d_children; - // symbols at this node - std::map d_symbols; - }; - /** for each string with operator overloading, this stores the data structure - * above. */ - std::unordered_map d_overload_type_arg_trie; - /** The set of overloaded symbols. */ - CDHashSet>* d_overloaded_symbols; - /** allow function variants - * This is true if we allow overloading (non-constant) functions that expect - * the same argument types. - */ - bool d_allowFunctionVariants; - /** get unique overloaded function - * If tat->d_symbols contains an active overloaded function, it - * returns that function, where that function must be unique - * if reqUnique=true. - * Otherwise, it returns the null expression. - */ - cvc5::Term getOverloadedFunctionAt(const TypeArgTrie* tat, - bool reqUnique = true) const; -}; - -bool OverloadedTypeTrie::isOverloadedFunction(cvc5::Term fun) const -{ - return d_overloaded_symbols->find(fun) != d_overloaded_symbols->end(); -} - -cvc5::Term OverloadedTypeTrie::getOverloadedConstantForType( - const std::string& name, cvc5::Sort t) const -{ - std::unordered_map::const_iterator it = - d_overload_type_arg_trie.find(name); - if (it != d_overload_type_arg_trie.end()) { - std::map::const_iterator its = - it->second.d_symbols.find(t); - if (its != it->second.d_symbols.end()) { - cvc5::Term expr = its->second; - // must be an active symbol - if (isOverloadedFunction(expr)) { - return expr; - } - } - } - return d_nullTerm; -} - -cvc5::Term OverloadedTypeTrie::getOverloadedFunctionForTypes( - const std::string& name, const std::vector& argTypes) const -{ - std::unordered_map::const_iterator it = - d_overload_type_arg_trie.find(name); - if (it != d_overload_type_arg_trie.end()) { - const TypeArgTrie* tat = &it->second; - for (unsigned i = 0; i < argTypes.size(); i++) { - std::map::const_iterator itc = - tat->d_children.find(argTypes[i]); - if (itc != tat->d_children.end()) { - tat = &itc->second; - } else { - Trace("parser-overloading") - << "Could not find overloaded function " << name << std::endl; - - // no functions match - return d_nullTerm; - } - } - // we ensure that there is *only* one active symbol at this node - return getOverloadedFunctionAt(tat); - } - return d_nullTerm; -} - -bool OverloadedTypeTrie::bind(const string& name, - cvc5::Term prev_bound_obj, - cvc5::Term obj) -{ - bool retprev = true; - if (!isOverloadedFunction(prev_bound_obj)) { - // mark previous as overloaded - retprev = markOverloaded(name, prev_bound_obj); - } - // mark this as overloaded - bool retobj = markOverloaded(name, obj); - return retprev && retobj; -} - -bool OverloadedTypeTrie::markOverloaded(const string& name, cvc5::Term obj) -{ - Trace("parser-overloading") << "Overloaded function : " << name; - Trace("parser-overloading") << " with type " << obj.getSort() << std::endl; - // get the argument types - cvc5::Sort t = obj.getSort(); - cvc5::Sort rangeType = t; - std::vector argTypes; - if (t.isFunction()) - { - argTypes = t.getFunctionDomainSorts(); - rangeType = t.getFunctionCodomainSort(); - } - else if (t.isDatatypeConstructor()) - { - argTypes = t.getDatatypeConstructorDomainSorts(); - rangeType = t.getDatatypeConstructorCodomainSort(); - } - else if (t.isDatatypeSelector()) - { - argTypes.push_back(t.getDatatypeSelectorDomainSort()); - rangeType = t.getDatatypeSelectorCodomainSort(); - } - // add to the trie - TypeArgTrie* tat = &d_overload_type_arg_trie[name]; - for (unsigned i = 0; i < argTypes.size(); i++) { - tat = &(tat->d_children[argTypes[i]]); - } - - // check if function variants are allowed here - if (d_allowFunctionVariants || argTypes.empty()) - { - // they are allowed, check for redefinition - std::map::iterator it = - tat->d_symbols.find(rangeType); - if (it != tat->d_symbols.end()) - { - cvc5::Term prev_obj = it->second; - // if there is already an active function with the same name and expects - // the same argument types and has the same return type, we reject the - // re-declaration here. - if (isOverloadedFunction(prev_obj)) - { - return false; - } - } - } - else - { - // they are not allowed, we cannot have any function defined here. - cvc5::Term existingFun = getOverloadedFunctionAt(tat, false); - if (!existingFun.isNull()) - { - return false; - } - } - - // otherwise, update the symbols - d_overloaded_symbols->insert(obj); - tat->d_symbols[rangeType] = obj; - return true; -} - -cvc5::Term OverloadedTypeTrie::getOverloadedFunctionAt( - const OverloadedTypeTrie::TypeArgTrie* tat, bool reqUnique) const -{ - cvc5::Term retExpr; - for (std::map::const_iterator its = - tat->d_symbols.begin(); - its != tat->d_symbols.end(); - ++its) - { - cvc5::Term expr = its->second; - if (isOverloadedFunction(expr)) - { - if (retExpr.isNull()) - { - if (!reqUnique) - { - return expr; - } - else - { - retExpr = expr; - } - } - else - { - // multiple functions match - return d_nullTerm; - } - } - } - return retExpr; -} - -class SymbolTable::Implementation { - public: - Implementation() - : d_context(), - d_exprMap(&d_context), - d_typeMap(&d_context), - d_overload_trie(&d_context) - { - } - - ~Implementation() {} - - bool bind(const string& name, cvc5::Term obj, bool doOverload); - void bindType(const string& name, cvc5::Sort t); - void bindType(const string& name, - const vector& params, - cvc5::Sort t); - bool isBound(const string& name) const; - bool isBoundType(const string& name) const; - cvc5::Term lookup(const string& name) const; - cvc5::Sort lookupType(const string& name) const; - cvc5::Sort lookupType(const string& name, - const vector& params) const; - size_t lookupArity(const string& name); - void popScope(); - void pushScope(); - size_t getLevel() const; - void reset(); - void resetAssertions(); - //------------------------ operator overloading - /** implementation of function from header */ - bool isOverloadedFunction(cvc5::Term fun) const; - - /** implementation of function from header */ - cvc5::Term getOverloadedConstantForType(const std::string& name, - cvc5::Sort t) const; - - /** implementation of function from header */ - cvc5::Term getOverloadedFunctionForTypes( - const std::string& name, const std::vector& argTypes) const; - //------------------------ end operator overloading - private: - /** The context manager for the scope maps. */ - Context d_context; - - /** A map for expressions. */ - CDHashMap d_exprMap; - - /** A map for types. */ - using TypeMap = CDHashMap, cvc5::Sort>>; - TypeMap d_typeMap; - - //------------------------ operator overloading - // the null expression - cvc5::Term d_nullTerm; - // overloaded type trie, stores all information regarding overloading - OverloadedTypeTrie d_overload_trie; - /** bind with overloading - * This is called whenever obj is bound to name where overloading symbols is - * allowed. If a symbol is previously bound to that name, it marks both as - * overloaded. Returns false if the binding was invalid. - */ - bool bindWithOverloading(const string& name, cvc5::Term obj); - //------------------------ end operator overloading -}; /* SymbolTable::Implementation */ - -bool SymbolTable::Implementation::bind(const string& name, - cvc5::Term obj, - bool doOverload) -{ - PrettyCheckArgument(!obj.isNull(), obj, "cannot bind to a null cvc5::Term"); - Trace("sym-table") << "SymbolTable: bind " << name - << ", doOverload=" << doOverload << std::endl; - if (doOverload) { - if (!bindWithOverloading(name, obj)) { - return false; - } - } - d_exprMap.insert(name, obj); - - return true; -} - -bool SymbolTable::Implementation::isBound(const string& name) const { - return d_exprMap.find(name) != d_exprMap.end(); -} - -cvc5::Term SymbolTable::Implementation::lookup(const string& name) const -{ - Assert(isBound(name)); - cvc5::Term expr = (*d_exprMap.find(name)).second; - if (isOverloadedFunction(expr)) { - return d_nullTerm; - } else { - return expr; - } -} - -void SymbolTable::Implementation::bindType(const string& name, cvc5::Sort t) -{ - d_typeMap.insert(name, make_pair(vector(), t)); -} - -void SymbolTable::Implementation::bindType(const string& name, - const vector& params, - cvc5::Sort t) -{ - if (TraceIsOn("sort")) { - Trace("sort") << "bindType(" << name << ", ["; - if (params.size() > 0) { - copy(params.begin(), - params.end() - 1, - ostream_iterator(Trace("sort"), ", ")); - Trace("sort") << params.back(); - } - Trace("sort") << "], " << t << ")" << endl; - } - - d_typeMap.insert(name, make_pair(params, t)); -} - -bool SymbolTable::Implementation::isBoundType(const string& name) const { - return d_typeMap.find(name) != d_typeMap.end(); -} - -cvc5::Sort SymbolTable::Implementation::lookupType(const string& name) const -{ - std::pair, cvc5::Sort> p = - (*d_typeMap.find(name)).second; - PrettyCheckArgument(p.first.size() == 0, name, - "type constructor arity is wrong: " - "`%s' requires %u parameters but was provided 0", - name.c_str(), p.first.size()); - return p.second; -} - -cvc5::Sort SymbolTable::Implementation::lookupType( - const string& name, const vector& params) const -{ - std::pair, cvc5::Sort> p = - (*d_typeMap.find(name)).second; - PrettyCheckArgument(p.first.size() == params.size(), params, - "type constructor arity is wrong: " - "`%s' requires %u parameters but was provided %u", - name.c_str(), p.first.size(), params.size()); - if (p.first.size() == 0) { - PrettyCheckArgument(p.second.isUninterpretedSort(), name.c_str()); - return p.second; - } - if (p.second.isDatatype()) - { - PrettyCheckArgument(p.second.getDatatype().isParametric(), - name, - "expected parametric datatype"); - return p.second.instantiate(params); - } - bool isUninterpretedSortConstructor = - p.second.isUninterpretedSortConstructor(); - if (TraceIsOn("sort")) - { - Trace("sort") << "instantiating using a sort " - << (isUninterpretedSortConstructor ? "constructor" - : "substitution") - << std::endl; - Trace("sort") << "have formals ["; - copy(p.first.begin(), - p.first.end() - 1, - ostream_iterator(Trace("sort"), ", ")); - Trace("sort") << p.first.back() << "]" << std::endl << "parameters ["; - copy(params.begin(), - params.end() - 1, - ostream_iterator(Trace("sort"), ", ")); - Trace("sort") << params.back() << "]" << endl - << "type ctor " << name << std::endl - << "type is " << p.second << std::endl; - } - cvc5::Sort instantiation = isUninterpretedSortConstructor - ? p.second.instantiate(params) - : p.second.substitute(p.first, params); - Trace("sort") << "instance is " << instantiation << std::endl; - - return instantiation; -} - -size_t SymbolTable::Implementation::lookupArity(const string& name) { - std::pair, cvc5::Sort> p = - (*d_typeMap.find(name)).second; - return p.first.size(); -} - -void SymbolTable::Implementation::popScope() { - // should not pop beyond level one - if (d_context.getLevel() == 0) - { - throw ScopeException(); - } - d_context.pop(); -} - -void SymbolTable::Implementation::pushScope() { d_context.push(); } - -size_t SymbolTable::Implementation::getLevel() const { - return d_context.getLevel(); -} - -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(cvc5::Term fun) const -{ - return d_overload_trie.isOverloadedFunction(fun); -} - -cvc5::Term SymbolTable::Implementation::getOverloadedConstantForType( - const std::string& name, cvc5::Sort t) const -{ - return d_overload_trie.getOverloadedConstantForType(name, t); -} - -cvc5::Term SymbolTable::Implementation::getOverloadedFunctionForTypes( - const std::string& name, const std::vector& argTypes) const -{ - return d_overload_trie.getOverloadedFunctionForTypes(name, argTypes); -} - -bool SymbolTable::Implementation::bindWithOverloading(const string& name, - cvc5::Term obj) -{ - CDHashMap::const_iterator it = d_exprMap.find(name); - if (it != d_exprMap.end()) - { - const cvc5::Term& prev_bound_obj = (*it).second; - if (prev_bound_obj != obj) { - return d_overload_trie.bind(name, prev_bound_obj, obj); - } - } - return true; -} - -bool SymbolTable::isOverloadedFunction(cvc5::Term fun) const -{ - return d_implementation->isOverloadedFunction(fun); -} - -cvc5::Term SymbolTable::getOverloadedConstantForType(const std::string& name, - cvc5::Sort t) const -{ - return d_implementation->getOverloadedConstantForType(name, t); -} - -cvc5::Term SymbolTable::getOverloadedFunctionForTypes( - const std::string& name, const std::vector& argTypes) const -{ - return d_implementation->getOverloadedFunctionForTypes(name, argTypes); -} - -SymbolTable::SymbolTable() : d_implementation(new SymbolTable::Implementation()) -{ -} - -SymbolTable::~SymbolTable() {} -bool SymbolTable::bind(const string& name, cvc5::Term obj, bool doOverload) -{ - return d_implementation->bind(name, obj, doOverload); -} - -void SymbolTable::bindType(const string& name, cvc5::Sort t) -{ - d_implementation->bindType(name, t); -} - -void SymbolTable::bindType(const string& name, - const vector& params, - cvc5::Sort t) -{ - d_implementation->bindType(name, params, t); -} - -bool SymbolTable::isBound(const string& name) const -{ - return d_implementation->isBound(name); -} -bool SymbolTable::isBoundType(const string& name) const -{ - return d_implementation->isBoundType(name); -} -cvc5::Term SymbolTable::lookup(const string& name) const -{ - return d_implementation->lookup(name); -} -cvc5::Sort SymbolTable::lookupType(const string& name) const -{ - return d_implementation->lookupType(name); -} - -cvc5::Sort SymbolTable::lookupType(const string& name, - const vector& params) const -{ - return d_implementation->lookupType(name, params); -} -size_t SymbolTable::lookupArity(const string& name) { - return d_implementation->lookupArity(name); -} -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 cvc5::internal diff --git a/src/expr/symbol_table.h b/src/expr/symbol_table.h deleted file mode 100644 index bc7628df0..000000000 --- a/src/expr/symbol_table.h +++ /dev/null @@ -1,206 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Andrew Reynolds, Morgan Deters, Christopher L. Conway - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * Convenience class for scoping variable and type declarations. - */ - -#include "cvc5_public.h" - -#ifndef CVC5__SYMBOL_TABLE_H -#define CVC5__SYMBOL_TABLE_H - -#include -#include -#include - -#include "base/exception.h" -#include "cvc5_export.h" - -namespace cvc5 { -class Solver; -class Sort; -class Term; -} // namespace cvc5 - -namespace cvc5::internal { - -class CVC5_EXPORT ScopeException : public Exception -{ -}; - -/** - * A convenience class for handling scoped declarations. Implements the usual - * nested scoping rules for declarations, with separate bindings for expressions - * and types. - */ -class CVC5_EXPORT SymbolTable -{ - public: - /** Create a symbol table. */ - SymbolTable(); - ~SymbolTable(); - - /** - * Bind an expression to a name in the current scope level. - * - * When doOverload is false: - * if name is already bound to an expression in the current - * level, then the binding is replaced. If name is bound - * in a previous level, then the binding is "covered" by this one - * until the current scope is popped. - * If levelZero is true the name shouldn't be already bound. - * - * When doOverload is true: - * if name is already bound to an expression in the current - * level, then we mark the previous bound expression and obj as overloaded - * functions. - * - * @param name an identifier - * @param obj the expression to bind to name - * @param doOverload set if the binding can overload the function name. - * - * Returns false if the binding was invalid. - */ - bool bind(const std::string& name, cvc5::Term obj, bool doOverload = false); - - /** - * Bind a type to a name in the current scope. If name - * is already bound to a type in the current level, then the binding - * is replaced. If name is bound in a previous level, - * then the binding is "covered" by this one until the current scope - * is popped. - * - * @param name an identifier - * @param t the type to bind to name - */ - void bindType(const std::string& name, cvc5::Sort t); - - /** - * Bind a type to a name in the current scope. If name - * is already bound to a type or type constructor in the current - * level, then the binding is replaced. If name is - * bound in a previous level, then the binding is "covered" by this - * one until the current scope is popped. - * - * @param name an identifier - * @param params the parameters to the type - * @param t the type to bind to name - */ - void bindType(const std::string& name, - const std::vector& params, - cvc5::Sort t); - - /** - * Check whether a name is bound to an expression with bind(). - * - * @param name the identifier to check. - * @returns true iff name is bound in the current scope. - */ - bool isBound(const std::string& name) const; - - /** - * Check whether a name is bound to a type (or type constructor). - * - * @param name the identifier to check. - * @returns true iff name is bound to a type in the current scope. - */ - bool isBoundType(const std::string& name) const; - - /** - * Lookup a bound expression. - * - * @param name the identifier to lookup - * @returns the unique expression bound to name in the current - * scope. - * It returns the null expression if there is not a unique expression bound to - * name in the current scope (i.e. if there is not exactly one). - */ - cvc5::Term lookup(const std::string& name) const; - - /** - * Lookup a bound type. - * - * @param name the type identifier to lookup - * @returns the type bound to name in the current scope. - */ - cvc5::Sort lookupType(const std::string& name) const; - - /** - * Lookup a bound parameterized type. - * - * @param name the type-constructor identifier to lookup - * @param params the types to use to parameterize the type - * @returns the type bound to name(params) in - * the current scope. - */ - cvc5::Sort lookupType(const std::string& name, - const std::vector& params) const; - - /** - * Lookup the arity of a bound parameterized type. - */ - size_t lookupArity(const std::string& name); - - /** - * Pop a scope level, deletes all bindings since the last call to pushScope, - * and decreases the level by 1. - * - * @throws ScopeException if the scope level is 0. - */ - void popScope(); - - /** Push a scope level and increase the scope level by 1. */ - void pushScope(); - - /** Get the current level of this symbol table. */ - size_t getLevel() const; - - /** Reset everything. */ - void reset(); - /** Reset assertions. */ - void resetAssertions(); - - //------------------------ operator overloading - /** is this function overloaded? */ - bool isOverloadedFunction(cvc5::Term fun) const; - - /** Get overloaded constant for type. - * If possible, it returns the defined symbol with name - * that has type t. Otherwise returns null expression. - */ - cvc5::Term getOverloadedConstantForType(const std::string& name, - cvc5::Sort t) const; - - /** - * If possible, returns the unique defined function for a name - * that expects arguments with types "argTypes". - * For example, if argTypes = (T1, ..., Tn), then this may return an - * expression with type function(T1, ..., Tn), or constructor(T1, ...., Tn). - * - * If there is not a unique defined function for the name and argTypes, - * this returns the null expression. This can happen either if there are - * no functions with name and expected argTypes, or alternatively there is - * more than one function with name and expected argTypes. - */ - cvc5::Term getOverloadedFunctionForTypes( - const std::string& name, const std::vector& argTypes) const; - //------------------------ end operator overloading - - private: - /** The implementation of the symbol table */ - class Implementation; - std::unique_ptr d_implementation; -}; /* class SymbolTable */ - -} // namespace cvc5::internal - -#endif /* CVC5__SYMBOL_TABLE_H */ diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index 6e2104053..84edfed03 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -29,6 +29,8 @@ #include "smt/command.h" #include "smt/solver_engine.h" +using namespace cvc5::parser; + namespace cvc5::main { // Function to cancel any (externally-imposed) limit on CPU time. diff --git a/src/main/command_executor.h b/src/main/command_executor.h index 5fe92312f..b6ba02d40 100644 --- a/src/main/command_executor.h +++ b/src/main/command_executor.h @@ -20,7 +20,7 @@ #include #include "api/cpp/cvc5.h" -#include "expr/symbol_manager.h" +#include "parser/api/cpp/symbol_manager.h" namespace cvc5 { @@ -46,7 +46,7 @@ class CommandExecutor * Certain commands (e.g. reset-assertions) have a specific impact on the * symbol manager. */ - std::unique_ptr d_symman; + std::unique_ptr d_symman; cvc5::Result d_result; @@ -71,7 +71,7 @@ class CommandExecutor cvc5::Solver* getSolver() { return d_solver.get(); } /** Get a pointer to the symbol manager owned by this CommandExecutor */ - SymbolManager* getSymbolManager() { return d_symman.get(); } + parser::SymbolManager* getSymbolManager() { return d_symman.get(); } cvc5::Result getResult() const { return d_result; } void reset(); @@ -106,7 +106,7 @@ private: }; /* class CommandExecutor */ bool solverInvoke(cvc5::Solver* solver, - SymbolManager* sm, + parser::SymbolManager* sm, Command* cmd, std::ostream& out); diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index cd1f11881..3af740aef 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -42,7 +42,7 @@ #include "api/cpp/cvc5.h" #include "base/check.h" #include "base/output.h" -#include "expr/symbol_manager.h" +#include "parser/api/cpp/symbol_manager.h" #include "parser/input.h" #include "parser/parser.h" #include "parser/parser_builder.h" diff --git a/src/main/interactive_shell.h b/src/main/interactive_shell.h index 1943d7d16..9b036220e 100644 --- a/src/main/interactive_shell.h +++ b/src/main/interactive_shell.h @@ -26,10 +26,9 @@ namespace cvc5 { class Solver; -class SymbolManager; - namespace parser { class Parser; + class SymbolManager; } // namespace parser class Command; @@ -42,7 +41,7 @@ namespace parser { using CmdSeq = std::vector>; InteractiveShell(Solver* solver, - SymbolManager* sm, + cvc5::parser::SymbolManager* sm, std::istream& in, std::ostream& out); @@ -60,13 +59,13 @@ namespace parser { /** * Return the internal parser being used. */ - parser::Parser* getParser() { return d_parser.get(); } + cvc5::parser::Parser* getParser() { return d_parser.get(); } private: Solver* d_solver; std::istream& d_in; std::ostream& d_out; - std::unique_ptr d_parser; + std::unique_ptr d_parser; bool d_quit; bool d_usingEditline; diff --git a/src/parser/CMakeLists.txt b/src/parser/CMakeLists.txt index 74fd7c4e5..cf1e54536 100644 --- a/src/parser/CMakeLists.txt +++ b/src/parser/CMakeLists.txt @@ -27,6 +27,8 @@ set(libcvc5parser_src_files antlr_input_imports.cpp antlr_line_buffered_input.cpp antlr_line_buffered_input.h + api/cpp/symbol_manager.cpp + api/cpp/symbol_manager.h bounded_token_buffer.cpp bounded_token_buffer.h bounded_token_factory.cpp @@ -48,6 +50,8 @@ set(libcvc5parser_src_files smt2/smt2_input.h smt2/sygus_input.cpp smt2/sygus_input.h + symbol_table.cpp + symbol_table.h tptp/tptp.cpp tptp/tptp.h tptp/tptp_input.cpp diff --git a/src/parser/api/cpp/symbol_manager.cpp b/src/parser/api/cpp/symbol_manager.cpp new file mode 100644 index 000000000..10cb4cc5b --- /dev/null +++ b/src/parser/api/cpp/symbol_manager.cpp @@ -0,0 +1,454 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Mathias Preiner, Andres Noetzli + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The symbol manager. + */ + +#include "parser/api/cpp/symbol_manager.h" + +#include "context/cdhashmap.h" +#include "context/cdhashset.h" +#include "context/cdlist.h" +#include "context/cdo.h" +#include "parser/symbol_table.h" + +using namespace cvc5::context; +using namespace cvc5::internal::parser; + +namespace cvc5::parser { + +// ---------------------------------------------- SymbolManager::Implementation + +class SymbolManager::Implementation +{ + using TermStringMap = + CDHashMap>; + using TermSet = CDHashSet>; + using SortList = CDList; + using TermList = CDList; + + public: + Implementation() + : d_context(), + d_names(&d_context), + d_namedAsserts(&d_context), + d_declareSorts(&d_context), + d_declareTerms(&d_context), + d_funToSynth(&d_context), + d_hasPushedScope(&d_context, false), + d_lastSynthName(&d_context) + { + // use an outermost push, to be able to clear all definitions + d_context.push(); + } + + ~Implementation() { d_context.pop(); } + SymbolTable& getSymbolTable() { return d_symtabAllocated; } + + /** set expression name */ + NamingResult setExpressionName(cvc5::Term t, + const std::string& name, + bool isAssertion = false); + /** get expression name */ + bool getExpressionName(cvc5::Term t, + std::string& name, + bool isAssertion = false) const; + /** get expression names */ + void getExpressionNames(const std::vector& ts, + std::vector& names, + bool areAssertions = false) const; + /** get expression names */ + std::map getExpressionNames( + bool areAssertions) const; + /** get model declare sorts */ + std::vector getModelDeclareSorts() const; + /** get model declare terms */ + std::vector getModelDeclareTerms() const; + /** get functions to synthesize */ + std::vector getFunctionsToSynthesize() const; + /** Add declared sort to the list of model declarations. */ + void addModelDeclarationSort(cvc5::Sort s); + /** Add declared term to the list of model declarations. */ + void addModelDeclarationTerm(cvc5::Term t); + /** Add function to the list of functions to synthesize. */ + void addFunctionToSynthesize(cvc5::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; + /** Set the last abduct-to-synthesize had the given name. */ + void setLastSynthName(const std::string& name); + /** Get the name of the last abduct-to-synthesize */ + const std::string& getLastSynthName() const; + + private: + /** + * The declaration scope that is "owned" by this symbol manager. + */ + SymbolTable d_symtabAllocated; + /** The context manager for the scope maps. */ + Context d_context; + /** Map terms to names */ + TermStringMap d_names; + /** The set of terms with assertion names */ + TermSet d_namedAsserts; + /** Declared sorts (for model printing) */ + SortList d_declareSorts; + /** Declared terms (for model printing) */ + TermList d_declareTerms; + /** Functions to synthesize (for response to check-synth) */ + TermList d_funToSynth; + /** + * Have we pushed a scope (e.g. a let or quantifier) in the current context? + */ + CDO d_hasPushedScope; + /** The last abduct or interpolant to synthesize name */ + CDO d_lastSynthName; +}; + +NamingResult SymbolManager::Implementation::setExpressionName( + cvc5::Term t, const std::string& name, bool isAssertion) +{ + Trace("sym-manager") << "SymbolManager: set expression name: " << t << " -> " + << name << ", isAssertion=" << isAssertion << std::endl; + if (d_hasPushedScope.get()) + { + // cannot name subexpressions under binders + return NamingResult::ERROR_IN_BINDER; + } + + if (isAssertion) + { + d_namedAsserts.insert(t); + } + if (d_names.find(t) != d_names.end()) + { + // already named assertion + return NamingResult::ERROR_ALREADY_NAMED; + } + d_names[t] = name; + return NamingResult::SUCCESS; +} + +bool SymbolManager::Implementation::getExpressionName(cvc5::Term t, + std::string& name, + bool isAssertion) const +{ + TermStringMap::const_iterator it = d_names.find(t); + if (it == d_names.end()) + { + return false; + } + if (isAssertion) + { + // must be an assertion name + if (d_namedAsserts.find(t) == d_namedAsserts.end()) + { + return false; + } + } + name = (*it).second; + return true; +} + +void SymbolManager::Implementation::getExpressionNames( + const std::vector& ts, + std::vector& names, + bool areAssertions) const +{ + for (const cvc5::Term& t : ts) + { + std::string name; + if (getExpressionName(t, name, areAssertions)) + { + names.push_back(name); + } + } +} + +std::map +SymbolManager::Implementation::getExpressionNames(bool areAssertions) const +{ + std::map emap; + for (TermStringMap::const_iterator it = d_names.begin(), + itend = d_names.end(); + it != itend; + ++it) + { + cvc5::Term t = (*it).first; + if (areAssertions && d_namedAsserts.find(t) == d_namedAsserts.end()) + { + continue; + } + emap[t] = (*it).second; + } + return emap; +} + +std::vector SymbolManager::Implementation::getModelDeclareSorts() + const +{ + std::vector declareSorts(d_declareSorts.begin(), + d_declareSorts.end()); + return declareSorts; +} + +std::vector SymbolManager::Implementation::getModelDeclareTerms() + const +{ + std::vector declareTerms(d_declareTerms.begin(), + d_declareTerms.end()); + return declareTerms; +} + +std::vector +SymbolManager::Implementation::getFunctionsToSynthesize() const +{ + return std::vector(d_funToSynth.begin(), d_funToSynth.end()); +} + +void SymbolManager::Implementation::addModelDeclarationSort(cvc5::Sort s) +{ + Trace("sym-manager") << "SymbolManager: addModelDeclarationSort " << s + << std::endl; + d_declareSorts.push_back(s); +} + +void SymbolManager::Implementation::addModelDeclarationTerm(cvc5::Term t) +{ + Trace("sym-manager") << "SymbolManager: addModelDeclarationTerm " << t + << std::endl; + d_declareTerms.push_back(t); +} + +void SymbolManager::Implementation::addFunctionToSynthesize(cvc5::Term f) +{ + Trace("sym-manager") << "SymbolManager: addFunctionToSynthesize " << f + << std::endl; + d_funToSynth.push_back(f); +} + +void SymbolManager::Implementation::pushScope(bool isUserContext) +{ + 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(); + if (!isUserContext) + { + d_hasPushedScope = true; + } + d_symtabAllocated.pushScope(); +} + +void SymbolManager::Implementation::popScope() +{ + Trace("sym-manager") << "SymbolManager: popScope" << std::endl; + d_symtabAllocated.popScope(); + if (d_context.getLevel() == 0) + { + throw ScopeException(); + } + d_context.pop(); + Trace("sym-manager-debug") + << "d_hasPushedScope is now " << d_hasPushedScope.get() << std::endl; +} + +bool SymbolManager::Implementation::hasPushedScope() const +{ + return d_hasPushedScope.get(); +} + +void SymbolManager::Implementation::setLastSynthName(const std::string& name) +{ + d_lastSynthName = name; +} + +const std::string& SymbolManager::Implementation::getLastSynthName() const +{ + return d_lastSynthName.get(); +} + +void SymbolManager::Implementation::reset() +{ + Trace("sym-manager") << "SymbolManager: reset" << std::endl; + // reset resets the symbol table even when global declarations are true + d_symtabAllocated.reset(); + // 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 + +SymbolManager::SymbolManager(cvc5::Solver* s) + : d_solver(s), + d_implementation(new SymbolManager::Implementation()), + d_globalDeclarations(false) +{ +} + +SymbolManager::~SymbolManager() {} + +SymbolTable* SymbolManager::getSymbolTable() +{ + return &d_implementation->getSymbolTable(); +} + +bool SymbolManager::bind(const std::string& name, + cvc5::Term obj, + bool doOverload) +{ + return d_implementation->getSymbolTable().bind(name, obj, doOverload); +} + +NamingResult SymbolManager::setExpressionName(cvc5::Term t, + const std::string& name, + bool isAssertion) +{ + return d_implementation->setExpressionName(t, name, isAssertion); +} + +bool SymbolManager::getExpressionName(cvc5::Term t, + std::string& name, + bool isAssertion) const +{ + return d_implementation->getExpressionName(t, name, isAssertion); +} + +void SymbolManager::getExpressionNames(const std::vector& ts, + std::vector& names, + bool areAssertions) const +{ + return d_implementation->getExpressionNames(ts, names, areAssertions); +} + +std::map SymbolManager::getExpressionNames( + bool areAssertions) const +{ + return d_implementation->getExpressionNames(areAssertions); +} +std::vector SymbolManager::getModelDeclareSorts() const +{ + return d_implementation->getModelDeclareSorts(); +} +std::vector SymbolManager::getModelDeclareTerms() const +{ + return d_implementation->getModelDeclareTerms(); +} + +std::vector SymbolManager::getFunctionsToSynthesize() const +{ + return d_implementation->getFunctionsToSynthesize(); +} + +void SymbolManager::addModelDeclarationSort(cvc5::Sort s) +{ + d_implementation->addModelDeclarationSort(s); +} + +void SymbolManager::addModelDeclarationTerm(cvc5::Term t) +{ + d_implementation->addModelDeclarationTerm(t); +} + +void SymbolManager::addFunctionToSynthesize(cvc5::Term f) +{ + d_implementation->addFunctionToSynthesize(f); +} + +size_t SymbolManager::scopeLevel() const +{ + return d_implementation->getSymbolTable().getLevel(); +} + +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); +} + +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_implementation->popScope(); +} + +void SymbolManager::setGlobalDeclarations(bool flag) +{ + d_globalDeclarations = flag; +} + +bool SymbolManager::getGlobalDeclarations() const +{ + return d_globalDeclarations; +} + +void SymbolManager::setLastSynthName(const std::string& name) +{ + d_implementation->setLastSynthName(name); +} + +const std::string& SymbolManager::getLastSynthName() const +{ + return d_implementation->getLastSynthName(); +} + +void SymbolManager::reset() +{ + d_implementation->reset(); +} + +void SymbolManager::resetAssertions() +{ + d_implementation->resetAssertions(); + if (!d_globalDeclarations) + { + d_implementation->getSymbolTable().resetAssertions(); + } +} + +} // namespace cvc5::parser diff --git a/src/parser/api/cpp/symbol_manager.h b/src/parser/api/cpp/symbol_manager.h new file mode 100644 index 000000000..4aa732d71 --- /dev/null +++ b/src/parser/api/cpp/symbol_manager.h @@ -0,0 +1,220 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Mathias Preiner, Andres Noetzli + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The symbol manager. + */ + +#include "cvc5_public.h" + +#ifndef CVC5__EXPR__SYMBOL_MANAGER_H +#define CVC5__EXPR__SYMBOL_MANAGER_H + +#include +#include +#include + +#include "api/cpp/cvc5.h" +#include "cvc5_export.h" + +namespace cvc5 { + +namespace internal::parser { +class SymbolTable; +} + +namespace parser { +/** Represents the result of a call to `setExpressionName()`. */ +enum class NamingResult +{ + /** The expression name was set successfully. */ + SUCCESS, + /** The expression already has a name. */ + ERROR_ALREADY_NAMED, + /** The expression is in a binder. */ + ERROR_IN_BINDER +}; + +/** + * Symbol manager, which manages: + * (1) The symbol table used by the parser, + * (2) Information related to the (! ... :named s) feature in SMT-LIB version 2. + * + * Like SymbolTable, this class currently lives in src/expr/ since it uses + * context-dependent data structures. + */ +class CVC5_EXPORT SymbolManager +{ + public: + SymbolManager(cvc5::Solver* s); + ~SymbolManager(); + /** Get the underlying symbol table */ + internal::parser::SymbolTable* getSymbolTable(); + + /** + * Bind an expression to a name in the current scope level in the underlying + * symbol table. + * + * When doOverload is false: + * if name is already bound to an expression in the current + * level, then the binding is replaced. If name is bound + * in a previous level, then the binding is "covered" by this one + * until the current scope is popped. + * If levelZero is true the name shouldn't be already bound. + * + * When doOverload is true: + * if name is already bound to an expression in the current + * level, then we mark the previous bound expression and obj as overloaded + * functions. + * + * @param name an identifier + * @param obj the expression to bind to name + * @param doOverload set if the binding can overload the function name. + * + * Returns false if the binding was invalid. + */ + bool bind(const std::string& name, cvc5::Term obj, bool doOverload = false); + + //---------------------------- named expressions + /** Set name of term t to name + * + * @param t The term to name + * @param name The given name + * @param isAssertion Whether t is being given a name in an assertion + * context. In particular, this is true if and only if there was an assertion + * command of the form (assert (! t :named name)). + * @return true if the name was set. This method may return false if t + * already has a name. + */ + NamingResult setExpressionName(cvc5::Term t, + const std::string& name, + bool isAssertion = false); + /** Get name for term t + * + * @param t The term + * @param name The argument to update with the name of t + * @param isAssertion Whether we only wish to get the assertion name of t + * @return true if t has a name. If so, name is updated to that name. + * Otherwise, name is unchanged. + */ + bool getExpressionName(cvc5::Term t, + std::string& name, + bool isAssertion = false) const; + /** + * Convert list of terms to list of names. This adds to names the names of + * all terms in ts that has names. Terms that do not have names are not + * included. + * + * Notice that we do not distinguish what terms among those in ts have names. + * If the caller of this method wants more fine-grained information about what + * specific terms had names, then use the more fine grained interface above, + * per term. + * + * @param ts The terms + * @param names The name list + * @param areAssertions Whether we only wish to include assertion names + */ + void getExpressionNames(const std::vector& ts, + std::vector& names, + bool areAssertions = false) const; + /** + * Get a mapping of all expression names. + * + * @param areAssertions Whether we only wish to include assertion names + * @return the mapping containing all expression names. + */ + std::map getExpressionNames( + bool areAssertions = false) const; + /** + * @return The sorts we have declared that should be printed in the model. + */ + std::vector getModelDeclareSorts() const; + /** + * @return The terms we have declared that should be printed in the model. + */ + std::vector getModelDeclareTerms() const; + /** + * @return The functions we have declared that should be printed in a response + * to check-synth. + */ + std::vector getFunctionsToSynthesize() const; + /** + * Add declared sort to the list of model declarations. + */ + void addModelDeclarationSort(cvc5::Sort s); + /** + * Add declared term to the list of model declarations. + */ + void addModelDeclarationTerm(cvc5::Term t); + /** + * Add a function to synthesize. This ensures the solution for f is printed + * in a successful response to check-synth. + */ + void addFunctionToSynthesize(cvc5::Term f); + + //---------------------------- end named expressions + /** + * Get the scope level of the symbol table. + */ + size_t scopeLevel() const; + /** + * Push a scope in the symbol table. + * + * @param isUserContext If true, this push is denoting a push of the user + * context, e.g. via an smt2 push/pop command. Otherwise, this push is + * due to a let/quantifier binding. + */ + void pushScope(bool isUserContext); + /** + * Pop a scope in the symbol table. + */ + void popScope(); + /** + * 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. */ + bool getGlobalDeclarations() const; + /** + * Set the last abduct or interpolant to synthesize had the given name. This + * is required since e.g. get-abduct-next must know the name of the + * abduct-to-synthesize to print its result. For example, the sequence: + * (get-abduct A ) + * (get-abduct-next) + * The latter command must know the symbol "A". + */ + void setLastSynthName(const std::string& name); + /** Get the name of the last abduct or interpolant to synthesize */ + const std::string& getLastSynthName() const; + + private: + /** The API Solver object. */ + cvc5::Solver* d_solver; + /** The implementation of the symbol manager */ + class Implementation; + std::unique_ptr d_implementation; + /** + * Whether the global declarations option is enabled. This corresponds to the + * SMT-LIB option :global-declarations. By default, its value is false. + */ + bool d_globalDeclarations; +}; + +} // namespace parser +} // namespace cvc5 + +#endif /* CVC5__EXPR__SYMBOL_MANAGER_H */ diff --git a/src/parser/parser.h b/src/parser/parser.h index 47bb7d7d6..8499f3e06 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -25,11 +25,11 @@ #include "api/cpp/cvc5.h" #include "cvc5_export.h" -#include "expr/symbol_manager.h" -#include "expr/symbol_table.h" +#include "parser/api/cpp/symbol_manager.h" #include "parser/input.h" #include "parser/parse_op.h" #include "parser/parser_exception.h" +#include "symbol_table.h" namespace cvc5 { @@ -117,7 +117,7 @@ private: /** * This current symbol table used by this parser, from symbol manager. */ - internal::SymbolTable* d_symtab; + internal::parser::SymbolTable* d_symtab; /** * The level of the assertions in the declaration scope. Things declared diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h index 43d7c9f11..f952ea0af 100644 --- a/src/parser/parser_builder.h +++ b/src/parser/parser_builder.h @@ -29,11 +29,11 @@ namespace cvc5 { class Solver; class Options; -class SymbolManager; namespace parser { class Parser; +class SymbolManager; /** * A builder for input language parsers. build() can be diff --git a/src/parser/symbol_table.cpp b/src/parser/symbol_table.cpp new file mode 100644 index 000000000..bfb514d85 --- /dev/null +++ b/src/parser/symbol_table.cpp @@ -0,0 +1,689 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Mathias Preiner, Tim King + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Convenience class for scoping variable and type declarations + * (implementation). + */ + +#include "parser/symbol_table.h" + +#include +#include +#include +#include + +#include "api/cpp/cvc5.h" +#include "context/cdhashmap.h" +#include "context/cdhashset.h" +#include "context/context.h" + +namespace cvc5::internal::parser { + +using context::CDHashMap; +using context::CDHashSet; +using context::Context; +using std::copy; +using std::endl; +using std::ostream_iterator; +using std::pair; +using std::string; +using std::vector; + +/** Overloaded type trie. + * + * This data structure stores a trie of expressions with + * the same name, and must be distinguished by their argument types. + * It is context-dependent. + * + * Using the argument allowFunVariants, + * it may either be configured to allow function variants or not, + * where a function variant is function that expects the same + * argument types as another. + * + * For example, the following definitions introduce function + * variants for the symbol f: + * + * 1. (declare-fun f (Int) Int) and + * (declare-fun f (Int) Bool) + * + * 2. (declare-fun f (Int) Int) and + * (declare-fun f (Int) Int) + * + * 3. (declare-datatypes ((Tup 0)) ((f (data Int)))) and + * (declare-fun f (Int) Tup) + * + * 4. (declare-datatypes ((Tup 0)) ((mkTup (f Int)))) and + * (declare-fun f (Tup) Bool) + * + * If function variants is set to true, we allow function variants + * but not function redefinition. In examples 2 and 3, f is + * declared twice as a symbol of identical argument and range + * types. We never accept these definitions. However, we do + * allow examples 1 and 4 above when allowFunVariants is true. + * + * For 0-argument functions (constants), we always allow + * function variants. That is, we always accept these examples: + * + * 5. (declare-fun c () Int) + * (declare-fun c () Bool) + * + * 6. (declare-datatypes ((Enum 0)) ((c))) + * (declare-fun c () Int) + * + * and always reject constant redefinition such as: + * + * 7. (declare-fun c () Int) + * (declare-fun c () Int) + * + * 8. (declare-datatypes ((Enum 0)) ((c))) and + * (declare-fun c () Enum) + */ +class OverloadedTypeTrie +{ + public: + OverloadedTypeTrie(Context* c, bool allowFunVariants = false) + : d_overloaded_symbols( + new (true) CDHashSet>(c)), + d_allowFunctionVariants(allowFunVariants) + { + } + ~OverloadedTypeTrie() { d_overloaded_symbols->deleteSelf(); } + + /** is this function overloaded? */ + bool isOverloadedFunction(cvc5::Term fun) const; + + /** Get overloaded constant for type. + * If possible, it returns a defined symbol with name + * that has type t. Otherwise returns null expression. + */ + cvc5::Term getOverloadedConstantForType(const std::string& name, + cvc5::Sort t) const; + + /** + * If possible, returns a defined function for a name + * and a vector of expected argument types. Otherwise returns + * null expression. + */ + cvc5::Term getOverloadedFunctionForTypes( + const std::string& name, const std::vector& argTypes) const; + /** called when obj is bound to name, and prev_bound_obj was already bound to + * name Returns false if the binding is invalid. + */ + bool bind(const string& name, cvc5::Term prev_bound_obj, cvc5::Term obj); + + private: + /** Marks expression obj with name as overloaded. + * Adds relevant information to the type arg trie data structure. + * It returns false if there is already an expression bound to that name + * whose type expects the same arguments as the type of obj but is not + * identical to the type of obj. For example, if we declare : + * + * (declare-datatypes () ((List (cons (hd Int) (tl List)) (nil)))) + * (declare-fun cons (Int List) List) + * + * cons : constructor_type( Int, List, List ) + * cons : function_type( Int, List, List ) + * + * These are put in the same place in the trie but do not have identical type, + * hence we return false. + */ + bool markOverloaded(const string& name, cvc5::Term obj); + /** the null expression */ + cvc5::Term d_nullTerm; + // The (context-independent) trie storing that maps expected argument + // vectors to symbols. All expressions stored in d_symbols are only + // interpreted as active if they also appear in the context-dependent + // set d_overloaded_symbols. + class TypeArgTrie + { + public: + // children of this node + std::map d_children; + // symbols at this node + std::map d_symbols; + }; + /** for each string with operator overloading, this stores the data structure + * above. */ + std::unordered_map d_overload_type_arg_trie; + /** The set of overloaded symbols. */ + CDHashSet>* d_overloaded_symbols; + /** allow function variants + * This is true if we allow overloading (non-constant) functions that expect + * the same argument types. + */ + bool d_allowFunctionVariants; + /** get unique overloaded function + * If tat->d_symbols contains an active overloaded function, it + * returns that function, where that function must be unique + * if reqUnique=true. + * Otherwise, it returns the null expression. + */ + cvc5::Term getOverloadedFunctionAt(const TypeArgTrie* tat, + bool reqUnique = true) const; +}; + +bool OverloadedTypeTrie::isOverloadedFunction(cvc5::Term fun) const +{ + return d_overloaded_symbols->find(fun) != d_overloaded_symbols->end(); +} + +cvc5::Term OverloadedTypeTrie::getOverloadedConstantForType( + const std::string& name, cvc5::Sort t) const +{ + std::unordered_map::const_iterator it = + d_overload_type_arg_trie.find(name); + if (it != d_overload_type_arg_trie.end()) + { + std::map::const_iterator its = + it->second.d_symbols.find(t); + if (its != it->second.d_symbols.end()) + { + cvc5::Term expr = its->second; + // must be an active symbol + if (isOverloadedFunction(expr)) + { + return expr; + } + } + } + return d_nullTerm; +} + +cvc5::Term OverloadedTypeTrie::getOverloadedFunctionForTypes( + const std::string& name, const std::vector& argTypes) const +{ + std::unordered_map::const_iterator it = + d_overload_type_arg_trie.find(name); + if (it != d_overload_type_arg_trie.end()) + { + const TypeArgTrie* tat = &it->second; + for (unsigned i = 0; i < argTypes.size(); i++) + { + std::map::const_iterator itc = + tat->d_children.find(argTypes[i]); + if (itc != tat->d_children.end()) + { + tat = &itc->second; + } + else + { + Trace("parser-overloading") + << "Could not find overloaded function " << name << std::endl; + + // no functions match + return d_nullTerm; + } + } + // we ensure that there is *only* one active symbol at this node + return getOverloadedFunctionAt(tat); + } + return d_nullTerm; +} + +bool OverloadedTypeTrie::bind(const string& name, + cvc5::Term prev_bound_obj, + cvc5::Term obj) +{ + bool retprev = true; + if (!isOverloadedFunction(prev_bound_obj)) + { + // mark previous as overloaded + retprev = markOverloaded(name, prev_bound_obj); + } + // mark this as overloaded + bool retobj = markOverloaded(name, obj); + return retprev && retobj; +} + +bool OverloadedTypeTrie::markOverloaded(const string& name, cvc5::Term obj) +{ + Trace("parser-overloading") << "Overloaded function : " << name; + Trace("parser-overloading") << " with type " << obj.getSort() << std::endl; + // get the argument types + cvc5::Sort t = obj.getSort(); + cvc5::Sort rangeType = t; + std::vector argTypes; + if (t.isFunction()) + { + argTypes = t.getFunctionDomainSorts(); + rangeType = t.getFunctionCodomainSort(); + } + else if (t.isDatatypeConstructor()) + { + argTypes = t.getDatatypeConstructorDomainSorts(); + rangeType = t.getDatatypeConstructorCodomainSort(); + } + else if (t.isDatatypeSelector()) + { + argTypes.push_back(t.getDatatypeSelectorDomainSort()); + rangeType = t.getDatatypeSelectorCodomainSort(); + } + // add to the trie + TypeArgTrie* tat = &d_overload_type_arg_trie[name]; + for (unsigned i = 0; i < argTypes.size(); i++) + { + tat = &(tat->d_children[argTypes[i]]); + } + + // check if function variants are allowed here + if (d_allowFunctionVariants || argTypes.empty()) + { + // they are allowed, check for redefinition + std::map::iterator it = + tat->d_symbols.find(rangeType); + if (it != tat->d_symbols.end()) + { + cvc5::Term prev_obj = it->second; + // if there is already an active function with the same name and expects + // the same argument types and has the same return type, we reject the + // re-declaration here. + if (isOverloadedFunction(prev_obj)) + { + return false; + } + } + } + else + { + // they are not allowed, we cannot have any function defined here. + cvc5::Term existingFun = getOverloadedFunctionAt(tat, false); + if (!existingFun.isNull()) + { + return false; + } + } + + // otherwise, update the symbols + d_overloaded_symbols->insert(obj); + tat->d_symbols[rangeType] = obj; + return true; +} + +cvc5::Term OverloadedTypeTrie::getOverloadedFunctionAt( + const OverloadedTypeTrie::TypeArgTrie* tat, bool reqUnique) const +{ + cvc5::Term retExpr; + for (std::map::const_iterator its = + tat->d_symbols.begin(); + its != tat->d_symbols.end(); + ++its) + { + cvc5::Term expr = its->second; + if (isOverloadedFunction(expr)) + { + if (retExpr.isNull()) + { + if (!reqUnique) + { + return expr; + } + else + { + retExpr = expr; + } + } + else + { + // multiple functions match + return d_nullTerm; + } + } + } + return retExpr; +} + +class SymbolTable::Implementation +{ + public: + Implementation() + : d_context(), + d_exprMap(&d_context), + d_typeMap(&d_context), + d_overload_trie(&d_context) + { + } + + ~Implementation() {} + + bool bind(const string& name, cvc5::Term obj, bool doOverload); + void bindType(const string& name, cvc5::Sort t); + void bindType(const string& name, + const vector& params, + cvc5::Sort t); + bool isBound(const string& name) const; + bool isBoundType(const string& name) const; + cvc5::Term lookup(const string& name) const; + cvc5::Sort lookupType(const string& name) const; + cvc5::Sort lookupType(const string& name, + const vector& params) const; + size_t lookupArity(const string& name); + void popScope(); + void pushScope(); + size_t getLevel() const; + void reset(); + void resetAssertions(); + //------------------------ operator overloading + /** implementation of function from header */ + bool isOverloadedFunction(cvc5::Term fun) const; + + /** implementation of function from header */ + cvc5::Term getOverloadedConstantForType(const std::string& name, + cvc5::Sort t) const; + + /** implementation of function from header */ + cvc5::Term getOverloadedFunctionForTypes( + const std::string& name, const std::vector& argTypes) const; + //------------------------ end operator overloading + private: + /** The context manager for the scope maps. */ + Context d_context; + + /** A map for expressions. */ + CDHashMap d_exprMap; + + /** A map for types. */ + using TypeMap = CDHashMap, cvc5::Sort>>; + TypeMap d_typeMap; + + //------------------------ operator overloading + // the null expression + cvc5::Term d_nullTerm; + // overloaded type trie, stores all information regarding overloading + OverloadedTypeTrie d_overload_trie; + /** bind with overloading + * This is called whenever obj is bound to name where overloading symbols is + * allowed. If a symbol is previously bound to that name, it marks both as + * overloaded. Returns false if the binding was invalid. + */ + bool bindWithOverloading(const string& name, cvc5::Term obj); + //------------------------ end operator overloading +}; /* SymbolTable::Implementation */ + +bool SymbolTable::Implementation::bind(const string& name, + cvc5::Term obj, + bool doOverload) +{ + PrettyCheckArgument(!obj.isNull(), obj, "cannot bind to a null cvc5::Term"); + Trace("sym-table") << "SymbolTable: bind " << name + << ", doOverload=" << doOverload << std::endl; + if (doOverload) + { + if (!bindWithOverloading(name, obj)) + { + return false; + } + } + d_exprMap.insert(name, obj); + + return true; +} + +bool SymbolTable::Implementation::isBound(const string& name) const +{ + return d_exprMap.find(name) != d_exprMap.end(); +} + +cvc5::Term SymbolTable::Implementation::lookup(const string& name) const +{ + Assert(isBound(name)); + cvc5::Term expr = (*d_exprMap.find(name)).second; + if (isOverloadedFunction(expr)) + { + return d_nullTerm; + } + else + { + return expr; + } +} + +void SymbolTable::Implementation::bindType(const string& name, cvc5::Sort t) +{ + d_typeMap.insert(name, make_pair(vector(), t)); +} + +void SymbolTable::Implementation::bindType(const string& name, + const vector& params, + cvc5::Sort t) +{ + if (TraceIsOn("sort")) + { + Trace("sort") << "bindType(" << name << ", ["; + if (params.size() > 0) + { + copy(params.begin(), + params.end() - 1, + ostream_iterator(Trace("sort"), ", ")); + Trace("sort") << params.back(); + } + Trace("sort") << "], " << t << ")" << endl; + } + + d_typeMap.insert(name, make_pair(params, t)); +} + +bool SymbolTable::Implementation::isBoundType(const string& name) const +{ + return d_typeMap.find(name) != d_typeMap.end(); +} + +cvc5::Sort SymbolTable::Implementation::lookupType(const string& name) const +{ + std::pair, cvc5::Sort> p = + (*d_typeMap.find(name)).second; + PrettyCheckArgument(p.first.size() == 0, + name, + "type constructor arity is wrong: " + "`%s' requires %u parameters but was provided 0", + name.c_str(), + p.first.size()); + return p.second; +} + +cvc5::Sort SymbolTable::Implementation::lookupType( + const string& name, const vector& params) const +{ + std::pair, cvc5::Sort> p = + (*d_typeMap.find(name)).second; + PrettyCheckArgument(p.first.size() == params.size(), + params, + "type constructor arity is wrong: " + "`%s' requires %u parameters but was provided %u", + name.c_str(), + p.first.size(), + params.size()); + if (p.first.size() == 0) + { + PrettyCheckArgument(p.second.isUninterpretedSort(), name.c_str()); + return p.second; + } + if (p.second.isDatatype()) + { + PrettyCheckArgument(p.second.getDatatype().isParametric(), + name, + "expected parametric datatype"); + return p.second.instantiate(params); + } + bool isUninterpretedSortConstructor = + p.second.isUninterpretedSortConstructor(); + if (TraceIsOn("sort")) + { + Trace("sort") << "instantiating using a sort " + << (isUninterpretedSortConstructor ? "constructor" + : "substitution") + << std::endl; + Trace("sort") << "have formals ["; + copy(p.first.begin(), + p.first.end() - 1, + ostream_iterator(Trace("sort"), ", ")); + Trace("sort") << p.first.back() << "]" << std::endl << "parameters ["; + copy(params.begin(), + params.end() - 1, + ostream_iterator(Trace("sort"), ", ")); + Trace("sort") << params.back() << "]" << endl + << "type ctor " << name << std::endl + << "type is " << p.second << std::endl; + } + cvc5::Sort instantiation = isUninterpretedSortConstructor + ? p.second.instantiate(params) + : p.second.substitute(p.first, params); + Trace("sort") << "instance is " << instantiation << std::endl; + + return instantiation; +} + +size_t SymbolTable::Implementation::lookupArity(const string& name) +{ + std::pair, cvc5::Sort> p = + (*d_typeMap.find(name)).second; + return p.first.size(); +} + +void SymbolTable::Implementation::popScope() +{ + // should not pop beyond level one + if (d_context.getLevel() == 0) + { + throw ScopeException(); + } + d_context.pop(); +} + +void SymbolTable::Implementation::pushScope() { d_context.push(); } + +size_t SymbolTable::Implementation::getLevel() const +{ + return d_context.getLevel(); +} + +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(cvc5::Term fun) const +{ + return d_overload_trie.isOverloadedFunction(fun); +} + +cvc5::Term SymbolTable::Implementation::getOverloadedConstantForType( + const std::string& name, cvc5::Sort t) const +{ + return d_overload_trie.getOverloadedConstantForType(name, t); +} + +cvc5::Term SymbolTable::Implementation::getOverloadedFunctionForTypes( + const std::string& name, const std::vector& argTypes) const +{ + return d_overload_trie.getOverloadedFunctionForTypes(name, argTypes); +} + +bool SymbolTable::Implementation::bindWithOverloading(const string& name, + cvc5::Term obj) +{ + CDHashMap::const_iterator it = d_exprMap.find(name); + if (it != d_exprMap.end()) + { + const cvc5::Term& prev_bound_obj = (*it).second; + if (prev_bound_obj != obj) + { + return d_overload_trie.bind(name, prev_bound_obj, obj); + } + } + return true; +} + +bool SymbolTable::isOverloadedFunction(cvc5::Term fun) const +{ + return d_implementation->isOverloadedFunction(fun); +} + +cvc5::Term SymbolTable::getOverloadedConstantForType(const std::string& name, + cvc5::Sort t) const +{ + return d_implementation->getOverloadedConstantForType(name, t); +} + +cvc5::Term SymbolTable::getOverloadedFunctionForTypes( + const std::string& name, const std::vector& argTypes) const +{ + return d_implementation->getOverloadedFunctionForTypes(name, argTypes); +} + +SymbolTable::SymbolTable() : d_implementation(new SymbolTable::Implementation()) +{ +} + +SymbolTable::~SymbolTable() {} +bool SymbolTable::bind(const string& name, cvc5::Term obj, bool doOverload) +{ + return d_implementation->bind(name, obj, doOverload); +} + +void SymbolTable::bindType(const string& name, cvc5::Sort t) +{ + d_implementation->bindType(name, t); +} + +void SymbolTable::bindType(const string& name, + const vector& params, + cvc5::Sort t) +{ + d_implementation->bindType(name, params, t); +} + +bool SymbolTable::isBound(const string& name) const +{ + return d_implementation->isBound(name); +} +bool SymbolTable::isBoundType(const string& name) const +{ + return d_implementation->isBoundType(name); +} +cvc5::Term SymbolTable::lookup(const string& name) const +{ + return d_implementation->lookup(name); +} +cvc5::Sort SymbolTable::lookupType(const string& name) const +{ + return d_implementation->lookupType(name); +} + +cvc5::Sort SymbolTable::lookupType(const string& name, + const vector& params) const +{ + return d_implementation->lookupType(name, params); +} +size_t SymbolTable::lookupArity(const string& name) +{ + return d_implementation->lookupArity(name); +} +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 cvc5::internal::parser diff --git a/src/parser/symbol_table.h b/src/parser/symbol_table.h new file mode 100644 index 000000000..575b8de26 --- /dev/null +++ b/src/parser/symbol_table.h @@ -0,0 +1,206 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Morgan Deters, Christopher L. Conway + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Convenience class for scoping variable and type declarations. + */ + +#include "cvc5parser_public.h" + +#ifndef CVC5__SYMBOL_TABLE_H +#define CVC5__SYMBOL_TABLE_H + +#include +#include +#include + +#include "base/exception.h" +#include "cvc5_export.h" + +namespace cvc5 { +class Solver; +class Sort; +class Term; +} // namespace cvc5 + +namespace cvc5::internal::parser { + +class CVC5_EXPORT ScopeException : public internal::Exception +{ +}; + +/** + * A convenience class for handling scoped declarations. Implements the usual + * nested scoping rules for declarations, with separate bindings for expressions + * and types. + */ +class CVC5_EXPORT SymbolTable +{ + public: + /** Create a symbol table. */ + SymbolTable(); + ~SymbolTable(); + + /** + * Bind an expression to a name in the current scope level. + * + * When doOverload is false: + * if name is already bound to an expression in the current + * level, then the binding is replaced. If name is bound + * in a previous level, then the binding is "covered" by this one + * until the current scope is popped. + * If levelZero is true the name shouldn't be already bound. + * + * When doOverload is true: + * if name is already bound to an expression in the current + * level, then we mark the previous bound expression and obj as overloaded + * functions. + * + * @param name an identifier + * @param obj the expression to bind to name + * @param doOverload set if the binding can overload the function name. + * + * Returns false if the binding was invalid. + */ + bool bind(const std::string& name, cvc5::Term obj, bool doOverload = false); + + /** + * Bind a type to a name in the current scope. If name + * is already bound to a type in the current level, then the binding + * is replaced. If name is bound in a previous level, + * then the binding is "covered" by this one until the current scope + * is popped. + * + * @param name an identifier + * @param t the type to bind to name + */ + void bindType(const std::string& name, cvc5::Sort t); + + /** + * Bind a type to a name in the current scope. If name + * is already bound to a type or type constructor in the current + * level, then the binding is replaced. If name is + * bound in a previous level, then the binding is "covered" by this + * one until the current scope is popped. + * + * @param name an identifier + * @param params the parameters to the type + * @param t the type to bind to name + */ + void bindType(const std::string& name, + const std::vector& params, + cvc5::Sort t); + + /** + * Check whether a name is bound to an expression with bind(). + * + * @param name the identifier to check. + * @returns true iff name is bound in the current scope. + */ + bool isBound(const std::string& name) const; + + /** + * Check whether a name is bound to a type (or type constructor). + * + * @param name the identifier to check. + * @returns true iff name is bound to a type in the current scope. + */ + bool isBoundType(const std::string& name) const; + + /** + * Lookup a bound expression. + * + * @param name the identifier to lookup + * @returns the unique expression bound to name in the current + * scope. + * It returns the null expression if there is not a unique expression bound to + * name in the current scope (i.e. if there is not exactly one). + */ + cvc5::Term lookup(const std::string& name) const; + + /** + * Lookup a bound type. + * + * @param name the type identifier to lookup + * @returns the type bound to name in the current scope. + */ + cvc5::Sort lookupType(const std::string& name) const; + + /** + * Lookup a bound parameterized type. + * + * @param name the type-constructor identifier to lookup + * @param params the types to use to parameterize the type + * @returns the type bound to name(params) in + * the current scope. + */ + cvc5::Sort lookupType(const std::string& name, + const std::vector& params) const; + + /** + * Lookup the arity of a bound parameterized type. + */ + size_t lookupArity(const std::string& name); + + /** + * Pop a scope level, deletes all bindings since the last call to pushScope, + * and decreases the level by 1. + * + * @throws ScopeException if the scope level is 0. + */ + void popScope(); + + /** Push a scope level and increase the scope level by 1. */ + void pushScope(); + + /** Get the current level of this symbol table. */ + size_t getLevel() const; + + /** Reset everything. */ + void reset(); + /** Reset assertions. */ + void resetAssertions(); + + //------------------------ operator overloading + /** is this function overloaded? */ + bool isOverloadedFunction(cvc5::Term fun) const; + + /** Get overloaded constant for type. + * If possible, it returns the defined symbol with name + * that has type t. Otherwise returns null expression. + */ + cvc5::Term getOverloadedConstantForType(const std::string& name, + cvc5::Sort t) const; + + /** + * If possible, returns the unique defined function for a name + * that expects arguments with types "argTypes". + * For example, if argTypes = (T1, ..., Tn), then this may return an + * expression with type function(T1, ..., Tn), or constructor(T1, ...., Tn). + * + * If there is not a unique defined function for the name and argTypes, + * this returns the null expression. This can happen either if there are + * no functions with name and expected argTypes, or alternatively there is + * more than one function with name and expected argTypes. + */ + cvc5::Term getOverloadedFunctionForTypes( + const std::string& name, const std::vector& argTypes) const; + //------------------------ end operator overloading + + private: + /** The implementation of the symbol table */ + class Implementation; + std::unique_ptr d_implementation; +}; /* class SymbolTable */ + +} // namespace cvc5::internal::parser + +#endif /* CVC5__SYMBOL_TABLE_H */ diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 5599eab39..43c0b06c6 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -27,19 +27,20 @@ #include "base/modal_exception.h" #include "base/output.h" #include "expr/node.h" -#include "expr/symbol_manager.h" #include "expr/type_node.h" #include "options/io_utils.h" #include "options/main_options.h" #include "options/options.h" #include "options/printer_options.h" #include "options/smt_options.h" +#include "parser/api/cpp/symbol_manager.h" #include "printer/printer.h" #include "proof/unsat_core.h" #include "util/smt2_quote_string.h" #include "util/utility.h" using namespace std; +using namespace cvc5::parser; namespace cvc5 { @@ -1054,7 +1055,7 @@ void DefineFunctionCommand::invoke(cvc5::Solver* solver, SymbolManager* sm) bool global = sm->getGlobalDeclarations(); cvc5::Term fun = solver->defineFun(d_symbol, d_formals, d_sort, d_formula, global); - sm->getSymbolTable()->bind(d_symbol, fun, global); + sm->bind(d_symbol, fun, global); d_commandStatus = CommandSuccess::instance(); } catch (exception& e) diff --git a/src/smt/command.h b/src/smt/command.h index 534208205..0c85732f2 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -36,10 +36,13 @@ namespace cvc5 { class Solver; class Term; -class SymbolManager; class Command; class CommandStatus; +namespace parser { +class SymbolManager; +} + namespace smt { class Model; } @@ -144,12 +147,12 @@ class CVC5_EXPORT Command /** * Invoke the command on the solver and symbol manager sm. */ - virtual void invoke(cvc5::Solver* solver, SymbolManager* sm) = 0; + virtual void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) = 0; /** * Same as above, and prints the result to output stream out. */ virtual void invoke(cvc5::Solver* solver, - SymbolManager* sm, + parser::SymbolManager* sm, std::ostream& out); virtual void toStream(std::ostream& out) const = 0; @@ -241,7 +244,7 @@ class CVC5_EXPORT EmptyCommand : public Command public: EmptyCommand(std::string name = ""); std::string getName() const; - void invoke(cvc5::Solver* solver, SymbolManager* sm) override; + void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override; std::string getCommandName() const override; void toStream(std::ostream& out) const override; @@ -256,9 +259,9 @@ class CVC5_EXPORT EchoCommand : public Command std::string getOutput() const; - void invoke(cvc5::Solver* solver, SymbolManager* sm) override; + void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override; void invoke(cvc5::Solver* solver, - SymbolManager* sm, + parser::SymbolManager* sm, std::ostream& out) override; std::string getCommandName() const override; @@ -278,7 +281,7 @@ class CVC5_EXPORT AssertCommand : public Command cvc5::Term getTerm() const; - void invoke(cvc5::Solver* solver, SymbolManager* sm) override; + void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override; std::string getCommandName() const override; void toStream(std::ostream& out) const override; @@ -289,7 +292,7 @@ class CVC5_EXPORT PushCommand : public Command public: PushCommand(uint32_t nscopes); - void invoke(cvc5::Solver* solver, SymbolManager* sm) override; + void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override; std::string getCommandName() const override; void toStream(std::ostream& out) const override; @@ -302,7 +305,7 @@ class CVC5_EXPORT PopCommand : public Command public: PopCommand(uint32_t nscopes); - void invoke(cvc5::Solver* solver, SymbolManager* sm) override; + void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override; std::string getCommandName() const override; void toStream(std::ostream& out) const override; @@ -318,7 +321,7 @@ class CVC5_EXPORT DeclarationDefinitionCommand : public Command public: DeclarationDefinitionCommand(const std::string& id); - void invoke(cvc5::Solver* solver, SymbolManager* sm) override = 0; + void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override = 0; std::string getSymbol() const; }; /* class DeclarationDefinitionCommand */ @@ -335,7 +338,7 @@ class CVC5_EXPORT DeclareFunctionCommand : public DeclarationDefinitionCommand cvc5::Term getFunction() const; cvc5::Sort getSort() const; - void invoke(cvc5::Solver* solver, SymbolManager* sm) override; + void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override; std::string getCommandName() const override; void toStream(std::ostream& out) const override; }; /* class DeclareFunctionCommand */ @@ -356,7 +359,7 @@ class CVC5_EXPORT DeclarePoolCommand : public DeclarationDefinitionCommand cvc5::Sort getSort() const; const std::vector& getInitialValue() const; - void invoke(cvc5::Solver* solver, SymbolManager* sm) override; + void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override; std::string getCommandName() const override; void toStream(std::ostream& out) const override; }; /* class DeclarePoolCommand */ @@ -372,7 +375,7 @@ class CVC5_EXPORT DeclareOracleFunCommand : public Command Sort getSort() const; const std::string& getBinaryName() const; - void invoke(Solver* solver, SymbolManager* sm) override; + void invoke(Solver* solver, parser::SymbolManager* sm) override; std::string getCommandName() const override; void toStream(std::ostream& out) const override; @@ -397,7 +400,7 @@ class CVC5_EXPORT DeclareSortCommand : public DeclarationDefinitionCommand size_t getArity() const; cvc5::Sort getSort() const; - void invoke(cvc5::Solver* solver, SymbolManager* sm) override; + void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override; std::string getCommandName() const override; void toStream(std::ostream& out) const override; }; /* class DeclareSortCommand */ @@ -417,7 +420,7 @@ class CVC5_EXPORT DefineSortCommand : public DeclarationDefinitionCommand const std::vector& getParameters() const; cvc5::Sort getSort() const; - void invoke(cvc5::Solver* solver, SymbolManager* sm) override; + void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override; std::string getCommandName() const override; void toStream(std::ostream& out) const override; }; /* class DefineSortCommand */ @@ -437,7 +440,7 @@ class CVC5_EXPORT DefineFunctionCommand : public DeclarationDefinitionCommand cvc5::Sort getSort() const; cvc5::Term getFormula() const; - void invoke(cvc5::Solver* solver, SymbolManager* sm) override; + void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override; std::string getCommandName() const override; void toStream(std::ostream& out) const override; @@ -469,7 +472,7 @@ class CVC5_EXPORT DefineFunctionRecCommand : public Command const std::vector >& getFormals() const; const std::vector& getFormulas() const; - void invoke(cvc5::Solver* solver, SymbolManager* sm) override; + void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override; std::string getCommandName() const override; void toStream(std::ostream& out) const override; @@ -494,7 +497,7 @@ class CVC5_EXPORT DeclareHeapCommand : public Command DeclareHeapCommand(cvc5::Sort locSort, cvc5::Sort dataSort); cvc5::Sort getLocationSort() const; cvc5::Sort getDataSort() const; - void invoke(cvc5::Solver* solver, SymbolManager* sm) override; + void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override; std::string getCommandName() const override; void toStream(std::ostream& out) const override; @@ -514,7 +517,7 @@ class CVC5_EXPORT CheckSatCommand : public Command public: CheckSatCommand(); cvc5::Result getResult() const; - void invoke(cvc5::Solver* solver, SymbolManager* sm) override; + void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override; void printResult(cvc5::Solver* solver, std::ostream& out) const override; std::string getCommandName() const override; void toStream(std::ostream& out) const override; @@ -536,7 +539,7 @@ class CVC5_EXPORT CheckSatAssumingCommand : public Command const std::vector& getTerms() const; cvc5::Result getResult() const; - void invoke(cvc5::Solver* solver, SymbolManager* sm) override; + void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override; void printResult(cvc5::Solver* solver, std::ostream& out) const override; std::string getCommandName() const override; void toStream(std::ostream& out) const override; @@ -564,7 +567,7 @@ class CVC5_EXPORT DeclareSygusVarCommand : public DeclarationDefinitionCommand * The declared sygus variable is communicated to the SMT engine in case a * synthesis conjecture is built later on. */ - void invoke(cvc5::Solver* solver, SymbolManager* sm) override; + void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override; /** returns this command's name */ std::string getCommandName() const override; /** prints this command */ @@ -607,7 +610,7 @@ class CVC5_EXPORT SynthFunCommand : public DeclarationDefinitionCommand * The declared function-to-synthesize is communicated to the SMT engine in * case a synthesis conjecture is built later on. */ - void invoke(cvc5::Solver* solver, SymbolManager* sm) override; + void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override; /** returns this command's name */ std::string getCommandName() const override; /** prints this command */ @@ -638,7 +641,7 @@ class CVC5_EXPORT SygusConstraintCommand : public Command * The declared constraint is communicated to the SMT engine in case a * synthesis conjecture is built later on. */ - void invoke(cvc5::Solver* solver, SymbolManager* sm) override; + void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override; /** returns this command's name */ std::string getCommandName() const override; /** prints this command */ @@ -677,7 +680,7 @@ class CVC5_EXPORT SygusInvConstraintCommand : public Command * invariant constraint is built, in case an actual synthesis conjecture is * built later on. */ - void invoke(cvc5::Solver* solver, SymbolManager* sm) override; + void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override; /** returns this command's name */ std::string getCommandName() const override; /** prints this command */ @@ -707,7 +710,7 @@ class CVC5_EXPORT CheckSynthCommand : public Command * and then perform a satisfiability check, whose result is stored in * d_result. */ - void invoke(cvc5::Solver* solver, SymbolManager* sm) override; + void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override; /** returns this command's name */ std::string getCommandName() const override; /** prints this command */ @@ -736,7 +739,7 @@ class CVC5_EXPORT SimplifyCommand : public Command cvc5::Term getTerm() const; cvc5::Term getResult() const; - void invoke(cvc5::Solver* solver, SymbolManager* sm) override; + void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override; void printResult(cvc5::Solver* solver, std::ostream& out) const override; std::string getCommandName() const override; void toStream(std::ostream& out) const override; @@ -754,7 +757,7 @@ class CVC5_EXPORT GetValueCommand : public Command const std::vector& getTerms() const; cvc5::Term getResult() const; - void invoke(cvc5::Solver* solver, SymbolManager* sm) override; + void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override; void printResult(cvc5::Solver* solver, std::ostream& out) const override; std::string getCommandName() const override; void toStream(std::ostream& out) const override; @@ -769,7 +772,7 @@ class CVC5_EXPORT GetAssignmentCommand : public Command GetAssignmentCommand(); cvc5::Term getResult() const; - void invoke(cvc5::Solver* solver, SymbolManager* sm) override; + void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override; void printResult(cvc5::Solver* solver, std::ostream& out) const override; std::string getCommandName() const override; void toStream(std::ostream& out) const override; @@ -779,7 +782,7 @@ class CVC5_EXPORT GetModelCommand : public Command { public: GetModelCommand(); - void invoke(cvc5::Solver* solver, SymbolManager* sm) override; + void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override; void printResult(cvc5::Solver* solver, std::ostream& out) const override; std::string getCommandName() const override; void toStream(std::ostream& out) const override; @@ -795,7 +798,7 @@ class CVC5_EXPORT BlockModelCommand : public Command public: BlockModelCommand(modes::BlockModelsMode mode); - void invoke(cvc5::Solver* solver, SymbolManager* sm) override; + void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override; std::string getCommandName() const override; void toStream(std::ostream& out) const override; @@ -811,7 +814,7 @@ class CVC5_EXPORT BlockModelValuesCommand : public Command BlockModelValuesCommand(const std::vector& terms); const std::vector& getTerms() const; - void invoke(cvc5::Solver* solver, SymbolManager* sm) override; + void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override; std::string getCommandName() const override; void toStream(std::ostream& out) const override; @@ -825,7 +828,7 @@ class CVC5_EXPORT GetProofCommand : public Command public: GetProofCommand(); - void invoke(cvc5::Solver* solver, SymbolManager* sm) override; + void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override; void printResult(cvc5::Solver* solver, std::ostream& out) const override; @@ -843,7 +846,7 @@ class CVC5_EXPORT GetInstantiationsCommand : public Command GetInstantiationsCommand(); static bool isEnabled(cvc5::Solver* solver, const cvc5::Result& res); - void invoke(cvc5::Solver* solver, SymbolManager* sm) override; + void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override; void printResult(cvc5::Solver* solver, std::ostream& out) const override; std::string getCommandName() const override; void toStream(std::ostream& out) const override; @@ -878,7 +881,7 @@ class CVC5_EXPORT GetInterpolantCommand : public Command * query. */ cvc5::Term getResult() const; - void invoke(cvc5::Solver* solver, SymbolManager* sm) override; + void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override; void printResult(cvc5::Solver* solver, std::ostream& out) const override; std::string getCommandName() const override; void toStream(std::ostream& out) const override; @@ -905,7 +908,7 @@ class CVC5_EXPORT GetInterpolantNextCommand : public Command */ cvc5::Term getResult() const; - void invoke(cvc5::Solver* solver, SymbolManager* sm) override; + void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override; void printResult(cvc5::Solver* solver, std::ostream& out) const override; std::string getCommandName() const override; void toStream(std::ostream& out) const override; @@ -945,7 +948,7 @@ class CVC5_EXPORT GetAbductCommand : public Command */ cvc5::Term getResult() const; - void invoke(cvc5::Solver* solver, SymbolManager* sm) override; + void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override; void printResult(cvc5::Solver* solver, std::ostream& out) const override; std::string getCommandName() const override; void toStream(std::ostream& out) const override; @@ -971,7 +974,7 @@ class CVC5_EXPORT GetAbductNextCommand : public Command */ cvc5::Term getResult() const; - void invoke(cvc5::Solver* solver, SymbolManager* sm) override; + void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override; void printResult(cvc5::Solver* solver, std::ostream& out) const override; std::string getCommandName() const override; void toStream(std::ostream& out) const override; @@ -996,7 +999,7 @@ class CVC5_EXPORT GetQuantifierEliminationCommand : public Command cvc5::Term getTerm() const; bool getDoFull() const; - void invoke(cvc5::Solver* solver, SymbolManager* sm) override; + void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override; cvc5::Term getResult() const; void printResult(cvc5::Solver* solver, std::ostream& out) const override; @@ -1008,7 +1011,7 @@ class CVC5_EXPORT GetUnsatAssumptionsCommand : public Command { public: GetUnsatAssumptionsCommand(); - void invoke(cvc5::Solver* solver, SymbolManager* sm) override; + void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override; std::vector getResult() const; void printResult(cvc5::Solver* solver, std::ostream& out) const override; std::string getCommandName() const override; @@ -1024,7 +1027,7 @@ class CVC5_EXPORT GetUnsatCoreCommand : public Command GetUnsatCoreCommand(); const std::vector& getUnsatCore() const; - void invoke(cvc5::Solver* solver, SymbolManager* sm) override; + void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override; void printResult(cvc5::Solver* solver, std::ostream& out) const override; std::string getCommandName() const override; @@ -1034,7 +1037,7 @@ class CVC5_EXPORT GetUnsatCoreCommand : public Command /** The solver we were invoked with */ cvc5::Solver* d_solver; /** The symbol manager we were invoked with */ - SymbolManager* d_sm; + parser::SymbolManager* d_sm; /** the result of the unsat core call */ std::vector d_result; }; /* class GetUnsatCoreCommand */ @@ -1045,7 +1048,7 @@ class CVC5_EXPORT GetDifficultyCommand : public Command GetDifficultyCommand(); const std::map& getDifficultyMap() const; - void invoke(cvc5::Solver* solver, SymbolManager* sm) override; + void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override; void printResult(cvc5::Solver* solver, std::ostream& out) const override; std::string getCommandName() const override; @@ -1053,7 +1056,7 @@ class CVC5_EXPORT GetDifficultyCommand : public Command protected: /** The symbol manager we were invoked with */ - SymbolManager* d_sm; + parser::SymbolManager* d_sm; /** the result of the get difficulty call */ std::map d_result; }; @@ -1064,7 +1067,7 @@ class CVC5_EXPORT GetLearnedLiteralsCommand : public Command GetLearnedLiteralsCommand(); const std::vector& getLearnedLiterals() const; - void invoke(cvc5::Solver* solver, SymbolManager* sm) override; + void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override; void printResult(cvc5::Solver* solver, std::ostream& out) const override; std::string getCommandName() const override; @@ -1083,7 +1086,7 @@ class CVC5_EXPORT GetAssertionsCommand : public Command public: GetAssertionsCommand(); - void invoke(cvc5::Solver* solver, SymbolManager* sm) override; + void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override; std::string getResult() const; void printResult(cvc5::Solver* solver, std::ostream& out) const override; std::string getCommandName() const override; @@ -1099,7 +1102,7 @@ class CVC5_EXPORT SetBenchmarkLogicCommand : public Command SetBenchmarkLogicCommand(std::string logic); std::string getLogic() const; - void invoke(cvc5::Solver* solver, SymbolManager* sm) override; + void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override; std::string getCommandName() const override; void toStream(std::ostream& out) const override; }; /* class SetBenchmarkLogicCommand */ @@ -1116,7 +1119,7 @@ class CVC5_EXPORT SetInfoCommand : public Command const std::string& getFlag() const; const std::string& getValue() const; - void invoke(cvc5::Solver* solver, SymbolManager* sm) override; + void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override; std::string getCommandName() const override; void toStream(std::ostream& out) const override; }; /* class SetInfoCommand */ @@ -1133,7 +1136,7 @@ class CVC5_EXPORT GetInfoCommand : public Command std::string getFlag() const; std::string getResult() const; - void invoke(cvc5::Solver* solver, SymbolManager* sm) override; + void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override; void printResult(cvc5::Solver* solver, std::ostream& out) const override; std::string getCommandName() const override; void toStream(std::ostream& out) const override; @@ -1151,7 +1154,7 @@ class CVC5_EXPORT SetOptionCommand : public Command const std::string& getFlag() const; const std::string& getValue() const; - void invoke(cvc5::Solver* solver, SymbolManager* sm) override; + void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override; std::string getCommandName() const override; void toStream(std::ostream& out) const override; }; /* class SetOptionCommand */ @@ -1168,7 +1171,7 @@ class CVC5_EXPORT GetOptionCommand : public Command std::string getFlag() const; std::string getResult() const; - void invoke(cvc5::Solver* solver, SymbolManager* sm) override; + void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override; void printResult(cvc5::Solver* solver, std::ostream& out) const override; std::string getCommandName() const override; void toStream(std::ostream& out) const override; @@ -1184,7 +1187,7 @@ class CVC5_EXPORT DatatypeDeclarationCommand : public Command DatatypeDeclarationCommand(const std::vector& datatypes); const std::vector& getDatatypes() const; - void invoke(cvc5::Solver* solver, SymbolManager* sm) override; + void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override; std::string getCommandName() const override; void toStream(std::ostream& out) const override; }; /* class DatatypeDeclarationCommand */ @@ -1193,7 +1196,7 @@ class CVC5_EXPORT ResetCommand : public Command { public: ResetCommand() {} - void invoke(cvc5::Solver* solver, SymbolManager* sm) override; + void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override; std::string getCommandName() const override; void toStream(std::ostream& out) const override; }; /* class ResetCommand */ @@ -1202,7 +1205,7 @@ class CVC5_EXPORT ResetAssertionsCommand : public Command { public: ResetAssertionsCommand() {} - void invoke(cvc5::Solver* solver, SymbolManager* sm) override; + void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override; std::string getCommandName() const override; void toStream(std::ostream& out) const override; }; /* class ResetAssertionsCommand */ @@ -1211,7 +1214,7 @@ class CVC5_EXPORT QuitCommand : public Command { public: QuitCommand() {} - void invoke(cvc5::Solver* solver, SymbolManager* sm) override; + void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override; std::string getCommandName() const override; void toStream(std::ostream& out) const override; }; /* class QuitCommand */ diff --git a/test/unit/main/interactive_shell_black.cpp b/test/unit/main/interactive_shell_black.cpp index d96a02a77..dd916167d 100644 --- a/test/unit/main/interactive_shell_black.cpp +++ b/test/unit/main/interactive_shell_black.cpp @@ -18,15 +18,18 @@ #include #include "api/cpp/cvc5.h" -#include "expr/symbol_manager.h" #include "main/interactive_shell.h" #include "options/base_options.h" #include "options/language.h" #include "options/options.h" +#include "parser/api/cpp/symbol_manager.h" #include "parser/parser_builder.h" #include "smt/command.h" #include "test.h" +using namespace cvc5::parser; +using namespace cvc5::internal::parser; + namespace cvc5::internal { namespace test { diff --git a/test/unit/node/symbol_table_black.cpp b/test/unit/node/symbol_table_black.cpp index 3d5ba7cfa..f4cea0bb5 100644 --- a/test/unit/node/symbol_table_black.cpp +++ b/test/unit/node/symbol_table_black.cpp @@ -20,13 +20,14 @@ #include "base/exception.h" #include "context/context.h" #include "expr/kind.h" -#include "expr/symbol_table.h" +#include "parser/symbol_table.h" #include "test_api.h" namespace cvc5::internal { using namespace kind; using namespace context; +using namespace parser; namespace test { diff --git a/test/unit/parser/parser_black.cpp b/test/unit/parser/parser_black.cpp index 904f3d463..028b7abf4 100644 --- a/test/unit/parser/parser_black.cpp +++ b/test/unit/parser/parser_black.cpp @@ -17,20 +17,20 @@ #include "api/cpp/cvc5.h" #include "base/output.h" -#include "expr/symbol_manager.h" #include "options/base_options.h" #include "options/language.h" #include "options/options.h" +#include "parser/api/cpp/symbol_manager.h" #include "parser/parser.h" #include "parser/parser_builder.h" #include "parser/smt2/smt2.h" #include "smt/command.h" #include "test.h" -namespace cvc5::internal { - -using namespace parser; +using namespace cvc5::parser; +using namespace cvc5::internal::parser; +namespace cvc5::internal { namespace test { class TestParserBlackParser : public TestInternal diff --git a/test/unit/parser/parser_builder_black.cpp b/test/unit/parser/parser_builder_black.cpp index 1dab98d80..ae82898ef 100644 --- a/test/unit/parser/parser_builder_black.cpp +++ b/test/unit/parser/parser_builder_black.cpp @@ -22,17 +22,16 @@ #include #include "api/cpp/cvc5.h" -#include "expr/symbol_manager.h" #include "options/language.h" +#include "parser/api/cpp/symbol_manager.h" #include "parser/parser.h" #include "parser/parser_builder.h" #include "smt/command.h" #include "test_api.h" -namespace cvc5::internal { - -using namespace parser; +using namespace cvc5::parser; +namespace cvc5::internal { namespace test { class TestParseBlackParserBuilder : public TestApi