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