From 55d024accae4abf992c9585961bd0765d9eef2ab Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Mon, 27 Jun 2022 15:28:27 -0700 Subject: [PATCH] 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. --- src/CMakeLists.txt | 12 ++ src/context/cdhashmap.h | 2 +- src/context/cdhashset.h | 2 +- src/context/cdinsert_hashmap.h | 24 ++- src/context/cdlist.h | 2 +- src/context/cdo.h | 2 +- src/context/context.h | 14 +- src/context/context_mm.h | 10 +- src/expr/CMakeLists.txt | 4 - src/main/command_executor.cpp | 2 + src/main/command_executor.h | 8 +- src/main/interactive_shell.cpp | 2 +- src/main/interactive_shell.h | 9 +- src/parser/CMakeLists.txt | 4 + .../api/cpp}/symbol_manager.cpp | 39 +++-- src/{expr => parser/api/cpp}/symbol_manager.h | 38 ++++- src/parser/parser.h | 6 +- src/parser/parser_builder.h | 2 +- src/{expr => parser}/symbol_table.cpp | 140 +++++++++++------- src/{expr => parser}/symbol_table.h | 10 +- src/smt/command.cpp | 5 +- src/smt/command.h | 111 +++++++------- test/unit/main/interactive_shell_black.cpp | 5 +- test/unit/node/symbol_table_black.cpp | 3 +- test/unit/parser/parser_black.cpp | 8 +- test/unit/parser/parser_builder_black.cpp | 7 +- 26 files changed, 290 insertions(+), 181 deletions(-) rename src/{expr => parser/api/cpp}/symbol_manager.cpp (94%) rename src/{expr => parser/api/cpp}/symbol_manager.h (85%) rename src/{expr => parser}/symbol_table.cpp (91%) rename src/{expr => parser}/symbol_table.h (97%) 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/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/expr/symbol_manager.cpp b/src/parser/api/cpp/symbol_manager.cpp similarity index 94% rename from src/expr/symbol_manager.cpp rename to src/parser/api/cpp/symbol_manager.cpp index 3e8cf3207..10cb4cc5b 100644 --- a/src/expr/symbol_manager.cpp +++ b/src/parser/api/cpp/symbol_manager.cpp @@ -13,16 +13,18 @@ * The symbol manager. */ -#include "expr/symbol_manager.h" +#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 { +namespace cvc5::parser { // ---------------------------------------------- SymbolManager::Implementation @@ -50,6 +52,8 @@ class SymbolManager::Implementation } ~Implementation() { d_context.pop(); } + SymbolTable& getSymbolTable() { return d_symtabAllocated; } + /** set expression name */ NamingResult setExpressionName(cvc5::Term t, const std::string& name, @@ -93,6 +97,10 @@ class SymbolManager::Implementation 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 */ @@ -246,14 +254,16 @@ void SymbolManager::Implementation::pushScope(bool 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 internal::ScopeException(); + throw ScopeException(); } d_context.pop(); Trace("sym-manager-debug") @@ -278,6 +288,8 @@ const std::string& SymbolManager::Implementation::getLastSynthName() const 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) { @@ -308,9 +320,16 @@ SymbolManager::SymbolManager(cvc5::Solver* s) SymbolManager::~SymbolManager() {} -internal::SymbolTable* SymbolManager::getSymbolTable() +SymbolTable* SymbolManager::getSymbolTable() { - return &d_symtabAllocated; + 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, @@ -370,7 +389,7 @@ void SymbolManager::addFunctionToSynthesize(cvc5::Term f) size_t SymbolManager::scopeLevel() const { - return d_symtabAllocated.getLevel(); + return d_implementation->getSymbolTable().getLevel(); } void SymbolManager::pushScope(bool isUserContext) @@ -382,7 +401,6 @@ void SymbolManager::pushScope(bool isUserContext) return; } d_implementation->pushScope(isUserContext); - d_symtabAllocated.pushScope(); } void SymbolManager::popScope() @@ -396,7 +414,6 @@ void SymbolManager::popScope() { return; } - d_symtabAllocated.popScope(); d_implementation->popScope(); } @@ -422,8 +439,6 @@ const std::string& SymbolManager::getLastSynthName() const void SymbolManager::reset() { - // reset resets the symbol table even when global declarations are true - d_symtabAllocated.reset(); d_implementation->reset(); } @@ -432,8 +447,8 @@ void SymbolManager::resetAssertions() d_implementation->resetAssertions(); if (!d_globalDeclarations) { - d_symtabAllocated.resetAssertions(); + d_implementation->getSymbolTable().resetAssertions(); } } -} // namespace cvc5 +} // namespace cvc5::parser diff --git a/src/expr/symbol_manager.h b/src/parser/api/cpp/symbol_manager.h similarity index 85% rename from src/expr/symbol_manager.h rename to src/parser/api/cpp/symbol_manager.h index 3fbb3375c..4aa732d71 100644 --- a/src/expr/symbol_manager.h +++ b/src/parser/api/cpp/symbol_manager.h @@ -24,10 +24,14 @@ #include "api/cpp/cvc5.h" #include "cvc5_export.h" -#include "expr/symbol_table.h" namespace cvc5 { +namespace internal::parser { +class SymbolTable; +} + +namespace parser { /** Represents the result of a call to `setExpressionName()`. */ enum class NamingResult { @@ -53,7 +57,32 @@ class CVC5_EXPORT SymbolManager SymbolManager(cvc5::Solver* s); ~SymbolManager(); /** Get the underlying symbol table */ - internal::SymbolTable* getSymbolTable(); + 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 * @@ -175,10 +204,6 @@ class CVC5_EXPORT SymbolManager 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; @@ -189,6 +214,7 @@ class CVC5_EXPORT SymbolManager 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/expr/symbol_table.cpp b/src/parser/symbol_table.cpp similarity index 91% rename from src/expr/symbol_table.cpp rename to src/parser/symbol_table.cpp index b3977f12e..bfb514d85 100644 --- a/src/expr/symbol_table.cpp +++ b/src/parser/symbol_table.cpp @@ -14,7 +14,7 @@ * (implementation). */ -#include "expr/symbol_table.h" +#include "parser/symbol_table.h" #include #include @@ -26,7 +26,7 @@ #include "context/cdhashset.h" #include "context/context.h" -namespace cvc5::internal { +namespace cvc5::internal::parser { using context::CDHashMap; using context::CDHashSet; @@ -63,31 +63,32 @@ using std::vector; * * 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 + * 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 { +class OverloadedTypeTrie +{ public: OverloadedTypeTrie(Context* c, bool allowFunVariants = false) : d_overloaded_symbols( @@ -142,7 +143,8 @@ class OverloadedTypeTrie { // 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 { + class TypeArgTrie + { public: // children of this node std::map d_children; @@ -160,11 +162,11 @@ class OverloadedTypeTrie { */ 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. - */ + * 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; }; @@ -179,13 +181,16 @@ cvc5::Term OverloadedTypeTrie::getOverloadedConstantForType( { std::unordered_map::const_iterator it = d_overload_type_arg_trie.find(name); - if (it != d_overload_type_arg_trie.end()) { + 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()) { + if (its != it->second.d_symbols.end()) + { cvc5::Term expr = its->second; // must be an active symbol - if (isOverloadedFunction(expr)) { + if (isOverloadedFunction(expr)) + { return expr; } } @@ -198,18 +203,23 @@ cvc5::Term OverloadedTypeTrie::getOverloadedFunctionForTypes( { std::unordered_map::const_iterator it = d_overload_type_arg_trie.find(name); - if (it != d_overload_type_arg_trie.end()) { + if (it != d_overload_type_arg_trie.end()) + { const TypeArgTrie* tat = &it->second; - for (unsigned i = 0; i < argTypes.size(); i++) { + 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()) { + if (itc != tat->d_children.end()) + { tat = &itc->second; - } else { + } + else + { Trace("parser-overloading") << "Could not find overloaded function " << name << std::endl; - // no functions match + // no functions match return d_nullTerm; } } @@ -224,7 +234,8 @@ bool OverloadedTypeTrie::bind(const string& name, cvc5::Term obj) { bool retprev = true; - if (!isOverloadedFunction(prev_bound_obj)) { + if (!isOverloadedFunction(prev_bound_obj)) + { // mark previous as overloaded retprev = markOverloaded(name, prev_bound_obj); } @@ -258,7 +269,8 @@ bool OverloadedTypeTrie::markOverloaded(const string& name, cvc5::Term obj) } // add to the trie TypeArgTrie* tat = &d_overload_type_arg_trie[name]; - for (unsigned i = 0; i < argTypes.size(); i++) { + for (unsigned i = 0; i < argTypes.size(); i++) + { tat = &(tat->d_children[argTypes[i]]); } @@ -272,7 +284,7 @@ bool OverloadedTypeTrie::markOverloaded(const string& name, cvc5::Term obj) { 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 + // the same argument types and has the same return type, we reject the // re-declaration here. if (isOverloadedFunction(prev_obj)) { @@ -310,11 +322,11 @@ cvc5::Term OverloadedTypeTrie::getOverloadedFunctionAt( { if (retExpr.isNull()) { - if (!reqUnique) + if (!reqUnique) { return expr; } - else + else { retExpr = expr; } @@ -329,7 +341,8 @@ cvc5::Term OverloadedTypeTrie::getOverloadedFunctionAt( return retExpr; } -class SymbolTable::Implementation { +class SymbolTable::Implementation +{ public: Implementation() : d_context(), @@ -402,17 +415,20 @@ bool SymbolTable::Implementation::bind(const string& name, 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)) { + if (doOverload) + { + if (!bindWithOverloading(name, obj)) + { return false; } } - d_exprMap.insert(name, obj); + d_exprMap.insert(name, obj); return true; } -bool SymbolTable::Implementation::isBound(const string& name) const { +bool SymbolTable::Implementation::isBound(const string& name) const +{ return d_exprMap.find(name) != d_exprMap.end(); } @@ -420,9 +436,12 @@ cvc5::Term SymbolTable::Implementation::lookup(const string& name) const { Assert(isBound(name)); cvc5::Term expr = (*d_exprMap.find(name)).second; - if (isOverloadedFunction(expr)) { + if (isOverloadedFunction(expr)) + { return d_nullTerm; - } else { + } + else + { return expr; } } @@ -436,9 +455,11 @@ void SymbolTable::Implementation::bindType(const string& name, const vector& params, cvc5::Sort t) { - if (TraceIsOn("sort")) { + if (TraceIsOn("sort")) + { Trace("sort") << "bindType(" << name << ", ["; - if (params.size() > 0) { + if (params.size() > 0) + { copy(params.begin(), params.end() - 1, ostream_iterator(Trace("sort"), ", ")); @@ -447,10 +468,11 @@ void SymbolTable::Implementation::bindType(const string& name, Trace("sort") << "], " << t << ")" << endl; } - d_typeMap.insert(name, make_pair(params, t)); + d_typeMap.insert(name, make_pair(params, t)); } -bool SymbolTable::Implementation::isBoundType(const string& name) const { +bool SymbolTable::Implementation::isBoundType(const string& name) const +{ return d_typeMap.find(name) != d_typeMap.end(); } @@ -458,10 +480,12 @@ 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, + 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()); + name.c_str(), + p.first.size()); return p.second; } @@ -470,11 +494,15 @@ cvc5::Sort SymbolTable::Implementation::lookupType( { std::pair, cvc5::Sort> p = (*d_typeMap.find(name)).second; - PrettyCheckArgument(p.first.size() == params.size(), params, + 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) { + name.c_str(), + p.first.size(), + params.size()); + if (p.first.size() == 0) + { PrettyCheckArgument(p.second.isUninterpretedSort(), name.c_str()); return p.second; } @@ -513,13 +541,15 @@ cvc5::Sort SymbolTable::Implementation::lookupType( return instantiation; } -size_t SymbolTable::Implementation::lookupArity(const string& name) { +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() { +void SymbolTable::Implementation::popScope() +{ // should not pop beyond level one if (d_context.getLevel() == 0) { @@ -530,11 +560,13 @@ void SymbolTable::Implementation::popScope() { void SymbolTable::Implementation::pushScope() { d_context.push(); } -size_t SymbolTable::Implementation::getLevel() const { +size_t SymbolTable::Implementation::getLevel() const +{ return d_context.getLevel(); } -void SymbolTable::Implementation::reset() { +void SymbolTable::Implementation::reset() +{ Trace("sym-table") << "SymbolTable: reset" << std::endl; this->SymbolTable::Implementation::~Implementation(); new (this) SymbolTable::Implementation(); @@ -575,7 +607,8 @@ bool SymbolTable::Implementation::bindWithOverloading(const string& name, if (it != d_exprMap.end()) { const cvc5::Term& prev_bound_obj = (*it).second; - if (prev_bound_obj != obj) { + if (prev_bound_obj != obj) + { return d_overload_trie.bind(name, prev_bound_obj, obj); } } @@ -643,7 +676,8 @@ cvc5::Sort SymbolTable::lookupType(const string& name, { return d_implementation->lookupType(name, params); } -size_t SymbolTable::lookupArity(const string& name) { +size_t SymbolTable::lookupArity(const string& name) +{ return d_implementation->lookupArity(name); } void SymbolTable::popScope() { d_implementation->popScope(); } @@ -652,4 +686,4 @@ size_t SymbolTable::getLevel() const { return d_implementation->getLevel(); } void SymbolTable::reset() { d_implementation->reset(); } void SymbolTable::resetAssertions() { d_implementation->resetAssertions(); } -} // namespace cvc5::internal +} // namespace cvc5::internal::parser diff --git a/src/expr/symbol_table.h b/src/parser/symbol_table.h similarity index 97% rename from src/expr/symbol_table.h rename to src/parser/symbol_table.h index bc7628df0..575b8de26 100644 --- a/src/expr/symbol_table.h +++ b/src/parser/symbol_table.h @@ -13,7 +13,7 @@ * Convenience class for scoping variable and type declarations. */ -#include "cvc5_public.h" +#include "cvc5parser_public.h" #ifndef CVC5__SYMBOL_TABLE_H #define CVC5__SYMBOL_TABLE_H @@ -31,9 +31,9 @@ class Sort; class Term; } // namespace cvc5 -namespace cvc5::internal { +namespace cvc5::internal::parser { -class CVC5_EXPORT ScopeException : public Exception +class CVC5_EXPORT ScopeException : public internal::Exception { }; @@ -176,7 +176,7 @@ class CVC5_EXPORT SymbolTable /** 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; @@ -201,6 +201,6 @@ class CVC5_EXPORT SymbolTable std::unique_ptr d_implementation; }; /* class SymbolTable */ -} // namespace cvc5::internal +} // 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 -- 2.30.2