GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/datatypes/theory_datatypes.cpp Lines: 1075 1205 89.2 %
Date: 2021-03-22 Branches: 2515 5547 45.3 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_datatypes.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Morgan Deters, Tim King
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 the theory of datatypes
13
 **
14
 ** Implementation of the theory of datatypes.
15
 **/
16
#include "theory/datatypes/theory_datatypes.h"
17
18
#include <map>
19
#include <sstream>
20
21
#include "base/check.h"
22
#include "expr/dtype.h"
23
#include "expr/dtype_cons.h"
24
#include "expr/kind.h"
25
#include "expr/proof_node_manager.h"
26
#include "options/datatypes_options.h"
27
#include "options/quantifiers_options.h"
28
#include "options/smt_options.h"
29
#include "options/theory_options.h"
30
#include "smt/logic_exception.h"
31
#include "theory/datatypes/datatypes_rewriter.h"
32
#include "theory/datatypes/theory_datatypes_type_rules.h"
33
#include "theory/datatypes/theory_datatypes_utils.h"
34
#include "theory/logic_info.h"
35
#include "theory/quantifiers_engine.h"
36
#include "theory/rewriter.h"
37
#include "theory/theory_model.h"
38
#include "theory/theory_state.h"
39
#include "theory/type_enumerator.h"
40
#include "theory/valuation.h"
41
42
using namespace std;
43
using namespace CVC4::kind;
44
using namespace CVC4::context;
45
46
namespace CVC4 {
47
namespace theory {
48
namespace datatypes {
49
50
8995
TheoryDatatypes::TheoryDatatypes(Context* c,
51
                                 UserContext* u,
52
                                 OutputChannel& out,
53
                                 Valuation valuation,
54
                                 const LogicInfo& logicInfo,
55
8995
                                 ProofNodeManager* pnm)
56
    : Theory(THEORY_DATATYPES, c, u, out, valuation, logicInfo, pnm),
57
      d_term_sk(u),
58
      d_labels(c),
59
      d_selector_apps(c),
60
      d_collectTermsCache(c),
61
      d_collectTermsCacheU(u),
62
      d_functionTerms(c),
63
      d_singleton_eq(u),
64
      d_lemmas_produced_c(u),
65
      d_sygusExtension(nullptr),
66
      d_state(c, u, valuation),
67
      d_im(*this, d_state, pnm),
68
8995
      d_notify(d_im, *this)
69
{
70
71
8995
  d_true = NodeManager::currentNM()->mkConst( true );
72
8995
  d_zero = NodeManager::currentNM()->mkConst( Rational(0) );
73
8995
  d_dtfCounter = 0;
74
75
  // indicate we are using the default theory state object
76
8995
  d_theoryState = &d_state;
77
8995
  d_inferManager = &d_im;
78
79
8995
  ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr;
80
8995
  if (pc != nullptr)
81
  {
82
    // add checkers
83
962
    d_pchecker.registerTo(pc);
84
  }
85
8995
}
86
87
26976
TheoryDatatypes::~TheoryDatatypes() {
88
33244
  for(std::map< Node, EqcInfo* >::iterator i = d_eqc_info.begin(), iend = d_eqc_info.end();
89
33244
      i != iend; ++i){
90
24252
    EqcInfo* current = (*i).second;
91
24252
    Assert(current != NULL);
92
24252
    delete current;
93
  }
94
17984
}
95
96
8995
TheoryRewriter* TheoryDatatypes::getTheoryRewriter() { return &d_rewriter; }
97
98
8995
bool TheoryDatatypes::needsEqualityEngine(EeSetupInfo& esi)
99
{
100
8995
  esi.d_notify = &d_notify;
101
8995
  esi.d_name = "theory::datatypes::ee";
102
8995
  return true;
103
}
104
105
8995
void TheoryDatatypes::finishInit()
106
{
107
8995
  Assert(d_equalityEngine != nullptr);
108
  // The kinds we are treating as function application in congruence
109
8995
  d_equalityEngine->addFunctionKind(kind::APPLY_CONSTRUCTOR);
110
8995
  d_equalityEngine->addFunctionKind(kind::APPLY_SELECTOR_TOTAL);
111
8995
  d_equalityEngine->addFunctionKind(kind::APPLY_TESTER);
112
  // We could but don't do congruence for DT_SIZE and DT_HEIGHT_BOUND here.
113
  // It also could make sense in practice to do congruence for APPLY_UF, but
114
  // this is not done.
115
8995
  if (getQuantifiersEngine() && options::sygus())
116
  {
117
    quantifiers::TermDbSygus* tds =
118
2190
        getQuantifiersEngine()->getTermDatabaseSygus();
119
4380
    d_sygusExtension.reset(
120
2190
        new SygusExtension(d_state, d_im, tds, getDecisionManager()));
121
    // do congruence on evaluation functions
122
2190
    d_equalityEngine->addFunctionKind(kind::DT_SYGUS_EVAL);
123
  }
124
  // testers are not relevant for model building
125
8995
  d_valuation.setIrrelevantKind(APPLY_TESTER);
126
8995
}
127
128
3345227
TheoryDatatypes::EqcInfo* TheoryDatatypes::getOrMakeEqcInfo( TNode n, bool doMake ){
129
3345227
  if( !hasEqcInfo( n ) ){
130
578142
    if( doMake ){
131
      //add to labels
132
167284
      d_labels[ n ] = 0;
133
134
167284
      std::map< Node, EqcInfo* >::iterator eqc_i = d_eqc_info.find( n );
135
      EqcInfo* ei;
136
167284
      if( eqc_i != d_eqc_info.end() ){
137
143032
        ei = eqc_i->second;
138
      }else{
139
24252
        ei = new EqcInfo( getSatContext() );
140
24252
        d_eqc_info[n] = ei;
141
      }
142
167284
      if( n.getKind()==APPLY_CONSTRUCTOR ){
143
127444
        ei->d_constructor = n;
144
      }
145
146
      //add to selectors
147
167284
      d_selector_apps[n] = 0;
148
149
167284
      return ei;
150
    }else{
151
410858
      return NULL;
152
    }
153
  }else{
154
2767085
    std::map< Node, EqcInfo* >::iterator eqc_i = d_eqc_info.find( n );
155
2767085
    return (*eqc_i).second;
156
  }
157
}
158
159
681381
TNode TheoryDatatypes::getEqcConstructor( TNode r ) {
160
681381
  if( r.getKind()==APPLY_CONSTRUCTOR ){
161
424159
    return r;
162
  }else{
163
257222
    EqcInfo * ei = getOrMakeEqcInfo( r, false );
164
257222
    if( ei && !ei->d_constructor.get().isNull() ){
165
67802
      return ei->d_constructor.get();
166
    }else{
167
189420
      return r;
168
    }
169
  }
170
}
171
172
764390
bool TheoryDatatypes::preCheck(Effort level)
173
{
174
764390
  d_im.reset();
175
764390
  d_im.clearPending();
176
764390
  return false;
177
}
178
179
764390
void TheoryDatatypes::postCheck(Effort level)
180
{
181
  // Apply any last pending inferences, which may occur if the last processed
182
  // fact was an internal one and triggered further internal inferences.
183
764390
  d_im.process();
184
764390
  if (level == EFFORT_LAST_CALL)
185
  {
186
9652
    Assert(d_sygusExtension != nullptr);
187
9652
    d_sygusExtension->check();
188
9652
    return;
189
  }
190
1539556
  else if (level == EFFORT_FULL && !d_state.isInConflict()
191
784540
           && !d_im.hasSentLemma() && !d_valuation.needCheck())
192
  {
193
    //check for cycles
194
26612
    Assert(!d_im.hasPendingFact());
195
4
    do {
196
26616
      d_im.reset();
197
26616
      Trace("datatypes-proc") << "Check cycles..." << std::endl;
198
26616
      checkCycles();
199
26616
      Trace("datatypes-proc") << "...finish check cycles" << std::endl;
200
26616
      d_im.process();
201
26616
      if (d_state.isInConflict() || d_im.hasSentLemma())
202
      {
203
395
        return;
204
      }
205
26221
    } while (d_im.hasSentFact());
206
207
    //check for splits
208
26217
    Trace("datatypes-debug") << "Check for splits " << endl;
209
1238
    do {
210
27455
      d_im.reset();
211
54910
      std::map< TypeNode, Node > rec_singletons;
212
27455
      eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(d_equalityEngine);
213
1282573
      while( !eqcs_i.isFinished() ){
214
1256667
        Node n = (*eqcs_i);
215
        //TODO : avoid irrelevant (pre-registered but not asserted) terms here?
216
1256667
        TypeNode tn = n.getType();
217
629108
        if( tn.isDatatype() ){
218
178287
          Trace("datatypes-debug") << "Process equivalence class " << n << std::endl;
219
178287
          EqcInfo* eqc = getOrMakeEqcInfo( n );
220
          //if there are more than 1 possible constructors for eqc
221
178287
          if( !hasLabel( eqc, n ) ){
222
40430
            Trace("datatypes-debug") << "No constructor..." << std::endl;
223
79311
            TypeNode tt = tn;
224
40430
            const DType& dt = tt.getDType();
225
80860
            Trace("datatypes-debug")
226
80860
                << "Datatype " << dt.getName() << " is "
227
80860
                << dt.isInterpretedFinite(tt) << " "
228
40430
                << dt.isRecursiveSingleton(tt) << std::endl;
229
40430
            bool continueProc = true;
230
40430
            if( dt.isRecursiveSingleton( tt ) ){
231
8
              Trace("datatypes-debug") << "Check recursive singleton..." << std::endl;
232
              //handle recursive singleton case
233
8
              std::map< TypeNode, Node >::iterator itrs = rec_singletons.find( tn );
234
8
              if( itrs!=rec_singletons.end() ){
235
8
                Node eq = n.eqNode( itrs->second );
236
4
                if( d_singleton_eq.find( eq )==d_singleton_eq.end() ){
237
4
                  d_singleton_eq[eq] = true;
238
                  // get assumptions
239
4
                  bool success = true;
240
8
                  std::vector< Node > assumptions;
241
                  //if there is at least one uninterpreted sort occurring within the datatype and the logic is not quantified, add lemmas ensuring cardinality is more than one,
242
                  //  do not infer the equality if at least one sort was processed.
243
                  //otherwise, if the logic is quantified, under the assumption that all uninterpreted sorts have cardinality one,
244
                  //  infer the equality.
245
4
                  for( unsigned i=0; i<dt.getNumRecursiveSingletonArgTypes( tt ); i++ ){
246
                    TypeNode type = dt.getRecursiveSingletonArgType(tt, i);
247
                    if( getQuantifiersEngine() ){
248
                      // under the assumption that the cardinality of this type is one
249
                      Node a = getSingletonLemma(type, true);
250
                      assumptions.push_back( a.negate() );
251
                    }else{
252
                      success = false;
253
                      // assert that the cardinality of this type is more than one
254
                      getSingletonLemma(type, false);
255
                    }
256
                  }
257
4
                  if( success ){
258
8
                    Node assumption = n.eqNode(itrs->second);
259
4
                    assumptions.push_back(assumption);
260
8
                    Node lemma = assumptions.size()==1 ? assumptions[0] : NodeManager::currentNM()->mkNode( OR, assumptions );
261
4
                    Trace("dt-singleton") << "*************Singleton equality lemma " << lemma << std::endl;
262
4
                    d_im.lemma(lemma, InferenceId::DATATYPES_REC_SINGLETON_EQ);
263
                  }
264
                }
265
              }else{
266
4
                rec_singletons[tn] = n;
267
              }
268
              //do splitting for quantified logics (incomplete anyways)
269
8
              continueProc = ( getQuantifiersEngine()!=NULL );
270
            }
271
40430
            if( continueProc ){
272
40422
              Trace("datatypes-debug") << "Get possible cons..." << std::endl;
273
              //all other cases
274
79295
              std::vector< bool > pcons;
275
40422
              getPossibleCons( eqc, n, pcons );
276
              //check if we do not need to resolve the constructor type for this equivalence class.
277
              // this is if there are no selectors for this equivalence class, and its possible values are infinite,
278
              //  then do not split.
279
40422
              int consIndex = -1;
280
40422
              int fconsIndex = -1;
281
40422
              bool needSplit = true;
282
215022
              for( unsigned int j=0; j<pcons.size(); j++ ) {
283
174600
                if( pcons[j] ) {
284
172549
                  if( consIndex==-1 ){
285
40271
                    consIndex = j;
286
                  }
287
345098
                  Trace("datatypes-debug") << j << " compute finite..."
288
172549
                                           << std::endl;
289
172549
                  bool ifin = dt[j].isInterpretedFinite(tt);
290
345098
                  Trace("datatypes-debug") << "...returned " << ifin
291
172549
                                           << std::endl;
292
172549
                  if (!ifin)
293
                  {
294
117560
                    if( !eqc || !eqc->d_selectors ){
295
112740
                      needSplit = false;
296
                    }
297
                  }else{
298
54989
                    if( fconsIndex==-1 ){
299
35607
                      fconsIndex = j;
300
                    }
301
                  }
302
                }
303
              }
304
              //if we want to force an assignment of constructors to all ground eqc
305
              //d_dtfCounter++;
306
67400
              if( !needSplit && options::dtForceAssignment() && d_dtfCounter%2==0 ){
307
                Trace("datatypes-force-assign") << "Force assignment for " << n << std::endl;
308
                needSplit = true;
309
                consIndex = fconsIndex!=-1 ? fconsIndex : consIndex;
310
              }
311
312
40422
              if( needSplit ) {
313
13444
                if( dt.getNumConstructors()==1 ){
314
                  //this may not be necessary?
315
                  //if only one constructor, then this term must be this constructor
316
23790
                  Node t = utils::mkTester(n, 0, dt);
317
11895
                  d_im.addPendingInference(
318
                      t, InferenceId::DATATYPES_SPLIT, d_true);
319
11895
                  Trace("datatypes-infer") << "DtInfer : 1-cons (full) : " << t << std::endl;
320
                }else{
321
1549
                  Assert(consIndex != -1 || dt.isSygus());
322
3098
                  if( options::dtBinarySplit() && consIndex!=-1 ){
323
                    Node test = utils::mkTester(n, consIndex, dt);
324
                    Trace("dt-split") << "*************Split for possible constructor " << dt[consIndex] << " for " << n << endl;
325
                    test = Rewriter::rewrite( test );
326
                    NodeBuilder<> nb(kind::OR);
327
                    nb << test << test.notNode();
328
                    Node lemma = nb;
329
                    d_im.lemma(lemma, InferenceId::DATATYPES_BINARY_SPLIT);
330
                    d_im.requirePhase(test, true);
331
                  }else{
332
1549
                    Trace("dt-split") << "*************Split for constructors on " << n <<  endl;
333
3098
                    Node lemma = utils::mkSplit(n, dt);
334
1549
                    Trace("dt-split-debug") << "Split lemma is : " << lemma << std::endl;
335
1549
                    d_im.sendDtLemma(lemma,
336
                                     InferenceId::DATATYPES_SPLIT,
337
                                     LemmaProperty::SEND_ATOMS);
338
                  }
339
3098
                  if( !options::dtBlastSplits() ){
340
1549
                    break;
341
                  }
342
                }
343
              }else{
344
26978
                Trace("dt-split-debug") << "Do not split constructor for " << n << " : " << n.getType() << " " << dt.getNumConstructors() << std::endl;
345
              }
346
            }
347
          }else{
348
137857
            Trace("datatypes-debug") << "Has constructor " << eqc->d_constructor.get() << std::endl;
349
          }
350
        }
351
627559
        ++eqcs_i;
352
      }
353
27455
      if (d_im.hasSentLemma())
354
      {
355
        // clear pending facts: we added a lemma, so internal inferences are
356
        // no longer necessary
357
1553
        d_im.clearPendingFacts();
358
      }
359
      else
360
      {
361
        // we did not add a lemma, process internal inferences. This loop
362
        // will repeat.
363
25902
        Trace("datatypes-debug") << "Flush pending facts..." << std::endl;
364
25902
        d_im.process();
365
      }
366
54695
    } while (!d_state.isInConflict() && !d_im.hasSentLemma()
367
53016
             && d_im.hasSentFact());
368
52434
    Trace("datatypes-debug")
369
52434
        << "Finished, conflict=" << d_state.isInConflict()
370
26217
        << ", lemmas=" << d_im.hasSentLemma() << std::endl;
371
26217
    if (!d_state.isInConflict())
372
    {
373
26002
      Trace("dt-model-debug") << std::endl;
374
26002
      printModelDebug("dt-model-debug");
375
    }
376
  }
377
378
754343
  Trace("datatypes-check") << "Finished check effort " << level << std::endl;
379
754343
  if( Debug.isOn("datatypes") || Debug.isOn("datatypes-split") ) {
380
    Notice() << "TheoryDatatypes::check(): done" << endl;
381
  }
382
}
383
384
13772
bool TheoryDatatypes::needsCheckLastEffort() {
385
13772
  return d_sygusExtension != nullptr;
386
}
387
388
2893885
void TheoryDatatypes::notifyFact(TNode atom,
389
                                 bool polarity,
390
                                 TNode fact,
391
                                 bool isInternal)
392
{
393
5787770
  Trace("datatypes-debug") << "TheoryDatatypes::assertFact : " << fact
394
2893885
                           << ", isInternal = " << isInternal << std::endl;
395
  // could be sygus-specific
396
2893885
  if (d_sygusExtension)
397
  {
398
2632655
    d_sygusExtension->assertFact(atom, polarity);
399
  }
400
  //add to tester if applicable
401
5787770
  Node t_arg;
402
2893885
  int tindex = utils::isTester(atom, t_arg);
403
2893885
  if (tindex >= 0)
404
  {
405
1511449
    Trace("dt-tester") << "Assert tester : " << atom << " for " << t_arg << std::endl;
406
3022898
    Node rep = getRepresentative( t_arg );
407
1511449
    EqcInfo* eqc = getOrMakeEqcInfo( rep, true );
408
    Node tst =
409
3022898
        isInternal ? (polarity ? Node(atom) : atom.notNode()) : Node(fact);
410
1511449
    addTester(tindex, tst, eqc, rep, t_arg);
411
1511449
    Trace("dt-tester") << "Done assert tester." << std::endl;
412
1511449
    Trace("dt-tester") << "Done pending merges." << std::endl;
413
1511449
    if (!d_state.isInConflict() && polarity)
414
    {
415
387365
      if (d_sygusExtension)
416
      {
417
342598
        Trace("dt-tester") << "Assert tester to sygus : " << atom << std::endl;
418
342598
        d_sygusExtension->assertTester(tindex, t_arg, atom);
419
342598
        Trace("dt-tester") << "Done assert tester to sygus." << std::endl;
420
      }
421
    }
422
  }else{
423
1382436
    Trace("dt-tester-debug") << "Assert (non-tester) : " << atom << std::endl;
424
  }
425
2893885
  Trace("datatypes-debug") << "TheoryDatatypes::assertFact : finished " << fact << std::endl;
426
  // now, flush pending facts if this wasn't an internal call
427
2893885
  if (!isInternal)
428
  {
429
2486617
    d_im.process();
430
  }
431
2893885
}
432
433
159069
void TheoryDatatypes::preRegisterTerm(TNode n)
434
{
435
318138
  Trace("datatypes-prereg")
436
159069
      << "TheoryDatatypes::preRegisterTerm() " << n << endl;
437
  // external selectors should be preprocessed away by now
438
159069
  Assert(n.getKind() != APPLY_SELECTOR);
439
  // must ensure the type is well founded and has no nested recursion if
440
  // the option dtNestedRec is not set to true.
441
318138
  TypeNode tn = n.getType();
442
159069
  if (tn.isDatatype())
443
  {
444
47434
    const DType& dt = tn.getDType();
445
47434
    Trace("dt-expand") << "Check properties of " << dt.getName() << std::endl;
446
47434
    if (!dt.isWellFounded())
447
    {
448
      std::stringstream ss;
449
      ss << "Cannot handle non-well-founded datatype " << dt.getName();
450
      throw LogicException(ss.str());
451
    }
452
47434
    Trace("dt-expand") << "...well-founded ok" << std::endl;
453
94888
    if (!options::dtNestedRec())
454
    {
455
47256
      if (dt.hasNestedRecursion())
456
      {
457
2
        std::stringstream ss;
458
1
        ss << "Cannot handle nested-recursive datatype " << dt.getName();
459
1
        throw LogicException(ss.str());
460
      }
461
47255
      Trace("dt-expand") << "...nested recursion ok" << std::endl;
462
    }
463
  }
464
159068
  collectTerms( n );
465
159068
  switch (n.getKind()) {
466
81456
  case kind::EQUAL:
467
  case kind::APPLY_TESTER:
468
    // add predicate trigger for testers and equalities
469
    // Get triggered for both equal and dis-equal
470
81456
    d_equalityEngine->addTriggerPredicate(n);
471
81456
    break;
472
77612
  default:
473
    // Function applications/predicates
474
77612
    d_equalityEngine->addTerm(n);
475
77612
    if (d_sygusExtension)
476
    {
477
35601
      d_sygusExtension->preRegisterTerm(n);
478
    }
479
77612
    break;
480
  }
481
159068
  d_im.process();
482
159068
}
483
484
74687
TrustNode TheoryDatatypes::expandDefinition(Node n)
485
{
486
74687
  NodeManager* nm = NodeManager::currentNM();
487
149374
  TypeNode tn = n.getType();
488
149374
  Node ret;
489
74687
  switch (n.getKind())
490
  {
491
3138
    case kind::APPLY_SELECTOR:
492
    {
493
6276
      Node selector = n.getOperator();
494
      // APPLY_SELECTOR always applies to an external selector, cindexOf is
495
      // legal here
496
3138
      size_t cindex = utils::cindexOf(selector);
497
3138
      const DType& dt = utils::datatypeOf(selector);
498
3138
      const DTypeConstructor& c = dt[cindex];
499
6276
      Node selector_use;
500
6276
      TypeNode ndt = n[0].getType();
501
3138
      if (options::dtSharedSelectors())
502
      {
503
3138
        size_t selectorIndex = utils::indexOf(selector);
504
6276
        Trace("dt-expand") << "...selector index = " << selectorIndex
505
3138
                           << std::endl;
506
3138
        Assert(selectorIndex < c.getNumArgs());
507
3138
        selector_use = c.getSelectorInternal(ndt, selectorIndex);
508
      }else{
509
        selector_use = selector;
510
      }
511
6276
      Node sel = nm->mkNode(kind::APPLY_SELECTOR_TOTAL, selector_use, n[0]);
512
3138
      if (options::dtRewriteErrorSel())
513
      {
514
347
        ret = sel;
515
      }
516
      else
517
      {
518
5582
        Node tester = c.getTester();
519
5582
        Node tst = nm->mkNode(APPLY_TESTER, tester, n[0]);
520
2791
        tst = Rewriter::rewrite(tst);
521
2791
        if (tst == d_true)
522
        {
523
768
          ret = sel;
524
        }else{
525
2023
          mkExpDefSkolem(selector, ndt, n.getType());
526
          Node sk =
527
4046
              nm->mkNode(kind::APPLY_UF, d_exp_def_skolem[ndt][selector], n[0]);
528
2023
          if (tst == nm->mkConst(false))
529
          {
530
13
            ret = sk;
531
          }
532
          else
533
          {
534
2010
            ret = nm->mkNode(kind::ITE, tst, sel, sk);
535
          }
536
        }
537
5582
        Trace("dt-expand") << "Expand def : " << n << " to " << ret
538
2791
                           << std::endl;
539
3138
      }
540
    }
541
3138
    break;
542
6
    case TUPLE_UPDATE:
543
    case RECORD_UPDATE:
544
    {
545
6
      Assert(tn.isDatatype());
546
6
      const DType& dt = tn.getDType();
547
12
      NodeBuilder<> b(APPLY_CONSTRUCTOR);
548
6
      b << dt[0].getConstructor();
549
      size_t size, updateIndex;
550
6
      if (n.getKind() == TUPLE_UPDATE)
551
      {
552
1
        Assert(tn.isTuple());
553
1
        size = tn.getTupleLength();
554
1
        updateIndex = n.getOperator().getConst<TupleUpdate>().getIndex();
555
      }
556
      else
557
      {
558
5
        Assert(tn.isRecord());
559
5
        const DTypeConstructor& recCons = dt[0];
560
5
        size = recCons.getNumArgs();
561
        // get the index for the name
562
5
        updateIndex = recCons.getSelectorIndexForName(
563
10
            n.getOperator().getConst<RecordUpdate>().getField());
564
      }
565
6
      Debug("tuprec") << "expr is " << n << std::endl;
566
6
      Debug("tuprec") << "updateIndex is " << updateIndex << std::endl;
567
6
      Debug("tuprec") << "t is " << tn << std::endl;
568
6
      Debug("tuprec") << "t has arity " << size << std::endl;
569
17
      for (size_t i = 0; i < size; ++i)
570
      {
571
11
        if (i == updateIndex)
572
        {
573
6
          b << n[1];
574
12
          Debug("tuprec") << "arg " << i << " gets updated to " << n[1]
575
6
                          << std::endl;
576
        }
577
        else
578
        {
579
25
          b << nm->mkNode(
580
20
              APPLY_SELECTOR_TOTAL, dt[0].getSelectorInternal(tn, i), n[0]);
581
10
          Debug("tuprec") << "arg " << i << " copies "
582
5
                          << b[b.getNumChildren() - 1] << std::endl;
583
        }
584
      }
585
6
      ret = b;
586
12
      Debug("tuprec") << "return " << ret << std::endl;
587
    }
588
6
    break;
589
71543
    default: break;
590
  }
591
74687
  if (!ret.isNull() && n != ret)
592
  {
593
3144
    return TrustNode::mkTrustRewrite(n, ret, nullptr);
594
  }
595
71543
  return TrustNode::null();
596
}
597
598
74112
TrustNode TheoryDatatypes::ppRewrite(TNode in, std::vector<SkolemLemma>& lems)
599
{
600
74112
  Debug("tuprec") << "TheoryDatatypes::ppRewrite(" << in << ")" << endl;
601
  // first, see if we need to expand definitions
602
148224
  TrustNode texp = expandDefinition(in);
603
74112
  if (!texp.isNull())
604
  {
605
2899
    return texp;
606
  }
607
71213
  if( in.getKind()==EQUAL ){
608
7553
    Node nn;
609
7553
    std::vector< Node > rew;
610
3823
    if (utils::checkClash(in[0], in[1], rew))
611
    {
612
      nn = NodeManager::currentNM()->mkConst(false);
613
    }
614
    else
615
    {
616
11397
      nn = rew.size()==0 ? d_true :
617
7574
                ( rew.size()==1 ? rew[0] : NodeManager::currentNM()->mkNode( kind::AND, rew ) );
618
    }
619
3823
    if (in != nn)
620
    {
621
93
      return TrustNode::mkTrustRewrite(in, nn, nullptr);
622
    }
623
  }
624
625
  // nothing to do
626
71120
  return TrustNode::null();
627
}
628
629
66708
TrustNode TheoryDatatypes::explain(TNode literal)
630
{
631
66708
  return d_im.explainLit(literal);
632
}
633
634
/** called when a new equivalance class is created */
635
322909
void TheoryDatatypes::eqNotifyNewClass(TNode t){
636
322909
  if( t.getKind()==APPLY_CONSTRUCTOR ){
637
127444
    getOrMakeEqcInfo( t, true );
638
  }
639
322909
}
640
641
/** called when two equivalance classes have merged */
642
3158691
void TheoryDatatypes::eqNotifyMerge(TNode t1, TNode t2)
643
{
644
3158691
  if( t1.getType().isDatatype() ){
645
1307660
    Trace("datatypes-debug")
646
653830
        << "NotifyMerge : " << t1 << " " << t2 << std::endl;
647
653830
    merge(t1,t2);
648
  }
649
3158691
}
650
651
653830
void TheoryDatatypes::merge( Node t1, Node t2 ){
652
653830
  if (!d_state.isInConflict())
653
  {
654
1301208
    TNode trep1 = t1;
655
1301208
    TNode trep2 = t2;
656
652347
    Trace("datatypes-debug") << "Merge " << t1 << " " << t2 << std::endl;
657
652347
    EqcInfo* eqc2 = getOrMakeEqcInfo( t2 );
658
652347
    if( eqc2 ){
659
490351
      bool checkInst = false;
660
490351
      if( !eqc2->d_constructor.get().isNull() ){
661
93198
        trep2 = eqc2->d_constructor.get();
662
      }
663
490351
      EqcInfo* eqc1 = getOrMakeEqcInfo( t1 );
664
490351
      if( eqc1 ){
665
478731
        Trace("datatypes-debug") << "  merge eqc info " << eqc2 << " into " << eqc1 << std::endl;
666
478731
        if( !eqc1->d_constructor.get().isNull() ){
667
394750
          trep1 = eqc1->d_constructor.get();
668
        }
669
        //check for clash
670
954831
        TNode cons1 = eqc1->d_constructor.get();
671
954831
        TNode cons2 = eqc2->d_constructor.get();
672
        //if both have constructor, then either clash or unification
673
478731
        if( !cons1.isNull() && !cons2.isNull() ){
674
38890
          Trace("datatypes-debug") << "  constructors : " << cons1 << " " << cons2 << std::endl;
675
75155
          Node unifEq = cons1.eqNode( cons2 );
676
75155
          std::vector< Node > rew;
677
38890
          if (utils::checkClash(cons1, cons2, rew))
678
          {
679
5250
            std::vector<Node> conf;
680
2625
            conf.push_back(unifEq);
681
5250
            Trace("dt-conflict")
682
2625
                << "CONFLICT: Clash conflict : " << conf << std::endl;
683
2625
            d_im.sendDtConflict(conf, InferenceId::DATATYPES_CLASH_CONFLICT);
684
2625
            return;
685
          }
686
          else
687
          {
688
            //do unification
689
105351
            for( int i=0; i<(int)cons1.getNumChildren(); i++ ) {
690
69086
              if( !areEqual( cons1[i], cons2[i] ) ){
691
44380
                Node eq = cons1[i].eqNode( cons2[i] );
692
22190
                d_im.addPendingInference(
693
                    eq, InferenceId::DATATYPES_UNIF, unifEq);
694
22190
                Trace("datatypes-infer") << "DtInfer : cons-inj : " << eq << " by " << unifEq << std::endl;
695
              }
696
            }
697
          }
698
        }
699
476106
        Trace("datatypes-debug") << "  instantiated : " << eqc1->d_inst << " " << eqc2->d_inst << std::endl;
700
476106
        eqc1->d_inst = eqc1->d_inst || eqc2->d_inst;
701
476106
        if( !cons2.isNull() ){
702
87017
          if( cons1.isNull() ){
703
50752
            Trace("datatypes-debug") << "  must check if it is okay to set the constructor." << std::endl;
704
50752
            checkInst = true;
705
50752
            addConstructor( eqc2->d_constructor.get(), eqc1, t1 );
706
50752
            if (d_state.isInConflict())
707
            {
708
6
              return;
709
            }
710
          }
711
        }
712
      }else{
713
11620
        Trace("datatypes-debug") << "  no eqc info for " << t1 << ", must create" << std::endl;
714
        //just copy the equivalence class information
715
11620
        eqc1 = getOrMakeEqcInfo( t1, true );
716
11620
        eqc1->d_inst.set( eqc2->d_inst );
717
11620
        eqc1->d_constructor.set( eqc2->d_constructor );
718
11620
        eqc1->d_selectors.set( eqc2->d_selectors );
719
      }
720
721
722
      //merge labels
723
487720
      NodeUIntMap::iterator lbl_i = d_labels.find(t2);
724
487720
      if( lbl_i != d_labels.end() ){
725
487720
        Trace("datatypes-debug") << "  merge labels from " << eqc2 << " " << t2 << std::endl;
726
487720
        size_t n_label = (*lbl_i).second;
727
953240
        for (size_t i = 0; i < n_label; i++)
728
        {
729
466375
          Assert(i < d_labels_data[t2].size());
730
931895
          Node t = d_labels_data[ t2 ][i];
731
931895
          Node t_arg = d_labels_args[t2][i];
732
466375
          unsigned tindex = d_labels_tindex[t2][i];
733
466375
          addTester( tindex, t, eqc1, t1, t_arg );
734
466375
          if (d_state.isInConflict())
735
          {
736
855
            Trace("datatypes-debug") << "  conflict!" << std::endl;
737
855
            return;
738
          }
739
        }
740
741
      }
742
      //merge selectors
743
486865
      if( !eqc1->d_selectors && eqc2->d_selectors ){
744
74922
        eqc1->d_selectors = true;
745
74922
        checkInst = true;
746
      }
747
486865
      NodeUIntMap::iterator sel_i = d_selector_apps.find(t2);
748
486865
      if( sel_i != d_selector_apps.end() ){
749
486865
        Trace("datatypes-debug") << "  merge selectors from " << eqc2 << " " << t2 << std::endl;
750
486865
        size_t n_sel = (*sel_i).second;
751
1243048
        for (size_t j = 0; j < n_sel; j++)
752
        {
753
756183
          addSelector( d_selector_apps_data[t2][j], eqc1, t1, eqc2->d_constructor.get().isNull() );
754
        }
755
      }
756
486865
      if( checkInst ){
757
125668
        Trace("datatypes-debug") << "  checking instantiate" << std::endl;
758
125668
        instantiate( eqc1, t1 );
759
125668
        if (d_state.isInConflict())
760
        {
761
          return;
762
        }
763
      }
764
    }
765
648861
    Trace("datatypes-debug") << "Finished Merge " << t1 << " " << t2 << std::endl;
766
  }
767
}
768
769
24252
TheoryDatatypes::EqcInfo::EqcInfo( context::Context* c )
770
    : d_inst( c, false )
771
48504
    , d_constructor( c, Node::null() )
772
72756
    , d_selectors( c, false )
773
24252
{}
774
775
178287
bool TheoryDatatypes::hasLabel( EqcInfo* eqc, Node n ){
776
178287
  return ( eqc && !eqc->d_constructor.get().isNull() ) || !getLabel( n ).isNull();
777
}
778
779
1037992
Node TheoryDatatypes::getLabel( Node n ) {
780
1037992
  NodeUIntMap::iterator lbl_i = d_labels.find(n);
781
1037992
  if( lbl_i != d_labels.end() ){
782
965112
    size_t n_lbl = (*lbl_i).second;
783
965112
    if( n_lbl>0 && d_labels_data[n][ n_lbl-1 ].getKind()!=kind::NOT ){
784
284931
      return d_labels_data[n][ n_lbl-1 ];
785
    }
786
  }
787
753061
  return Node::null();
788
}
789
790
2350294
int TheoryDatatypes::getLabelIndex( EqcInfo* eqc, Node n ){
791
2350294
  if( eqc && !eqc->d_constructor.get().isNull() ){
792
1493626
    return utils::indexOf(eqc->d_constructor.get().getOperator());
793
  }else{
794
1713336
    Node lbl = getLabel( n );
795
856668
    if( lbl.isNull() ){
796
712631
      return -1;
797
    }else{
798
144037
      int tindex = utils::isTester(lbl);
799
288074
      Trace("datatypes-debug") << "Label of " << n << " is " << lbl
800
144037
                               << " with tindex " << tindex << std::endl;
801
144037
      Assert(tindex != -1);
802
144037
      return tindex;
803
    }
804
  }
805
}
806
807
21391
bool TheoryDatatypes::hasTester( Node n ) {
808
21391
  NodeUIntMap::iterator lbl_i = d_labels.find(n);
809
21391
  if( lbl_i != d_labels.end() ){
810
2
    return (*lbl_i).second>0;
811
  }else{
812
21389
    return false;
813
  }
814
}
815
816
106156
void TheoryDatatypes::getPossibleCons( EqcInfo* eqc, Node n, std::vector< bool >& pcons ){
817
212312
  TypeNode tn = n.getType();
818
106156
  const DType& dt = tn.getDType();
819
106156
  int lindex = getLabelIndex( eqc, n );
820
106156
  pcons.resize( dt.getNumConstructors(), lindex==-1 );
821
106156
  if( lindex!=-1 ){
822
    pcons[ lindex ] = true;
823
  }else{
824
106156
    NodeUIntMap::iterator lbl_i = d_labels.find(n);
825
106156
    if( lbl_i != d_labels.end() ){
826
69720
      size_t n_lbl = (*lbl_i).second;
827
432934
      for (size_t i = 0; i < n_lbl; i++)
828
      {
829
363214
        Assert(d_labels_data[n][i].getKind() == NOT);
830
363214
        unsigned tindex = d_labels_tindex[n][i];
831
363214
        pcons[ tindex ] = false;
832
      }
833
    }
834
  }
835
106156
}
836
837
2023
void TheoryDatatypes::mkExpDefSkolem( Node sel, TypeNode dt, TypeNode rt ) {
838
2023
  if( d_exp_def_skolem[dt].find( sel )==d_exp_def_skolem[dt].end() ){
839
586
    std::stringstream ss;
840
293
    ss << sel << "_uf";
841
879
    d_exp_def_skolem[dt][ sel ] = NodeManager::currentNM()->mkSkolem( ss.str().c_str(),
842
586
                                  NodeManager::currentNM()->mkFunctionType( dt, rt ) );
843
  }
844
2023
}
845
846
148162
Node TheoryDatatypes::getTermSkolemFor( Node n ) {
847
148162
  if( n.getKind()==APPLY_CONSTRUCTOR ){
848
7516
    NodeMap::const_iterator it = d_term_sk.find( n );
849
7516
    if( it==d_term_sk.end() ){
850
      //add purification unit lemma ( k = n )
851
1256
      Node k = NodeManager::currentNM()->mkSkolem( "k", n.getType(), "reference skolem for datatypes" );
852
628
      d_term_sk[n] = k;
853
1256
      Node eq = k.eqNode( n );
854
628
      Trace("datatypes-infer") << "DtInfer : ref : " << eq << std::endl;
855
628
      d_im.addPendingLemma(eq, InferenceId::DATATYPES_PURIFY);
856
628
      return k;
857
    }else{
858
6888
      return (*it).second;
859
    }
860
  }else{
861
140646
    return n;
862
  }
863
}
864
865
1977824
void TheoryDatatypes::addTester(
866
    unsigned ttindex, Node t, EqcInfo* eqc, Node n, Node t_arg)
867
{
868
1977824
  Trace("datatypes-debug") << "Add tester : " << t << " to eqc(" << n << ")" << std::endl;
869
1977824
  Debug("datatypes-labels") << "Add tester " << t << " " << n << " " << eqc << std::endl;
870
1977824
  bool tpolarity = t.getKind()!=NOT;
871
1977824
  Assert((tpolarity ? t : t[0]).getKind() == APPLY_TESTER);
872
2470359
  Node j, jt;
873
1977824
  bool makeConflict = false;
874
1977824
  int prevTIndex = getLabelIndex(eqc, n);
875
1977824
  if (prevTIndex >= 0)
876
  {
877
1371967
    unsigned ptu = static_cast<unsigned>(prevTIndex);
878
    //if we already know the constructor type, check whether it is in conflict or redundant
879
1371967
    if ((ptu == ttindex) != tpolarity)
880
    {
881
2169
      if( !eqc->d_constructor.get().isNull() ){
882
        //conflict because equivalence class contains a constructor
883
4338
        std::vector<Node> conf;
884
2169
        conf.push_back(t);
885
2169
        conf.push_back(t_arg.eqNode(eqc->d_constructor.get()));
886
4338
        Trace("dt-conflict")
887
2169
            << "CONFLICT: Tester eq conflict " << conf << std::endl;
888
2169
        d_im.sendDtConflict(conf, InferenceId::DATATYPES_TESTER_CONFLICT);
889
2169
        return;
890
      }else{
891
        makeConflict = true;
892
        //conflict because the existing label is contradictory
893
        j = getLabel( n );
894
        jt = j;
895
      }
896
    }else{
897
1369798
      return;
898
    }
899
  }else{
900
    //otherwise, scan list of labels
901
605857
    NodeUIntMap::iterator lbl_i = d_labels.find(n);
902
605857
    Assert(lbl_i != d_labels.end());
903
605857
    size_t n_lbl = (*lbl_i).second;
904
1098392
    std::map< int, bool > neg_testers;
905
2671395
    for (size_t i = 0; i < n_lbl; i++)
906
    {
907
2113293
      Assert(d_labels_data[n][i].getKind() == NOT);
908
2113293
      unsigned jtindex = d_labels_tindex[n][i];
909
2113293
      if( jtindex==ttindex ){
910
47755
        if( tpolarity ){  //we are in conflict
911
165
          j = d_labels_data[n][i];
912
165
          jt = j[0];
913
165
          makeConflict = true;
914
165
          break;
915
        }else{            //it is redundant
916
47590
          return;
917
        }
918
      }else{
919
2065538
        neg_testers[jtindex] = true;
920
      }
921
    }
922
558267
    if( !makeConflict ){
923
558102
      Debug("datatypes-labels") << "Add to labels " << t << std::endl;
924
558102
      d_labels[n] = n_lbl + 1;
925
558102
      if (n_lbl < d_labels_data[n].size())
926
      {
927
        // reuse spot in the vector
928
543739
        d_labels_data[n][n_lbl] = t;
929
543739
        d_labels_args[n][n_lbl] = t_arg;
930
543739
        d_labels_tindex[n][n_lbl] = ttindex;
931
      }else{
932
14363
        d_labels_data[n].push_back(t);
933
14363
        d_labels_args[n].push_back(t_arg);
934
14363
        d_labels_tindex[n].push_back(ttindex);
935
      }
936
558102
      n_lbl++;
937
938
558102
      const DType& dt = t_arg.getType().getDType();
939
558102
      Debug("datatypes-labels") << "Labels at " << n_lbl << " / " << dt.getNumConstructors() << std::endl;
940
558102
      if( tpolarity ){
941
140646
        instantiate( eqc, n );
942
        // We could propagate is-C1(x) => not is-C2(x) here for all other
943
        // constructors, but empirically this hurts performance.
944
      }else{
945
        //check if we have reached the maximum number of testers
946
        // in this case, add the positive tester
947
417456
        if (n_lbl == dt.getNumConstructors() - 1)
948
        {
949
131464
          std::vector< bool > pcons;
950
65732
          getPossibleCons( eqc, n, pcons );
951
65732
          int testerIndex = -1;
952
225722
          for( unsigned i=0; i<pcons.size(); i++ ) {
953
225722
            if( pcons[i] ){
954
65732
              testerIndex = i;
955
65732
              break;
956
            }
957
          }
958
65732
          Assert(testerIndex != -1);
959
          //we must explain why each term in the set of testers for this equivalence class is equal
960
131464
          std::vector< Node > eq_terms;
961
131464
          NodeBuilder<> nb(kind::AND);
962
426889
          for (unsigned i = 0; i < n_lbl; i++)
963
          {
964
722314
            Node ti = d_labels_data[n][i];
965
361157
            nb << ti;
966
361157
            Assert(ti.getKind() == NOT);
967
722314
            Node t_arg2 = d_labels_args[n][i];
968
361157
            if( std::find( eq_terms.begin(), eq_terms.end(), t_arg2 )==eq_terms.end() ){
969
75642
              eq_terms.push_back( t_arg2 );
970
75642
              if( t_arg2!=t_arg ){
971
9910
                nb << t_arg2.eqNode( t_arg );
972
              }
973
            }
974
          }
975
          Node t_concl = testerIndex == -1
976
                             ? NodeManager::currentNM()->mkConst(false)
977
131464
                             : utils::mkTester(t_arg, testerIndex, dt);
978
131464
          Node t_concl_exp = ( nb.getNumChildren() == 1 ) ? nb.getChild( 0 ) : nb;
979
65732
          d_im.addPendingInference(
980
              t_concl, InferenceId::DATATYPES_LABEL_EXH, t_concl_exp);
981
65732
          Trace("datatypes-infer") << "DtInfer : label : " << t_concl << " by " << t_concl_exp << std::endl;
982
65732
          return;
983
        }
984
      }
985
    }
986
  }
987
492535
  if( makeConflict ){
988
165
    Debug("datatypes-labels") << "Explain " << j << " " << t << std::endl;
989
330
    std::vector<Node> conf;
990
165
    conf.push_back(j);
991
165
    conf.push_back(t);
992
165
    conf.push_back(jt[0].eqNode(t_arg));
993
165
    Trace("dt-conflict") << "CONFLICT: Tester conflict : " << conf << std::endl;
994
165
    d_im.sendDtConflict(conf, InferenceId::DATATYPES_TESTER_MERGE_CONFLICT);
995
  }
996
}
997
998
779257
void TheoryDatatypes::addSelector( Node s, EqcInfo* eqc, Node n, bool assertFacts ) {
999
779257
  Trace("dt-collapse-sel") << "Add selector : " << s << " to eqc(" << n << ")" << std::endl;
1000
  //check to see if it is redundant
1001
779257
  NodeUIntMap::iterator sel_i = d_selector_apps.find(n);
1002
779257
  Assert(sel_i != d_selector_apps.end());
1003
779257
  if( sel_i != d_selector_apps.end() ){
1004
779257
    size_t n_sel = (*sel_i).second;
1005
1471477
    for (size_t j = 0; j < n_sel; j++)
1006
    {
1007
1899694
      Node ss = d_selector_apps_data[n][j];
1008
1207474
      if( s.getOperator()==ss.getOperator() && ( s.getKind()!=DT_HEIGHT_BOUND || s[1]==ss[1] ) ){
1009
515254
        Trace("dt-collapse-sel") << "...redundant." << std::endl;
1010
515254
        return;
1011
      }
1012
    }
1013
    //add it to the vector
1014
    //sel->push_back( s );
1015
264003
    d_selector_apps[n] = n_sel + 1;
1016
264003
    if (n_sel < d_selector_apps_data[n].size())
1017
    {
1018
245868
      d_selector_apps_data[n][n_sel] = s;
1019
    }else{
1020
18135
      d_selector_apps_data[n].push_back( s );
1021
    }
1022
1023
264003
    eqc->d_selectors = true;
1024
  }
1025
264003
  if( assertFacts && !eqc->d_constructor.get().isNull() ){
1026
    //conclude the collapsed merge
1027
206931
    collapseSelector( s, eqc->d_constructor.get() );
1028
  }
1029
}
1030
1031
50752
void TheoryDatatypes::addConstructor( Node c, EqcInfo* eqc, Node n ){
1032
50752
  Trace("datatypes-debug") << "Add constructor : " << c << " to eqc(" << n << ")" << std::endl;
1033
50752
  Assert(eqc->d_constructor.get().isNull());
1034
  //check labels
1035
50752
  NodeUIntMap::iterator lbl_i = d_labels.find(n);
1036
50752
  if( lbl_i != d_labels.end() ){
1037
50752
    size_t constructorIndex = utils::indexOf(c.getOperator());
1038
50752
    size_t n_lbl = (*lbl_i).second;
1039
270826
    for (size_t i = 0; i < n_lbl; i++)
1040
    {
1041
440154
      Node t = d_labels_data[n][i];
1042
220080
      if (d_labels_data[n][i].getKind() == NOT)
1043
      {
1044
170349
        unsigned tindex = d_labels_tindex[n][i];
1045
170349
        if (tindex == constructorIndex)
1046
        {
1047
12
          std::vector<Node> conf;
1048
6
          conf.push_back(t);
1049
6
          conf.push_back(t[0][0].eqNode(c));
1050
12
          Trace("dt-conflict")
1051
6
              << "CONFLICT: Tester merge eq conflict : " << conf << std::endl;
1052
6
          d_im.sendDtConflict(conf, InferenceId::DATATYPES_TESTER_CONFLICT);
1053
6
          return;
1054
        }
1055
      }
1056
    }
1057
  }
1058
  //check selectors
1059
50746
  NodeUIntMap::iterator sel_i = d_selector_apps.find(n);
1060
50746
  if( sel_i != d_selector_apps.end() ){
1061
50746
    size_t n_sel = (*sel_i).second;
1062
216215
    for (size_t j = 0; j < n_sel; j++)
1063
    {
1064
330938
      Node s = d_selector_apps_data[n][j];
1065
      //collapse the selector
1066
165469
      collapseSelector( s, c );
1067
    }
1068
  }
1069
50746
  eqc->d_constructor.set( c );
1070
}
1071
1072
372400
void TheoryDatatypes::collapseSelector( Node s, Node c ) {
1073
372400
  Assert(c.getKind() == APPLY_CONSTRUCTOR);
1074
372400
  Trace("dt-collapse-sel") << "collapse selector : " << s << " " << c << std::endl;
1075
744800
  Node r;
1076
372400
  bool wrong = false;
1077
744800
  Node eq_exp = s[0].eqNode(c);
1078
372400
  if( s.getKind()==kind::APPLY_SELECTOR_TOTAL ){
1079
527068
    Node selector = s.getOperator();
1080
263534
    size_t constructorIndex = utils::indexOf(c.getOperator());
1081
263534
    const DType& dt = utils::datatypeOf(selector);
1082
263534
    const DTypeConstructor& dtc = dt[constructorIndex];
1083
263534
    int selectorIndex = dtc.getSelectorIndexInternal(selector);
1084
263534
    wrong = selectorIndex<0;
1085
263534
    r = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, s.getOperator(), c );
1086
  }
1087
372400
  if( !r.isNull() ){
1088
527068
    Node rrs;
1089
263534
    if (wrong)
1090
    {
1091
      // Must use make ground term here instead of the rewriter, since we
1092
      // do not want to introduce arbitrary values. This is important so that
1093
      // we avoid constants for types that are not "closed enumerable", e.g.
1094
      // uninterpreted sorts and arrays, where the solver does not fully
1095
      // handle values of the sort. The call to mkGroundTerm does not introduce
1096
      // values for these sorts.
1097
155761
      rrs = r.getType().mkGroundTerm();
1098
311522
      Trace("datatypes-wrong-sel")
1099
155761
          << "Bad apply " << r << " term = " << rrs
1100
155761
          << ", value = " << r.getType().mkGroundValue() << std::endl;
1101
    }
1102
    else
1103
    {
1104
107773
      rrs = Rewriter::rewrite(r);
1105
    }
1106
263534
    if (s != rrs)
1107
    {
1108
345906
      Node eq = s.eqNode(rrs);
1109
      // Since collapsing selectors may generate new terms, we must send
1110
      // this out as a lemma if it is of an external type, or otherwise we
1111
      // may ask for the equality status of terms that only datatypes knows
1112
      // about, see issue #5344.
1113
172953
      bool forceLemma = !s.getType().isDatatype();
1114
172953
      Trace("datatypes-infer") << "DtInfer : collapse sel";
1115
172953
      Trace("datatypes-infer") << " : " << eq << " by " << eq_exp << std::endl;
1116
172953
      d_im.addPendingInference(
1117
          eq, InferenceId::DATATYPES_COLLAPSE_SEL, eq_exp, forceLemma);
1118
    }
1119
  }
1120
372400
}
1121
1122
123192
EqualityStatus TheoryDatatypes::getEqualityStatus(TNode a, TNode b){
1123
123192
  Assert(d_equalityEngine->hasTerm(a) && d_equalityEngine->hasTerm(b));
1124
123192
  if (d_equalityEngine->areEqual(a, b))
1125
  {
1126
    // The terms are implied to be equal
1127
9088
    return EQUALITY_TRUE;
1128
  }
1129
114104
  if (d_equalityEngine->areDisequal(a, b, false))
1130
  {
1131
    // The terms are implied to be dis-equal
1132
    return EQUALITY_FALSE;
1133
  }
1134
114104
  return EQUALITY_FALSE_IN_MODEL;
1135
}
1136
1137
135947
void TheoryDatatypes::addCarePairs(TNodeTrie* t1,
1138
                                   TNodeTrie* t2,
1139
                                   unsigned arity,
1140
                                   unsigned depth,
1141
                                   unsigned& n_pairs)
1142
{
1143
135947
  if( depth==arity ){
1144
12224
    if( t2!=NULL ){
1145
24448
      Node f1 = t1->getData();
1146
24448
      Node f2 = t2->getData();
1147
12224
      if( !areEqual( f1, f2 ) ){
1148
12224
        Trace("dt-cg") << "Check " << f1 << " and " << f2 << std::endl;
1149
24448
        vector< pair<TNode, TNode> > currentPairs;
1150
36664
        for (unsigned k = 0; k < f1.getNumChildren(); ++ k) {
1151
48880
          TNode x = f1[k];
1152
48880
          TNode y = f2[k];
1153
24440
          Assert(d_equalityEngine->hasTerm(x));
1154
24440
          Assert(d_equalityEngine->hasTerm(y));
1155
24440
          Assert(!areDisequal(x, y));
1156
24440
          Assert(!areCareDisequal(x, y));
1157
24440
          if (!d_equalityEngine->areEqual(x, y))
1158
          {
1159
13784
            Trace("dt-cg") << "Arg #" << k << " is " << x << " " << y << std::endl;
1160
41352
            if (d_equalityEngine->isTriggerTerm(x, THEORY_DATATYPES)
1161
41352
                && d_equalityEngine->isTriggerTerm(y, THEORY_DATATYPES))
1162
            {
1163
1646
              TNode x_shared = d_equalityEngine->getTriggerTermRepresentative(
1164
3292
                  x, THEORY_DATATYPES);
1165
1646
              TNode y_shared = d_equalityEngine->getTriggerTermRepresentative(
1166
3292
                  y, THEORY_DATATYPES);
1167
1646
              currentPairs.push_back(make_pair(x_shared, y_shared));
1168
            }
1169
          }
1170
        }
1171
13870
        for (unsigned c = 0; c < currentPairs.size(); ++ c) {
1172
1646
          Trace("dt-cg-pair") << "Pair : " << currentPairs[c].first << " " << currentPairs[c].second << std::endl;
1173
1646
          addCarePair(currentPairs[c].first, currentPairs[c].second);
1174
1646
          n_pairs++;
1175
        }
1176
      }
1177
    }
1178
  }else{
1179
123723
    if( t2==NULL ){
1180
113715
      if( depth<(arity-1) ){
1181
        //add care pairs internal to each child
1182
43510
        for (std::pair<const TNode, TNodeTrie>& tt : t1->d_data)
1183
        {
1184
25520
          addCarePairs(&tt.second, nullptr, arity, depth + 1, n_pairs);
1185
        }
1186
      }
1187
      //add care pairs based on each pair of non-disequal arguments
1188
298510
      for (std::map<TNode, TNodeTrie>::iterator it = t1->d_data.begin();
1189
298510
           it != t1->d_data.end();
1190
           ++it)
1191
      {
1192
184795
        std::map<TNode, TNodeTrie>::iterator it2 = it;
1193
184795
        ++it2;
1194
480549
        for( ; it2 != t1->d_data.end(); ++it2 ){
1195
147877
          if (!d_equalityEngine->areDisequal(it->first, it2->first, false))
1196
          {
1197
64914
            if( !areCareDisequal(it->first, it2->first) ){
1198
13062
              addCarePairs( &it->second, &it2->second, arity, depth+1, n_pairs );
1199
            }
1200
          }
1201
        }
1202
      }
1203
    }else{
1204
      //add care pairs based on product of indices, non-disequal arguments
1205
33144
      for (std::pair<const TNode, TNodeTrie>& tt1 : t1->d_data)
1206
      {
1207
49908
        for (std::pair<const TNode, TNodeTrie>& tt2 : t2->d_data)
1208
        {
1209
26772
          if (!d_equalityEngine->areDisequal(tt1.first, tt2.first, false))
1210
          {
1211
16166
            if (!areCareDisequal(tt1.first, tt2.first))
1212
            {
1213
9170
              addCarePairs(&tt1.second, &tt2.second, arity, depth + 1, n_pairs);
1214
            }
1215
          }
1216
        }
1217
      }
1218
    }
1219
  }
1220
135947
}
1221
1222
14341
void TheoryDatatypes::computeCareGraph(){
1223
14341
  unsigned n_pairs = 0;
1224
14341
  Trace("dt-cg-summary") << "Compute graph for dt..." << d_functionTerms.size() << " " << d_sharedTerms.size() << std::endl;
1225
14341
  Trace("dt-cg") << "Build indices..." << std::endl;
1226
28682
  std::map<TypeNode, std::map<Node, TNodeTrie> > index;
1227
28682
  std::map< Node, unsigned > arity;
1228
  //populate indices
1229
14341
  unsigned functionTerms = d_functionTerms.size();
1230
384191
  for( unsigned i=0; i<functionTerms; i++ ){
1231
739700
    TNode f1 = d_functionTerms[i];
1232
369850
    Assert(d_equalityEngine->hasTerm(f1));
1233
369850
    Trace("dt-cg-debug") << "...build for " << f1 << std::endl;
1234
    //break into index based on operator, and type of first argument (since some operators are parametric)
1235
739700
    Node op = f1.getOperator();
1236
739700
    TypeNode tn = f1[0].getType();
1237
739700
    std::vector< TNode > reps;
1238
369850
    bool has_trigger_arg = false;
1239
785217
    for( unsigned j=0; j<f1.getNumChildren(); j++ ){
1240
415367
      reps.push_back(d_equalityEngine->getRepresentative(f1[j]));
1241
415367
      if (d_equalityEngine->isTriggerTerm(f1[j], THEORY_DATATYPES))
1242
      {
1243
361553
        has_trigger_arg = true;
1244
      }
1245
    }
1246
    //only may contribute to care pairs if has at least one trigger argument
1247
369850
    if( has_trigger_arg ){
1248
327145
      index[tn][op].addTerm( f1, reps );
1249
327145
      arity[op] = reps.size();
1250
    }
1251
  }
1252
  //for each index
1253
41464
  for (std::pair<const TypeNode, std::map<Node, TNodeTrie> >& tt : index)
1254
  {
1255
115318
    for (std::pair<const Node, TNodeTrie>& t : tt.second)
1256
    {
1257
176390
      Trace("dt-cg") << "Process index " << tt.first << ", " << t.first << "..."
1258
88195
                     << std::endl;
1259
88195
      addCarePairs(&t.second, nullptr, arity[t.first], 0, n_pairs);
1260
    }
1261
  }
1262
14341
  Trace("dt-cg-summary") << "...done, # pairs = " << n_pairs << std::endl;
1263
14341
}
1264
1265
12873
bool TheoryDatatypes::collectModelValues(TheoryModel* m,
1266
                                         const std::set<Node>& termSet)
1267
{
1268
25746
  Trace("dt-cmi") << "Datatypes : Collect model values "
1269
12873
                  << d_equalityEngine->consistent() << std::endl;
1270
12873
  Trace("dt-model") << std::endl;
1271
12873
  printModelDebug( "dt-model" );
1272
12873
  Trace("dt-model") << std::endl;
1273
1274
  //get all constructors
1275
12873
  eq::EqClassesIterator eqccs_i = eq::EqClassesIterator(d_equalityEngine);
1276
25746
  std::vector< Node > cons;
1277
25746
  std::vector< Node > nodes;
1278
25746
  std::map< Node, Node > eqc_cons;
1279
927275
  while( !eqccs_i.isFinished() ){
1280
914402
    Node eqc = (*eqccs_i);
1281
    //for all equivalence classes that are datatypes
1282
    //if( termSet.find( eqc )==termSet.end() ){
1283
    //  Trace("dt-cmi-debug") << "Irrelevant eqc : " << eqc << std::endl;
1284
    //}
1285
457201
    if( eqc.getType().isDatatype() ){
1286
93431
      EqcInfo* ei = getOrMakeEqcInfo( eqc );
1287
93431
      if( ei && !ei->d_constructor.get().isNull() ){
1288
144080
        Node c = ei->d_constructor.get();
1289
72040
        cons.push_back( c );
1290
72040
        eqc_cons[ eqc ] = c;
1291
      }else{
1292
        //if eqc contains a symbol known to datatypes (a selector), then we must assign
1293
        //should assign constructors to EQC if they have a selector or a tester
1294
21391
        bool shouldConsider = ( ei && ei->d_selectors ) || hasTester( eqc );
1295
21391
        if( shouldConsider ){
1296
2
          nodes.push_back( eqc );
1297
        }
1298
      }
1299
    }
1300
    //}
1301
457201
    ++eqccs_i;
1302
  }
1303
1304
  //unsigned orig_size = nodes.size();
1305
25746
  std::map< TypeNode, int > typ_enum_map;
1306
25746
  std::vector< TypeEnumerator > typ_enum;
1307
12873
  unsigned index = 0;
1308
12877
  while( index<nodes.size() ){
1309
4
    Node eqc = nodes[index];
1310
4
    Node neqc;
1311
2
    bool addCons = false;
1312
4
    TypeNode tt = eqc.getType();
1313
2
    const DType& dt = tt.getDType();
1314
2
    if (!d_equalityEngine->hasTerm(eqc))
1315
    {
1316
      Assert(false);
1317
    }else{
1318
2
      Trace("dt-cmi") << "NOTICE : Datatypes: no constructor in equivalence class " << eqc << std::endl;
1319
2
      Trace("dt-cmi") << "   Type : " << eqc.getType() << std::endl;
1320
2
      EqcInfo* ei = getOrMakeEqcInfo( eqc );
1321
4
      std::vector< bool > pcons;
1322
2
      getPossibleCons( ei, eqc, pcons );
1323
2
      Trace("dt-cmi") << "Possible constructors : ";
1324
16
      for( unsigned i=0; i<pcons.size(); i++ ){
1325
14
        Trace("dt-cmi") << pcons[i] << " ";
1326
      }
1327
2
      Trace("dt-cmi") << std::endl;
1328
6
      for( unsigned r=0; r<2; r++ ){
1329
4
        if( neqc.isNull() ){
1330
10
          for( unsigned i=0; i<pcons.size(); i++ ){
1331
            //must try the infinite ones first
1332
10
            bool cfinite = dt[ i ].isInterpretedFinite( tt );
1333
10
            if( pcons[i] && (r==1)==cfinite ){
1334
2
              neqc = utils::getInstCons(eqc, dt, i);
1335
2
              break;
1336
            }
1337
          }
1338
        }
1339
      }
1340
2
      addCons = true;
1341
    }
1342
2
    if( !neqc.isNull() ){
1343
2
      Trace("dt-cmi") << "Assign : " << neqc << std::endl;
1344
2
      if (!m->assertEquality(eqc, neqc, true))
1345
      {
1346
        return false;
1347
      }
1348
2
      eqc_cons[ eqc ] = neqc;
1349
    }
1350
2
    if( addCons ){
1351
2
      cons.push_back( neqc );
1352
    }
1353
2
    ++index;
1354
  }
1355
1356
84931
  for( std::map< Node, Node >::iterator it = eqc_cons.begin(); it != eqc_cons.end(); ++it ){
1357
144116
    Node eqc = it->first;
1358
72058
    if( eqc.getType().isCodatatype() ){
1359
      //until models are implemented for codatatypes
1360
      //throw Exception("Models for codatatypes are not supported in this version.");
1361
      //must proactive expand to avoid looping behavior in model builder
1362
75
      if( !it->second.isNull() ){
1363
124
        std::map< Node, int > vmap;
1364
124
        Node v = getCodatatypesValue( it->first, eqc_cons, vmap, 0 );
1365
62
        Trace("dt-cmi") << "  EQC(" << it->first << "), constructor is " << it->second << ", value is " << v << ", const = " << v.isConst() << std::endl;
1366
62
        if (!m->assertEquality(eqc, v, true))
1367
        {
1368
          return false;
1369
        }
1370
62
        m->assertSkeleton(v);
1371
      }
1372
    }else{
1373
71983
      Trace("dt-cmi") << "Datatypes : assert representative " << it->second << " for " << it->first << std::endl;
1374
71983
      m->assertSkeleton(it->second);
1375
    }
1376
  }
1377
12873
  return true;
1378
}
1379
1380
1381
199
Node TheoryDatatypes::getCodatatypesValue( Node n, std::map< Node, Node >& eqc_cons, std::map< Node, int >& vmap, int depth ){
1382
199
  std::map< Node, int >::iterator itv = vmap.find( n );
1383
199
  if( itv!=vmap.end() ){
1384
6
    int debruijn = depth - 1 - itv->second;
1385
    return NodeManager::currentNM()->mkConst(
1386
6
        UninterpretedConstant(n.getType(), debruijn));
1387
193
  }else if( n.getType().isDatatype() ){
1388
173
    Node nc = eqc_cons[n];
1389
139
    if( !nc.isNull() ){
1390
105
      vmap[n] = depth;
1391
105
      Trace("dt-cmi-cdt-debug") << "    map " << n << " -> " << depth << std::endl;
1392
105
      Assert(nc.getKind() == APPLY_CONSTRUCTOR);
1393
210
      std::vector< Node > children;
1394
105
      children.push_back( nc.getOperator() );
1395
242
      for( unsigned i=0; i<nc.getNumChildren(); i++ ){
1396
274
        Node r = getRepresentative( nc[i] );
1397
274
        Node rv = getCodatatypesValue( r, eqc_cons, vmap, depth+1 );
1398
137
        children.push_back( rv );
1399
      }
1400
105
      vmap.erase( n );
1401
105
      return NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children );
1402
    }
1403
  }
1404
88
  return n;
1405
}
1406
1407
Node TheoryDatatypes::getSingletonLemma( TypeNode tn, bool pol ) {
1408
  int index = pol ? 0 : 1;
1409
  std::map< TypeNode, Node >::iterator it = d_singleton_lemma[index].find( tn );
1410
  if( it==d_singleton_lemma[index].end() ){
1411
    Node a;
1412
    if( pol ){
1413
      Node v1 = NodeManager::currentNM()->mkBoundVar( tn );
1414
      Node v2 = NodeManager::currentNM()->mkBoundVar( tn );
1415
      a = NodeManager::currentNM()->mkNode( FORALL, NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, v1, v2 ), v1.eqNode( v2 ) );
1416
    }else{
1417
      Node v1 = NodeManager::currentNM()->mkSkolem( "k1", tn );
1418
      Node v2 = NodeManager::currentNM()->mkSkolem( "k2", tn );
1419
      a = v1.eqNode( v2 ).negate();
1420
      //send out immediately as lemma
1421
      d_im.lemma(a, InferenceId::DATATYPES_REC_SINGLETON_FORCE_DEQ);
1422
      Trace("dt-singleton") << "******** assert " << a << " to avoid singleton cardinality for type " << tn << std::endl;
1423
    }
1424
    d_singleton_lemma[index][tn] = a;
1425
    return a;
1426
  }else{
1427
    return it->second;
1428
  }
1429
}
1430
1431
307230
void TheoryDatatypes::collectTerms( Node n ) {
1432
307230
  if (d_collectTermsCache.find(n) != d_collectTermsCache.end())
1433
  {
1434
    // already processed
1435
45911
    return;
1436
  }
1437
261319
  d_collectTermsCache[n] = true;
1438
261319
  Kind nk = n.getKind();
1439
261319
  if (nk == APPLY_CONSTRUCTOR)
1440
  {
1441
116901
    Debug("datatypes") << "  Found constructor " << n << endl;
1442
116901
    if (n.getNumChildren() > 0)
1443
    {
1444
69887
      d_functionTerms.push_back(n);
1445
    }
1446
116901
    return;
1447
  }
1448
144418
  if (nk == APPLY_SELECTOR_TOTAL || nk == DT_SIZE || nk == DT_HEIGHT_BOUND)
1449
  {
1450
23074
    d_functionTerms.push_back(n);
1451
    // we must also record which selectors exist
1452
23074
    Trace("dt-collapse-sel") << "  Found selector " << n << endl;
1453
46148
    Node rep = getRepresentative(n[0]);
1454
    // record it in the selectors
1455
23074
    EqcInfo* eqc = getOrMakeEqcInfo(rep, true);
1456
    // add it to the eqc info
1457
23074
    addSelector(n, eqc, rep);
1458
  }
1459
1460
  // now, do user-context-dependent lemmas
1461
144418
  if (nk != DT_SIZE && nk != DT_HEIGHT_BOUND)
1462
  {
1463
    // if not one of these kinds, there are no lemmas
1464
136783
    return;
1465
  }
1466
7635
  if (d_collectTermsCacheU.find(n) != d_collectTermsCacheU.end())
1467
  {
1468
3683
    return;
1469
  }
1470
3952
  d_collectTermsCacheU[n] = true;
1471
1472
3952
  NodeManager* nm = NodeManager::currentNM();
1473
1474
3952
  if (nk == DT_SIZE)
1475
  {
1476
7904
    Node lem = nm->mkNode(LEQ, d_zero, n);
1477
7904
    Trace("datatypes-infer")
1478
3952
        << "DtInfer : size geq zero : " << lem << std::endl;
1479
3952
    d_im.addPendingLemma(lem, InferenceId::DATATYPES_SIZE_POS);
1480
  }
1481
  else if (nk == DT_HEIGHT_BOUND && n[1].getConst<Rational>().isZero())
1482
  {
1483
    std::vector<Node> children;
1484
    const DType& dt = n[0].getType().getDType();
1485
    for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
1486
    {
1487
      if (utils::isNullaryConstructor(dt[i]))
1488
      {
1489
        Node test = utils::mkTester(n[0], i, dt);
1490
        children.push_back(test);
1491
      }
1492
    }
1493
    Node lem;
1494
    if (children.empty())
1495
    {
1496
      lem = n.negate();
1497
    }
1498
    else
1499
    {
1500
      lem = n.eqNode(children.size() == 1 ? children[0]
1501
                                          : nm->mkNode(OR, children));
1502
    }
1503
    Trace("datatypes-infer") << "DtInfer : zero height : " << lem << std::endl;
1504
    d_im.addPendingLemma(lem, InferenceId::DATATYPES_HEIGHT_ZERO);
1505
  }
1506
}
1507
1508
168223
Node TheoryDatatypes::getInstantiateCons(Node n, const DType& dt, int index)
1509
{
1510
168223
  if( n.getKind()==APPLY_CONSTRUCTOR && n.getNumChildren()==0 ){
1511
20061
    return n;
1512
  }
1513
  //add constructor to equivalence class
1514
296324
  Node k = getTermSkolemFor( n );
1515
296324
  Node n_ic = utils::getInstCons(k, dt, index);
1516
148162
  n_ic = Rewriter::rewrite( n_ic );
1517
  // it may be a new term, so we collect terms and add it to the equality engine
1518
148162
  collectTerms( n_ic );
1519
148162
  d_equalityEngine->addTerm(n_ic);
1520
148162
  Debug("dt-enum") << "Made instantiate cons " << n_ic << std::endl;
1521
148162
  return n_ic;
1522
}
1523
1524
266314
void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){
1525
266314
  Trace("datatypes-debug") << "Instantiate: " << n << std::endl;
1526
  //add constructor to equivalence class if not done so already
1527
266314
  int index = getLabelIndex( eqc, n );
1528
266314
  if (index == -1 || eqc->d_inst)
1529
  {
1530
216243
    return;
1531
  }
1532
316385
  Node exp;
1533
316385
  Node tt;
1534
168223
  if (!eqc->d_constructor.get().isNull())
1535
  {
1536
27577
    exp = d_true;
1537
27577
    tt = eqc->d_constructor;
1538
  }
1539
  else
1540
  {
1541
140646
    exp = getLabel(n);
1542
140646
    tt = exp[0];
1543
  }
1544
316385
  TypeNode ttn = tt.getType();
1545
168223
  const DType& dt = ttn.getDType();
1546
  // instantiate this equivalence class
1547
168223
  eqc->d_inst = true;
1548
316385
  Node tt_cons = getInstantiateCons(tt, dt, index);
1549
316385
  Node eq;
1550
168223
  if (tt == tt_cons)
1551
  {
1552
20061
    return;
1553
  }
1554
148162
  eq = tt.eqNode(tt_cons);
1555
  // Determine if the equality must be sent out as a lemma. Notice that
1556
  // we  keep new equalities from the instantiate rule internal
1557
  // as long as they are for datatype constructors that have no arguments that
1558
  // have finite external type, which corresponds to:
1559
  //   forceLemma = dt[index].hasFiniteExternalArgType(ttn);
1560
  // Such equalities must be sent because they introduce selector terms that
1561
  // may contribute to conflicts due to cardinality (good examples of this are
1562
  // regress0/datatypes/dt-param-card4-bool-sat.smt2 and
1563
  // regress0/datatypes/list-bool.smt2).
1564
  bool forceLemma;
1565
296324
  if (options::dtPoliteOptimize())
1566
  {
1567
148162
    forceLemma = dt[index].hasFiniteExternalArgType(ttn);
1568
  }
1569
  else
1570
  {
1571
    forceLemma = dt.involvesExternalType();
1572
  }
1573
296324
  Trace("datatypes-infer-debug") << "DtInstantiate : " << eqc << " " << eq
1574
148162
                                 << " forceLemma = " << forceLemma << std::endl;
1575
148162
  d_im.addPendingInference(eq, InferenceId::DATATYPES_INST, exp, forceLemma);
1576
296324
  Trace("datatypes-infer") << "DtInfer : instantiate : " << eq << " by " << exp
1577
148162
                           << std::endl;
1578
}
1579
1580
26616
void TheoryDatatypes::checkCycles() {
1581
26616
  Trace("datatypes-cycle-check") << "Check acyclicity" << std::endl;
1582
52843
  std::vector< Node > cdt_eqc;
1583
26616
  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(d_equalityEngine);
1584
1484900
  while( !eqcs_i.isFinished() ){
1585
1458673
    Node eqc = (*eqcs_i);
1586
1458673
    TypeNode tn = eqc.getType();
1587
729531
    if( tn.isDatatype() ) {
1588
226858
      if( !tn.isCodatatype() ){
1589
451126
        if( options::dtCyclic() ){
1590
          //do cycle checks
1591
450737
          std::map< TNode, bool > visited;
1592
450737
          std::map< TNode, bool > proc;
1593
450737
          std::vector<Node> expl;
1594
225563
          Trace("datatypes-cycle-check") << "...search for cycle starting at " << eqc << std::endl;
1595
450737
          Node cn = searchForCycle( eqc, eqc, visited, proc, expl );
1596
225563
          Trace("datatypes-cycle-check") << "...finish." << std::endl;
1597
          //if we discovered a different cycle while searching this one
1598
225563
          if( !cn.isNull() && cn!=eqc ){
1599
20
            visited.clear();
1600
20
            proc.clear();
1601
20
            expl.clear();
1602
40
            Node prev = cn;
1603
20
            cn = searchForCycle( cn, cn, visited, proc, expl );
1604
20
            Assert(prev == cn);
1605
          }
1606
1607
225563
          if( !cn.isNull() ) {
1608
389
            Assert(expl.size() > 0);
1609
778
            Trace("dt-conflict")
1610
389
                << "CONFLICT: Cycle conflict : " << expl << std::endl;
1611
389
            d_im.sendDtConflict(expl, InferenceId::DATATYPES_CYCLE);
1612
389
            return;
1613
          }
1614
        }
1615
      }else{
1616
        //indexing
1617
1295
        cdt_eqc.push_back( eqc );
1618
      }
1619
    }
1620
729142
    ++eqcs_i;
1621
  }
1622
26227
  Trace("datatypes-cycle-check") << "Check uniqueness" << std::endl;
1623
  //process codatatypes
1624
26312
  if( cdt_eqc.size()>1 && options::cdtBisimilar() ){
1625
85
    printModelDebug("dt-cdt-debug");
1626
85
    Trace("dt-cdt-debug") << "Process " << cdt_eqc.size() << " co-datatypes" << std::endl;
1627
170
    std::vector< std::vector< Node > > part_out;
1628
170
    std::vector<Node> exp;
1629
170
    std::map< Node, Node > cn;
1630
170
    std::map< Node, std::map< Node, int > > dni;
1631
1376
    for( unsigned i=0; i<cdt_eqc.size(); i++ ){
1632
1291
      cn[cdt_eqc[i]] = cdt_eqc[i];
1633
    }
1634
85
    separateBisimilar( cdt_eqc, part_out, exp, cn, dni, 0, false );
1635
85
    Trace("dt-cdt-debug") << "Done separate bisimilar." << std::endl;
1636
85
    if( !part_out.empty() ){
1637
10
      Trace("dt-cdt-debug") << "Process partition size " << part_out.size() << std::endl;
1638
20
      for( unsigned i=0; i<part_out.size(); i++ ){
1639
20
        std::vector< Node > part;
1640
10
        part.push_back( part_out[i][0] );
1641
20
        for( unsigned j=1; j<part_out[i].size(); j++ ){
1642
10
          Trace("dt-cdt") << "Codatatypes : " << part_out[i][0] << " and " << part_out[i][j] << " must be equal!!" << std::endl;
1643
10
          part.push_back( part_out[i][j] );
1644
20
          std::vector< std::vector< Node > > tpart_out;
1645
10
          exp.clear();
1646
10
          cn.clear();
1647
10
          cn[part_out[i][0]] = part_out[i][0];
1648
10
          cn[part_out[i][j]] = part_out[i][j];
1649
10
          dni.clear();
1650
10
          separateBisimilar( part, tpart_out, exp, cn, dni, 0, true );
1651
10
          Assert(tpart_out.size() == 1 && tpart_out[0].size() == 2);
1652
10
          part.pop_back();
1653
          //merge based on explanation
1654
10
          Trace("dt-cdt") << "  exp is : ";
1655
38
          for( unsigned k=0; k<exp.size(); k++ ){
1656
28
            Trace("dt-cdt") << exp[k] << " ";
1657
          }
1658
10
          Trace("dt-cdt") << std::endl;
1659
20
          Node eq = part_out[i][0].eqNode( part_out[i][j] );
1660
20
          Node eqExp = NodeManager::currentNM()->mkAnd(exp);
1661
10
          d_im.addPendingInference(eq, InferenceId::DATATYPES_BISIMILAR, eqExp);
1662
10
          Trace("datatypes-infer") << "DtInfer : cdt-bisimilar : " << eq << " by " << eqExp << std::endl;
1663
        }
1664
      }
1665
    }
1666
  }
1667
}
1668
1669
//everything is in terms of representatives
1670
287
void TheoryDatatypes::separateBisimilar(
1671
    std::vector<Node>& part,
1672
    std::vector<std::vector<Node> >& part_out,
1673
    std::vector<Node>& exp,
1674
    std::map<Node, Node>& cn,
1675
    std::map<Node, std::map<Node, int> >& dni,
1676
    int dniLvl,
1677
    bool mkExp)
