GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/sygus/type_info.cpp Lines: 197 233 84.5 %
Date: 2021-03-23 Branches: 311 782 39.8 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file type_info.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 sygus type info class
13
 **/
14
15
#include "theory/quantifiers/sygus/type_info.h"
16
17
#include "base/check.h"
18
#include "expr/dtype.h"
19
#include "expr/dtype_cons.h"
20
#include "expr/sygus_datatype.h"
21
#include "theory/datatypes/sygus_datatype_utils.h"
22
#include "theory/quantifiers/sygus/term_database_sygus.h"
23
#include "theory/quantifiers/sygus/type_node_id_trie.h"
24
25
using namespace CVC4::kind;
26
27
namespace CVC4 {
28
namespace theory {
29
namespace quantifiers {
30
31
2682
SygusTypeInfo::SygusTypeInfo()
32
    : d_hasIte(false),
33
      d_min_term_size(0),
34
      d_sym_cons_any_constant(-1),
35
2682
      d_has_subterm_sym_cons(false)
36
{
37
2682
}
38
39
2682
void SygusTypeInfo::initialize(TermDbSygus* tds, TypeNode tn)
40
{
41
2682
  d_this = tn;
42
2682
  Assert(tn.isDatatype());
43
2682
  const DType& dt = tn.getDType();
44
2682
  Assert(dt.isSygus());
45
2682
  Trace("sygus-db") << "Register type " << dt.getName() << "..." << std::endl;
46
5364
  TypeNode btn = dt.getSygusType();
47
2682
  d_btype = btn;
48
2682
  Assert(!d_btype.isNull());
49
  // get the sygus variable list
50
5364
  Node var_list = dt.getSygusVarList();
51
2682
  if (!var_list.isNull())
52
  {
53
7435
    for (unsigned j = 0; j < var_list.getNumChildren(); j++)
54
    {
55
10794
      Node sv = var_list[j];
56
      SygusVarNumAttribute svna;
57
5397
      sv.setAttribute(svna, j);
58
5397
      d_var_list.push_back(sv);
59
    }
60
  }
61
  else
62
  {
63
    // no arguments to synthesis functions
64
644
    d_var_list.clear();
65
  }
66
67
  // compute min term size information: this must be computed before registering
68
  // subfield types
69
2682
  d_min_term_size = 1;
70
17955
  for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
71
  {
72
15273
    if (dt[i].getNumArgs() == 0)
73
    {
74
6611
      d_min_term_size = 0;
75
    }
76
  }
77
78
  // register connected types
79
17955
  for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
80
  {
81
32085
    for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
82
    {
83
33624
      TypeNode ctn = dt[i].getArgType(j);
84
16812
      Trace("sygus-db") << "  register subfield type " << ctn << std::endl;
85
16812
      if (tds->registerSygusType(ctn))
86
      {
87
16748
        SygusTypeInfo& stic = tds->getTypeInfo(ctn);
88
        // carry type attributes
89
16748
        if (stic.d_has_subterm_sym_cons)
90
        {
91
288
          d_has_subterm_sym_cons = true;
92
        }
93
      }
94
    }
95
  }
96
  // iterate over constructors
97
17955
  for (unsigned i = 0; i < dt.getNumConstructors(); i++)
98
  {
99
30546
    Node sop = dt[i].getSygusOp();
100
15273
    Assert(!sop.isNull());
101
15273
    Trace("sygus-db") << "  Operator #" << i << " : " << sop;
102
15273
    Kind builtinKind = UNDEFINED_KIND;
103
15273
    if (sop.getKind() == kind::BUILTIN)
104
    {
105
5126
      builtinKind = NodeManager::operatorToKind(sop);
106
5126
      Trace("sygus-db") << ", kind = " << builtinKind;
107
    }
108
10147
    else if (sop.isConst() && dt[i].getNumArgs() == 0)
109
    {
110
4362
      Trace("sygus-db") << ", constant";
111
4362
      d_consts[sop] = i;
112
4362
      d_arg_const[i] = sop;
113
    }
114
5785
    else if (sop.getKind() == LAMBDA)
115
    {
116
      // do type checking
117
3351
      Assert(sop[0].getNumChildren() == dt[i].getNumArgs());
118
9687
      for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
119
      {
120
12672
        TypeNode ct = dt[i].getArgType(j);
121
12672
        TypeNode cbt = tds->sygusToBuiltinType(ct);
122
12672
        TypeNode lat = sop[0][j].getType();
123
12672
        AlwaysAssert(cbt.isSubtypeOf(lat))
124
6336
            << "In sygus datatype " << dt.getName()
125
            << ", argument to a lambda constructor is not " << lat << std::endl;
126
      }
127
      // See if it is a builtin kind, possible if the operator is of the form:
128
      // lambda x1 ... xn. f( x1, ..., xn ) and f is not a parameterized kind
129
      // (e.g. APPLY_UF is a parameterized kind).
130
3351
      if (sop[1].getMetaKind() != kind::metakind::PARAMETERIZED)
131
      {
132
2783
        size_t nchild = sop[0].getNumChildren();
133
2783
        if (nchild == sop[1].getNumChildren())
134
        {
135
2637
          builtinKind = sop[1].getKind();
136
7823
          for (size_t j = 0; j < nchild; j++)
137
          {
138
5202
            if (sop[0][j] != sop[1][j])
139
            {
140
              // arguments not in order
141
16
              builtinKind = UNDEFINED_KIND;
142
16
              break;
143
            }
144
          }
145
        }
146
      }
147
    }
148
15273
    if (builtinKind != UNDEFINED_KIND)
149
    {
150
7747
      d_kinds[builtinKind] = i;
151
7747
      d_arg_kind[i] = builtinKind;
152
7747
      if (builtinKind == ITE)
153
      {
154
        // mark that this type has an ITE
155
903
        d_hasIte = true;
156
      }
157
    }
158
    // symbolic constructors
159
15273
    if (sop.getAttribute(SygusAnyConstAttribute()))
160
    {
161
64
      d_sym_cons_any_constant = i;
162
64
      d_has_subterm_sym_cons = true;
163
    }
164
15273
    d_ops[sop] = i;
165
15273
    d_arg_ops[i] = sop;
166
15273
    Trace("sygus-db") << std::endl;
167
    // We must properly catch type errors in sygus grammars for arguments of
168
    // builtin operators. The challenge is that we easily ask for expected
169
    // argument types of builtin operators e.g. PLUS. Hence we use a call to
170
    // mkGeneric below. This ensures that terms that this constructor encodes
171
    // are of the type specified in the datatype. This will fail if
172
    // e.g. bitvector-and is a constructor of an integer grammar. Our (version
173
    // 2) SyGuS parser ensures that sygus constructors are built from well-typed
174
    // terms, so the term created by mkGeneric will also be well-typed here.
175
30546
    Node g = tds->mkGeneric(dt, i);
176
30546
    TypeNode gtn = g.getType();
177
30546
    AlwaysAssert(gtn.isSubtypeOf(btn))
178
15273
        << "Sygus datatype " << dt.getName()
179
        << " encodes terms that are not of type " << btn << std::endl;
180
15273
    Trace("sygus-db") << "...done register Operator #" << i << std::endl;
181
  }
182
  // compute minimum type depth information
183
2682
  computeMinTypeDepthInternal(tn, 0);
184
  // compute minimum term size information
185
2682
  d_min_term_size = 1;
186
17955
  for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
187
  {
188
15273
    unsigned csize = 0;
189
15273
    if (dt[i].getNumArgs() > 0)
190
    {
191
8662
      csize = 1;
192
25474
      for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
193
      {
194
33624
        TypeNode ct = dt[i].getArgType(j);
195
16812
        if (ct == tn)
196
        {
197
10617
          csize += d_min_term_size;
198
        }
199
6195
        else if (tds->isRegistered(ct))
200
        {
201
6131
          SygusTypeInfo& stic = tds->getTypeInfo(ct);
202
6131
          csize += stic.getMinTermSize();
203
        }
204
        else
205
        {
206
64
          Assert(!ct.isDatatype() || !ct.getDType().isSygus());
207
        }
208
      }
209
    }
210
15273
    d_min_cons_term_size[i] = csize;
211
  }
212
5364
  Trace("sygus-db") << "Register type " << dt.getName() << " finished"
213
2682
                    << std::endl;
214
2682
}
215
216
2
void SygusTypeInfo::initializeVarSubclasses()
217
{
218
2
  if (d_var_list.empty())
219
  {
220
    // no variables
221
    return;
222
  }
223
2
  if (!d_var_subclass_id.empty())
224
  {
225
    // already computed
226
    return;
227
  }
228
  // compute variable subclasses
229
4
  std::vector<TypeNode> sf_types;
230
2
  getSubfieldTypes(sf_types);
231
  // maps variables to the list of subfield types they occur in
232
4
  std::map<Node, std::vector<TypeNode> > type_occurs;
233
6
  for (const Node& v : d_var_list)
234
  {
235
4
    type_occurs[v].clear();
236
  }
237
  // for each type of subfield type of this enumerator
238
4
  for (unsigned i = 0, ntypes = sf_types.size(); i < ntypes; i++)
239
  {
240
4
    std::vector<unsigned> rm_indices;
241
4
    TypeNode stn = sf_types[i];
242
2
    Assert(stn.isDatatype());
243
2
    const DType& dt = stn.getDType();
244
8
    for (unsigned j = 0, ncons = dt.getNumConstructors(); j < ncons; j++)
245
    {
246
12
      Node sopn = dt[j].getSygusOp();
247
6
      Assert(!sopn.isNull());
248
6
      if (type_occurs.find(sopn) != type_occurs.end())
249
      {
250
        // if it is a variable, store that it occurs in stn
251
4
        type_occurs[sopn].push_back(stn);
252
      }
253
    }
254
  }
255
4
  TypeNodeIdTrie tnit;
256
6
  for (std::pair<const Node, std::vector<TypeNode> >& to : type_occurs)
257
  {
258
4
    tnit.add(to.first, to.second);
259
  }
260
  // 0 is reserved for "no type class id"
261
2
  unsigned typeIdCount = 1;
262
2
  tnit.assignIds(d_var_subclass_id, typeIdCount);
263
  // assign the list and reverse map to index
264
6
  for (std::pair<const Node, std::vector<TypeNode> >& to : type_occurs)
265
  {
266
8
    Node v = to.first;
267
4
    unsigned sc = d_var_subclass_id[v];
268
4
    Trace("sygus-db") << v << " has subclass id " << sc << std::endl;
269
4
    d_var_subclass_list_index[v] = d_var_subclass_list[sc].size();
270
4
    d_var_subclass_list[sc].push_back(v);
271
  }
272
}
273
274
11315
TypeNode SygusTypeInfo::getBuiltinType() const { return d_btype; }
275
276
223070
const std::vector<Node>& SygusTypeInfo::getVarList() const
277
{
278
223070
  return d_var_list;
279
}
280
281
53964
void SygusTypeInfo::computeMinTypeDepthInternal(TypeNode tn,
282
                                                unsigned type_depth)
283
{
284
53964
  std::map<TypeNode, unsigned>::iterator it = d_min_type_depth.find(tn);
285
53964
  if (it != d_min_type_depth.end() && type_depth >= it->second)
286
  {
287
    // no new information
288
92362
    return;
289
  }
290
7861
  if (!tn.isDatatype())
291
  {
292
    // do not recurse to non-datatype types
293
156
    return;
294
  }
295
7705
  const DType& dt = tn.getDType();
296
7705
  if (!dt.isSygus())
297
  {
298
    // do not recurse to non-sygus datatype types
299
    return;
300
  }
301
7705
  d_min_type_depth[tn] = type_depth;
302
  // compute for connected types
303
51856
  for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
304
  {
305
95433
    for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
306
    {
307
102564
      TypeNode at = dt[i].getArgType(j);
308
51282
      computeMinTypeDepthInternal(at, type_depth + 1);
309
    }
310
  }
311
}
312
313
unsigned SygusTypeInfo::getMinTypeDepth(TypeNode tn) const
314
{
315
  std::map<TypeNode, unsigned>::const_iterator it = d_min_type_depth.find(tn);
316
  if (it != d_min_type_depth.end())
317
  {
318
    Assert(false);
319
    return 0;
320
  }
321
  return it->second;
322
}
323
324
6131
unsigned SygusTypeInfo::getMinTermSize() const { return d_min_term_size; }
325
326
unsigned SygusTypeInfo::getMinConsTermSize(unsigned cindex)
327
{
328
  std::map<unsigned, unsigned>::iterator it = d_min_cons_term_size.find(cindex);
329
  if (it != d_min_cons_term_size.end())
330
  {
331
    return it->second;
332
  }
333
  Assert(false);
334
  return 0;
335
}
336
337
663
void SygusTypeInfo::getSubfieldTypes(std::vector<TypeNode>& sf_types) const
338
{
339
2065
  for (const std::pair<const TypeNode, unsigned>& st : d_min_type_depth)
340
  {
341
1402
    sf_types.push_back(st.first);
342
  }
343
663
}
344
345
29219
int SygusTypeInfo::getKindConsNum(Kind k) const
346
{
347
29219
  std::map<Kind, unsigned>::const_iterator it = d_kinds.find(k);
348
29219
  if (it != d_kinds.end())
349
  {
350
28725
    return static_cast<int>(it->second);
351
  }
352
494
  return -1;
353
}
354
355
288
int SygusTypeInfo::getConstConsNum(Node n) const
356
{
357
288
  std::map<Node, unsigned>::const_iterator it = d_consts.find(n);
358
288
  if (it != d_consts.end())
359
  {
360
258
    return static_cast<int>(it->second);
361
  }
362
30
  return -1;
363
}
364
365
373
int SygusTypeInfo::getOpConsNum(Node n) const
366
{
367
373
  std::map<Node, unsigned>::const_iterator it = d_ops.find(n);
368
373
  if (it != d_ops.end())
369
  {
370
36
    return static_cast<int>(it->second);
371
  }
372
337
  return -1;
373
}
374
375
11868
bool SygusTypeInfo::hasKind(Kind k) const { return getKindConsNum(k) != -1; }
376
214
bool SygusTypeInfo::hasIte() const { return d_hasIte; }
377
288
bool SygusTypeInfo::hasConst(Node n) const { return getConstConsNum(n) != -1; }
378
bool SygusTypeInfo::hasOp(Node n) const { return getOpConsNum(n) != -1; }
379
380
Node SygusTypeInfo::getConsNumOp(unsigned i) const
381
{
382
  std::map<unsigned, Node>::const_iterator itn = d_arg_ops.find(i);
383
  if (itn != d_arg_ops.end())
384
  {
385
    return itn->second;
386
  }
387
  return Node::null();
388
}
389
390
3825
Node SygusTypeInfo::getConsNumConst(unsigned i) const
391
{
392
3825
  std::map<unsigned, Node>::const_iterator itn = d_arg_const.find(i);
393
3825
  if (itn != d_arg_const.end())
394
  {
395
1977
    return itn->second;
396
  }
397
1848
  return Node::null();
398
}
399
400
13802
Kind SygusTypeInfo::getConsNumKind(unsigned i) const
401
{
402
13802
  std::map<unsigned, Kind>::const_iterator itk = d_arg_kind.find(i);
403
13802
  if (itk != d_arg_kind.end())
404
  {
405
7362
    return itk->second;
406
  }
407
6440
  return UNDEFINED_KIND;
408
}
409
410
bool SygusTypeInfo::isKindArg(unsigned i) const
411
{
412
  return getConsNumKind(i) != UNDEFINED_KIND;
413
}
414
415
bool SygusTypeInfo::isConstArg(unsigned i) const
416
{
417
  return d_arg_const.find(i) != d_arg_const.end();
418
}
419
420
2684
int SygusTypeInfo::getAnyConstantConsNum() const
421
{
422
2684
  return d_sym_cons_any_constant;
423
}
424
425
31985
bool SygusTypeInfo::hasSubtermSymbolicCons() const
426
{
427
31985
  return d_has_subterm_sym_cons;
428
}
429
430
26
unsigned SygusTypeInfo::getSubclassForVar(Node n) const
431
{
432
26
  std::map<Node, unsigned>::const_iterator itcc = d_var_subclass_id.find(n);
433
26
  if (itcc == d_var_subclass_id.end())
434
  {
435
    Assert(false);
436
    return 0;
437
  }
438
26
  return itcc->second;
439
}
440
441
16
unsigned SygusTypeInfo::getNumSubclassVars(unsigned sc) const
442
{
443
  std::map<unsigned, std::vector<Node> >::const_iterator itvv =
444
16
      d_var_subclass_list.find(sc);
445
16
  if (itvv == d_var_subclass_list.end())
446
  {
447
    Assert(false);
448
    return 0;
449
  }
450
16
  return itvv->second.size();
451
}
452
6
Node SygusTypeInfo::getVarSubclassIndex(unsigned sc, unsigned i) const
453
{
454
  std::map<unsigned, std::vector<Node> >::const_iterator itvv =
455
6
      d_var_subclass_list.find(sc);
456
6
  if (itvv == d_var_subclass_list.end() || i >= itvv->second.size())
457
  {
458
    Assert(false);
459
    return Node::null();
460
  }
461
6
  return itvv->second[i];
462
}
463
464
12
bool SygusTypeInfo::getIndexInSubclassForVar(Node v, unsigned& index) const
465
{
466
  std::map<Node, unsigned>::const_iterator itvv =
467
12
      d_var_subclass_list_index.find(v);
468
12
  if (itvv == d_var_subclass_list_index.end())
469
  {
470
    return false;
471
  }
472
12
  index = itvv->second;
473
12
  return true;
474
}
475
476
2
bool SygusTypeInfo::isSubclassVarTrivial() const
477
{
478
  for (const std::pair<const unsigned, std::vector<Node> >& p :
479
2
       d_var_subclass_list)
480
  {
481
2
    if (p.second.size() > 1)
482
    {
483
2
      return false;
484
    }
485
  }
486
  return true;
487
}
488
489
}  // namespace quantifiers
490
}  // namespace theory
491
26685
}  // namespace CVC4