GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/skolem_manager.cpp Lines: 130 134 97.0 %
Date: 2021-03-22 Branches: 287 718 40.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file skolem_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 skolem manager class
13
 **/
14
15
#include "expr/skolem_manager.h"
16
17
#include "expr/attribute.h"
18
#include "expr/bound_var_manager.h"
19
#include "expr/node_algorithm.h"
20
21
using namespace CVC4::kind;
22
23
namespace CVC4 {
24
25
// Attributes are global maps from Nodes to data. Thus, note that these could
26
// be implemented as internal maps in SkolemManager.
27
struct WitnessFormAttributeId
28
{
29
};
30
typedef expr::Attribute<WitnessFormAttributeId, Node> WitnessFormAttribute;
31
32
struct SkolemFormAttributeId
33
{
34
};
35
typedef expr::Attribute<SkolemFormAttributeId, Node> SkolemFormAttribute;
36
37
struct OriginalFormAttributeId
38
{
39
};
40
typedef expr::Attribute<OriginalFormAttributeId, Node> OriginalFormAttribute;
41
42
4600
Node SkolemManager::mkSkolem(Node v,
43
                             Node pred,
44
                             const std::string& prefix,
45
                             const std::string& comment,
46
                             int flags,
47
                             ProofGenerator* pg)
48
{
49
  // We do not currently insist that pred does not contain witness terms
50
4600
  Assert(v.getKind() == BOUND_VARIABLE);
51
  // make the witness term
52
4600
  NodeManager* nm = NodeManager::currentNM();
53
9200
  Node bvl = nm->mkNode(BOUND_VAR_LIST, v);
54
  // Make the witness term, where notice that pred may contain skolems. We do
55
  // not recursively convert pred to witness form, since witness terms should
56
  // be treated as opaque. Moreover, the use of witness forms leads to
57
  // variable shadowing issues in e.g. skolemization.
58
9200
  Node w = nm->mkNode(WITNESS, bvl, pred);
59
  // store the mapping to proof generator if it exists
60
4600
  if (pg != nullptr)
61
  {
62
    // We cache based on the existential of the original predicate
63
2804
    Node q = nm->mkNode(EXISTS, bvl, pred);
64
    // Notice this may overwrite an existing proof generator. This does not
65
    // matter since either should be able to prove q.
66
1402
    d_gens[q] = pg;
67
  }
68
4600
  Node k = mkSkolemInternal(w, prefix, comment, flags);
69
  // set witness form attribute for k
70
  WitnessFormAttribute wfa;
71
4600
  k.setAttribute(wfa, w);
72
9200
  Trace("sk-manager-skolem")
73
4600
      << "skolem: " << k << " witness " << w << std::endl;
74
9200
  return k;
75
}
76
77
1046
Node SkolemManager::mkSkolemize(Node q,
78
                                std::vector<Node>& skolems,
79
                                const std::string& prefix,
80
                                const std::string& comment,
81
                                int flags,
82
                                ProofGenerator* pg)
83
{
84
1046
  Trace("sk-manager-debug") << "mkSkolemize " << q << std::endl;
85
1046
  Assert(q.getKind() == EXISTS);
86
1046
  Node currQ = q;
87
3101
  for (const Node& av : q[0])
88
  {
89
2055
    Assert(currQ.getKind() == EXISTS && av == currQ[0][0]);
90
    // currQ is updated to the result of skolemizing its first variable in
91
    // the method below.
92
4110
    Node sk = skolemize(currQ, currQ, prefix, comment, flags);
93
4110
    Trace("sk-manager-debug")
94
2055
        << "made skolem " << sk << " for " << av << std::endl;
95
2055
    skolems.push_back(sk);
96
  }
97
1046
  if (pg != nullptr)
98
  {
99
    // Same as above, this may overwrite an existing proof generator
100
    d_gens[q] = pg;
101
  }
102
1046
  Trace("sk-manager-debug") << "...mkSkolemize returns " << currQ << std::endl;
103
1046
  return currQ;
104
}
105
106
2055
Node SkolemManager::skolemize(Node q,
107
                              Node& qskolem,
108
                              const std::string& prefix,
109
                              const std::string& comment,
110
                              int flags)
111
{
112
2055
  Assert(q.getKind() == EXISTS);
113
4110
  Node v;
114
4110
  std::vector<Node> ovars;
115
2055
  Trace("sk-manager-debug") << "mkSkolemize..." << std::endl;
116
2055
  NodeManager* nm = NodeManager::currentNM();
117
6953
  for (const Node& av : q[0])
118
  {
119
9008
    if (v.isNull())
120
    {
121
2055
      v = av;
122
2055
      continue;
123
    }
124
4898
    ovars.push_back(av);
125
  }
126
2055
  Assert(!v.isNull());
127
  // make the predicate with one variable stripped off
128
4110
  Node pred = q[1];
129
2055
  Trace("sk-manager-debug") << "make exists predicate" << std::endl;
130
2055
  if (!ovars.empty())
131
  {
132
    // keeps the same variables
133
2018
    Node bvl = nm->mkNode(BOUND_VAR_LIST, ovars);
134
    // update the predicate
135
1009
    pred = nm->mkNode(EXISTS, bvl, pred);
136
  }
137
2055
  Trace("sk-manager-debug") << "call sub mkSkolem" << std::endl;
138
  // don't use a proof generator, since this may be an intermediate, partially
139
  // skolemized formula.
140
2055
  Node k = mkSkolem(v, pred, prefix, comment, flags, nullptr);
141
2055
  Assert(k.getType() == v.getType());
142
4110
  TNode tv = v;
143
4110
  TNode tk = k;
144
4110
  Trace("sk-manager-debug")
145
2055
      << "qskolem apply " << tv << " -> " << tk << " to " << pred << std::endl;
146
  // the quantified formula with one step of skolemization
147
2055
  qskolem = pred.substitute(tv, tk);
148
2055
  Trace("sk-manager-debug") << "qskolem done substitution" << std::endl;
149
4110
  return k;
150
}
151
152
41833
Node SkolemManager::mkPurifySkolem(Node t,
153
                                   const std::string& prefix,
154
                                   const std::string& comment,
155
                                   int flags)
156
{
157
83666
  Node to = getOriginalForm(t);
158
  // We do not currently insist that to does not contain witness terms
159
160
41833
  Node k = mkSkolemInternal(to, prefix, comment, flags);
161
  // set original form attribute for k
162
  OriginalFormAttribute ofa;
163
41833
  k.setAttribute(ofa, to);
164
165
83666
  Trace("sk-manager-skolem")
166
41833
      << "skolem: " << k << " purify " << to << std::endl;
167
83666
  return k;
168
}
169
170
Node SkolemManager::mkBooleanTermVariable(Node t)
171
{
172
  return mkPurifySkolem(t, "", "", NodeManager::SKOLEM_BOOL_TERM_VAR);
173
}
174
175
23
ProofGenerator* SkolemManager::getProofGenerator(Node t) const
176
{
177
23
  std::map<Node, ProofGenerator*>::const_iterator it = d_gens.find(t);
178
23
  if (it != d_gens.end())
179
  {
180
    return it->second;
181
  }
182
23
  return nullptr;
183
}
184
185
1456
Node SkolemManager::getWitnessForm(Node k)
186
{
187
1456
  Assert(k.getKind() == SKOLEM);
188
  // simply look up the witness form for k via an attribute
189
  WitnessFormAttribute wfa;
190
1456
  return k.getAttribute(wfa);
191
}
192
193
145685
Node SkolemManager::getOriginalForm(Node n)
194
{
195
145685
  if (n.isNull())
196
  {
197
4
    return n;
198
  }
199
291362
  Trace("sk-manager-debug")
200
145681
      << "SkolemManager::getOriginalForm " << n << std::endl;
201
  OriginalFormAttribute ofa;
202
145681
  NodeManager* nm = NodeManager::currentNM();
203
291362
  std::unordered_map<TNode, Node, TNodeHashFunction> visited;
204
145681
  std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
205
291362
  std::vector<TNode> visit;
206
291362
  TNode cur;
207
145681
  visit.push_back(n);
208
521550
  do
209
  {
210
667231
    cur = visit.back();
211
667231
    visit.pop_back();
212
667231
    it = visited.find(cur);
213
214
667231
    if (it == visited.end())
215
    {
216
428171
      if (cur.hasAttribute(ofa))
217
      {
218
263674
        visited[cur] = cur.getAttribute(ofa);
219
      }
220
      else
221
      {
222
164497
        visited[cur] = Node::null();
223
164497
        visit.push_back(cur);
224
164497
        if (cur.getMetaKind() == metakind::PARAMETERIZED)
225
        {
226
18576
          visit.push_back(cur.getOperator());
227
        }
228
502974
        for (const Node& cn : cur)
229
        {
230
338477
          visit.push_back(cn);
231
        }
232
      }
233
    }
234
239060
    else if (it->second.isNull())
235
    {
236
328994
      Node ret = cur;
237
164497
      bool childChanged = false;
238
328994
      std::vector<Node> children;
239
164497
      if (cur.getMetaKind() == metakind::PARAMETERIZED)
240
      {
241
18576
        it = visited.find(cur.getOperator());
242
18576
        Assert(it != visited.end());
243
18576
        Assert(!it->second.isNull());
244
18576
        childChanged = childChanged || cur.getOperator() != it->second;
245
18576
        children.push_back(it->second);
246
      }
247
502974
      for (const Node& cn : cur)
248
      {
249
338477
        it = visited.find(cn);
250
338477
        Assert(it != visited.end());
251
338477
        Assert(!it->second.isNull());
252
338477
        childChanged = childChanged || cn != it->second;
253
338477
        children.push_back(it->second);
254
      }
255
164497
      if (childChanged)
256
      {
257
31441
        ret = nm->mkNode(cur.getKind(), children);
258
      }
259
164497
      cur.setAttribute(ofa, ret);
260
164497
      visited[cur] = ret;
261
    }
262
667231
  } while (!visit.empty());
263
145681
  Assert(visited.find(n) != visited.end());
264
145681
  Assert(!visited.find(n)->second.isNull());
265
145681
  Trace("sk-manager-debug") << "..return " << visited[n] << std::endl;
266
145681
  return visited[n];
267
}
268
269
46433
Node SkolemManager::mkSkolemInternal(Node w,
270
                                     const std::string& prefix,
271
                                     const std::string& comment,
272
                                     int flags)
273
{
274
  // note that witness, original forms are independent, but share skolems
275
46433
  NodeManager* nm = NodeManager::currentNM();
276
  // w is not necessarily a witness term
277
  SkolemFormAttribute sfa;
278
92866
  Node k;
279
  // could already have a skolem if we used w already
280
46433
  if (w.hasAttribute(sfa))
281
  {
282
8480
    return w.getAttribute(sfa);
283
  }
284
  // make the new skolem
285
37953
  if (flags & NodeManager::SKOLEM_BOOL_TERM_VAR)
286
  {
287
706
    Assert (w.getType().isBoolean());
288
706
    k = nm->mkBooleanTermVariable();
289
  }
290
  else
291
  {
292
37247
    k = nm->mkSkolem(prefix, w.getType(), comment, flags);
293
  }
294
  // set skolem form attribute for w
295
37953
  w.setAttribute(sfa, k);
296
75906
  Trace("sk-manager") << "SkolemManager::mkSkolem: " << k << " : " << w
297
37953
                      << std::endl;
298
37953
  return k;
299
}
300
301
26676
}  // namespace CVC4