1678
{
1679
287
  if( !mkExp ){
1680
249
    Trace("dt-cdt-debug") << "Separate bisimilar : " << std::endl;
1681
2019
    for( unsigned i=0; i<part.size(); i++ ){
1682
1770
      Trace("dt-cdt-debug") << "   " << part[i] << ", current = " << cn[part[i]] << std::endl;
1683
    }
1684
  }
1685
287
  Assert(part.size() > 1);
1686
574
  std::map< Node, std::vector< Node > > new_part;
1687
574
  std::map< Node, std::vector< Node > > new_part_c;
1688
574
  std::map< int, std::vector< Node > > new_part_rec;
1689
1690
574
  std::map< Node, Node > cn_cons;
1691
2133
  for( unsigned j=0; j<part.size(); j++ ){
1692
3692
    Node c = cn[part[j]];
1693
1846
    std::map< Node, int >::iterator it_rec = dni[part[j]].find( c );
1694
1846
    if( it_rec!=dni[part[j]].end() ){
1695
      //looped
1696
46
      if( !mkExp ){ Trace("dt-cdt-debug") << "  - " << part[j] << " is looping at index " << it_rec->second << std::endl; }
1697
46
      new_part_rec[ it_rec->second ].push_back( part[j] );
1698
    }else{
1699
1800
      if( c.getType().isDatatype() ){
1700
3010
        Node ncons = getEqcConstructor( c );
1701
1505
        if( ncons.getKind()==APPLY_CONSTRUCTOR ) {
1702
898
          Node cc = ncons.getOperator();
1703
449
          cn_cons[part[j]] = ncons;
1704
449
          if (mkExp && c != ncons)
1705
          {
1706
20
            exp.push_back(c.eqNode(ncons));
1707
          }
1708
449
          new_part[cc].push_back( part[j] );
1709
449
          if( !mkExp ){ Trace("dt-cdt-debug") << "  - " << part[j] << " is datatype " << ncons << "." << std::endl; }
1710
        }else{
1711
1056
          new_part_c[c].push_back( part[j] );
1712
1056
          if( !mkExp ){ Trace("dt-cdt-debug") << "  - " << part[j] << " is unspecified datatype." << std::endl; }
1713
        }
1714
      }else{
1715
        //add equivalences
1716
295
        if( !mkExp ){ Trace("dt-cdt-debug") << "  - " << part[j] << " is term " << c << "." << std::endl; }
1717
295
        new_part_c[c].push_back( part[j] );
1718
      }
1719
    }
1720
  }
1721
  //direct add for constants
1722
1517
  for( std::map< Node, std::vector< Node > >::iterator it = new_part_c.begin(); it != new_part_c.end(); ++it ){
1723
1230
    if( it->second.size()>1 ){
1724
218
      std::vector< Node > vec;
1725
109
      vec.insert( vec.begin(), it->second.begin(), it->second.end() );
1726
109
      part_out.push_back( vec );
1727
    }
1728
  }
1729
  //direct add for recursive
1730
313
  for( std::map< int, std::vector< Node > >::iterator it = new_part_rec.begin(); it != new_part_rec.end(); ++it ){
1731
26
    if( it->second.size()>1 ){
1732
40
      std::vector< Node > vec;
1733
20
      vec.insert( vec.begin(), it->second.begin(), it->second.end() );
1734
20
      part_out.push_back( vec );
1735
    }else{
1736
      //add back : could match a datatype?
1737
    }
1738
  }
1739
  //recurse for the datatypes
1740
514
  for( std::map< Node, std::vector< Node > >::iterator it = new_part.begin(); it != new_part.end(); ++it ){
1741
227
    if( it->second.size()>1 ){
1742
      //set dni to check for loops
1743
166
      std::map< Node, Node > dni_rem;
1744
388
      for( unsigned i=0; i<it->second.size(); i++ ){
1745
610
        Node n = it->second[i];
1746
305
        dni[n][cn[n]] = dniLvl;
1747
305
        dni_rem[n] = cn[n];
1748
      }
1749
1750
      //we will split based on the arguments of the datatype
1751
166
      std::vector< std::vector< Node > > split_new_part;
1752
83
      split_new_part.push_back( it->second );
1753
1754
83
      unsigned nChildren = cn_cons[it->second[0]].getNumChildren();
1755
      //for each child of constructor
1756
83
      unsigned cindex = 0;
1757
389
      while( cindex<nChildren && !split_new_part.empty() ){
1758
153
        if( !mkExp ){ Trace("dt-cdt-debug") << "Split argument #" << cindex << " of " << it->first << "..." << std::endl; }
1759
306
        std::vector< std::vector< Node > > next_split_new_part;
1760
345
        for( unsigned j=0; j<split_new_part.size(); j++ ){
1761
          //set current node
1762
727
          for( unsigned k=0; k<split_new_part[j].size(); k++ ){
1763
1070
            Node n = split_new_part[j][k];
1764
1070
            Node cnc = cn_cons[n][cindex];
1765
1070
            Node nr = getRepresentative(cnc);
1766
535
            cn[n] = nr;
1767
535
            if (mkExp && cnc != nr)
1768
            {
1769
8
              exp.push_back(nr.eqNode(cnc));
1770
            }
1771
          }
1772
384
          std::vector< std::vector< Node > > c_part_out;
1773
192
          separateBisimilar( split_new_part[j], c_part_out, exp, cn, dni, dniLvl+1, mkExp );
1774
192
          next_split_new_part.insert( next_split_new_part.end(), c_part_out.begin(), c_part_out.end() );
1775
        }
1776
153
        split_new_part.clear();
1777
153
        split_new_part.insert( split_new_part.end(), next_split_new_part.begin(), next_split_new_part.end() );
1778
153
        cindex++;
1779
      }
1780
83
      part_out.insert( part_out.end(), split_new_part.begin(), split_new_part.end() );
1781
1782
388
      for( std::map< Node, Node >::iterator it2 = dni_rem.begin(); it2 != dni_rem.end(); ++it2 ){
1783
305
        dni[it2->first].erase( it2->second );
1784
      }
1785
    }
1786
  }
1787
287
}
1788
1789
//postcondition: if cycle detected, explanation is why n is a subterm of on
1790
815373
Node TheoryDatatypes::searchForCycle(TNode n,
1791
                                     TNode on,
1792
                                     std::map<TNode, bool>& visited,
1793
                                     std::map<TNode, bool>& proc,
1794
                                     std::vector<Node>& explanation,
1795
                                     bool firstTime)
