GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/uf/cardinality_extension.cpp Lines: 815 1013 80.5 %
Date: 2021-03-22 Branches: 1694 4150 40.8 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file cardinality_extension.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 theory of UF with cardinality.
13
 **/
14
15
#include "theory/uf/cardinality_extension.h"
16
17
#include <sstream>
18
19
#include "options/smt_options.h"
20
#include "options/uf_options.h"
21
#include "smt/logic_exception.h"
22
#include "theory/decision_manager.h"
23
#include "theory/quantifiers/term_database.h"
24
#include "theory/quantifiers_engine.h"
25
#include "theory/theory_engine.h"
26
#include "theory/theory_model.h"
27
#include "theory/uf/equality_engine.h"
28
#include "theory/uf/theory_uf.h"
29
30
using namespace std;
31
using namespace CVC4::kind;
32
using namespace CVC4::context;
33
34
namespace CVC4 {
35
namespace theory {
36
namespace uf {
37
38
/* These are names are unambigious are we use abbreviations. */
39
typedef CardinalityExtension::SortModel SortModel;
40
typedef SortModel::Region Region;
41
typedef Region::RegionNodeInfo RegionNodeInfo;
42
typedef RegionNodeInfo::DiseqList DiseqList;
43
44
2262
Region::Region(SortModel* cf, context::Context* c)
45
  : d_cf( cf )
46
  , d_testCliqueSize( c, 0 )
47
  , d_splitsSize( c, 0 )
48
  , d_testClique( c )
49
  , d_splits( c )
50
  , d_reps_size( c, 0 )
51
  , d_total_diseq_external( c, 0 )
52
  , d_total_diseq_internal( c, 0 )
53
2262
  , d_valid( c, true ) {}
54
55
6786
Region::~Region() {
56
10616
  for(iterator i = begin(), iend = end(); i != iend; ++i) {
57
8354
    RegionNodeInfo* regionNodeInfo = (*i).second;
58
8354
    delete regionNodeInfo;
59
  }
60
2262
  d_nodes.clear();
61
4524
}
62
63
4251
void Region::addRep( Node n ) {
64
4251
  setRep( n, true );
65
4251
}
66
67
394
void Region::takeNode( Region* r, Node n ){
68
394
  Assert(!hasRep(n));
69
394
  Assert(r->hasRep(n));
70
  //add representative
71
394
  setRep( n, true );
72
  //take disequalities from r
73
394
  RegionNodeInfo* rni = r->d_nodes[n];
74
1182
  for( int t=0; t<2; t++ ){
75
788
    DiseqList* del = rni->get(t);
76
2322
    for(DiseqList::iterator it = del->begin(); it != del->end(); ++it ){
77
1534
      if( (*it).second ){
78
1005
        r->setDisequal( n, (*it).first, t, false );
79
1005
        if( t==0 ){
80
526
          if( hasRep( (*it).first ) ){
81
474
            setDisequal( (*it).first, n, 0, false );
82
474
            setDisequal( (*it).first, n, 1, true );
83
474
            setDisequal( n, (*it).first, 1, true );
84
          }else{
85
52
            setDisequal( n, (*it).first, 0, true );
86
          }
87
        }else{
88
479
          r->setDisequal( (*it).first, n, 1, false );
89
479
          r->setDisequal( (*it).first, n, 0, true );
90
479
          setDisequal( n, (*it).first, 0, true );
91
        }
92
      }
93
    }
94
  }
95
  //remove representative
96
394
  r->setRep( n, false );
97
394
}
98
99
39358
void Region::combine( Region* r ){
100
  //take all nodes from r
101
208358
  for(Region::iterator it = r->d_nodes.begin(); it != r->d_nodes.end(); ++it) {
102
169000
    if( it->second->valid() ){
103
41916
      setRep( it->first, true );
104
    }
105
  }
106
208358
  for(Region::iterator it = r->d_nodes.begin(); it != r->d_nodes.end(); ++it){
107
169000
    if( it->second->valid() ){
108
      //take disequalities from r
109
83832
      Node n = it->first;
110
41916
      RegionNodeInfo* rni = it->second;
111
125748
      for( int t=0; t<2; t++ ){
112
83832
        RegionNodeInfo::DiseqList* del = rni->get(t);
113
213080
        for( RegionNodeInfo::DiseqList::iterator it2 = del->begin(),
114
83832
               it2end = del->end(); it2 != it2end; ++it2 ){
115
129248
          if( (*it2).second ){
116
119263
            if( t==0 && hasRep( (*it2).first ) ){
117
51413
              setDisequal( (*it2).first, n, 0, false );
118
51413
              setDisequal( (*it2).first, n, 1, true );
119
51413
              setDisequal( n, (*it2).first, 1, true );
120
            }else{
121
67850
              setDisequal( n, (*it2).first, t, true );
122
            }
123
          }
124
        }
125
      }
126
    }
127
  }
128
39358
  r->d_valid = false;
129
39358
}
130
131
/** setEqual */
132
31529
void Region::setEqual( Node a, Node b ){
133
31529
  Assert(hasRep(a) && hasRep(b));
134
  //move disequalities of b over to a
135
94587
  for( int t=0; t<2; t++ ){
136
63058
    DiseqList* del = d_nodes[b]->get(t);
137
115942
    for( DiseqList::iterator it = del->begin(); it != del->end(); ++it ){
138
52884
      if( (*it).second ){
139
78046
        Node n = (*it).first;
140
        //get the region that contains the endpoint of the disequality b != ...
141
39023
        Region* nr = d_cf->d_regions[ d_cf->d_regions_map[ n ] ];
142
39023
        if( !isDisequal( a, n, t ) ){
143
17235
          setDisequal( a, n, t, true );
144
17235
          nr->setDisequal( n, a, t, true );
145
        }
146
39023
        setDisequal( b, n, t, false );
147
39023
        nr->setDisequal( n, b, t, false );
148
      }
149
    }
150
  }
151
  //remove b from representatives
152
31529
  setRep( b, false );
153
31529
}
154
155
363641
void Region::setDisequal( Node n1, Node n2, int type, bool valid ){
156
  //Debug("uf-ss-region-debug") << "set disequal " << n1 << " " << n2 << " "
157
  //                            << type << " " << valid << std::endl;
158
  //debugPrint("uf-ss-region-debug");
159
  //Assert( isDisequal( n1, n2, type )!=valid );
160
363641
  if( isDisequal( n1, n2, type )!=valid ){    //DO_THIS: make assertion
161
362932
    d_nodes[ n1 ]->get(type)->setDisequal( n2, valid );
162
362932
    if( type==0 ){
163
158783
      d_total_diseq_external = d_total_diseq_external + ( valid ? 1 : -1 );
164
    }else{
165
204149
      d_total_diseq_internal = d_total_diseq_internal + ( valid ? 1 : -1 );
166
204149
      if( valid ){
167
        //if they are both a part of testClique, then remove split
168
285854
        if( d_testClique.find( n1 )!=d_testClique.end() && d_testClique[n1] &&
169
144470
            d_testClique.find( n2 )!=d_testClique.end() && d_testClique[n2] ){
170
3086
          Node eq = NodeManager::currentNM()->mkNode( EQUAL, n1, n2 );
171
1543
          if( d_splits.find( eq )!=d_splits.end() && d_splits[ eq ] ){
172
1514
            Debug("uf-ss-debug") << "removing split for " << n1 << " " << n2
173
757
                                 << std::endl;
174
757
            d_splits[ eq ] = false;
175
757
            d_splitsSize = d_splitsSize - 1;
176
          }
177
        }
178
      }
179
    }
180
  }
181
363641
}
182
183
78484
void Region::setRep( Node n, bool valid ) {
184
78484
  Assert(hasRep(n) != valid);
185
78484
  if( valid && d_nodes.find( n )==d_nodes.end() ){
186
8354
    d_nodes[n] = new RegionNodeInfo(d_cf->d_state.getSatContext());
187
  }
188
78484
  d_nodes[n]->setValid(valid);
189
78484
  d_reps_size = d_reps_size + ( valid ? 1 : -1 );
190
  //removing a member of the test clique from this region
191
78484
  if( d_testClique.find( n ) != d_testClique.end() && d_testClique[n] ){
192
1444
    Assert(!valid);
193
1444
    d_testClique[n] = false;
194
1444
    d_testCliqueSize = d_testCliqueSize - 1;
195
    //remove all splits involving n
196
13273
    for( split_iterator it = begin_splits(); it != end_splits(); ++it ){
197
11829
      if( (*it).second ){
198
3653
        if( (*it).first[0]==n || (*it).first[1]==n ){
199
3615
          d_splits[ (*it).first ] = false;
200
3615
          d_splitsSize = d_splitsSize - 1;
201
        }
202
      }
203
    }
204
  }
205
78484
}
206
207
445096
bool Region::isDisequal( Node n1, Node n2, int type ) {
208
445096
  RegionNodeInfo::DiseqList* del = d_nodes[ n1 ]->get(type);
209
445096
  return del->isSet(n2) && del->getDisequalityValue(n2);
210
}
211
212
struct sortInternalDegree {
213
  Region* r;
214
14134
  bool operator() (Node i, Node j) {
215
28268
    return (r->getRegionInfo(i)->getNumInternalDisequalities() >
216
28268
            r->getRegionInfo(j)->getNumInternalDisequalities());
217
  }
218
};
219
220
struct sortExternalDegree {
221
  Region* r;
222
  bool operator() (Node i,Node j) {
223
    return (r->getRegionInfo(i)->getNumExternalDisequalities() >
224
            r->getRegionInfo(j)->getNumExternalDisequalities());
225
  }
226
};
227
228
int gmcCount = 0;
229
230
92133
bool Region::getMustCombine( int cardinality ){
231
92133
  if (d_total_diseq_external >= static_cast<unsigned>(cardinality))
232
  {
233
    //The number of external disequalities is greater than or equal to
234
    //cardinality.  Thus, a clique of size cardinality+1 may exist
235
    //between nodes in d_regions[i] and other regions Check if this is
236
    //actually the case: must have n nodes with outgoing degree
237
    //(cardinality+1-n) for some n>0
238
20637
    std::vector< int > degrees;
239
138078
    for( Region::iterator it = begin(); it != end(); ++it ){
240
131132
      RegionNodeInfo* rni = it->second;
241
131132
      if( rni->valid() ){
242
60594
        if( rni->getNumDisequalities() >= cardinality ){
243
46745
          int outDeg = rni->getNumExternalDisequalities();
244
46745
          if( outDeg>=cardinality ){
245
            //we have 1 node of degree greater than (cardinality)
246
14849
            return true;
247
39650
          }else if( outDeg>=1 ){
248
38528
            degrees.push_back( outDeg );
249
38528
            if( (int)degrees.size()>=cardinality ){
250
              //we have (cardinality) nodes of degree 1
251
659
              return true;
252
            }
253
          }
254
        }
255
      }
256
    }
257
6946
    gmcCount++;
258
6946
    if( gmcCount%100==0 ){
259
120
      Trace("gmc-count") << gmcCount << " " << cardinality
260
60
                         << " sample : " << degrees.size() << std::endl;
261
    }
262
    //this should happen relatively infrequently....
263
6946
    std::sort( degrees.begin(), degrees.end() );
264
39439
    for( int i=0; i<(int)degrees.size(); i++ ){
265
33502
      if( degrees[i]>=cardinality+1-((int)degrees.size()-i) ){
266
1009
        return true;
267
      }
268
    }
269
  }
270
83370
  return false;
271
}
272
273
903916
bool Region::check( Theory::Effort level, int cardinality,
274
                    std::vector< Node >& clique ) {
275
903916
  if( d_reps_size>unsigned(cardinality) ){
276
61165
    if( d_total_diseq_internal==d_reps_size*( d_reps_size - 1 ) ){
277
39948
      if( d_reps_size>1 ){
278
        //quick clique check, all reps form a clique
279
22057
        for( iterator it = begin(); it != end(); ++it ){
280
19549
          if( it->second->valid() ){
281
15500
            clique.push_back( it->first );
282
          }
283
        }
284
2508
        Trace("quick-clique") << "Found quick clique" << std::endl;
285
2508
        return true;
286
      }else{
287
37440
        return false;
288
      }
289
    }
290
21217
    else if (level==Theory::EFFORT_FULL)
291
    {
292
      //build test clique, up to size cardinality+1
293
1786
      if( d_testCliqueSize<=unsigned(cardinality) ){
294
3448
        std::vector< Node > newClique;
295
1724
        if( d_testCliqueSize<unsigned(cardinality) ){
296
13352
          for( iterator it = begin(); it != end(); ++it ){
297
            //if not in the test clique, add it to the set of new members
298
38931
            if( it->second->valid() &&
299
19467
                ( d_testClique.find( it->first ) == d_testClique.end() ||
300
1
                  !d_testClique[ it->first ] ) ){
301
              //if( it->second->getNumInternalDisequalities()>cardinality ||
302
              //    level==Theory::EFFORT_FULL ){
303
7545
              newClique.push_back( it->first );
304
              //}
305
            }
306
          }
307
          //choose remaining nodes with the highest degrees
308
          sortInternalDegree sidObj;
309
1432
          sidObj.r = this;
310
1432
          std::sort( newClique.begin(), newClique.end(), sidObj );
311
1432
          int offset = ( cardinality - d_testCliqueSize ) + 1;
312
1432
          newClique.erase( newClique.begin() + offset, newClique.end() );
313
        }else{
314
          //scan for the highest degree
315
292
          int maxDeg = -1;
316
584
          Node maxNode;
317
3063
          for( std::map< Node, RegionNodeInfo* >::iterator
318
292
                 it = d_nodes.begin(); it != d_nodes.end(); ++it ){
319
            //if not in the test clique, add it to the set of new members
320
8266
            if( it->second->valid() &&
321
6416
                ( d_testClique.find( it->first )==d_testClique.end() ||
322
1522
                  !d_testClique[ it->first ] ) ){
323
309
              if( it->second->getNumInternalDisequalities()>maxDeg ){
324
294
                maxDeg = it->second->getNumInternalDisequalities();
325
294
                maxNode = it->first;
326
              }
327
            }
328
          }
329
292
          Assert(maxNode != Node::null());
330
292
          newClique.push_back( maxNode );
331
        }
332
        //check splits internal to new members
333
9462
        for( int j=0; j<(int)newClique.size(); j++ ){
334
15476
          Debug("uf-ss-debug") << "Choose to add clique member "
335
7738
                               << newClique[j] << std::endl;
336
36086
          for( int k=(j+1); k<(int)newClique.size(); k++ ){
337
28348
            if( !isDisequal( newClique[j], newClique[k], 1 ) ){
338
7066
              Node at_j = newClique[j];
339
7066
              Node at_k = newClique[k];
340
              Node j_eq_k =
341
7066
                NodeManager::currentNM()->mkNode( EQUAL, at_j, at_k );
342
3533
              d_splits[ j_eq_k ] = true;
343
3533
              d_splitsSize = d_splitsSize + 1;
344
            }
345
          }
346
          //check disequalities with old members
347
10146
          for( NodeBoolMap::iterator it = d_testClique.begin();
348
10146
               it != d_testClique.end(); ++it ){
349
2408
            if( (*it).second ){
350
1524
              if( !isDisequal( (*it).first, newClique[j], 1 ) ){
351
1998
                Node at_it = (*it).first;
352
1998
                Node at_j = newClique[j];
353
1998
                Node it_eq_j = at_it.eqNode(at_j);
354
999
                d_splits[ it_eq_j ] = true;
355
999
                d_splitsSize = d_splitsSize + 1;
356
              }
357
            }
358
          }
359
        }
360
        //add new clique members to test clique
361
9462
        for( int j=0; j<(int)newClique.size(); j++ ){
362
7738
          d_testClique[ newClique[j] ] = true;
363
7738
          d_testCliqueSize = d_testCliqueSize + 1;
364
        }
365
      }
366
      // Check if test clique has larger size than cardinality, and
367
      // forms a clique.
368
1786
      if( d_testCliqueSize >= unsigned(cardinality+1) && d_splitsSize==0 ){
369
        //test clique is a clique
370
120
        for( NodeBoolMap::iterator it = d_testClique.begin();
371
120
             it != d_testClique.end(); ++it ){
372
88
          if( (*it).second ){
373
86
            clique.push_back( (*it).first );
374
          }
375
        }
376
32
        return true;
377
      }
378
    }
379
  }
380
863936
  return false;
381
}
382
383
void Region::getNumExternalDisequalities(
384
    std::map< Node, int >& num_ext_disequalities ){
385
  for( Region::iterator it = begin(); it != end(); ++it ){
386
    RegionNodeInfo* rni = it->second;
387
    if( rni->valid() ){
388
      DiseqList* del = rni->get(0);
389
      for( DiseqList::iterator it2 = del->begin(); it2 != del->end(); ++it2 ){
390
        if( (*it2).second ){
391
          num_ext_disequalities[ (*it2).first ]++;
392
        }
393
      }
394
    }
395
  }
396
}
397
398
1989
void Region::debugPrint( const char* c, bool incClique ) {
399
1989
  Debug( c ) << "Num reps: " << d_reps_size << std::endl;
400
4559
  for( Region::iterator it = begin(); it != end(); ++it ){
401
2570
    RegionNodeInfo* rni = it->second;
402
2570
    if( rni->valid() ){
403
      Node n = it->first;
404
      Debug( c ) << "   " << n << std::endl;
405
      for( int i=0; i<2; i++ ){
406
        Debug( c ) << "      " << ( i==0 ? "Ext" : "Int" ) << " disequal:";
407
        DiseqList* del = rni->get(i);
408
        for( DiseqList::iterator it2 = del->begin(); it2 != del->end(); ++it2 ){
409
          if( (*it2).second ){
410
            Debug( c ) << " " << (*it2).first;
411
          }
412
        }
413
        Debug( c ) << ", total = " << del->size() << std::endl;
414
      }
415
    }
416
  }
417
1989
  Debug( c ) << "Total disequal: " << d_total_diseq_external << " external,";
418
1989
  Debug( c ) << " " << d_total_diseq_internal << " internal." << std::endl;
419
420
1989
  if( incClique ){
421
1989
    if( !d_testClique.empty() ){
422
      Debug( c ) << "Candidate clique members: " << std::endl;
423
      Debug( c ) << "   ";
424
      for( NodeBoolMap::iterator it = d_testClique.begin();
425
           it != d_testClique.end(); ++ it ){
426
        if( (*it).second ){
427
          Debug( c ) << (*it).first << " ";
428
        }
429
      }
430
      Debug( c ) << ", size = " << d_testCliqueSize << std::endl;
431
    }
432
1989
    if( !d_splits.empty() ){
433
      Debug( c ) << "Required splits: " << std::endl;
434
      Debug( c ) << "   ";
435
      for( NodeBoolMap::iterator it = d_splits.begin(); it != d_splits.end();
436
           ++ it ){
437
        if( (*it).second ){
438
          Debug( c ) << (*it).first << " ";
439
        }
440
      }
441
      Debug( c ) << ", size = " << d_splitsSize << std::endl;
442
    }
443
  }
444
1989
}
445
446
447
SortModel::CardinalityDecisionStrategy::CardinalityDecisionStrategy(
447
447
    Node t, context::Context* satContext, Valuation valuation)
448
447
    : DecisionStrategyFmf(satContext, valuation), d_cardinality_term(t)
449
{
450
447
}
451
1153
Node SortModel::CardinalityDecisionStrategy::mkLiteral(unsigned i)
452
{
453
1153
  NodeManager* nm = NodeManager::currentNM();
454
  return nm->mkNode(
455
1153
      CARDINALITY_CONSTRAINT, d_cardinality_term, nm->mkConst(Rational(i + 1)));
456
}
457
534811
std::string SortModel::CardinalityDecisionStrategy::identify() const
458
{
459
534811
  return std::string("uf_card");
460
}
461
462
447
SortModel::SortModel(Node n,
463
                     TheoryState& state,
464
                     TheoryInferenceManager& im,
465
447
                     CardinalityExtension* thss)
466
    : d_type(n.getType()),
467
      d_state(state),
468
      d_im(im),
469
      d_thss(thss),
470
447
      d_regions_index(d_state.getSatContext(), 0),
471
447
      d_regions_map(d_state.getSatContext()),
472
447
      d_split_score(d_state.getSatContext()),
473
447
      d_disequalities_index(d_state.getSatContext(), 0),
474
447
      d_reps(d_state.getSatContext(), 0),
475
447
      d_cardinality(d_state.getSatContext(), 1),
476
447
      d_hasCard(d_state.getSatContext(), false),
477
447
      d_maxNegCard(d_state.getSatContext(), 0),
478
447
      d_initialized(d_state.getUserContext(), false),
479
4470
      d_c_dec_strat(nullptr)
480
{
481
447
  d_cardinality_term = n;
482
483
1202473
  if (options::ufssMode() == options::UfssMode::FULL)
484
  {
485
    // Register the strategy with the decision manager of the theory.
486
    // We are guaranteed that the decision manager is ready since we
487
    // construct this module during TheoryUF::finishInit.
488
1341
    d_c_dec_strat.reset(new CardinalityDecisionStrategy(
489
894
        n, d_state.getSatContext(), thss->getTheory()->getValuation()));
490
  }
491
447
}
492
493
1341
SortModel::~SortModel() {
494
2709
  for(std::vector<Region*>::iterator i = d_regions.begin();
495
2709
      i != d_regions.end(); ++i) {
496
2262
    Region* region = *i;
497
2262
    delete region;
498
  }
499
447
  d_regions.clear();
500
894
}
501
502
/** initialize */
503
4563
void SortModel::initialize()
504
{
505
4563
  if (d_c_dec_strat.get() != nullptr && !d_initialized)
506
  {
507
859
    d_initialized = true;
508
    // Strategy is user-context-dependent, since it is in sync with
509
    // user-context-dependent flag d_initialized.
510
1718
    d_thss->getTheory()->getDecisionManager()->registerStrategy(
511
859
        DecisionManager::STRAT_UF_CARD, d_c_dec_strat.get());
512
  }
513
4563
}
514
515
/** new node */
516
4251
void SortModel::newEqClass( Node n ){
517
4251
  if (!d_state.isInConflict())
518
  {
519
4251
    if( d_regions_map.find( n )==d_regions_map.end() ){
520
4251
      d_regions_map[n] = d_regions_index;
521
4251
      Debug("uf-ss") << "CardinalityExtension: New Eq Class " << n << std::endl;
522
8502
      Debug("uf-ss-debug") << d_regions_index << " " << (int)d_regions.size()
523
4251
                           << std::endl;
524
4251
      if (d_regions_index < d_regions.size())
525
      {
526
1989
        d_regions[d_regions_index]->debugPrint("uf-ss-debug", true);
527
1989
        d_regions[d_regions_index]->setValid(true);
528
1989
        Assert(d_regions[d_regions_index]->getNumReps() == 0);
529
      }else{
530
2262
        d_regions.push_back(new Region(this, d_state.getSatContext()));
531
      }
532
4251
      d_regions[d_regions_index]->addRep(n);
533
4251
      d_regions_index = d_regions_index + 1;
534
535
4251
      d_reps = d_reps + 1;
536
    }
537
  }
538
4251
}
539
540
/** merge */
541
31529
void SortModel::merge( Node a, Node b ){
542
31529
  if (d_state.isInConflict())
543
  {
544
    return;
545
  }
546
63058
  Debug("uf-ss") << "CardinalityExtension: Merging " << a << " = " << b << "..."
547
31529
                 << std::endl;
548
31529
  if (a != b)
549
  {
550
31529
    Assert(d_regions_map.find(a) != d_regions_map.end());
551
31529
    Assert(d_regions_map.find(b) != d_regions_map.end());
552
31529
    int ai = d_regions_map[a];
553
31529
    int bi = d_regions_map[b];
554
31529
    Debug("uf-ss") << "   regions: " << ai << " " << bi << std::endl;
555
31529
    if (ai != bi)
556
    {
557
28424
      if (d_regions[ai]->getNumReps() == 1)
558
      {
559
19023
        int ri = combineRegions(bi, ai);
560
19023
        d_regions[ri]->setEqual(a, b);
561
19023
        checkRegion(ri);
562
      }
563
9401
      else if (d_regions[bi]->getNumReps() == 1)
564
      {
565
9007
        int ri = combineRegions(ai, bi);
566
9007
        d_regions[ri]->setEqual(a, b);
567
9007
        checkRegion(ri);
568
      }
569
      else
570
      {
571
        // Either move a to d_regions[bi], or b to d_regions[ai].
572
394
        RegionNodeInfo* a_region_info = d_regions[ai]->getRegionInfo(a);
573
394
        RegionNodeInfo* b_region_info = d_regions[bi]->getRegionInfo(b);
574
394
        int aex = (a_region_info->getNumInternalDisequalities()
575
394
                   - getNumDisequalitiesToRegion(a, bi));
576
394
        int bex = (b_region_info->getNumInternalDisequalities()
577
394
                   - getNumDisequalitiesToRegion(b, ai));
578
        // Based on which would produce the fewest number of
579
        // external disequalities.
580
394
        if (aex < bex)
581
        {
582
154
          moveNode(a, bi);
583
154
          d_regions[bi]->setEqual(a, b);
584
        }else{
585
240
          moveNode(b, ai);
586
240
          d_regions[ai]->setEqual( a, b );
587
        }
588
394
        checkRegion(ai);
589
394
        checkRegion(bi);
590
      }
591
    }
592
    else
593
    {
594
3105
      d_regions[ai]->setEqual(a, b);
595
3105
      checkRegion(ai);
596
    }
597
31529
    d_regions_map[b] = -1;
598
  }
599
31529
  d_reps = d_reps - 1;
600
}
601
602
/** assert terms are disequal */
603
12560
void SortModel::assertDisequal( Node a, Node b, Node reason ){
604
12560
  if (d_state.isInConflict())
605
  {
606
    return;
607
  }
608
  // if they are not already disequal
609
12560
  eq::EqualityEngine* ee = d_thss->getTheory()->getEqualityEngine();
610
12560
  a = ee->getRepresentative(a);
611
12560
  b = ee->getRepresentative(b);
612
12560
  int ai = d_regions_map[a];
613
12560
  int bi = d_regions_map[b];
614
12560
  if (d_regions[ai]->isDisequal(a, b, ai == bi))
615
  {
616
    // already disequal
617
    return;
618
  }
619
25120
  Debug("uf-ss") << "Assert disequal " << a << " != " << b << "..."
620
12560
                 << std::endl;
621
25120
  Debug("uf-ss-disequal") << "Assert disequal " << a << " != " << b << "..."
622
12560
                          << std::endl;
623
  // add to list of disequalities
624
12560
  if (d_disequalities_index < d_disequalities.size())
625
  {
626
9533
    d_disequalities[d_disequalities_index] = reason;
627
  }
628
  else
629
  {
630
3027
    d_disequalities.push_back(reason);
631
  }
632
12560
  d_disequalities_index = d_disequalities_index + 1;
633
  // now, add disequalities to regions
634
12560
  Assert(d_regions_map.find(a) != d_regions_map.end());
635
12560
  Assert(d_regions_map.find(b) != d_regions_map.end());
636
12560
  Debug("uf-ss") << "   regions: " << ai << " " << bi << std::endl;
637
12560
  if (ai == bi)
638
  {
639
    // internal disequality
640
452
    d_regions[ai]->setDisequal(a, b, 1, true);
641
452
    d_regions[ai]->setDisequal(b, a, 1, true);
642
    // do not need to check if it needs to combine (no new ext. disequalities)
643
452
    checkRegion(ai, false);
644
  }
645
  else
646
  {
647
    // external disequality
648
12108
    d_regions[ai]->setDisequal(a, b, 0, true);
649
12108
    d_regions[bi]->setDisequal(b, a, 0, true);
650
12108
    checkRegion(ai);
651
12108
    checkRegion(bi);
652
  }
653
}
654
655
bool SortModel::areDisequal( Node a, Node b ) {
656
  Assert(a == d_thss->getTheory()->getEqualityEngine()->getRepresentative(a));
657
  Assert(b == d_thss->getTheory()->getEqualityEngine()->getRepresentative(b));
658
  if( d_regions_map.find( a )!=d_regions_map.end() &&
659
      d_regions_map.find( b )!=d_regions_map.end() ){
660
    int ai = d_regions_map[a];
661
    int bi = d_regions_map[b];
662
    return d_regions[ai]->isDisequal(a, b, ai==bi ? 1 : 0);
663
  }else{
664
    return false;
665
  }
666
}
667
668
282235
void SortModel::check(Theory::Effort level)
669
{
670
282235
  Assert(options::ufssMode() == options::UfssMode::FULL);
671
282235
  if (!d_hasCard && d_state.isInConflict())
672
  {
673
    // not necessary to check
674
    return;
675
  }
676
564470
  Debug("uf-ss") << "CardinalityExtension: Check " << level << " " << d_type
677
282235
                 << std::endl;
678
282235
  if (level == Theory::EFFORT_FULL)
679
  {
680
9162
    Debug("fmf-full-check") << std::endl;
681
18324
    Debug("fmf-full-check")
682
9162
        << "Full check for SortModel " << d_type << ", status : " << std::endl;
683
9162
    debugPrint("fmf-full-check");
684
9162
    Debug("fmf-full-check") << std::endl;
685
  }
686
282235
  if (d_reps <= (unsigned)d_cardinality)
687
  {
688
213928
    Debug("uf-ss-debug") << "We have " << d_reps << " representatives for type "
689
106964
                         << d_type << ", <= " << d_cardinality << std::endl;
690
106964
    if( level==Theory::EFFORT_FULL ){
691
9622
      Debug("uf-ss-sat") << "We have " << d_reps << " representatives for type "
692
4811
                         << d_type << ", <= " << d_cardinality << std::endl;
693
    }
694
106964
    return;
695
  }
696
  // first check if we can generate a clique conflict
697
  // do a check within each region
698
1574901
  for (size_t i = 0; i < d_regions_index; i++)
699
  {
700
1400340
    if (d_regions[i]->valid())
701
    {
702
1621952
      std::vector<Node> clique;
703
811331
      if (d_regions[i]->check(level, d_cardinality, clique))
704
      {
705
        // add clique lemma
706
710
        addCliqueLemma(clique);
707
710
        return;
708
      }
709
      else
710
      {
711
810621
        Trace("uf-ss-debug") << "No clique in Region #" << i << std::endl;
712
      }
713
    }
714
  }
715
  // do splitting on demand
716
174561
  bool addedLemma = false;
717
174561
  if (level == Theory::EFFORT_FULL)
718
  {
719
4319
    Trace("uf-ss-debug") << "Add splits?" << std::endl;
720
    // see if we have any recommended splits from large regions
721
56172
    for (size_t i = 0; i < d_regions_index; i++)
722
    {
723
51853
      if (d_regions[i]->valid() && d_regions[i]->getNumReps() > d_cardinality)
724
      {
725
1754
        int sp = addSplit(d_regions[i]);
726
1754
        if (sp == 1)
727
        {
728
1754
          addedLemma = true;
729
        }
730
        else if (sp == -1)
731
        {
732
          check(level);
733
          return;
734
        }
735
      }
736
    }
737
  }
738
  // If no added lemmas, force continuation via combination of regions.
739
174561
  if (level != Theory::EFFORT_FULL || addedLemma)
740
  {
741
171996
    return;
742
  }
743
  // check at full effort
744
2565
  Trace("uf-ss-debug") << "No splits added. " << d_cardinality << std::endl;
745
2565
  Trace("uf-ss-si") << "Must combine region" << std::endl;
746
2565
  bool recheck = false;
747
2565
  SortInference* si = d_state.getSortInference();
748
2565
  if (si != nullptr)
749
  {
750
    // If sort inference is enabled, search for regions with same sort.
751
48
    std::map<int, int> sortsFound;
752
224
    for (size_t i = 0; i < d_regions_index; i++)
753
    {
754
224
      if (d_regions[i]->valid())
755
      {
756
72
        Node op = d_regions[i]->frontKey();
757
48
        int sort_id = si->getSortId(op);
758
48
        if (sortsFound.find(sort_id) != sortsFound.end())
759
        {
760
48
          Debug("fmf-full-check") << "Combined regions " << i << " "
761
24
                                  << sortsFound[sort_id] << std::endl;
762
24
          combineRegions(sortsFound[sort_id], i);
763
24
          recheck = true;
764
24
          break;
765
        }
766
        else
767
        {
768
24
          sortsFound[sort_id] = i;
769
        }
770
      }
771
    }
772
  }
773
2565
  if (!recheck)
774
  {
775
    // naive strategy, force region combination involving the first
776
    // valid region
777
8074
    for (size_t i = 0; i < d_regions_index; i++)
778
    {
779
8074
      if (d_regions[i]->valid())
780
      {
781
2541
        int fcr = forceCombineRegion(i, false);
782
5082
        Debug("fmf-full-check")
783
2541
            << "Combined regions " << i << " " << fcr << std::endl;
784
5082
        Trace("uf-ss-debug")
785
2541
            << "Combined regions " << i << " " << fcr << std::endl;
786
2541
        recheck = true;
787
2541
        break;
788
      }
789
    }
790
  }
791
2565
  if (recheck)
792
  {
793
2565
    Trace("uf-ss-debug") << "Must recheck." << std::endl;
794
2565
    check(level);
795
  }
796
}
797
798
412
void SortModel::presolve() {
799
412
  d_initialized = false;
800
412
}
801
802
788
int SortModel::getNumDisequalitiesToRegion( Node n, int ri ){
803
788
  int ni = d_regions_map[n];
804
788
  int counter = 0;
805
788
  DiseqList* del = d_regions[ni]->getRegionInfo(n)->get(0);
806
2304
  for( DiseqList::iterator it = del->begin(); it != del->end(); ++it ){
807
1516
    if( (*it).second ){
808
699
      if( d_regions_map[ (*it).first ]==ri ){
809
615
        counter++;
810
      }
811
    }
812
  }
813
788
  return counter;
814
}
815
816
8763
void SortModel::getDisequalitiesToRegions(int ri,
817
                                          std::map< int, int >& regions_diseq)
818
{
819
8763
  Region* region = d_regions[ri];
820
103380
  for(Region::iterator it = region->begin(); it != region->end(); ++it ){
821
94617
    if( it->second->valid() ){
822
24612
      DiseqList* del = it->second->get(0);
823
199758
      for( DiseqList::iterator it2 = del->begin(); it2 != del->end(); ++it2 ){
824
175146
        if( (*it2).second ){
825
120507
          Assert(isValid(d_regions_map[(*it2).first]));
826
          //Notice() << "Found disequality with " << (*it2).first << ", region = " << d_regions_map[ (*it2).first ] << std::endl;
827
120507
          regions_diseq[ d_regions_map[ (*it2).first ] ]++;
828
        }
829
      }
830
    }
831
  }
832
8763
}
833
834
void SortModel::setSplitScore( Node n, int s ){
835
  if( d_split_score.find( n )!=d_split_score.end() ){
836
    int ss = d_split_score[ n ];
837
    d_split_score[ n ] = s>ss ? s : ss;
838
  }else{
839
    d_split_score[ n ] = s;
840
  }
841
  for( int i=0; i<(int)n.getNumChildren(); i++ ){
842
    setSplitScore( n[i], s+1 );
843
  }
844
}
845
846
8604
void SortModel::assertCardinality(uint32_t c, bool val)
847
{
848
8604
  if (!d_state.isInConflict())
849
  {
850
17208
    Trace("uf-ss-assert")
851
8604
        << "Assert cardinality " << d_type << " " << c << " " << val
852
8604
        << " level = "
853
8604
        << d_thss->getTheory()->getValuation().getAssertionLevel() << std::endl;
854
8604
    Assert(c > 0);
855
17087
    Node cl = getCardinalityLiteral( c );
856
8604
    if( val ){
857
7466
      bool doCheckRegions = !d_hasCard;
858
7466
      bool prevHasCard = d_hasCard;
859
7466
      d_hasCard = true;
860
7466
      if (!prevHasCard || c < d_cardinality)
861
      {
862
7464
        d_cardinality = c;
863
7464
        simpleCheckCardinality();
864
7464
        if (d_state.isInConflict())
865
        {
866
121
          return;
867
        }
868
      }
869
      //should check all regions now
870
7345
      if (doCheckRegions)
871
      {
872
46066
        for (size_t i = 0; i < d_regions_index; i++)
873
        {
874
38752
          if( d_regions[i]->valid() ){
875
32595
            checkRegion( i );
876
32595
            if (d_state.isInConflict())
877
            {
878
              return;
879
            }
880
          }
881
        }
882
      }
883
      // we assert it positively, if its beyond the bound, abort
884
22035
      if (options::ufssAbortCardinality() >= 0
885
7345
          && c >= static_cast<uint32_t>(options::ufssAbortCardinality()))
886
      {
887
        std::stringstream ss;
888
        ss << "Maximum cardinality (" << options::ufssAbortCardinality()
889
           << ")  for finite model finding exceeded." << std::endl;
890
        throw LogicException(ss.str());
891
      }
892
    }
893
    else
894
    {
895
1138
      if (c > d_maxNegCard.get())
896
      {
897
2036
        Trace("uf-ss-com-card-debug") << "Maximum negative cardinality for "
898
1018
                                      << d_type << " is now " << c << std::endl;
899
1018
        d_maxNegCard.set(c);
900
1018
        simpleCheckCardinality();
901
      }
902
    }
903
  }
904
}
905
906
97949
void SortModel::checkRegion( int ri, bool checkCombine ){
907
97949
  if( isValid(ri) && d_hasCard ){
908
92585
    Assert(d_cardinality > 0);
909
92585
    if( checkCombine && d_regions[ri]->getMustCombine( d_cardinality ) ){
910
8763
      int riNew = forceCombineRegion( ri, true );
911
8763
      if( riNew>=0 ){
912
8763
        checkRegion( riNew, checkCombine );
913
      }
914
    }
915
    //now check if region is in conflict
916
185170
    std::vector< Node > clique;
917
92585
    if( d_regions[ri]->check( Theory::EFFORT_STANDARD, d_cardinality, clique ) ){
918
      //explain clique
919
1830
      addCliqueLemma(clique);
920
    }
921
  }
922
97949
}
923
924
11304
int SortModel::forceCombineRegion( int ri, bool useDensity ){
925
11304
  if( !useDensity ){
926
22329
    for( int i=0; i<(int)d_regions_index; i++ ){
927
22329
      if( ri!=i && d_regions[i]->valid() ){
928
2541
        return combineRegions( ri, i );
929
      }
930
    }
931
    return -1;
932
  }else{
933
    //this region must merge with another
934
8763
    if( Debug.isOn("uf-ss-check-region") ){
935
      Debug("uf-ss-check-region") << "We must combine Region #" << ri << ". " << std::endl;
936
      d_regions[ri]->debugPrint("uf-ss-check-region");
937
    }
938
    //take region with maximum disequality density
939
8763
    double maxScore = 0;
940
8763
    int maxRegion = -1;
941
17526
    std::map< int, int > regions_diseq;
942
8763
    getDisequalitiesToRegions( ri, regions_diseq );
943
55824
    for( std::map< int, int >::iterator it = regions_diseq.begin(); it != regions_diseq.end(); ++it ){
944
47061
      Debug("uf-ss-check-region") << it->first << " : " << it->second << std::endl;
945
    }
946
55824
    for( std::map< int, int >::iterator it = regions_diseq.begin(); it != regions_diseq.end(); ++it ){
947
47061
      Assert(it->first != ri);
948
47061
      Assert(isValid(it->first));
949
47061
      Assert(d_regions[it->first]->getNumReps() > 0);
950
47061
      double tempScore = double(it->second)/double(d_regions[it->first]->getNumReps() );
951
47061
      if( tempScore>maxScore ){
952
10792
        maxRegion = it->first;
953
10792
        maxScore = tempScore;
954
      }
955
    }
956
8763
    if( maxRegion!=-1 ){
957
8763
      if( Debug.isOn("uf-ss-check-region") ){
958
        Debug("uf-ss-check-region") << "Combine with region #" << maxRegion << ":" << std::endl;
959
        d_regions[maxRegion]->debugPrint("uf-ss-check-region");
960
      }
961
8763
      return combineRegions( ri, maxRegion );
962
    }
963
    return -1;
964
  }
965
}
966
967
968
39358
int SortModel::combineRegions( int ai, int bi ){
969
39358
  Debug("uf-ss-region") << "uf-ss: Combine Region #" << bi << " with Region #" << ai << std::endl;
970
39358
  Assert(isValid(ai) && isValid(bi));
971
39358
  Region* region_bi = d_regions[bi];
972
208358
  for(Region::iterator it = region_bi->begin(); it != region_bi->end(); ++it){
973
169000
    Region::RegionNodeInfo* rni = it->second;
974
169000
    if( rni->valid() ){
975
41916
      d_regions_map[ it->first ] = ai;
976
    }
977
  }
978
  //update regions disequal DO_THIS?
979
39358
  d_regions[ai]->combine( d_regions[bi] );
980
39358
  d_regions[bi]->setValid( false );
981
39358
  return ai;
982
}
983
984
394
void SortModel::moveNode( Node n, int ri ){
985
394
  Debug("uf-ss-region") << "uf-ss: Move node " << n << " to Region #" << ri << std::endl;
986
394
  Assert(isValid(d_regions_map[n]));
987
394
  Assert(isValid(ri));
988
  //move node to region ri
989
394
  d_regions[ri]->takeNode( d_regions[ d_regions_map[n] ], n );
990
394
  d_regions_map[n] = ri;
991
394
}
992
993
1754
int SortModel::addSplit(Region* r)
994
{
995
3508
  Node s;
996
1754
  if( r->hasSplits() ){
997
    //take the first split you find
998
9261
    for( Region::split_iterator it = r->begin_splits();
999
9261
         it != r->end_splits(); ++it ){
1000
9261
      if( (*it).second ){
1001
1754
        s = (*it).first;
1002
1754
        break;
1003
      }
1004
    }
1005
1754
    Assert(s != Node::null());
1006
  }
1007
1754
  if (!s.isNull() ){
1008
    //add lemma to output channel
1009
1754
    Assert(s.getKind() == EQUAL);
1010
3508
    Node ss = Rewriter::rewrite( s );
1011
1754
    if( ss.getKind()!=EQUAL ){
1012
      Node b_t = NodeManager::currentNM()->mkConst( true );
1013
      Node b_f = NodeManager::currentNM()->mkConst( false );
1014
      if( ss==b_f ){
1015
        Trace("uf-ss-lemma") << "....Assert disequal directly : "
1016
                             << s[0] << " " << s[1] << std::endl;
1017
        assertDisequal( s[0], s[1], b_t );
1018
        return -1;
1019
      }else{
1020
        Trace("uf-ss-warn") << "Split on unknown literal : " << ss << std::endl;
1021
      }
1022
      if (ss == b_t)
1023
      {
1024
        CVC4Message() << "Bad split " << s << std::endl;
1025
        AlwaysAssert(false);
1026
      }
1027
    }
1028
1754
    if (Trace.isOn("uf-ss-split-si"))
1029
    {
1030
      SortInference* si = d_state.getSortInference();
1031
      if (si != nullptr)
1032
      {
1033
        for (size_t i = 0; i < 2; i++)
1034
        {
1035
          int sid = si->getSortId(ss[i]);
1036
          Trace("uf-ss-split-si") << sid << " ";
1037
        }
1038
        Trace("uf-ss-split-si") << std::endl;
1039
      }
1040
    }
1041
    //Trace("uf-ss-lemma") << d_th->getEqualityEngine()->areEqual( s[0], s[1] ) << " ";
1042
    //Trace("uf-ss-lemma") << d_th->getEqualityEngine()->areDisequal( s[0], s[1] ) << std::endl;
1043
    //Trace("uf-ss-lemma") << s[0].getType() << " " << s[1].getType() << std::endl;
1044
    //Notice() << "*** Split on " << s << std::endl;
1045
    //split on the equality s
1046
3508
    Node lem = NodeManager::currentNM()->mkNode( kind::OR, ss, ss.negate() );
1047
    // send lemma, with caching
1048
1754
    if (d_im.lemma(lem, InferenceId::UF_CARD_SPLIT))
1049
    {
1050
1754
      Trace("uf-ss-lemma") << "*** Split on " << s << std::endl;
1051
      //tell the sat solver to explore the equals branch first
1052
1754
      d_im.requirePhase(ss, true);
1053
1754
      ++( d_thss->d_statistics.d_split_lemmas );
1054
    }
1055
1754
    return 1;
1056
  }else{
1057
    return 0;
1058
  }
1059
}
1060
1061
2540
void SortModel::addCliqueLemma(std::vector<Node>& clique)
1062
{
1063
2540
  Assert(d_hasCard);
1064
2540
  Assert(d_cardinality > 0);
1065
8696
  while (clique.size() > d_cardinality + 1)
1066
  {
1067
3078
    clique.pop_back();
1068
  }
1069
  // add as lemma
1070
5080
  std::vector<Node> eqs;
1071
15048
  for (unsigned i = 0, size = clique.size(); i < size; i++)
1072
  {
1073
58674
    for (unsigned j = 0; j < i; j++)
1074
    {
1075
46166
      eqs.push_back(clique[i].eqNode(clique[j]));
1076
    }
1077
  }
1078
2540
  eqs.push_back(d_cardinality_literal[d_cardinality].notNode());
1079
5080
  Node lem = NodeManager::currentNM()->mkNode(OR, eqs);
1080
  // send lemma, with caching
1081
2540
  if (d_im.lemma(lem, InferenceId::UF_CARD_CLIQUE))
1082
  {
1083
2540
    Trace("uf-ss-lemma") << "*** Add clique lemma " << lem << std::endl;
1084
2540
    ++(d_thss->d_statistics.d_clique_lemmas);
1085
  }
1086
2540
}
1087
1088
8482
void SortModel::simpleCheckCardinality() {
1089
8482
  if( d_maxNegCard.get()!=0 && d_hasCard.get() && d_cardinality.get()<d_maxNegCard.get() ){
1090
248
    Node lem = NodeManager::currentNM()->mkNode( AND, getCardinalityLiteral( d_cardinality.get() ),
1091
496
                                                      getCardinalityLiteral( d_maxNegCard.get() ).negate() );
1092
124
    Trace("uf-ss-lemma") << "*** Simple cardinality conflict : " << lem << std::endl;
1093
124
    d_im.conflict(lem, InferenceId::UF_CARD_SIMPLE_CONFLICT);
1094
  }
1095
8482
}
1096
1097
9162
void SortModel::debugPrint( const char* c ){
1098
9162
  if( Debug.isOn( c ) ){
1099
    Debug( c ) << "Number of reps = " << d_reps << std::endl;
1100
    Debug( c ) << "Cardinality req = " << d_cardinality << std::endl;
1101
    unsigned debugReps = 0;
1102
    for( unsigned i=0; i<d_regions_index; i++ ){
1103
      Region* region = d_regions[i];
1104
      if( region->valid() ){
1105
        Debug( c ) << "Region #" << i << ": " << std::endl;
1106
        region->debugPrint( c, true );
1107
        Debug( c ) << std::endl;
1108
        for( Region::iterator it = region->begin(); it != region->end(); ++it ){
1109
          if( it->second->valid() ){
1110
            if( d_regions_map[ it->first ]!=(int)i ){
1111
              Debug( c ) << "***Bad regions map : " << it->first
1112
                         << " " << d_regions_map[ it->first ].get() << std::endl;
1113
            }
1114
          }
1115
        }
1116
        debugReps += region->getNumReps();
1117
      }
1118
    }
1119
1120
    if( debugReps!=d_reps ){
1121
      Debug( c ) << "***Bad reps: " << d_reps << ", "
1122
                 << "actual = " << debugReps << std::endl;
1123
    }
1124
  }
1125
9162
}
1126
1127
1825
bool SortModel::checkLastCall()
1128
{
1129
1825
  TheoryModel* m = d_state.getModel();
1130
1825
  if( Trace.isOn("uf-ss-warn") ){
1131
    std::vector< Node > eqcs;
1132
    eq::EqClassesIterator eqcs_i =
1133
        eq::EqClassesIterator(m->getEqualityEngine());
1134
    while( !eqcs_i.isFinished() ){
1135
      Node eqc = (*eqcs_i);
1136
      if( eqc.getType()==d_type ){
1137
        if( std::find( eqcs.begin(), eqcs.end(), eqc )==eqcs.end() ){
1138
          eqcs.push_back( eqc );
1139
          //we must ensure that this equivalence class has been accounted for
1140
          if( d_regions_map.find( eqc )==d_regions_map.end() ){
1141
            Trace("uf-ss-warn") << "WARNING : equivalence class " << eqc << " unaccounted for." << std::endl;
1142
            Trace("uf-ss-warn") << "  type : " << d_type << std::endl;
1143
            Trace("uf-ss-warn") << "  kind : " << eqc.getKind() << std::endl;
1144
          }
1145
        }
1146
      }
1147
      ++eqcs_i;
1148
    }
1149
  }
1150
1825
  RepSet* rs = m->getRepSetPtr();
1151
1825
  size_t nReps = rs->getNumRepresentatives(d_type);
1152
1825
  if (nReps != d_maxNegCard + 1)
1153
  {
1154
30
    Trace("uf-ss-warn") << "WARNING : Model does not have same # "
1155
15
                           "representatives as cardinality for "
1156
15
                        << d_type << "." << std::endl;
1157
30
    Trace("uf-ss-warn") << "   Max neg cardinality : " << d_maxNegCard
1158
15
                        << std::endl;
1159
15
    Trace("uf-ss-warn") << "   # Reps : " << nReps << std::endl;
1160
15
    if (d_maxNegCard >= nReps)
1161
    {
1162
315
      while (d_fresh_aloc_reps.size() <= d_maxNegCard)
1163
      {
1164
300
        std::stringstream ss;
1165
150
        ss << "r_" << d_type << "_";
1166
        Node nn = NodeManager::currentNM()->mkSkolem(
1167
300
            ss.str(), d_type, "enumeration to meet negative card constraint");
1168
150
        d_fresh_aloc_reps.push_back( nn );
1169
      }
1170
15
      if (d_maxNegCard == 0)
1171
      {
1172
        rs->d_type_reps[d_type].push_back(d_fresh_aloc_reps[0]);
1173
      }
1174
      else
1175
      {
1176
        //must add lemma
1177
30
        std::vector< Node > force_cl;
1178
165
        for (size_t i = 0; i <= d_maxNegCard; i++)
1179
        {
1180
1309
          for (size_t j = (i + 1); j <= d_maxNegCard; j++)
1181
          {
1182
1159
            force_cl.push_back(
1183
2318
                d_fresh_aloc_reps[i].eqNode(d_fresh_aloc_reps[j]).negate());
1184
          }
1185
        }
1186
30
        Node cl = getCardinalityLiteral( d_maxNegCard );
1187
        Node lem = NodeManager::currentNM()->mkNode(
1188
30
            OR, cl, NodeManager::currentNM()->mkAnd(force_cl));
1189
15
        Trace("uf-ss-lemma") << "*** Enforce negative cardinality constraint lemma : " << lem << std::endl;
1190
15
        d_im.lemma(lem, InferenceId::UF_CARD_ENFORCE_NEGATIVE);
1191
15
        return false;
1192
      }
1193
    }
1194
  }
1195
1810
  return true;
1196
}
1197
1198
int SortModel::getNumRegions(){
1199
  int count = 0;
1200
  for( int i=0; i<(int)d_regions_index; i++ ){
1201
    if( d_regions[i]->valid() ){
1202
      count++;
1203
    }
1204
  }
1205
  return count;
1206
}
1207
1208
10562
Node SortModel::getCardinalityLiteral(uint32_t c)
1209
{
1210
10562
  Assert(c > 0);
1211
10562
  std::map<uint32_t, Node>::iterator itcl = d_cardinality_literal.find(c);
1212
10562
  if (itcl != d_cardinality_literal.end())
1213
  {
1214
9632
    return itcl->second;
1215
  }
1216
  // get the literal from the decision strategy
1217
1860
  Node lit = d_c_dec_strat->getLiteral(c - 1);
1218
930
  d_cardinality_literal[c] = lit;
1219
1220
  // return the literal
1221
930
  return lit;
1222
}
1223
1224
250
CardinalityExtension::CardinalityExtension(TheoryState& state,
1225
                                           TheoryInferenceManager& im,
1226
250
                                           TheoryUF* th)
1227
    : d_state(state),
1228
      d_im(im),
1229
      d_th(th),
1230
      d_rep_model(),
1231
      d_min_pos_com_card(state.getSatContext(), 0),
1232
      d_min_pos_com_card_set(state.getSatContext(), false),
1233
      d_cc_dec_strat(nullptr),
1234
250
      d_initializedCombinedCardinality(state.getUserContext(), false),
1235
250
      d_card_assertions_eqv_lemma(state.getUserContext()),
1236
      d_min_pos_tn_master_card(state.getSatContext(), 0),
1237
      d_min_pos_tn_master_card_set(state.getSatContext(), false),
1238
750
      d_rel_eqc(state.getSatContext())
1239
{
1240
12044
  if (options::ufssMode() == options::UfssMode::FULL && options::ufssFairness())
1241
  {
1242
    // Register the strategy with the decision manager of the theory.
1243
    // We are guaranteed that the decision manager is ready since we
1244
    // construct this module during TheoryUF::finishInit.
1245
726
    d_cc_dec_strat.reset(new CombinedCardinalityDecisionStrategy(
1246
484
        state.getSatContext(), th->getValuation()));
1247
  }
1248
250
}
1249
1250
500
CardinalityExtension::~CardinalityExtension()
1251
{
1252
697
  for (std::map<TypeNode, SortModel*>::iterator it = d_rep_model.begin();
1253
697
       it != d_rep_model.end(); ++it) {
1254
447
    delete it->second;
1255
  }
1256
250
}
1257
1258
/** ensure eqc */
1259
void CardinalityExtension::ensureEqc(SortModel* c, Node a)
1260
{
1261
  if( !hasEqc( a ) ){
1262
    d_rel_eqc[a] = true;
1263
    Trace("uf-ss-solver") << "CardinalityExtension: New eq class " << a << " : "
1264
                          << a.getType() << std::endl;
1265
    c->newEqClass( a );
1266
    Trace("uf-ss-solver") << "CardinalityExtension: Done New eq class."
1267
                          << std::endl;
1268
  }
1269
}
1270
1271
void CardinalityExtension::ensureEqcRec(Node n)
1272
{
1273
  if( !hasEqc( n ) ){
1274
    SortModel* c = getSortModel( n );
1275
    if( c ){
1276
      ensureEqc( c, n );
1277
    }
1278
    for( unsigned i=0; i<n.getNumChildren(); i++ ){
1279
      ensureEqcRec( n[i] );
1280
    }
1281
  }
1282
}
1283
1284
/** has eqc */
1285
bool CardinalityExtension::hasEqc(Node a)
1286
{
1287
  NodeBoolMap::iterator it = d_rel_eqc.find( a );
1288
  return it!=d_rel_eqc.end() && (*it).second;
1289
}
1290
1291
/** new node */
1292
30484
void CardinalityExtension::newEqClass(Node a)
1293
{
1294
30484
  SortModel* c = getSortModel( a );
1295
30484
  if( c ){
1296
8502
    Trace("uf-ss-solver") << "CardinalityExtension: New eq class " << a << " : "
1297
4251
                          << a.getType() << std::endl;
1298
4251
    c->newEqClass( a );
1299
8502
    Trace("uf-ss-solver") << "CardinalityExtension: Done New eq class."
1300
4251
                          << std::endl;
1301
  }
1302
30484
}
1303
1304
/** merge */
1305
394220
void CardinalityExtension::merge(Node a, Node b)
1306
{
1307
  //TODO: ensure they are relevant
1308
394220
  SortModel* c = getSortModel( a );
1309
394220
  if( c ){
1310
63058
    Trace("uf-ss-solver") << "CardinalityExtension: Merge " << a << " " << b
1311
31529
                          << " : " << a.getType() << std::endl;
1312
31529
    c->merge( a, b );
1313
31529
    Trace("uf-ss-solver") << "CardinalityExtension: Done Merge." << std::endl;
1314
  }
1315
394220
}
1316
1317
/** assert terms are disequal */
1318
24443
void CardinalityExtension::assertDisequal(Node a, Node b, Node reason)
1319
{
1320
24443
  SortModel* c = getSortModel( a );
1321
24443
  if( c ){
1322
25120
    Trace("uf-ss-solver") << "CardinalityExtension: Assert disequal " << a
1323
12560
                          << " " << b << " : " << a.getType() << std::endl;
1324
12560
    c->assertDisequal( a, b, reason );
1325
25120
    Trace("uf-ss-solver") << "CardinalityExtension: Done Assert disequal."
1326
12560
                          << std::endl;
1327
  }
1328
24443
}
1329
1330
/** assert a node */
1331
274692
void CardinalityExtension::assertNode(Node n, bool isDecision)
1332
{
1333
274692
  Trace("uf-ss") << "Assert " << n << " " << isDecision << std::endl;
1334
274692
  bool polarity = n.getKind() != kind::NOT;
1335
549384
  TNode lit = polarity ? n : n[0];
1336
274692
  if (options::ufssMode() == options::UfssMode::FULL)
1337
  {
1338
150190
    if( lit.getKind()==CARDINALITY_CONSTRAINT ){
1339
17222
      TypeNode tn = lit[0].getType();
1340
8611
      Assert(tn.isSort());
1341
8611
      Assert(d_rep_model[tn]);
1342
      uint32_t nCard =
1343
8611
          lit[1].getConst<Rational>().getNumerator().getUnsignedInt();
1344
17222
      Node ct = d_rep_model[tn]->getCardinalityTerm();
1345
8611
      Trace("uf-ss-debug") << "...check cardinality terms : " << lit[0] << " " << ct << std::endl;
1346
8611
      if( lit[0]==ct ){
1347
8604
        if( options::ufssFairnessMonotone() ){
1348
54
          SortInference* si = d_state.getSortInference();
1349
54
          Trace("uf-ss-com-card-debug") << "...set master/slave" << std::endl;
1350
54
          if( tn!=d_tn_mono_master ){
1351
42
            std::map< TypeNode, bool >::iterator it = d_tn_mono_slave.find( tn );
1352
42
            if( it==d_tn_mono_slave.end() ){
1353
              bool isMonotonic;
1354
10
              if (si != nullptr)
1355
              {
1356
                isMonotonic = si->isMonotonic(tn);
1357
              }else{
1358
                //if ground, everything is monotonic
1359
10
                isMonotonic = true;
1360
              }
1361
10
              if( isMonotonic ){
1362
10
                if( d_tn_mono_master.isNull() ){
1363
4
                  Trace("uf-ss-com-card-debug") << "uf-ss-fair-monotone: Set master : " << tn << std::endl;
1364
4
                  d_tn_mono_master = tn;
1365
                }else{
1366
6
                  Trace("uf-ss-com-card-debug") << "uf-ss-fair-monotone: Set slave : " << tn << std::endl;
1367
6
                  d_tn_mono_slave[tn] = true;
1368
                }
1369
              }else{
1370
                Trace("uf-ss-com-card-debug") << "uf-ss-fair-monotone: Set non-monotonic : " << tn << std::endl;
1371
                d_tn_mono_slave[tn] = false;
1372
              }
1373
            }
1374
          }
1375
          //set the minimum positive cardinality for master if necessary
1376
54
          if( polarity && tn==d_tn_mono_master ){
1377
16
            Trace("uf-ss-com-card-debug") << "...set min positive cardinality" << std::endl;
1378
32
            if (!d_min_pos_tn_master_card_set.get()
1379
16
                || nCard < d_min_pos_tn_master_card.get())
1380
            {
1381
16
              d_min_pos_tn_master_card_set.set(true);
1382
16
              d_min_pos_tn_master_card.set( nCard );
1383
            }
1384
          }
1385
        }
1386
8604
        Trace("uf-ss-com-card-debug") << "...assert cardinality" << std::endl;
1387
8604
        d_rep_model[tn]->assertCardinality(nCard, polarity);
1388
        //check if combined cardinality is violated
1389
8604
        checkCombinedCardinality();
1390
      }else{
1391
        //otherwise, make equal via lemma
1392
7
        if( d_card_assertions_eqv_lemma.find( lit )==d_card_assertions_eqv_lemma.end() ){
1393
14
          Node eqv_lit = NodeManager::currentNM()->mkNode( CARDINALITY_CONSTRAINT, ct, lit[1] );
1394
7
          eqv_lit = lit.eqNode( eqv_lit );
1395
7
          Trace("uf-ss-lemma") << "*** Cardinality equiv lemma : " << eqv_lit << std::endl;
1396
7
          d_im.lemma(eqv_lit, InferenceId::UF_CARD_EQUIV);
1397
7
          d_card_assertions_eqv_lemma[lit] = true;
1398
        }
1399
      }
1400
141579
    }else if( lit.getKind()==COMBINED_CARDINALITY_CONSTRAINT ){
1401
3412
      if( polarity ){
1402
        //safe to assume int here
1403
        uint32_t nCard =
1404
2948
            lit[0].getConst<Rational>().getNumerator().getUnsignedInt();
1405
2948
        if (!d_min_pos_com_card_set.get() || nCard < d_min_pos_com_card.get())
1406
        {
1407
2948
          d_min_pos_com_card_set.set(true);
1408
2948
          d_min_pos_com_card.set( nCard );
1409
2948
          checkCombinedCardinality();
1410
        }
1411
      }
1412
    }else{
1413
138167
      if( Trace.isOn("uf-ss-warn") ){
1414
        ////FIXME: this is too strict: theory propagations are showing up as isDecision=true, but
1415
        ////       a theory propagation is not a decision.
1416
        if( isDecision ){
1417
          for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
1418
            if( !it->second->hasCardinalityAsserted() ){
1419
              Trace("uf-ss-warn") << "WARNING: Assert " << n << " as a decision before cardinality for " << it->first << "." << std::endl;
1420
              // CVC4Message() << "Error: constraint asserted before cardinality
1421
              // for " << it->first << std::endl; Unimplemented();
1422
            }
1423
          }
1424
        }
1425
      }
1426
    }
1427
  }
1428
  else
1429
  {
1430
124502
    if( lit.getKind()==CARDINALITY_CONSTRAINT || lit.getKind()==COMBINED_CARDINALITY_CONSTRAINT ){
1431
      // cardinality constraint from user input, set incomplete
1432
2
      Trace("uf-ss") << "Literal " << lit << " not handled when uf ss mode is not FULL, set incomplete." << std::endl;
1433
2
      d_im.setIncomplete();
1434
    }
1435
  }
1436
274692
  Trace("uf-ss") << "Assert: done " << n << " " << isDecision << std::endl;
1437
274692
}
1438
1439
bool CardinalityExtension::areDisequal(Node a, Node b)
1440
{
1441
  if( a==b ){
1442
    return false;
1443
  }
1444
  eq::EqualityEngine* ee = d_th->getEqualityEngine();
1445
  a = ee->getRepresentative(a);
1446
  b = ee->getRepresentative(b);
1447
  if (ee->areDisequal(a, b, false))
1448
  {
1449
    return true;
1450
  }
1451
  SortModel* c = getSortModel(a);
1452
  if (c)
1453
  {
1454
    return c->areDisequal(a, b);
1455
  }
1456
  return false;
1457
}
1458
1459
/** check */
1460
127301
void CardinalityExtension::check(Theory::Effort level)
1461
{
1462
127301
  if (level == Theory::EFFORT_LAST_CALL)
1463
  {
1464
    // if last call, call last call check for each sort
1465
2750
    for (std::pair<const TypeNode, SortModel*>& r : d_rep_model)
1466
    {
1467
1825
      if (!r.second->checkLastCall())
1468
      {
1469
15
        break;
1470
      }
1471
    }
1472
940
    return;
1473
  }
1474
126361
  if (!d_state.isInConflict())
1475
  {
1476
126361
    if (options::ufssMode() == options::UfssMode::FULL)
1477
    {
1478
119694
      Trace("uf-ss-solver")
1479
59847
          << "CardinalityExtension: check " << level << std::endl;
1480
59847
      if (level == Theory::EFFORT_FULL)
1481
      {
1482
3248
        if (Debug.isOn("uf-ss-debug"))
1483
        {
1484
          debugPrint("uf-ss-debug");
1485
        }
1486
3248
        if (Trace.isOn("uf-ss-state"))
1487
        {
1488
          Trace("uf-ss-state")
1489
              << "CardinalityExtension::check " << level << std::endl;
1490
          for (std::pair<const TypeNode, SortModel*>& rm : d_rep_model)
1491
          {
1492
            Trace("uf-ss-state") << "  " << rm.first << " has cardinality "
1493
                                 << rm.second->getCardinality() << std::endl;
1494
          }
1495
        }
1496
      }
1497
339517
      for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
1498
279670
        it->second->check(level);
1499
279670
        if (d_state.isInConflict())
1500
        {
1501
          break;
1502
        }
1503
      }
1504
    }
1505
66514
    else if (options::ufssMode() == options::UfssMode::NO_MINIMAL)
1506
    {
1507
66514
      if( level==Theory::EFFORT_FULL ){
1508
        // split on an equality between two equivalence classes (at most one per type)
1509
1754
        std::map< TypeNode, std::vector< Node > > eqc_list;
1510
1754
        std::map< TypeNode, bool > type_proc;
1511
877
        eq::EqClassesIterator eqcs_i(d_th->getEqualityEngine());
1512
261529
        while( !eqcs_i.isFinished() ){
1513
260652
          Node a = *eqcs_i;
1514
260652
          TypeNode tn = a.getType();
1515
130326
          if( tn.isSort() ){
1516
9816
            if( type_proc.find( tn )==type_proc.end() ){
1517
8965
              std::map< TypeNode, std::vector< Node > >::iterator itel = eqc_list.find( tn );
1518
8965
              if( itel!=eqc_list.end() ){
1519
17845
                for( unsigned j=0; j<itel->second.size(); j++ ){
1520
25039
                  Node b = itel->second[j];
1521
12771
                  if( !d_th->getEqualityEngine()->areDisequal( a, b, false ) ){
1522
1006
                    Node eq = Rewriter::rewrite( a.eqNode( b ) );
1523
1006
                    Node lem = NodeManager::currentNM()->mkNode( kind::OR, eq, eq.negate() );
1524
503
                    Trace("uf-ss-lemma") << "*** Split (no-minimal) : " << lem << std::endl;
1525
503
                    d_im.lemma(lem, InferenceId::UF_CARD_SPLIT);
1526
503
                    d_im.requirePhase(eq, true);
1527
503
                    type_proc[tn] = true;
1528
503
                    break;
1529
                  }
1530
                }
1531
              }
1532
8965
              eqc_list[tn].push_back( a );
1533
            }
1534
          }
1535
130326
          ++eqcs_i;
1536
        }
1537
      }
1538
    }
1539
    else
1540
    {
1541
      // unhandled uf ss mode
1542
      Assert(false);
1543
    }
1544
252722
    Trace("uf-ss-solver") << "Done CardinalityExtension: check " << level
1545
126361
                          << std::endl;
1546
  }
1547
}
1548
1549
300
void CardinalityExtension::presolve()
1550
{
1551
300
  d_initializedCombinedCardinality = false;
1552
712
  for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
1553
412
    it->second->presolve();
1554
412
    it->second->initialize();
1555
  }
1556
300
}
1557
1558
242
CardinalityExtension::CombinedCardinalityDecisionStrategy::
1559
    CombinedCardinalityDecisionStrategy(context::Context* satContext,
1560
242
                                        Valuation valuation)
