diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-09-14 14:57:35 -0500 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-09-14 12:57:35 -0700 |
commit | c2111c86973b8a80e20a3fdf3cbd0b2ff0dc7010 (patch) | |
tree | 2de4addf5a0a769f27240f28aeb576a97d5ef625 /src/theory/strings/skolem_cache.cpp | |
parent | 4a9a0dcb8b06e3fc917b642426140b044a64facd (diff) |
Add Skolem cache for strings, refactor length registration (#2457)
This PR is in preparation for doing more aggressive caching of skolems (for example, in the strings preprocessor).
It refactors sendLengthLemma -> registerLength, which unifies how length lemmas for skolems and other string terms are handled.
Diffstat (limited to 'src/theory/strings/skolem_cache.cpp')
-rw-r--r-- | src/theory/strings/skolem_cache.cpp | 50 |
1 files changed, 50 insertions, 0 deletions
diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp new file mode 100644 index 000000000..db673dafe --- /dev/null +++ b/src/theory/strings/skolem_cache.cpp @@ -0,0 +1,50 @@ +/********************* */ +/*! \file skolem_cache.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 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 Implementation of a cache of skolems for theory of strings. + **/ + +#include "theory/strings/skolem_cache.h" + +namespace CVC4 { +namespace theory { +namespace strings { + +SkolemCache::SkolemCache() {} + +Node SkolemCache::mkSkolemCached(Node a, Node b, SkolemId id, const char* c) +{ + std::map<SkolemId, Node>::iterator it = d_skolemCache[a][b].find(id); + if (it == d_skolemCache[a][b].end()) + { + Node sk = mkSkolem(c); + d_skolemCache[a][b][id] = sk; + return sk; + } + return it->second; +} + +Node SkolemCache::mkSkolem(const char* c) +{ + NodeManager* nm = NodeManager::currentNM(); + Node n = nm->mkSkolem(c, nm->stringType(), "string skolem"); + d_allSkolems.insert(n); + return n; +} + +bool SkolemCache::isSkolem(Node n) const +{ + return d_allSkolems.find(n) != d_allSkolems.end(); +} + +} // namespace strings +} // namespace theory +} // namespace CVC4 |