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 arrays.
11 : : */
12 : :
13 : : #include "cvc5_private.h"
14 : :
15 : : #ifndef CVC5__THEORY__ARRAYS__THEORY_ARRAYS_H
16 : : #define CVC5__THEORY__ARRAYS__THEORY_ARRAYS_H
17 : :
18 : : #include <tuple>
19 : : #include <unordered_map>
20 : :
21 : : #include "context/cdhashmap.h"
22 : : #include "context/cdhashset.h"
23 : : #include "context/cdqueue.h"
24 : : #include "theory/arrays/array_info.h"
25 : : #include "theory/arrays/inference_manager.h"
26 : : #include "theory/arrays/proof_checker.h"
27 : : #include "theory/arrays/theory_arrays_rewriter.h"
28 : : #include "theory/decision_strategy.h"
29 : : #include "theory/theory.h"
30 : : #include "theory/theory_state.h"
31 : : #include "theory/uf/equality_engine.h"
32 : : #include "util/statistics_stats.h"
33 : :
34 : : namespace cvc5::internal {
35 : : namespace theory {
36 : : namespace arrays {
37 : :
38 : : /**
39 : : * Decision procedure for arrays.
40 : : *
41 : : * Overview of decision procedure:
42 : : *
43 : : * Preliminary notation:
44 : : * Stores(a) = {t | a ~ t and t = store( _ _ _ )}
45 : : * InStores(a) = {t | t = store (b _ _) and a ~ b }
46 : : * Indices(a) = {i | there exists a term b[i] such that a ~ b or store(b i v)}
47 : : * ~ represents the equivalence relation based on the asserted equalities in
48 : : * the current context.
49 : : *
50 : : * The rules implemented are the following:
51 : : * store(b i v)
52 : : * Row1 -------------------
53 : : * store(b i v)[i] = v
54 : : *
55 : : * store(b i v) a'[j]
56 : : * Row ---------------------- [ a' ~ store(b i v) or a' ~ b ]
57 : : * i = j OR a[j] = b[j]
58 : : *
59 : : * a b same kind arrays
60 : : * Ext ------------------------ [ a!= b in current context, k new var]
61 : : * a = b OR a[k] != b[k]p
62 : : *
63 : : *
64 : : * The Row1 one rule is implemented implicitly as follows:
65 : : * - for each store(b i v) term add the following equality to the congruence
66 : : * closure store(b i v)[i] = v
67 : : * - if one of the literals in a conflict is of the form store(b i v)[i] = v
68 : : * remove it from the conflict
69 : : *
70 : : * Because new store terms are not created, we need to check if we need to
71 : : * instantiate a new Row axiom in the following cases:
72 : : * 1. the congruence relation changes (i.e. two terms get merged)
73 : : * - when a new equality between array terms a = b is asserted we check
74 : : * if we can instantiate a Row lemma for all pairs of indices i where a is being
75 : : * read and stores
76 : : * - this is only done during full effort check
77 : : * 2. a new read term is created either as a consequences of an Ext lemma or
78 : : * a Row lemma
79 : : * - this is implemented in the checkRowForIndex method which is called
80 : : * when preregistering a term of the form a[i].
81 : : * - as a consequence lemmas are instantiated even before full effort
82 : : * check
83 : : *
84 : : * The Ext axiom is instantiated when a disequality is asserted during full
85 : : * effort check. Ext lemmas are stored in a cache to prevent instantiating
86 : : * essentially the same lemma multiple times.
87 : : */
88 : :
89 : 0 : static inline std::string spaces(int level)
90 : : {
91 : 0 : std::string indentStr(level, ' ');
92 : 0 : return indentStr;
93 : : }
94 : :
95 : : class TheoryArrays : public Theory
96 : : {
97 : : /////////////////////////////////////////////////////////////////////////////
98 : : // MISC
99 : : /////////////////////////////////////////////////////////////////////////////
100 : :
101 : : private:
102 : : /** True node for predicates = true */
103 : : Node d_true;
104 : :
105 : : /** True node for predicates = false */
106 : : Node d_false;
107 : :
108 : : // Statistics
109 : :
110 : : /** number of Row lemmas */
111 : : IntStat d_numRow;
112 : : /** number of Ext lemmas */
113 : : IntStat d_numExt;
114 : : /** number of propagations */
115 : : IntStat d_numProp;
116 : : /** number of explanations */
117 : : IntStat d_numExplain;
118 : : /** calls to non-linear */
119 : : IntStat d_numNonLinear;
120 : : /** splits on array variables */
121 : : IntStat d_numSharedArrayVarSplits;
122 : : /** splits in getModelVal */
123 : : IntStat d_numGetModelValSplits;
124 : : /** conflicts in getModelVal */
125 : : IntStat d_numGetModelValConflicts;
126 : : /** splits in setModelVal */
127 : : IntStat d_numSetModelValSplits;
128 : : /** conflicts in setModelVal */
129 : : IntStat d_numSetModelValConflicts;
130 : :
131 : : public:
132 : : TheoryArrays(Env& env,
133 : : OutputChannel& out,
134 : : Valuation valuation,
135 : : std::string name = "theory::arrays::");
136 : : ~TheoryArrays();
137 : :
138 : : //--------------------------------- initialization
139 : : /** get the official theory rewriter of this theory */
140 : : TheoryRewriter* getTheoryRewriter() override;
141 : : /** get the proof checker of this theory */
142 : : ProofRuleChecker* getProofChecker() override;
143 : : /**
144 : : * Returns true if we need an equality engine. If so, we initialize the
145 : : * information regarding how it should be setup. For details, see the
146 : : * documentation in Theory::needsEqualityEngine.
147 : : */
148 : : bool needsEqualityEngine(EeSetupInfo& esi) override;
149 : : /** finish initialization */
150 : : void finishInit() override;
151 : : //--------------------------------- end initialization
152 : :
153 : 0 : std::string identify() const override { return std::string("TheoryArrays"); }
154 : :
155 : : /////////////////////////////////////////////////////////////////////////////
156 : : // PREPROCESSING
157 : : /////////////////////////////////////////////////////////////////////////////
158 : :
159 : : private:
160 : : // PPNotifyClass: dummy template class for d_ppEqualityEngine - notifications
161 : : // not used
162 : : class PPNotifyClass
163 : : {
164 : : public:
165 : : bool notify(CVC5_UNUSED TNode propagation) { return true; }
166 : : void notify(CVC5_UNUSED TNode t1, CVC5_UNUSED TNode t2) {}
167 : : };
168 : :
169 : : /** The notify class for d_ppEqualityEngine */
170 : : PPNotifyClass d_ppNotify;
171 : :
172 : : /** Equaltity engine */
173 : : eq::EqualityEngine d_ppEqualityEngine;
174 : :
175 : : // List of facts learned by preprocessor - needed for permanent ref for
176 : : // benefit of d_ppEqualityEngine
177 : : context::CDList<Node> d_ppFacts;
178 : :
179 : : Node preprocessTerm(TNode term);
180 : : Node recursivePreprocessTerm(TNode term);
181 : : bool ppDisequal(TNode a, TNode b);
182 : : Node solveWrite(TNode term, bool solve1, bool solve2, bool ppCheck);
183 : :
184 : : /** The theory rewriter for this theory. */
185 : : TheoryArraysRewriter d_rewriter;
186 : : /** A (default) theory state object */
187 : : TheoryState d_state;
188 : : /** The arrays inference manager */
189 : : InferenceManager d_im;
190 : :
191 : : public:
192 : : bool ppAssert(TrustNode tin, TrustSubstitutionMap& outSubstitutions) override;
193 : : TrustNode ppRewrite(TNode atom, std::vector<SkolemLemma>& lems) override;
194 : :
195 : : /////////////////////////////////////////////////////////////////////////////
196 : : // T-PROPAGATION / REGISTRATION
197 : : /////////////////////////////////////////////////////////////////////////////
198 : :
199 : : private:
200 : : /** Literals to propagate */
201 : : context::CDList<Node> d_literalsToPropagate;
202 : :
203 : : /** Index of the next literal to propagate */
204 : : context::CDO<unsigned> d_literalsToPropagateIndex;
205 : :
206 : : /** Should be called to propagate the literal. */
207 : : bool propagateLit(TNode literal);
208 : :
209 : : /** For debugging only- checks invariants about when things are
210 : : * preregistered*/
211 : : context::CDHashSet<Node> d_isPreRegistered;
212 : :
213 : : /** Helper for preRegisterTerm, also used internally */
214 : : void preRegisterTermInternal(TNode n);
215 : :
216 : : public:
217 : : void preRegisterTerm(TNode n) override;
218 : : TrustNode explain(TNode n) override;
219 : :
220 : : /////////////////////////////////////////////////////////////////////////////
221 : : // SHARING
222 : : /////////////////////////////////////////////////////////////////////////////
223 : :
224 : : private:
225 : : class MayEqualNotifyClass
226 : : {
227 : : public:
228 : : bool notify(CVC5_UNUSED TNode propagation) { return true; }
229 : : void notify(CVC5_UNUSED TNode t1, CVC5_UNUSED TNode t2) {}
230 : : };
231 : :
232 : : /** The notify class for d_mayEqualEqualityEngine */
233 : : MayEqualNotifyClass d_mayEqualNotify;
234 : :
235 : : /** Equaltity engine for determining if two arrays might be equal */
236 : : eq::EqualityEngine d_mayEqualEqualityEngine;
237 : :
238 : : // Helper for computeCareGraph
239 : : void checkPair(TNode r1, TNode r2);
240 : :
241 : : public:
242 : : void notifySharedTerm(TNode t) override;
243 : : void computeCareGraph() override;
244 : : bool isShared(TNode t)
245 : : {
246 : : return (d_sharedArrays.find(t) != d_sharedArrays.end());
247 : : }
248 : :
249 : : /////////////////////////////////////////////////////////////////////////////
250 : : // MODEL GENERATION
251 : : /////////////////////////////////////////////////////////////////////////////
252 : :
253 : : public:
254 : : /** Collect model values in m based on the relevant terms given by termSet */
255 : : bool collectModelValues(TheoryModel* m,
256 : : const std::set<Node>& termSet) override;
257 : :
258 : : /////////////////////////////////////////////////////////////////////////////
259 : : // NOTIFICATIONS
260 : : /////////////////////////////////////////////////////////////////////////////
261 : :
262 : : void presolve() override;
263 : :
264 : : /////////////////////////////////////////////////////////////////////////////
265 : : // MAIN SOLVER
266 : : /////////////////////////////////////////////////////////////////////////////
267 : :
268 : : //--------------------------------- standard check
269 : : /** Post-check, called after the fact queue of the theory is processed. */
270 : : void postCheck(Effort level) override;
271 : : /** Pre-notify fact, return true if processed. */
272 : : bool preNotifyFact(TNode atom,
273 : : bool pol,
274 : : TNode fact,
275 : : bool isPrereg,
276 : : bool isInternal) override;
277 : : /** Notify fact */
278 : : void notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) override;
279 : : //--------------------------------- end standard check
280 : :
281 : : private:
282 : : TNode weakEquivGetRep(TNode node);
283 : : TNode weakEquivGetRepIndex(TNode node, TNode index);
284 : : void visitAllLeaves(TNode reason, std::vector<TNode>& conjunctions);
285 : : void weakEquivBuildCond(TNode node,
286 : : TNode index,
287 : : std::vector<TNode>& conjunctions);
288 : : void weakEquivMakeRep(TNode node);
289 : : void weakEquivMakeRepIndex(TNode node);
290 : : void weakEquivAddSecondary(TNode index,
291 : : TNode arrayFrom,
292 : : TNode arrayTo,
293 : : TNode reason);
294 : : void checkWeakEquiv(bool arraysMerged);
295 : :
296 : : // NotifyClass: template helper class for d_equalityEngine - handles call-back
297 : : // from congruence closure module
298 : : class NotifyClass : public eq::EqualityEngineNotify
299 : : {
300 : : TheoryArrays& d_arrays;
301 : :
302 : : public:
303 : 28740 : NotifyClass(TheoryArrays& arrays) : d_arrays(arrays) {}
304 : :
305 : 915412 : bool eqNotifyTriggerPredicate(TNode predicate, bool value) override
306 : : {
307 [ + - ]: 1830824 : Trace("arrays::propagate")
308 [ - - ]: 915412 : << spaces(d_arrays.context()->getLevel())
309 : 0 : << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", "
310 [ - - ][ - + ]: 915412 : << (value ? "true" : "false") << ")" << std::endl;
311 : : // Just forward to arrays
312 [ + + ]: 915412 : if (value)
313 : : {
314 : 814206 : return d_arrays.propagateLit(predicate);
315 : : }
316 : 101206 : return d_arrays.propagateLit(predicate.notNode());
317 : : }
318 : :
319 : 244969 : bool eqNotifyTriggerTermEquality(CVC5_UNUSED TheoryId tag,
320 : : TNode t1,
321 : : TNode t2,
322 : : bool value) override
323 : : {
324 [ + - ]: 489938 : Trace("arrays::propagate")
325 [ - - ]: 244969 : << spaces(d_arrays.context()->getLevel())
326 : 0 : << "NotifyClass::eqNotifyTriggerTermEquality(" << t1 << ", " << t2
327 [ - - ][ - + ]: 244969 : << ", " << (value ? "true" : "false") << ")" << std::endl;
328 [ + + ]: 244969 : if (value)
329 : : {
330 : : // Propagate equality between shared terms
331 : 179644 : return d_arrays.propagateLit(t1.eqNode(t2));
332 : : }
333 : 65325 : return d_arrays.propagateLit(t1.eqNode(t2).notNode());
334 : : }
335 : :
336 : 209 : void eqNotifyConstantTermMerge(TNode t1, TNode t2) override
337 : : {
338 [ + - ][ - + ]: 418 : Trace("arrays::propagate") << spaces(d_arrays.context()->getLevel())
[ - - ]
339 : 0 : << "NotifyClass::eqNotifyConstantTermMerge("
340 : 209 : << t1 << ", " << t2 << ")" << std::endl;
341 : 209 : d_arrays.conflict(t1, t2);
342 : 209 : }
343 : :
344 : 53350 : void eqNotifyNewClass(TNode t) override
345 : : {
346 : 53350 : d_arrays.preRegisterTermInternal(t);
347 : 53350 : }
348 : 1696681 : void eqNotifyMerge(TNode t1, TNode t2) override
349 : : {
350 [ + + ]: 1696681 : if (t1.getType().isArray())
351 : : {
352 : 10618 : d_arrays.mergeArrays(t1, t2);
353 : : }
354 : 1696678 : }
355 : 89104 : void eqNotifyDisequal(CVC5_UNUSED TNode t1,
356 : : CVC5_UNUSED TNode t2,
357 : : CVC5_UNUSED TNode reason) override
358 : : {
359 : 89104 : }
360 : : };
361 : :
362 : : /** The notify class for d_equalityEngine */
363 : : NotifyClass d_notify;
364 : :
365 : : /** The proof checker */
366 : : ArraysProofRuleChecker d_checker;
367 : :
368 : : /** Conflict when merging constants */
369 : : void conflict(TNode a, TNode b);
370 : :
371 : : /** The conflict node */
372 : : Node d_conflictNode;
373 : :
374 : : /**
375 : : * Context dependent map from a congruence class canonical representative of
376 : : * type array to an Info pointer that keeps track of information useful to
377 : : * axiom instantiation
378 : : */
379 : : ArrayInfo d_infoMap;
380 : :
381 : : context::CDQueue<Node> d_mergeQueue;
382 : :
383 : : bool d_mergeInProgress;
384 : :
385 : : using RowLemmaType = std::tuple<TNode, TNode, TNode, TNode>;
386 : :
387 : : context::CDQueue<RowLemmaType> d_RowQueue;
388 : : context::CDHashSet<RowLemmaType, RowLemmaTypeHashFunction> d_RowAlreadyAdded;
389 : :
390 : : typedef context::CDHashSet<Node> CDNodeSet;
391 : :
392 : : CDNodeSet d_sharedArrays;
393 : : CDNodeSet d_sharedOther;
394 : : context::CDO<bool> d_sharedTerms;
395 : :
396 : : // Map from constant values to read terms that read from that values equal to
397 : : // that constant value in the current model When a new read term is created,
398 : : // we check the index to see if we know the model value. If so, we add it to
399 : : // d_constReads (and d_constReadsList) If not, we push it onto d_reads and
400 : : // figure out where it goes at computeCareGraph time. d_constReadsList is used
401 : : // as a backup in case we can't compute the model at computeCareGraph time.
402 : : typedef std::unordered_map<Node, CTNodeList*> CNodeNListMap;
403 : : CNodeNListMap d_constReads;
404 : : context::CDList<TNode> d_reads;
405 : : context::CDList<TNode> d_constReadsList;
406 : : context::Context* d_constReadsContext;
407 : : /** Helper class to keep d_constReadsContext in sync with satContext */
408 : : class ContextPopper : public context::ContextNotifyObj
409 : : {
410 : : context::Context* d_satContext;
411 : : context::Context* d_contextToPop;
412 : :
413 : : protected:
414 : 8922283 : void contextNotifyPop() override
415 : : {
416 [ + + ]: 8922283 : if (d_contextToPop->getLevel() > d_satContext->getLevel())
417 : : {
418 : 45309 : d_contextToPop->pop();
419 : : }
420 : 8922283 : }
421 : :
422 : : public:
423 : 28740 : ContextPopper(context::Context* context, context::Context* contextToPop)
424 : 28740 : : context::ContextNotifyObj(context),
425 : 28740 : d_satContext(context),
426 : 28740 : d_contextToPop(contextToPop)
427 : : {
428 : 28740 : }
429 : :
430 : : }; /* class ContextPopper */
431 : : ContextPopper d_contextPopper;
432 : :
433 : : // The decision requests we have for the core
434 : : context::CDQueue<Node> d_decisionRequests;
435 : :
436 : : // List of nodes that need permanent references in this context
437 : : context::CDList<Node> d_permRef;
438 : : context::CDList<Node> d_modelConstraints;
439 : : context::CDHashSet<Node> d_lemmasSaved;
440 : : std::vector<Node> d_lemmas;
441 : :
442 : : // Default values for each mayEqual equivalence class
443 : : typedef context::CDHashMap<Node, Node> DefValMap;
444 : : DefValMap d_defValues;
445 : :
446 : : typedef std::
447 : : unordered_map<std::pair<TNode, TNode>, CTNodeList*, TNodePairHashFunction>
448 : : ReadBucketMap;
449 : : ReadBucketMap d_readBucketTable;
450 : : context::Context* d_readTableContext;
451 : : context::CDList<Node> d_arrayMerges;
452 : : std::vector<CTNodeList*> d_readBucketAllocations;
453 : :
454 : : Node getSkolem(TNode ref);
455 : : Node mkAnd(std::vector<TNode>& conjunctions,
456 : : bool invert = false,
457 : : unsigned startIndex = 0);
458 : : void setNonLinear(TNode a);
459 : : Node removeRepLoops(TNode a, TNode rep);
460 : : Node expandStores(TNode s,
461 : : std::vector<TNode>& assumptions,
462 : : bool checkLoop = false,
463 : : TNode a = TNode(),
464 : : TNode b = TNode());
465 : : void mergeArrays(TNode a, TNode b);
466 : : void checkStore(TNode a);
467 : : void checkRowForIndex(TNode i, TNode a);
468 : : void checkRowLemmas(TNode a, TNode b);
469 : : void propagateRowLemma(RowLemmaType lem);
470 : : void queueRowLemma(RowLemmaType lem);
471 : : bool dischargeLemmas();
472 : :
473 : : /**
474 : : * The decision strategy for the theory of arrays, which calls the
475 : : * getNextDecisionEngineRequest function below.
476 : : */
477 : : class TheoryArraysDecisionStrategy : public DecisionStrategy
478 : : {
479 : : public:
480 : : TheoryArraysDecisionStrategy(TheoryArrays* ta);
481 : : /** initialize */
482 : : void initialize() override;
483 : : /** get next decision request */
484 : : Node getNextDecisionRequest() override;
485 : : /** identify */
486 : : std::string identify() const override;
487 : :
488 : : private:
489 : : /** pointer to the theory of arrays */
490 : : TheoryArrays* d_ta;
491 : : };
492 : : /** an instance of the above decision strategy */
493 : : std::unique_ptr<TheoryArraysDecisionStrategy> d_dstrat;
494 : : /** Have we registered the above strategy? (context-independent) */
495 : : bool d_dstratInit;
496 : : /** get the next decision request
497 : : *
498 : : * If the "arrays-eager-index" option is enabled, then whenever a
499 : : * read-over-write lemma is generated, a decision request is also generated
500 : : * for the comparison between the indexes that appears in the lemma.
501 : : */
502 : : Node getNextDecisionRequest();
503 : : /**
504 : : * Compute relevant terms. This includes select nodes for the
505 : : * RIntro1 and RIntro2 rules.
506 : : */
507 : : void computeRelevantTerms(std::set<Node>& termSet) override;
508 : : }; /* class TheoryArrays */
509 : :
510 : : } // namespace arrays
511 : : } // namespace theory
512 : : } // namespace cvc5::internal
513 : :
514 : : #endif /* CVC5__THEORY__ARRAYS__THEORY_ARRAYS_H */
|
