GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/sygus/sygus_explain.cpp Lines: 157 164 95.7 %
Date: 2021-03-23 Branches: 292 788 37.1 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file sygus_explain.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 techniques for sygus explanations
13
 **/
14
15
#include "theory/quantifiers/sygus/sygus_explain.h"
16
17
#include "expr/dtype.h"
18
#include "expr/dtype_cons.h"
19
#include "smt/logic_exception.h"
20
#include "theory/datatypes/theory_datatypes_utils.h"
21
#include "theory/quantifiers/sygus/sygus_invariance.h"
22
#include "theory/quantifiers/sygus/term_database_sygus.h"
23
24
using namespace CVC4::kind;
25
using namespace std;
26
27
namespace CVC4 {
28
namespace theory {
29
namespace quantifiers {
30
31
87888
void TermRecBuild::addTerm(Node n)
32
{
33
87888
  d_term.push_back(n);
34
175776
  std::vector<Node> currc;
35
87888
  d_kind.push_back(n.getKind());
36
87888
  if (n.getMetaKind() == kind::metakind::PARAMETERIZED)
37
  {
38
87864
    currc.push_back(n.getOperator());
39
87864
    d_has_op.push_back(true);
40
  }
41
  else
42
  {
43
24
    d_has_op.push_back(false);
44
  }
45
157201
  for (unsigned i = 0; i < n.getNumChildren(); i++)
46
  {
47
69313
    currc.push_back(n[i]);
48
  }
49
87888
  d_children.push_back(currc);
50
87888
}
51
52
21406
void TermRecBuild::init(Node n)
53
{
54
21406
  Assert(d_term.empty());
55
21406
  addTerm(n);
56
21406
}
57
58
66482
void TermRecBuild::push(unsigned p)
59
{
60
66482
  Assert(!d_term.empty());
61
66482
  unsigned curr = d_term.size() - 1;
62
66482
  Assert(d_pos.size() == curr);
63
66482
  Assert(d_pos.size() + 1 == d_children.size());
64
66482
  Assert(p < d_term[curr].getNumChildren());
65
66482
  addTerm(d_term[curr][p]);
66
66482
  d_pos.push_back(p);
67
66482
}
68
69
66482
void TermRecBuild::pop()
70
{
71
66482
  Assert(!d_pos.empty());
72
66482
  d_pos.pop_back();
73
66482
  d_kind.pop_back();
74
66482
  d_has_op.pop_back();
75
66482
  d_children.pop_back();
76
66482
  d_term.pop_back();
77
66482
}
78
79
135717
void TermRecBuild::replaceChild(unsigned i, Node r)
80
{
81
135717
  Assert(!d_term.empty());
82
135717
  unsigned curr = d_term.size() - 1;
83
135717
  unsigned o = d_has_op[curr] ? 1 : 0;
84
135717
  d_children[curr][i + o] = r;
85
135717
}
86
87
Node TermRecBuild::getChild(unsigned i)
88
{
89
  unsigned curr = d_term.size() - 1;
90
  unsigned o = d_has_op[curr] ? 1 : 0;
91
  return d_children[curr][i + o];
92
}
93
94
108817
Node TermRecBuild::build(unsigned d)
95
{
96
108817
  Assert(d_pos.size() + 1 == d_term.size());
97
108817
  Assert(d < d_term.size());
98
108817
  int p = d < d_pos.size() ? d_pos[d] : -2;
99
217634
  std::vector<Node> children;
100
108817
  unsigned o = d_has_op[d] ? 1 : 0;
101
437471
  for (unsigned i = 0; i < d_children[d].size(); i++)
102
  {
103
657308
    Node nc;
104
328654
    if (p + o == i)
105
    {
106
39582
      nc = build(d + 1);
107
    }
108
    else
109
    {
110
289072
      nc = d_children[d][i];
111
    }
112
328654
    children.push_back(nc);
113
  }
114
217634
  return NodeManager::currentNM()->mkNode(d_kind[d], children);
115
}
116
117
58793
void SygusExplain::getExplanationForEquality(Node n,
118
                                             Node vn,
119
                                             std::vector<Node>& exp)
120
{
121
117586
  std::map<unsigned, bool> cexc;
122
58793
  getExplanationForEquality(n, vn, exp, cexc);
123
58793
}
124
125
60292
void SygusExplain::getExplanationForEquality(Node n,
126
                                             Node vn,
127
                                             std::vector<Node>& exp,
128
                                             std::map<unsigned, bool>& cexc)
129
{
130
  // since builtin types occur in grammar, types are comparable but not
131
  // necessarily equal
132
60292
  Assert(n.getType().isComparableTo(n.getType()));
133
60292
  if (n == vn)
134
  {
135
663
    return;
136
  }
137
119921
  TypeNode tn = n.getType();
138
60292
  if (!tn.isDatatype())
139
  {
140
    // sygus datatype fields that are not sygus datatypes are treated as
141
    // abstractions only, hence we disregard this field
142
663
    return;
143
  }
144
59629
  Assert(vn.getKind() == kind::APPLY_CONSTRUCTOR);
145
59629
  const DType& dt = tn.getDType();
146
59629
  int i = datatypes::utils::indexOf(vn.getOperator());
147
119258
  Node tst = datatypes::utils::mkTester(n, i, dt);
148
59629
  exp.push_back(tst);
149
86116
  for (unsigned j = 0; j < vn.getNumChildren(); j++)
150
  {
151
26487
    if (cexc.find(j) == cexc.end())
152
    {
153
      Node sel = NodeManager::currentNM()->mkNode(
154
52974
          kind::APPLY_SELECTOR_TOTAL, dt[i].getSelectorInternal(tn, j), n);
155
26487
      getExplanationForEquality(sel, vn[j], exp);
156
    }
157
  }
158
}
159
160
1499
Node SygusExplain::getExplanationForEquality(Node n, Node vn)
161
{
162
2998
  std::map<unsigned, bool> cexc;
163
2998
  return getExplanationForEquality(n, vn, cexc);
164
}
165
166
1499
Node SygusExplain::getExplanationForEquality(Node n,
167
                                             Node vn,
168
                                             std::map<unsigned, bool>& cexc)
169
{
170
2998
  std::vector<Node> exp;
171
1499
  getExplanationForEquality(n, vn, exp, cexc);
172
1499
  Assert(!exp.empty());
173
1856
  return exp.size() == 1 ? exp[0]
174
3355
                         : NodeManager::currentNM()->mkNode(kind::AND, exp);
175
}
176
177
// we have ( n = vn => eval( n ) = bvr ) ^ vn != vnr , returns exp such that exp
178
// => ( eval( n ) = bvr ^ vn != vnr )
179
87888
void SygusExplain::getExplanationFor(TermRecBuild& trb,
180
                                     Node n,
181
                                     Node vn,
182
                                     std::vector<Node>& exp,
183
                                     std::map<TypeNode, int>& var_count,
184
                                     SygusInvarianceTest& et,
185
                                     Node vnr,
186
                                     Node& vnr_exp,
187
                                     int& sz)
188
{
189
87888
  Assert(vnr.isNull() || vn != vnr);
190
87888
  Assert(n.getType().isComparableTo(vn.getType()));
191
175674
  TypeNode ntn = n.getType();
192
87888
  if (!ntn.isDatatype())
193
  {
194
    // SyGuS datatype fields that are not sygus datatypes are treated as
195
    // abstractions only, hence we disregard this field. It is important
196
    // that users of this method pay special attention to any constants,
197
    // otherwise the explanation n.eqNode(vn) is necessary here. For example,
198
    // any lemma schema that blocks the current value of an enumerator should
199
    // not make any assumptions about the value of the arguments of its any
200
    // constant constructors, since their explanation is not included here.
201
102
    return;
202
  }
203
87786
  Assert(vn.getKind() == APPLY_CONSTRUCTOR);
204
87786
  Assert(vnr.isNull() || vnr.getKind() == APPLY_CONSTRUCTOR);
205
175572
  std::map<unsigned, bool> cexc;
206
  // for each child,
207
  // check whether replacing that child by a fresh variable
208
  // also satisfies the invariance test.
209
157021
  for (unsigned i = 0; i < vn.getNumChildren(); i++)
210
  {
211
138470
    TypeNode xtn = vn[i].getType();
212
138470
    Node x = d_tdb->getFreeVarInc(xtn, var_count);
213
69235
    trb.replaceChild(i, x);
214
138470
    Node nvn = trb.build();
215
69235
    Assert(nvn.getKind() == kind::APPLY_CONSTRUCTOR);
216
69235
    if (et.is_invariant(d_tdb, nvn, x))
217
    {
218
2753
      cexc[i] = true;
219
      // we are tracking term size if positive
220
2753
      if (sz >= 0)
221
      {
222
332
        int s = d_tdb->getSygusTermSize(vn[i]);
223
332
        sz = sz - s;
224
      }
225
    }
226
    else
227
    {
228
      // revert
229
66482
      trb.replaceChild(i, vn[i]);
230
    }
231
  }
232
87786
  const DType& dt = ntn.getDType();
233
87786
  int cindex = datatypes::utils::indexOf(vn.getOperator());
234
87786
  Assert(cindex >= 0 && cindex < (int)dt.getNumConstructors());
235
175572
  Node tst = datatypes::utils::mkTester(n, cindex, dt);
236
87786
  exp.push_back(tst);
237
  // if the operator of vn is different than vnr, then disunification obligation
238
  // is met
239
87786
  if (!vnr.isNull())
240
  {
241
4923
    if (vnr.getOperator() != vn.getOperator())
242
    {
243
2653
      vnr = Node::null();
244
2653
      vnr_exp = NodeManager::currentNM()->mkConst(true);
245
    }
246
  }
247
157021
  for (unsigned i = 0; i < vn.getNumChildren(); i++)
248
  {
249
    Node sel = NodeManager::currentNM()->mkNode(
250
138470
        kind::APPLY_SELECTOR_TOTAL, dt[cindex].getSelectorInternal(ntn, i), n);
251
138470
    Node vnr_c = vnr.isNull() ? vnr : (vn[i] == vnr[i] ? Node::null() : vnr[i]);
252
69235
    if (cexc.find(i) == cexc.end())
253
    {
254
66482
      trb.push(i);
255
132964
      Node vnr_exp_c;
256
66482
      getExplanationFor(
257
          trb, sel, vn[i], exp, var_count, et, vnr_c, vnr_exp_c, sz);
258
66482
      trb.pop();
259
66482
      if (!vnr_c.isNull())
260
      {
261
2264
        Assert(!vnr_exp_c.isNull());
262
2264
        if (vnr_exp_c.isConst() || vnr_exp.isNull())
263
        {
264
          // recursively satisfied the disunification obligation
265
2264
          if (vnr_exp_c.isConst())
266
          {
267
            // was successful, don't consider further
268
2264
            vnr = Node::null();
269
          }
270
2264
          vnr_exp = vnr_exp_c;
271
        }
272
      }
273
    }
274
    else
275
    {
276
      // if excluded, we may need to add the explanation for this
277
2753
      if (vnr_exp.isNull() && !vnr_c.isNull())
278
      {
279
8
        vnr_exp = getExplanationForEquality(sel, vnr[i]);
280
      }
281
    }
282
  }
283
}
284
285
void SygusExplain::getExplanationFor(Node n,
286
                                     Node vn,
287
                                     std::vector<Node>& exp,
288
                                     SygusInvarianceTest& et,
289
                                     Node vnr,
290
                                     unsigned& sz)
291
{
292
  std::map<TypeNode, int> var_count;
293
  return getExplanationFor(n, vn, exp, et, vnr, var_count, sz);
294
}
295
296
2659
void SygusExplain::getExplanationFor(Node n,
297
                                     Node vn,
298
                                     std::vector<Node>& exp,
299
                                     SygusInvarianceTest& et,
300
                                     Node vnr,
301
                                     std::map<TypeNode, int>& var_count,
302
                                     unsigned& sz)
303
{
304
  // naive :
305
  // return getExplanationForEquality( n, vn, exp );
306
307
  // set up the recursion object;
308
5318
  TermRecBuild trb;
309
2659
  trb.init(vn);
310
5318
  Node vnr_exp;
311
2659
  int sz_use = sz;
312
2659
  getExplanationFor(trb, n, vn, exp, var_count, et, vnr, vnr_exp, sz_use);
313
2659
  Assert(sz_use >= 0);
314
2659
  sz = sz_use;
315
2659
  Assert(vnr.isNull() || !vnr_exp.isNull());
316
2659
  if (!vnr_exp.isNull() && !vnr_exp.isConst())
317
  {
318
6
    exp.push_back(vnr_exp.negate());
319
  }
320
2659
}
321
322
11448
void SygusExplain::getExplanationFor(Node n,
323
                                     Node vn,
324
                                     std::vector<Node>& exp,
325
                                     SygusInvarianceTest& et,
326
                                     bool strict)
327
{
328
22896
  std::map<TypeNode, int> var_count;
329
11448
  getExplanationFor(n, vn, exp, et, var_count, strict);
330
11448
}
331
332
23491
void SygusExplain::getExplanationFor(Node n,
333
                                     Node vn,
334
                                     std::vector<Node>& exp,
335
                                     SygusInvarianceTest& et,
336
                                     std::map<TypeNode, int>& var_count,
337
                                     bool strict)
338
{
339
23491
  if (!strict)
340
  {
341
    // check if it is invariant over the entire node
342
19342
    TypeNode vtn = vn.getType();
343
19342
    Node x = d_tdb->getFreeVarInc(vtn, var_count);
344
12043
    if (et.is_invariant(d_tdb, x, x))
345
    {
346
4744
      return;
347
    }
348
7299
    var_count[vtn]--;
349
  }
350
18747
  int sz = -1;
351
37494
  TermRecBuild trb;
352
18747
  trb.init(vn);
353
37494
  Node vnr;
354
37494
  Node vnr_exp;
355
18747
  getExplanationFor(trb, n, vn, exp, var_count, et, vnr, vnr_exp, sz);
356
}
357
358
} /* CVC4::theory::quantifiers namespace */
359
} /* CVC4::theory namespace */
360
26685
} /* CVC4 namespace */