GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/strings/term_registry.cpp Lines: 275 302 91.1 %
Date: 2021-03-22 Branches: 657 1392 47.2 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file term_registry.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Andres Noetzli, Tianyi Liang
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 registry for the theory of strings.
13
 **/
14
15
#include "theory/strings/term_registry.h"
16
17
#include "expr/attribute.h"
18
#include "options/smt_options.h"
19
#include "options/strings_options.h"
20
#include "smt/logic_exception.h"
21
#include "theory/rewriter.h"
22
#include "theory/strings/inference_manager.h"
23
#include "theory/strings/theory_strings_utils.h"
24
#include "theory/strings/word.h"
25
26
using namespace std;
27
using namespace CVC4::context;
28
using namespace CVC4::kind;
29
30
namespace CVC4 {
31
namespace theory {
32
namespace strings {
33
34
struct StringsProxyVarAttributeId
35
{
36
};
37
typedef expr::Attribute<StringsProxyVarAttributeId, bool>
38
    StringsProxyVarAttribute;
39
40
8995
TermRegistry::TermRegistry(SolverState& s,
41
                           SequencesStatistics& statistics,
42
8995
                           ProofNodeManager* pnm)
43
    : d_state(s),
44
      d_im(nullptr),
45
      d_statistics(statistics),
46
      d_hasStrCode(false),
47
      d_functionsTerms(s.getSatContext()),
48
8995
      d_inputVars(s.getUserContext()),
49
      d_preregisteredTerms(s.getSatContext()),
50
8995
      d_registeredTerms(s.getUserContext()),
51
8995
      d_registeredTypes(s.getUserContext()),
52
8995
      d_proxyVar(s.getUserContext()),
53
8995
      d_lengthLemmaTermsCache(s.getUserContext()),
54
      d_epg(pnm ? new EagerProofGenerator(
55
                      pnm,
56
962
                      s.getUserContext(),
57
962
                      "strings::TermRegistry::EagerProofGenerator")
58
55894
                : nullptr)
59
{
60
8995
  NodeManager* nm = NodeManager::currentNM();
61
8995
  d_zero = nm->mkConst(Rational(0));
62
8995
  d_one = nm->mkConst(Rational(1));
63
8995
  d_negOne = NodeManager::currentNM()->mkConst(Rational(-1));
64
8995
  d_cardSize = utils::getAlphabetCardinality();
65
8995
}
66
67
8992
TermRegistry::~TermRegistry() {}
68
69
8995
void TermRegistry::finishInit(InferenceManager* im) { d_im = im; }
70
71
20108
Node TermRegistry::eagerReduce(Node t, SkolemCache* sc)
72
{
73
20108
  NodeManager* nm = NodeManager::currentNM();
74
20108
  Node lemma;
75
20108
  Kind tk = t.getKind();
76
20108
  if (tk == STRING_TO_CODE)
77
  {
78
    // ite( str.len(s)==1, 0 <= str.code(s) < |A|, str.code(s)=-1 )
79
2106
    Node code_len = utils::mkNLength(t[0]).eqNode(nm->mkConst(Rational(1)));
80
2106
    Node code_eq_neg1 = t.eqNode(nm->mkConst(Rational(-1)));
81
    Node code_range = nm->mkNode(
82
        AND,
83
2106
        nm->mkNode(GEQ, t, nm->mkConst(Rational(0))),
84
2106
        nm->mkNode(
85
6318
            LT, t, nm->mkConst(Rational(utils::getAlphabetCardinality()))));
86
1053
    lemma = nm->mkNode(ITE, code_len, code_range, code_eq_neg1);
87
  }
88
19055
  else if (tk == STRING_STRIDOF)
89
  {
90
    // (and (>= (str.indexof x y n) (- 1)) (<= (str.indexof x y n) (str.len
91
    // x)))
92
286
    Node l = utils::mkNLength(t[0]);
93
429
    lemma = nm->mkNode(AND,
94
286
                       nm->mkNode(GEQ, t, nm->mkConst(Rational(-1))),
95
286
                       nm->mkNode(LEQ, t, l));
96
  }
97
18912
  else if (tk == STRING_STOI)
98
  {
99
    // (>= (str.to_int x) (- 1))
100
53
    lemma = nm->mkNode(GEQ, t, nm->mkConst(Rational(-1)));
101
  }
102
18859
  else if (tk == STRING_STRCTN)
103
  {
104
    // ite( (str.contains s r), (= s (str.++ sk1 r sk2)), (not (= s r)))
105
    Node sk1 =
106
3828
        sc->mkSkolemCached(t[0], t[1], SkolemCache::SK_FIRST_CTN_PRE, "sc1");
107
    Node sk2 =
108
3828
        sc->mkSkolemCached(t[0], t[1], SkolemCache::SK_FIRST_CTN_POST, "sc2");
109
1914
    lemma = t[0].eqNode(utils::mkNConcat(sk1, t[1], sk2));
110
1914
    lemma = nm->mkNode(ITE, t, lemma, t[0].eqNode(t[1]).notNode());
111
  }
112
20108
  return lemma;
113
}
114
115
8110
Node TermRegistry::lengthPositive(Node t)
116
{
117
8110
  NodeManager* nm = NodeManager::currentNM();
118
16220
  Node zero = nm->mkConst(Rational(0));
119
16220
  Node emp = Word::mkEmptyWord(t.getType());
120
16220
  Node tlen = nm->mkNode(STRING_LENGTH, t);
121
16220
  Node tlenEqZero = tlen.eqNode(zero);
122
16220
  Node tEqEmp = t.eqNode(emp);
123
16220
  Node caseEmpty = nm->mkNode(AND, tlenEqZero, tEqEmp);
124
16220
  Node caseNEmpty = nm->mkNode(GT, tlen, zero);
125
  // (or (and (= (str.len t) 0) (= t "")) (> (str.len t) 0))
126
16220
  return nm->mkNode(OR, caseEmpty, caseNEmpty);
127
}
128
129
105160
void TermRegistry::preRegisterTerm(TNode n)
130
{
131
105160
  if (d_preregisteredTerms.find(n) != d_preregisteredTerms.end())
132
  {
133
42708
    return;
134
  }
135
104368
  eq::EqualityEngine* ee = d_state.getEqualityEngine();
136
104368
  d_preregisteredTerms.insert(n);
137
208736
  Trace("strings-preregister")
138
104368
      << "TheoryString::preregister : " << n << std::endl;
139
  // check for logic exceptions
140
104368
  Kind k = n.getKind();
141
104368
  if (!options::stringExp())
142
  {
143
11401
    if (k == STRING_STRIDOF || k == STRING_ITOS || k == STRING_STOI
144
11401
        || k == STRING_STRREPL || k == STRING_SUBSTR || k == STRING_STRREPLALL
145
11401
        || k == SEQ_NTH || k == STRING_REPLACE_RE || k == STRING_REPLACE_RE_ALL
146
11401
        || k == STRING_STRCTN || k == STRING_LEQ || k == STRING_TOLOWER
147
11401
        || k == STRING_TOUPPER || k == STRING_REV || k == STRING_UPDATE)
148
    {
149
      std::stringstream ss;
150
      ss << "Term of kind " << k
151
         << " not supported in default mode, try --strings-exp";
152
      throw LogicException(ss.str());
153
    }
154
  }
155
104368
  if (k == EQUAL)
156
  {
157
39105
    if (n[0].getType().isRegExp())
158
    {
159
      std::stringstream ss;
160
      ss << "Equality between regular expressions is not supported";
161
      throw LogicException(ss.str());
162
    }
163
39105
    ee->addTriggerPredicate(n);
164
39105
    return;
165
  }
166
65263
  else if (k == STRING_IN_REGEXP)
167
  {
168
2019
    d_im->requirePhase(n, true);
169
2019
    ee->addTriggerPredicate(n);
170
2019
    ee->addTerm(n[0]);
171
2019
    ee->addTerm(n[1]);
172
2019
    return;
173
  }
174
63244
  else if (k == STRING_TO_CODE)
175
  {
176
1695
    d_hasStrCode = true;
177
  }
178
63244
  registerTerm(n, 0);
179
126488
  TypeNode tn = n.getType();
180
63244
  if (tn.isRegExp() && n.isVar())
181
  {
182
    std::stringstream ss;
183
    ss << "Regular expression variables are not supported.";
184
    throw LogicException(ss.str());
185
  }
186
63244
  if (tn.isString())  // string-only
187
  {
188
    // all characters of constants should fall in the alphabet
189
32268
    if (n.isConst())
190
    {
191
7114
      std::vector<unsigned> vec = n.getConst<String>().getVec();
192
14005
      for (unsigned u : vec)
193
      {
194
10448
        if (u >= d_cardSize)
195
        {
196
          std::stringstream ss;
197
          ss << "Characters in string \"" << n
198
             << "\" are outside of the given alphabet.";
199
          throw LogicException(ss.str());
200
        }
201
      }
202
    }
203
32268
    ee->addTerm(n);
204
  }
205
30976
  else if (tn.isBoolean())
206
  {
207
    // All kinds that we do congruence over that may return a Boolean go here
208
1595
    if (k==STRING_STRCTN || k == STRING_LEQ || k == SEQ_NTH)
209
    {
210
      // Get triggered for both equal and dis-equal
211
1593
      ee->addTriggerPredicate(n);
212
    }
213
  }
214
  else
215
  {
216
    // Function applications/predicates
217
29381
    ee->addTerm(n);
218
  }
219
  // Set d_functionsTerms stores all function applications that are
220
  // relevant to theory combination. Notice that this is a subset of
221
  // the applications whose kinds are function kinds in the equality
222
  // engine. This means it does not include applications of operators
223
  // like re.++, which is not a function kind in the equality engine.
224
  // Concatenation terms do not need to be considered here because
225
  // their arguments have string type and do not introduce any shared
226
  // terms.
227
63244
  if (n.hasOperator() && ee->isFunctionKind(k) && k != STRING_CONCAT)
228
  {
229
28884
    d_functionsTerms.push_back(n);
230
  }
231
63244
  if (options::stringFMF())
232
  {
233
11717
    if (tn.isStringLike())
234
    {
235
      // Our decision strategy will minimize the length of this term if it is a
236
      // variable but not an internally generated Skolem, or a term that does
237
      // not belong to this theory.
238
8570
      if (n.isVar() ? !d_skCache.isSkolem(n)
239
2455
                    : kindToTheoryId(k) != THEORY_STRINGS)
240
      {
241
305
        d_inputVars.insert(n);
242
305
        Trace("strings-preregister") << "input variable: " << n << std::endl;
243
      }
244
    }
245
  }
246
}
247
248
114598
void TermRegistry::registerTerm(Node n, int effort)
249
{
250
229196
  Trace("strings-register") << "TheoryStrings::registerTerm() " << n
251
114598
                            << ", effort = " << effort << std::endl;
252
114598
  if (d_registeredTerms.find(n) != d_registeredTerms.end())
253
  {
254
74253
    Trace("strings-register") << "...already registered" << std::endl;
255
148506
    return;
256
  }
257
40345
  bool do_register = true;
258
80690
  TypeNode tn = n.getType();
259
40345
  if (!tn.isStringLike())
260
  {
261
19002
    if (options::stringEagerLen())
262
    {
263
19002
      do_register = effort == 0;
264
    }
265
    else
266
    {
267
      do_register = effort > 0 || n.getKind() != STRING_CONCAT;
268
    }
269
  }
270
40345
  if (!do_register)
271
  {
272
    Trace("strings-register") << "...do not register" << std::endl;
273
    return;
274
  }
275
40345
  Trace("strings-register") << "...register" << std::endl;
276
40345
  d_registeredTerms.insert(n);
277
  // ensure the type is registered
278
40345
  registerType(tn);
279
80690
  TrustNode regTermLem;
280
40345
  if (tn.isStringLike())
281
  {
282
    // register length information:
283
    //  for variables, split on empty vs positive length
284
    //  for concat/const/replace, introduce proxy var and state length relation
285
21343
    regTermLem = getRegisterTermLemma(n);
286
  }
287
19002
  else if (n.getKind() != STRING_STRCTN)
288
  {
289
    // we don't send out eager reduction lemma for str.contains currently
290
36204
    Node eagerRedLemma = eagerReduce(n, &d_skCache);
291
18102
    if (!eagerRedLemma.isNull())
292
    {
293
      // if there was an eager reduction, we make the trust node for it
294
1157
      if (d_epg != nullptr)
295
      {
296
184
        regTermLem = d_epg->mkTrustNode(
297
92
            eagerRedLemma, PfRule::STRING_EAGER_REDUCTION, {}, {n});
298
      }
299
      else
300
      {
301
1065
        regTermLem = TrustNode::mkTrustLemma(eagerRedLemma, nullptr);
302
      }
303
    }
304
  }
305
40345
  if (!regTermLem.isNull())
306
  {
307
16272
    Trace("strings-lemma") << "Strings::Lemma REG-TERM : " << regTermLem
308
8136
                           << std::endl;
309
16272
    Trace("strings-assert")
310
8136
        << "(assert " << regTermLem.getNode() << ")" << std::endl;
311
8136
    d_im->trustedLemma(regTermLem, InferenceId::STRINGS_REGISTER_TERM);
312
  }
313
}
314
315
40345
void TermRegistry::registerType(TypeNode tn)
316
{
317
40345
  if (d_registeredTypes.find(tn) != d_registeredTypes.end())
318
  {
319
38409
    return;
320
  }
321
1936
  d_registeredTypes.insert(tn);
322
1936
  if (tn.isStringLike())
323
  {
324
    // preregister the empty word for the type
325
1584
    Node emp = Word::mkEmptyWord(tn);
326
792
    if (!d_state.hasTerm(emp))
327
    {
328
792
      preRegisterTerm(emp);
329
    }
330
  }
331
}
332
333
21343
TrustNode TermRegistry::getRegisterTermLemma(Node n)
334
{
335
21343
  Assert(n.getType().isStringLike());
336
21343
  NodeManager* nm = NodeManager::currentNM();
337
  // register length information:
338
  //  for variables, split on empty vs positive length
339
  //  for concat/const/replace, introduce proxy var and state length relation
340
42686
  Node lsum;
341
21343
  if (n.getKind() != STRING_CONCAT && !n.isConst())
342
  {
343
14628
    Node lsumb = nm->mkNode(STRING_LENGTH, n);
344
14496
    lsum = Rewriter::rewrite(lsumb);
345
    // can register length term if it does not rewrite
346
14496
    if (lsum == lsumb)
347
    {
348
14364
      registerTermAtomic(n, LENGTH_SPLIT);
349
14364
      return TrustNode::null();
350
    }
351
  }
352
13958
  Node sk = d_skCache.mkSkolemCached(n, SkolemCache::SK_PURIFY, "lsym");
353
  StringsProxyVarAttribute spva;
354
6979
  sk.setAttribute(spva, true);
355
13958
  Node eq = Rewriter::rewrite(sk.eqNode(n));
356
6979
  d_proxyVar[n] = sk;
357
  // If we are introducing a proxy for a constant or concat term, we do not
358
  // need to send lemmas about its length, since its length is already
359
  // implied.
360
6979
  if (n.isConst() || n.getKind() == STRING_CONCAT)
361
  {
362
    // do not send length lemma for sk.
363
6847
    registerTermAtomic(sk, LENGTH_IGNORE);
364
  }
365
13958
  Node skl = nm->mkNode(STRING_LENGTH, sk);
366
6979
  if (n.getKind() == STRING_CONCAT)
367
  {
368
7618
    std::vector<Node> nodeVec;
369
12848
    for (const Node& nc : n)
370
    {
371
9039
      if (nc.getAttribute(StringsProxyVarAttribute()))
372
      {
373
        Assert(d_proxyVarToLength.find(nc) != d_proxyVarToLength.end());
374
        nodeVec.push_back(d_proxyVarToLength[nc]);
375
      }
376
      else
377
      {
378
18078
        Node lni = nm->mkNode(STRING_LENGTH, nc);
379
9039
        nodeVec.push_back(lni);
380
      }
381
    }
382
3809
    lsum = nm->mkNode(PLUS, nodeVec);
383
3809
    lsum = Rewriter::rewrite(lsum);
384
  }
385
3170
  else if (n.isConst())
386
  {
387
3038
    lsum = nm->mkConst(Rational(Word::getLength(n)));
388
  }
389
6979
  Assert(!lsum.isNull());
390
6979
  d_proxyVarToLength[sk] = lsum;
391
13958
  Node ceq = Rewriter::rewrite(skl.eqNode(lsum));
392
393
13958
  Node ret = nm->mkNode(AND, eq, ceq);
394
395
  // it is a simple rewrite to justify this
396
6979
  if (d_epg != nullptr)
397
  {
398
569
    return d_epg->mkTrustNode(ret, PfRule::MACRO_SR_PRED_INTRO, {}, {ret});
399
  }
400
6410
  return TrustNode::mkTrustLemma(ret, nullptr);
401
}
402
403
22267
void TermRegistry::registerTermAtomic(Node n, LengthStatus s)
404
{
405
22267
  if (d_lengthLemmaTermsCache.find(n) != d_lengthLemmaTermsCache.end())
406
  {
407
22643
    return;
408
  }
409
14368
  d_lengthLemmaTermsCache.insert(n);
410
411
14368
  if (s == LENGTH_IGNORE)
412
  {
413
    // ignore it
414
6845
    return;
415
  }
416
15046
  std::map<Node, bool> reqPhase;
417
15046
  TrustNode lenLem = getRegisterTermAtomicLemma(n, s, reqPhase);
418
7523
  if (!lenLem.isNull())
419
  {
420
15038
    Trace("strings-lemma") << "Strings::Lemma REGISTER-TERM-ATOMIC : " << lenLem
421
7519
                           << std::endl;
422
15038
    Trace("strings-assert")
423
7519
        << "(assert " << lenLem.getNode() << ")" << std::endl;
424
7519
    d_im->trustedLemma(lenLem, InferenceId::STRINGS_REGISTER_TERM_ATOMIC);
425
  }
426
22417
  for (const std::pair<const Node, bool>& rp : reqPhase)
427
  {
428
14894
    d_im->requirePhase(rp.first, rp.second);
429
  }
430
}
431
432
28259
SkolemCache* TermRegistry::getSkolemCache() { return &d_skCache; }
433
434
6475
const context::CDList<TNode>& TermRegistry::getFunctionTerms() const
435
{
436
6475
  return d_functionsTerms;
437
}
438
439
61
const context::CDHashSet<Node, NodeHashFunction>& TermRegistry::getInputVars()
440
    const
441
{
442
61
  return d_inputVars;
443
}
444
445
9726
bool TermRegistry::hasStringCode() const { return d_hasStrCode; }
446
447
7523
TrustNode TermRegistry::getRegisterTermAtomicLemma(
448
    Node n, LengthStatus s, std::map<Node, bool>& reqPhase)
449
{
450
7523
  if (n.isConst())
451
  {
452
    // No need to send length for constant terms. This case may be triggered
453
    // for cases where the skolem cache automatically replaces a skolem by
454
    // a constant.
455
4
    return TrustNode::null();
456
  }
457
7519
  Assert(n.getType().isStringLike());
458
7519
  NodeManager* nm = NodeManager::currentNM();
459
15038
  Node n_len = nm->mkNode(kind::STRING_LENGTH, n);
460
15038
  Node emp = Word::mkEmptyWord(n.getType());
461
7519
  if (s == LENGTH_GEQ_ONE)
462
  {
463
16
    Node neq_empty = n.eqNode(emp).negate();
464
16
    Node len_n_gt_z = nm->mkNode(GT, n_len, d_zero);
465
16
    Node len_geq_one = nm->mkNode(AND, neq_empty, len_n_gt_z);
466
16
    Trace("strings-lemma") << "Strings::Lemma SK-GEQ-ONE : " << len_geq_one
467
8
                           << std::endl;
468
8
    Trace("strings-assert") << "(assert " << len_geq_one << ")" << std::endl;
469
8
    return TrustNode::mkTrustLemma(len_geq_one, nullptr);
470
  }
471
472
7511
  if (s == LENGTH_ONE)
473
  {
474
    Node len_one = n_len.eqNode(d_one);
475
    Trace("strings-lemma") << "Strings::Lemma SK-ONE : " << len_one
476
                           << std::endl;
477
    Trace("strings-assert") << "(assert " << len_one << ")" << std::endl;
478
    return TrustNode::mkTrustLemma(len_one, nullptr);
479
  }
480
7511
  Assert(s == LENGTH_SPLIT);
481
482
  // get the positive length lemma
483
15022
  Node lenLemma = lengthPositive(n);
484
  // split whether the string is empty
485
15022
  Node n_len_eq_z = n_len.eqNode(d_zero);
486
15022
  Node n_len_eq_z_2 = n.eqNode(emp);
487
15022
  Node case_empty = nm->mkNode(AND, n_len_eq_z, n_len_eq_z_2);
488
15022
  Node case_emptyr = Rewriter::rewrite(case_empty);
489
7511
  if (!case_emptyr.isConst())
490
  {
491
    // prefer trying the empty case first
492
    // notice that requirePhase must only be called on rewritten literals that
493
    // occur in the CNF stream.
494
7447
    n_len_eq_z = Rewriter::rewrite(n_len_eq_z);
495
7447
    Assert(!n_len_eq_z.isConst());
496
7447
    reqPhase[n_len_eq_z] = true;
497
7447
    n_len_eq_z_2 = Rewriter::rewrite(n_len_eq_z_2);
498
7447
    Assert(!n_len_eq_z_2.isConst());
499
7447
    reqPhase[n_len_eq_z_2] = true;
500
  }
501
  else
502
  {
503
    // If n = "" ---> true or len( n ) = 0 ----> true, then we expect that
504
    // n ---> "". Since this method is only called on non-constants n, it must
505
    // be that n = "" ^ len( n ) = 0 does not rewrite to true.
506
64
    Assert(!case_emptyr.getConst<bool>());
507
  }
508
509
7511
  if (d_epg != nullptr)
510
  {
511
599
    return d_epg->mkTrustNode(lenLemma, PfRule::STRING_LENGTH_POS, {}, {n});
512
  }
513
6912
  return TrustNode::mkTrustLemma(lenLemma, nullptr);
514
}
515
516
185649
Node TermRegistry::getSymbolicDefinition(Node n, std::vector<Node>& exp) const
517
{
518
185649
  if (n.getNumChildren() == 0)
519
  {
520
178822
    Node pn = getProxyVariableFor(n);
521
89411
    if (pn.isNull())
522
    {
523
12455
      return Node::null();
524
    }
525
153912
    Node eq = n.eqNode(pn);
526
76956
    eq = Rewriter::rewrite(eq);
527
76956
    if (std::find(exp.begin(), exp.end(), eq) == exp.end())
528
    {
529
75162
      exp.push_back(eq);
530
    }
531
76956
    return pn;
532
  }
533
192476
  std::vector<Node> children;
534
96238
  if (n.getMetaKind() == metakind::PARAMETERIZED)
535
  {
536
38
    children.push_back(n.getOperator());
537
  }
538
241391
  for (const Node& nc : n)
539
  {
540
160942
    if (n.getType().isRegExp())
541
    {
542
44340
      children.push_back(nc);
543
    }
544
    else
545
    {
546
217415
      Node ns = getSymbolicDefinition(nc, exp);
547
116602
      if (ns.isNull())
548
      {
549
15789
        return Node::null();
550
      }
551
      else
552
      {
553
100813
        children.push_back(ns);
554
      }
555
    }
556
  }
557
80449
  return NodeManager::currentNM()->mkNode(n.getKind(), children);
558
}
559
560
93505
Node TermRegistry::getProxyVariableFor(Node n) const
561
{
562
93505
  NodeNodeMap::const_iterator it = d_proxyVar.find(n);
563
93505
  if (it != d_proxyVar.end())
564
  {
565
80886
    return (*it).second;
566
  }
567
12619
  return Node::null();
568
}
569
570
3928
Node TermRegistry::ensureProxyVariableFor(Node n)
571
{
572
3928
  Node proxy = getProxyVariableFor(n);
573
3928
  if (proxy.isNull())
574
  {
575
164
    registerTerm(n, 0);
576
164
    proxy = getProxyVariableFor(n);
577
  }
578
3928
  Assert(!proxy.isNull());
579
3928
  return proxy;
580
}
581
582
43121
void TermRegistry::removeProxyEqs(Node n, std::vector<Node>& unproc) const
583
{
584
43121
  if (n.getKind() == AND)
585
  {
586
710
    for (const Node& nc : n)
587
    {
588
528
      removeProxyEqs(nc, unproc);
589
    }
590
364
    return;
591
  }
592
42939
  Trace("strings-subs-proxy") << "Input : " << n << std::endl;
593
85878
  Node ns = Rewriter::rewrite(n);
594
42939
  if (ns.getKind() == EQUAL)
595
  {
596
128625
    for (size_t i = 0; i < 2; i++)
597
    {
598
      // determine whether this side has a proxy variable
599
85750
      if (ns[i].getAttribute(StringsProxyVarAttribute()))
600
      {
601
2
        if (getProxyVariableFor(ns[1 - i]) == ns[i])
602
        {
603
          Trace("strings-subs-proxy")
604
              << "...trivial definition via " << ns[i] << std::endl;
605
          // it is a trivial equality, e.g. between a proxy variable
606
          // and its definition
607
          return;
608
        }
609
      }
610
    }
611
  }
612
42939
  if (!n.isConst() || !n.getConst<bool>())
613
  {
614
42927
    Trace("strings-subs-proxy") << "...unprocessed" << std::endl;
615
42927
    unproc.push_back(n);
616
  }
617
}
618
619
}  // namespace strings
620
}  // namespace theory
621
26676
}  // namespace CVC4