1796
{
1797
815373
  Trace("datatypes-cycle-check2") << "Search for cycle " << n << " " << on << endl;
1798
1630746
  TNode ncons;
1799
1630746
  TNode nn;
1800
815373
  if( !firstTime ){
1801
589790
    nn = getRepresentative( n );
1802
589790
    if( nn==on ){
1803
389
      if (n != nn)
1804
      {
1805
351
        explanation.push_back(n.eqNode(nn));
1806
      }
1807
389
      return on;
1808
    }
1809
  }else{
1810
225583
    nn = getRepresentative( n );
1811
  }
1812
814984
  if( proc.find( nn )!=proc.end() ){
1813
135088
    return Node::null();
1814
  }
1815
679896
  Trace("datatypes-cycle-check2") << "...representative : " << nn << " " << ( visited.find( nn ) == visited.end() ) << " " << visited.size() << std::endl;
1816
679896
  if( visited.find( nn ) == visited.end() ) {
1817
679876
    Trace("datatypes-cycle-check2") << "  visit : " << nn << std::endl;
1818
679876
    visited[nn] = true;
1819
1359752
    TNode nncons = getEqcConstructor(nn);
1820
679876
    if (nncons.getKind() == APPLY_CONSTRUCTOR)
1821
    {
1822
1079966
      for (unsigned i = 0; i < nncons.getNumChildren(); i++)
1823
      {
1824
        TNode cn =
1825
1178244
            searchForCycle(nncons[i], on, visited, proc, explanation, false);
1826
589790
        if( cn==on ) {
1827
          //add explanation for why the constructor is connected
1828
1220
          if (n != nncons)
1829
          {
1830
827
            explanation.push_back(n.eqNode(nncons));
1831
          }
1832
1220
          return on;
1833
588570
        }else if( !cn.isNull() ){
1834
116
          return cn;
1835
        }
1836
      }
1837
    }
1838
678540
    Trace("datatypes-cycle-check2") << "  unvisit : " << nn << std::endl;
1839
678540
    proc[nn] = true;
1840
678540
    visited.erase( nn );
1841
678540
    return Node::null();
1842
  }else{
1843
40
    TypeNode tn = nn.getType();
1844
20
    if( tn.isDatatype() ) {
1845
20
      if( !tn.isCodatatype() ){
1846
20
        return nn;
1847
      }
1848
    }
1849
    return Node::null();
1850
  }
1851
}
1852
1853
2539058
bool TheoryDatatypes::hasTerm(TNode a) { return d_equalityEngine->hasTerm(a); }
1854
1855
81310
bool TheoryDatatypes::areEqual( TNode a, TNode b ){
1856
81310
  if( a==b ){
1857
5553
    return true;
1858
75757
  }else if( hasTerm( a ) && hasTerm( b ) ){
1859
75757
    return d_equalityEngine->areEqual(a, b);
1860
  }else{
1861
    return false;
1862
  }
1863
}
1864
1865
24440
bool TheoryDatatypes::areDisequal( TNode a, TNode b ){
1866
24440
  if( a==b ){
1867
5952
    return false;
1868
18488
  }else if( hasTerm( a ) && hasTerm( b ) ){
1869
18488
    return d_equalityEngine->areDisequal(a, b, false);
1870
  }else{
1871
    //TODO : constants here?
1872
    return false;
1873
  }
1874
}
1875
1876
105520
bool TheoryDatatypes::areCareDisequal( TNode x, TNode y ) {
1877
105520
  Trace("datatypes-cg") << "areCareDisequal: " << x << " " << y << std::endl;
1878
105520
  Assert(d_equalityEngine->hasTerm(x));
1879
105520
  Assert(d_equalityEngine->hasTerm(y));
1880
316560
  if (d_equalityEngine->isTriggerTerm(x, THEORY_DATATYPES)
1881
316560
      && d_equalityEngine->isTriggerTerm(y, THEORY_DATATYPES))
1882
  {
1883
    TNode x_shared =
1884
101304
        d_equalityEngine->getTriggerTermRepresentative(x, THEORY_DATATYPES);
1885
    TNode y_shared =
1886
101304
        d_equalityEngine->getTriggerTermRepresentative(y, THEORY_DATATYPES);
1887
80076
    EqualityStatus eqStatus = d_valuation.getEqualityStatus(x_shared, y_shared);
1888
80076
    if( eqStatus==EQUALITY_FALSE_AND_PROPAGATED || eqStatus==EQUALITY_FALSE || eqStatus==EQUALITY_FALSE_IN_MODEL ){
1889
58848
      return true;
1890
    }
1891
  }
1892
46672
  return false;
1893
}
1894
1895
2350568
TNode TheoryDatatypes::getRepresentative( TNode a ){
1896
2350568
  if( hasTerm( a ) ){
1897
2350568
    return d_equalityEngine->getRepresentative(a);
1898
  }else{
1899
    return a;
1900
  }
1901
}
1902
1903
38960
void TheoryDatatypes::printModelDebug( const char* c ){
1904
38960
  if(! (Trace.isOn(c))) {
1905
38960
    return;
1906
  }
1907
1908
  Trace( c ) << "Datatypes model : " << std::endl;
1909
  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(d_equalityEngine);
1910
  while( !eqcs_i.isFinished() ){
1911
    Node eqc = (*eqcs_i);
1912
    //if( !eqc.getType().isBoolean() ){
1913
      if( eqc.getType().isDatatype() ){
1914
        Trace( c ) << "DATATYPE : ";
1915
      }
1916
      Trace( c ) << eqc << " : " << eqc.getType() << " : " << std::endl;
1917
      Trace( c ) << "   { ";
1918
      //add terms to model
1919
      eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, d_equalityEngine);
1920
      while( !eqc_i.isFinished() ){
1921
        if( (*eqc_i)!=eqc ){
1922
          Trace( c ) << (*eqc_i) << " ";
1923
        }
1924
        ++eqc_i;
1925
      }
1926
      Trace( c ) << "}" << std::endl;
1927
      if( eqc.getType().isDatatype() ){
1928
        EqcInfo* ei = getOrMakeEqcInfo( eqc );
1929
        if( ei ){
1930
          Trace( c ) << "   Instantiated : " << ei->d_inst.get() << std::endl;
1931
          Trace( c ) << "   Constructor : ";
1932
          if( !ei->d_constructor.get().isNull() ){
1933
            Trace( c )<< ei->d_constructor.get();
1934
          }
1935
          Trace( c ) << std::endl << "   Labels : ";
1936
          if( hasLabel( ei, eqc ) ){
1937
            Trace( c ) << getLabel( eqc );
1938
          }else{
1939
            NodeUIntMap::iterator lbl_i = d_labels.find(eqc);
1940
            if( lbl_i != d_labels.end() ){
1941
              for (size_t j = 0; j < (*lbl_i).second; j++)
1942
              {
1943
                Trace( c ) << d_labels_data[eqc][j] << " ";
1944
              }
1945
            }
1946
          }
1947
          Trace( c ) << std::endl;
1948
          Trace( c ) << "   Selectors : " << ( ei->d_selectors ? "yes, " : "no " );
1949
          NodeUIntMap::iterator sel_i = d_selector_apps.find(eqc);
1950
          if( sel_i != d_selector_apps.end() ){
1951
            for (size_t j = 0; j < (*sel_i).second; j++)
1952
            {
1953
              Trace( c ) << d_selector_apps_data[eqc][j] << " ";
1954
            }
1955
          }
1956
          Trace( c ) << std::endl;
1957
        }
1958
      }
1959
    //}
1960
    ++eqcs_i;
1961
  }
