diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-11-19 06:42:04 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-11-19 06:42:04 -0600 |
commit | b0130a1e032c201fab3c4b19f25871428b761967 (patch) | |
tree | f18039906a287a4d55345b1c4bd0ac86cf5232c5 /src/smt/expr_names.cpp | |
parent | 2901ee18f824d1f9e4338ef2853da0ab4ccbff0e (diff) |
Use symbol manager for unsat cores (#5468)
This PR uses the symbol manager for handling names for unsat cores.
This replaces interfaces in SmtEngine for managing expression names. It removes the SetExpressionName command.
Diffstat (limited to 'src/smt/expr_names.cpp')
-rw-r--r-- | src/smt/expr_names.cpp | 39 |
1 files changed, 0 insertions, 39 deletions
diff --git a/src/smt/expr_names.cpp b/src/smt/expr_names.cpp deleted file mode 100644 index ccced2cac..000000000 --- a/src/smt/expr_names.cpp +++ /dev/null @@ -1,39 +0,0 @@ -/********************* */ -/*! \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 |