diff options
Diffstat (limited to 'src/expr')
| -rw-r--r-- | src/expr/CMakeLists.txt | 2 | ||||
| -rw-r--r-- | src/expr/symbol_manager.cpp | 75 | ||||
| -rw-r--r-- | src/expr/symbol_manager.h | 103 |
3 files changed, 180 insertions, 0 deletions
diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index d7af52fec..fb3df5327 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -76,6 +76,8 @@ libcvc4_add_sources( proof_step_buffer.h skolem_manager.cpp skolem_manager.h + symbol_manager.cpp + symbol_manager.h symbol_table.cpp symbol_table.h tconv_seq_proof_generator.cpp diff --git a/src/expr/symbol_manager.cpp b/src/expr/symbol_manager.cpp new file mode 100644 index 000000000..ac3b5d211 --- /dev/null +++ b/src/expr/symbol_manager.cpp @@ -0,0 +1,75 @@ +/********************* */ +/*! \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 "expr/symbol_manager.h" + +namespace CVC4 { + +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<api::Term, std::string>::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<api::Term>& ts, + std::vector<std::string>& names, + bool areAssertions) const +{ + for (const api::Term& t : ts) + { + std::string name; + if (getExpressionName(t, name, areAssertions)) + { + names.push_back(name); + } + } +} + +} // namespace CVC4 diff --git a/src/expr/symbol_manager.h b/src/expr/symbol_manager.h new file mode 100644 index 000000000..4890ed994 --- /dev/null +++ b/src/expr/symbol_manager.h @@ -0,0 +1,103 @@ +/********************* */ +/*! \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 "cvc4_public.h" + +#ifndef CVC4__EXPR__SYMBOL_MANAGER_H +#define CVC4__EXPR__SYMBOL_MANAGER_H + +#include <map> +#include <set> +#include <string> + +#include "api/cvc4cpp.h" +#include "expr/symbol_table.h" + +namespace CVC4 { + +/** + * 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 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<api::Term>& ts, + std::vector<std::string>& 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<api::Term, std::string> d_names; + /** The set of terms with assertion names */ + std::set<api::Term> d_namedAsserts; +}; + +} // namespace CVC4 + +#endif /* CVC4__EXPR__SYMBOL_MANAGER_H */ |