1561
242
    : DecisionStrategyFmf(satContext, valuation)
1562
{
1563
242
}
1564
741
Node CardinalityExtension::CombinedCardinalityDecisionStrategy::mkLiteral(
1565
    unsigned i)
1566
{
1567
741
  NodeManager* nm = NodeManager::currentNM();
1568
741
  return nm->mkNode(COMBINED_CARDINALITY_CONSTRAINT, nm->mkConst(Rational(i)));
1569
}
1570
1571
std::string
1572
189344
CardinalityExtension::CombinedCardinalityDecisionStrategy::identify() const
1573
{
1574
189344
  return std::string("uf_combined_card");
1575
}
1576
1577
439711
void CardinalityExtension::preRegisterTerm(TNode n)
1578
{
1579
439711
  if (options::ufssMode() == options::UfssMode::FULL)
1580
  {
1581
    //initialize combined cardinality
1582
217682
    initializeCombinedCardinality();
1583
1584
217682
    Trace("uf-ss-register") << "Preregister " << n << "." << std::endl;
1585
    //shouldn't have to preregister this type (it may be that there are no quantifiers over tn)
1586
435364
    TypeNode tn = n.getType();
1587
217682
    std::map< TypeNode, SortModel* >::iterator it = d_rep_model.find( tn );
1588
217682
    if( it==d_rep_model.end() ){
1589
213978
      SortModel* rm = NULL;
1590
213978
      if( tn.isSort() ){
1591
447
        Trace("uf-ss-register") << "Create sort model " << tn << "." << std::endl;
1592
447
        rm = new SortModel(n, d_state, d_im, this);
1593
      }
1594
213978
      if( rm ){
1595
447
        rm->initialize();
1596
447
        d_rep_model[tn] = rm;
1597
        //d_rep_model_init[tn] = true;
1598
      }
1599
    }else{
1600
      //ensure sort model is initialized
1601
3704
      it->second->initialize();
1602
    }
1603
  }
1604
439711
}
1605
1606
449147
SortModel* CardinalityExtension::getSortModel(Node n)
1607
{
1608
898294
  TypeNode tn = n.getType();
1609
449147
  std::map< TypeNode, SortModel* >::iterator it = d_rep_model.find( tn );
1610
  //pre-register the type if not done already
1611
449147
  if( it==d_rep_model.end() ){
1612
400807
    preRegisterTerm( n );
1613
400807
    it = d_rep_model.find( tn );
1614
  }
1615
449147
  if( it!=d_rep_model.end() ){
1616
48340
    return it->second;
1617
  }else{
1618
400807
    return NULL;
1619
  }
1620
}
1621
1622
/** get cardinality for sort */
1623
int CardinalityExtension::getCardinality(Node n)
1624
{
1625
  SortModel* c = getSortModel( n );
1626
  if( c ){
1627
    return c->getCardinality();
1628
  }else{
1629
    return -1;
1630
  }
1631
}
1632
1633
int CardinalityExtension::getCardinality(TypeNode tn)
1634
{
1635
  std::map< TypeNode, SortModel* >::iterator it = d_rep_model.find( tn );
1636
  if( it!=d_rep_model.end() && it->second ){
1637
    return it->second->getCardinality();
1638
  }
1639
  return -1;
1640
}
1641
1642
//print debug
1643
void CardinalityExtension::debugPrint(const char* c)
1644
{
1645
  for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
1646
    Debug( c ) << "Conflict find structure for " << it->first << ": " << std::endl;
1647
    it->second->debugPrint( c );
1648
    Debug( c ) << std::endl;
1649
  }
