From 80930ce4f6d21b417028a5ec207ddfbd7d85e66d Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 11 Nov 2020 12:56:03 -0600 Subject: Move symbol manager to src/expr/ (#5420) This is required since symbol manager will use context dependent data structures (in its cpp). This is required since classes in src/parser/ are not allowed to include private headers. --- src/parser/CMakeLists.txt | 2 - src/parser/parser.h | 2 +- src/parser/parser_builder.h | 6 +-- src/parser/symbol_manager.cpp | 77 ------------------------------- src/parser/symbol_manager.h | 102 ------------------------------------------ 5 files changed, 4 insertions(+), 185 deletions(-) delete mode 100644 src/parser/symbol_manager.cpp delete mode 100644 src/parser/symbol_manager.h (limited to 'src/parser') diff --git a/src/parser/CMakeLists.txt b/src/parser/CMakeLists.txt index 7b55c0915..8e69da34b 100644 --- a/src/parser/CMakeLists.txt +++ b/src/parser/CMakeLists.txt @@ -55,8 +55,6 @@ set(libcvc4parser_src_files smt2/smt2_input.h smt2/sygus_input.cpp smt2/sygus_input.h - symbol_manager.cpp - symbol_manager.h tptp/TptpLexer.c tptp/TptpParser.c tptp/tptp.cpp diff --git a/src/parser/parser.h b/src/parser/parser.h index 405935165..c762fc117 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -26,11 +26,11 @@ #include "api/cvc4cpp.h" #include "expr/kind.h" +#include "expr/symbol_manager.h" #include "expr/symbol_table.h" #include "parser/input.h" #include "parser/parse_op.h" #include "parser/parser_exception.h" -#include "parser/symbol_manager.h" #include "util/unsafe_interrupt_exception.h" namespace CVC4 { diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h index 9d62c12a3..bf205b13a 100644 --- a/src/parser/parser_builder.h +++ b/src/parser/parser_builder.h @@ -26,16 +26,16 @@ namespace CVC4 { -class Options; - namespace api { 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_manager.cpp b/src/parser/symbol_manager.cpp deleted file mode 100644 index 32e17aea8..000000000 --- a/src/parser/symbol_manager.cpp +++ /dev/null @@ -1,77 +0,0 @@ -/********************* */ -/*! \file symbol_manager.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 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.\endverbatim - ** - ** \brief The symbol manager - **/ - -#include "parser/symbol_manager.h" - -namespace CVC4 { -namespace parser { - -SymbolManager::SymbolManager(api::Solver* s) : d_solver(s) {} - -SymbolTable* SymbolManager::getSymbolTable() { return &d_symtabAllocated; } - -bool SymbolManager::setExpressionName(api::Term t, - const std::string& name, - bool isAssertion) -{ - if (d_names.find(t) != d_names.end()) - { - // already named assertion - return false; - } - if (isAssertion) - { - d_namedAsserts.insert(t); - } - d_names[t] = name; - return true; -} - -bool SymbolManager::getExpressionName(api::Term t, - std::string& name, - bool isAssertion) const -{ - std::map::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::getExpressionNames(const std::vector& ts, - std::vector& names, - bool areAssertions) const -{ - for (const api::Term& t : ts) - { - std::string name; - if (getExpressionName(t, name, areAssertions)) - { - names.push_back(name); - } - } -} - -} // namespace parser -} // namespace CVC4 diff --git a/src/parser/symbol_manager.h b/src/parser/symbol_manager.h deleted file mode 100644 index 20b0c80e4..000000000 --- a/src/parser/symbol_manager.h +++ /dev/null @@ -1,102 +0,0 @@ -/********************* */ -/*! \file symbol_manager.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 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.\endverbatim - ** - ** \brief The symbol manager - **/ - -#include "cvc4parser_public.h" - -#ifndef CVC4__PARSER__SYMBOL_MANAGER_H -#define CVC4__PARSER__SYMBOL_MANAGER_H - -#include -#include -#include - -#include "api/cvc4cpp.h" -#include "expr/symbol_table.h" - -namespace CVC4 { -namespace parser { - -/** - * 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. - */ -class CVC4_PUBLIC SymbolManager -{ - public: - SymbolManager(api::Solver* s); - ~SymbolManager() {} - /** Get the underlying symbol table */ - 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. - */ - bool setExpressionName(api::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(api::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; - //---------------------------- end named expressions - - private: - /** The API Solver object. */ - api::Solver* d_solver; - /** - * The declaration scope that is "owned" by this symbol manager. - */ - SymbolTable d_symtabAllocated; - /** Map terms to names */ - std::map d_names; - /** The set of terms with assertion names */ - std::set d_namedAsserts; -}; - -} // namespace parser -} // namespace CVC4 - -#endif /* CVC4__PARSER__SYMBOL_MANAGER_H */ -- cgit v1.2.3