From: Andrew Reynolds Date: Mon, 3 Aug 2020 18:42:17 +0000 (-0500) Subject: Split expression names from SmtEngine (#4832) X-Git-Tag: cvc5-1.0.0~3054 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ecc9fca138bcaee5a96e160e59a67e75e9247cab;p=cvc5.git Split expression names from SmtEngine (#4832) Towards splitting SmtEngine / deleting SmtEnginePrivate. --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 61261afe4..17c4a26f5 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -230,6 +230,8 @@ libcvc4_add_sources( smt/dump.h smt/dump_manager.cpp smt/dump_manager.h + smt/expr_names.cpp + smt/expr_names.h smt/listeners.cpp smt/listeners.h smt/logic_exception.h diff --git a/src/smt/expr_names.cpp b/src/smt/expr_names.cpp new file mode 100644 index 000000000..78c0346e4 --- /dev/null +++ b/src/smt/expr_names.cpp @@ -0,0 +1,39 @@ +/********************* */ +/*! \file expr_names.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 Utility for maintaining expression names. + **/ + +#include "smt/expr_names.h" + +namespace CVC4 { +namespace smt { + +ExprNames::ExprNames(context::UserContext* u) + : d_exprNames(u) +{ +} + +void ExprNames::setExpressionName(const Node& e, const std::string& name) { + d_exprNames[e] = name; +} + +bool ExprNames::getExpressionName(const Node& e, std::string& name) const { + auto it = d_exprNames.find(e); + if(it!=d_exprNames.end()) { + name = (*it).second; + return true; + } + return false; +} + +} // namespace smt +} // namespace CVC4 diff --git a/src/smt/expr_names.h b/src/smt/expr_names.h new file mode 100644 index 000000000..b4bb9993e --- /dev/null +++ b/src/smt/expr_names.h @@ -0,0 +1,59 @@ +/********************* */ +/*! \file expr_names.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 Utility for maintaining expression names. + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__SMT__EXPR_NAMES_H +#define CVC4__SMT__EXPR_NAMES_H + +#include + +#include "context/cdhashmap.h" +#include "expr/node.h" + +namespace CVC4 { +namespace smt { + +/** + * This utility is responsible for maintaining names for expressions. + */ +class ExprNames +{ + public: + ExprNames(context::UserContext* u); + /** + * Get expression name. + * + * Return true if given expression has a name in the current context. + * If it returns true, the name of expression 'e' is stored in 'name'. + */ + bool getExpressionName(const Node& e, std::string& name) const; + + /** + * Set name of given expression 'e' to 'name'. + * + * This information is user-context-dependent. + * If 'e' already has a name, it is overwritten. + */ + void setExpressionName(const Node& e, const std::string& name); + + private: + /** mapping from expressions to name */ + context::CDHashMap< Node, std::string, NodeHashFunction > d_exprNames; +}; + +} // namespace smt +} // namespace CVC4 + +#endif diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index f114dba7c..6d1e7ffbc 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -82,6 +82,7 @@ #include "prop/prop_engine.h" #include "smt/abduction_solver.h" #include "smt/abstract_values.h" +#include "smt/expr_names.h" #include "smt/command.h" #include "smt/defined_function.h" #include "smt/dump_manager.h" @@ -176,10 +177,6 @@ class SmtEnginePrivate /** Process assertions module */ ProcessAssertions d_processor; - //------------------------------- expression names - /** mapping from expressions to name */ - context::CDHashMap< Node, std::string, NodeHashFunction > d_exprNames; - //------------------------------- end expression names public: IteSkolemMap& getIteSkolemMap() { return d_assertions.getIteSkolemMap(); } @@ -214,7 +211,6 @@ class SmtEnginePrivate d_assertions(), d_assertionsProcessed(smt.getUserContext(), false), d_processor(smt, *smt.getResourceManager()), - d_exprNames(smt.getUserContext()), d_iteRemover(smt.getUserContext()), d_sygusConjectureStale(smt.getUserContext(), true) { @@ -299,24 +295,6 @@ class SmtEnginePrivate Assert(d_assertions.size() == 0); return applySubstitutions(n).toExpr(); } - - //------------------------------- expression names - // implements setExpressionName, as described in smt_engine.h - void setExpressionName(Expr e, std::string name) { - d_exprNames[Node::fromExpr(e)] = name; - } - - // implements getExpressionName, as described in smt_engine.h - bool getExpressionName(Expr e, std::string& name) const { - context::CDHashMap< Node, std::string, NodeHashFunction >::const_iterator it = d_exprNames.find(e); - if(it!=d_exprNames.end()) { - name = (*it).second; - return true; - }else{ - return false; - } - } - //------------------------------- end expression names };/* class SmtEnginePrivate */ }/* namespace CVC4::smt */ @@ -328,6 +306,7 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr) d_exprManager(em), d_nodeManager(d_exprManager->getNodeManager()), d_absValues(new AbstractValues(d_nodeManager)), + d_exprNames(new ExprNames(d_userContext.get())), d_dumpm(new DumpManager(d_userContext.get())), d_routListener(new ResourceOutListener(*this)), d_snmListener(new SmtNodeManagerListener(*d_dumpm.get())), @@ -578,6 +557,7 @@ SmtEngine::~SmtEngine() #endif d_absValues.reset(nullptr); + d_exprNames.reset(nullptr); d_dumpm.reset(nullptr); d_theoryEngine.reset(nullptr); @@ -3219,13 +3199,13 @@ CVC4::SExpr SmtEngine::getOption(const std::string& key) const return SExpr::parseAtom(d_options.getOption(key)); } -bool SmtEngine::getExpressionName(Expr e, std::string& name) const { - return d_private->getExpressionName(e, name); +bool SmtEngine::getExpressionName(const Node& e, std::string& name) const { + return d_exprNames->getExpressionName(e, name); } -void SmtEngine::setExpressionName(Expr e, const std::string& name) { +void SmtEngine::setExpressionName(const Node& e, const std::string& name) { Trace("smt-debug") << "Set expression name " << e << " to " << name << std::endl; - d_private->setExpressionName(e,name); + d_exprNames->setExpressionName(e,name); } Options& SmtEngine::getOptions() { return d_options; } diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 99b993e7b..f51b6759b 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -93,6 +93,7 @@ namespace prop { namespace smt { /** Utilities */ class AbstractValues; +class ExprNames; class DumpManager; class ResourceOutListener; class SmtNodeManagerListener; @@ -858,7 +859,7 @@ class CVC4_PUBLIC SmtEngine * Return true if given expressoion has a name in the current context. * If it returns true, the name of expression 'e' is stored in 'name'. */ - bool getExpressionName(Expr e, std::string& name) const; + bool getExpressionName(const Node& e, std::string& name) const; /** * Set name of given expression 'e' to 'name'. @@ -866,7 +867,7 @@ class CVC4_PUBLIC SmtEngine * This information is user-context-dependent. * If 'e' already has a name, it is overwritten. */ - void setExpressionName(Expr e, const std::string& name); + void setExpressionName(const Node& e, const std::string& name); /** Get the options object (const and non-const versions) */ Options& getOptions(); @@ -1121,6 +1122,8 @@ class CVC4_PUBLIC SmtEngine NodeManager* d_nodeManager; /** Abstract values */ std::unique_ptr d_absValues; + /** Expression names */ + std::unique_ptr d_exprNames; /** The dump manager */ std::unique_ptr d_dumpm; /** Resource out listener */