1650
}
1651
1652
/** initialize */
1653
217682
void CardinalityExtension::initializeCombinedCardinality()
1654
{
1655
435364
  if (d_cc_dec_strat.get() != nullptr
1656
217682
      && !d_initializedCombinedCardinality.get())
1657
  {
1658
434
    d_initializedCombinedCardinality = true;
1659
868
    d_th->getDecisionManager()->registerStrategy(
1660
434
        DecisionManager::STRAT_UF_COMBINED_CARD, d_cc_dec_strat.get());
1661
  }
1662
217682
}
1663
1664
/** check */
1665
11552
void CardinalityExtension::checkCombinedCardinality()
1666
{
1667
11552
  Assert(options::ufssMode() == options::UfssMode::FULL);
1668
11552
  if( options::ufssFairness() ){
1669
11552
    Trace("uf-ss-com-card-debug") << "Check combined cardinality, get maximum negative cardinalities..." << std::endl;
1670
11552
    uint32_t totalCombinedCard = 0;
1671
11552
    uint32_t maxMonoSlave = 0;
1672
23104
    TypeNode maxSlaveType;
1673
76632
    for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
1674
65080
      uint32_t max_neg = it->second->getMaximumNegativeCardinality();
1675
65080
      if( !options::ufssFairnessMonotone() ){
1676
64910
        totalCombinedCard += max_neg;
1677
      }else{
1678
170
        std::map< TypeNode, bool >::iterator its = d_tn_mono_slave.find( it->first );
1679
170
        if( its==d_tn_mono_slave.end() || !its->second ){
1680
74
          totalCombinedCard += max_neg;
1681
        }else{
1682
96
          if( max_neg>maxMonoSlave ){
1683
8
            maxMonoSlave = max_neg;
1684
8
            maxSlaveType = it->first;
1685
          }
1686
        }
1687
      }
1688
    }
1689
11552
    Trace("uf-ss-com-card-debug") << "Check combined cardinality, total combined card : " << totalCombinedCard << std::endl;
1690
11552
    if( options::ufssFairnessMonotone() ){
1691
70
      Trace("uf-ss-com-card-debug") << "Max slave monotonic negated cardinality : " << maxMonoSlave << std::endl;
1692
140
      if (!d_min_pos_tn_master_card_set.get()
1693
70
          && maxMonoSlave > d_min_pos_tn_master_card.get())
1694
      {
1695
        uint32_t mc = d_min_pos_tn_master_card.get();
1696
        std::vector< Node > conf;
1697
        conf.push_back( d_rep_model[d_tn_mono_master]->getCardinalityLiteral( mc ) );
1698
        conf.push_back( d_rep_model[maxSlaveType]->getCardinalityLiteral( maxMonoSlave ).negate() );
1699
        Node cf = NodeManager::currentNM()->mkNode( AND, conf );
1700
        Trace("uf-ss-lemma") << "*** Combined monotone cardinality conflict"
1701
                             << " : " << cf << std::endl;
1702
        Trace("uf-ss-com-card") << "*** Combined monotone cardinality conflict"
1703
                                << " : " << cf << std::endl;
1704
        d_im.conflict(cf, InferenceId::UF_CARD_MONOTONE_COMBINED);
1705
        return;
1706
      }
1707
    }
1708
11552
    uint32_t cc = d_min_pos_com_card.get();
1709
11552
    if (d_min_pos_com_card_set.get() && totalCombinedCard > cc)
1710
    {
1711
      //conflict
1712
1294
      Node com_lit = d_cc_dec_strat->getLiteral(cc);
1713
1294
      std::vector< Node > conf;
1714
647
      conf.push_back( com_lit );
1715
647
      uint32_t totalAdded = 0;
1716
2293
      for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin();
1717
2293
           it != d_rep_model.end(); ++it ){
1718
2293
        bool doAdd = true;
1719
2293
        if( options::ufssFairnessMonotone() ){
1720
          std::map< TypeNode, bool >::iterator its =
1721
            d_tn_mono_slave.find( it->first );
1722
          if( its!=d_tn_mono_slave.end() && its->second ){
1723
            doAdd = false;
1724
          }
1725
        }
1726
2293
        if( doAdd ){
1727
2293
          uint32_t c = it->second->getMaximumNegativeCardinality();
1728
2293
          if( c>0 ){
1729
1695
            conf.push_back( it->second->getCardinalityLiteral( c ).negate() );
1730
1695
            totalAdded += c;
1731
          }
1732
2293
          if( totalAdded>cc ){
1733
647
            break;
1734
          }
1735
        }
1736
      }
1737
1294
      Node cf = NodeManager::currentNM()->mkNode( AND, conf );
1738
1294
      Trace("uf-ss-lemma") << "*** Combined cardinality conflict : " << cf
1739
647
                           << std::endl;
1740
1294
      Trace("uf-ss-com-card") << "*** Combined cardinality conflict : " << cf
1741
647
                              << std::endl;
1742
647
      d_im.conflict(cf, InferenceId::UF_CARD_COMBINED);
1743
    }
