GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/sets/term_registry.cpp Lines: 61 76 80.3 %
Date: 2021-03-23 Branches: 117 264 44.3 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file term_registry.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Mudathir Mohamed, Andres Noetzli
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 sets term registry object
13
 **/
14
15
#include "theory/sets/term_registry.h"
16
17
#include "expr/emptyset.h"
18
19
using namespace std;
20
using namespace CVC4::kind;
21
22
namespace CVC4 {
23
namespace theory {
24
namespace sets {
25
26
8997
TermRegistry::TermRegistry(SolverState& state,
27
                           InferenceManager& im,
28
8997
                           SkolemCache& skc)
29
    : d_im(im),
30
      d_skCache(skc),
31
8997
      d_proxy(state.getUserContext()),
32
17994
      d_proxy_to_term(state.getUserContext())
33
{
34
8997
}
35
36
19298
Node TermRegistry::getProxy(Node n)
37
{
38
19298
  Kind nk = n.getKind();
39
19298
  if (nk != EMPTYSET && nk != SINGLETON && nk != INTERSECTION && nk != SETMINUS
40
3241
      && nk != UNION && nk != UNIVERSE_SET)
41
  {
42
1060
    return n;
43
  }
44
18238
  NodeMap::const_iterator it = d_proxy.find(n);
45
18238
  if (it != d_proxy.end())
46
  {
47
14375
    return (*it).second;
48
  }
49
3863
  NodeManager* nm = NodeManager::currentNM();
50
3863
  Node k = d_skCache.mkTypedSkolemCached(
51
7726
      n.getType(), n, SkolemCache::SK_PURIFY, "sp");
52
3863
  d_proxy[n] = k;
53
3863
  d_proxy_to_term[k] = n;
54
7726
  Node eq = k.eqNode(n);
55
3863
  Trace("sets-lemma") << "Sets::Lemma : " << eq << " by proxy" << std::endl;
56
3863
  d_im.lemma(eq, InferenceId::SETS_PROXY);
57
3863
  if (nk == SINGLETON)
58
  {
59
3916
    Node slem = nm->mkNode(MEMBER, n[0], k);
60
3916
    Trace("sets-lemma") << "Sets::Lemma : " << slem << " by singleton"
61
1958
                        << std::endl;
62
1958
    d_im.lemma(slem, InferenceId::SETS_PROXY_SINGLETON);
63
  }
64
3863
  return k;
65
}
66
67
8000
Node TermRegistry::getEmptySet(TypeNode tn)
68
{
69
8000
  std::map<TypeNode, Node>::iterator it = d_emptyset.find(tn);
70
8000
  if (it != d_emptyset.end())
71
  {
72
7900
    return it->second;
73
  }
74
200
  Node n = NodeManager::currentNM()->mkConst(EmptySet(tn));
75
100
  d_emptyset[tn] = n;
76
100
  return n;
77
}
78
79
2751
Node TermRegistry::getUnivSet(TypeNode tn)
80
{
81
2751
  std::map<TypeNode, Node>::iterator it = d_univset.find(tn);
82
2751
  if (it != d_univset.end())
83
  {
84
2613
    return it->second;
85
  }
86
138
  NodeManager* nm = NodeManager::currentNM();
87
276
  Node n = nm->mkNullaryOperator(tn, UNIVERSE_SET);
88
152
  for (it = d_univset.begin(); it != d_univset.end(); ++it)
89
  {
90
28
    Node n1;
91
28
    Node n2;
92
14
    if (tn.isSubtypeOf(it->first))
93
    {
94
      n1 = n;
95
      n2 = it->second;
96
    }
97
14
    else if (it->first.isSubtypeOf(tn))
98
    {
99
      n1 = it->second;
100
      n2 = n;
101
    }
102
14
    if (!n1.isNull())
103
    {
104
      Node ulem = nm->mkNode(SUBSET, n1, n2);
105
      Trace("sets-lemma") << "Sets::Lemma : " << ulem << " by univ-type"
106
                          << std::endl;
107
      d_im.lemma(ulem, InferenceId::SETS_UNIV_TYPE);
108
    }
109
  }
110
138
  d_univset[tn] = n;
111
138
  return n;
112
}
113
114
Node TermRegistry::getTypeConstraintSkolem(Node n, TypeNode tn)
115
{
116
  std::map<TypeNode, Node>::iterator it = d_tc_skolem[n].find(tn);
117
  if (it == d_tc_skolem[n].end())
118
  {
119
    Node k = NodeManager::currentNM()->mkSkolem("tc_k", tn);
120
    d_tc_skolem[n][tn] = k;
121
    return k;
122
  }
123
  return it->second;
124
}
125
126
4236
void TermRegistry::debugPrintSet(Node s, const char* c) const
127
{
128
4236
  if (s.getNumChildren() == 0)
129
  {
130
2960
    NodeMap::const_iterator it = d_proxy_to_term.find(s);
131
2960
    if (it != d_proxy_to_term.end())
132
    {
133
823
      debugPrintSet((*it).second, c);
134
    }
135
    else
136
    {
137
2137
      Trace(c) << s;
138
    }
139
  }
140
  else
141
  {
142
1276
    Trace(c) << "(" << s.getOperator();
143
3825
    for (const Node& sc : s)
144
    {
145
2549
      Trace(c) << " ";
146
2549
      debugPrintSet(sc, c);
147
    }
148
1276
    Trace(c) << ")";
149
  }
150
4236
}
151
152
}  // namespace sets
153
}  // namespace theory
154
26685
}  // namespace CVC4