GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/datatypes/sygus_simple_sym.cpp Lines: 261 281 92.9 %
Date: 2021-03-22 Branches: 563 1106 50.9 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file sygus_simple_sym.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Haniel Barbosa, 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 simple symmetry breaking for sygus
13
 **/
14
15
#include "theory/datatypes/sygus_simple_sym.h"
16
17
#include "expr/dtype_cons.h"
18
#include "theory/quantifiers/term_util.h"
19
20
using namespace std;
21
using namespace CVC4::kind;
22
23
namespace CVC4 {
24
namespace theory {
25
namespace datatypes {
26
27
2190
SygusSimpleSymBreak::SygusSimpleSymBreak(quantifiers::TermDbSygus* tds)
28
2190
    : d_tds(tds)
29
{
30
2190
}
31
32
/** Requirement trie
33
 *
34
 * This class is used to make queries about sygus grammars, including what
35
 * constructors they contain, and their types.
36
 *
37
 * As a simple example, consider the trie:
38
 * root:
39
 *   d_req_kind = PLUS
40
 *   d_children[0]:
41
 *     d_req_type = A
42
 *   d_children[1]:
43
 *     d_req_type = A
44
 * This trie is satisfied by sygus types that have a constructor whose builtin
45
 * kind is PLUS and whose argument types are both A.
46
 */
47
12440
class ReqTrie
48
{
49
 public:
50
12440
  ReqTrie() : d_req_kind(UNDEFINED_KIND) {}
51
  /** the children of this node */
52
  std::map<unsigned, ReqTrie> d_children;
53
  /** the (builtin) kind required by this node */
54
  Kind d_req_kind;
55
  /** the type that this node is required to be */
56
  TypeNode d_req_type;
57
  /** the constant required by this node */
58
  Node d_req_const;
59
  /** print this trie */
60
7610
  void print(const char* c, int indent = 0)
61
  {
62
7610
    if (d_req_kind != UNDEFINED_KIND)
63
    {
64
2969
      Trace(c) << d_req_kind << " ";
65
    }
66
4641
    else if (!d_req_type.isNull())
67
    {
68
4621
      Trace(c) << d_req_type;
69
    }
70
20
    else if (!d_req_const.isNull())
71
    {
72
20
      Trace(c) << d_req_const;
73
    }
74
    else
75
    {
76
      Trace(c) << "_";
77
    }
78
7610
    Trace(c) << std::endl;
79
13958
    for (std::map<unsigned, ReqTrie>::iterator it = d_children.begin();
80
13958
         it != d_children.end();
81
         ++it)
82
    {
83
16060
      for (int i = 0; i <= indent; i++)
84
      {
85
9712
        Trace(c) << "  ";
86
      }
87
6348
      Trace(c) << it->first << " : ";
88
6348
      it->second.print(c, indent + 1);
89
    }
90
7610
  }
91
  /**
92
   * Are the requirements of this trie satisfied by sygus type tn?
93
   * tdb is a reference to the sygus term database.
94
   */
95
7416
  bool satisfiedBy(quantifiers::TermDbSygus* tdb, TypeNode tn)
96
  {
97
7416
    if (!d_req_const.isNull())
98
    {
99
20
      quantifiers::SygusTypeInfo& sti = tdb->getTypeInfo(tn);
100
20
      if (!sti.hasConst(d_req_const))
101
      {
102
4
        return false;
103
      }
104
    }
105
7412
    if (!d_req_type.isNull())
106
    {
107
8802
      Trace("sygus-sb-debug")
108
4401
          << "- check if " << tn << " is type " << d_req_type << std::endl;
109
4401
      if (tn != d_req_type)
110
      {
111
28
        return false;
112
      }
113
    }
114
7384
    if (d_req_kind != UNDEFINED_KIND)
115
    {
116
5782
      Trace("sygus-sb-debug")
117
2891
          << "- check if " << tn << " has " << d_req_kind << std::endl;
118
5653
      std::vector<TypeNode> argts;
119
2891
      if (tdb->canConstructKind(tn, d_req_kind, argts))
120
      {
121
8812
        for (std::map<unsigned, ReqTrie>::iterator it = d_children.begin();
122
8812
             it != d_children.end();
123
             ++it)
124
        {
125
6050
          if (it->first < argts.size())
126
          {
127
12048
            TypeNode tnc = argts[it->first];
128
6050
            if (!it->second.satisfiedBy(tdb, tnc))
129
            {
130
52
              return false;
131
            }
132
          }
133
          else
134
          {
135
            return false;
136
          }
137
        }
138
      }
139
      else
140
      {
141
77
        return false;
142
      }
143
    }
144
7255
    return true;
145
  }
146
  /** is this the empty (trivially satisfied) trie? */
147
12189
  bool empty()
148
  {
149
23026
    return d_req_kind == UNDEFINED_KIND && d_req_const.isNull()
150
23026
           && d_req_type.isNull() && d_children.empty();
151
  }
152
};
153
154
4976
bool SygusSimpleSymBreak::considerArgKind(
155
    TypeNode tn, TypeNode tnp, Kind k, Kind pk, int arg)
156
{
157
4976
  const DType& pdt = tnp.getDType();
158
4976
  const DType& dt = tn.getDType();
159
4976
  quantifiers::SygusTypeInfo& ti = d_tds->getTypeInfo(tn);
160
4976
  quantifiers::SygusTypeInfo& pti = d_tds->getTypeInfo(tnp);
161
4976
  Assert(ti.hasKind(k));
162
4976
  Assert(pti.hasKind(pk));
163
9952
  Trace("sygus-sb-debug") << "Consider sygus arg kind " << k << ", pk = " << pk
164
4976
                          << ", arg = " << arg << " in " << tnp << "?"
165
4976
                          << std::endl;
166
4976
  int c = ti.getKindConsNum(k);
167
4976
  int pc = pti.getKindConsNum(pk);
168
  // check for associativity
169
4976
  if (k == pk && quantifiers::TermUtil::isAssoc(k))
170
  {
171
    // if the operator is associative, then a repeated occurrence should only
172
    // occur in the leftmost argument position
173
416
    int firstArg = getFirstArgOccurrence(pdt[pc], tn);
174
416
    Assert(firstArg != -1);
175
416
    if (arg == firstArg)
176
    {
177
208
      return true;
178
    }
179
    // the argument types of the child must be the parent's type
180
604
    for (unsigned i = 0, nargs = dt[c].getNumArgs(); i < nargs; i++)
181
    {
182
802
      TypeNode type = dt[c].getArgType(i);
183
406
      if (type != tnp)
184
      {
185
10
        return true;
186
      }
187
    }
188
396
    Trace("sygus-sb-simple")
189
198
        << "  sb-simple : do not consider " << k << " at child arg " << arg
190
198
        << " of " << k
191
198
        << " since it is associative, with first arg = " << firstArg
192
198
        << std::endl;
193
198
    return false;
194
  }
195
  // describes the shape of an alternate term to construct
196
  //  we check whether this term is in the sygus grammar below
197
9120
  ReqTrie rt;
198
4560
  Assert(rt.empty());
199
200
  // construct rt by cases
201
4560
  if (pk == NOT || pk == BITVECTOR_NOT || pk == UMINUS || pk == BITVECTOR_NEG)
202
  {
203
    // negation normal form
204
254
    if (pk == k)
205
    {
206
41
      rt.d_req_type = dt[c].getArgType(0);
207
    }
208
    else
209
    {
210
213
      Kind reqk = UNDEFINED_KIND;      // required kind for all children
211
426
      std::map<unsigned, Kind> reqkc;  // required kind for some children
212
213
      if (pk == NOT)
213
      {
214
139
        if (k == AND)
215
        {
216
33
          rt.d_req_kind = OR;
217
33
          reqk = NOT;
218
        }
219
106
        else if (k == OR)
220
        {
221
31
          rt.d_req_kind = AND;
222
31
          reqk = NOT;
223
        }
224
75
        else if (k == EQUAL)
225
        {
226
29
          rt.d_req_kind = XOR;
227
        }
228
46
        else if (k == XOR)
229
        {
230
4
          rt.d_req_kind = EQUAL;
231
        }
232
42
        else if (k == ITE)
233
        {
234
2
          rt.d_req_kind = ITE;
235
2
          reqkc[1] = NOT;
236
2
          reqkc[2] = NOT;
237
2
          rt.d_children[0].d_req_type = dt[c].getArgType(0);
238
        }
239
40
        else if (k == LEQ || k == GT)
240
        {
241
          //  (not (~ x y)) ----->  (~ (+ y 1) x)
242
20
          rt.d_req_kind = k;
243
20
          rt.d_children[0].d_req_kind = PLUS;
244
20
          rt.d_children[0].d_children[0].d_req_type = dt[c].getArgType(1);
245
40
          rt.d_children[0].d_children[1].d_req_const =
246
60
              NodeManager::currentNM()->mkConst(Rational(1));
247
20
          rt.d_children[1].d_req_type = dt[c].getArgType(0);
248
        }
249
20
        else if (k == LT || k == GEQ)
250
        {
251
          //  (not (~ x y)) ----->  (~ y (+ x 1))
252
          rt.d_req_kind = k;
253
          rt.d_children[0].d_req_type = dt[c].getArgType(1);
254
          rt.d_children[1].d_req_kind = PLUS;
255
          rt.d_children[1].d_children[0].d_req_type = dt[c].getArgType(0);
256
          rt.d_children[1].d_children[1].d_req_const =
257
              NodeManager::currentNM()->mkConst(Rational(1));
258
        }
259
      }
260
74
      else if (pk == BITVECTOR_NOT)
261
      {
262
44
        if (k == BITVECTOR_AND)
263
        {
264
4
          rt.d_req_kind = BITVECTOR_OR;
265
4
          reqk = BITVECTOR_NOT;
266
        }
267
40
        else if (k == BITVECTOR_OR)
268
        {
269
4
          rt.d_req_kind = BITVECTOR_AND;
270
4
          reqk = BITVECTOR_NOT;
271
        }
272
36
        else if (k == BITVECTOR_XNOR)
273
        {
274
          rt.d_req_kind = BITVECTOR_XOR;
275
        }
276
36
        else if (k == BITVECTOR_XOR)
277
        {
278
4
          rt.d_req_kind = BITVECTOR_XNOR;
279
        }
280
      }
281
30
      else if (pk == UMINUS)
282
      {
283
        if (k == PLUS)
284
        {
285
          rt.d_req_kind = PLUS;
286
          reqk = UMINUS;
287
        }
288
      }
289
30
      else if (pk == BITVECTOR_NEG)
290
      {
291
30
        if (k == PLUS)
292
        {
293
          rt.d_req_kind = PLUS;
294
          reqk = BITVECTOR_NEG;
295
        }
296
      }
297
213
      if (!rt.empty() && (reqk != UNDEFINED_KIND || !reqkc.empty()))
298
      {
299
74
        int pcr = pti.getKindConsNum(rt.d_req_kind);
300
74
        if (pcr != -1)
301
        {
302
68
          Assert(pcr < static_cast<int>(pdt.getNumConstructors()));
303
          // must have same number of arguments
304
68
          if (pdt[pcr].getNumArgs() == dt[c].getNumArgs())
305
          {
306
206
            for (unsigned i = 0, nargs = pdt[pcr].getNumArgs(); i < nargs; i++)
307
            {
308
138
              Kind rk = reqk;
309
138
              if (reqk == UNDEFINED_KIND)
310
              {
311
6
                std::map<unsigned, Kind>::iterator itr = reqkc.find(i);
312
6
                if (itr != reqkc.end())
313
                {
314
4
                  rk = itr->second;
315
                }
316
              }
317
138
              if (rk != UNDEFINED_KIND)
318
              {
319
136
                rt.d_children[i].d_req_kind = rk;
320
136
                rt.d_children[i].d_children[0].d_req_type = dt[c].getArgType(i);
321
              }
322
            }
323
          }
324
        }
325
      }
326
254
    }
327
  }
328
4306
  else if (k == MINUS || k == BITVECTOR_SUB)
329
  {
330
620
    if (pk == EQUAL || pk == MINUS || pk == BITVECTOR_SUB || pk == LEQ
331
282
        || pk == LT || pk == GEQ || pk == GT)
332
    {
333
338
      int oarg = arg == 0 ? 1 : 0;
334
      //  (~ x (- y z))  ---->  (~ (+ x z) y)
335
      //  (~ (- y z) x)  ---->  (~ y (+ x z))
336
338
      rt.d_req_kind = pk;
337
338
      rt.d_children[arg].d_req_type = dt[c].getArgType(0);
338
338
      rt.d_children[oarg].d_req_kind = k == MINUS ? PLUS : BITVECTOR_PLUS;
339
338
      rt.d_children[oarg].d_children[0].d_req_type = pdt[pc].getArgType(oarg);
340
338
      rt.d_children[oarg].d_children[1].d_req_type = dt[c].getArgType(1);
341
    }
342
282
    else if (pk == PLUS || pk == BITVECTOR_PLUS)
343
    {
344
      //  (+ x (- y z))  -----> (- (+ x y) z)
345
      //  (+ (- y z) x)  -----> (- (+ x y) z)
346
126
      rt.d_req_kind = pk == PLUS ? MINUS : BITVECTOR_SUB;
347
126
      int oarg = arg == 0 ? 1 : 0;
348
126
      rt.d_children[0].d_req_kind = pk;
349
126
      rt.d_children[0].d_children[0].d_req_type = pdt[pc].getArgType(oarg);
350
126
      rt.d_children[0].d_children[1].d_req_type = dt[c].getArgType(0);
351
126
      rt.d_children[1].d_req_type = dt[c].getArgType(1);
352
620
    }
353
  }
354
3686
  else if (k == ITE)
355
  {
356
706
    if (pk != ITE)
357
    {
358
      //  (o X (ite y z w) X')  -----> (ite y (o X z X') (o X w X'))
359
564
      rt.d_req_kind = ITE;
360
564
      rt.d_children[0].d_req_type = dt[c].getArgType(0);
361
564
      unsigned n_args = pdt[pc].getNumArgs();
362
1692
      for (unsigned r = 1; r <= 2; r++)
363
      {
364
1128
        rt.d_children[r].d_req_kind = pk;
365
3388
        for (unsigned q = 0; q < n_args; q++)
366
        {
367
2260
          if ((int)q == arg)
368
          {
369
1128
            rt.d_children[r].d_children[q].d_req_type = dt[c].getArgType(r);
370
          }
371
          else
372
          {
373
1132
            rt.d_children[r].d_children[q].d_req_type = pdt[pc].getArgType(q);
374
          }
375
        }
376
      }
377
      // this increases term size but is probably a good idea
378
    }
379
  }
380
2980
  else if (k == NOT)
381
  {
382
242
    if (pk == ITE)
383
    {
384
      //  (ite (not y) z w)  -----> (ite y w z)
385
62
      rt.d_req_kind = ITE;
386
62
      rt.d_children[0].d_req_type = dt[c].getArgType(0);
387
62
      rt.d_children[1].d_req_type = pdt[pc].getArgType(2);
388
62
      rt.d_children[2].d_req_type = pdt[pc].getArgType(1);
389
    }
390
  }
391
9120
  Trace("sygus-sb-debug") << "Consider sygus arg kind " << k << ", pk = " << pk
392
4560
                          << ", arg = " << arg << "?" << std::endl;
393
4560
  if (!rt.empty())
394
  {
395
1262
    rt.print("sygus-sb-debug");
396
    // check if it meets the requirements
397
1262
    if (rt.satisfiedBy(d_tds, tnp))
398
    {
399
1153
      Trace("sygus-sb-debug") << "...success!" << std::endl;
400
2306
      Trace("sygus-sb-simple")
401
1153
          << "  sb-simple : do not consider " << k << " as arg " << arg
402
1153
          << " of " << pk << std::endl;
403
      // do not need to consider the kind in the search since there are ways to
404
      // construct equivalent terms
405
1153
      return false;
406
    }
407
    else
408
    {
409
109
      Trace("sygus-sb-debug") << "...failed." << std::endl;
410
    }
411
109
    Trace("sygus-sb-debug") << std::endl;
412
  }
413
  // must consider this kind in the search
414
3407
  return true;
415
}
416
417
1916
bool SygusSimpleSymBreak::considerConst(
418
    TypeNode tn, TypeNode tnp, Node c, Kind pk, int arg)
419
{
420
1916
  const DType& pdt = tnp.getDType();
421
  // child grammar-independent
422
1916
  if (!considerConst(pdt, tnp, c, pk, arg))
423
  {
424
592
    return false;
425
  }
426
  // this can probably be made child grammar independent
427
1324
  quantifiers::SygusTypeInfo& ti = d_tds->getTypeInfo(tn);
428
1324
  quantifiers::SygusTypeInfo& pti = d_tds->getTypeInfo(tnp);
429
1324
  int pc = pti.getKindConsNum(pk);
430
1324
  if (pdt[pc].getNumArgs() == 2)
431
  {
432
    Kind ok;
433
    int offset;
434
1012
    if (quantifiers::TermUtil::hasOffsetArg(pk, arg, offset, ok))
435
    {
436
88
      Trace("sygus-sb-simple-debug")
437
44
          << pk << " has offset arg " << ok << " " << offset << std::endl;
438
44
      int ok_arg = pti.getKindConsNum(ok);
439
44
      if (ok_arg != -1)
440
      {
441
16
        Trace("sygus-sb-simple-debug")
442
8
            << "...at argument " << ok_arg << std::endl;
443
        // other operator be the same type
444
8
        if (d_tds->isTypeMatch(pdt[ok_arg], pdt[arg]))
445
        {
446
          int status;
447
          Node co = quantifiers::TermUtil::mkTypeValueOffset(
448
12
              c.getType(), c, offset, status);
449
16
          Trace("sygus-sb-simple-debug")
450
8
              << c << " with offset " << offset << " is " << co
451
8
              << ", status=" << status << std::endl;
452
8
          if (status == 0 && !co.isNull())
453
          {
454
8
            if (ti.hasConst(co))
455
            {
456
8
              Trace("sygus-sb-simple")
457
4
                  << "  sb-simple : by offset reasoning, do not consider const "
458
4
                  << c;
459
8
              Trace("sygus-sb-simple")
460
4
                  << " as arg " << arg << " of " << pk << " since we can use "
461
4
                  << co << " under " << ok << " " << std::endl;
462
4
              return false;
463
            }
464
          }
465
        }
466
      }
467
    }
468
  }
469
1320
  return true;
470
}
471
472
1916
bool SygusSimpleSymBreak::considerConst(
473
    const DType& pdt, TypeNode tnp, Node c, Kind pk, int arg)
474
{
475
1916
  quantifiers::SygusTypeInfo& pti = d_tds->getTypeInfo(tnp);
476
1916
  Assert(pti.hasKind(pk));
477
1916
  int pc = pti.getKindConsNum(pk);
478
1916
  bool ret = true;
479
3832
  Trace("sygus-sb-debug") << "Consider sygus const " << c << ", parent = " << pk
480
1916
                          << ", arg = " << arg << "?" << std::endl;
481
1916
  if (quantifiers::TermUtil::isIdempotentArg(c, pk, arg))
482
  {
483
308
    if (pdt[pc].getNumArgs() == 2)
484
    {
485
308
      int oarg = arg == 0 ? 1 : 0;
486
616
      TypeNode otn = pdt[pc].getArgType(oarg);
487
308
      if (otn == tnp)
488
      {
489
608
        Trace("sygus-sb-simple")
490
304
            << "  sb-simple : " << c << " is idempotent arg " << arg << " of "
491
304
            << pk << "..." << std::endl;
492
304
        ret = false;
493
      }
494
    }
495
  }
496
  else
497
  {
498
3216
    Node sc = quantifiers::TermUtil::isSingularArg(c, pk, arg);
499
1608
    if (!sc.isNull())
500
    {
501
194
      if (pti.hasConst(sc))
502
      {
503
368
        Trace("sygus-sb-simple")
504
184
            << "  sb-simple : " << c << " is singular arg " << arg << " of "
505
184
            << pk << ", evaluating to " << sc << "..." << std::endl;
506
184
        ret = false;
507
      }
508
    }
509
  }
510
1916
  if (ret)
511
  {
512
2856
    ReqTrie rt;
513
1428
    Assert(rt.empty());
514
2856
    Node max_c = quantifiers::TermUtil::mkTypeMaxValue(c.getType());
515
2856
    Node zero_c = quantifiers::TermUtil::mkTypeValue(c.getType(), 0);
516
2856
    Node one_c = quantifiers::TermUtil::mkTypeValue(c.getType(), 1);
517
1428
    if (pk == XOR || pk == BITVECTOR_XOR)
518
    {
519
16
      if (c == max_c)
520
      {
521
        rt.d_req_kind = pk == XOR ? NOT : BITVECTOR_NOT;
522
      }
523
    }
524
1420
    else if (pk == ITE)
525
    {
526
316
      if (arg == 0)
527
      {
528
104
        if (c == max_c)
529
        {
530
52
          rt.d_children[1].d_req_type = tnp;
531
        }
532
52
        else if (c == zero_c)
533
        {
534
52
          rt.d_children[2].d_req_type = tnp;
535
        }
536
      }
537
    }
538
1104
    else if (pk == STRING_SUBSTR)
539
    {
540
      if (c == one_c && arg == 2)
541
      {
542
        rt.d_req_kind = STRING_CHARAT;
543
        rt.d_children[0].d_req_type = pdt[pc].getArgType(0);
544
        rt.d_children[1].d_req_type = pdt[pc].getArgType(1);
545
      }
546
    }
547
1428
    if (!rt.empty())
548
    {
549
      // check if satisfied
550
104
      if (rt.satisfiedBy(d_tds, tnp))
551
      {
552
208
        Trace("sygus-sb-simple") << "  sb-simple : do not consider const " << c
553
104
                                 << " as arg " << arg << " of " << pk;
554
104
        Trace("sygus-sb-simple") << " in " << pdt.getName() << std::endl;
555
        // do not need to consider the constant in the search since there are
556
        // ways to construct equivalent terms
557
104
        ret = false;
558
      }
559
    }
560
  }
561
1916
  return ret;
562
}
563
564
4351
int SygusSimpleSymBreak::solveForArgument(TypeNode tn,
565
                                          unsigned cindex,
566
                                          unsigned arg)
567
{
568
  // we currently do not solve for arguments
569
4351
  return -1;
570
}
571
572
416
int SygusSimpleSymBreak::getFirstArgOccurrence(const DTypeConstructor& c,
573
                                               TypeNode tn)
574
{
575
416
  for (unsigned i = 0, nargs = c.getNumArgs(); i < nargs; i++)
576
  {
577
416
    if (c.getArgType(i) == tn)
578
    {
579
416
      return i;
580
    }
581
  }
582
  return -1;
583
}
584
585
}  // namespace datatypes
586
}  // namespace theory
587
26676
}  // namespace CVC4