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