GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/term_util.cpp Lines: 264 311 84.9 %
Date: 2021-03-22 Branches: 567 1022 55.5 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file term_util.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Mathias Preiner, Morgan Deters
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 term utilities class
13
 **/
14
15
#include "theory/quantifiers/term_util.h"
16
17
#include "expr/node_algorithm.h"
18
#include "options/base_options.h"
19
#include "options/datatypes_options.h"
20
#include "options/quantifiers_options.h"
21
#include "options/uf_options.h"
22
#include "theory/arith/arith_msum.h"
23
#include "theory/bv/theory_bv_utils.h"
24
#include "theory/quantifiers/term_database.h"
25
#include "theory/quantifiers/term_enumeration.h"
26
#include "theory/quantifiers_engine.h"
27
#include "theory/strings/word.h"
28
#include "theory/rewriter.h"
29
30
using namespace std;
31
using namespace CVC4::kind;
32
using namespace CVC4::context;
33
using namespace CVC4::theory::inst;
34
35
namespace CVC4 {
36
namespace theory {
37
namespace quantifiers {
38
39
4433
size_t TermUtil::getVariableNum(Node q, Node v)
40
{
41
4433
  Node::iterator it = std::find(q[0].begin(), q[0].end(), v);
42
4433
  Assert(it != q[0].end());
43
4433
  return it - q[0].begin();
44
}
45
46
25984
Node TermUtil::getRemoveQuantifiers2( Node n, std::map< Node, Node >& visited ) {
47
25984
  std::map< Node, Node >::iterator it = visited.find( n );
48
25984
  if( it!=visited.end() ){
49
11824
    return it->second;
50
  }else{
51
28320
    Node ret = n;
52
14160
    if( n.getKind()==FORALL ){
53
583
      ret = getRemoveQuantifiers2( n[1], visited );
54
13577
    }else if( n.getNumChildren()>0 ){
55
20638
      std::vector< Node > children;
56
10319
      bool childrenChanged = false;
57
35127
      for( unsigned i=0; i<n.getNumChildren(); i++ ){
58
49616
        Node ni = getRemoveQuantifiers2( n[i], visited );
59
24808
        childrenChanged = childrenChanged || ni!=n[i];
60
24808
        children.push_back( ni );
61
      }
62
10319
      if( childrenChanged ){
63
6
        if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
64
          children.insert( children.begin(), n.getOperator() );
65
        }
66
6
        ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
67
      }
68
    }
69
14160
    visited[n] = ret;
70
14160
    return ret;
71
  }
72
}
73
74
12335193
Node TermUtil::getInstConstAttr( Node n ) {
75
12335193
  if (!n.hasAttribute(InstConstantAttribute()) ){
76
837790
    Node q;
77
418895
    if (n.hasOperator())
78
    {
79
307466
      q = getInstConstAttr(n.getOperator());
80
    }
81
418895
    if (q.isNull())
82
    {
83
868896
      for (const Node& nc : n)
84
      {
85
548679
        q = getInstConstAttr(nc);
86
548679
        if (!q.isNull())
87
        {
88
98614
          break;
89
        }
90
      }
91
    }
92
    InstConstantAttribute ica;
93
418895
    n.setAttribute(ica, q);
94
  }
95
12335193
  return n.getAttribute(InstConstantAttribute());
96
}
97
98
8015661
bool TermUtil::hasInstConstAttr( Node n ) {
99
8015661
  return !getInstConstAttr(n).isNull();
100
}
101
102
148137
Node TermUtil::getBoundVarAttr( Node n ) {
103
148137
  if (!n.hasAttribute(BoundVarAttribute()) ){
104
151100
    Node bv;
105
75550
    if( n.getKind()==BOUND_VARIABLE ){
106
7398
      bv = n;
107
    }else{
108
89805
      for( unsigned i=0; i<n.getNumChildren(); i++ ){
109
75796
        bv = getBoundVarAttr(n[i]);
110
75796
        if( !bv.isNull() ){
111
54143
          break;
112
        }
113
      }
114
    }
115
    BoundVarAttribute bva;
116
75550
    n.setAttribute(bva, bv);
117
  }
118
148137
  return n.getAttribute(BoundVarAttribute());
119
}
120
121
72341
bool TermUtil::hasBoundVarAttr( Node n ) {
122
72341
  return !getBoundVarAttr(n).isNull();
123
}
124
125
//remove quantifiers
126
593
Node TermUtil::getRemoveQuantifiers( Node n ) {
127
1186
  std::map< Node, Node > visited;
128
1186
  return getRemoveQuantifiers2( n, visited );
129
}
130
131
//quantified simplify
132
1571
Node TermUtil::getQuantSimplify( Node n ) {
133
3142
  std::unordered_set<Node, NodeHashFunction> fvs;
134
1571
  expr::getFreeVariables(n, fvs);
135
1571
  if (fvs.empty())
136
  {
137
978
    return Rewriter::rewrite( n );
138
  }
139
1186
  std::vector<Node> bvs;
140
593
  bvs.insert(bvs.end(), fvs.begin(), fvs.end());
141
593
  NodeManager* nm = NodeManager::currentNM();
142
1186
  Node q = nm->mkNode(FORALL, nm->mkNode(BOUND_VAR_LIST, bvs), n);
143
593
  q = Rewriter::rewrite(q);
144
593
  return getRemoveQuantifiers(q);
145
}
146
147
156886
void TermUtil::computeInstConstContains(Node n, std::vector<Node>& ics)
148
{
149
156886
  computeVarContainsInternal(n, INST_CONSTANT, ics);
150
156886
}
151
152
224
void TermUtil::computeVarContains(Node n, std::vector<Node>& vars)
153
{
154
224
  computeVarContainsInternal(n, BOUND_VARIABLE, vars);
155
224
}
156
157
1731
void TermUtil::computeQuantContains(Node n, std::vector<Node>& quants)
158
{
159
1731
  computeVarContainsInternal(n, FORALL, quants);
160
1731
}
161
162
158841
void TermUtil::computeVarContainsInternal(Node n,
163
                                          Kind k,
164
                                          std::vector<Node>& vars)
165
{
166
317682
  std::unordered_set<TNode, TNodeHashFunction> visited;
167
158841
  std::unordered_set<TNode, TNodeHashFunction>::iterator it;
168
317682
  std::vector<TNode> visit;
169
317682
  TNode cur;
170
158841
  visit.push_back(n);
171
1249746
  do
172
  {
173
1408587
    cur = visit.back();
174
1408587
    visit.pop_back();
175
1408587
    it = visited.find(cur);
176
177
1408587
    if (it == visited.end())
178
    {
179
1255459
      visited.insert(cur);
180
1255459
      if (cur.getKind() == k)
181
      {
182
368633
        if (std::find(vars.begin(), vars.end(), cur) == vars.end())
183
        {
184
368633
          vars.push_back(cur);
185
        }
186
      }
187
      else
188
      {
189
886826
        if (cur.hasOperator())
190
        {
191
414010
          visit.push_back(cur.getOperator());
192
        }
193
1722562
        for (const Node& cn : cur)
194
        {
195
835736
          visit.push_back(cn);
196
        }
197
      }
198
    }
199
1408587
  } while (!visit.empty());
200
158841
}
201
202
108944
void TermUtil::computeInstConstContainsForQuant(Node q,
203
                                                Node n,
204
                                                std::vector<Node>& vars)
205
{
206
217888
  std::vector<Node> ics;
207
108944
  computeInstConstContains(n, ics);
208
367235
  for (const Node& v : ics)
209
  {
210
258291
    if (v.getAttribute(InstConstantAttribute()) == q)
211
    {
212
258291
      if (std::find(vars.begin(), vars.end(), v) == vars.end())
213
      {
214
258291
        vars.push_back(v);
215
      }
216
    }
217
  }
218
108944
}
219
220
int TermUtil::getTermDepth( Node n ) {
221
  if (!n.hasAttribute(TermDepthAttribute()) ){
222
    int maxDepth = -1;
223
    for( unsigned i=0; i<n.getNumChildren(); i++ ){
224
      int depth = getTermDepth( n[i] );
225
      if( depth>maxDepth ){
226
        maxDepth = depth;
227
      }
228
    }
229
    TermDepthAttribute tda;
230
    n.setAttribute(tda,1+maxDepth);
231
  }
232
  return n.getAttribute(TermDepthAttribute());
233
}
234
235
685722
bool TermUtil::containsUninterpretedConstant( Node n ) {
236
685722
  if (!n.hasAttribute(ContainsUConstAttribute()) ){
237
22460
    bool ret = false;
238
22460
    if( n.getKind()==UNINTERPRETED_CONSTANT ){
239
782
      ret = true;
240
    }else{
241
42011
      for( unsigned i=0; i<n.getNumChildren(); i++ ){
242
20333
        if( containsUninterpretedConstant( n[i] ) ){
243
          ret = true;
244
          break;
245
        }
246
      }
247
    }
248
    ContainsUConstAttribute cuca;
249
22460
    n.setAttribute(cuca, ret ? 1 : 0);
250
  }
251
685722
  return n.getAttribute(ContainsUConstAttribute())!=0;
252
}
253
254
10068
Node TermUtil::simpleNegate(Node n)
255
{
256
10068
  Assert(n.getType().isBoolean());
257
10068
  NodeManager* nm = NodeManager::currentNM();
258
10068
  if( n.getKind()==OR || n.getKind()==AND ){
259
6318
    std::vector< Node > children;
260
11823
    for (const Node& cn : n)
261
    {
262
8664
      children.push_back(simpleNegate(cn));
263
    }
264
3159
    return nm->mkNode(n.getKind() == OR ? AND : OR, children);
265
  }
266
6909
  else if (n.isConst())
267
  {
268
127
    return nm->mkConst(!n.getConst<bool>());
269
  }
270
6782
  return n.negate();
271
}
272
273
1555
Node TermUtil::mkNegate(Kind notk, Node n)
274
{
275
1555
  if (n.getKind() == notk)
276
  {
277
26
    return n[0];
278
  }
279
1529
  return NodeManager::currentNM()->mkNode(notk, n);
280
}
281
282
4796
bool TermUtil::isNegate(Kind k)
283
{
284
4796
  return k == NOT || k == BITVECTOR_NOT || k == BITVECTOR_NEG || k == UMINUS;
285
}
286
287
138809
bool TermUtil::isAssoc(Kind k, bool reqNAry)
288
{
289
138809
  if (reqNAry)
290
  {
291
137869
    if (k == UNION || k == INTERSECTION)
292
    {
293
74
      return false;
294
    }
295
  }
296
119858
  return k == PLUS || k == MULT || k == NONLINEAR_MULT || k == AND || k == OR
297
101180
         || k == XOR || k == BITVECTOR_PLUS || k == BITVECTOR_MULT
298
92469
         || k == BITVECTOR_AND || k == BITVECTOR_OR || k == BITVECTOR_XOR
299
81838
         || k == BITVECTOR_XNOR || k == BITVECTOR_CONCAT || k == STRING_CONCAT
300
79544
         || k == UNION || k == INTERSECTION || k == JOIN || k == PRODUCT
301
218271
         || k == SEP_STAR;
302
}
303
304
411682
bool TermUtil::isComm(Kind k, bool reqNAry)
305
{
306
411682
  if (reqNAry)
307
  {
308
    if (k == UNION || k == INTERSECTION)
309
    {
310
      return false;
311
    }
312
  }
313
346042
  return k == EQUAL || k == PLUS || k == MULT || k == NONLINEAR_MULT || k == AND
314
285282
         || k == OR || k == XOR || k == BITVECTOR_PLUS || k == BITVECTOR_MULT
315
253178
         || k == BITVECTOR_AND || k == BITVECTOR_OR || k == BITVECTOR_XOR
316
242022
         || k == BITVECTOR_XNOR || k == UNION || k == INTERSECTION
317
653566
         || k == SEP_STAR;
318
}
319
320
138159
bool TermUtil::isNonAdditive( Kind k ) {
321
138159
  return k==AND || k==OR || k==BITVECTOR_AND || k==BITVECTOR_OR;
322
}
323
324
325868
bool TermUtil::isBoolConnective( Kind k ) {
325
325868
  return k==OR || k==AND || k==EQUAL || k==ITE || k==FORALL || k==NOT || k==SEP_STAR;
326
}
327
328
274311
bool TermUtil::isBoolConnectiveTerm( TNode n ) {
329
469755
  return isBoolConnective( n.getKind() ) &&
330
1143626
         ( n.getKind()!=EQUAL || n[0].getType().isBoolean() ) &&
331
665513
         ( n.getKind()!=ITE || n.getType().isBoolean() );
332
}
333
334
21897
Node TermUtil::mkTypeValue(TypeNode tn, int32_t val)
335
{
336
21897
  Node n;
337
21897
  if (tn.isInteger() || tn.isReal())
338
  {
339
9706
    Rational c(val);
340
4853
    n = NodeManager::currentNM()->mkConst(c);
341
  }
342
17044
  else if (tn.isBitVector())
343
  {
344
    // cast to unsigned
345
1491
    uint32_t uv = static_cast<uint32_t>(val);
346
2982
    BitVector bval(tn.getConst<BitVectorSize>(), uv);
347
1491
    n = NodeManager::currentNM()->mkConst<BitVector>(bval);
348
  }
349
15553
  else if (tn.isBoolean())
350
  {
351
15073
    if (val == 0)
352
    {
353
14401
      n = NodeManager::currentNM()->mkConst(false);
354
    }
355
  }
356
480
  else if (tn.isStringLike())
357
  {
358
300
    if (val == 0)
359
    {
360
174
      n = strings::Word::mkEmptyWord(tn);
361
    }
362
  }
363
21897
  return n;
364
}
365
366
15512
Node TermUtil::mkTypeMaxValue(TypeNode tn)
367
{
368
15512
  Node n;
369
15512
  if (tn.isBitVector())
370
  {
371
396
    n = bv::utils::mkOnes(tn.getConst<BitVectorSize>());
372
  }
373
15116
  else if (tn.isBoolean())
374
  {
375
14028
    n = NodeManager::currentNM()->mkConst(true);
376
  }
377
15512
  return n;
378
}
379
380
8
Node TermUtil::mkTypeValueOffset(TypeNode tn,
381
                                 Node val,
382
                                 int32_t offset,
383
                                 int32_t& status)
384
{
385
8
  Node val_o;
386
16
  Node offset_val = mkTypeValue(tn, offset);
387
8
  status = -1;
388
8
  if (!offset_val.isNull())
389
  {
390
8
    if (tn.isInteger() || tn.isReal())
391
    {
392
8
      val_o = Rewriter::rewrite(
393
16
          NodeManager::currentNM()->mkNode(PLUS, val, offset_val));
394
8
      status = 0;
395
    }
396
    else if (tn.isBitVector())
397
    {
398
      val_o = Rewriter::rewrite(
399
          NodeManager::currentNM()->mkNode(BITVECTOR_PLUS, val, offset_val));
400
    }
401
  }
402
16
  return val_o;
403
}
404
405
2
Node TermUtil::mkTypeConst(TypeNode tn, bool pol)
406
{
407
2
  return pol ? mkTypeMaxValue(tn) : mkTypeValue(tn, 0);
408
}
409
410
bool TermUtil::isAntisymmetric(Kind k, Kind& dk)
411
{
412
  if (k == GT)
413
  {
414
    dk = LT;
415
    return true;
416
  }
417
  else if (k == GEQ)
418
  {
419
    dk = LEQ;
420
    return true;
421
  }
422
  else if (k == BITVECTOR_UGT)
423
  {
424
    dk = BITVECTOR_ULT;
425
    return true;
426
  }
427
  else if (k == BITVECTOR_UGE)
428
  {
429
    dk = BITVECTOR_ULE;
430
    return true;
431
  }
432
  else if (k == BITVECTOR_SGT)
433
  {
434
    dk = BITVECTOR_SLT;
435
    return true;
436
  }
437
  else if (k == BITVECTOR_SGE)
438
  {
439
    dk = BITVECTOR_SLE;
440
    return true;
441
  }
442
  return false;
443
}
444
445
1916
bool TermUtil::isIdempotentArg(Node n, Kind ik, int arg)
446
{
447
  // these should all be binary operators
448
  // Assert( ik!=DIVISION && ik!=INTS_DIVISION && ik!=INTS_MODULUS &&
449
  // ik!=BITVECTOR_UDIV );
450
3832
  TypeNode tn = n.getType();
451
1916
  if (n == mkTypeValue(tn, 0))
452
  {
453
927
    if (ik == PLUS || ik == OR || ik == XOR || ik == BITVECTOR_PLUS
454
725
        || ik == BITVECTOR_OR
455
717
        || ik == BITVECTOR_XOR
456
709
        || ik == STRING_CONCAT)
457
    {
458
230
      return true;
459
    }
460
697
    else if (ik == MINUS || ik == BITVECTOR_SHL || ik == BITVECTOR_LSHR
461
597
             || ik == BITVECTOR_ASHR || ik == BITVECTOR_SUB
462
589
             || ik == BITVECTOR_UREM)
463
    {
464
112
      return arg == 1;
465
    }
466
  }
467
989
  else if (n == mkTypeValue(tn, 1))
468
  {
469
628
    if (ik == MULT || ik == BITVECTOR_MULT)
470
    {
471
12
      return true;
472
    }
473
616
    else if (ik == DIVISION || ik == DIVISION_TOTAL || ik == INTS_DIVISION
474
608
             || ik == INTS_DIVISION_TOTAL
475
608
             || ik == INTS_MODULUS
476
608
             || ik == INTS_MODULUS_TOTAL
477
608
             || ik == BITVECTOR_UDIV
478
600
             || ik == BITVECTOR_SDIV)
479
    {
480
20
      return arg == 1;
481
    }
482
  }
483
361
  else if (n == mkTypeMaxValue(tn))
484
  {
485
225
    if (ik == EQUAL || ik == BITVECTOR_AND || ik == BITVECTOR_XNOR)
486
    {
487
      return true;
488
    }
489
  }
490
1542
  return false;
491
}
492
493
1608
Node TermUtil::isSingularArg(Node n, Kind ik, unsigned arg)
494
{
495
3216
  TypeNode tn = n.getType();
496
1608
  if (n == mkTypeValue(tn, 0))
497
  {
498
641
    if (ik == AND || ik == MULT || ik == BITVECTOR_AND || ik == BITVECTOR_MULT)
499
    {
500
82
      return n;
501
    }
502
559
    else if (ik == BITVECTOR_SHL || ik == BITVECTOR_LSHR || ik == BITVECTOR_ASHR
503
553
             || ik == BITVECTOR_UREM)
504
    {
505
8
      if (arg == 0)
506
      {
507
8
        return n;
508
      }
509
    }
510
551
    else if (ik == BITVECTOR_UDIV || ik == BITVECTOR_UDIV
511
543
             || ik == BITVECTOR_SDIV)
512
    {
513
12
      if (arg == 0)
514
      {
515
6
        return n;
516
      }
517
6
      else if (arg == 1)
518
      {
519
6
        return mkTypeMaxValue(tn);
520
      }
521
    }
522
539
    else if (ik == DIVISION || ik == DIVISION_TOTAL || ik == INTS_DIVISION
523
535
             || ik == INTS_DIVISION_TOTAL
524
535
             || ik == INTS_MODULUS
525
529
             || ik == INTS_MODULUS_TOTAL)
526
    {
527
14
      if (arg == 0)
528
      {
529
6
        return n;
530
      }
531
    }
532
529
    else if (ik == STRING_SUBSTR)
533
    {
534
      if (arg == 0)
535
      {
536
        return n;
537
      }
538
      else if (arg == 2)
539
      {
540
        return mkTypeValue(NodeManager::currentNM()->stringType(), 0);
541
      }
542
    }
543
529
    else if (ik == STRING_STRIDOF)
544
    {
545
      if (arg == 0 || arg == 1)
546
      {
547
        return mkTypeValue(NodeManager::currentNM()->integerType(), -1);
548
      }
549
    }
550
  }
551
967
  else if (n == mkTypeValue(tn, 1))
552
  {
553
606
    if (ik == BITVECTOR_UREM)
554
    {
555
4
      return mkTypeValue(tn, 0);
556
    }
557
  }
558
361
  else if (n == mkTypeMaxValue(tn))
559
  {
560
225
    if (ik == OR || ik == BITVECTOR_OR)
561
    {
562
82
      return n;
563
    }
564
  }
565
  else
566
  {
567
136
    if (n.getType().isReal() && n.getConst<Rational>().sgn() < 0)
568
    {
569
      // negative arguments
570
2
      if (ik == STRING_SUBSTR || ik == STRING_CHARAT)
571
      {
572
        return mkTypeValue(NodeManager::currentNM()->stringType(), 0);
573
      }
574
2
      else if (ik == STRING_STRIDOF)
575
      {
576
        Assert(arg == 2);
577
        return mkTypeValue(NodeManager::currentNM()->integerType(), -1);
578
      }
579
    }
580
  }
581
1414
  return Node::null();
582
}
583
584
1012
bool TermUtil::hasOffsetArg(Kind ik, int arg, int& offset, Kind& ok)
585
{
586
1012
  if (ik == LT)
587
  {
588
8
    Assert(arg == 0 || arg == 1);
589
8
    offset = arg == 0 ? 1 : -1;
590
8
    ok = LEQ;
591
8
    return true;
592
  }
593
1004
  else if (ik == BITVECTOR_ULT)
594
  {
595
18
    Assert(arg == 0 || arg == 1);
596
18
    offset = arg == 0 ? 1 : -1;
597
18
    ok = BITVECTOR_ULE;
598
18
    return true;
599
  }
600
986
  else if (ik == BITVECTOR_SLT)
601
  {
602
18
    Assert(arg == 0 || arg == 1);
603
18
    offset = arg == 0 ? 1 : -1;
604
18
    ok = BITVECTOR_SLE;
605
18
    return true;
606
  }
607
968
  return false;
608
}
609
610
}/* CVC4::theory::quantifiers namespace */
611
}/* CVC4::theory namespace */
612
26676
}/* CVC4 namespace */