Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Clark Barrett, Andrew Reynolds, Morgan Deters
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 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 : : * Implementation of the theory of arrays.
14 : : */
15 : :
16 : : #include "theory/arrays/theory_arrays.h"
17 : :
18 : : #include <map>
19 : : #include <memory>
20 : :
21 : : #include "expr/array_store_all.h"
22 : : #include "expr/kind.h"
23 : : #include "expr/node_algorithm.h"
24 : : #include "options/arrays_options.h"
25 : : #include "options/smt_options.h"
26 : : #include "proof/proof_checker.h"
27 : : #include "smt/logic_exception.h"
28 : : #include "theory/arrays/skolem_cache.h"
29 : : #include "theory/arrays/theory_arrays_rewriter.h"
30 : : #include "theory/decision_manager.h"
31 : : #include "theory/theory_model.h"
32 : : #include "theory/trust_substitutions.h"
33 : : #include "theory/valuation.h"
34 : :
35 : : using namespace std;
36 : :
37 : : namespace cvc5::internal {
38 : : namespace theory {
39 : : namespace arrays {
40 : :
41 : : // These are the options that produce the best empirical results on QF_AX benchmarks.
42 : : // eagerLemmas = true
43 : : // eagerIndexSplitting = false
44 : :
45 : : // Use static configuration of options for now
46 : : const bool d_ccStore = false;
47 : : //const bool d_eagerLemmas = false;
48 : : const bool d_preprocess = true;
49 : : const bool d_solveWrite = true;
50 : : const bool d_solveWrite2 = false;
51 : : // These are now options
52 : : //const bool d_propagateLemmas = true;
53 : : //bool d_useNonLinearOpt = true;
54 : : //bool d_eagerIndexSplitting = false;
55 : :
56 : 50855 : TheoryArrays::TheoryArrays(Env& env,
57 : : OutputChannel& out,
58 : : Valuation valuation,
59 : 50855 : std::string name)
60 : : : Theory(THEORY_ARRAYS, env, out, valuation, name),
61 : 50855 : d_numRow(statisticsRegistry().registerInt(name + "number of Row lemmas")),
62 : 50855 : d_numExt(statisticsRegistry().registerInt(name + "number of Ext lemmas")),
63 : : d_numProp(
64 : 50855 : statisticsRegistry().registerInt(name + "number of propagations")),
65 : : d_numExplain(
66 : 50855 : statisticsRegistry().registerInt(name + "number of explanations")),
67 : 50855 : d_numNonLinear(statisticsRegistry().registerInt(
68 : 50855 : name + "number of calls to setNonLinear")),
69 : 50855 : d_numSharedArrayVarSplits(statisticsRegistry().registerInt(
70 : 50855 : name + "number of shared array var splits")),
71 : 50855 : d_numGetModelValSplits(statisticsRegistry().registerInt(
72 : 50855 : name + "number of getModelVal splits")),
73 : 50855 : d_numGetModelValConflicts(statisticsRegistry().registerInt(
74 : 50855 : name + "number of getModelVal conflicts")),
75 : 50855 : d_numSetModelValSplits(statisticsRegistry().registerInt(
76 : 50855 : name + "number of setModelVal splits")),
77 : 50855 : d_numSetModelValConflicts(statisticsRegistry().registerInt(
78 : 50855 : name + "number of setModelVal conflicts")),
79 : 101710 : d_ppEqualityEngine(env, userContext(), name + "pp", true),
80 : 101710 : d_ppFacts(userContext()),
81 : : d_rewriter(env.getNodeManager(), env.getRewriter()),
82 : : d_state(env, valuation),
83 : 50855 : d_im(env, *this, d_state),
84 : : d_literalsToPropagate(context()),
85 : 0 : d_literalsToPropagateIndex(context(), 0),
86 : : d_isPreRegistered(context()),
87 : 50855 : d_mayEqualEqualityEngine(env, context(), name + "mayEqual", true),
88 : : d_notify(*this),
89 : : d_checker(nodeManager()),
90 : : d_infoMap(statisticsRegistry(), context(), name),
91 : : d_mergeQueue(context()),
92 : : d_mergeInProgress(false),
93 : : d_RowQueue(context()),
94 : 101710 : d_RowAlreadyAdded(userContext()),
95 : : d_sharedArrays(context()),
96 : : d_sharedOther(context()),
97 : 0 : d_sharedTerms(context(), false),
98 : : d_reads(context()),
99 : : d_constReadsList(context()),
100 : 50855 : d_constReadsContext(new context::Context()),
101 : : d_contextPopper(context(), d_constReadsContext),
102 : : d_decisionRequests(context()),
103 : : d_permRef(context()),
104 : : d_modelConstraints(context()),
105 : : d_lemmasSaved(context()),
106 : : d_defValues(context()),
107 : 50855 : d_readTableContext(new context::Context()),
108 : : d_arrayMerges(context()),
109 : 50855 : d_dstrat(new TheoryArraysDecisionStrategy(this)),
110 : 406840 : d_dstratInit(false)
111 : : {
112 : 50855 : d_true = nodeManager()->mkConst<bool>(true);
113 : 50855 : d_false = nodeManager()->mkConst<bool>(false);
114 : :
115 : : // The preprocessing congruence kinds
116 : 50855 : d_ppEqualityEngine.addFunctionKind(Kind::SELECT);
117 : 50855 : d_ppEqualityEngine.addFunctionKind(Kind::STORE);
118 : :
119 : : // indicate we are using the default theory state object, and the arrays
120 : : // inference manager
121 : 50855 : d_theoryState = &d_state;
122 : 50855 : d_inferManager = &d_im;
123 : 50855 : }
124 : :
125 : 101198 : TheoryArrays::~TheoryArrays() {
126 : 50599 : vector<CTNodeList*>::iterator it = d_readBucketAllocations.begin(), iend = d_readBucketAllocations.end();
127 [ - + ]: 50599 : for (; it != iend; ++it) {
128 : 0 : (*it)->deleteSelf();
129 : : }
130 [ + - ]: 50599 : delete d_readTableContext;
131 : 50599 : CNodeNListMap::iterator it2 = d_constReads.begin();
132 [ + + ]: 51808 : for( ; it2 != d_constReads.end(); ++it2 ) {
133 : 1209 : it2->second->deleteSelf();
134 : : }
135 [ + - ]: 50599 : delete d_constReadsContext;
136 : 101198 : }
137 : :
138 : 50855 : TheoryRewriter* TheoryArrays::getTheoryRewriter() { return &d_rewriter; }
139 : :
140 : 20017 : ProofRuleChecker* TheoryArrays::getProofChecker() { return &d_checker; }
141 : :
142 : 50855 : bool TheoryArrays::needsEqualityEngine(EeSetupInfo& esi)
143 : : {
144 : 50855 : esi.d_notify = &d_notify;
145 : 50855 : esi.d_name = d_instanceName + "ee";
146 : 50855 : esi.d_notifyNewClass = true;
147 : 50855 : esi.d_notifyMerge = true;
148 : 50855 : return true;
149 : : }
150 : :
151 : 50855 : void TheoryArrays::finishInit()
152 : : {
153 [ - + ][ - + ]: 50855 : Assert(d_equalityEngine != nullptr);
[ - - ]
154 : :
155 : : // The kinds we are treating as function application in congruence
156 : 50855 : d_equalityEngine->addFunctionKind(Kind::SELECT);
157 : : if (d_ccStore)
158 : : {
159 : : d_equalityEngine->addFunctionKind(Kind::STORE);
160 : : }
161 : 50855 : }
162 : :
163 : : /////////////////////////////////////////////////////////////////////////////
164 : : // PREPROCESSING
165 : : /////////////////////////////////////////////////////////////////////////////
166 : :
167 : :
168 : 6384 : bool TheoryArrays::ppDisequal(TNode a, TNode b) {
169 : 6384 : bool termsExist = d_ppEqualityEngine.hasTerm(a) && d_ppEqualityEngine.hasTerm(b);
170 : 6384 : Assert(!termsExist || !a.isConst() || !b.isConst() || a == b
171 : : || d_ppEqualityEngine.areDisequal(a, b, false));
172 : 12768 : return ((termsExist && d_ppEqualityEngine.areDisequal(a, b, false))
173 : 19152 : || rewrite(a.eqNode(b)) == d_false);
174 : : }
175 : :
176 : :
177 : 0 : Node TheoryArrays::solveWrite(TNode term, bool solve1, bool solve2, bool ppCheck)
178 : : {
179 [ - - ]: 0 : if (!solve1) {
180 : 0 : return term;
181 : : }
182 : 0 : if (term[0].getKind() != Kind::STORE && term[1].getKind() != Kind::STORE)
183 : : {
184 : 0 : return term;
185 : : }
186 : 0 : TNode left = term[0];
187 : 0 : TNode right = term[1];
188 : 0 : int leftWrites = 0, rightWrites = 0;
189 : :
190 : : // Count nested writes
191 : 0 : TNode e1 = left;
192 [ - - ]: 0 : while (e1.getKind() == Kind::STORE)
193 : : {
194 : 0 : ++leftWrites;
195 : 0 : e1 = e1[0];
196 : : }
197 : :
198 : 0 : TNode e2 = right;
199 [ - - ]: 0 : while (e2.getKind() == Kind::STORE)
200 : : {
201 : 0 : ++rightWrites;
202 : 0 : e2 = e2[0];
203 : : }
204 : :
205 [ - - ]: 0 : if (rightWrites > leftWrites) {
206 : 0 : TNode tmp = left;
207 : 0 : left = right;
208 : 0 : right = tmp;
209 : 0 : int tmpWrites = leftWrites;
210 : 0 : leftWrites = rightWrites;
211 : 0 : rightWrites = tmpWrites;
212 : : }
213 : :
214 : 0 : NodeManager* nm = nodeManager();
215 [ - - ]: 0 : if (rightWrites == 0) {
216 [ - - ]: 0 : if (e1 != e2) {
217 : 0 : return term;
218 : : }
219 : : // write(store, index_0, v_0, index_1, v_1, ..., index_n, v_n) = store IFF
220 : : //
221 : : // read(store, index_n) = v_n &
222 : : // index_{n-1} != index_n -> read(store, index_{n-1}) = v_{n-1} &
223 : : // (index_{n-2} != index_{n-1} & index_{n-2} != index_n) -> read(store, index_{n-2}) = v_{n-2} &
224 : : // ...
225 : : // (index_1 != index_2 & ... & index_1 != index_n) -> read(store, index_1) = v_1
226 : : // (index_0 != index_1 & index_0 != index_2 & ... & index_0 != index_n) -> read(store, index_0) = v_0
227 : 0 : TNode write_i, write_j, index_i, index_j;
228 : 0 : Node conc;
229 : 0 : NodeBuilder result(nm, Kind::AND);
230 : : int i, j;
231 : 0 : write_i = left;
232 [ - - ]: 0 : for (i = leftWrites-1; i >= 0; --i) {
233 : 0 : index_i = write_i[1];
234 : :
235 : : // build: [index_i /= index_n && index_i /= index_(n-1) &&
236 : : // ... && index_i /= index_(i+1)] -> read(store, index_i) = v_i
237 : 0 : write_j = left;
238 : : {
239 : 0 : NodeBuilder hyp(nm, Kind::AND);
240 [ - - ]: 0 : for (j = leftWrites - 1; j > i; --j) {
241 : 0 : index_j = write_j[1];
242 : 0 : if (!ppCheck || !ppDisequal(index_i, index_j)) {
243 : 0 : Node hyp2(index_i.eqNode(index_j));
244 : 0 : hyp << hyp2.notNode();
245 : : }
246 : 0 : write_j = write_j[0];
247 : : }
248 : :
249 : 0 : Node r1 = nm->mkNode(Kind::SELECT, e1, index_i);
250 : 0 : conc = r1.eqNode(write_i[2]);
251 [ - - ]: 0 : if (hyp.getNumChildren() != 0) {
252 [ - - ]: 0 : if (hyp.getNumChildren() == 1) {
253 : 0 : conc = hyp.getChild(0).impNode(conc);
254 : : }
255 : : else {
256 : 0 : r1 = hyp;
257 : 0 : conc = r1.impNode(conc);
258 : : }
259 : : }
260 : :
261 : : // And into result
262 : 0 : result << conc;
263 : :
264 : : // Prepare for next iteration
265 : 0 : write_i = write_i[0];
266 : : }
267 : : }
268 : 0 : Assert(result.getNumChildren() > 0);
269 [ - - ]: 0 : if (result.getNumChildren() == 1) {
270 : 0 : return result.getChild(0);
271 : : }
272 : 0 : return result;
273 : : }
274 : : else {
275 [ - - ]: 0 : if (!solve2) {
276 : 0 : return term;
277 : : }
278 : : // store(...) = store(a,i,v) ==>
279 : : // store(store(...),i,select(a,i)) = a && select(store(...),i)=v
280 : 0 : Node l = left;
281 : 0 : Node tmp;
282 : 0 : NodeBuilder nb(nm, Kind::AND);
283 [ - - ]: 0 : while (right.getKind() == Kind::STORE)
284 : : {
285 : 0 : tmp = nm->mkNode(Kind::SELECT, l, right[1]);
286 : 0 : nb << tmp.eqNode(right[2]);
287 : 0 : tmp = nm->mkNode(Kind::SELECT, right[0], right[1]);
288 : 0 : l = nm->mkNode(Kind::STORE, l, right[1], tmp);
289 : 0 : right = right[0];
290 : : }
291 : 0 : nb << solveWrite(l.eqNode(right), solve1, solve2, ppCheck);
292 : 0 : return nb;
293 : : }
294 : : Unreachable();
295 : : return term;
296 : : }
297 : :
298 : 15955 : TrustNode TheoryArrays::ppRewrite(TNode term, std::vector<SkolemLemma>& lems)
299 : : {
300 : : // first, check for logic exceptions
301 : 15955 : Kind k = term.getKind();
302 [ + + ]: 15955 : if (!options().arrays.arraysExp)
303 : : {
304 [ + + ][ - + ]: 13784 : if (k == Kind::EQ_RANGE || k == Kind::STORE_ALL)
305 : : {
306 : 2 : std::stringstream ss;
307 : 1 : ss << "Term of kind `" << k
308 : 1 : << "` not supported in default mode, try `--arrays-exp`.";
309 : 1 : throw LogicException(ss.str());
310 : : }
311 : : }
312 : : // see if we need to expand definitions
313 : 31908 : Node texp = d_rewriter.expandDefinition(term);
314 [ + + ]: 15954 : if (!texp.isNull())
315 : : {
316 : : // do not track proofs here
317 : 30 : return TrustNode::mkTrustRewrite(term, texp, nullptr);
318 : : }
319 : : if (!d_preprocess)
320 : : {
321 : : return TrustNode::null();
322 : : }
323 : 15924 : d_ppEqualityEngine.addTerm(term);
324 : 15924 : NodeManager* nm = nodeManager();
325 : 31848 : Node ret;
326 [ + + ][ - + ]: 15924 : switch (k)
327 : : {
328 : 11698 : case Kind::SELECT:
329 : : {
330 : : // select(store(a,i,v),j) = select(a,j)
331 : : // IF i != j
332 : 11698 : if (term[0].getKind() == Kind::STORE && ppDisequal(term[0][1], term[1]))
333 : : {
334 : 0 : ret = nm->mkNode(Kind::SELECT, term[0][0], term[1]);
335 : : }
336 : 11698 : break;
337 : : }
338 : 3039 : case Kind::STORE:
339 : : {
340 : : // store(store(a,i,v),j,w) = store(store(a,j,w),i,v)
341 : : // IF i != j and j comes before i in the ordering
342 : 4415 : if (term[0].getKind() == Kind::STORE && (term[1] < term[0][1])
343 : 4415 : && ppDisequal(term[1], term[0][1]))
344 : : {
345 : 0 : Node inner = nm->mkNode(Kind::STORE, term[0][0], term[1], term[2]);
346 : 0 : Node outer = nm->mkNode(Kind::STORE, inner, term[0][1], term[0][2]);
347 : 0 : ret = outer;
348 : : }
349 : 3039 : break;
350 : : }
351 : 0 : case Kind::EQUAL:
352 : : {
353 : 0 : ret = solveWrite(term, d_solveWrite, d_solveWrite2, true);
354 : 0 : break;
355 : : }
356 : 1187 : default:
357 : 1187 : break;
358 : : }
359 [ - + ][ - - ]: 15924 : if (!ret.isNull() && ret != term)
[ - + ]
360 : : {
361 : 0 : return TrustNode::mkTrustRewrite(term, ret, nullptr);
362 : : }
363 : 15924 : return TrustNode::null();
364 : : }
365 : :
366 : 696 : bool TheoryArrays::ppAssert(TrustNode tin,
367 : : TrustSubstitutionMap& outSubstitutions)
368 : : {
369 : 1392 : TNode in = tin.getNode();
370 [ + + ][ + ]: 696 : switch(in.getKind()) {
371 : 465 : case Kind::EQUAL:
372 : : {
373 : 465 : d_ppFacts.push_back(in);
374 : 465 : d_ppEqualityEngine.assertEquality(in, true, in);
375 : 465 : if (in[0].isVar() && d_valuation.isLegalElimination(in[0], in[1]))
376 : : {
377 : 156 : outSubstitutions.addSubstitutionSolved(in[0], in[1], tin);
378 : 156 : return true;
379 : : }
380 : 309 : if (in[1].isVar() && d_valuation.isLegalElimination(in[1], in[0]))
381 : : {
382 : 0 : outSubstitutions.addSubstitutionSolved(in[1], in[0], tin);
383 : 0 : return true;
384 : : }
385 : 309 : break;
386 : : }
387 : 134 : case Kind::NOT:
388 : : {
389 : 134 : d_ppFacts.push_back(in);
390 [ + + ]: 134 : if (in[0].getKind() == Kind::EQUAL)
391 : : {
392 : 348 : Node a = in[0][0];
393 : 232 : Node b = in[0][1];
394 : 116 : d_ppEqualityEngine.assertEquality(in[0], false, in);
395 : : }
396 : 134 : break;
397 : : }
398 : 97 : default:
399 : 97 : break;
400 : : }
401 : 540 : return false;
402 : : }
403 : :
404 : :
405 : : /////////////////////////////////////////////////////////////////////////////
406 : : // T-PROPAGATION / REGISTRATION
407 : : /////////////////////////////////////////////////////////////////////////////
408 : :
409 : 158473 : bool TheoryArrays::propagateLit(TNode literal)
410 : : {
411 [ + - ][ - + ]: 316946 : Trace("arrays") << spaces(context()->getLevel())
[ - - ]
412 : 0 : << "TheoryArrays::propagateLit(" << literal << ")"
413 : 158473 : << std::endl;
414 : :
415 : : // If already in conflict, no more propagation
416 [ - + ]: 158473 : if (d_state.isInConflict())
417 : : {
418 : 0 : Trace("arrays") << spaces(context()->getLevel())
419 : 0 : << "TheoryArrays::propagateLit(" << literal
420 : 0 : << "): already in conflict" << std::endl;
421 : 0 : return false;
422 : : }
423 : :
424 : 158473 : bool ok = d_out->propagate(literal);
425 [ + + ]: 158473 : if (!ok) {
426 : 3617 : d_state.notifyInConflict();
427 : : }
428 : 158473 : return ok;
429 : : }/* TheoryArrays::propagate(TNode) */
430 : :
431 : :
432 : 0 : TNode TheoryArrays::weakEquivGetRep(TNode node) {
433 : 0 : TNode pointer;
434 : : while (true) {
435 : 0 : pointer = d_infoMap.getWeakEquivPointer(node);
436 [ - - ]: 0 : if (pointer.isNull()) {
437 : 0 : return node;
438 : : }
439 : 0 : node = pointer;
440 : : }
441 : : }
442 : :
443 : 0 : TNode TheoryArrays::weakEquivGetRepIndex(TNode node, TNode index) {
444 : 0 : Assert(!index.isNull());
445 : 0 : TNode pointer, index2;
446 : : while (true) {
447 : 0 : pointer = d_infoMap.getWeakEquivPointer(node);
448 [ - - ]: 0 : if (pointer.isNull()) {
449 : 0 : return node;
450 : : }
451 : 0 : index2 = d_infoMap.getWeakEquivIndex(node);
452 : 0 : if (index2.isNull() || !d_equalityEngine->areEqual(index, index2))
453 : : {
454 : 0 : node = pointer;
455 : : }
456 : : else {
457 : 0 : TNode secondary = d_infoMap.getWeakEquivSecondary(node);
458 [ - - ]: 0 : if (secondary.isNull()) {
459 : 0 : return node;
460 : : }
461 : 0 : node = secondary;
462 : : }
463 : 0 : }
464 : : }
465 : :
466 : 0 : void TheoryArrays::visitAllLeaves(TNode reason, vector<TNode>& conjunctions) {
467 [ - - ][ - - ]: 0 : switch (reason.getKind()) {
468 : 0 : case Kind::AND:
469 : 0 : Assert(reason.getNumChildren() == 2);
470 : 0 : visitAllLeaves(reason[0], conjunctions);
471 : 0 : visitAllLeaves(reason[1], conjunctions);
472 : 0 : break;
473 : 0 : case Kind::NOT: conjunctions.push_back(reason); break;
474 : 0 : case Kind::EQUAL:
475 : 0 : d_equalityEngine->explainEquality(
476 : : reason[0], reason[1], true, conjunctions);
477 : 0 : break;
478 : 0 : default:
479 : 0 : Unreachable();
480 : : }
481 : 0 : }
482 : :
483 : 0 : void TheoryArrays::weakEquivBuildCond(TNode node, TNode index, vector<TNode>& conjunctions) {
484 : 0 : Assert(!index.isNull());
485 : 0 : TNode pointer, index2;
486 : : while (true) {
487 : 0 : pointer = d_infoMap.getWeakEquivPointer(node);
488 [ - - ]: 0 : if (pointer.isNull()) {
489 : 0 : return;
490 : : }
491 : 0 : index2 = d_infoMap.getWeakEquivIndex(node);
492 [ - - ]: 0 : if (index2.isNull()) {
493 : : // Null index means these two nodes became equal: explain the equality.
494 : 0 : d_equalityEngine->explainEquality(node, pointer, true, conjunctions);
495 : 0 : node = pointer;
496 : : }
497 [ - - ]: 0 : else if (!d_equalityEngine->areEqual(index, index2))
498 : : {
499 : : // If indices are not equal in current context, need to add that to the lemma.
500 : 0 : Node reason = index.eqNode(index2).notNode();
501 : 0 : d_permRef.push_back(reason);
502 : 0 : conjunctions.push_back(reason);
503 : 0 : node = pointer;
504 : : }
505 : : else {
506 : 0 : TNode secondary = d_infoMap.getWeakEquivSecondary(node);
507 [ - - ]: 0 : if (secondary.isNull()) {
508 : 0 : return;
509 : : }
510 : 0 : TNode reason = d_infoMap.getWeakEquivSecondaryReason(node);
511 : 0 : Assert(!reason.isNull());
512 : 0 : visitAllLeaves(reason, conjunctions);
513 : 0 : node = secondary;
514 : : }
515 : 0 : }
516 : : }
517 : :
518 : 0 : void TheoryArrays::weakEquivMakeRep(TNode node) {
519 : 0 : TNode pointer = d_infoMap.getWeakEquivPointer(node);
520 [ - - ]: 0 : if (pointer.isNull()) {
521 : 0 : return;
522 : : }
523 : 0 : weakEquivMakeRep(pointer);
524 : 0 : d_infoMap.setWeakEquivPointer(pointer, node);
525 : 0 : d_infoMap.setWeakEquivIndex(pointer, d_infoMap.getWeakEquivIndex(node));
526 : 0 : d_infoMap.setWeakEquivPointer(node, TNode());
527 : 0 : weakEquivMakeRepIndex(node);
528 : : }
529 : :
530 : 0 : void TheoryArrays::weakEquivMakeRepIndex(TNode node) {
531 : 0 : TNode secondary = d_infoMap.getWeakEquivSecondary(node);
532 [ - - ]: 0 : if (secondary.isNull()) {
533 : 0 : return;
534 : : }
535 : 0 : TNode index = d_infoMap.getWeakEquivIndex(node);
536 : 0 : Assert(!index.isNull());
537 : 0 : TNode index2 = d_infoMap.getWeakEquivIndex(secondary);
538 : 0 : Node reason;
539 : 0 : TNode next;
540 : 0 : while (index2.isNull() || !d_equalityEngine->areEqual(index, index2))
541 : : {
542 : 0 : next = d_infoMap.getWeakEquivPointer(secondary);
543 : 0 : d_infoMap.setWeakEquivSecondary(node, next);
544 : 0 : reason = d_infoMap.getWeakEquivSecondaryReason(node);
545 [ - - ]: 0 : if (index2.isNull()) {
546 : 0 : reason = reason.andNode(secondary.eqNode(next));
547 : : }
548 : : else {
549 : 0 : reason = reason.andNode(index.eqNode(index2).notNode());
550 : : }
551 : 0 : d_permRef.push_back(reason);
552 : 0 : d_infoMap.setWeakEquivSecondaryReason(node, reason);
553 [ - - ]: 0 : if (next.isNull()) {
554 : 0 : return;
555 : : }
556 : 0 : secondary = next;
557 : 0 : index2 = d_infoMap.getWeakEquivIndex(secondary);
558 : : }
559 : 0 : weakEquivMakeRepIndex(secondary);
560 : 0 : d_infoMap.setWeakEquivSecondary(secondary, node);
561 : 0 : d_infoMap.setWeakEquivSecondaryReason(secondary, d_infoMap.getWeakEquivSecondaryReason(node));
562 : 0 : d_infoMap.setWeakEquivSecondary(node, TNode());
563 : 0 : d_infoMap.setWeakEquivSecondaryReason(node, TNode());
564 : : }
565 : :
566 : 0 : void TheoryArrays::weakEquivAddSecondary(TNode index, TNode arrayFrom, TNode arrayTo, TNode reason) {
567 : 0 : std::unordered_set<TNode> marked;
568 : 0 : vector<TNode> index_trail;
569 : 0 : vector<TNode>::iterator it, iend;
570 : 0 : Node equivalence_trail = reason;
571 : 0 : Node current_reason;
572 : 0 : TNode pointer, indexRep;
573 [ - - ]: 0 : if (!index.isNull()) {
574 : 0 : index_trail.push_back(index);
575 : 0 : marked.insert(d_equalityEngine->getRepresentative(index));
576 : : }
577 [ - - ]: 0 : while (arrayFrom != arrayTo) {
578 : 0 : index = d_infoMap.getWeakEquivIndex(arrayFrom);
579 : 0 : pointer = d_infoMap.getWeakEquivPointer(arrayFrom);
580 [ - - ]: 0 : if (!index.isNull()) {
581 : 0 : indexRep = d_equalityEngine->getRepresentative(index);
582 : 0 : if (marked.find(indexRep) == marked.end() && weakEquivGetRepIndex(arrayFrom, index) != arrayTo) {
583 : 0 : weakEquivMakeRepIndex(arrayFrom);
584 : 0 : d_infoMap.setWeakEquivSecondary(arrayFrom, arrayTo);
585 : 0 : current_reason = equivalence_trail;
586 [ - - ]: 0 : for (it = index_trail.begin(), iend = index_trail.end(); it != iend; ++it) {
587 : 0 : current_reason = current_reason.andNode(index.eqNode(*it).notNode());
588 : : }
589 : 0 : d_permRef.push_back(current_reason);
590 : 0 : d_infoMap.setWeakEquivSecondaryReason(arrayFrom, current_reason);
591 : : }
592 : 0 : marked.insert(indexRep);
593 : : }
594 : : else {
595 : 0 : equivalence_trail = equivalence_trail.andNode(arrayFrom.eqNode(pointer));
596 : : }
597 : 0 : arrayFrom = pointer;
598 : : }
599 : 0 : }
600 : :
601 : 0 : void TheoryArrays::checkWeakEquiv(bool arraysMerged) {
602 : 0 : eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(&d_mayEqualEqualityEngine);
603 [ - - ]: 0 : for (; !eqcs_i.isFinished(); ++eqcs_i) {
604 : 0 : Node eqc = (*eqcs_i);
605 [ - - ]: 0 : if (!eqc.getType().isArray()) {
606 : 0 : continue;
607 : : }
608 : 0 : eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, &d_mayEqualEqualityEngine);
609 : 0 : TNode rep = d_mayEqualEqualityEngine.getRepresentative(*eqc_i);
610 : 0 : TNode weakEquivRep = weakEquivGetRep(rep);
611 [ - - ]: 0 : for (; !eqc_i.isFinished(); ++eqc_i) {
612 : 0 : TNode n = *eqc_i;
613 : 0 : Assert(!arraysMerged || weakEquivGetRep(n) == weakEquivRep);
614 : 0 : TNode pointer = d_infoMap.getWeakEquivPointer(n);
615 : 0 : TNode index = d_infoMap.getWeakEquivIndex(n);
616 : 0 : TNode secondary = d_infoMap.getWeakEquivSecondary(n);
617 : 0 : Assert(pointer.isNull() == (weakEquivGetRep(n) == n));
618 : 0 : Assert(!pointer.isNull() || secondary.isNull());
619 : 0 : Assert(!index.isNull() || secondary.isNull());
620 : 0 : Assert(d_infoMap.getWeakEquivSecondaryReason(n).isNull()
621 : : || !secondary.isNull());
622 [ - - ]: 0 : if (!pointer.isNull()) {
623 [ - - ]: 0 : if (index.isNull()) {
624 : 0 : Assert(d_equalityEngine->areEqual(n, pointer));
625 : : }
626 : : else {
627 : 0 : Assert(
628 : : (n.getKind() == Kind::STORE && n[0] == pointer && n[1] == index)
629 : : || (pointer.getKind() == Kind::STORE && pointer[0] == n
630 : : && pointer[1] == index));
631 : : }
632 : : }
633 : : }
634 : : }
635 : 0 : }
636 : :
637 : : /**
638 : : * Stores in d_infoMap the following information for each term a of type array:
639 : : *
640 : : * - all i, such that there exists a term a[i] or a = store(b i v)
641 : : * (i.e. all indices it is being read atl; store(b i v) is implicitly read at
642 : : * position i due to the implicit axiom store(b i v)[i] = v )
643 : : *
644 : : * - all the stores a is congruent to (this information is context dependent)
645 : : *
646 : : * - all store terms of the form store (a i v) (i.e. in which a appears
647 : : * directly; this is invariant because no new store terms are created)
648 : : *
649 : : * Note: completeness depends on having pre-register called on all the input
650 : : * terms before starting to instantiate lemmas.
651 : : */
652 : 119124 : void TheoryArrays::preRegisterTermInternal(TNode node)
653 : : {
654 [ + + ]: 119124 : if (d_state.isInConflict())
655 : : {
656 : 72513 : return;
657 : : }
658 [ + - ][ - + ]: 237930 : Trace("arrays") << spaces(context()->getLevel())
[ - - ]
659 : 0 : << "TheoryArrays::preRegisterTerm(" << node << ")"
660 : 118965 : << std::endl;
661 : 118965 : Kind nk = node.getKind();
662 [ + + ]: 118965 : if (nk == Kind::EQUAL)
663 : : {
664 : : // Add the trigger for equality
665 : : // NOTE: note that if the equality is true or false already, it might not be added
666 : 10215 : d_state.addEqualityEngineTriggerPredicate(node);
667 : 10215 : return;
668 : : }
669 : : // add to equality engine and the may equality engine
670 : 108750 : TypeNode nodeType = node.getType();
671 [ + + ]: 108750 : if (nodeType.isArray())
672 : : {
673 : : // index type should not be an array, otherwise we throw a logic exception
674 [ - + ]: 11498 : if (nodeType.getArrayIndexType().isArray())
675 : : {
676 : 0 : std::stringstream ss;
677 : 0 : ss << "Arrays cannot be indexed by array types, offending array type is "
678 : 0 : << nodeType;
679 : 0 : throw LogicException(ss.str());
680 : : }
681 : 11498 : d_mayEqualEqualityEngine.addTerm(node);
682 : : }
683 [ + + ]: 108750 : if (d_equalityEngine->hasTerm(node))
684 : : {
685 : : // Notice that array terms may be added to its equality engine before
686 : : // being preregistered in the central equality engine architecture.
687 : : // Prior to this, an assertion in this case was:
688 : : // Assert(nk != Kind::SELECT
689 : : // || d_isPreRegistered.find(node) != d_isPreRegistered.end());
690 : 62139 : return;
691 : : }
692 : 46611 : d_equalityEngine->addTerm(node);
693 : :
694 [ + + ][ + + ]: 46611 : switch (node.getKind())
695 : : {
696 : 35940 : case Kind::SELECT:
697 : : {
698 : : // Reads
699 : 71880 : TNode store = d_equalityEngine->getRepresentative(node[0]);
700 : :
701 : : // The may equal needs the store
702 : 35940 : d_mayEqualEqualityEngine.addTerm(store);
703 : :
704 [ - + ]: 35940 : Assert((d_isPreRegistered.insert(node), true));
705 : :
706 [ - + ][ - + ]: 35940 : Assert(d_equalityEngine->getRepresentative(store) == store);
[ - - ]
707 : 35940 : d_infoMap.addIndex(store, node[1]);
708 : :
709 : : // Synchronize d_constReadsContext with SAT context
710 [ - + ][ - + ]: 35940 : Assert(d_constReadsContext->getLevel() <= context()->getLevel());
[ - - ]
711 [ + + ]: 71581 : while (d_constReadsContext->getLevel() < context()->getLevel())
712 : : {
713 : 35641 : d_constReadsContext->push();
714 : : }
715 : :
716 : : // Record read in sharing data structure
717 : 71880 : TNode index = d_equalityEngine->getRepresentative(node[1]);
718 [ + - ][ + + ]: 35940 : if (!options().arrays.arraysWeakEquivalence && index.isConst())
[ + + ]
719 : : {
720 : : CTNodeList* temp;
721 : 6531 : CNodeNListMap::iterator it = d_constReads.find(index);
722 [ + + ]: 6531 : if (it == d_constReads.end())
723 : : {
724 : 856 : temp = new (true) CTNodeList(d_constReadsContext);
725 : 856 : d_constReads[index] = temp;
726 : : }
727 : : else
728 : : {
729 : 5675 : temp = (*it).second;
730 : : }
731 : 6531 : temp->push_back(node);
732 : 6531 : d_constReadsList.push_back(node);
733 : : }
734 : : else
735 : : {
736 : 29409 : d_reads.push_back(node);
737 : : }
738 : :
739 : 35940 : checkRowForIndex(node[1], store);
740 : 35940 : break;
741 : : }
742 : 2124 : case Kind::STORE:
743 : : {
744 : 4248 : TNode a = d_equalityEngine->getRepresentative(node[0]);
745 : :
746 [ + + ]: 2124 : if (node.isConst())
747 : : {
748 : : // Can't use d_mayEqualEqualityEngine to merge node with a because they
749 : : // are both constants, so just set the default value manually for node.
750 [ - + ][ - + ]: 19 : Assert(a == node[0]);
[ - - ]
751 : 19 : d_mayEqualEqualityEngine.addTerm(node);
752 [ - + ][ - + ]: 19 : Assert(d_mayEqualEqualityEngine.getRepresentative(node) == node);
[ - - ]
753 [ - + ][ - + ]: 19 : Assert(d_mayEqualEqualityEngine.getRepresentative(a) == a);
[ - - ]
754 : 19 : DefValMap::iterator it = d_defValues.find(a);
755 [ - + ][ - + ]: 19 : Assert(it != d_defValues.end());
[ - - ]
756 : 19 : d_defValues[node] = (*it).second;
757 : : }
758 : : else
759 : : {
760 : 2105 : d_mayEqualEqualityEngine.assertEquality(node.eqNode(a), true, d_true);
761 [ - + ][ - + ]: 2105 : Assert(d_mayEqualEqualityEngine.consistent());
[ - - ]
762 : : }
763 : :
764 : 4248 : TNode i = node[1];
765 : 4248 : TNode v = node[2];
766 : 2124 : NodeManager* nm = nodeManager();
767 : 6372 : Node ni = nm->mkNode(Kind::SELECT, node, i);
768 [ + - ]: 2124 : if (!d_equalityEngine->hasTerm(ni))
769 : : {
770 : 2124 : preRegisterTermInternal(ni);
771 : : }
772 : : // Apply RIntro1 Rule
773 : 2124 : d_im.assertInference(ni.eqNode(v),
774 : : true,
775 : : InferenceId::ARRAYS_READ_OVER_WRITE_1,
776 : 2124 : d_true,
777 : : ProofRule::ARRAYS_READ_OVER_WRITE_1);
778 : :
779 : 2124 : d_infoMap.addStore(node, node);
780 : 2124 : d_infoMap.addInStore(a, node);
781 : 2124 : d_infoMap.setModelRep(node, node);
782 : :
783 : : // Add-Store for Weak Equivalence
784 [ - + ]: 2124 : if (options().arrays.arraysWeakEquivalence)
785 : : {
786 : 0 : Assert(weakEquivGetRep(node[0]) == weakEquivGetRep(a));
787 : 0 : Assert(weakEquivGetRep(node) == node);
788 : 0 : d_infoMap.setWeakEquivPointer(node, node[0]);
789 : 0 : d_infoMap.setWeakEquivIndex(node, node[1]);
790 : : #ifdef CVC5_ASSERTIONS
791 : 0 : checkWeakEquiv(false);
792 : : #endif
793 : : }
794 : :
795 : 2124 : checkStore(node);
796 : 2124 : break;
797 : : }
798 : 43 : case Kind::STORE_ALL:
799 : : {
800 : 86 : ArrayStoreAll storeAll = node.getConst<ArrayStoreAll>();
801 : 86 : Node defaultValue = storeAll.getValue();
802 [ - + ]: 43 : if (!defaultValue.isConst()) {
803 : 0 : throw LogicException("Array theory solver does not yet support non-constant default values for arrays");
804 : : }
805 : 43 : d_infoMap.setConstArr(node, node);
806 [ - + ][ - + ]: 43 : Assert(d_mayEqualEqualityEngine.getRepresentative(node) == node);
[ - - ]
807 : 43 : d_defValues[node] = defaultValue;
808 : 43 : setNonLinear(node);
809 : 43 : break;
810 : : }
811 : 8504 : default:
812 : : // Variables etc, already processed above
813 : 8504 : break;
814 : : }
815 : : // Invariant: preregistered terms are exactly the terms in the equality engine
816 : : // Disabled, see comment above for Kind::EQUAL
817 : : // Assert(d_equalityEngine->hasTerm(node) ||
818 : : // !d_equalityEngine->consistent());
819 : : }
820 : :
821 : 43593 : void TheoryArrays::preRegisterTerm(TNode node)
822 : : {
823 : 43593 : preRegisterTermInternal(node);
824 : : // If we have a select from an array of Bools, mark it as a term that can be propagated.
825 : : // Note: do this here instead of in preRegisterTermInternal to prevent internal select
826 : : // terms from being propagated out (as this results in an assertion failure).
827 [ + + ][ + + ]: 43593 : if (node.getKind() == Kind::SELECT && node.getType().isBoolean())
[ + + ][ + + ]
[ - - ]
828 : : {
829 : 231 : d_state.addEqualityEngineTriggerPredicate(node);
830 : : }
831 : 43593 : }
832 : :
833 : 14197 : TrustNode TheoryArrays::explain(TNode literal)
834 : : {
835 : 14197 : return d_im.explainLit(literal);
836 : : }
837 : :
838 : : /////////////////////////////////////////////////////////////////////////////
839 : : // SHARING
840 : : /////////////////////////////////////////////////////////////////////////////
841 : :
842 : 73252 : void TheoryArrays::notifySharedTerm(TNode t)
843 : : {
844 [ + - ][ - + ]: 146504 : Trace("arrays::sharing") << spaces(context()->getLevel())
[ - - ]
845 : 0 : << "TheoryArrays::notifySharedTerm(" << t << ")"
846 : 73252 : << std::endl;
847 [ + + ]: 73252 : if (t.getType().isArray()) {
848 : 5161 : d_sharedArrays.insert(t);
849 : : }
850 : : else {
851 : : #ifdef CVC5_ASSERTIONS
852 : 68091 : d_sharedOther.insert(t);
853 : : #endif
854 : 68091 : d_sharedTerms = true;
855 : : }
856 : 73252 : }
857 : :
858 : 803624 : void TheoryArrays::checkPair(TNode r1, TNode r2)
859 : : {
860 [ + - ]: 803624 : Trace("arrays::sharing") << "TheoryArrays::computeCareGraph(): checking reads " << r1 << " and " << r2 << std::endl;
861 : :
862 : 803624 : TNode x = r1[1];
863 : 803624 : TNode y = r2[1];
864 [ - + ][ - + ]: 803624 : Assert(d_equalityEngine->isTriggerTerm(x, THEORY_ARRAYS));
[ - - ]
865 : :
866 : 1607250 : if (d_equalityEngine->hasTerm(x) && d_equalityEngine->hasTerm(y)
867 : 2739650 : && (d_equalityEngine->areEqual(x, y)
868 : 1132400 : || d_equalityEngine->areDisequal(x, y, false)))
869 : : {
870 [ + - ]: 740868 : Trace("arrays::sharing") << "TheoryArrays::computeCareGraph(): equality known, skipping" << std::endl;
871 : 740868 : return;
872 : : }
873 : :
874 : : // If the terms are already known to be equal, we are also in good shape
875 [ + + ]: 62756 : if (d_equalityEngine->areEqual(r1, r2))
876 : : {
877 [ + - ]: 17846 : Trace("arrays::sharing") << "TheoryArrays::computeCareGraph(): equal, skipping" << std::endl;
878 : 17846 : return;
879 : : }
880 : :
881 [ + + ]: 44910 : if (r1[0] != r2[0]) {
882 : : // If arrays are known to be disequal, or cannot become equal, we can continue
883 : 78692 : Assert(d_mayEqualEqualityEngine.hasTerm(r1[0])
884 : : && d_mayEqualEqualityEngine.hasTerm(r2[0]));
885 : 118038 : if (r1[0].getType() != r2[0].getType()
886 : 118038 : || d_equalityEngine->areDisequal(r1[0], r2[0], false))
887 : : {
888 [ + - ]: 17452 : Trace("arrays::sharing") << "TheoryArrays::computeCareGraph(): arrays can't be equal, skipping" << std::endl;
889 : 17452 : return;
890 : : }
891 [ + + ]: 21894 : else if (!d_mayEqualEqualityEngine.areEqual(r1[0], r2[0])) {
892 : 763 : return;
893 : : }
894 : : }
895 : :
896 [ + + ]: 26695 : if (!d_equalityEngine->isTriggerTerm(y, THEORY_ARRAYS))
897 : : {
898 [ + - ]: 15 : Trace("arrays::sharing") << "TheoryArrays::computeCareGraph(): not connected to shared terms, skipping" << std::endl;
899 : 15 : return;
900 : : }
901 : :
902 : : // Get representative trigger terms
903 : : TNode x_shared =
904 : 26680 : d_equalityEngine->getTriggerTermRepresentative(x, THEORY_ARRAYS);
905 : : TNode y_shared =
906 : 26680 : d_equalityEngine->getTriggerTermRepresentative(y, THEORY_ARRAYS);
907 : 26680 : EqualityStatus eqStatusDomain = d_valuation.getEqualityStatus(x_shared, y_shared);
908 [ - - ][ - + ]: 26680 : switch (eqStatusDomain) {
[ + ]
909 : 0 : case EQUALITY_TRUE_AND_PROPAGATED:
910 : : // Should have been propagated to us
911 : 0 : Assert(false);
912 : : break;
913 : 0 : case EQUALITY_TRUE:
914 : : // Missed propagation - need to add the pair so that theory engine can force propagation
915 [ - - ]: 0 : Trace("arrays::sharing") << "TheoryArrays::computeCareGraph(): missed propagation" << std::endl;
916 : 0 : break;
917 : 0 : case EQUALITY_FALSE_AND_PROPAGATED:
918 [ - - ]: 0 : Trace("arrays::sharing") << "TheoryArrays::computeCareGraph(): checkPair "
919 : 0 : "called when false in model"
920 : 0 : << std::endl;
921 : : // Should have been propagated to us
922 : 0 : Assert(false);
923 : : break;
924 : 18883 : case EQUALITY_FALSE: CVC5_FALLTHROUGH;
925 : : case EQUALITY_FALSE_IN_MODEL:
926 : : // This is unlikely, but I think it could happen
927 [ + - ]: 18883 : Trace("arrays::sharing") << "TheoryArrays::computeCareGraph(): checkPair called when false in model" << std::endl;
928 : 18883 : return;
929 : 7797 : default:
930 : : // Covers EQUALITY_TRUE_IN_MODEL (common case) and EQUALITY_UNKNOWN
931 : 7797 : break;
932 : : }
933 : :
934 : : // Add this pair
935 [ + - ]: 7797 : Trace("arrays::sharing") << "TheoryArrays::computeCareGraph(): adding to care-graph" << std::endl;
936 : 7797 : addCarePair(x_shared, y_shared);
937 : : }
938 : :
939 : :
940 : 28217 : void TheoryArrays::computeCareGraph()
941 : : {
942 [ + + ]: 28217 : if (d_sharedArrays.size() > 0) {
943 : 753 : CDNodeSet::key_iterator it1 = d_sharedArrays.key_begin(), it2, iend = d_sharedArrays.key_end();
944 [ + + ]: 3119 : for (; it1 != iend; ++it1) {
945 [ + + ]: 16232 : for (it2 = it1, ++it2; it2 != iend; ++it2) {
946 [ + + ]: 13866 : if ((*it1).getType() != (*it2).getType()) {
947 : 4696 : continue;
948 : : }
949 : 9170 : EqualityStatus eqStatusArr = getEqualityStatus((*it1), (*it2));
950 [ + + ]: 9170 : if (eqStatusArr != EQUALITY_UNKNOWN) {
951 : 8974 : continue;
952 : : }
953 [ - + ][ - + ]: 196 : Assert(d_valuation.getEqualityStatus((*it1), (*it2))
[ - - ]
954 : : == EQUALITY_UNKNOWN);
955 : 196 : addCarePair((*it1), (*it2));
956 : 196 : ++d_numSharedArrayVarSplits;
957 : 196 : return;
958 : : }
959 : : }
960 : : }
961 [ + + ]: 28021 : if (d_sharedTerms) {
962 : : // Synchronize d_constReadsContext with SAT context
963 [ - + ][ - + ]: 1331 : Assert(d_constReadsContext->getLevel() <= context()->getLevel());
[ - - ]
964 [ + + ]: 20562 : while (d_constReadsContext->getLevel() < context()->getLevel())
965 : : {
966 : 19231 : d_constReadsContext->push();
967 : : }
968 : :
969 : : // Go through the read terms and see if there are any to split on
970 : :
971 : : // Give constReadsContext a push so that all the work it does here is erased - models can change if context changes at all
972 : : // The context is popped at the end. If this loop is interrupted for some reason, we have to make sure the context still
973 : : // gets popped or the solver will be in an inconsistent state
974 : 1331 : d_constReadsContext->push();
975 : 1331 : unsigned size = d_reads.size();
976 [ + + ]: 18546 : for (unsigned i = 0; i < size; ++ i) {
977 : 17215 : TNode r1 = d_reads[i];
978 : :
979 [ + - ]: 17215 : Trace("arrays::sharing") << "TheoryArrays::computeCareGraph(): checking read " << r1 << std::endl;
980 [ - + ][ - + ]: 17215 : Assert(d_equalityEngine->hasTerm(r1));
[ - - ]
981 : 17215 : TNode x = r1[1];
982 : :
983 [ + + ]: 17215 : if (!d_equalityEngine->isTriggerTerm(x, THEORY_ARRAYS))
984 : : {
985 [ + - ]: 174 : Trace("arrays::sharing") << "TheoryArrays::computeCareGraph(): not connected to shared terms, skipping" << std::endl;
986 : 174 : continue;
987 : : }
988 : : Node x_shared =
989 : 51123 : d_equalityEngine->getTriggerTermRepresentative(x, THEORY_ARRAYS);
990 : :
991 : : // Get the model value of index and find all reads that read from that same model value: these are the pairs we have to check
992 : : // Also, insert this read in the list at the proper index
993 : :
994 [ + + ]: 17041 : if (!x_shared.isConst()) {
995 : 12000 : x_shared = d_valuation.getCandidateModelValue(x_shared);
996 : : }
997 [ + + ]: 17041 : if (!x_shared.isNull()) {
998 : : CTNodeList* temp;
999 : 12730 : CNodeNListMap::iterator it = d_constReads.find(x_shared);
1000 [ + + ]: 12730 : if (it == d_constReads.end()) {
1001 : : // This is the only x_shared with this model value - no need to create any splits
1002 : 353 : temp = new(true) CTNodeList(d_constReadsContext);
1003 : 353 : d_constReads[x_shared] = temp;
1004 : : }
1005 : : else {
1006 : 12377 : temp = (*it).second;
1007 [ + + ]: 458033 : for (size_t j = 0; j < temp->size(); ++j) {
1008 : 445656 : checkPair(r1, (*temp)[j]);
1009 : : }
1010 : : }
1011 : 12730 : temp->push_back(r1);
1012 : : }
1013 : : else {
1014 : : // We don't know the model value for x. Just do brute force examination of all pairs of reads.
1015 : : // Note that we have to loop over *all* reads here, not just subsequent reads, because there
1016 : : // may be an earlier read that *does* have a model value. So if we don't check here, the two
1017 : : // reads won't get compared.
1018 [ + + ]: 344248 : for (unsigned j = 0; j < size; ++j)
1019 : : {
1020 : 339937 : TNode r2 = d_reads[j];
1021 [ - + ][ - + ]: 339937 : Assert(d_equalityEngine->hasTerm(r2));
[ - - ]
1022 : 339937 : checkPair(r1,r2);
1023 : : }
1024 [ + + ]: 22342 : for (unsigned j = 0; j < d_constReadsList.size(); ++j) {
1025 : 18031 : TNode r2 = d_constReadsList[j];
1026 [ - + ][ - + ]: 18031 : Assert(d_equalityEngine->hasTerm(r2));
[ - - ]
1027 : 18031 : checkPair(r1,r2);
1028 : : }
1029 : : }
1030 : : }
1031 : 1331 : d_constReadsContext->pop();
1032 : : }
1033 : : }
1034 : :
1035 : :
1036 : : /////////////////////////////////////////////////////////////////////////////
1037 : : // MODEL GENERATION
1038 : : /////////////////////////////////////////////////////////////////////////////
1039 : :
1040 : 14918 : bool TheoryArrays::collectModelValues(TheoryModel* m,
1041 : : const std::set<Node>& termSet)
1042 : : {
1043 : : // termSet contains terms appearing in assertions and shared terms, and also
1044 : : // includes additional reads due to the RIntro1 and RIntro2 rules.
1045 : 14918 : NodeManager* nm = nodeManager();
1046 : : // Compute arrays that we need to produce representatives for
1047 : 29836 : std::vector<Node> arrays;
1048 : :
1049 : 14918 : eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(d_equalityEngine);
1050 [ + + ]: 49313 : for (; !eqcs_i.isFinished(); ++eqcs_i)
1051 : : {
1052 : 34395 : Node eqc = (*eqcs_i);
1053 [ + + ]: 34395 : if (!eqc.getType().isArray())
1054 : : {
1055 : : // not an array, skip
1056 : 33493 : continue;
1057 : : }
1058 : 902 : eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, d_equalityEngine);
1059 [ + + ]: 1199 : for (; !eqc_i.isFinished(); ++eqc_i)
1060 : : {
1061 : 938 : Node n = *eqc_i;
1062 : : // If this EC is an array type and it contains something other than STORE
1063 : : // nodes, we have to compute a representative explicitly
1064 [ + + ]: 938 : if (termSet.find(n) != termSet.end())
1065 : : {
1066 [ + + ]: 900 : if (n.getKind() != Kind::STORE)
1067 : : {
1068 : 641 : arrays.push_back(n);
1069 : 641 : break;
1070 : : }
1071 : : }
1072 : : }
1073 : : }
1074 : :
1075 : : // Build a list of all the relevant reads, indexed by the store representative
1076 : 29836 : std::map<Node, std::vector<Node> > selects;
1077 : 14918 : set<Node>::iterator set_it = termSet.begin(), set_it_end = termSet.end();
1078 [ + + ]: 23324 : for (; set_it != set_it_end; ++set_it)
1079 : : {
1080 : 16812 : Node n = *set_it;
1081 : : // If this term is a select, record that the EC rep of its store parameter
1082 : : // is being read from using this term
1083 [ + + ]: 8406 : if (n.getKind() == Kind::SELECT)
1084 : : {
1085 : 3581 : selects[d_equalityEngine->getRepresentative(n[0])].push_back(n);
1086 : : }
1087 : : }
1088 : :
1089 : 29836 : Node rep;
1090 : 14918 : DefValMap::iterator it;
1091 : 29836 : TypeSet defaultValuesSet;
1092 : :
1093 : : // Compute all default values already in use
1094 : : // if (fullModel) {
1095 [ + + ]: 15559 : for (size_t i = 0; i < arrays.size(); ++i)
1096 : : {
1097 : 1282 : TNode nrep = d_equalityEngine->getRepresentative(arrays[i]);
1098 : 641 : d_mayEqualEqualityEngine.addTerm(
1099 : : nrep); // add the term in case it isn't there already
1100 : 1282 : TNode mayRep = d_mayEqualEqualityEngine.getRepresentative(nrep);
1101 : 641 : it = d_defValues.find(mayRep);
1102 [ + + ]: 641 : if (it != d_defValues.end())
1103 : : {
1104 : 87 : defaultValuesSet.add(nrep.getType().getArrayConstituentType(),
1105 : 87 : (*it).second);
1106 : : }
1107 : : }
1108 : : //}
1109 : :
1110 : : // Loop through all array equivalence classes that need a representative
1111 : : // computed
1112 : : // The default values map for arrays not appearing in d_defValues. This map
1113 : : // is local to the current model.
1114 : 29836 : std::map<Node, Node> defMap;
1115 : 14918 : std::map<Node, Node>::iterator itd;
1116 [ + + ]: 15559 : for (size_t i = 0; i < arrays.size(); ++i)
1117 : : {
1118 : 641 : TNode n = arrays[i];
1119 : 641 : TNode nrep = d_equalityEngine->getRepresentative(n);
1120 : :
1121 : : // if (fullModel) {
1122 : : // Compute default value for this array - there is one default value for
1123 : : // every mayEqual equivalence class
1124 : 641 : TNode mayRep = d_mayEqualEqualityEngine.getRepresentative(nrep);
1125 : : // If this mayEqual EC doesn't have a default value associated, get the next
1126 : : // available default value for the associated array element type
1127 : 641 : it = d_defValues.find(mayRep);
1128 [ + + ]: 641 : if (it == d_defValues.end())
1129 : : {
1130 : 554 : itd = defMap.find(mayRep);
1131 [ + + ]: 554 : if (itd == defMap.end())
1132 : : {
1133 : 484 : TypeNode valueType = nrep.getType().getArrayConstituentType();
1134 : 484 : rep = defaultValuesSet.nextTypeEnum(valueType);
1135 [ - + ]: 484 : if (rep.isNull())
1136 : : {
1137 : 0 : Assert(defaultValuesSet.getSet(valueType)->begin()
1138 : : != defaultValuesSet.getSet(valueType)->end());
1139 : 0 : rep = *(defaultValuesSet.getSet(valueType)->begin());
1140 : : }
1141 [ + - ]: 484 : Trace("arrays-models") << "New default value = " << rep << endl;
1142 : 484 : defMap[mayRep] = rep;
1143 : : }
1144 : : else
1145 : : {
1146 : 70 : rep = itd->second;
1147 : : }
1148 : : }
1149 : : else
1150 : : {
1151 : 87 : rep = (*it).second;
1152 : : }
1153 : :
1154 : : // Build the STORE_ALL term with the default value
1155 : 641 : rep = nm->mkConst(ArrayStoreAll(nrep.getType(), rep));
1156 : :
1157 : : // For each read, require that the rep stores the right value
1158 : 641 : vector<Node>& reads = selects[nrep];
1159 [ + + ]: 3248 : for (unsigned j = 0; j < reads.size(); ++j)
1160 : : {
1161 : 2607 : rep = nm->mkNode(Kind::STORE, rep, reads[j][1], reads[j]);
1162 : : }
1163 [ - + ]: 641 : if (!m->assertEquality(n, rep, true))
1164 : : {
1165 : 0 : return false;
1166 : : }
1167 [ + + ]: 641 : if (!n.isConst())
1168 : : {
1169 : 555 : m->assertSkeleton(rep);
1170 : : }
1171 : : }
1172 : 14918 : return true;
1173 : : }
1174 : :
1175 : : /////////////////////////////////////////////////////////////////////////////
1176 : : // NOTIFICATIONS
1177 : : /////////////////////////////////////////////////////////////////////////////
1178 : :
1179 : :
1180 : 50846 : void TheoryArrays::presolve()
1181 : : {
1182 [ + - ]: 50846 : Trace("arrays")<<"Presolving \n";
1183 [ + + ]: 50846 : if (!d_dstratInit)
1184 : : {
1185 : 42098 : d_dstratInit = true;
1186 : : // add the decision strategy, which is user-context-independent
1187 : 84196 : d_im.getDecisionManager()->registerStrategy(
1188 : : DecisionManager::STRAT_ARRAYS,
1189 : 42098 : d_dstrat.get(),
1190 : : DecisionManager::STRAT_SCOPE_CTX_INDEPENDENT);
1191 : : }
1192 : 50846 : }
1193 : :
1194 : :
1195 : : /////////////////////////////////////////////////////////////////////////////
1196 : : // MAIN SOLVER
1197 : : /////////////////////////////////////////////////////////////////////////////
1198 : :
1199 : 3315 : Node TheoryArrays::getSkolem(TNode ref)
1200 : : {
1201 : 3315 : Node skolem = SkolemCache::getExtIndexSkolem(nodeManager(), ref);
1202 : :
1203 [ + - ]: 3315 : Trace("pf::array") << "Pregistering a Skolem" << std::endl;
1204 : 3315 : preRegisterTermInternal(skolem);
1205 [ + - ]: 3315 : Trace("pf::array") << "Pregistering a Skolem DONE" << std::endl;
1206 : :
1207 [ + - ]: 3315 : Trace("pf::array") << "getSkolem DONE" << std::endl;
1208 : 3315 : return skolem;
1209 : : }
1210 : :
1211 : 126790 : void TheoryArrays::postCheck(Effort level)
1212 : : {
1213 : 126790 : bool eagerLemmas = options().arrays.arraysEagerLemmas;
1214 : 126790 : bool weakEquiv = options().arrays.arraysWeakEquivalence;
1215 : :
1216 [ + + ][ + + ]: 126790 : if ((eagerLemmas || fullEffort(level)) && !d_state.isInConflict()
1217 [ + + ][ - + ]: 253580 : && weakEquiv)
[ - + ]
1218 : : {
1219 : : // Replay all array merges to update weak equivalence data structures
1220 : 0 : context::CDList<Node>::iterator it = d_arrayMerges.begin(),
1221 : 0 : iend = d_arrayMerges.end();
1222 : 0 : TNode a, b, eq;
1223 [ - - ]: 0 : for (; it != iend; ++it) {
1224 : 0 : eq = *it;
1225 : 0 : a = eq[0];
1226 : 0 : b = eq[1];
1227 : 0 : weakEquivMakeRep(b);
1228 [ - - ]: 0 : if (weakEquivGetRep(a) == b) {
1229 : 0 : weakEquivAddSecondary(TNode(), a, b, eq);
1230 : : }
1231 : : else {
1232 : 0 : d_infoMap.setWeakEquivPointer(b, a);
1233 : 0 : d_infoMap.setWeakEquivIndex(b, TNode());
1234 : : }
1235 : : #ifdef CVC5_ASSERTIONS
1236 : 0 : checkWeakEquiv(false);
1237 : : #endif
1238 : : }
1239 : : #ifdef CVC5_ASSERTIONS
1240 : 0 : checkWeakEquiv(true);
1241 : : #endif
1242 : :
1243 : 0 : d_readTableContext->push();
1244 : 0 : TNode mayRep, iRep;
1245 : 0 : CTNodeList* bucketList = NULL;
1246 : 0 : CTNodeList::const_iterator i = d_reads.begin(), readsEnd = d_reads.end();
1247 [ - - ]: 0 : for (; i != readsEnd; ++i) {
1248 : 0 : const TNode& r = *i;
1249 : :
1250 [ - - ]: 0 : Trace("arrays::weak") << "TheoryArrays::check(): checking read " << r << std::endl;
1251 : :
1252 : : // Find the bucket for this read.
1253 : 0 : mayRep = d_mayEqualEqualityEngine.getRepresentative(r[0]);
1254 : 0 : iRep = d_equalityEngine->getRepresentative(r[1]);
1255 : 0 : std::pair<TNode, TNode> key(mayRep, iRep);
1256 : 0 : ReadBucketMap::iterator rbm_it = d_readBucketTable.find(key);
1257 [ - - ]: 0 : if (rbm_it == d_readBucketTable.end())
1258 : : {
1259 : 0 : bucketList = new(true) CTNodeList(d_readTableContext);
1260 : 0 : d_readBucketAllocations.push_back(bucketList);
1261 : 0 : d_readBucketTable[key] = bucketList;
1262 : : }
1263 : : else {
1264 : 0 : bucketList = rbm_it->second;
1265 : : }
1266 : 0 : CTNodeList::const_iterator ctnl_it = bucketList->begin(),
1267 : 0 : ctnl_iend = bucketList->end();
1268 [ - - ]: 0 : for (; ctnl_it != ctnl_iend; ++ctnl_it)
1269 : : {
1270 : 0 : const TNode& r2 = *ctnl_it;
1271 : 0 : Assert(r2.getKind() == Kind::SELECT);
1272 : 0 : Assert(mayRep == d_mayEqualEqualityEngine.getRepresentative(r2[0]));
1273 : 0 : Assert(iRep == d_equalityEngine->getRepresentative(r2[1]));
1274 [ - - ]: 0 : if (d_equalityEngine->areEqual(r, r2))
1275 : : {
1276 : 0 : continue;
1277 : : }
1278 [ - - ]: 0 : if (weakEquivGetRepIndex(r[0], r[1]) == weakEquivGetRepIndex(r2[0], r[1])) {
1279 : : // add lemma: r[1] = r2[1] /\ cond(r[0],r2[0]) => r = r2
1280 : 0 : vector<TNode> conjunctions;
1281 : 0 : Assert(d_equalityEngine->areEqual(r, rewrite(r)));
1282 : 0 : Assert(d_equalityEngine->areEqual(r2, rewrite(r2)));
1283 : 0 : Node lemma = rewrite(r).eqNode(rewrite(r2)).negate();
1284 : 0 : d_permRef.push_back(lemma);
1285 : 0 : conjunctions.push_back(lemma);
1286 [ - - ]: 0 : if (r[1] != r2[1]) {
1287 : 0 : d_equalityEngine->explainEquality(r[1], r2[1], true, conjunctions);
1288 : : }
1289 : : // TODO: get smaller lemmas by eliminating shared parts of path
1290 : 0 : weakEquivBuildCond(r[0], r[1], conjunctions);
1291 : 0 : weakEquivBuildCond(r2[0], r[1], conjunctions);
1292 : 0 : lemma = mkAnd(conjunctions, true);
1293 : : // LSH FIXME: which kind of arrays lemma is this
1294 [ - - ]: 0 : Trace("arrays-lem")
1295 : 0 : << "Arrays::addExtLemma (weak-eq) " << lemma << "\n";
1296 : 0 : d_out->lemma(lemma, InferenceId::NONE, LemmaProperty::SEND_ATOMS);
1297 : 0 : d_readTableContext->pop();
1298 : 0 : Trace("arrays") << spaces(context()->getLevel())
1299 : 0 : << "Arrays::check(): done" << endl;
1300 : 0 : return;
1301 : : }
1302 : : }
1303 : 0 : bucketList->push_back(r);
1304 : : }
1305 : 0 : d_readTableContext->pop();
1306 : : }
1307 : :
1308 [ + + ][ + + ]: 126764 : if (!eagerLemmas && fullEffort(level) && !d_state.isInConflict()
1309 [ + + ][ + - ]: 253554 : && !weakEquiv)
[ + + ]
1310 : : {
1311 : : // generate the lemmas on the worklist
1312 [ + - ]: 69008 : Trace("arrays-lem")<< "Arrays::discharging lemmas. Number of queued lemmas: " << d_RowQueue.size() << "\n";
1313 [ + + ][ + - ]: 69353 : while (d_RowQueue.size() > 0 && !d_state.isInConflict())
[ + + ]
1314 : : {
1315 [ + + ]: 1658 : if (dischargeLemmas()) {
1316 : 1313 : break;
1317 : : }
1318 : : }
1319 : : }
1320 : :
1321 [ + - ][ - + ]: 253580 : Trace("arrays") << spaces(context()->getLevel()) << "Arrays::check(): done"
[ - - ]
1322 : 126790 : << endl;
1323 : : }
1324 : :
1325 : 175975 : bool TheoryArrays::preNotifyFact(
1326 : : TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
1327 : : {
1328 [ + + ][ + + ]: 175975 : if (!isInternal && !isPrereg)
1329 : : {
1330 [ + + ]: 117421 : if (atom.getKind() == Kind::EQUAL)
1331 : : {
1332 [ + + ]: 117297 : if (!d_equalityEngine->hasTerm(atom[0]))
1333 : : {
1334 [ - + ][ - + ]: 2307 : Assert(atom[0].isConst());
[ - - ]
1335 : 2307 : d_equalityEngine->addTerm(atom[0]);
1336 : : }
1337 [ + + ]: 117297 : if (!d_equalityEngine->hasTerm(atom[1]))
1338 : : {
1339 [ - + ][ - + ]: 460 : Assert(atom[1].isConst());
[ - - ]
1340 : 460 : d_equalityEngine->addTerm(atom[1]);
1341 : : }
1342 : : }
1343 : : }
1344 : 175975 : return false;
1345 : : }
1346 : :
1347 : 175972 : void TheoryArrays::notifyFact(TNode atom, bool pol, TNode fact, bool isInternal)
1348 : : {
1349 : : // if a disequality
1350 [ + + ][ + + ]: 175972 : if (atom.getKind() == Kind::EQUAL && !pol && !isInternal)
[ + + ][ + + ]
1351 : : {
1352 : : // Notice that this should be an external assertion, since we do not
1353 : : // internally infer disequalities.
1354 : : // Apply ArrDiseq Rule if diseq is between arrays
1355 : 43055 : if (fact[0][0].getType().isArray() && !d_state.isInConflict())
1356 : : {
1357 : 3315 : NodeManager* nm = nodeManager();
1358 : :
1359 : 6630 : TNode k;
1360 : : // k is the skolem for this disequality.
1361 [ + - ]: 6630 : Trace("pf::array") << "Check: Kind::NOT: array theory making a skolem"
1362 : 3315 : << std::endl;
1363 : :
1364 : : // If not in replay mode, generate a fresh skolem variable
1365 : 3315 : k = getSkolem(fact);
1366 : :
1367 : 9945 : Node ak = nm->mkNode(Kind::SELECT, fact[0][0], k);
1368 : 9945 : Node bk = nm->mkNode(Kind::SELECT, fact[0][1], k);
1369 : 6630 : Node eq = ak.eqNode(bk);
1370 : 9945 : Node lemma = fact[0].orNode(eq.notNode());
1371 : :
1372 [ + + ][ + + ]: 6630 : if (options().arrays.arraysPropagate > 0 && d_equalityEngine->hasTerm(ak)
[ - - ]
1373 [ + - ][ + - ]: 6630 : && d_equalityEngine->hasTerm(bk))
[ + + ][ + - ]
[ - - ]
1374 : : {
1375 : : // Propagate witness disequality - might produce a conflict
1376 [ + - ]: 5158 : Trace("pf::array") << "Asserting to the equality engine:" << std::endl
1377 : 0 : << "\teq = " << eq << std::endl
1378 : 2579 : << "\treason = " << fact << std::endl;
1379 : 2579 : d_im.assertInference(
1380 : : eq, false, InferenceId::ARRAYS_EXT, fact, ProofRule::ARRAYS_EXT);
1381 : 2579 : ++d_numProp;
1382 : : }
1383 : :
1384 : : // If this is the solution pass, generate the lemma. Otherwise, don't
1385 : : // generate it - as this is the lemma that we're reproving...
1386 [ + - ]: 3315 : Trace("arrays-lem") << "Arrays::addExtLemma " << lemma << "\n";
1387 : 6630 : d_im.arrayLemma(
1388 : 6630 : eq.notNode(), InferenceId::ARRAYS_EXT, fact, ProofRule::ARRAYS_EXT);
1389 : 3315 : ++d_numExt;
1390 : : }
1391 : : else
1392 : : {
1393 [ + - ]: 79480 : Trace("pf::array") << "Check: Kind::NOT: array theory NOT making a skolem"
1394 : 39740 : << std::endl;
1395 : 39740 : d_modelConstraints.push_back(fact);
1396 : : }
1397 : : }
1398 : 175972 : }
1399 : :
1400 : 0 : Node TheoryArrays::mkAnd(std::vector<TNode>& conjunctions, bool invert, unsigned startIndex)
1401 : : {
1402 [ - - ]: 0 : if (conjunctions.empty())
1403 : : {
1404 [ - - ]: 0 : return invert ? d_false : d_true;
1405 : : }
1406 : :
1407 : 0 : std::set<TNode> all;
1408 : :
1409 : 0 : unsigned i = startIndex;
1410 : 0 : TNode t;
1411 [ - - ]: 0 : for (; i < conjunctions.size(); ++i) {
1412 : 0 : t = conjunctions[i];
1413 [ - - ]: 0 : if (t == d_true) {
1414 : 0 : continue;
1415 : : }
1416 [ - - ]: 0 : else if (t.getKind() == Kind::AND)
1417 : : {
1418 [ - - ]: 0 : for(TNode::iterator child_it = t.begin(); child_it != t.end(); ++child_it) {
1419 [ - - ]: 0 : if (*child_it == d_true) {
1420 : 0 : continue;
1421 : : }
1422 : 0 : all.insert(*child_it);
1423 : : }
1424 : : }
1425 : : else {
1426 : 0 : all.insert(t);
1427 : : }
1428 : : }
1429 : :
1430 [ - - ]: 0 : if (all.size() == 0) {
1431 [ - - ]: 0 : return invert ? d_false : d_true;
1432 : : }
1433 [ - - ]: 0 : if (all.size() == 1) {
1434 : : // All the same, or just one
1435 [ - - ]: 0 : if (invert) {
1436 : 0 : return (*(all.begin())).negate();
1437 : : }
1438 : : else {
1439 : 0 : return *(all.begin());
1440 : : }
1441 : : }
1442 : :
1443 [ - - ]: 0 : NodeBuilder conjunction(nodeManager(), invert ? Kind::OR : Kind::AND);
1444 : 0 : std::set<TNode>::const_iterator it = all.begin();
1445 : 0 : std::set<TNode>::const_iterator it_end = all.end();
1446 [ - - ]: 0 : while (it != it_end) {
1447 [ - - ]: 0 : if (invert) {
1448 : 0 : conjunction << (*it).negate();
1449 : : }
1450 : : else {
1451 : 0 : conjunction << *it;
1452 : : }
1453 : 0 : ++ it;
1454 : : }
1455 : :
1456 : 0 : return conjunction;
1457 : : }
1458 : :
1459 : :
1460 : 3518 : void TheoryArrays::setNonLinear(TNode a)
1461 : : {
1462 [ - + ]: 3985 : if (options().arrays.arraysWeakEquivalence) return;
1463 [ + + ]: 3518 : if (d_infoMap.isNonLinear(a)) return;
1464 : :
1465 [ + - ][ - + ]: 6102 : Trace("arrays") << spaces(context()->getLevel()) << "Arrays::setNonLinear ("
[ - - ]
1466 : 3051 : << a << ")\n";
1467 : 3051 : d_infoMap.setNonLinear(a);
1468 : 3051 : ++d_numNonLinear;
1469 : :
1470 : 3051 : const CTNodeList* i_a = d_infoMap.getIndices(a);
1471 : 3051 : const CTNodeList* st_a = d_infoMap.getStores(a);
1472 : 3051 : const CTNodeList* inst_a = d_infoMap.getInStores(a);
1473 : :
1474 : 3051 : size_t it = 0;
1475 : :
1476 : : // Propagate non-linearity down chain of stores
1477 [ + + ]: 5271 : for( ; it < st_a->size(); ++it) {
1478 : 2220 : TNode store = (*st_a)[it];
1479 [ - + ][ - + ]: 2220 : Assert(store.getKind() == Kind::STORE);
[ - - ]
1480 : 2220 : setNonLinear(store[0]);
1481 : : }
1482 : :
1483 : : // Instantiate ROW lemmas that were ignored before
1484 : 3051 : size_t it2 = 0;
1485 : 6102 : RowLemmaType lem;
1486 [ + + ]: 20521 : for(; it2 < i_a->size(); ++it2) {
1487 : 34940 : TNode i = (*i_a)[it2];
1488 : 17470 : it = 0;
1489 [ + + ]: 33591 : for ( ; it < inst_a->size(); ++it) {
1490 : 32242 : TNode store = (*inst_a)[it];
1491 [ - + ][ - + ]: 16121 : Assert(store.getKind() == Kind::STORE);
[ - - ]
1492 : 32242 : TNode j = store[1];
1493 : 16121 : TNode c = store[0];
1494 : 16121 : lem = std::make_tuple(store, c, j, i);
1495 [ + - ][ - + ]: 32242 : Trace("arrays-lem") << spaces(context()->getLevel())
[ - - ]
1496 : 0 : << "Arrays::setNonLinear (" << store << ", " << c
1497 : 16121 : << ", " << j << ", " << i << ")\n";
1498 : 16121 : queueRowLemma(lem);
1499 : : }
1500 : : }
1501 : :
1502 : : }
1503 : :
1504 : 7721 : void TheoryArrays::mergeArrays(TNode a, TNode b)
1505 : : {
1506 : : // Note: a is the new representative
1507 : 15442 : Assert(a.getType().isArray() && b.getType().isArray());
1508 : :
1509 [ - + ]: 7721 : if (d_mergeInProgress) {
1510 : : // Nested call to mergeArrays, just push on the queue and return
1511 : 0 : d_mergeQueue.push(a.eqNode(b));
1512 : 0 : return;
1513 : : }
1514 : :
1515 : 7721 : d_mergeInProgress = true;
1516 : 7721 : bool optLinear = options().arrays.arraysOptimizeLinear;
1517 : 7721 : bool weakEquiv = options().arrays.arraysWeakEquivalence;
1518 : :
1519 : 7724 : Node n;
1520 : : while (true) {
1521 : : // Normally, a is its own representative, but it's possible for a to have
1522 : : // been merged with another array after it got queued up by the equality engine,
1523 : : // so we take its representative to be safe.
1524 : 7721 : a = d_equalityEngine->getRepresentative(a);
1525 [ - + ][ - + ]: 7721 : Assert(d_equalityEngine->getRepresentative(b) == a);
[ - - ]
1526 [ + - ][ - + ]: 15442 : Trace("arrays-merge") << spaces(context()->getLevel()) << "Arrays::merge: ("
[ - - ]
1527 : 7721 : << a << ", " << b << ")\n";
1528 : :
1529 [ + + ][ + - ]: 7721 : if (optLinear && !weakEquiv)
1530 : : {
1531 : 6071 : bool aNL = d_infoMap.isNonLinear(a);
1532 : 6071 : bool bNL = d_infoMap.isNonLinear(b);
1533 [ + + ]: 6071 : if (aNL) {
1534 [ + + ]: 426 : if (bNL) {
1535 : : // already both marked as non-linear - no need to do anything
1536 : : }
1537 : : else {
1538 : : // Set b to be non-linear
1539 : 370 : setNonLinear(b);
1540 : : }
1541 : : }
1542 : : else {
1543 [ + + ]: 5645 : if (bNL) {
1544 : : // Set a to be non-linear
1545 : 63 : setNonLinear(a);
1546 : : }
1547 : : else {
1548 : : // Check for new non-linear arrays
1549 : 5582 : const CTNodeList* astores = d_infoMap.getStores(a);
1550 : 5582 : const CTNodeList* bstores = d_infoMap.getStores(b);
1551 [ + - ][ + - ]: 11164 : Assert(astores->size() <= 1 && bstores->size() <= 1);
[ - + ][ - - ]
1552 [ + + ][ + + ]: 5582 : if (astores->size() > 0 && bstores->size() > 0) {
[ + + ]
1553 : 411 : setNonLinear(a);
1554 : 411 : setNonLinear(b);
1555 : : }
1556 : : }
1557 : : }
1558 : : }
1559 : :
1560 : 7724 : TNode constArrA = d_infoMap.getConstArr(a);
1561 : 7724 : TNode constArrB = d_infoMap.getConstArr(b);
1562 [ + + ]: 7721 : if (constArrA.isNull()) {
1563 [ - + ]: 7638 : if (!constArrB.isNull()) {
1564 : 0 : d_infoMap.setConstArr(a,constArrB);
1565 : : }
1566 : : }
1567 [ - + ]: 83 : else if (!constArrB.isNull()) {
1568 [ - - ]: 0 : if (constArrA != constArrB) {
1569 : 0 : conflict(constArrA,constArrB);
1570 : : }
1571 : : }
1572 : :
1573 : 7724 : TNode mayRepA = d_mayEqualEqualityEngine.getRepresentative(a);
1574 : 7724 : TNode mayRepB = d_mayEqualEqualityEngine.getRepresentative(b);
1575 : :
1576 : : // If a and b have different default values associated with their mayequal equivalence classes,
1577 : : // things get complicated. Similarly, if two mayequal equivalence classes have different
1578 : : // constant representatives, it's not clear what to do. - disallow these cases for now. -Clark
1579 : 7721 : DefValMap::iterator it = d_defValues.find(mayRepA);
1580 : 7721 : DefValMap::iterator it2 = d_defValues.find(mayRepB);
1581 : 7724 : TNode defValue;
1582 : :
1583 [ + + ]: 7721 : if (it != d_defValues.end()) {
1584 : 88 : defValue = (*it).second;
1585 [ + + ][ + + ]: 174 : if ((it2 != d_defValues.end() && (defValue != (*it2).second)) ||
[ + + ]
1586 [ + - ][ + + ]: 86 : (mayRepA.isConst() && mayRepB.isConst() && mayRepA != mayRepB)) {
[ + - ]
1587 : 3 : throw LogicException("Array theory solver does not yet support write-chains connecting two different constant arrays");
1588 : : }
1589 : : }
1590 [ - + ]: 7633 : else if (it2 != d_defValues.end()) {
1591 : 0 : defValue = (*it2).second;
1592 : : }
1593 : 7718 : d_mayEqualEqualityEngine.assertEquality(a.eqNode(b), true, d_true);
1594 [ - + ][ - + ]: 7718 : Assert(d_mayEqualEqualityEngine.consistent());
[ - - ]
1595 [ + + ]: 7718 : if (!defValue.isNull()) {
1596 : 85 : mayRepA = d_mayEqualEqualityEngine.getRepresentative(a);
1597 : 85 : d_defValues[mayRepA] = defValue;
1598 : : }
1599 : :
1600 : 7718 : checkRowLemmas(a,b);
1601 : 7718 : checkRowLemmas(b,a);
1602 : :
1603 : : // merge info adds the list of the 2nd argument to the first
1604 : 7718 : d_infoMap.mergeInfo(a, b);
1605 : :
1606 [ - + ]: 7718 : if (weakEquiv)
1607 : : {
1608 : 0 : d_arrayMerges.push_back(a.eqNode(b));
1609 : : }
1610 : :
1611 : : // If no more to do, break
1612 [ + - ][ + - ]: 7718 : if (d_state.isInConflict() || d_mergeQueue.empty())
[ + - ]
1613 : : {
1614 : 7718 : break;
1615 : : }
1616 : :
1617 : : // Otherwise, prepare for next iteration
1618 : 0 : n = d_mergeQueue.front();
1619 : 0 : a = n[0];
1620 : 0 : b = n[1];
1621 : 0 : d_mergeQueue.pop();
1622 : 0 : }
1623 : 7718 : d_mergeInProgress = false;
1624 : : }
1625 : :
1626 : 2124 : void TheoryArrays::checkStore(TNode a)
1627 : : {
1628 [ - + ]: 2124 : if (options().arrays.arraysWeakEquivalence) return;
1629 : :
1630 [ + - ]: 2124 : Trace("arrays-cri")<<"Arrays::checkStore "<<a<<"\n";
1631 : :
1632 [ - + ]: 2124 : if(TraceIsOn("arrays-cri")) {
1633 : 0 : d_infoMap.getInfo(a)->print();
1634 : : }
1635 [ - + ][ - + ]: 2124 : Assert(a.getType().isArray());
[ - - ]
1636 [ - + ][ - + ]: 2124 : Assert(a.getKind() == Kind::STORE);
[ - - ]
1637 : 4248 : TNode b = a[0];
1638 : 4248 : TNode i = a[1];
1639 : :
1640 : 4248 : TNode brep = d_equalityEngine->getRepresentative(b);
1641 : :
1642 [ + + ][ + + ]: 2124 : if (!options().arrays.arraysOptimizeLinear || d_infoMap.isNonLinear(brep))
[ + + ][ + + ]
[ - - ]
1643 : : {
1644 : 460 : const CTNodeList* js = d_infoMap.getIndices(brep);
1645 : 460 : size_t it = 0;
1646 : 920 : RowLemmaType lem;
1647 [ + + ]: 792 : for(; it < js->size(); ++it) {
1648 : 332 : TNode j = (*js)[it];
1649 [ + + ]: 332 : if (i == j) continue;
1650 : 291 : lem = std::make_tuple(a, b, i, j);
1651 [ + - ][ - + ]: 582 : Trace("arrays-lem") << spaces(context()->getLevel())
[ - - ]
1652 : 0 : << "Arrays::checkStore (" << a << ", " << b << ", "
1653 : 291 : << i << ", " << j << ")\n";
1654 : 291 : queueRowLemma(lem);
1655 : : }
1656 : : }
1657 : : }
1658 : :
1659 : 35940 : void TheoryArrays::checkRowForIndex(TNode i, TNode a)
1660 : : {
1661 [ - + ]: 35940 : if (options().arrays.arraysWeakEquivalence) return;
1662 : :
1663 [ + - ]: 35940 : Trace("arrays-cri")<<"Arrays::checkRowForIndex "<<a<<"\n";
1664 [ + - ]: 35940 : Trace("arrays-cri")<<" index "<<i<<"\n";
1665 : :
1666 [ - + ]: 35940 : if(TraceIsOn("arrays-cri")) {
1667 : 0 : d_infoMap.getInfo(a)->print();
1668 : : }
1669 [ - + ][ - + ]: 35940 : Assert(a.getType().isArray());
[ - - ]
1670 [ - + ][ - + ]: 35940 : Assert(d_equalityEngine->getRepresentative(a) == a);
[ - - ]
1671 : :
1672 : 71880 : TNode constArr = d_infoMap.getConstArr(a);
1673 [ + + ]: 35940 : if (!constArr.isNull()) {
1674 : 1408 : ArrayStoreAll storeAll = constArr.getConst<ArrayStoreAll>();
1675 : 1408 : Node defValue = storeAll.getValue();
1676 : 1408 : Node selConst = nodeManager()->mkNode(Kind::SELECT, constArr, i);
1677 [ + + ]: 704 : if (!d_equalityEngine->hasTerm(selConst))
1678 : : {
1679 : 20 : preRegisterTermInternal(selConst);
1680 : : }
1681 : : // not currently supported in proofs, use TRUST
1682 : 704 : d_im.assertInference(selConst.eqNode(defValue),
1683 : : true,
1684 : : InferenceId::ARRAYS_CONST_ARRAY_DEFAULT,
1685 : 704 : d_true,
1686 : : ProofRule::TRUST);
1687 : : }
1688 : :
1689 : 35940 : const CTNodeList* stores = d_infoMap.getStores(a);
1690 : 35940 : const CTNodeList* instores = d_infoMap.getInStores(a);
1691 : 35940 : size_t it = 0;
1692 : 71880 : RowLemmaType lem;
1693 : :
1694 [ + + ]: 58198 : for(; it < stores->size(); ++it) {
1695 : 22258 : TNode store = (*stores)[it];
1696 [ - + ][ - + ]: 22258 : Assert(store.getKind() == Kind::STORE);
[ - - ]
1697 : 22258 : TNode j = store[1];
1698 [ + + ]: 22258 : if (i == j) continue;
1699 : 21888 : lem = std::make_tuple(store, store[0], j, i);
1700 [ + - ][ - - ]: 43776 : Trace("arrays-lem") << spaces(context()->getLevel())
1701 : 0 : << "Arrays::checkRowForIndex (" << store << ", "
1702 [ - + ][ - + ]: 21888 : << store[0] << ", " << j << ", " << i << ")\n";
[ - - ]
1703 : 21888 : queueRowLemma(lem);
1704 : : }
1705 : :
1706 [ + + ][ + + ]: 35940 : if (!options().arrays.arraysOptimizeLinear || d_infoMap.isNonLinear(a))
[ + + ][ + + ]
[ - - ]
1707 : : {
1708 : 10206 : it = 0;
1709 [ + + ]: 18222 : for(; it < instores->size(); ++it) {
1710 : 8016 : TNode instore = (*instores)[it];
1711 [ - + ][ - + ]: 8016 : Assert(instore.getKind() == Kind::STORE);
[ - - ]
1712 : 8016 : TNode j = instore[1];
1713 [ + + ]: 8016 : if (i == j) continue;
1714 : 7348 : lem = std::make_tuple(instore, instore[0], j, i);
1715 [ + - ][ - - ]: 14696 : Trace("arrays-lem") << spaces(context()->getLevel())
1716 : 0 : << "Arrays::checkRowForIndex (" << instore << ", "
1717 [ - + ][ - + ]: 7348 : << instore[0] << ", " << j << ", " << i << ")\n";
[ - - ]
1718 : 7348 : queueRowLemma(lem);
1719 : : }
1720 : : }
1721 : : }
1722 : :
1723 : :
1724 : : // a just became equal to b
1725 : : // look for new ROW lemmas
1726 : 15436 : void TheoryArrays::checkRowLemmas(TNode a, TNode b)
1727 : : {
1728 [ - + ]: 15436 : if (options().arrays.arraysWeakEquivalence) return;
1729 : :
1730 [ + - ]: 15436 : Trace("arrays-crl")<<"Arrays::checkLemmas begin \n"<<a<<"\n";
1731 [ - + ]: 15436 : if(TraceIsOn("arrays-crl"))
1732 : 0 : d_infoMap.getInfo(a)->print();
1733 [ + - ]: 15436 : Trace("arrays-crl")<<" ------------ and "<<b<<"\n";
1734 [ - + ]: 15436 : if(TraceIsOn("arrays-crl"))
1735 : 0 : d_infoMap.getInfo(b)->print();
1736 : :
1737 : 15436 : const CTNodeList* i_a = d_infoMap.getIndices(a);
1738 : 15436 : size_t it = 0;
1739 : 30872 : TNode constArr = d_infoMap.getConstArr(b);
1740 [ + + ]: 15436 : if (!constArr.isNull()) {
1741 [ + + ]: 739 : for( ; it < i_a->size(); ++it) {
1742 : 1312 : TNode i = (*i_a)[it];
1743 : 1968 : Node selConst = nodeManager()->mkNode(Kind::SELECT, constArr, i);
1744 [ + - ]: 656 : if (!d_equalityEngine->hasTerm(selConst))
1745 : : {
1746 : 656 : preRegisterTermInternal(selConst);
1747 : : }
1748 : : }
1749 : : }
1750 : :
1751 : 15436 : const CTNodeList* st_b = d_infoMap.getStores(b);
1752 : 15436 : const CTNodeList* inst_b = d_infoMap.getInStores(b);
1753 : : size_t its;
1754 : :
1755 : 15436 : RowLemmaType lem;
1756 : :
1757 [ + + ]: 82070 : for(it = 0 ; it < i_a->size(); ++it) {
1758 : 133268 : TNode i = (*i_a)[it];
1759 : 66634 : its = 0;
1760 [ + + ]: 102975 : for ( ; its < st_b->size(); ++its) {
1761 : 72682 : TNode store = (*st_b)[its];
1762 [ - + ][ - + ]: 36341 : Assert(store.getKind() == Kind::STORE);
[ - - ]
1763 : 72682 : TNode j = store[1];
1764 : 36341 : TNode c = store[0];
1765 : 36341 : lem = std::make_tuple(store, c, j, i);
1766 [ + - ][ - + ]: 72682 : Trace("arrays-lem") << spaces(context()->getLevel())
[ - - ]
1767 : 0 : << "Arrays::checkRowLemmas (" << store << ", " << c
1768 : 36341 : << ", " << j << ", " << i << ")\n";
1769 : 36341 : queueRowLemma(lem);
1770 : : }
1771 : : }
1772 : :
1773 [ + + ][ + + ]: 15436 : if (!options().arrays.arraysOptimizeLinear || d_infoMap.isNonLinear(b))
[ + + ][ + + ]
[ - - ]
1774 : : {
1775 [ + + ]: 37815 : for(it = 0 ; it < i_a->size(); ++it ) {
1776 : 65442 : TNode i = (*i_a)[it];
1777 : 32721 : its = 0;
1778 [ + + ]: 57308 : for ( ; its < inst_b->size(); ++its) {
1779 : 49174 : TNode store = (*inst_b)[its];
1780 [ - + ][ - + ]: 24587 : Assert(store.getKind() == Kind::STORE);
[ - - ]
1781 : 49174 : TNode j = store[1];
1782 : 24587 : TNode c = store[0];
1783 : 24587 : lem = std::make_tuple(store, c, j, i);
1784 [ + - ]: 49174 : Trace("arrays-lem")
1785 [ - + ][ - - ]: 24587 : << spaces(context()->getLevel()) << "Arrays::checkRowLemmas ("
1786 : 24587 : << store << ", " << c << ", " << j << ", " << i << ")\n";
1787 : 24587 : queueRowLemma(lem);
1788 : : }
1789 : : }
1790 : : }
1791 [ + - ]: 15436 : Trace("arrays-crl")<<"Arrays::checkLemmas done.\n";
1792 : : }
1793 : :
1794 : 32706 : void TheoryArrays::propagateRowLemma(RowLemmaType lem)
1795 : : {
1796 [ + - ]: 65412 : Trace("pf::array") << "TheoryArrays: RowLemma Propagate called. "
1797 : 0 : "arraysPropagate = "
1798 : 32706 : << options().arrays.arraysPropagate << std::endl;
1799 : :
1800 : 32706 : TNode a, b, i, j;
1801 : 32706 : std::tie(a, b, i, j) = lem;
1802 : :
1803 : 65412 : Assert(a.getType().isArray() && b.getType().isArray());
1804 : 32706 : if (d_equalityEngine->areEqual(a, b) || d_equalityEngine->areEqual(i, j))
1805 : : {
1806 : 0 : return;
1807 : : }
1808 : :
1809 : 32706 : NodeManager* nm = nodeManager();
1810 : 65412 : Node aj = nm->mkNode(Kind::SELECT, a, j);
1811 : 65412 : Node bj = nm->mkNode(Kind::SELECT, b, j);
1812 : :
1813 : : // Try to avoid introducing new read terms: track whether these already exist
1814 : 32706 : bool ajExists = d_equalityEngine->hasTerm(aj);
1815 : 32706 : bool bjExists = d_equalityEngine->hasTerm(bj);
1816 [ + + ][ + + ]: 32706 : bool bothExist = ajExists && bjExists;
1817 : :
1818 : : // If propagating, check propagations
1819 : 32706 : int64_t prop = options().arrays.arraysPropagate;
1820 [ + - ]: 32706 : if (prop > 0) {
1821 : 32706 : if (d_equalityEngine->areDisequal(i, j, true) && (bothExist || prop > 1))
1822 : : {
1823 [ + - ][ - + ]: 33970 : Trace("arrays-lem") << spaces(context()->getLevel())
[ - - ]
1824 : 0 : << "Arrays::queueRowLemma: propagating aj = bj ("
1825 : 16985 : << aj << ", " << bj << ")\n";
1826 : 33970 : Node aj_eq_bj = aj.eqNode(bj);
1827 : : Node reason =
1828 [ + + ][ + + ]: 20799 : (i.isConst() && j.isConst()) ? d_true : i.eqNode(j).notNode();
[ + + ][ - - ]
1829 : 16985 : d_permRef.push_back(reason);
1830 [ + + ]: 16985 : if (!ajExists) {
1831 : 5251 : preRegisterTermInternal(aj);
1832 : : }
1833 [ + + ]: 16985 : if (!bjExists) {
1834 : 9489 : preRegisterTermInternal(bj);
1835 : : }
1836 : 16985 : d_im.assertInference(aj_eq_bj,
1837 : : true,
1838 : : InferenceId::ARRAYS_READ_OVER_WRITE,
1839 : : reason,
1840 : : ProofRule::ARRAYS_READ_OVER_WRITE);
1841 : 16985 : ++d_numProp;
1842 : 16985 : return;
1843 : : }
1844 : 15721 : if (bothExist && d_equalityEngine->areDisequal(aj, bj, true))
1845 : : {
1846 [ + - ][ - + ]: 62 : Trace("arrays-lem") << spaces(context()->getLevel())
[ - - ]
1847 : 0 : << "Arrays::queueRowLemma: propagating i = j (" << i
1848 : 31 : << ", " << j << ")\n";
1849 : : Node reason =
1850 [ - + ][ - - ]: 62 : (aj.isConst() && bj.isConst()) ? d_true : aj.eqNode(bj).notNode();
[ + - ][ - - ]
1851 : 31 : Node j_eq_i = j.eqNode(i);
1852 : 31 : d_im.assertInference(j_eq_i,
1853 : : true,
1854 : : InferenceId::ARRAYS_READ_OVER_WRITE_CONTRA,
1855 : : reason,
1856 : : ProofRule::ARRAYS_READ_OVER_WRITE_CONTRA);
1857 : 31 : ++d_numProp;
1858 : 31 : return;
1859 : : }
1860 : : }
1861 : : }
1862 : :
1863 : 106576 : void TheoryArrays::queueRowLemma(RowLemmaType lem)
1864 : : {
1865 [ + - ]: 106576 : Trace("pf::array") << "Array solver: queue row lemma called" << std::endl;
1866 : :
1867 [ + + ][ + + ]: 106576 : if (d_state.isInConflict() || d_RowAlreadyAdded.contains(lem))
[ + + ]
1868 : : {
1869 : 79587 : return;
1870 : : }
1871 : 49105 : TNode a, b, i, j;
1872 : 49105 : std::tie(a, b, i, j) = lem;
1873 : :
1874 : 98210 : Assert(a.getType().isArray() && b.getType().isArray());
1875 : 49105 : if (d_equalityEngine->areEqual(a, b) || d_equalityEngine->areEqual(i, j))
1876 : : {
1877 : 19748 : return;
1878 : : }
1879 : :
1880 : 29357 : NodeManager* nm = nodeManager();
1881 : 58714 : Node aj = nm->mkNode(Kind::SELECT, a, j);
1882 : 58714 : Node bj = nm->mkNode(Kind::SELECT, b, j);
1883 : :
1884 : : // Try to avoid introducing new read terms: track whether these already exist
1885 : 29357 : bool ajExists = d_equalityEngine->hasTerm(aj);
1886 : 29357 : bool bjExists = d_equalityEngine->hasTerm(bj);
1887 [ + + ][ + + ]: 29357 : bool bothExist = ajExists && bjExists;
1888 : :
1889 : : // If propagating, check propagations
1890 : 29357 : int64_t prop = options().arrays.arraysPropagate;
1891 : :
1892 [ + - ]: 29357 : if (prop > 0) {
1893 : 29357 : propagateRowLemma(lem);
1894 : : }
1895 : :
1896 : : // Prefer equality between indexes so as not to introduce new read terms
1897 [ + + ]: 22152 : if (options().arrays.arraysEagerIndexSplitting && !bothExist
1898 : 51509 : && !d_equalityEngine->areDisequal(i, j, false))
1899 : : {
1900 : 16150 : Node i_eq_j;
1901 : 8075 : i_eq_j = d_valuation.ensureLiteral(i.eqNode(j)); // TODO: think about this
1902 : : #if 0
1903 : : i_eq_j = i.eqNode(j);
1904 : : #endif
1905 : 8075 : getOutputChannel().preferPhase(i_eq_j, true);
1906 : 8075 : d_decisionRequests.push(i_eq_j);
1907 : : }
1908 : :
1909 : : // TODO: maybe add triggers here
1910 : :
1911 [ + + ][ + + ]: 29357 : if (options().arrays.arraysEagerLemmas || bothExist)
[ + + ]
1912 : : {
1913 : : // Make sure that any terms introduced by rewriting are appropriately stored in the equality database
1914 : 5064 : Node aj2 = rewrite(aj);
1915 [ + + ]: 5064 : if (aj != aj2) {
1916 [ - + ]: 2368 : if (!ajExists) {
1917 : 0 : preRegisterTermInternal(aj);
1918 : : }
1919 [ - + ]: 2368 : if (!d_equalityEngine->hasTerm(aj2))
1920 : : {
1921 : 0 : preRegisterTermInternal(aj2);
1922 : : }
1923 : 2368 : d_im.assertInference(aj.eqNode(aj2),
1924 : : true,
1925 : : InferenceId::ARRAYS_EQ_TAUTOLOGY,
1926 : 2368 : d_true,
1927 : : ProofRule::MACRO_SR_PRED_INTRO);
1928 : : }
1929 : 5064 : Node bj2 = rewrite(bj);
1930 [ + + ]: 5064 : if (bj != bj2) {
1931 [ - + ]: 1246 : if (!bjExists) {
1932 : 0 : preRegisterTermInternal(bj);
1933 : : }
1934 [ - + ]: 1246 : if (!d_equalityEngine->hasTerm(bj2))
1935 : : {
1936 : 0 : preRegisterTermInternal(bj2);
1937 : : }
1938 : 1246 : d_im.assertInference(bj.eqNode(bj2),
1939 : : true,
1940 : : InferenceId::ARRAYS_EQ_TAUTOLOGY,
1941 : 1246 : d_true,
1942 : : ProofRule::MACRO_SR_PRED_INTRO);
1943 : : }
1944 [ + + ]: 5064 : if (aj2 == bj2) {
1945 : 2368 : return;
1946 : : }
1947 : :
1948 : : // construct lemma
1949 : 2696 : Node eq1 = aj2.eqNode(bj2);
1950 : 2696 : Node eq1_r = rewrite(eq1);
1951 [ - + ]: 2696 : if (eq1_r == d_true) {
1952 [ - - ]: 0 : if (!d_equalityEngine->hasTerm(aj2))
1953 : : {
1954 : 0 : preRegisterTermInternal(aj2);
1955 : : }
1956 [ - - ]: 0 : if (!d_equalityEngine->hasTerm(bj2))
1957 : : {
1958 : 0 : preRegisterTermInternal(bj2);
1959 : : }
1960 : 0 : d_im.assertInference(eq1,
1961 : : true,
1962 : : InferenceId::ARRAYS_EQ_TAUTOLOGY,
1963 : 0 : d_true,
1964 : : ProofRule::MACRO_SR_PRED_INTRO);
1965 : 0 : return;
1966 : : }
1967 : :
1968 : 2696 : Node eq2 = i.eqNode(j);
1969 : 2696 : Node eq2_r = rewrite(eq2);
1970 [ - + ]: 2696 : if (eq2_r == d_true) {
1971 : 0 : d_im.assertInference(eq2,
1972 : : true,
1973 : : InferenceId::ARRAYS_EQ_TAUTOLOGY,
1974 : 0 : d_true,
1975 : : ProofRule::MACRO_SR_PRED_INTRO);
1976 : 0 : return;
1977 : : }
1978 : :
1979 : 8088 : Node lemma = nm->mkNode(Kind::OR, eq2_r, eq1_r);
1980 : :
1981 [ + - ]: 2696 : Trace("arrays-lem") << "Arrays::addRowLemma (1) adding " << lemma << "\n";
1982 : 2696 : d_RowAlreadyAdded.insert(lem);
1983 : : // use non-rewritten nodes
1984 : 2696 : d_im.arrayLemma(aj.eqNode(bj),
1985 : : InferenceId::ARRAYS_READ_OVER_WRITE,
1986 : 5392 : eq2.notNode(),
1987 : : ProofRule::ARRAYS_READ_OVER_WRITE);
1988 : 2696 : ++d_numRow;
1989 : : }
1990 : : else {
1991 : 24293 : d_RowQueue.push(lem);
1992 : : }
1993 : : }
1994 : :
1995 : 12044800 : Node TheoryArrays::getNextDecisionRequest()
1996 : : {
1997 [ + + ]: 12044800 : if(! d_decisionRequests.empty()) {
1998 : 91640 : Node n = d_decisionRequests.front();
1999 : 45820 : d_decisionRequests.pop();
2000 : 45820 : return n;
2001 : : }
2002 : 11999000 : return Node::null();
2003 : : }
2004 : :
2005 : :
2006 : 1658 : bool TheoryArrays::dischargeLemmas()
2007 : : {
2008 : 1658 : bool reduceSharing = options().arrays.arraysReduceSharing;
2009 : 1658 : bool lemmasAdded = false;
2010 : :
2011 [ + + ]: 29327 : for (size_t count = 0, sz = d_RowQueue.size(); count < sz; ++count)
2012 : : {
2013 : 28384 : RowLemmaType l = d_RowQueue.front();
2014 : 28384 : d_RowQueue.pop();
2015 [ + + ]: 28384 : if (d_RowAlreadyAdded.contains(l)) {
2016 : 19788 : continue;
2017 : : }
2018 : :
2019 : 8596 : TNode a, b, i, j;
2020 : 8596 : std::tie(a, b, i, j) = l;
2021 : 17192 : Assert(a.getType().isArray() && b.getType().isArray());
2022 : :
2023 : 8596 : NodeManager* nm = nodeManager();
2024 : 17192 : Node aj = nm->mkNode(Kind::SELECT, a, j);
2025 : 17192 : Node bj = nm->mkNode(Kind::SELECT, b, j);
2026 : 8596 : bool ajExists = d_equalityEngine->hasTerm(aj);
2027 : 8596 : bool bjExists = d_equalityEngine->hasTerm(bj);
2028 : :
2029 : : // Check for redundant lemma
2030 : : // TODO: more checks possible (i.e. check d_RowAlreadyAdded in context)
2031 : 17192 : if (!d_equalityEngine->hasTerm(i) || !d_equalityEngine->hasTerm(j)
2032 : 17192 : || d_equalityEngine->areEqual(i, j) || !d_equalityEngine->hasTerm(a)
2033 : 14252 : || !d_equalityEngine->hasTerm(b) || d_equalityEngine->areEqual(a, b)
2034 : 17192 : || (ajExists && bjExists && d_equalityEngine->areEqual(aj, bj)))
2035 : : {
2036 : 5247 : continue;
2037 : : }
2038 : :
2039 : 3349 : int64_t prop = options().arrays.arraysPropagate;
2040 [ + - ]: 3349 : if (prop > 0) {
2041 : 3349 : propagateRowLemma(l);
2042 [ + + ]: 3349 : if (d_state.isInConflict())
2043 : : {
2044 : 715 : return true;
2045 : : }
2046 : : }
2047 : :
2048 : : // Make sure that any terms introduced by rewriting are appropriately stored in the equality database
2049 : 2634 : Node aj2 = rewrite(aj);
2050 [ + + ]: 2634 : if (aj != aj2) {
2051 [ + - ]: 144 : if (!ajExists) {
2052 : 144 : preRegisterTermInternal(aj);
2053 : : }
2054 [ - + ]: 144 : if (!d_equalityEngine->hasTerm(aj2))
2055 : : {
2056 : 0 : preRegisterTermInternal(aj2);
2057 : : }
2058 : 144 : d_im.assertInference(aj.eqNode(aj2),
2059 : : true,
2060 : : InferenceId::ARRAYS_EQ_TAUTOLOGY,
2061 : 144 : d_true,
2062 : : ProofRule::MACRO_SR_PRED_INTRO);
2063 : : }
2064 : 2634 : Node bj2 = rewrite(bj);
2065 [ + + ]: 2634 : if (bj != bj2) {
2066 [ + + ]: 269 : if (!bjExists) {
2067 : 19 : preRegisterTermInternal(bj);
2068 : : }
2069 [ - + ]: 269 : if (!d_equalityEngine->hasTerm(bj2))
2070 : : {
2071 : 0 : preRegisterTermInternal(bj2);
2072 : : }
2073 : 269 : d_im.assertInference(bj.eqNode(bj2),
2074 : : true,
2075 : : InferenceId::ARRAYS_EQ_TAUTOLOGY,
2076 : 269 : d_true,
2077 : : ProofRule::MACRO_SR_PRED_INTRO);
2078 : : }
2079 [ + + ]: 2634 : if (aj2 == bj2) {
2080 : 144 : continue;
2081 : : }
2082 : :
2083 : : // construct lemma
2084 : 2490 : Node eq1 = aj2.eqNode(bj2);
2085 : 2490 : Node eq1_r = rewrite(eq1);
2086 [ - + ]: 2490 : if (eq1_r == d_true) {
2087 [ - - ]: 0 : if (!d_equalityEngine->hasTerm(aj2))
2088 : : {
2089 : 0 : preRegisterTermInternal(aj2);
2090 : : }
2091 [ - - ]: 0 : if (!d_equalityEngine->hasTerm(bj2))
2092 : : {
2093 : 0 : preRegisterTermInternal(bj2);
2094 : : }
2095 : 0 : d_im.assertInference(eq1,
2096 : : true,
2097 : : InferenceId::ARRAYS_EQ_TAUTOLOGY,
2098 : 0 : d_true,
2099 : : ProofRule::MACRO_SR_PRED_INTRO);
2100 : 0 : continue;
2101 : : }
2102 : :
2103 : 2490 : Node eq2 = i.eqNode(j);
2104 : 2490 : Node eq2_r = rewrite(eq2);
2105 [ - + ]: 2490 : if (eq2_r == d_true) {
2106 : 0 : d_im.assertInference(eq2,
2107 : : true,
2108 : : InferenceId::ARRAYS_EQ_TAUTOLOGY,
2109 : 0 : d_true,
2110 : : ProofRule::MACRO_SR_PRED_INTRO);
2111 : 0 : continue;
2112 : : }
2113 : :
2114 : 4980 : Node lem = nm->mkNode(Kind::OR, eq2_r, eq1_r);
2115 : :
2116 [ + - ]: 2490 : Trace("arrays-lem") << "Arrays::addRowLemma (2) adding " << lem << "\n";
2117 : 2490 : d_RowAlreadyAdded.insert(l);
2118 : : // use non-rewritten nodes, theory preprocessing will rewrite
2119 : 2490 : d_im.arrayLemma(aj.eqNode(bj),
2120 : : InferenceId::ARRAYS_READ_OVER_WRITE,
2121 : 4980 : eq2.notNode(),
2122 : : ProofRule::ARRAYS_READ_OVER_WRITE);
2123 : 2490 : ++d_numRow;
2124 : 2490 : lemmasAdded = true;
2125 [ - + ]: 2490 : if (reduceSharing)
2126 : : {
2127 : 0 : return true;
2128 : : }
2129 : : }
2130 : 943 : return lemmasAdded;
2131 : : }
2132 : :
2133 : 172 : void TheoryArrays::conflict(TNode a, TNode b) {
2134 [ + - ]: 172 : Trace("pf::array") << "TheoryArrays::Conflict called" << std::endl;
2135 : 172 : d_im.conflictEqConstantMerge(a, b);
2136 : 172 : }
2137 : :
2138 : 50855 : TheoryArrays::TheoryArraysDecisionStrategy::TheoryArraysDecisionStrategy(
2139 : 50855 : TheoryArrays* ta)
2140 : 50855 : : DecisionStrategy(ta->d_env), d_ta(ta)
2141 : : {
2142 : 50855 : }
2143 : 42098 : void TheoryArrays::TheoryArraysDecisionStrategy::initialize() {}
2144 : 12044800 : Node TheoryArrays::TheoryArraysDecisionStrategy::getNextDecisionRequest()
2145 : : {
2146 : 12044800 : return d_ta->getNextDecisionRequest();
2147 : : }
2148 : 0 : std::string TheoryArrays::TheoryArraysDecisionStrategy::identify() const
2149 : : {
2150 : 0 : return std::string("th_arrays_dec");
2151 : : }
2152 : :
2153 : 14918 : void TheoryArrays::computeRelevantTerms(std::set<Node>& termSet)
2154 : : {
2155 : 14918 : NodeManager* nm = nodeManager();
2156 : : // make sure RIntro1 reads are included in the relevant set of reads
2157 : 14918 : eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(d_equalityEngine);
2158 [ + + ]: 49313 : for (; !eqcs_i.isFinished(); ++eqcs_i)
2159 : : {
2160 : 34395 : Node eqc = (*eqcs_i);
2161 [ + + ]: 34395 : if (!eqc.getType().isArray())
2162 : : {
2163 : : // not an array, skip
2164 : 33493 : continue;
2165 : : }
2166 : 902 : eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, d_equalityEngine);
2167 [ + + ]: 2638 : for (; !eqc_i.isFinished(); ++eqc_i)
2168 : : {
2169 : 3472 : Node n = *eqc_i;
2170 [ + + ]: 1736 : if (termSet.find(n) != termSet.end())
2171 : : {
2172 [ + + ]: 1694 : if (n.getKind() == Kind::STORE)
2173 : : {
2174 : : // Make sure RIntro1 reads are included
2175 : 1257 : Node r = nm->mkNode(Kind::SELECT, n, n[1]);
2176 [ + - ]: 838 : Trace("arrays::collectModelInfo")
2177 : 0 : << "TheoryArrays::collectModelInfo, adding RIntro1 read: " << r
2178 : 419 : << endl;
2179 : 419 : termSet.insert(r);
2180 : : }
2181 : : }
2182 : : }
2183 : : }
2184 : :
2185 : : // Now do a fixed-point iteration to get all reads that need to be included
2186 : : // because of RIntro2 rule
2187 : : bool changed;
2188 [ + + ]: 14959 : do
2189 : : {
2190 : 14959 : changed = false;
2191 : 14959 : eqcs_i = eq::EqClassesIterator(d_equalityEngine);
2192 [ + + ]: 50073 : for (; !eqcs_i.isFinished(); ++eqcs_i)
2193 : : {
2194 : 70228 : Node eqc = (*eqcs_i);
2195 : 35114 : eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, d_equalityEngine);
2196 [ + + ]: 82503 : for (; !eqc_i.isFinished(); ++eqc_i)
2197 : : {
2198 : 94778 : Node n = *eqc_i;
2199 [ + + ][ + + ]: 47389 : if (n.getKind() == Kind::SELECT && termSet.find(n) != termSet.end())
[ + + ]
2200 : : {
2201 : : // Find all terms equivalent to n[0] and get corresponding read terms
2202 : 14757 : Node array_eqc = d_equalityEngine->getRepresentative(n[0]);
2203 : : eq::EqClassIterator array_eqc_i =
2204 : 4919 : eq::EqClassIterator(array_eqc, d_equalityEngine);
2205 [ + + ]: 18017 : for (; !array_eqc_i.isFinished(); ++array_eqc_i)
2206 : : {
2207 : 26196 : Node arr = *array_eqc_i;
2208 : 39294 : if (arr.getKind() == Kind::STORE
2209 [ + - ]: 4900 : && termSet.find(arr) != termSet.end()
2210 : 17998 : && !d_equalityEngine->areEqual(arr[1], n[1]))
2211 : : {
2212 : 8301 : Node r = nm->mkNode(Kind::SELECT, arr, n[1]);
2213 : 2767 : if (termSet.find(r) == termSet.end()
2214 [ + + ][ + + ]: 5534 : && d_equalityEngine->hasTerm(r))
[ + + ][ + + ]
[ - - ]
2215 : : {
2216 [ + - ]: 76 : Trace("arrays::collectModelInfo")
2217 : : << "TheoryArrays::collectModelInfo, adding RIntro2(a) "
2218 : 0 : "read: "
2219 : 38 : << r << endl;
2220 : 38 : termSet.insert(r);
2221 : 38 : changed = true;
2222 : : }
2223 : 2767 : r = nm->mkNode(Kind::SELECT, arr[0], n[1]);
2224 : 2767 : if (termSet.find(r) == termSet.end()
2225 [ + + ][ + + ]: 5534 : && d_equalityEngine->hasTerm(r))
[ + + ][ + + ]
[ - - ]
2226 : : {
2227 [ + - ]: 98 : Trace("arrays::collectModelInfo")
2228 : : << "TheoryArrays::collectModelInfo, adding RIntro2(b) "
2229 : 0 : "read: "
2230 : 49 : << r << endl;
2231 : 49 : termSet.insert(r);
2232 : 49 : changed = true;
2233 : : }
2234 : : }
2235 : : }
2236 : :
2237 : : // Find all stores in which n[0] appears and get corresponding read
2238 : : // terms
2239 : 4919 : const CTNodeList* instores = d_infoMap.getInStores(array_eqc);
2240 : 4919 : size_t it = 0;
2241 [ + + ]: 9692 : for (; it < instores->size(); ++it)
2242 : : {
2243 : 9546 : TNode instore = (*instores)[it];
2244 [ - + ][ - + ]: 4773 : Assert(instore.getKind() == Kind::STORE);
[ - - ]
2245 [ + + ][ - - ]: 9546 : if (termSet.find(instore) != termSet.end()
2246 : 9546 : && !d_equalityEngine->areEqual(instore[1], n[1]))
2247 : : {
2248 : 9108 : Node r = nm->mkNode(Kind::SELECT, instore, n[1]);
2249 : 3036 : if (termSet.find(r) == termSet.end()
2250 [ + + ][ + + ]: 6072 : && d_equalityEngine->hasTerm(r))
[ + + ][ + + ]
[ - - ]
2251 : : {
2252 [ + - ]: 282 : Trace("arrays::collectModelInfo")
2253 : : << "TheoryArrays::collectModelInfo, adding RIntro2(c) "
2254 : 0 : "read: "
2255 : 141 : << r << endl;
2256 : 141 : termSet.insert(r);
2257 : 141 : changed = true;
2258 : : }
2259 : 3036 : r = nm->mkNode(Kind::SELECT, instore[0], n[1]);
2260 : 3036 : if (termSet.find(r) == termSet.end()
2261 [ + + ][ + + ]: 6072 : && d_equalityEngine->hasTerm(r))
[ + + ][ + + ]
[ - - ]
2262 : : {
2263 [ + - ]: 32 : Trace("arrays::collectModelInfo")
2264 : : << "TheoryArrays::collectModelInfo, adding RIntro2(d) "
2265 : 0 : "read: "
2266 : 16 : << r << endl;
2267 : 16 : termSet.insert(r);
2268 : 16 : changed = true;
2269 : : }
2270 : : }
2271 : : }
2272 : : }
2273 : : }
2274 : : }
2275 : : } while (changed);
2276 : 14918 : }
2277 : :
2278 : : } // namespace arrays
2279 : : } // namespace theory
2280 : : } // namespace cvc5::internal
|
