src/theory/strings/skolem_cache.cpp

   1 /*********************                                                        */
   2 /*! \file skolem_cache.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory) and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief Implementation of a cache of skolems for theory of strings.
  13  **/
  14
  15 #include "theory/strings/skolem_cache.h"
  16
  17 #include "theory/rewriter.h"
  18
  19 namespace CVC4 {
  20 namespace theory {
  21 namespace strings {
  22
  23 SkolemCache::SkolemCache() {}
  24
  25 Node SkolemCache::mkSkolemCached(Node a, Node b, SkolemId id, const char* c)
  26 {
  27   a = a.isNull() ? a : Rewriter::rewrite(a);
  28   b = b.isNull() ? b : Rewriter::rewrite(b);
  29   std::map<SkolemId, Node>::iterator it = d_skolemCache[a][b].find(id);
  30   if (it == d_skolemCache[a][b].end())
  31   {
  32     Node sk = mkSkolem(c);
  33     d_skolemCache[a][b][id] = sk;
  34     return sk;
  35   }
  36   return it->second;
  37 }
  38
  39 Node SkolemCache::mkSkolemCached(Node a, SkolemId id, const char* c)
  40 {
  41   return mkSkolemCached(a, Node::null(), id, c);
  42 }
  43
  44 Node SkolemCache::mkSkolem(const char* c)
  45 {
  46   NodeManager* nm = NodeManager::currentNM();
  47   Node n = nm->mkSkolem(c, nm->stringType(), "string skolem");
  48   d_allSkolems.insert(n);
  49   return n;
  50 }
  51
  52 bool SkolemCache::isSkolem(Node n) const
  53 {
  54   return d_allSkolems.find(n) != d_allSkolems.end();
  55 }
  56
  57 }  // namespace strings
  58 }  // namespace theory
  59 }  // namespace CVC4