GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/sets/skolem_cache.cpp Lines: 19 19 100.0 %
Date: 2021-03-22 Branches: 40 82 48.8 %

Line Exec Source
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-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.\endverbatim
11
 **
12
 ** \brief Implementation of a cache of skolems for theory of sets.
13
 **/
14
15
#include "theory/sets/skolem_cache.h"
16
17
#include "theory/rewriter.h"
18
19
using namespace CVC4::kind;
20
21
namespace CVC4 {
22
namespace theory {
23
namespace sets {
24
25
8995
SkolemCache::SkolemCache() {}
26
27
5750
Node SkolemCache::mkTypedSkolemCached(
28
    TypeNode tn, Node a, Node b, SkolemId id, const char* c)
29
{
30
5750
  a = a.isNull() ? a : Rewriter::rewrite(a);
31
5750
  b = b.isNull() ? b : Rewriter::rewrite(b);
32
33
5750
  std::map<SkolemId, Node>::iterator it = d_skolemCache[a][b].find(id);
34
5750
  if (it == d_skolemCache[a][b].end())
35
  {
36
10120
    Node sk = mkTypedSkolem(tn, c);
37
5060
    d_skolemCache[a][b][id] = sk;
38
5060
    return sk;
39
  }
40
690
  return it->second;
41
}
42
3863
Node SkolemCache::mkTypedSkolemCached(TypeNode tn,
43
                                      Node a,
44
                                      SkolemId id,
45
                                      const char* c)
46
{
47
3863
  return mkTypedSkolemCached(tn, a, Node::null(), id, c);
48
}
49
50
5060
Node SkolemCache::mkTypedSkolem(TypeNode tn, const char* c)
51
{
52
5060
  Node n = NodeManager::currentNM()->mkSkolem(c, tn, "sets skolem");
53
5060
  d_allSkolems.insert(n);
54
5060
  return n;
55
}
56
57
89552
bool SkolemCache::isSkolem(Node n) const
58
{
59
89552
  return d_allSkolems.find(n) != d_allSkolems.end();
60
}
61
62
}  // namespace sets
63
}  // namespace theory
64
26676
}  // namespace CVC4