Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * Theory of UF with cardinality.
11 : : */
12 : :
13 : : #include "cvc5_private.h"
14 : :
15 : : #ifndef CVC5__THEORY_UF_STRONG_SOLVER_H
16 : : #define CVC5__THEORY_UF_STRONG_SOLVER_H
17 : :
18 : : #include "context/cdhashmap.h"
19 : : #include "context/context.h"
20 : : #include "smt/env_obj.h"
21 : : #include "theory/decision_strategy.h"
22 : : #include "theory/theory.h"
23 : : #include "util/statistics_stats.h"
24 : :
25 : : namespace cvc5::internal {
26 : : namespace theory {
27 : : namespace uf {
28 : :
29 : : class TheoryUF;
30 : :
31 : : /**
32 : : * This module implements a theory solver for UF with cardinality constraints.
33 : : * For high level details, see Reynolds et al "Finite Model Finding in SMT",
34 : : * CAV 2013, or Reynolds dissertation "Finite Model Finding in Satisfiability
35 : : * Modulo Theories".
36 : : */
37 : : class CardinalityExtension : protected EnvObj
38 : : {
39 : : protected:
40 : : typedef context::CDHashMap<Node, bool> NodeBoolMap;
41 : : typedef context::CDHashMap<Node, int> NodeIntMap;
42 : :
43 : : public:
44 : : /**
45 : : * Information for incremental conflict/clique finding for a
46 : : * particular sort.
47 : : */
48 : : class SortModel : protected EnvObj
49 : : {
50 : : private:
51 : : std::map< Node, std::vector< int > > d_totality_lems;
52 : : std::map< TypeNode, std::map< int, std::vector< Node > > > d_sym_break_terms;
53 : : std::map< Node, int > d_sym_break_index;
54 : :
55 : : public:
56 : : /**
57 : : * A partition of the current equality graph for which cliques
58 : : * can occur internally.
59 : : */
60 : : class Region
61 : : {
62 : : public:
63 : : /** information stored about each node in region */
64 : : class RegionNodeInfo {
65 : : public:
66 : : /** disequality list for node */
67 : : class DiseqList {
68 : : public:
69 : 27188 : DiseqList(context::Context* c) : d_size(c, 0), d_disequalities(c) {}
70 : 27176 : ~DiseqList() {}
71 : :
72 : 569214 : void setDisequal(Node n, bool valid)
73 : : {
74 : 569214 : Assert((!isSet(n)) || getDisequalityValue(n) != valid);
75 : 569214 : d_disequalities[n] = valid;
76 [ + + ]: 569214 : d_size = d_size + (valid ? 1 : -1);
77 : 569214 : }
78 : 1789381 : bool isSet(Node n) const {
79 : 1789381 : return d_disequalities.find(n) != d_disequalities.end();
80 : : }
81 : 513831 : bool getDisequalityValue(Node n) const {
82 [ - + ][ - + ]: 513831 : Assert(isSet(n));
[ - - ]
83 : 513831 : return (*(d_disequalities.find(n))).second;
84 : : }
85 : :
86 : 317099 : int size() const { return d_size; }
87 : :
88 : : typedef NodeBoolMap::iterator iterator;
89 : 254387 : iterator begin() { return d_disequalities.begin(); }
90 : 650766 : iterator end() { return d_disequalities.end(); }
91 : :
92 : : private:
93 : : context::CDO<int> d_size;
94 : : NodeBoolMap d_disequalities;
95 : : }; /* class DiseqList */
96 : : public:
97 : : /** constructor */
98 : 13594 : RegionNodeInfo(context::Context* c)
99 : 13594 : : d_internal(c), d_external(c), d_valid(c, true)
100 : : {
101 : 13594 : d_disequalities[0] = &d_internal;
102 : 13594 : d_disequalities[1] = &d_external;
103 : 13594 : }
104 : 13588 : ~RegionNodeInfo(){}
105 : :
106 : 97541 : int getNumDisequalities() const {
107 : 97541 : return d_disequalities[0]->size() + d_disequalities[1]->size();
108 : : }
109 : 73038 : int getNumExternalDisequalities() const {
110 : 73038 : return d_disequalities[0]->size();
111 : : }
112 : 48979 : int getNumInternalDisequalities() const {
113 : 48979 : return d_disequalities[1]->size();
114 : : }
115 : :
116 : 1502479 : bool valid() const { return d_valid; }
117 : 112392 : void setValid(bool valid) { d_valid = valid; }
118 : :
119 : 1529937 : 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 : 106684 : iterator begin() { return d_nodes.begin(); }
158 : 776130 : iterator end() { return d_nodes.end(); }
159 : :
160 : : typedef NodeBoolMap::iterator split_iterator;
161 : 5044 : split_iterator begin_splits() { return d_splits.begin(); }
162 : 37859 : split_iterator end_splits() { return d_splits.end(); }
163 : :
164 : : /** Returns a RegionInfo. */
165 : 49810 : RegionNodeInfo* getRegionInfo(Node n) {
166 [ - + ][ - + ]: 49810 : Assert(d_nodes.find(n) != d_nodes.end());
[ - - ]
167 : 49810 : return (* (d_nodes.find(n))).second;
168 : : }
169 : :
170 : : /** Returns whether or not d_valid is set in current context. */
171 : 2380854 : bool valid() const { return d_valid; }
172 : :
173 : : /** Sets d_valid to the value valid in the current context.*/
174 : 59261 : 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 : 237084 : 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 : 358250 : bool hasRep( Node n ) {
192 [ + + ][ + + ]: 358250 : 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 : 2800 : 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 : 224 : 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 : 520735 : bool isValid( int ri ) {
241 [ + - ][ + - ]: 520735 : 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 literals */
267 : : std::map<uint32_t, Node> d_cardinality_literal;
268 : : /** whether a positive cardinality constraint has been asserted */
269 : : context::CDO<bool> d_hasCard;
270 : : /** clique lemmas that have been asserted */
271 : : std::map< int, std::vector< std::vector< Node > > > d_cliques;
272 : : /** maximum negatively asserted cardinality */
273 : : context::CDO<uint32_t> d_maxNegCard;
274 : : /** list of fresh representatives allocated */
275 : : std::vector< Node > d_fresh_aloc_reps;
276 : : /** whether we are initialized */
277 : : context::CDO<bool> d_initialized;
278 : : /** simple check cardinality */
279 : : void simpleCheckCardinality();
280 : :
281 : : public:
282 : : SortModel(Env& env,
283 : : TypeNode tn,
284 : : TheoryState& state,
285 : : TheoryInferenceManager& im,
286 : : CardinalityExtension* thss);
287 : : virtual ~SortModel();
288 : : /** initialize */
289 : : void initialize();
290 : : /** new node */
291 : : void newEqClass( Node n );
292 : : /** merge */
293 : : void merge( Node a, Node b );
294 : : /** assert terms are disequal */
295 : : void assertDisequal( Node a, Node b, Node reason );
296 : : /** are disequal */
297 : : bool areDisequal( Node a, Node b );
298 : : /** check */
299 : : void check(Theory::Effort level);
300 : : /** presolve */
301 : : void presolve();
302 : : /** assert cardinality */
303 : : void assertCardinality(uint32_t c, bool val);
304 : : /** get cardinality */
305 : 0 : uint32_t getCardinality() const { return d_cardinality; }
306 : : /** has cardinality */
307 : 0 : bool hasCardinalityAsserted() const { return d_hasCard; }
308 : : /** get cardinality term */
309 : : TypeNode getType() const { return d_type; }
310 : : /** get cardinality literal */
311 : : Node getCardinalityLiteral(uint32_t c);
312 : : /** get maximum negative cardinality */
313 : 87824 : uint32_t getMaximumNegativeCardinality() const
314 : : {
315 : 87824 : return d_maxNegCard.get();
316 : : }
317 : : //print debug
318 : : void debugPrint( const char* c );
319 : : /**
320 : : * Check at last call effort. This will verify that the model is minimal.
321 : : * This return lemmas if there are terms in the model that the cardinality
322 : : * extension was not notified of.
323 : : *
324 : : * @return false if current model is not minimal. In this case, lemmas are
325 : : * sent on the output channel of the UF theory.
326 : : */
327 : : bool checkLastCall();
328 : : /** get number of regions (for debugging) */
329 : : int getNumRegions();
330 : :
331 : : private:
332 : : /**
333 : : * Decision strategy for cardinality constraints. This asserts
334 : : * the minimal constraint positively in the SAT context. For details, see
335 : : * Section 6.3 of Reynolds et al, "Constraint Solving for Finite Model
336 : : * Finding in SMT Solvers", TPLP 2017.
337 : : */
338 : : class CardinalityDecisionStrategy : public DecisionStrategyFmf
339 : : {
340 : : public:
341 : : CardinalityDecisionStrategy(Env& env, TypeNode type, Valuation valuation);
342 : : /** make literal (the i^th combined cardinality literal) */
343 : : Node mkLiteral(unsigned i) override;
344 : : /** identify */
345 : : std::string identify() const override;
346 : : private:
347 : : /** The type we are considering cardinality constraints for */
348 : : TypeNode d_type;
349 : : };
350 : : /** cardinality decision strategy */
351 : : std::unique_ptr<CardinalityDecisionStrategy> d_c_dec_strat;
352 : : }; /** class SortModel */
353 : :
354 : : public:
355 : : CardinalityExtension(Env& env,
356 : : TheoryState& state,
357 : : TheoryInferenceManager& im,
358 : : TheoryUF* th);
359 : : ~CardinalityExtension();
360 : : /** get theory */
361 : 20031 : TheoryUF* getTheory() { return d_th; }
362 : : /** new node */
363 : : void newEqClass( Node n );
364 : : /** merge */
365 : : void merge( Node a, Node b );
366 : : /** assert terms are disequal */
367 : : void assertDisequal( Node a, Node b, Node reason );
368 : : /** assert node */
369 : : void assertNode( Node n, bool isDecision );
370 : : /** are disequal */
371 : : bool areDisequal( Node a, Node b );
372 : : /** check */
373 : : void check( Theory::Effort level );
374 : : /** presolve */
375 : : void presolve();
376 : : /** preregister a term */
377 : : void preRegisterTerm( TNode n );
378 : : /** identify */
379 : : std::string identify() const { return std::string("CardinalityExtension"); }
380 : : //print debug
381 : : void debugPrint( const char* c );
382 : : /** get cardinality for node */
383 : : int getCardinality( Node n );
384 : : /** get cardinality for type */
385 : : int getCardinality( TypeNode tn );
386 : : /** has eqc */
387 : : bool hasEqc(Node a);
388 : :
389 : : class Statistics {
390 : : public:
391 : : IntStat d_clique_conflicts;
392 : : IntStat d_clique_lemmas;
393 : : IntStat d_split_lemmas;
394 : : IntStat d_max_model_size;
395 : : Statistics(StatisticsRegistry& sr);
396 : : };
397 : : /** statistics class */
398 : : Statistics d_statistics;
399 : :
400 : : private:
401 : : /** get sort model */
402 : : SortModel* getSortModel(Node n);
403 : : /** initialize */
404 : : void initializeCombinedCardinality();
405 : : /** check */
406 : : void checkCombinedCardinality();
407 : : /** ensure eqc */
408 : : void ensureEqc(SortModel* c, Node a);
409 : : /** ensure eqc for all subterms of n */
410 : : void ensureEqcRec(Node n);
411 : :
412 : : /** Reference to the state object */
413 : : TheoryState& d_state;
414 : : /** Reference to the inference manager */
415 : : TheoryInferenceManager& d_im;
416 : : /** theory uf pointer */
417 : : TheoryUF* d_th;
418 : : /** rep model structure, one for each type */
419 : : std::map<TypeNode, SortModel*> d_rep_model;
420 : :
421 : : /** minimum positive combined cardinality */
422 : : context::CDO<uint32_t> d_min_pos_com_card;
423 : : /** Whether the field above has been set */
424 : : context::CDO<bool> d_min_pos_com_card_set;
425 : : /**
426 : : * Decision strategy for combined cardinality constraints. This asserts
427 : : * the minimal combined cardinality constraint positively in the SAT
428 : : * context. It is enabled by the ufssFairness option. For details, see
429 : : * the extension to multiple sorts in Section 6.3 of Reynolds et al,
430 : : * "Constraint Solving for Finite Model Finding in SMT Solvers", TPLP 2017.
431 : : */
432 : : class CombinedCardinalityDecisionStrategy : public DecisionStrategyFmf
433 : : {
434 : : public:
435 : : CombinedCardinalityDecisionStrategy(Env& env, Valuation valuation);
436 : : /** make literal (the i^th combined cardinality literal) */
437 : : Node mkLiteral(unsigned i) override;
438 : : /** identify */
439 : : std::string identify() const override;
440 : : };
441 : : /** combined cardinality decision strategy */
442 : : std::unique_ptr<CombinedCardinalityDecisionStrategy> d_cc_dec_strat;
443 : : /** Have we initialized combined cardinality? */
444 : : context::CDO<bool> d_initializedCombinedCardinality;
445 : :
446 : : /** cardinality literals for which we have added */
447 : : NodeBoolMap d_card_assertions_eqv_lemma;
448 : : /** the master monotone type (if ufssFairnessMonotone enabled) */
449 : : TypeNode d_tn_mono_master;
450 : : std::map<TypeNode, bool> d_tn_mono_slave;
451 : : /** The minimum positive asserted master cardinality */
452 : : context::CDO<uint32_t> d_min_pos_tn_master_card;
453 : : /** Whether the field above has been set */
454 : : context::CDO<bool> d_min_pos_tn_master_card_set;
455 : : /** relevant eqc */
456 : : NodeBoolMap d_rel_eqc;
457 : : }; /* class CardinalityExtension */
458 : :
459 : : } // namespace uf
460 : : } // namespace theory
461 : : } // namespace cvc5::internal
462 : :
463 : : #endif /* CVC5__THEORY_UF_STRONG_SOLVER_H */
|
