GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/prop/skolem_def_manager.cpp Lines: 70 79 88.6 %
Date: 2021-03-23 Branches: 92 222 41.4 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file skolem_def_manager.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-2020 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 Skolem definition manager
13
 **/
14
15
#include "prop/skolem_def_manager.h"
16
17
#include "expr/attribute.h"
18
19
namespace CVC4 {
20
namespace prop {
21
22
9029
SkolemDefManager::SkolemDefManager(context::Context* context,
23
9029
                                   context::UserContext* userContext)
24
9029
    : d_skDefs(userContext), d_skActive(context)
25
{
26
9029
}
27
28
9026
SkolemDefManager::~SkolemDefManager() {}
29
30
29583
void SkolemDefManager::notifySkolemDefinition(TNode skolem, Node def)
31
{
32
  // Notice that skolem may have kind SKOLEM or BOOLEAN_TERM_VARIABLE
33
59166
  Trace("sk-defs") << "notifySkolemDefinition: " << def << " for " << skolem
34
29583
                   << std::endl;
35
  // in very rare cases, a skolem may be generated twice for terms that are
36
  // equivalent up to purification
37
29583
  if (d_skDefs.find(skolem) == d_skDefs.end())
38
  {
39
29579
    d_skDefs.insert(skolem, def);
40
  }
41
29583
}
42
43
2039
TNode SkolemDefManager::getDefinitionForSkolem(TNode skolem) const
44
{
45
2039
  NodeNodeMap::const_iterator it = d_skDefs.find(skolem);
46
2039
  AlwaysAssert(it != d_skDefs.end()) << "No skolem def for " << skolem;
47
2039
  return it->second;
48
}
49
50
void SkolemDefManager::notifyAsserted(TNode literal,
51
                                      std::vector<TNode>& activatedSkolems)
52
{
53
  std::unordered_set<Node, NodeHashFunction> skolems;
54
  getSkolems(literal, skolems);
55
  for (const Node& k : skolems)
56
  {
57
    if (d_skActive.find(k) != d_skActive.end())
58
    {
59
      // already active
60
      continue;
61
    }
62
    d_skActive.insert(k);
63
    // add to the activated list
64
    activatedSkolems.push_back(k);
65
  }
66
}
67
68
struct HasSkolemTag
69
{
70
};
71
struct HasSkolemComputedTag
72
{
73
};
74
/** Attribute true for nodes with skolems in them */
75
typedef expr::Attribute<HasSkolemTag, bool> HasSkolemAttr;
76
/** Attribute true for nodes where we have computed the above attribute */
77
typedef expr::Attribute<HasSkolemComputedTag, bool> HasSkolemComputedAttr;
78
79
15891
bool SkolemDefManager::hasSkolems(TNode n) const
80
{
81
31782
  std::unordered_set<TNode, TNodeHashFunction> visited;
82
15891
  std::unordered_set<TNode, TNodeHashFunction>::iterator it;
83
31782
  std::vector<TNode> visit;
84
31782
  TNode cur;
85
15891
  visit.push_back(n);
86
117819
  do
87
  {
88
133710
    cur = visit.back();
89
179588
    if (cur.getAttribute(HasSkolemComputedAttr()))
90
    {
91
45878
      visit.pop_back();
92
      // already computed
93
45878
      continue;
94
    }
95
87832
    it = visited.find(cur);
96
87832
    if (it == visited.end())
97
    {
98
49626
      visited.insert(cur);
99
49626
      if (cur.getNumChildren() == 0)
100
      {
101
11420
        visit.pop_back();
102
11420
        bool hasSkolem = false;
103
11420
        if (cur.isVar())
104
        {
105
8034
          hasSkolem = (d_skDefs.find(cur) != d_skDefs.end());
106
        }
107
11420
        cur.setAttribute(HasSkolemAttr(), hasSkolem);
108
11420
        cur.setAttribute(HasSkolemComputedAttr(), true);
109
      }
110
      else
111
      {
112
38206
        visit.insert(visit.end(), cur.begin(), cur.end());
113
      }
114
    }
115
    else
116
    {
117
38206
      visit.pop_back();
118
38206
      bool hasSkolem = false;
119
107963
      for (TNode i : cur)
120
      {
121
75438
        Assert(i.getAttribute(HasSkolemComputedAttr()));
122
75438
        if (i.getAttribute(HasSkolemAttr()))
123
        {
124
5681
          hasSkolem = true;
125
5681
          break;
126
        }
127
      }
128
38206
      cur.setAttribute(HasSkolemAttr(), hasSkolem);
129
38206
      cur.setAttribute(HasSkolemComputedAttr(), true);
130
    }
131
133710
  } while (!visit.empty());
132
15891
  Assert(n.getAttribute(HasSkolemComputedAttr()));
133
31782
  return n.getAttribute(HasSkolemAttr());
134
}
135
136
2694
void SkolemDefManager::getSkolems(
137
    TNode n, std::unordered_set<Node, NodeHashFunction>& skolems) const
138
{
139
5388
  std::unordered_set<TNode, TNodeHashFunction> visited;
140
2694
  std::unordered_set<TNode, TNodeHashFunction>::iterator it;
141
5388
  std::vector<TNode> visit;
142
5388
  TNode cur;
143
2694
  visit.push_back(n);
144
13197
  do
145
  {
146
15891
    cur = visit.back();
147
15891
    visit.pop_back();
148
15891
    if (!hasSkolems(cur))
149
    {
150
      // does not have skolems, continue
151
6461
      continue;
152
    }
153
9430
    it = visited.find(cur);
154
9430
    if (it == visited.end())
155
    {
156
7898
      visited.insert(cur);
157
7898
      if (cur.isVar())
158
      {
159
2039
        if (d_skDefs.find(cur) != d_skDefs.end())
160
        {
161
2039
          skolems.insert(cur);
162
        }
163
      }
164
      else
165
      {
166
5859
        visit.insert(visit.end(), cur.begin(), cur.end());
167
      }
168
    }
169
15891
  } while (!visit.empty());
170
2694
}
171
172
}  // namespace prop
173
26685
}  // namespace CVC4