src/theory/sets/skolem_cache.cpp

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Andrew Reynolds, Aina Niemetz
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   7  * Copyright (c) 2009-2021 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.
  11  * ****************************************************************************
  12  *
  13  * Implementation of a cache of skolems for theory of sets.
  14  */
  15
  16 #include "theory/sets/skolem_cache.h"
  17
  18 #include "expr/skolem_manager.h"
  19 #include "theory/rewriter.h"
  20
  21 using namespace cvc5::kind;
  22
  23 namespace cvc5 {
  24 namespace theory {
  25 namespace sets {
  26
  27 SkolemCache::SkolemCache(Rewriter* rr) : d_rewriter(rr) {}
  28
  29 Node SkolemCache::mkTypedSkolemCached(
  30     TypeNode tn, Node a, Node b, SkolemId id, const char* c)
  31 {
  32   if (d_rewriter != nullptr)
  33   {
  34     a = a.isNull() ? a : d_rewriter->rewrite(a);
  35     b = b.isNull() ? b : d_rewriter->rewrite(b);
  36   }
  37   std::map<SkolemId, Node>::iterator it = d_skolemCache[a][b].find(id);
  38   if (it == d_skolemCache[a][b].end())
  39   {
  40     SkolemManager* sm = NodeManager::currentNM()->getSkolemManager();
  41     Node sk;
  42     if (id == SkolemId::SK_PURIFY)
  43     {
  44       Assert(a.getType() == tn);
  45       sk = sm->mkPurifySkolem(a, c);
  46     }
  47     else
  48     {
  49       sk = sm->mkDummySkolem(c, tn, "sets skolem");
  50     }
  51     d_skolemCache[a][b][id] = sk;
  52     d_allSkolems.insert(sk);
  53     return sk;
  54   }
  55   return it->second;
  56 }
  57 Node SkolemCache::mkTypedSkolemCached(TypeNode tn,
  58                                       Node a,
  59                                       SkolemId id,
  60                                       const char* c)
  61 {
  62   return mkTypedSkolemCached(tn, a, Node::null(), id, c);
  63 }
  64
  65 Node SkolemCache::mkTypedSkolem(TypeNode tn, const char* c)
  66 {
  67   SkolemManager* sm = NodeManager::currentNM()->getSkolemManager();
  68   Node n = sm->mkDummySkolem(c, tn, "sets skolem");
  69   d_allSkolems.insert(n);
  70   return n;
  71 }
  72
  73 bool SkolemCache::isSkolem(Node n) const
  74 {
  75   return d_allSkolems.find(n) != d_allSkolems.end();
  76 }
  77
  78 }  // namespace sets
  79 }  // namespace theory
  80 }  // namespace cvc5