1962
}
1963
1964
12873
void TheoryDatatypes::computeRelevantTerms(std::set<Node>& termSet)
1965
{
1966
25746
  Trace("dt-cmi") << "Have " << termSet.size() << " relevant terms..."
1967
12873
                  << std::endl;
1968
1969
  //also include non-singleton equivalence classes  TODO : revisit this
1970
12873
  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(d_equalityEngine);
1971
927275
  while( !eqcs_i.isFinished() ){
1972
914402
    TNode r = (*eqcs_i);
1973
457201
    bool addedFirst = false;
1974
914402
    Node first;
1975
914402
    TypeNode rtn = r.getType();
1976
457201
    if (!rtn.isBoolean())
1977
    {
1978
346301
      eq::EqClassIterator eqc_i = eq::EqClassIterator(r, d_equalityEngine);
1979
1763189
      while (!eqc_i.isFinished())
1980
      {
1981
1416888
        TNode n = (*eqc_i);
1982
708444
        if (first.isNull())
1983
        {
1984
346301
          first = n;
1985
          // always include all datatypes
1986
346301
          if (rtn.isDatatype())
1987
          {
1988
93431
            addedFirst = true;
1989
93431
            termSet.insert(n);
1990
          }
1991
        }
1992
        else
1993
        {
1994
362143
          if (!addedFirst)
1995
          {
1996
36780
            addedFirst = true;
1997
36780
            termSet.insert(first);
1998
          }
1999
362143
          termSet.insert(n);
2000
        }
2001
708444
        ++eqc_i;
2002
      }
2003
    }
2004
457201
    ++eqcs_i;
2005
  }
2006
12873
}
2007
2008
std::pair<bool, Node> TheoryDatatypes::entailmentCheck(TNode lit)
2009
{
2010
  Trace("dt-entail") << "Check entailed : " << lit << std::endl;
2011
  Node atom = lit.getKind()==NOT ? lit[0] : lit;
2012
  bool pol = lit.getKind()!=NOT;
2013
  if( atom.getKind()==APPLY_TESTER ){
2014
    Node n = atom[0];
2015
    if( hasTerm( n ) ){
2016
      Node r = d_equalityEngine->getRepresentative(n);
2017
      EqcInfo * ei = getOrMakeEqcInfo( r, false );
2018
      int l_index = getLabelIndex( ei, r );
2019
      int t_index = static_cast<int>(utils::indexOf(atom.getOperator()));
2020
      Trace("dt-entail") << "  Tester indices are " << t_index << " and " << l_index << std::endl;
2021
      if( l_index!=-1 && (l_index==t_index)==pol ){
2022
        std::vector< TNode > exp_c;
2023
        Node eqToExplain;
2024
        if( ei && !ei->d_constructor.get().isNull() ){
2025
          eqToExplain = n.eqNode(ei->d_constructor.get());
2026
        }else{
2027
          Node lbl = getLabel( n );
2028
          Assert(!lbl.isNull());
2029
          exp_c.push_back( lbl );
2030
          Assert(areEqual(n, lbl[0]));
2031
          eqToExplain = n.eqNode(lbl[0]);
2032
        }
2033
        d_equalityEngine->explainLit(eqToExplain, exp_c);
2034
        Node exp = NodeManager::currentNM()->mkAnd(exp_c);
2035
        Trace("dt-entail") << "  entailed, explanation is " << exp << std::endl;
2036
        return make_pair(true, exp);
2037
      }
2038
    }
2039
  }
2040
  return make_pair(false, Node::null());
2041
}
2042
2043
} /* namepsace CVC4::theory::datatypes */
2044
} /* namepsace CVC4::theory */
2045
26676
} /* namepsace CVC4 */