GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/uf/cardinality_extension.h Lines: 53 55 96.4 %
Date: 2021-03-23 Branches: 38 104 36.5 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file cardinality_extension.h
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 Theory of UF with cardinality.
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY_UF_STRONG_SOLVER_H
18
#define CVC4__THEORY_UF_STRONG_SOLVER_H
19
20
#include "context/cdhashmap.h"
21
#include "context/context.h"
22
#include "theory/decision_strategy.h"
23
#include "theory/theory.h"
24
#include "util/statistics_registry.h"
25
26
namespace CVC4 {
27
namespace theory {
28
namespace uf {
29
30
class TheoryUF;
31
32
/**
33
 * This module implements a theory solver for UF with cardinality constraints.
34
 * For high level details, see Reynolds et al "Finite Model Finding in SMT",
35
 * CAV 2013, or Reynolds dissertation "Finite Model Finding in Satisfiability
36
 * Modulo Theories".
37
 */
38
class CardinalityExtension
39
{
40
 protected:
41
  typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
42
  typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
43
44
 public:
45
  /**
46
   * Information for incremental conflict/clique finding for a
47
   * particular sort.
48
   */
49
  class SortModel
50
  {
51
   private:
52
    std::map< Node, std::vector< int > > d_totality_lems;
53
    std::map< TypeNode, std::map< int, std::vector< Node > > > d_sym_break_terms;
54
    std::map< Node, int > d_sym_break_index;
55
56
   public:
57
    /**
58
     * A partition of the current equality graph for which cliques
59
     * can occur internally.
60
     */
61
    class Region
62
    {
63
     public:
64
      /** information stored about each node in region */
65
      class RegionNodeInfo {
66
      public:
67
        /** disequality list for node */
68
        class DiseqList {
69
        public:
70
16708
          DiseqList( context::Context* c )
71
16708
            : d_size( c, 0 ), d_disequalities( c ) {}
72
16708
          ~DiseqList(){}
73
74
362932
          void setDisequal( Node n, bool valid ){
75
362932
            Assert((!isSet(n)) || getDisequalityValue(n) != valid);
76
362932
            d_disequalities[ n ] = valid;
77
362932
            d_size = d_size + ( valid ? 1 : -1 );
78
362932
          }
79
1119145
          bool isSet(Node n) const {
80
1119145
            return d_disequalities.find(n) != d_disequalities.end();
81
          }
82
311117
          bool getDisequalityValue(Node n) const {
83
311117
            Assert(isSet(n));
84
311117
            return (*(d_disequalities.find(n))).second;
85
          }
86
87
197592
          int size() const { return d_size; }
88
89
          typedef NodeBoolMap::iterator iterator;
90
173078
          iterator begin() { return d_disequalities.begin(); }
91
404158
          iterator end() { return d_disequalities.end(); }
92
93
        private:
94
          context::CDO< int > d_size;
95
          NodeBoolMap d_disequalities;
96
        }; /* class DiseqList */
97
       public:
98
        /** constructor */
99
8354
        RegionNodeInfo( context::Context* c )
100
8354
          : d_internal(c), d_external(c), d_valid(c, true) {
101
8354
          d_disequalities[0] = &d_internal;
102
8354
          d_disequalities[1] = &d_external;
103
8354
        }
104
8354
        ~RegionNodeInfo(){}
105
106
60594
        int getNumDisequalities() const {
107
60594
          return d_disequalities[0]->size() + d_disequalities[1]->size();
108
        }
109
46745
        int getNumExternalDisequalities() const {
110
46745
          return d_disequalities[0]->size();
111
        }
112
29659
        int getNumInternalDisequalities() const {
113
29659
          return d_disequalities[1]->size();
114
        }
115
116
992003
        bool valid() const { return d_valid; }
117
78484
        void setValid(bool valid) { d_valid = valid; }
118
119
981106
        DiseqList* get(unsigned i) { return d_disequalities[i]; }
120
121
       private:
122
        DiseqList d_internal;
123
        DiseqList d_external;
124
        context::CDO< bool > d_valid;
125
        DiseqList* d_disequalities[2];
126
      }; /* class RegionNodeInfo */
127
128
    private:
129
      /** conflict find pointer */
130
      SortModel* d_cf;
131
132
      context::CDO<size_t> d_testCliqueSize;
133
      context::CDO< unsigned > d_splitsSize;
134
      //a postulated clique
135
      NodeBoolMap d_testClique;
136
      //disequalities needed for this clique to happen
137
      NodeBoolMap d_splits;
138
      //number of valid representatives in this region
139
      context::CDO<size_t> d_reps_size;
140
      //total disequality size (external)
141
      context::CDO< unsigned > d_total_diseq_external;
142
      //total disequality size (internal)
143
      context::CDO< unsigned > d_total_diseq_internal;
144
      /** set rep */
145
      void setRep( Node n, bool valid );
146
      //region node infomation
147
      std::map< Node, RegionNodeInfo* > d_nodes;
148
      //whether region is valid
149
      context::CDO< bool > d_valid;
150
151
     public:
152
      //constructor
153
      Region( SortModel* cf, context::Context* c );
154
      virtual ~Region();
155
156
      typedef std::map< Node, RegionNodeInfo* >::iterator iterator;
157
71012
      iterator begin() { return d_nodes.begin(); }
158
492046
      iterator end() { return d_nodes.end(); }
159
160
      typedef NodeBoolMap::iterator split_iterator;
161
3198
      split_iterator begin_splits() { return d_splits.begin(); }
162
22534
      split_iterator end_splits() { return d_splits.end(); }
163
164
      /** Returns a RegionInfo. */
165
29844
      RegionNodeInfo* getRegionInfo(Node n) {
166
29844
        Assert(d_nodes.find(n) != d_nodes.end());
167
29844
        return (* (d_nodes.find(n))).second;
168
      }
169
170
      /** Returns whether or not d_valid is set in current context. */
171
1864052
      bool valid() const { return d_valid; }
172
173
      /** Sets d_valid to the value valid in the current context.*/
174
41347
      void setValid(bool valid) { d_valid = valid; }
175
176
      /** add rep */
177
      void addRep( Node n );
178
      //take node from region
179
      void takeNode( Region* r, Node n );
180
      //merge with other region
181
      void combine( Region* r );
182
      /** merge */
183
      void setEqual( Node a, Node b );
184
      //set n1 != n2 to value 'valid', type is whether it is internal/external
185
      void setDisequal( Node n1, Node n2, int type, bool valid );
186
      //get num reps
187
151451
      size_t getNumReps() const { return d_reps_size; }
188
      //get test clique size
189
      size_t getTestCliqueSize() const { return d_testCliqueSize; }
190
      // has representative
191
246009
      bool hasRep( Node n ) {
192
246009
        return d_nodes.find(n) != d_nodes.end() && d_nodes[n]->valid();
193
      }
194
      // is disequal
195
      bool isDisequal( Node n1, Node n2, int type );
196
      /** get must merge */
197
      bool getMustCombine( int cardinality );
198
      /** has splits */
199
1754
      bool hasSplits() { return d_splitsSize>0; }
200
      /** get external disequalities */
201
      void getNumExternalDisequalities(std::map< Node, int >& num_ext_disequalities );
202
      /** check for cliques */
203
      bool check( Theory::Effort level, int cardinality, std::vector< Node >& clique );
204
      //print debug
205
      void debugPrint( const char* c, bool incClique = false );
206
207
      // Returns the first key in d_nodes.
208
48
      Node frontKey() const { return d_nodes.begin()->first; }
209
    }; /* class Region */
210
211
   private:
212
    /** the type this model is for */
213
    TypeNode d_type;
214
    /** Reference to the state object */
215
    TheoryState& d_state;
216
    /** Reference to the inference manager */
217
    TheoryInferenceManager& d_im;
218
    /** Pointer to the cardinality extension that owns this. */
219
    CardinalityExtension* d_thss;
220
    /** regions used to d_region_index */
221
    context::CDO<size_t> d_regions_index;
222
    /** vector of regions */
223
    std::vector< Region* > d_regions;
224
    /** map from Nodes to index of d_regions they exist in, -1 means invalid */
225
    NodeIntMap d_regions_map;
226
    /** the score for each node for splitting */
227
    NodeIntMap d_split_score;
228
    /** number of valid disequalities in d_disequalities */
229
    context::CDO< unsigned > d_disequalities_index;
230
    /** list of all disequalities */
231
    std::vector< Node > d_disequalities;
232
    /** number of representatives in all regions */
233
    context::CDO< unsigned > d_reps;
234
235
    /** get number of disequalities from node n to region ri */
236
    int getNumDisequalitiesToRegion( Node n, int ri );
237
    /** get number of disequalities from Region r to other regions */
238
    void getDisequalitiesToRegions( int ri, std::map< int, int >& regions_diseq );
239
    /** is valid */
240
345021
    bool isValid( int ri ) {
241
345021
      return ri>=0 && ri<(int)d_regions_index && d_regions[ ri ]->valid();
242
    }
243
    /** set split score */
244
    void setSplitScore( Node n, int s );
245
    /** check if we need to combine region ri */
246
    void checkRegion( int ri, bool checkCombine = true );
247
    /** force combine region */
248
    int forceCombineRegion( int ri, bool useDensity = true );
249
    /** merge regions */
250
    int combineRegions( int ai, int bi );
251
    /** move node n to region ri */
252
    void moveNode( Node n, int ri );
253
    /** allocate cardinality */
254
    void allocateCardinality();
255
    /**
256
     * Add splits. Returns
257
     *   0 = no split,
258
     *  -1 = entailed disequality added, or
259
     *   1 = split added.
260
     */
261
    int addSplit(Region* r);
262
    /** add clique lemma */
263
    void addCliqueLemma(std::vector<Node>& clique);
264
    /** cardinality */
265
    context::CDO<uint32_t> d_cardinality;
266
    /** cardinality lemma term */
267
    Node d_cardinality_term;
268
    /** cardinality literals */
269
    std::map<uint32_t, Node> d_cardinality_literal;
270
    /** whether a positive cardinality constraint has been asserted */
271
    context::CDO< bool > d_hasCard;
272
    /** clique lemmas that have been asserted */
273
    std::map< int, std::vector< std::vector< Node > > > d_cliques;
274
    /** maximum negatively asserted cardinality */
275
    context::CDO<uint32_t> d_maxNegCard;
276
    /** list of fresh representatives allocated */
277
    std::vector< Node > d_fresh_aloc_reps;
278
    /** whether we are initialized */
279
    context::CDO< bool > d_initialized;
280
    /** simple check cardinality */
281
    void simpleCheckCardinality();
282
283
   public:
284
    SortModel(Node n,
285
              TheoryState& state,
286
              TheoryInferenceManager& im,
287
              CardinalityExtension* thss);
288
    virtual ~SortModel();
289
    /** initialize */
290
    void initialize();
291
    /** new node */
292
    void newEqClass( Node n );
293
    /** merge */
294
    void merge( Node a, Node b );
295
    /** assert terms are disequal */
296
    void assertDisequal( Node a, Node b, Node reason );
297
    /** are disequal */
298
    bool areDisequal( Node a, Node b );
299
    /** check */
300
    void check(Theory::Effort level);
301
    /** presolve */
302
    void presolve();
303
    /** assert cardinality */
304
    void assertCardinality(uint32_t c, bool val);
305
    /** get cardinality */
306
    uint32_t getCardinality() const { return d_cardinality; }
307
    /** has cardinality */
308
    bool hasCardinalityAsserted() const { return d_hasCard; }
309
    /** get cardinality term */
310
8611
    Node getCardinalityTerm() const { return d_cardinality_term; }
311
    /** get cardinality literal */
312
    Node getCardinalityLiteral(uint32_t c);
313
    /** get maximum negative cardinality */
314
67373
    uint32_t getMaximumNegativeCardinality() const
315
    {
316
67373
      return d_maxNegCard.get();
317
    }
318
    //print debug
319
    void debugPrint( const char* c );
320
    /**
321
     * Check at last call effort. This will verify that the model is minimal.
322
     * This return lemmas if there are terms in the model that the cardinality
323
     * extension was not notified of.
324
     *
325
     * @return false if current model is not minimal. In this case, lemmas are
326
     * sent on the output channel of the UF theory.
327
     */
328
    bool checkLastCall();
329
    /** get number of regions (for debugging) */
330
    int getNumRegions();
331
332
   private:
333
    /**
334
     * Decision strategy for cardinality constraints. This asserts
335
     * the minimal constraint positively in the SAT context. For details, see
336
     * Section 6.3 of Reynolds et al, "Constraint Solving for Finite Model
337
     * Finding in SMT Solvers", TPLP 2017.
338
     */
339
894
    class CardinalityDecisionStrategy : public DecisionStrategyFmf
340
    {
341
     public:
342
      CardinalityDecisionStrategy(Node t,
343
                                  context::Context* satContext,
344
                                  Valuation valuation);
345
      /** make literal (the i^th combined cardinality literal) */
346
      Node mkLiteral(unsigned i) override;
347
      /** identify */
348
      std::string identify() const override;
349
350
     private:
351
      /** the cardinality term */
352
      Node d_cardinality_term;
353
    };
354
    /** cardinality decision strategy */
355
    std::unique_ptr<CardinalityDecisionStrategy> d_c_dec_strat;
356
  }; /** class SortModel */
357
358
 public:
359
  CardinalityExtension(TheoryState& state,
360
                       TheoryInferenceManager& im,
361
                       TheoryUF* th);
362
  ~CardinalityExtension();
363
  /** get theory */
364
22470
  TheoryUF* getTheory() { return d_th; }
365
  /** new node */
366
  void newEqClass( Node n );
367
  /** merge */
368
  void merge( Node a, Node b );
369
  /** assert terms are disequal */
370
  void assertDisequal( Node a, Node b, Node reason );
371
  /** assert node */
372
  void assertNode( Node n, bool isDecision );
373
  /** are disequal */
374
  bool areDisequal( Node a, Node b );
375
  /** check */
376
  void check( Theory::Effort level );
377
  /** presolve */
378
  void presolve();
379
  /** preregister a term */
380
  void preRegisterTerm( TNode n );
381
  /** identify */
382
  std::string identify() const { return std::string("CardinalityExtension"); }
383
  //print debug
384
  void debugPrint( const char* c );
385
  /** get cardinality for node */
386
  int getCardinality( Node n );
387
  /** get cardinality for type */
388
  int getCardinality( TypeNode tn );
389
  /** has eqc */
390
  bool hasEqc(Node a);
391
392
  class Statistics {
393
   public:
394
    IntStat d_clique_conflicts;
395
    IntStat d_clique_lemmas;
396
    IntStat d_split_lemmas;
397
    IntStat d_max_model_size;
398
    Statistics();
399
    ~Statistics();
400
  };
401
  /** statistics class */
402
  Statistics d_statistics;
403
404
 private:
405
  /** get sort model */
406
  SortModel* getSortModel(Node n);
407
  /** initialize */
408
  void initializeCombinedCardinality();
409
  /** check */
410
  void checkCombinedCardinality();
411
  /** ensure eqc */
412
  void ensureEqc(SortModel* c, Node a);
413
  /** ensure eqc for all subterms of n */
414
  void ensureEqcRec(Node n);
415
416
  /** Reference to the state object */
417
  TheoryState& d_state;
418
  /** Reference to the inference manager */
419
  TheoryInferenceManager& d_im;
420
  /** theory uf pointer */
421
  TheoryUF* d_th;
422
  /** rep model structure, one for each type */
423
  std::map<TypeNode, SortModel*> d_rep_model;
424
425
  /** minimum positive combined cardinality */
426
  context::CDO<uint32_t> d_min_pos_com_card;
427
  /** Whether the field above has been set */
428
  context::CDO<bool> d_min_pos_com_card_set;
429
  /**
430
   * Decision strategy for combined cardinality constraints. This asserts
431
   * the minimal combined cardinality constraint positively in the SAT
432
   * context. It is enabled by options::ufssFairness(). For details, see
433
   * the extension to multiple sorts in Section 6.3 of Reynolds et al,
434
   * "Constraint Solving for Finite Model Finding in SMT Solvers", TPLP 2017.
435
   */
436
484
  class CombinedCardinalityDecisionStrategy : public DecisionStrategyFmf
437
  {
438
   public:
439
    CombinedCardinalityDecisionStrategy(context::Context* satContext,
440
                                        Valuation valuation);
441
    /** make literal (the i^th combined cardinality literal) */
442
    Node mkLiteral(unsigned i) override;
443
    /** identify */
444
    std::string identify() const override;
445
  };
446
  /** combined cardinality decision strategy */
447
  std::unique_ptr<CombinedCardinalityDecisionStrategy> d_cc_dec_strat;
448
  /** Have we initialized combined cardinality? */
449
  context::CDO<bool> d_initializedCombinedCardinality;
450
451
  /** cardinality literals for which we have added */
452
  NodeBoolMap d_card_assertions_eqv_lemma;
453
  /** the master monotone type (if ufssFairnessMonotone enabled) */
454
  TypeNode d_tn_mono_master;
455
  std::map<TypeNode, bool> d_tn_mono_slave;
456
  /** The minimum positive asserted master cardinality */
457
  context::CDO<uint32_t> d_min_pos_tn_master_card;
458
  /** Whether the field above has been set */
459
  context::CDO<bool> d_min_pos_tn_master_card_set;
460
  /** relevant eqc */
461
  NodeBoolMap d_rel_eqc;
462
}; /* class CardinalityExtension */
463
464
}/* CVC4::theory namespace::uf */
465
}/* CVC4::theory namespace */
466
}/* CVC4 namespace */
467
468
#endif /* CVC4__THEORY_UF_STRONG_SOLVER_H */