1 /********************* */
2 /*! \file theory_arrays.cpp
4 ** Top contributors (to current version):
5 ** Clark Barrett, Morgan Deters, Guy Katz
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2017 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.\endverbatim
12 ** \brief Implementation of the theory of arrays.
14 ** Implementation of the theory of arrays.
17 #include "theory/arrays/theory_arrays.h"
22 #include "expr/kind.h"
23 #include "options/arrays_options.h"
24 #include "options/smt_options.h"
25 #include "proof/array_proof.h"
26 #include "proof/proof_manager.h"
27 #include "proof/theory_proof.h"
28 #include "smt/command.h"
29 #include "smt/logic_exception.h"
30 #include "smt/smt_statistics_registry.h"
31 #include "theory/rewriter.h"
32 #include "theory/theory_model.h"
33 #include "theory/valuation.h"
41 // These are the options that produce the best empirical results on QF_AX benchmarks.
43 // eagerIndexSplitting = false
45 // Use static configuration of options for now
46 const bool d_ccStore
= false;
47 const bool d_useArrTable
= false;
48 //const bool d_eagerLemmas = false;
49 const bool d_preprocess
= true;
50 const bool d_solveWrite
= true;
51 const bool d_solveWrite2
= false;
52 // These are now options
53 //const bool d_propagateLemmas = true;
54 //bool d_useNonLinearOpt = true;
55 //bool d_lazyRIntro1 = true;
56 //bool d_eagerIndexSplitting = false;
58 TheoryArrays::TheoryArrays(context::Context
* c
, context::UserContext
* u
,
59 OutputChannel
& out
, Valuation valuation
,
60 const LogicInfo
& logicInfo
, std::string name
)
61 : Theory(THEORY_ARRAY
, c
, u
, out
, valuation
, logicInfo
, name
),
62 d_numRow(name
+ "theory::arrays::number of Row lemmas", 0),
63 d_numExt(name
+ "theory::arrays::number of Ext lemmas", 0),
64 d_numProp(name
+ "theory::arrays::number of propagations", 0),
65 d_numExplain(name
+ "theory::arrays::number of explanations", 0),
66 d_numNonLinear(name
+ "theory::arrays::number of calls to setNonLinear", 0),
67 d_numSharedArrayVarSplits(name
+ "theory::arrays::number of shared array var splits", 0),
68 d_numGetModelValSplits(name
+ "theory::arrays::number of getModelVal splits", 0),
69 d_numGetModelValConflicts(name
+ "theory::arrays::number of getModelVal conflicts", 0),
70 d_numSetModelValSplits(name
+ "theory::arrays::number of setModelVal splits", 0),
71 d_numSetModelValConflicts(name
+ "theory::arrays::number of setModelVal conflicts", 0),
72 d_ppEqualityEngine(u
, name
+ "theory::arrays::TheoryArraysPP" , true),
75 d_literalsToPropagate(c
),
76 d_literalsToPropagateIndex(c
, 0),
78 d_mayEqualEqualityEngine(c
, name
+ "theory::arrays::TheoryArraysMayEqual", true),
80 d_equalityEngine(d_notify
, c
, name
+ "theory::arrays::TheoryArrays", true),
83 d_infoMap(c
, &d_backtracker
, name
),
85 d_mergeInProgress(false),
90 d_sharedTerms(c
, false),
93 d_constReadsContext(new context::Context()),
94 d_contextPopper(c
, d_constReadsContext
),
96 d_decisionRequests(c
),
98 d_modelConstraints(c
),
101 d_readTableContext(new context::Context()),
103 d_inCheckModel(false),
104 d_proofReconstruction(&d_equalityEngine
)
106 smtStatisticsRegistry()->registerStat(&d_numRow
);
107 smtStatisticsRegistry()->registerStat(&d_numExt
);
108 smtStatisticsRegistry()->registerStat(&d_numProp
);
109 smtStatisticsRegistry()->registerStat(&d_numExplain
);
110 smtStatisticsRegistry()->registerStat(&d_numNonLinear
);
111 smtStatisticsRegistry()->registerStat(&d_numSharedArrayVarSplits
);
112 smtStatisticsRegistry()->registerStat(&d_numGetModelValSplits
);
113 smtStatisticsRegistry()->registerStat(&d_numGetModelValConflicts
);
114 smtStatisticsRegistry()->registerStat(&d_numSetModelValSplits
);
115 smtStatisticsRegistry()->registerStat(&d_numSetModelValConflicts
);
117 d_true
= NodeManager::currentNM()->mkConst
<bool>(true);
118 d_false
= NodeManager::currentNM()->mkConst
<bool>(false);
120 // The preprocessing congruence kinds
121 d_ppEqualityEngine
.addFunctionKind(kind::SELECT
);
122 d_ppEqualityEngine
.addFunctionKind(kind::STORE
);
124 // The kinds we are treating as function application in congruence
125 d_equalityEngine
.addFunctionKind(kind::SELECT
);
127 d_equalityEngine
.addFunctionKind(kind::STORE
);
130 d_equalityEngine
.addFunctionKind(kind::ARR_TABLE_FUN
);
133 d_reasonRow
= d_equalityEngine
.getFreshMergeReasonType();
134 d_reasonRow1
= d_equalityEngine
.getFreshMergeReasonType();
135 d_reasonExt
= d_equalityEngine
.getFreshMergeReasonType();
137 d_proofReconstruction
.setRowMergeTag(d_reasonRow
);
138 d_proofReconstruction
.setRow1MergeTag(d_reasonRow1
);
139 d_proofReconstruction
.setExtMergeTag(d_reasonExt
);
141 d_equalityEngine
.addPathReconstructionTrigger(d_reasonRow
, &d_proofReconstruction
);
142 d_equalityEngine
.addPathReconstructionTrigger(d_reasonRow1
, &d_proofReconstruction
);
143 d_equalityEngine
.addPathReconstructionTrigger(d_reasonExt
, &d_proofReconstruction
);
146 TheoryArrays::~TheoryArrays() {
147 vector
<CTNodeList
*>::iterator it
= d_readBucketAllocations
.begin(), iend
= d_readBucketAllocations
.end();
148 for (; it
!= iend
; ++it
) {
151 delete d_readTableContext
;
152 CNodeNListMap::iterator it2
= d_constReads
.begin();
153 for( ; it2
!= d_constReads
.end(); ++it2
) {
154 it2
->second
->deleteSelf();
156 delete d_constReadsContext
;
157 smtStatisticsRegistry()->unregisterStat(&d_numRow
);
158 smtStatisticsRegistry()->unregisterStat(&d_numExt
);
159 smtStatisticsRegistry()->unregisterStat(&d_numProp
);
160 smtStatisticsRegistry()->unregisterStat(&d_numExplain
);
161 smtStatisticsRegistry()->unregisterStat(&d_numNonLinear
);
162 smtStatisticsRegistry()->unregisterStat(&d_numSharedArrayVarSplits
);
163 smtStatisticsRegistry()->unregisterStat(&d_numGetModelValSplits
);
164 smtStatisticsRegistry()->unregisterStat(&d_numGetModelValConflicts
);
165 smtStatisticsRegistry()->unregisterStat(&d_numSetModelValSplits
);
166 smtStatisticsRegistry()->unregisterStat(&d_numSetModelValConflicts
);
169 void TheoryArrays::setMasterEqualityEngine(eq::EqualityEngine
* eq
) {
170 d_equalityEngine
.setMasterEqualityEngine(eq
);
174 /////////////////////////////////////////////////////////////////////////////
176 /////////////////////////////////////////////////////////////////////////////
179 bool TheoryArrays::ppDisequal(TNode a
, TNode b
) {
180 bool termsExist
= d_ppEqualityEngine
.hasTerm(a
) && d_ppEqualityEngine
.hasTerm(b
);
181 Assert(!termsExist
|| !a
.isConst() || !b
.isConst() || a
== b
|| d_ppEqualityEngine
.areDisequal(a
, b
, false));
182 return ((termsExist
&& d_ppEqualityEngine
.areDisequal(a
, b
, false)) ||
183 Rewriter::rewrite(a
.eqNode(b
)) == d_false
);
187 Node
TheoryArrays::solveWrite(TNode term
, bool solve1
, bool solve2
, bool ppCheck
)
192 if (term
[0].getKind() != kind::STORE
&&
193 term
[1].getKind() != kind::STORE
) {
196 TNode left
= term
[0];
197 TNode right
= term
[1];
198 int leftWrites
= 0, rightWrites
= 0;
200 // Count nested writes
202 while (e1
.getKind() == kind::STORE
) {
208 while (e2
.getKind() == kind::STORE
) {
213 if (rightWrites
> leftWrites
) {
217 int tmpWrites
= leftWrites
;
218 leftWrites
= rightWrites
;
219 rightWrites
= tmpWrites
;
222 NodeManager
* nm
= NodeManager::currentNM();
223 if (rightWrites
== 0) {
227 // write(store, index_0, v_0, index_1, v_1, ..., index_n, v_n) = store IFF
229 // read(store, index_n) = v_n &
230 // index_{n-1} != index_n -> read(store, index_{n-1}) = v_{n-1} &
231 // (index_{n-2} != index_{n-1} & index_{n-2} != index_n) -> read(store, index_{n-2}) = v_{n-2} &
233 // (index_1 != index_2 & ... & index_1 != index_n) -> read(store, index_1) = v_1
234 // (index_0 != index_1 & index_0 != index_2 & ... & index_0 != index_n) -> read(store, index_0) = v_0
235 TNode write_i
, write_j
, index_i
, index_j
;
237 NodeBuilder
<> result(kind::AND
);
240 for (i
= leftWrites
-1; i
>= 0; --i
) {
241 index_i
= write_i
[1];
243 // build: [index_i /= index_n && index_i /= index_(n-1) &&
244 // ... && index_i /= index_(i+1)] -> read(store, index_i) = v_i
247 NodeBuilder
<> hyp(kind::AND
);
248 for (j
= leftWrites
- 1; j
> i
; --j
) {
249 index_j
= write_j
[1];
250 if (!ppCheck
|| !ppDisequal(index_i
, index_j
)) {
251 Node
hyp2(index_i
.eqNode(index_j
));
252 hyp
<< hyp2
.notNode();
254 write_j
= write_j
[0];
257 Node r1
= nm
->mkNode(kind::SELECT
, e1
, index_i
);
258 conc
= r1
.eqNode(write_i
[2]);
259 if (hyp
.getNumChildren() != 0) {
260 if (hyp
.getNumChildren() == 1) {
261 conc
= hyp
.getChild(0).impNode(conc
);
265 conc
= r1
.impNode(conc
);
272 // Prepare for next iteration
273 write_i
= write_i
[0];
276 Assert(result
.getNumChildren() > 0);
277 if (result
.getNumChildren() == 1) {
278 return result
.getChild(0);
286 // store(...) = store(a,i,v) ==>
287 // store(store(...),i,select(a,i)) = a && select(store(...),i)=v
290 NodeBuilder
<> nb(kind::AND
);
291 while (right
.getKind() == kind::STORE
) {
292 tmp
= nm
->mkNode(kind::SELECT
, l
, right
[1]);
293 nb
<< tmp
.eqNode(right
[2]);
294 tmp
= nm
->mkNode(kind::SELECT
, right
[0], right
[1]);
295 l
= nm
->mkNode(kind::STORE
, l
, right
[1], tmp
);
298 nb
<< solveWrite(l
.eqNode(right
), solve1
, solve2
, ppCheck
);
306 Node
TheoryArrays::ppRewrite(TNode term
) {
307 if (!d_preprocess
) return term
;
308 d_ppEqualityEngine
.addTerm(term
);
309 switch (term
.getKind()) {
311 // select(store(a,i,v),j) = select(a,j)
313 if (term
[0].getKind() == kind::STORE
&& ppDisequal(term
[0][1], term
[1])) {
314 return NodeBuilder
<2>(kind::SELECT
) << term
[0][0] << term
[1];
319 // store(store(a,i,v),j,w) = store(store(a,j,w),i,v)
320 // IF i != j and j comes before i in the ordering
321 if (term
[0].getKind() == kind::STORE
&& (term
[1] < term
[0][1]) && ppDisequal(term
[1],term
[0][1])) {
322 Node inner
= NodeBuilder
<3>(kind::STORE
) << term
[0][0] << term
[1] << term
[2];
323 Node outer
= NodeBuilder
<3>(kind::STORE
) << inner
<< term
[0][1] << term
[0][2];
329 return solveWrite(term
, d_solveWrite
, d_solveWrite2
, true);
339 Theory::PPAssertStatus
TheoryArrays::ppAssert(TNode in
, SubstitutionMap
& outSubstitutions
) {
340 switch(in
.getKind()) {
343 d_ppFacts
.push_back(in
);
344 d_ppEqualityEngine
.assertEquality(in
, true, in
);
345 if (in
[0].isVar() && !in
[1].hasSubterm(in
[0]) && (in
[1].getType()).isSubtypeOf(in
[0].getType()) ){
346 outSubstitutions
.addSubstitution(in
[0], in
[1]);
347 return PP_ASSERT_STATUS_SOLVED
;
349 if (in
[1].isVar() && !in
[0].hasSubterm(in
[1]) && (in
[0].getType()).isSubtypeOf(in
[1].getType())){
350 outSubstitutions
.addSubstitution(in
[1], in
[0]);
351 return PP_ASSERT_STATUS_SOLVED
;
357 d_ppFacts
.push_back(in
);
358 if (in
[0].getKind() == kind::EQUAL
) {
361 d_ppEqualityEngine
.assertEquality(in
[0], false, in
);
368 return PP_ASSERT_STATUS_UNSOLVED
;
372 /////////////////////////////////////////////////////////////////////////////
373 // T-PROPAGATION / REGISTRATION
374 /////////////////////////////////////////////////////////////////////////////
377 bool TheoryArrays::propagate(TNode literal
)
379 Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::propagate(" << literal
<< ")" << std::endl
;
381 // If already in conflict, no more propagation
383 Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::propagate(" << literal
<< "): already in conflict" << std::endl
;
388 if (d_inCheckModel
&& getSatContext()->getLevel() != d_topLevel
) {
391 bool ok
= d_out
->propagate(literal
);
396 }/* TheoryArrays::propagate(TNode) */
399 void TheoryArrays::explain(TNode literal
, std::vector
<TNode
>& assumptions
,
400 eq::EqProof
* proof
) {
402 bool polarity
= literal
.getKind() != kind::NOT
;
403 TNode atom
= polarity
? literal
: literal
[0];
404 //eq::EqProof * eqp = new eq::EqProof;
405 // eq::EqProof * eqp = NULL;
406 if (atom
.getKind() == kind::EQUAL
) {
407 d_equalityEngine
.explainEquality(atom
[0], atom
[1], polarity
, assumptions
, proof
);
409 d_equalityEngine
.explainPredicate(atom
, polarity
, assumptions
, proof
);
412 Debug("pf::array") << " Proof is : " << std::endl
;
413 proof
->debug_print("pf::array");
416 Debug("pf::array") << "Array: explain( " << literal
<< " ):" << std::endl
<< "\t";
417 for (unsigned i
= 0; i
< assumptions
.size(); ++i
) {
418 Debug("pf::array") << assumptions
[i
] << " ";
420 Debug("pf::array") << std::endl
;
423 TNode
TheoryArrays::weakEquivGetRep(TNode node
) {
426 pointer
= d_infoMap
.getWeakEquivPointer(node
);
427 if (pointer
.isNull()) {
434 TNode
TheoryArrays::weakEquivGetRepIndex(TNode node
, TNode index
) {
435 Assert(!index
.isNull());
436 TNode pointer
, index2
;
438 pointer
= d_infoMap
.getWeakEquivPointer(node
);
439 if (pointer
.isNull()) {
442 index2
= d_infoMap
.getWeakEquivIndex(node
);
443 if (index2
.isNull() || !d_equalityEngine
.areEqual(index
, index2
)) {
447 TNode secondary
= d_infoMap
.getWeakEquivSecondary(node
);
448 if (secondary
.isNull()) {
456 void TheoryArrays::visitAllLeaves(TNode reason
, vector
<TNode
>& conjunctions
) {
457 switch (reason
.getKind()) {
459 Assert(reason
.getNumChildren() == 2);
460 visitAllLeaves(reason
[0], conjunctions
);
461 visitAllLeaves(reason
[1], conjunctions
);
464 conjunctions
.push_back(reason
);
467 d_equalityEngine
.explainEquality(reason
[0], reason
[1], true, conjunctions
);
474 void TheoryArrays::weakEquivBuildCond(TNode node
, TNode index
, vector
<TNode
>& conjunctions
) {
475 Assert(!index
.isNull());
476 TNode pointer
, index2
;
478 pointer
= d_infoMap
.getWeakEquivPointer(node
);
479 if (pointer
.isNull()) {
482 index2
= d_infoMap
.getWeakEquivIndex(node
);
483 if (index2
.isNull()) {
484 // Null index means these two nodes became equal: explain the equality.
485 d_equalityEngine
.explainEquality(node
, pointer
, true, conjunctions
);
488 else if (!d_equalityEngine
.areEqual(index
, index2
)) {
489 // If indices are not equal in current context, need to add that to the lemma.
490 Node reason
= index
.eqNode(index2
).notNode();
491 d_permRef
.push_back(reason
);
492 conjunctions
.push_back(reason
);
496 TNode secondary
= d_infoMap
.getWeakEquivSecondary(node
);
497 if (secondary
.isNull()) {
500 TNode reason
= d_infoMap
.getWeakEquivSecondaryReason(node
);
501 Assert(!reason
.isNull());
502 visitAllLeaves(reason
, conjunctions
);
508 void TheoryArrays::weakEquivMakeRep(TNode node
) {
509 TNode pointer
= d_infoMap
.getWeakEquivPointer(node
);
510 if (pointer
.isNull()) {
513 weakEquivMakeRep(pointer
);
514 d_infoMap
.setWeakEquivPointer(pointer
, node
);
515 d_infoMap
.setWeakEquivIndex(pointer
, d_infoMap
.getWeakEquivIndex(node
));
516 d_infoMap
.setWeakEquivPointer(node
, TNode());
517 weakEquivMakeRepIndex(node
);
520 void TheoryArrays::weakEquivMakeRepIndex(TNode node
) {
521 TNode secondary
= d_infoMap
.getWeakEquivSecondary(node
);
522 if (secondary
.isNull()) {
525 TNode index
= d_infoMap
.getWeakEquivIndex(node
);
526 Assert(!index
.isNull());
527 TNode index2
= d_infoMap
.getWeakEquivIndex(secondary
);
530 while (index2
.isNull() || !d_equalityEngine
.areEqual(index
, index2
)) {
531 next
= d_infoMap
.getWeakEquivPointer(secondary
);
532 d_infoMap
.setWeakEquivSecondary(node
, next
);
533 reason
= d_infoMap
.getWeakEquivSecondaryReason(node
);
534 if (index2
.isNull()) {
535 reason
= reason
.andNode(secondary
.eqNode(next
));
538 reason
= reason
.andNode(index
.eqNode(index2
).notNode());
540 d_permRef
.push_back(reason
);
541 d_infoMap
.setWeakEquivSecondaryReason(node
, reason
);
546 index2
= d_infoMap
.getWeakEquivIndex(secondary
);
548 weakEquivMakeRepIndex(secondary
);
549 d_infoMap
.setWeakEquivSecondary(secondary
, node
);
550 d_infoMap
.setWeakEquivSecondaryReason(secondary
, d_infoMap
.getWeakEquivSecondaryReason(node
));
551 d_infoMap
.setWeakEquivSecondary(node
, TNode());
552 d_infoMap
.setWeakEquivSecondaryReason(node
, TNode());
555 void TheoryArrays::weakEquivAddSecondary(TNode index
, TNode arrayFrom
, TNode arrayTo
, TNode reason
) {
556 std::unordered_set
<TNode
, TNodeHashFunction
> marked
;
557 vector
<TNode
> index_trail
;
558 vector
<TNode
>::iterator it
, iend
;
559 Node equivalence_trail
= reason
;
561 TNode pointer
, indexRep
;
562 if (!index
.isNull()) {
563 index_trail
.push_back(index
);
564 marked
.insert(d_equalityEngine
.getRepresentative(index
));
566 while (arrayFrom
!= arrayTo
) {
567 index
= d_infoMap
.getWeakEquivIndex(arrayFrom
);
568 pointer
= d_infoMap
.getWeakEquivPointer(arrayFrom
);
569 if (!index
.isNull()) {
570 indexRep
= d_equalityEngine
.getRepresentative(index
);
571 if (marked
.find(indexRep
) == marked
.end() && weakEquivGetRepIndex(arrayFrom
, index
) != arrayTo
) {
572 weakEquivMakeRepIndex(arrayFrom
);
573 d_infoMap
.setWeakEquivSecondary(arrayFrom
, arrayTo
);
574 current_reason
= equivalence_trail
;
575 for (it
= index_trail
.begin(), iend
= index_trail
.end(); it
!= iend
; ++it
) {
576 current_reason
= current_reason
.andNode(index
.eqNode(*it
).notNode());
578 d_permRef
.push_back(current_reason
);
579 d_infoMap
.setWeakEquivSecondaryReason(arrayFrom
, current_reason
);
581 marked
.insert(indexRep
);
584 equivalence_trail
= equivalence_trail
.andNode(arrayFrom
.eqNode(pointer
));
590 void TheoryArrays::checkWeakEquiv(bool arraysMerged
) {
591 eq::EqClassesIterator eqcs_i
= eq::EqClassesIterator(&d_mayEqualEqualityEngine
);
592 for (; !eqcs_i
.isFinished(); ++eqcs_i
) {
593 Node eqc
= (*eqcs_i
);
594 if (!eqc
.getType().isArray()) {
597 eq::EqClassIterator eqc_i
= eq::EqClassIterator(eqc
, &d_mayEqualEqualityEngine
);
598 TNode rep
= d_mayEqualEqualityEngine
.getRepresentative(*eqc_i
);
599 TNode weakEquivRep
= weakEquivGetRep(rep
);
600 for (; !eqc_i
.isFinished(); ++eqc_i
) {
602 Assert(!arraysMerged
|| weakEquivGetRep(n
) == weakEquivRep
);
603 TNode pointer
= d_infoMap
.getWeakEquivPointer(n
);
604 TNode index
= d_infoMap
.getWeakEquivIndex(n
);
605 TNode secondary
= d_infoMap
.getWeakEquivSecondary(n
);
606 Assert(pointer
.isNull() == (weakEquivGetRep(n
) == n
));
607 Assert(!pointer
.isNull() || secondary
.isNull());
608 Assert(!index
.isNull() || secondary
.isNull());
609 Assert(d_infoMap
.getWeakEquivSecondaryReason(n
).isNull() || !secondary
.isNull());
610 if (!pointer
.isNull()) {
611 if (index
.isNull()) {
612 Assert(d_equalityEngine
.areEqual(n
, pointer
));
615 Assert((n
.getKind() == kind::STORE
&& n
[0] == pointer
&& n
[1] == index
) ||
616 (pointer
.getKind() == kind::STORE
&& pointer
[0] == n
&& pointer
[1] == index
));
624 * Stores in d_infoMap the following information for each term a of type array:
626 * - all i, such that there exists a term a[i] or a = store(b i v)
627 * (i.e. all indices it is being read atl; store(b i v) is implicitly read at
628 * position i due to the implicit axiom store(b i v)[i] = v )
630 * - all the stores a is congruent to (this information is context dependent)
632 * - all store terms of the form store (a i v) (i.e. in which a appears
633 * directly; this is invariant because no new store terms are created)
635 * Note: completeness depends on having pre-register called on all the input
636 * terms before starting to instantiate lemmas.
638 void TheoryArrays::preRegisterTermInternal(TNode node
)
643 Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::preRegisterTerm(" << node
<< ")" << std::endl
;
644 switch (node
.getKind()) {
646 // Add the trigger for equality
647 // NOTE: note that if the equality is true or false already, it might not be added
648 d_equalityEngine
.addTriggerEquality(node
);
651 // Invariant: array terms should be preregistered before being added to the equality engine
652 if (d_equalityEngine
.hasTerm(node
)) {
653 Assert(d_isPreRegistered
.find(node
) != d_isPreRegistered
.end());
657 TNode store
= d_equalityEngine
.getRepresentative(node
[0]);
659 // The may equal needs the store
660 d_mayEqualEqualityEngine
.addTerm(store
);
662 if (options::arraysLazyRIntro1() && !options::arraysWeakEquivalence()) {
663 // Apply RIntro1 rule to any stores equal to store if not done already
664 const CTNodeList
* stores
= d_infoMap
.getStores(store
);
665 CTNodeList::const_iterator it
= stores
->begin();
666 if (it
!= stores
->end()) {
667 NodeManager
* nm
= NodeManager::currentNM();
669 if (!d_infoMap
.rIntro1Applied(s
)) {
670 d_infoMap
.setRIntro1Applied(s
);
671 Assert(s
.getKind()==kind::STORE
);
672 Node ni
= nm
->mkNode(kind::SELECT
, s
, s
[1]);
674 preRegisterTermInternal(ni
);
676 d_equalityEngine
.assertEquality(ni
.eqNode(s
[2]), true, d_true
, d_reasonRow1
);
677 Assert(++it
== stores
->end());
682 if (node
.getType().isArray()) {
683 d_mayEqualEqualityEngine
.addTerm(node
);
684 d_equalityEngine
.addTriggerTerm(node
, THEORY_ARRAY
);
687 d_equalityEngine
.addTerm(node
);
690 Assert(d_equalityEngine
.getRepresentative(store
) == store
);
691 d_infoMap
.addIndex(store
, node
[1]);
693 // Synchronize d_constReadsContext with SAT context
694 Assert(d_constReadsContext
->getLevel() <= getSatContext()->getLevel());
695 while (d_constReadsContext
->getLevel() < getSatContext()->getLevel()) {
696 d_constReadsContext
->push();
699 // Record read in sharing data structure
700 TNode index
= d_equalityEngine
.getRepresentative(node
[1]);
701 if (!options::arraysWeakEquivalence() && index
.isConst()) {
703 CNodeNListMap::iterator it
= d_constReads
.find(index
);
704 if (it
== d_constReads
.end()) {
705 temp
= new(true) CTNodeList(d_constReadsContext
);
706 d_constReads
[index
] = temp
;
711 temp
->push_back(node
);
712 d_constReadsList
.push_back(node
);
715 d_reads
.push_back(node
);
718 Assert((d_isPreRegistered
.insert(node
), true));
719 checkRowForIndex(node
[1], store
);
723 if (d_equalityEngine
.hasTerm(node
)) {
726 d_equalityEngine
.addTriggerTerm(node
, THEORY_ARRAY
);
728 TNode a
= d_equalityEngine
.getRepresentative(node
[0]);
730 if (node
.isConst()) {
731 // Can't use d_mayEqualEqualityEngine to merge node with a because they are both constants,
732 // so just set the default value manually for node.
733 Assert(a
== node
[0]);
734 d_mayEqualEqualityEngine
.addTerm(node
);
735 Assert(d_mayEqualEqualityEngine
.getRepresentative(node
) == node
);
736 Assert(d_mayEqualEqualityEngine
.getRepresentative(a
) == a
);
737 DefValMap::iterator it
= d_defValues
.find(a
);
738 Assert(it
!= d_defValues
.end());
739 d_defValues
[node
] = (*it
).second
;
742 d_mayEqualEqualityEngine
.assertEquality(node
.eqNode(a
), true, d_true
);
743 Assert(d_mayEqualEqualityEngine
.consistent());
746 if (!options::arraysLazyRIntro1() || options::arraysWeakEquivalence()) {
749 NodeManager
* nm
= NodeManager::currentNM();
750 Node ni
= nm
->mkNode(kind::SELECT
, node
, i
);
751 if (!d_equalityEngine
.hasTerm(ni
)) {
752 preRegisterTermInternal(ni
);
755 // Apply RIntro1 Rule
756 d_equalityEngine
.assertEquality(ni
.eqNode(v
), true, d_true
, d_reasonRow1
);
759 d_infoMap
.addStore(node
, node
);
760 d_infoMap
.addInStore(a
, node
);
761 d_infoMap
.setModelRep(node
, node
);
763 //Add-Store for Weak Equivalence
764 if (options::arraysWeakEquivalence()) {
765 Assert(weakEquivGetRep(node
[0]) == weakEquivGetRep(a
));
766 Assert(weakEquivGetRep(node
) == node
);
767 d_infoMap
.setWeakEquivPointer(node
, node
[0]);
768 d_infoMap
.setWeakEquivIndex(node
, node
[1]);
769 #ifdef CVC4_ASSERTIONS
770 checkWeakEquiv(false);
777 case kind::STORE_ALL
: {
778 if (d_equalityEngine
.hasTerm(node
)) {
781 ArrayStoreAll storeAll
= node
.getConst
<ArrayStoreAll
>();
782 Node defaultValue
= Node::fromExpr(storeAll
.getExpr());
783 if (!defaultValue
.isConst()) {
784 throw LogicException("Array theory solver does not yet support non-constant default values for arrays");
786 d_infoMap
.setConstArr(node
, node
);
787 d_mayEqualEqualityEngine
.addTerm(node
);
788 Assert(d_mayEqualEqualityEngine
.getRepresentative(node
) == node
);
789 d_equalityEngine
.addTriggerTerm(node
, THEORY_ARRAY
);
790 d_defValues
[node
] = defaultValue
;
795 if (node
.getType().isArray()) {
796 // The may equal needs the node
797 d_mayEqualEqualityEngine
.addTerm(node
);
798 d_equalityEngine
.addTriggerTerm(node
, THEORY_ARRAY
);
799 Assert(d_equalityEngine
.getSize(node
) == 1);
802 d_equalityEngine
.addTerm(node
);
807 // Invariant: preregistered terms are exactly the terms in the equality engine
808 // Disabled, see comment above for kind::EQUAL
809 // Assert(d_equalityEngine.hasTerm(node) || !d_equalityEngine.consistent());
813 void TheoryArrays::preRegisterTerm(TNode node
)
815 preRegisterTermInternal(node
);
816 // If we have a select from an array of Bools, mark it as a term that can be propagated.
817 // Note: do this here instead of in preRegisterTermInternal to prevent internal select
818 // terms from being propagated out (as this results in an assertion failure).
819 if (node
.getKind() == kind::SELECT
&& node
.getType().isBoolean()) {
820 d_equalityEngine
.addTriggerPredicate(node
);
825 void TheoryArrays::propagate(Effort e
)
827 // direct propagation now
831 Node
TheoryArrays::explain(TNode literal
) {
832 Node explanation
= explain(literal
, NULL
);
836 Node
TheoryArrays::explain(TNode literal
, eq::EqProof
* proof
) {
838 Debug("arrays") << spaces(getSatContext()->getLevel())
839 << "TheoryArrays::explain(" << literal
<< ")" << std::endl
;
840 std::vector
<TNode
> assumptions
;
841 explain(literal
, assumptions
, proof
);
842 return mkAnd(assumptions
);
845 /////////////////////////////////////////////////////////////////////////////
847 /////////////////////////////////////////////////////////////////////////////
850 void TheoryArrays::addSharedTerm(TNode t
) {
851 Debug("arrays::sharing") << spaces(getSatContext()->getLevel()) << "TheoryArrays::addSharedTerm(" << t
<< ")" << std::endl
;
852 d_equalityEngine
.addTriggerTerm(t
, THEORY_ARRAY
);
853 if (t
.getType().isArray()) {
854 d_sharedArrays
.insert(t
);
857 #ifdef CVC4_ASSERTIONS
858 d_sharedOther
.insert(t
);
860 d_sharedTerms
= true;
865 EqualityStatus
TheoryArrays::getEqualityStatus(TNode a
, TNode b
) {
866 Assert(d_equalityEngine
.hasTerm(a
) && d_equalityEngine
.hasTerm(b
));
867 if (d_equalityEngine
.areEqual(a
, b
)) {
868 // The terms are implied to be equal
869 return EQUALITY_TRUE
;
871 else if (d_equalityEngine
.areDisequal(a
, b
, false)) {
872 // The terms are implied to be dis-equal
873 return EQUALITY_FALSE
;
875 return EQUALITY_UNKNOWN
;//FALSE_IN_MODEL;
879 void TheoryArrays::checkPair(TNode r1
, TNode r2
)
881 Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): checking reads " << r1
<< " and " << r2
<< std::endl
;
885 Assert(d_equalityEngine
.isTriggerTerm(x
, THEORY_ARRAY
));
887 if (d_equalityEngine
.hasTerm(x
) && d_equalityEngine
.hasTerm(y
) &&
888 (d_equalityEngine
.areEqual(x
,y
) || d_equalityEngine
.areDisequal(x
,y
,false))) {
889 Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): equality known, skipping" << std::endl
;
893 // If the terms are already known to be equal, we are also in good shape
894 if (d_equalityEngine
.areEqual(r1
, r2
)) {
895 Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): equal, skipping" << std::endl
;
899 if (r1
[0] != r2
[0]) {
900 // If arrays are known to be disequal, or cannot become equal, we can continue
901 Assert(d_mayEqualEqualityEngine
.hasTerm(r1
[0]) && d_mayEqualEqualityEngine
.hasTerm(r2
[0]));
902 if (r1
[0].getType() != r2
[0].getType() ||
903 d_equalityEngine
.areDisequal(r1
[0], r2
[0], false)) {
904 Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): arrays can't be equal, skipping" << std::endl
;
907 else if (!d_mayEqualEqualityEngine
.areEqual(r1
[0], r2
[0])) {
912 if (!d_equalityEngine
.isTriggerTerm(y
, THEORY_ARRAY
)) {
913 Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): not connected to shared terms, skipping" << std::endl
;
917 // Get representative trigger terms
918 TNode x_shared
= d_equalityEngine
.getTriggerTermRepresentative(x
, THEORY_ARRAY
);
919 TNode y_shared
= d_equalityEngine
.getTriggerTermRepresentative(y
, THEORY_ARRAY
);
920 EqualityStatus eqStatusDomain
= d_valuation
.getEqualityStatus(x_shared
, y_shared
);
921 switch (eqStatusDomain
) {
922 case EQUALITY_TRUE_AND_PROPAGATED
:
923 // Should have been propagated to us
927 // Missed propagation - need to add the pair so that theory engine can force propagation
928 Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): missed propagation" << std::endl
;
930 case EQUALITY_FALSE_AND_PROPAGATED
:
931 // Should have been propagated to us
934 case EQUALITY_FALSE_IN_MODEL
:
935 // This is unlikely, but I think it could happen
936 Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): checkPair called when false in model" << std::endl
;
939 // Covers EQUALITY_TRUE_IN_MODEL (common case) and EQUALITY_UNKNOWN
944 Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): adding to care-graph" << std::endl
;
945 addCarePair(x_shared
, y_shared
);
949 void TheoryArrays::computeCareGraph()
951 if (d_sharedArrays
.size() > 0) {
952 CDNodeSet::key_iterator it1
= d_sharedArrays
.key_begin(), it2
, iend
= d_sharedArrays
.key_end();
953 for (; it1
!= iend
; ++it1
) {
954 for (it2
= it1
, ++it2
; it2
!= iend
; ++it2
) {
955 if ((*it1
).getType() != (*it2
).getType()) {
958 EqualityStatus eqStatusArr
= getEqualityStatus((*it1
), (*it2
));
959 if (eqStatusArr
!= EQUALITY_UNKNOWN
) {
962 Assert(d_valuation
.getEqualityStatus((*it1
), (*it2
)) == EQUALITY_UNKNOWN
);
963 addCarePair((*it1
), (*it2
));
964 ++d_numSharedArrayVarSplits
;
970 // Synchronize d_constReadsContext with SAT context
971 Assert(d_constReadsContext
->getLevel() <= getSatContext()->getLevel());
972 while (d_constReadsContext
->getLevel() < getSatContext()->getLevel()) {
973 d_constReadsContext
->push();
976 // Go through the read terms and see if there are any to split on
978 // Give constReadsContext a push so that all the work it does here is erased - models can change if context changes at all
979 // The context is popped at the end. If this loop is interrupted for some reason, we have to make sure the context still
980 // gets popped or the solver will be in an inconsistent state
981 d_constReadsContext
->push();
982 unsigned size
= d_reads
.size();
983 for (unsigned i
= 0; i
< size
; ++ i
) {
984 TNode r1
= d_reads
[i
];
986 Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): checking read " << r1
<< std::endl
;
987 Assert(d_equalityEngine
.hasTerm(r1
));
990 if (!d_equalityEngine
.isTriggerTerm(x
, THEORY_ARRAY
)) {
991 Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): not connected to shared terms, skipping" << std::endl
;
994 Node x_shared
= d_equalityEngine
.getTriggerTermRepresentative(x
, THEORY_ARRAY
);
996 // 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
997 // Also, insert this read in the list at the proper index
999 if (!x_shared
.isConst()) {
1000 x_shared
= d_valuation
.getModelValue(x_shared
);
1002 if (!x_shared
.isNull()) {
1004 CNodeNListMap::iterator it
= d_constReads
.find(x_shared
);
1005 if (it
== d_constReads
.end()) {
1006 // This is the only x_shared with this model value - no need to create any splits
1007 temp
= new(true) CTNodeList(d_constReadsContext
);
1008 d_constReads
[x_shared
] = temp
;
1011 temp
= (*it
).second
;
1012 for (size_t j
= 0; j
< temp
->size(); ++j
) {
1013 checkPair(r1
, (*temp
)[j
]);
1016 temp
->push_back(r1
);
1019 // We don't know the model value for x. Just do brute force examination of all pairs of reads
1020 for (unsigned j
= 0; j
< size
; ++j
) {
1021 TNode r2
= d_reads
[j
];
1022 Assert(d_equalityEngine
.hasTerm(r2
));
1025 for (unsigned j
= 0; j
< d_constReadsList
.size(); ++j
) {
1026 TNode r2
= d_constReadsList
[j
];
1027 Assert(d_equalityEngine
.hasTerm(r2
));
1032 d_constReadsContext
->pop();
1037 /////////////////////////////////////////////////////////////////////////////
1039 /////////////////////////////////////////////////////////////////////////////
1042 void TheoryArrays::collectModelInfo( TheoryModel
* m
)
1046 // Compute terms appearing in assertions and shared terms
1047 computeRelevantTerms(termSet
);
1049 // Compute arrays that we need to produce representatives for and also make sure RIntro1 reads are included in the relevant set of reads
1050 NodeManager
* nm
= NodeManager::currentNM();
1051 std::vector
<Node
> arrays
;
1052 bool computeRep
, isArray
;
1053 eq::EqClassesIterator eqcs_i
= eq::EqClassesIterator(&d_equalityEngine
);
1054 for (; !eqcs_i
.isFinished(); ++eqcs_i
) {
1055 Node eqc
= (*eqcs_i
);
1056 isArray
= eqc
.getType().isArray();
1061 eq::EqClassIterator eqc_i
= eq::EqClassIterator(eqc
, &d_equalityEngine
);
1062 for (; !eqc_i
.isFinished(); ++eqc_i
) {
1064 // If this EC is an array type and it contains something other than STORE nodes, we have to compute a representative explicitly
1065 if (isArray
&& termSet
.find(n
) != termSet
.end()) {
1066 if (n
.getKind() == kind::STORE
) {
1067 // Make sure RIntro1 reads are included
1068 Node r
= nm
->mkNode(kind::SELECT
, n
, n
[1]);
1069 Trace("arrays::collectModelInfo") << "TheoryArrays::collectModelInfo, adding RIntro1 read: " << r
<< endl
;
1072 else if (!computeRep
) {
1073 arrays
.push_back(n
);
1080 // Now do a fixed-point iteration to get all reads that need to be included because of RIntro2 rule
1084 eqcs_i
= eq::EqClassesIterator(&d_equalityEngine
);
1085 for (; !eqcs_i
.isFinished(); ++eqcs_i
) {
1086 Node eqc
= (*eqcs_i
);
1087 eq::EqClassIterator eqc_i
= eq::EqClassIterator(eqc
, &d_equalityEngine
);
1088 for (; !eqc_i
.isFinished(); ++eqc_i
) {
1090 if (n
.getKind() == kind::SELECT
&& termSet
.find(n
) != termSet
.end()) {
1092 // Find all terms equivalent to n[0] and get corresponding read terms
1093 Node array_eqc
= d_equalityEngine
.getRepresentative(n
[0]);
1094 eq::EqClassIterator array_eqc_i
= eq::EqClassIterator(array_eqc
, &d_equalityEngine
);
1095 for (; !array_eqc_i
.isFinished(); ++array_eqc_i
) {
1096 Node arr
= *array_eqc_i
;
1097 if (arr
.getKind() == kind::STORE
&&
1098 termSet
.find(arr
) != termSet
.end() &&
1099 !d_equalityEngine
.areEqual(arr
[1],n
[1])) {
1100 Node r
= nm
->mkNode(kind::SELECT
, arr
, n
[1]);
1101 if (termSet
.find(r
) == termSet
.end() && d_equalityEngine
.hasTerm(r
)) {
1102 Trace("arrays::collectModelInfo") << "TheoryArrays::collectModelInfo, adding RIntro2(a) read: " << r
<< endl
;
1106 r
= nm
->mkNode(kind::SELECT
, arr
[0], n
[1]);
1107 if (termSet
.find(r
) == termSet
.end() && d_equalityEngine
.hasTerm(r
)) {
1108 Trace("arrays::collectModelInfo") << "TheoryArrays::collectModelInfo, adding RIntro2(b) read: " << r
<< endl
;
1115 // Find all stores in which n[0] appears and get corresponding read terms
1116 const CTNodeList
* instores
= d_infoMap
.getInStores(array_eqc
);
1118 for(; it
< instores
->size(); ++it
) {
1119 TNode instore
= (*instores
)[it
];
1120 Assert(instore
.getKind()==kind::STORE
);
1121 if (termSet
.find(instore
) != termSet
.end() &&
1122 !d_equalityEngine
.areEqual(instore
[1],n
[1])) {
1123 Node r
= nm
->mkNode(kind::SELECT
, instore
, n
[1]);
1124 if (termSet
.find(r
) == termSet
.end() && d_equalityEngine
.hasTerm(r
)) {
1125 Trace("arrays::collectModelInfo") << "TheoryArrays::collectModelInfo, adding RIntro2(c) read: " << r
<< endl
;
1129 r
= nm
->mkNode(kind::SELECT
, instore
[0], n
[1]);
1130 if (termSet
.find(r
) == termSet
.end() && d_equalityEngine
.hasTerm(r
)) {
1131 Trace("arrays::collectModelInfo") << "TheoryArrays::collectModelInfo, adding RIntro2(d) read: " << r
<< endl
;
1142 // Send the equality engine information to the model
1143 m
->assertEqualityEngine(&d_equalityEngine
, &termSet
);
1145 // Build a list of all the relevant reads, indexed by the store representative
1146 std::map
<Node
, std::vector
<Node
> > selects
;
1147 set
<Node
>::iterator set_it
= termSet
.begin(), set_it_end
= termSet
.end();
1148 for (; set_it
!= set_it_end
; ++set_it
) {
1150 // If this term is a select, record that the EC rep of its store parameter is being read from using this term
1151 if (n
.getKind() == kind::SELECT
) {
1152 selects
[d_equalityEngine
.getRepresentative(n
[0])].push_back(n
);
1157 DefValMap::iterator it
;
1158 TypeSet defaultValuesSet
;
1160 // Compute all default values already in use
1162 for (size_t i
=0; i
<arrays
.size(); ++i
) {
1163 TNode nrep
= d_equalityEngine
.getRepresentative(arrays
[i
]);
1164 d_mayEqualEqualityEngine
.addTerm(nrep
); // add the term in case it isn't there already
1165 TNode mayRep
= d_mayEqualEqualityEngine
.getRepresentative(nrep
);
1166 it
= d_defValues
.find(mayRep
);
1167 if (it
!= d_defValues
.end()) {
1168 defaultValuesSet
.add(nrep
.getType().getArrayConstituentType(), (*it
).second
);
1173 // Loop through all array equivalence classes that need a representative computed
1174 for (size_t i
=0; i
<arrays
.size(); ++i
) {
1175 TNode n
= arrays
[i
];
1176 TNode nrep
= d_equalityEngine
.getRepresentative(n
);
1179 // Compute default value for this array - there is one default value for every mayEqual equivalence class
1180 TNode mayRep
= d_mayEqualEqualityEngine
.getRepresentative(nrep
);
1181 it
= d_defValues
.find(mayRep
);
1182 // If this mayEqual EC doesn't have a default value associated, get the next available default value for the associated array element type
1183 if (it
== d_defValues
.end()) {
1184 TypeNode valueType
= nrep
.getType().getArrayConstituentType();
1185 rep
= defaultValuesSet
.nextTypeEnum(valueType
);
1187 Assert(defaultValuesSet
.getSet(valueType
)->begin() != defaultValuesSet
.getSet(valueType
)->end());
1188 rep
= *(defaultValuesSet
.getSet(valueType
)->begin());
1190 Trace("arrays-models") << "New default value = " << rep
<< endl
;
1191 d_defValues
[mayRep
] = rep
;
1197 // Build the STORE_ALL term with the default value
1198 rep
= nm
->mkConst(ArrayStoreAll(nrep
.getType().toType(), rep
.toExpr()));
1202 std::unordered_map<Node, Node, NodeHashFunction>::iterator it = d_skolemCache.find(n);
1203 if (it == d_skolemCache.end()) {
1204 rep = nm->mkSkolem("array_collect_model_var", n.getType(), "base model variable for array collectModelInfo");
1205 d_skolemCache[n] = rep;
1213 // For each read, require that the rep stores the right value
1214 vector
<Node
>& reads
= selects
[nrep
];
1215 for (unsigned j
= 0; j
< reads
.size(); ++j
) {
1216 rep
= nm
->mkNode(kind::STORE
, rep
, reads
[j
][1], reads
[j
]);
1218 m
->assertEquality(n
, rep
, true);
1220 m
->assertRepresentative(rep
);
1225 /////////////////////////////////////////////////////////////////////////////
1227 /////////////////////////////////////////////////////////////////////////////
1230 void TheoryArrays::presolve()
1232 Trace("arrays")<<"Presolving \n";
1236 /////////////////////////////////////////////////////////////////////////////
1238 /////////////////////////////////////////////////////////////////////////////
1241 Node
TheoryArrays::getSkolem(TNode ref
, const string
& name
, const TypeNode
& type
, const string
& comment
, bool makeEqual
)
1244 std::unordered_map
<Node
, Node
, NodeHashFunction
>::iterator it
= d_skolemCache
.find(ref
);
1245 if (it
== d_skolemCache
.end()) {
1246 NodeManager
* nm
= NodeManager::currentNM();
1247 skolem
= nm
->mkSkolem(name
, type
, comment
);
1248 d_skolemCache
[ref
] = skolem
;
1251 skolem
= (*it
).second
;
1252 if (d_equalityEngine
.hasTerm(ref
) &&
1253 d_equalityEngine
.hasTerm(skolem
) &&
1254 d_equalityEngine
.areEqual(ref
, skolem
)) {
1259 Debug("pf::array") << "Pregistering a Skolem" << std::endl
;
1260 preRegisterTermInternal(skolem
);
1261 Debug("pf::array") << "Pregistering a Skolem DONE" << std::endl
;
1264 Node d
= skolem
.eqNode(ref
);
1265 Debug("arrays-model-based") << "Asserting skolem equality " << d
<< endl
;
1266 d_equalityEngine
.assertEquality(d
, true, d_true
);
1267 Assert(!d_conflict
);
1268 d_skolemAssertions
.push_back(d
);
1269 d_skolemIndex
= d_skolemIndex
+ 1;
1272 Debug("pf::array") << "getSkolem DONE" << std::endl
;
1277 void TheoryArrays::check(Effort e
) {
1278 if (done() && !fullEffort(e
)) {
1282 getOutputChannel().spendResource(options::theoryCheckStep());
1284 TimerStat::CodeTimer
checkTimer(d_checkTime
);
1286 while (!done() && !d_conflict
)
1288 // Get all the assertions
1289 Assertion assertion
= get();
1290 TNode fact
= assertion
.assertion
;
1292 Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::check(): processing " << fact
<< std::endl
;
1294 bool polarity
= fact
.getKind() != kind::NOT
;
1295 TNode atom
= polarity
? fact
: fact
[0];
1297 if (!assertion
.isPreregistered
) {
1298 if (atom
.getKind() == kind::EQUAL
) {
1299 if (!d_equalityEngine
.hasTerm(atom
[0])) {
1300 Assert(atom
[0].isConst());
1301 d_equalityEngine
.addTerm(atom
[0]);
1303 if (!d_equalityEngine
.hasTerm(atom
[1])) {
1304 Assert(atom
[1].isConst());
1305 d_equalityEngine
.addTerm(atom
[1]);
1311 switch (fact
.getKind()) {
1313 d_equalityEngine
.assertEquality(fact
, true, fact
);
1316 d_equalityEngine
.assertPredicate(fact
, true, fact
);
1319 if (fact
[0].getKind() == kind::SELECT
) {
1320 d_equalityEngine
.assertPredicate(fact
[0], false, fact
);
1321 } else if (!d_equalityEngine
.areDisequal(fact
[0][0], fact
[0][1], false)) {
1322 // Assert the dis-equality
1323 d_equalityEngine
.assertEquality(fact
[0], false, fact
);
1325 // Apply ArrDiseq Rule if diseq is between arrays
1326 if(fact
[0][0].getType().isArray() && !d_conflict
) {
1327 if (d_conflict
) { Debug("pf::array") << "Entering the skolemization branch" << std::endl
; }
1329 NodeManager
* nm
= NodeManager::currentNM();
1330 TypeNode indexType
= fact
[0][0].getType()[0];
1333 // k is the skolem for this disequality.
1334 if (!d_proofsEnabled
) {
1335 Debug("pf::array") << "Check: kind::NOT: array theory making a skolem" << std::endl
;
1337 // If not in replay mode, generate a fresh skolem variable
1341 "an extensional lemma index variable from the theory of arrays",
1344 // Register this skolem for the proof replay phase
1345 PROOF(ProofManager::getSkolemizationManager()->registerSkolem(fact
, k
));
1347 if (!ProofManager::getSkolemizationManager()->hasSkolem(fact
)) {
1348 // In the solution pass we didn't need this skolem. Therefore, we don't need it
1349 // in this reply pass, either.
1353 // Reuse the same skolem as in the solution pass
1354 k
= ProofManager::getSkolemizationManager()->getSkolem(fact
);
1355 Debug("pf::array") << "Skolem = " << k
<< std::endl
;
1358 Node ak
= nm
->mkNode(kind::SELECT
, fact
[0][0], k
);
1359 Node bk
= nm
->mkNode(kind::SELECT
, fact
[0][1], k
);
1360 Node eq
= ak
.eqNode(bk
);
1361 Node lemma
= fact
[0].orNode(eq
.notNode());
1363 // In solve mode we don't care if ak and bk are registered. If they aren't, they'll be registered
1364 // when we output the lemma. However, in replay need the lemma to be propagated, and so we
1365 // preregister manually.
1366 if (d_proofsEnabled
) {
1367 if (!d_equalityEngine
.hasTerm(ak
)) { preRegisterTermInternal(ak
); }
1368 if (!d_equalityEngine
.hasTerm(bk
)) { preRegisterTermInternal(bk
); }
1371 if (options::arraysPropagate() > 0 && d_equalityEngine
.hasTerm(ak
) && d_equalityEngine
.hasTerm(bk
)) {
1372 // Propagate witness disequality - might produce a conflict
1373 d_permRef
.push_back(lemma
);
1374 Debug("pf::array") << "Asserting to the equality engine:" << std::endl
1375 << "\teq = " << eq
<< std::endl
1376 << "\treason = " << fact
<< std::endl
;
1378 d_equalityEngine
.assertEquality(eq
, false, fact
, d_reasonExt
);
1382 if (!d_proofsEnabled
) {
1383 // If this is the solution pass, generate the lemma. Otherwise, don't generate it -
1384 // as this is the lemma that we're reproving...
1385 Trace("arrays-lem")<<"Arrays::addExtLemma " << lemma
<<"\n";
1386 d_out
->lemma(lemma
);
1390 Debug("pf::array") << "Check: kind::NOT: array theory NOT making a skolem" << std::endl
;
1391 d_modelConstraints
.push_back(fact
);
1401 if ((options::arraysEagerLemmas() || fullEffort(e
)) && !d_conflict
&& options::arraysWeakEquivalence()) {
1402 // Replay all array merges to update weak equivalence data structures
1403 context::CDList
<Node
>::iterator it
= d_arrayMerges
.begin(), iend
= d_arrayMerges
.end();
1405 for (; it
!= iend
; ++it
) {
1409 weakEquivMakeRep(b
);
1410 if (weakEquivGetRep(a
) == b
) {
1411 weakEquivAddSecondary(TNode(), a
, b
, eq
);
1414 d_infoMap
.setWeakEquivPointer(b
, a
);
1415 d_infoMap
.setWeakEquivIndex(b
, TNode());
1417 #ifdef CVC4_ASSERTIONS
1418 checkWeakEquiv(false);
1421 #ifdef CVC4_ASSERTIONS
1422 checkWeakEquiv(true);
1425 d_readTableContext
->push();
1427 CTNodeList
* bucketList
= NULL
;
1428 CTNodeList::const_iterator i
= d_reads
.begin(), readsEnd
= d_reads
.end();
1429 for (; i
!= readsEnd
; ++i
) {
1430 const TNode
& r
= *i
;
1432 Debug("arrays::weak") << "TheoryArrays::check(): checking read " << r
<< std::endl
;
1434 // Find the bucket for this read.
1435 mayRep
= d_mayEqualEqualityEngine
.getRepresentative(r
[0]);
1436 iRep
= d_equalityEngine
.getRepresentative(r
[1]);
1437 std::pair
<TNode
, TNode
> key(mayRep
, iRep
);
1438 ReadBucketMap::iterator it
= d_readBucketTable
.find(key
);
1439 if (it
== d_readBucketTable
.end()) {
1440 bucketList
= new(true) CTNodeList(d_readTableContext
);
1441 d_readBucketAllocations
.push_back(bucketList
);
1442 d_readBucketTable
[key
] = bucketList
;
1445 bucketList
= it
->second
;
1447 CTNodeList::const_iterator it2
= bucketList
->begin(), iend
= bucketList
->end();
1448 for (; it2
!= iend
; ++it2
) {
1449 const TNode
& r2
= *it2
;
1450 Assert(r2
.getKind() == kind::SELECT
);
1451 Assert(mayRep
== d_mayEqualEqualityEngine
.getRepresentative(r2
[0]));
1452 Assert(iRep
== d_equalityEngine
.getRepresentative(r2
[1]));
1453 if (d_equalityEngine
.areEqual(r
, r2
)) {
1456 if (weakEquivGetRepIndex(r
[0], r
[1]) == weakEquivGetRepIndex(r2
[0], r
[1])) {
1457 // add lemma: r[1] = r2[1] /\ cond(r[0],r2[0]) => r = r2
1458 vector
<TNode
> conjunctions
;
1459 Assert(d_equalityEngine
.areEqual(r
, Rewriter::rewrite(r
)));
1460 Assert(d_equalityEngine
.areEqual(r2
, Rewriter::rewrite(r2
)));
1461 Node lemma
= Rewriter::rewrite(r
).eqNode(Rewriter::rewrite(r2
)).negate();
1462 d_permRef
.push_back(lemma
);
1463 conjunctions
.push_back(lemma
);
1464 if (r
[1] != r2
[1]) {
1465 d_equalityEngine
.explainEquality(r
[1], r2
[1], true, conjunctions
);
1467 // TODO: get smaller lemmas by eliminating shared parts of path
1468 weakEquivBuildCond(r
[0], r
[1], conjunctions
);
1469 weakEquivBuildCond(r2
[0], r
[1], conjunctions
);
1470 lemma
= mkAnd(conjunctions
, true);
1471 // LSH FIXME: which kind of arrays lemma is this
1472 Trace("arrays-lem") << "Arrays::addExtLemma " << lemma
<<"\n";
1473 d_out
->lemma(lemma
, RULE_INVALID
, false, false, true);
1474 d_readTableContext
->pop();
1475 Trace("arrays") << spaces(getSatContext()->getLevel()) << "Arrays::check(): done" << endl
;
1479 bucketList
->push_back(r
);
1481 d_readTableContext
->pop();
1484 if(!options::arraysEagerLemmas() && fullEffort(e
) && !d_conflict
&& !options::arraysWeakEquivalence()) {
1485 // generate the lemmas on the worklist
1486 Trace("arrays-lem")<< "Arrays::discharging lemmas. Number of queued lemmas: " << d_RowQueue
.size() << "\n";
1487 while (d_RowQueue
.size() > 0 && !d_conflict
) {
1488 if (dischargeLemmas()) {
1494 Trace("arrays") << spaces(getSatContext()->getLevel()) << "Arrays::check(): done" << endl
;
1498 Node
TheoryArrays::mkAnd(std::vector
<TNode
>& conjunctions
, bool invert
, unsigned startIndex
)
1500 Assert(conjunctions
.size() > 0);
1502 std::set
<TNode
> all
;
1503 std::set
<TNode
> explained
;
1505 unsigned i
= startIndex
;
1507 for (; i
< conjunctions
.size(); ++i
) {
1508 t
= conjunctions
[i
];
1512 else if (t
.getKind() == kind::AND
) {
1513 for(TNode::iterator child_it
= t
.begin(); child_it
!= t
.end(); ++child_it
) {
1514 if (*child_it
== d_true
) {
1517 all
.insert(*child_it
);
1520 else if (t
.getKind() == kind::OR
) {
1521 // Expand explanation resulting from propagating a ROW or EXT lemma
1522 if ((explained
.find(t
) == explained
.end())) {
1523 if (t
[1].getKind() == kind::EQUAL
) {
1525 d_equalityEngine
.explainEquality(t
[1][0], t
[1][1], false, conjunctions
);
1526 explained
.insert(t
);
1529 Assert(t
[1].getKind() == kind::NOT
&& t
[1][0].getKind() == kind::EQUAL
);
1530 Assert(t
[0].getKind() == kind::EQUAL
);
1531 all
.insert(t
[0].notNode());
1532 explained
.insert(t
);
1541 if (all
.size() == 0) {
1542 return invert
? d_false
: d_true
;
1544 if (all
.size() == 1) {
1545 // All the same, or just one
1547 return (*(all
.begin())).negate();
1550 return *(all
.begin());
1554 NodeBuilder
<> conjunction(invert
? kind::OR
: kind::AND
);
1555 std::set
<TNode
>::const_iterator it
= all
.begin();
1556 std::set
<TNode
>::const_iterator it_end
= all
.end();
1557 while (it
!= it_end
) {
1559 conjunction
<< (*it
).negate();
1571 void TheoryArrays::setNonLinear(TNode a
)
1573 if (options::arraysWeakEquivalence()) return;
1574 if (d_infoMap
.isNonLinear(a
)) return;
1576 Trace("arrays") << spaces(getSatContext()->getLevel()) << "Arrays::setNonLinear (" << a
<< ")\n";
1577 d_infoMap
.setNonLinear(a
);
1580 const CTNodeList
* i_a
= d_infoMap
.getIndices(a
);
1581 const CTNodeList
* st_a
= d_infoMap
.getStores(a
);
1582 const CTNodeList
* inst_a
= d_infoMap
.getInStores(a
);
1586 // Propagate non-linearity down chain of stores
1587 for( ; it
< st_a
->size(); ++it
) {
1588 TNode store
= (*st_a
)[it
];
1589 Assert(store
.getKind()==kind::STORE
);
1590 setNonLinear(store
[0]);
1593 // Instantiate ROW lemmas that were ignored before
1596 for(; it2
< i_a
->size(); ++it2
) {
1597 TNode i
= (*i_a
)[it2
];
1599 for ( ; it
< inst_a
->size(); ++it
) {
1600 TNode store
= (*inst_a
)[it
];
1601 Assert(store
.getKind() == kind::STORE
);
1604 lem
= make_quad(store
, c
, j
, i
);
1605 Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::setNonLinear ("<<store
<<", "<<c
<<", "<<j
<<", "<<i
<<")\n";
1613 * When two array equivalence classes are merged, we may need to apply RIntro1 to a store in one of the EC's
1614 * Here, we check the stores in a to see if any need RIntro1 applied
1615 * We apply RIntro1 whenever:
1616 * (a) a store becomes equal to another store
1617 * (b) a store becomes equal to any term t such that read(t,i) exists
1618 * (c) a store becomes equal to the root array of the store (i.e. store(store(...store(a,i,v)...)) = a)
1620 void TheoryArrays::checkRIntro1(TNode a
, TNode b
)
1622 const CTNodeList
* astores
= d_infoMap
.getStores(a
);
1623 // Apply RIntro1 if applicable
1624 CTNodeList::const_iterator it
= astores
->begin();
1626 if (it
== astores
->end()) {
1627 // No stores in this equivalence class - return
1632 if (it
!= astores
->end()) {
1633 // More than one store: should have already been applied
1634 Assert(d_infoMap
.rIntro1Applied(*it
));
1635 Assert(d_infoMap
.rIntro1Applied(*(--it
)));
1639 // Exactly one store - see if we need to apply RIntro1
1642 Assert(s
.getKind() == kind::STORE
);
1643 if (d_infoMap
.rIntro1Applied(s
)) {
1644 // RIntro1 already applied to s
1648 // Should be no reads from this EC
1649 Assert(d_infoMap
.getIndices(a
)->begin() == d_infoMap
.getIndices(a
)->end());
1652 if (d_infoMap
.getStores(b
)->size() > 0) {
1653 // Case (a): two stores become equal
1657 const CTNodeList
* i_b
= d_infoMap
.getIndices(b
);
1658 if (i_b
->begin() != i_b
->end()) {
1659 // Case (b): there are reads from b
1663 // Get root array of s
1665 while (e1
.getKind() == kind::STORE
) {
1668 Assert(d_equalityEngine
.hasTerm(e1
));
1669 Assert(d_equalityEngine
.hasTerm(b
));
1670 if (d_equalityEngine
.areEqual(e1
, b
)) {
1677 NodeManager
* nm
= NodeManager::currentNM();
1678 d_infoMap
.setRIntro1Applied(s
);
1679 Node ni
= nm
->mkNode(kind::SELECT
, s
, s
[1]);
1680 preRegisterTermInternal(ni
);
1681 d_equalityEngine
.assertEquality(ni
.eqNode(s
[2]), true, d_true
, d_reasonRow1
);
1688 void TheoryArrays::mergeArrays(TNode a
, TNode b
)
1690 // Note: a is the new representative
1691 Assert(a
.getType().isArray() && b
.getType().isArray());
1693 if (d_mergeInProgress
) {
1694 // Nested call to mergeArrays, just push on the queue and return
1695 d_mergeQueue
.push(a
.eqNode(b
));
1699 d_mergeInProgress
= true;
1703 // Normally, a is its own representative, but it's possible for a to have
1704 // been merged with another array after it got queued up by the equality engine,
1705 // so we take its representative to be safe.
1706 a
= d_equalityEngine
.getRepresentative(a
);
1707 Assert(d_equalityEngine
.getRepresentative(b
) == a
);
1708 Trace("arrays-merge") << spaces(getSatContext()->getLevel()) << "Arrays::merge: (" << a
<< ", " << b
<< ")\n";
1710 if (options::arraysLazyRIntro1() && !options::arraysWeakEquivalence()) {
1715 if (options::arraysOptimizeLinear() && !options::arraysWeakEquivalence()) {
1716 bool aNL
= d_infoMap
.isNonLinear(a
);
1717 bool bNL
= d_infoMap
.isNonLinear(b
);
1720 // already both marked as non-linear - no need to do anything
1723 // Set b to be non-linear
1729 // Set a to be non-linear
1733 // Check for new non-linear arrays
1734 const CTNodeList
* astores
= d_infoMap
.getStores(a
);
1735 const CTNodeList
* bstores
= d_infoMap
.getStores(b
);
1736 Assert(astores
->size() <= 1 && bstores
->size() <= 1);
1737 if (astores
->size() > 0 && bstores
->size() > 0) {
1745 TNode constArrA
= d_infoMap
.getConstArr(a
);
1746 TNode constArrB
= d_infoMap
.getConstArr(b
);
1747 if (constArrA
.isNull()) {
1748 if (!constArrB
.isNull()) {
1749 d_infoMap
.setConstArr(a
,constArrB
);
1752 else if (!constArrB
.isNull()) {
1753 if (constArrA
!= constArrB
) {
1754 conflict(constArrA
,constArrB
);
1758 TNode mayRepA
= d_mayEqualEqualityEngine
.getRepresentative(a
);
1759 TNode mayRepB
= d_mayEqualEqualityEngine
.getRepresentative(b
);
1761 // If a and b have different default values associated with their mayequal equivalence classes,
1762 // things get complicated. Similarly, if two mayequal equivalence classes have different
1763 // constant representatives, it's not clear what to do. - disallow these cases for now. -Clark
1764 DefValMap::iterator it
= d_defValues
.find(mayRepA
);
1765 DefValMap::iterator it2
= d_defValues
.find(mayRepB
);
1768 if (it
!= d_defValues
.end()) {
1769 defValue
= (*it
).second
;
1770 if ((it2
!= d_defValues
.end() && (defValue
!= (*it2
).second
)) ||
1771 (mayRepA
.isConst() && mayRepB
.isConst() && mayRepA
!= mayRepB
)) {
1772 throw LogicException("Array theory solver does not yet support write-chains connecting two different constant arrays");
1775 else if (it2
!= d_defValues
.end()) {
1776 defValue
= (*it2
).second
;
1778 d_mayEqualEqualityEngine
.assertEquality(a
.eqNode(b
), true, d_true
);
1779 Assert(d_mayEqualEqualityEngine
.consistent());
1780 if (!defValue
.isNull()) {
1781 mayRepA
= d_mayEqualEqualityEngine
.getRepresentative(a
);
1782 d_defValues
[mayRepA
] = defValue
;
1785 checkRowLemmas(a
,b
);
1786 checkRowLemmas(b
,a
);
1788 // merge info adds the list of the 2nd argument to the first
1789 d_infoMap
.mergeInfo(a
, b
);
1791 if (options::arraysWeakEquivalence()) {
1792 d_arrayMerges
.push_back(a
.eqNode(b
));
1795 // If no more to do, break
1796 if (d_conflict
|| d_mergeQueue
.empty()) {
1800 // Otherwise, prepare for next iteration
1801 n
= d_mergeQueue
.front();
1806 d_mergeInProgress
= false;
1810 void TheoryArrays::checkStore(TNode a
) {
1811 if (options::arraysWeakEquivalence()) return;
1812 Trace("arrays-cri")<<"Arrays::checkStore "<<a
<<"\n";
1814 if(Trace
.isOn("arrays-cri")) {
1815 d_infoMap
.getInfo(a
)->print();
1817 Assert(a
.getType().isArray());
1818 Assert(a
.getKind()==kind::STORE
);
1822 TNode brep
= d_equalityEngine
.getRepresentative(b
);
1824 if (!options::arraysOptimizeLinear() || d_infoMap
.isNonLinear(brep
)) {
1825 const CTNodeList
* js
= d_infoMap
.getIndices(brep
);
1828 for(; it
< js
->size(); ++it
) {
1829 TNode j
= (*js
)[it
];
1830 if (i
== j
) continue;
1831 lem
= make_quad(a
,b
,i
,j
);
1832 Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::checkStore ("<<a
<<", "<<b
<<", "<<i
<<", "<<j
<<")\n";
1839 void TheoryArrays::checkRowForIndex(TNode i
, TNode a
)
1841 if (options::arraysWeakEquivalence()) return;
1842 Trace("arrays-cri")<<"Arrays::checkRowForIndex "<<a
<<"\n";
1843 Trace("arrays-cri")<<" index "<<i
<<"\n";
1845 if(Trace
.isOn("arrays-cri")) {
1846 d_infoMap
.getInfo(a
)->print();
1848 Assert(a
.getType().isArray());
1849 Assert(d_equalityEngine
.getRepresentative(a
) == a
);
1851 TNode constArr
= d_infoMap
.getConstArr(a
);
1852 if (!constArr
.isNull()) {
1853 ArrayStoreAll storeAll
= constArr
.getConst
<ArrayStoreAll
>();
1854 Node defValue
= Node::fromExpr(storeAll
.getExpr());
1855 Node selConst
= NodeManager::currentNM()->mkNode(kind::SELECT
, constArr
, i
);
1856 if (!d_equalityEngine
.hasTerm(selConst
)) {
1857 preRegisterTermInternal(selConst
);
1859 d_equalityEngine
.assertEquality(selConst
.eqNode(defValue
), true, d_true
);
1862 const CTNodeList
* stores
= d_infoMap
.getStores(a
);
1863 const CTNodeList
* instores
= d_infoMap
.getInStores(a
);
1867 for(; it
< stores
->size(); ++it
) {
1868 TNode store
= (*stores
)[it
];
1869 Assert(store
.getKind()==kind::STORE
);
1871 if (i
== j
) continue;
1872 lem
= make_quad(store
, store
[0], j
, i
);
1873 Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::checkRowForIndex ("<<store
<<", "<<store
[0]<<", "<<j
<<", "<<i
<<")\n";
1877 if (!options::arraysOptimizeLinear() || d_infoMap
.isNonLinear(a
)) {
1879 for(; it
< instores
->size(); ++it
) {
1880 TNode instore
= (*instores
)[it
];
1881 Assert(instore
.getKind()==kind::STORE
);
1882 TNode j
= instore
[1];
1883 if (i
== j
) continue;
1884 lem
= make_quad(instore
, instore
[0], j
, i
);
1885 Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::checkRowForIndex ("<<instore
<<", "<<instore
[0]<<", "<<j
<<", "<<i
<<")\n";
1892 // a just became equal to b
1893 // look for new ROW lemmas
1894 void TheoryArrays::checkRowLemmas(TNode a
, TNode b
)
1896 if (options::arraysWeakEquivalence()) return;
1897 Trace("arrays-crl")<<"Arrays::checkLemmas begin \n"<<a
<<"\n";
1898 if(Trace
.isOn("arrays-crl"))
1899 d_infoMap
.getInfo(a
)->print();
1900 Trace("arrays-crl")<<" ------------ and "<<b
<<"\n";
1901 if(Trace
.isOn("arrays-crl"))
1902 d_infoMap
.getInfo(b
)->print();
1904 const CTNodeList
* i_a
= d_infoMap
.getIndices(a
);
1906 TNode constArr
= d_infoMap
.getConstArr(b
);
1907 if (!constArr
.isNull()) {
1908 for( ; it
< i_a
->size(); ++it
) {
1909 TNode i
= (*i_a
)[it
];
1910 Node selConst
= NodeManager::currentNM()->mkNode(kind::SELECT
, constArr
, i
);
1911 if (!d_equalityEngine
.hasTerm(selConst
)) {
1912 preRegisterTermInternal(selConst
);
1917 const CTNodeList
* st_b
= d_infoMap
.getStores(b
);
1918 const CTNodeList
* inst_b
= d_infoMap
.getInStores(b
);
1923 for(it
= 0 ; it
< i_a
->size(); ++it
) {
1924 TNode i
= (*i_a
)[it
];
1926 for ( ; its
< st_b
->size(); ++its
) {
1927 TNode store
= (*st_b
)[its
];
1928 Assert(store
.getKind() == kind::STORE
);
1931 lem
= make_quad(store
, c
, j
, i
);
1932 Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::checkRowLemmas ("<<store
<<", "<<c
<<", "<<j
<<", "<<i
<<")\n";
1937 if (!options::arraysOptimizeLinear() || d_infoMap
.isNonLinear(b
)) {
1938 for(it
= 0 ; it
< i_a
->size(); ++it
) {
1939 TNode i
= (*i_a
)[it
];
1941 for ( ; its
< inst_b
->size(); ++its
) {
1942 TNode store
= (*inst_b
)[its
];
1943 Assert(store
.getKind() == kind::STORE
);
1946 lem
= make_quad(store
, c
, j
, i
);
1947 Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::checkRowLemmas ("<<store
<<", "<<c
<<", "<<j
<<", "<<i
<<")\n";
1952 Trace("arrays-crl")<<"Arrays::checkLemmas done.\n";
1955 void TheoryArrays::propagate(RowLemmaType lem
)
1957 Debug("pf::array") << "TheoryArrays: RowLemma Propagate called. options::arraysPropagate() = "
1958 << options::arraysPropagate() << std::endl
;
1960 TNode a
= lem
.first
;
1961 TNode b
= lem
.second
;
1962 TNode i
= lem
.third
;
1963 TNode j
= lem
.fourth
;
1965 Assert(a
.getType().isArray() && b
.getType().isArray());
1966 if (d_equalityEngine
.areEqual(a
,b
) ||
1967 d_equalityEngine
.areEqual(i
,j
)) {
1971 NodeManager
* nm
= NodeManager::currentNM();
1972 Node aj
= nm
->mkNode(kind::SELECT
, a
, j
);
1973 Node bj
= nm
->mkNode(kind::SELECT
, b
, j
);
1975 // Try to avoid introducing new read terms: track whether these already exist
1976 bool ajExists
= d_equalityEngine
.hasTerm(aj
);
1977 bool bjExists
= d_equalityEngine
.hasTerm(bj
);
1978 bool bothExist
= ajExists
&& bjExists
;
1980 // If propagating, check propagations
1981 int prop
= options::arraysPropagate();
1983 if (d_equalityEngine
.areDisequal(i
,j
,true) && (bothExist
|| prop
> 1)) {
1984 Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::queueRowLemma: propagating aj = bj ("<<aj
<<", "<<bj
<<")\n";
1985 Node aj_eq_bj
= aj
.eqNode(bj
);
1986 Node i_eq_j
= i
.eqNode(j
);
1987 Node reason
= nm
->mkNode(kind::OR
, aj_eq_bj
, i_eq_j
);
1988 d_permRef
.push_back(reason
);
1990 preRegisterTermInternal(aj
);
1993 preRegisterTermInternal(bj
);
1995 d_equalityEngine
.assertEquality(aj_eq_bj
, true, reason
, d_reasonRow
);
1999 if (bothExist
&& d_equalityEngine
.areDisequal(aj
,bj
,true)) {
2000 Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::queueRowLemma: propagating i = j ("<<i
<<", "<<j
<<")\n";
2001 Node aj_eq_bj
= aj
.eqNode(bj
);
2002 Node i_eq_j
= i
.eqNode(j
);
2003 Node reason
= nm
->mkNode(kind::OR
, i_eq_j
, aj_eq_bj
);
2004 d_permRef
.push_back(reason
);
2005 d_equalityEngine
.assertEquality(i_eq_j
, true, reason
, d_reasonRow
);
2012 void TheoryArrays::queueRowLemma(RowLemmaType lem
)
2014 Debug("pf::array") << "Array solver: queue row lemma called" << std::endl
;
2016 if (d_conflict
|| d_RowAlreadyAdded
.contains(lem
)) {
2019 TNode a
= lem
.first
;
2020 TNode b
= lem
.second
;
2021 TNode i
= lem
.third
;
2022 TNode j
= lem
.fourth
;
2024 Assert(a
.getType().isArray() && b
.getType().isArray());
2025 if (d_equalityEngine
.areEqual(a
,b
) ||
2026 d_equalityEngine
.areEqual(i
,j
)) {
2030 NodeManager
* nm
= NodeManager::currentNM();
2031 Node aj
= nm
->mkNode(kind::SELECT
, a
, j
);
2032 Node bj
= nm
->mkNode(kind::SELECT
, b
, j
);
2034 // Try to avoid introducing new read terms: track whether these already exist
2035 bool ajExists
= d_equalityEngine
.hasTerm(aj
);
2036 bool bjExists
= d_equalityEngine
.hasTerm(bj
);
2037 bool bothExist
= ajExists
&& bjExists
;
2039 // If propagating, check propagations
2040 int prop
= options::arraysPropagate();
2045 // If equivalent lemma already exists, don't enqueue this one
2046 if (d_useArrTable
) {
2047 Node tableEntry
= NodeManager::currentNM()->mkNode(kind::ARR_TABLE_FUN
, a
, b
, i
, j
);
2048 if (d_equalityEngine
.getSize(tableEntry
) != 1) {
2053 // Prefer equality between indexes so as not to introduce new read terms
2054 if (options::arraysEagerIndexSplitting() && !bothExist
&& !d_equalityEngine
.areDisequal(i
,j
, false)) {
2056 if (!d_proofsEnabled
) {
2057 i_eq_j
= d_valuation
.ensureLiteral(i
.eqNode(j
)); // TODO: think about this
2059 i_eq_j
= i
.eqNode(j
);
2062 getOutputChannel().requirePhase(i_eq_j
, true);
2063 d_decisionRequests
.push(i_eq_j
);
2066 // TODO: maybe add triggers here
2068 if ((options::arraysEagerLemmas() || bothExist
) && !d_proofsEnabled
) {
2069 // Make sure that any terms introduced by rewriting are appropriately stored in the equality database
2070 Node aj2
= Rewriter::rewrite(aj
);
2073 preRegisterTermInternal(aj
);
2075 if (!d_equalityEngine
.hasTerm(aj2
)) {
2076 preRegisterTermInternal(aj2
);
2078 d_equalityEngine
.assertEquality(aj
.eqNode(aj2
), true, d_true
);
2080 Node bj2
= Rewriter::rewrite(bj
);
2083 preRegisterTermInternal(bj
);
2085 if (!d_equalityEngine
.hasTerm(bj2
)) {
2086 preRegisterTermInternal(bj2
);
2088 d_equalityEngine
.assertEquality(bj
.eqNode(bj2
), true, d_true
);
2095 Node eq1
= aj2
.eqNode(bj2
);
2096 Node eq1_r
= Rewriter::rewrite(eq1
);
2097 if (eq1_r
== d_true
) {
2098 if (!d_equalityEngine
.hasTerm(aj2
)) {
2099 preRegisterTermInternal(aj2
);
2101 if (!d_equalityEngine
.hasTerm(bj2
)) {
2102 preRegisterTermInternal(bj2
);
2104 d_equalityEngine
.assertEquality(eq1
, true, d_true
);
2108 Node eq2
= i
.eqNode(j
);
2109 Node eq2_r
= Rewriter::rewrite(eq2
);
2110 if (eq2_r
== d_true
) {
2111 d_equalityEngine
.assertEquality(eq2
, true, d_true
);
2115 Node lemma
= nm
->mkNode(kind::OR
, eq2_r
, eq1_r
);
2117 Trace("arrays-lem")<<"Arrays::addRowLemma adding "<<lemma
<<"\n";
2118 d_RowAlreadyAdded
.insert(lem
);
2119 d_out
->lemma(lemma
);
2123 d_RowQueue
.push(lem
);
2128 Node
TheoryArrays::getNextDecisionRequest( unsigned& priority
) {
2129 if(! d_decisionRequests
.empty()) {
2130 Node n
= d_decisionRequests
.front();
2131 d_decisionRequests
.pop();
2135 return Node::null();
2140 bool TheoryArrays::dischargeLemmas()
2142 bool lemmasAdded
= false;
2143 size_t sz
= d_RowQueue
.size();
2144 for (unsigned count
= 0; count
< sz
; ++count
) {
2145 RowLemmaType l
= d_RowQueue
.front();
2147 if (d_RowAlreadyAdded
.contains(l
)) {
2155 Assert(a
.getType().isArray() && b
.getType().isArray());
2157 NodeManager
* nm
= NodeManager::currentNM();
2158 Node aj
= nm
->mkNode(kind::SELECT
, a
, j
);
2159 Node bj
= nm
->mkNode(kind::SELECT
, b
, j
);
2160 bool ajExists
= d_equalityEngine
.hasTerm(aj
);
2161 bool bjExists
= d_equalityEngine
.hasTerm(bj
);
2163 // Check for redundant lemma
2164 // TODO: more checks possible (i.e. check d_RowAlreadyAdded in context)
2165 if (!d_equalityEngine
.hasTerm(i
) || !d_equalityEngine
.hasTerm(j
) || d_equalityEngine
.areEqual(i
,j
) ||
2166 !d_equalityEngine
.hasTerm(a
) || !d_equalityEngine
.hasTerm(b
) || d_equalityEngine
.areEqual(a
,b
) ||
2167 (ajExists
&& bjExists
&& d_equalityEngine
.areEqual(aj
,bj
))) {
2171 int prop
= options::arraysPropagate();
2179 // Make sure that any terms introduced by rewriting are appropriately stored in the equality database
2180 Node aj2
= Rewriter::rewrite(aj
);
2183 preRegisterTermInternal(aj
);
2185 if (!d_equalityEngine
.hasTerm(aj2
)) {
2186 preRegisterTermInternal(aj2
);
2188 d_equalityEngine
.assertEquality(aj
.eqNode(aj2
), true, d_true
);
2190 Node bj2
= Rewriter::rewrite(bj
);
2193 preRegisterTermInternal(bj
);
2195 if (!d_equalityEngine
.hasTerm(bj2
)) {
2196 preRegisterTermInternal(bj2
);
2198 d_equalityEngine
.assertEquality(bj
.eqNode(bj2
), true, d_true
);
2206 Node eq1
= aj2
.eqNode(bj2
);
2207 Node eq1_r
= Rewriter::rewrite(eq1
);
2208 if (eq1_r
== d_true
) {
2209 if (!d_equalityEngine
.hasTerm(aj2
)) {
2210 preRegisterTermInternal(aj2
);
2212 if (!d_equalityEngine
.hasTerm(bj2
)) {
2213 preRegisterTermInternal(bj2
);
2215 d_equalityEngine
.assertEquality(eq1
, true, d_true
);
2219 Node eq2
= i
.eqNode(j
);
2220 Node eq2_r
= Rewriter::rewrite(eq2
);
2221 if (eq2_r
== d_true
) {
2222 d_equalityEngine
.assertEquality(eq2
, true, d_true
);
2226 Node lem
= nm
->mkNode(kind::OR
, eq2_r
, eq1_r
);
2228 Trace("arrays-lem")<<"Arrays::addRowLemma adding "<<lem
<<"\n";
2229 d_RowAlreadyAdded
.insert(l
);
2233 if (options::arraysReduceSharing()) {
2240 void TheoryArrays::conflict(TNode a
, TNode b
) {
2241 Debug("pf::array") << "TheoryArrays::Conflict called" << std::endl
;
2242 std::shared_ptr
<eq::EqProof
> proof
= d_proofsEnabled
?
2243 std::make_shared
<eq::EqProof
>() : nullptr;
2245 d_conflictNode
= explain(a
.eqNode(b
), proof
.get());
2247 if (!d_inCheckModel
) {
2248 ProofArray
* proof_array
= NULL
;
2250 if (d_proofsEnabled
) {
2251 proof
->debug_print("pf::array");
2252 proof_array
= new ProofArray(proof
, /*row=*/d_reasonRow
,
2253 /*row1=*/d_reasonRow1
, /*ext=*/d_reasonExt
);
2256 d_out
->conflict(d_conflictNode
, proof_array
);
2262 }/* CVC4::theory::arrays namespace */
2263 }/* CVC4::theory namespace */
2264 }/* CVC4 namespace */