1744
  }
1745
}
1746
1747
250
CardinalityExtension::Statistics::Statistics()
1748
    : d_clique_conflicts("CardinalityExtension::Clique_Conflicts", 0),
1749
      d_clique_lemmas("CardinalityExtension::Clique_Lemmas", 0),
1750
      d_split_lemmas("CardinalityExtension::Split_Lemmas", 0),
1751
250
      d_max_model_size("CardinalityExtension::Max_Model_Size", 1)
1752
{
1753
250
  smtStatisticsRegistry()->registerStat(&d_clique_conflicts);
1754
250
  smtStatisticsRegistry()->registerStat(&d_clique_lemmas);
1755
250
  smtStatisticsRegistry()->registerStat(&d_split_lemmas);
1756
250
  smtStatisticsRegistry()->registerStat(&d_max_model_size);
1757
250
}
1758
1759
500
CardinalityExtension::Statistics::~Statistics()
1760
{
1761
250
  smtStatisticsRegistry()->unregisterStat(&d_clique_conflicts);
1762
250
  smtStatisticsRegistry()->unregisterStat(&d_clique_lemmas);
1763
250
  smtStatisticsRegistry()->unregisterStat(&d_split_lemmas);
1764
250
  smtStatisticsRegistry()->unregisterStat(&d_max_model_size);
1765
250
}
1766
1767
}/* CVC4::theory namespace::uf */
1768
}/* CVC4::theory namespace */
1769
1247841
}/* CVC4 namespace */