GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/skolemize.cpp Lines: 185 207 89.4 %
Date: 2021-03-23 Branches: 429 1026 41.8 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file skolemize.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Mathias Preiner
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 skolemization utility
13
 **/
14
15
#include "theory/quantifiers/skolemize.h"
16
17
#include "expr/dtype.h"
18
#include "expr/dtype_cons.h"
19
#include "expr/skolem_manager.h"
20
#include "options/quantifiers_options.h"
21
#include "options/smt_options.h"
22
#include "theory/quantifiers/quantifiers_attributes.h"
23
#include "theory/quantifiers/quantifiers_state.h"
24
#include "theory/quantifiers/term_util.h"
25
#include "theory/sort_inference.h"
26
#include "theory/theory_engine.h"
27
28
using namespace CVC4::kind;
29
30
namespace CVC4 {
31
namespace theory {
32
namespace quantifiers {
33
34
8997
Skolemize::Skolemize(QuantifiersState& qs, ProofNodeManager* pnm)
35
    : d_qstate(qs),
36
8997
      d_skolemized(qs.getUserContext()),
37
      d_pnm(pnm),
38
      d_epg(pnm == nullptr ? nullptr
39
                           : new EagerProofGenerator(
40
17994
                                 pnm, qs.getUserContext(), "Skolemize::epg"))
41
{
42
8997
}
43
44
22192
TrustNode Skolemize::process(Node q)
45
{
46
22192
  Assert(q.getKind() == FORALL);
47
  // do skolemization
48
22192
  if (d_skolemized.find(q) != d_skolemized.end())
49
  {
50
19750
    return TrustNode::null();
51
  }
52
4884
  Node lem;
53
2442
  ProofGenerator* pg = nullptr;
54
5238
  if (isProofEnabled() && !options::dtStcInduction()
55
2782
      && !options::intWfInduction())
56
  {
57
    // if using proofs and not using induction, we use the justified
58
    // skolemization
59
339
    NodeManager* nm = NodeManager::currentNM();
60
339
    SkolemManager* skm = nm->getSkolemManager();
61
678
    std::vector<Node> echildren(q.begin(), q.end());
62
339
    echildren[1] = echildren[1].notNode();
63
678
    Node existsq = nm->mkNode(EXISTS, echildren);
64
678
    Node res = skm->mkSkolemize(existsq, d_skolem_constants[q], "skv");
65
678
    Node qnot = q.notNode();
66
678
    CDProof cdp(d_pnm);
67
339
    cdp.addStep(res, PfRule::SKOLEMIZE, {qnot}, {});
68
678
    std::shared_ptr<ProofNode> pf = cdp.getProofFor(res);
69
678
    std::vector<Node> assumps;
70
339
    assumps.push_back(qnot);
71
678
    std::shared_ptr<ProofNode> pfs = d_pnm->mkScope({pf}, assumps);
72
339
    lem = nm->mkNode(IMPLIES, qnot, res);
73
339
    d_epg->setProofFor(lem, pfs);
74
339
    pg = d_epg.get();
75
678
    Trace("quantifiers-sk")
76
339
        << "Skolemize (with proofs) : " << d_skolem_constants[q] << " for "
77
339
        << std::endl;
78
339
    Trace("quantifiers-sk") << "   " << q << std::endl;
79
339
    Trace("quantifiers-sk") << "   " << res << std::endl;
80
  }
81
  else
82
  {
83
    // otherwise, we use the more general skolemization with inductive
84
    // strengthening, which does not support proofs
85
4206
    Node body = getSkolemizedBody(q);
86
4206
    NodeBuilder<> nb(kind::OR);
87
2103
    nb << q << body.notNode();
88
2103
    lem = nb;
89
  }
90
2442
  d_skolemized[q] = lem;
91
2442
  return TrustNode::mkTrustLemma(lem, pg);
92
}
93
94
33
bool Skolemize::getSkolemConstants(Node q, std::vector<Node>& skolems)
95
{
96
  std::unordered_map<Node, std::vector<Node>, NodeHashFunction>::iterator it =
97
33
      d_skolem_constants.find(q);
98
33
  if (it != d_skolem_constants.end())
99
  {
100
33
    skolems.insert(skolems.end(), it->second.begin(), it->second.end());
101
33
    return true;
102
  }
103
  return false;
104
}
105
106
Node Skolemize::getSkolemConstant(Node q, unsigned i)
107
{
108
  std::unordered_map<Node, std::vector<Node>, NodeHashFunction>::iterator it =
109
      d_skolem_constants.find(q);
110
  if (it != d_skolem_constants.end())
111
  {
112
    if (i < it->second.size())
113
    {
114
      return it->second[i];
115
    }
116
  }
117
  return Node::null();
118
}
119
120
90
void Skolemize::getSelfSel(const DType& dt,
121
                           const DTypeConstructor& dc,
122
                           Node n,
123
                           TypeNode ntn,
124
                           std::vector<Node>& selfSel)
125
{
126
180
  TypeNode tspec;
127
90
  if (dt.isParametric())
128
  {
129
    tspec = dc.getSpecializedConstructorType(n.getType());
130
    Trace("sk-ind-debug") << "Specialized constructor type : " << tspec
131
                          << std::endl;
132
    Assert(tspec.getNumChildren() == dc.getNumArgs());
133
  }
134
180
  Trace("sk-ind-debug") << "Check self sel " << dc.getName() << " "
135
90
                        << dt.getName() << std::endl;
136
90
  NodeManager* nm = NodeManager::currentNM();
137
172
  for (unsigned j = 0; j < dc.getNumArgs(); j++)
138
  {
139
164
    std::vector<Node> ssc;
140
82
    if (dt.isParametric())
141
    {
142
      Trace("sk-ind-debug") << "Compare " << tspec[j] << " " << ntn
143
                            << std::endl;
144
      if (tspec[j] == ntn)
145
      {
146
        ssc.push_back(n);
147
      }
148
    }
149
    else
150
    {
151
164
      TypeNode tn = dc[j].getRangeType();
152
82
      Trace("sk-ind-debug") << "Compare " << tn << " " << ntn << std::endl;
153
82
      if (tn == ntn)
154
      {
155
45
        ssc.push_back(n);
156
      }
157
    }
158
127
    for (unsigned k = 0; k < ssc.size(); k++)
159
    {
160
      Node ss = nm->mkNode(
161
90
          APPLY_SELECTOR_TOTAL, dc.getSelectorInternal(n.getType(), j), n);
162
45
      if (std::find(selfSel.begin(), selfSel.end(), ss) == selfSel.end())
163
      {
164
45
        selfSel.push_back(ss);
165
      }
166
    }
167
  }
168
90
}
169
170
2122
Node Skolemize::mkSkolemizedBody(Node f,
171
                                 Node n,
172
                                 std::vector<TypeNode>& argTypes,
173
                                 std::vector<TNode>& fvs,
174
                                 std::vector<Node>& sk,
175
                                 Node& sub,
176
                                 std::vector<unsigned>& sub_vars)
177
{
178
2122
  NodeManager* nm = NodeManager::currentNM();
179
2122
  Assert(sk.empty() || sk.size() == f[0].getNumChildren());
180
  // calculate the variables and substitution
181
4244
  std::vector<TNode> ind_vars;
182
4244
  std::vector<unsigned> ind_var_indicies;
183
4244
  std::vector<TNode> vars;
184
4244
  std::vector<unsigned> var_indicies;
185
5530
  for (unsigned i = 0; i < f[0].getNumChildren(); i++)
186
  {
187
3408
    if (isInductionTerm(f[0][i]))
188
    {
189
66
      ind_vars.push_back(f[0][i]);
190
66
      ind_var_indicies.push_back(i);
191
    }
192
    else
193
    {
194
3342
      vars.push_back(f[0][i]);
195
3342
      var_indicies.push_back(i);
196
    }
197
6816
    Node s;
198
    // make the new function symbol or use existing
199
3408
    if (i >= sk.size())
200
    {
201
3393
      if (argTypes.empty())
202
      {
203
10143
        s = NodeManager::currentNM()->mkSkolem(
204
6762
            "skv", f[0][i].getType(), "created during skolemization");
205
      }
206
      else
207
      {
208
        TypeNode typ = NodeManager::currentNM()->mkFunctionType(
209
24
            argTypes, f[0][i].getType());
210
        Node op = NodeManager::currentNM()->mkSkolem(
211
24
            "skop", typ, "op created during pre-skolemization");
212
        // DOTHIS: set attribute on op, marking that it should not be selected
213
        // as trigger
214
24
        std::vector<Node> funcArgs;
215
12
        funcArgs.push_back(op);
216
12
        funcArgs.insert(funcArgs.end(), fvs.begin(), fvs.end());
217
12
        s = NodeManager::currentNM()->mkNode(kind::APPLY_UF, funcArgs);
218
      }
219
3393
      sk.push_back(s);
220
    }
221
    else
222
    {
223
15
      Assert(sk[i].getType() == f[0][i].getType());
224
    }
225
  }
226
2122
  Node ret;
227
2122
  if (vars.empty())
228
  {
229
51
    ret = n;
230
  }
231
  else
232
  {
233
4142
    std::vector<Node> var_sk;
234
5413
    for (unsigned i = 0; i < var_indicies.size(); i++)
235
    {
236
3342
      var_sk.push_back(sk[var_indicies[i]]);
237
    }
238
2071
    Assert(vars.size() == var_sk.size());
239
2071
    ret = n.substitute(vars.begin(), vars.end(), var_sk.begin(), var_sk.end());
240
  }
241
2122
  if (!ind_vars.empty())
242
  {
243
51
    Trace("sk-ind") << "Ind strengthen : (not " << f << ")" << std::endl;
244
51
    Trace("sk-ind") << "Skolemized is : " << ret << std::endl;
245
102
    Node n_str_ind;
246
102
    TypeNode tn = ind_vars[0].getType();
247
102
    Node k = sk[ind_var_indicies[0]];
248
102
    Node nret = ret.substitute(ind_vars[0], k);
249
    // note : everything is under a negation
250
    // the following constructs ~( R( x, k ) => ~P( x ) )
251
51
    if (options::dtStcInduction() && tn.isDatatype())
252
    {
253
45
      const DType& dt = tn.getDType();
254
90
      std::vector<Node> disj;
255
135
      for (unsigned i = 0; i < dt.getNumConstructors(); i++)
256
      {
257
180
        std::vector<Node> selfSel;
258
90
        getSelfSel(dt, dt[i], k, tn, selfSel);
259
180
        std::vector<Node> conj;
260
90
        conj.push_back(nm->mkNode(APPLY_TESTER, dt[i].getTester(), k).negate());
261
135
        for (unsigned j = 0; j < selfSel.size(); j++)
262
        {
263
45
          conj.push_back(ret.substitute(ind_vars[0], selfSel[j]).negate());
264
        }
265
180
        disj.push_back(conj.size() == 1
266
180
                           ? conj[0]
267
                           : NodeManager::currentNM()->mkNode(OR, conj));
268
      }
269
45
      Assert(!disj.empty());
270
90
      n_str_ind = disj.size() == 1
271
90
                      ? disj[0]
272
                      : NodeManager::currentNM()->mkNode(AND, disj);
273
    }
274
6
    else if (options::intWfInduction() && tn.isInteger())
275
    {
276
      Node icond = NodeManager::currentNM()->mkNode(
277
12
          GEQ, k, NodeManager::currentNM()->mkConst(Rational(0)));
278
      Node iret =
279
18
          ret.substitute(
280
6
                 ind_vars[0],
281
18
                 NodeManager::currentNM()->mkNode(
282
12
                     MINUS, k, NodeManager::currentNM()->mkConst(Rational(1))))
283
12
              .negate();
284
6
      n_str_ind = NodeManager::currentNM()->mkNode(OR, icond.negate(), iret);
285
6
      n_str_ind = NodeManager::currentNM()->mkNode(AND, icond, n_str_ind);
286
    }
287
    else
288
    {
289
      Trace("sk-ind") << "Unknown induction for term : " << ind_vars[0]
290
                      << ", type = " << tn << std::endl;
291
      Assert(false);
292
    }
293
51
    Trace("sk-ind") << "Strengthening is : " << n_str_ind << std::endl;
294
295
102
    std::vector<Node> rem_ind_vars;
296
51
    rem_ind_vars.insert(
297
102
        rem_ind_vars.end(), ind_vars.begin() + 1, ind_vars.end());
298
51
    if (!rem_ind_vars.empty())
299
    {
300
26
      Node bvl = NodeManager::currentNM()->mkNode(BOUND_VAR_LIST, rem_ind_vars);
301
13
      nret = NodeManager::currentNM()->mkNode(FORALL, bvl, nret);
302
13
      nret = Rewriter::rewrite(nret);
303
13
      sub = nret;
304
13
      sub_vars.insert(
305
26
          sub_vars.end(), ind_var_indicies.begin() + 1, ind_var_indicies.end());
306
13
      n_str_ind = NodeManager::currentNM()
307
26
                      ->mkNode(FORALL, bvl, n_str_ind.negate())
308
26
                      .negate();
309
    }
310
51
    ret = NodeManager::currentNM()->mkNode(OR, nret, n_str_ind);
311
  }
312
4244
  Trace("quantifiers-sk-debug") << "mkSkolem body for " << f
313
2122
                                << " returns : " << ret << std::endl;
314
  // if it has an instantiation level, set the skolemized body to that level
315
2122
  if (f.hasAttribute(InstLevelAttribute()))
316
  {
317
    QuantAttributes::setInstantiationLevelAttr(
318
        ret, f.getAttribute(InstLevelAttribute()));
319
  }
320
321
2122
  Trace("quantifiers-sk") << "Skolemize : " << sk << " for " << std::endl;
322
2122
  Trace("quantifiers-sk") << "   " << f << std::endl;
323
324
4244
  return ret;
325
}
326
327
2103
Node Skolemize::getSkolemizedBody(Node f)
328
{
329
2103
  Assert(f.getKind() == FORALL);
330
  std::unordered_map<Node, Node, NodeHashFunction>::iterator it =
331
2103
      d_skolem_body.find(f);
332
2103
  if (it == d_skolem_body.end())
333
  {
334
4202
    std::vector<TypeNode> fvTypes;
335
4202
    std::vector<TNode> fvs;
336
4202
    Node sub;
337
4202
    std::vector<unsigned> sub_vars;
338
    Node ret = mkSkolemizedBody(
339
4202
        f, f[1], fvTypes, fvs, d_skolem_constants[f], sub, sub_vars);
340
2101
    d_skolem_body[f] = ret;
341
    // store sub quantifier information
342
2101
    if (!sub.isNull())
343
    {
344
      // if we are skolemizing one at a time, we already know the skolem
345
      // constants of the sub-quantified formula, store them
346
13
      Assert(d_skolem_constants[sub].empty());
347
28
      for (unsigned i = 0; i < sub_vars.size(); i++)
348
      {
349
15
        d_skolem_constants[sub].push_back(d_skolem_constants[f][sub_vars[i]]);
350
      }
351
    }
352
2101
    Assert(d_skolem_constants[f].size() == f[0].getNumChildren());
353
2101
    SortInference* si = d_qstate.getSortInference();
354
2101
    if (si != nullptr)
355
    {
356
      for (unsigned i = 0; i < d_skolem_constants[f].size(); i++)
357
      {
358
        // carry information for sort inference
359
        si->setSkolemVar(f, f[0][i], d_skolem_constants[f][i]);
360
      }
361
    }
362
2101
    return ret;
363
  }
364
2
  return it->second;
365
}
366
367
9035
bool Skolemize::isInductionTerm(Node n)
368
{
369
18070
  TypeNode tn = n.getType();
370
9035
  if (options::dtStcInduction() && tn.isDatatype())
371
  {
372
3847
    const DType& dt = tn.getDType();
373
3847
    return !dt.isCodatatype();
374
  }
375
5188
  if (options::intWfInduction() && tn.isInteger())
376
  {
377
1102
    return true;
378
  }
379
4086
  return false;
380
}
381
382
7
void Skolemize::getSkolemTermVectors(
383
    std::map<Node, std::vector<Node> >& sks) const
384
{
385
  std::unordered_map<Node, std::vector<Node>, NodeHashFunction>::const_iterator
386
7
      itk;
387
14
  for (const auto& p : d_skolemized)
388
  {
389
14
    Node q = p.first;
390
7
    itk = d_skolem_constants.find(q);
391
7
    Assert(itk != d_skolem_constants.end());
392
7
    sks[q].insert(sks[q].end(), itk->second.begin(), itk->second.end());
393
  }
394
7
}
395
396
2442
bool Skolemize::isProofEnabled() const { return d_epg != nullptr; }
397
398
} /* CVC4::theory::quantifiers namespace */
399
} /* CVC4::theory namespace */
400
26685
} /* CVC4 namespace */