GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/relevance_manager.cpp Lines: 102 142 71.8 %
Date: 2021-03-22 Branches: 142 506 28.1 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file relevance_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-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 relevance manager.
13
 **/
14
15
#include "theory/relevance_manager.h"
16
17
#include <sstream>
18
19
using namespace CVC4::kind;
20
21
namespace CVC4 {
22
namespace theory {
23
24
10
RelevanceManager::RelevanceManager(context::UserContext* userContext,
25
10
                                   Valuation val)
26
10
    : d_val(val), d_input(userContext), d_computed(false), d_success(false)
27
{
28
10
}
29
30
10
void RelevanceManager::notifyPreprocessedAssertions(
31
    const std::vector<Node>& assertions)
32
{
33
  // add to input list, which is user-context dependent
34
20
  std::vector<Node> toProcess;
35
40
  for (const Node& a : assertions)
36
  {
37
30
    if (a.getKind() == AND)
38
    {
39
      // split top-level AND
40
22
      for (const Node& ac : a)
41
      {
42
16
        toProcess.push_back(ac);
43
      }
44
    }
45
    else
46
    {
47
24
      d_input.push_back(a);
48
    }
49
  }
50
10
  addAssertionsInternal(toProcess);
51
10
}
52
53
void RelevanceManager::notifyPreprocessedAssertion(Node n)
54
{
55
  std::vector<Node> toProcess;
56
  toProcess.push_back(n);
57
  addAssertionsInternal(toProcess);
58
}
59
60
10
void RelevanceManager::addAssertionsInternal(std::vector<Node>& toProcess)
61
{
62
10
  size_t i = 0;
63
42
  while (i < toProcess.size())
64
  {
65
32
    Node a = toProcess[i];
66
16
    if (a.getKind() == AND)
67
    {
68
      // split AND
69
      for (const Node& ac : a)
70
      {
71
        toProcess.push_back(ac);
72
      }
73
    }
74
    else
75
    {
76
      // note that a could be a literal, in which case we could add it to
77
      // an "always relevant" set here.
78
16
      d_input.push_back(a);
79
    }
80
16
    i++;
81
  }
82
10
}
83
84
54
void RelevanceManager::resetRound()
85
{
86
54
  d_computed = false;
87
54
  d_rset.clear();
88
54
}
89
90
44
void RelevanceManager::computeRelevance()
91
{
92
44
  d_computed = true;
93
44
  Trace("rel-manager") << "RelevanceManager::computeRelevance..." << std::endl;
94
88
  std::unordered_map<TNode, int, TNodeHashFunction> cache;
95
248
  for (const Node& node: d_input)
96
  {
97
408
    TNode n = node;
98
204
    int val = justify(n, cache);
99
204
    if (val != 1)
100
    {
101
      std::stringstream serr;
102
      serr << "RelevanceManager::computeRelevance: WARNING: failed to justify "
103
           << n;
104
      Trace("rel-manager") << serr.str() << std::endl;
105
      Assert(false) << serr.str();
106
      d_success = false;
107
      return;
108
    }
109
  }
110
44
  Trace("rel-manager") << "...success, size = " << d_rset.size() << std::endl;
111
44
  d_success = true;
112
}
113
114
486
bool RelevanceManager::isBooleanConnective(TNode cur)
115
{
116
486
  Kind k = cur.getKind();
117
224
  return k == NOT || k == IMPLIES || k == AND || k == OR || k == ITE || k == XOR
118
689
         || (k == EQUAL && cur[0].getType().isBoolean());
119
}
120
121
145
bool RelevanceManager::updateJustifyLastChild(
122
    TNode cur,
123
    std::vector<int>& childrenJustify,
124
    std::unordered_map<TNode, int, TNodeHashFunction>& cache)
125
{
126
  // This method is run when we are informed that child index of cur
127
  // has justify status lastChildJustify. We return true if we would like to
128
  // compute the next child, in this case we push the status of the current
129
  // child to childrenJustify.
130
145
  size_t nchildren = cur.getNumChildren();
131
145
  Assert(isBooleanConnective(cur));
132
145
  size_t index = childrenJustify.size();
133
145
  Assert(index < nchildren);
134
145
  Assert(cache.find(cur[index]) != cache.end());
135
145
  Kind k = cur.getKind();
136
  // Lookup the last child's value in the overall cache, we may choose to
137
  // add this to childrenJustify if we return true.
138
145
  int lastChildJustify = cache[cur[index]];
139
145
  if (k == NOT)
140
  {
141
131
    cache[cur] = -lastChildJustify;
142
  }
143
14
  else if (k == IMPLIES || k == AND || k == OR)
144
  {
145
    if (lastChildJustify != 0)
146
    {
147
      // See if we short circuited? The value for short circuiting is false if
148
      // we are AND or the first child of IMPLIES.
149
      if (lastChildJustify
150
          == ((k == AND || (k == IMPLIES && index == 0)) ? -1 : 1))
151
      {
152
        cache[cur] = k == AND ? -1 : 1;
153
        return false;
154
      }
155
    }
156
    if (index + 1 == nchildren)
157
    {
158
      // finished all children, compute the overall value
159
      int ret = k == AND ? 1 : -1;
160
      for (int cv : childrenJustify)
161
      {
162
        if (cv == 0)
163
        {
164
          ret = 0;
165
          break;
166
        }
167
      }
168
      cache[cur] = ret;
169
    }
170
    else
171
    {
172
      // continue
173
      childrenJustify.push_back(lastChildJustify);
174
      return true;
175
    }
176
  }
177
14
  else if (lastChildJustify == 0)
178
  {
179
    // all other cases, an unknown child implies we are unknown
180
    cache[cur] = 0;
181
  }
182
14
  else if (k == ITE)
183
  {
184
14
    if (index == 0)
185
    {
186
7
      Assert(lastChildJustify != 0);
187
      // continue with branch
188
7
      childrenJustify.push_back(lastChildJustify);
189
7
      if (lastChildJustify == -1)
190
      {
191
        // also mark first branch as don't care
192
7
        childrenJustify.push_back(0);
193
      }
194
7
      return true;
195
    }
196
    else
197
    {
198
      // should be in proper branch
199
7
      Assert(childrenJustify[0] == (index == 1 ? 1 : -1));
200
      // we are the value of the branch
201
7
      cache[cur] = lastChildJustify;
202
    }
203
  }
204
  else
205
  {
206
    Assert(k == XOR || k == EQUAL);
207
    Assert(nchildren == 2);
208
    Assert(lastChildJustify != 0);
209
    if (index == 0)
210
    {
211
      // must compute the other child
212
      childrenJustify.push_back(lastChildJustify);
213
      return true;
214
    }
215
    else
216
    {
217
      // both children known, compute value
218
      Assert(childrenJustify.size() == 1 && childrenJustify[0] != 0);
219
      cache[cur] =
220
          ((k == XOR ? -1 : 1) * lastChildJustify == childrenJustify[0]) ? 1
221
                                                                         : -1;
222
    }
223
  }
224
138
  return false;
225
}
226
227
204
int RelevanceManager::justify(
228
    TNode n, std::unordered_map<TNode, int, TNodeHashFunction>& cache)
229
{
230
  // the vector of values of children
231
408
  std::unordered_map<TNode, std::vector<int>, TNodeHashFunction> childJustify;
232
204
  std::unordered_map<TNode, int, TNodeHashFunction>::iterator it;
233
204
  std::unordered_map<TNode, std::vector<int>, TNodeHashFunction>::iterator itc;
234
408
  std::vector<TNode> visit;
235
408
  TNode cur;
236
204
  visit.push_back(n);
237
290
  do
238
  {
239
494
    cur = visit.back();
240
    // should always have Boolean type
241
494
    Assert(cur.getType().isBoolean());
242
494
    it = cache.find(cur);
243
502
    if (it != cache.end())
244
    {
245
8
      visit.pop_back();
246
      // already computed value
247
8
      continue;
248
    }
249
486
    itc = childJustify.find(cur);
250
    // have we traversed to children yet?
251
486
    if (itc == childJustify.end())
252
    {
253
      // are we not a Boolean connective (including NOT)?
254
341
      if (isBooleanConnective(cur))
255
      {
256
        // initialize its children justify vector as empty
257
138
        childJustify[cur].clear();
258
        // start with the first child
259
138
        visit.push_back(cur[0]);
260
      }
261
      else
262
      {
263
203
        visit.pop_back();
264
        // The atom case, lookup the value in the valuation class to
265
        // see its current value in the SAT solver, if it has one.
266
203
        int ret = 0;
267
        // otherwise we look up the value
268
        bool value;
269
203
        if (d_val.hasSatValue(cur, value))
270
        {
271
203
          ret = value ? 1 : -1;
272
203
          d_rset.insert(cur);
273
        }
274
203
        cache[cur] = ret;
275
      }
276
    }
277
    else
278
    {
279
      // this processes the impact of the current child on the value of cur,
280
      // and possibly requests that a new child is computed.
281
145
      if (updateJustifyLastChild(cur, itc->second, cache))
282
      {
283
7
        Assert(itc->second.size() < cur.getNumChildren());
284
14
        TNode nextChild = cur[itc->second.size()];
285
7
        visit.push_back(nextChild);
286
      }
287
      else
288
      {
289
138
        visit.pop_back();
290
      }
291
    }
292
494
  } while (!visit.empty());
293
204
  Assert(cache.find(n) != cache.end());
294
408
  return cache[n];
295
}
296
297
1096
bool RelevanceManager::isRelevant(Node lit)
298
{
299
1096
  if (!d_computed)
300
  {
301
44
    computeRelevance();
302
  }
303
1096
  if (!d_success)
304
  {
305
    // always relevant if we failed to compute
306
    return true;
307
  }
308
  // agnostic to negation
309
1936
  while (lit.getKind() == NOT)
310
  {
311
420
    lit = lit[0];
312
  }
313
1096
  return d_rset.find(lit) != d_rset.end();
314
}
315
316
}  // namespace theory
317
26676
}  // namespace CVC4