1 /********************* */
2 /*! \file theory_arrays.h
4 ** Top contributors (to current version):
5 ** Morgan Deters, Clark Barrett, Tim King
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2018 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 Theory of arrays
17 #include "cvc4_private.h"
19 #ifndef __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_H
20 #define __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_H
23 #include <unordered_map>
25 #include "context/cdhashmap.h"
26 #include "context/cdhashset.h"
27 #include "context/cdqueue.h"
28 #include "theory/arrays/array_info.h"
29 #include "theory/arrays/array_proof_reconstruction.h"
30 #include "theory/theory.h"
31 #include "theory/uf/equality_engine.h"
32 #include "util/statistics_registry.h"
39 * Decision procedure for arrays.
41 * Overview of decision procedure:
43 * Preliminary notation:
44 * Stores(a) = {t | a ~ t and t = store( _ _ _ )}
45 * InStores(a) = {t | t = store (b _ _) and a ~ b }
46 * Indices(a) = {i | there exists a term b[i] such that a ~ b or store(b i v)}
47 * ~ represents the equivalence relation based on the asserted equalities in the
50 * The rules implemented are the following:
52 * Row1 -------------------
56 * Row ---------------------- [ a' ~ store(b i v) or a' ~ b ]
57 * i = j OR a[j] = b[j]
59 * a b same kind arrays
60 * Ext ------------------------ [ a!= b in current context, k new var]
61 * a = b OR a[k] != b[k]p
64 * The Row1 one rule is implemented implicitly as follows:
65 * - for each store(b i v) term add the following equality to the congruence
66 * closure store(b i v)[i] = v
67 * - if one of the literals in a conflict is of the form store(b i v)[i] = v
68 * remove it from the conflict
70 * Because new store terms are not created, we need to check if we need to
71 * instantiate a new Row axiom in the following cases:
72 * 1. the congruence relation changes (i.e. two terms get merged)
73 * - when a new equality between array terms a = b is asserted we check if
74 * we can instantiate a Row lemma for all pairs of indices i where a is
75 * being read and stores
76 * - this is only done during full effort check
77 * 2. a new read term is created either as a consequences of an Ext lemma or a
79 * - this is implemented in the checkRowForIndex method which is called
80 * when preregistering a term of the form a[i].
81 * - as a consequence lemmas are instantiated even before full effort check
83 * The Ext axiom is instantiated when a disequality is asserted during full effort
84 * check. Ext lemmas are stored in a cache to prevent instantiating essentially
85 * the same lemma multiple times.
88 static inline std::string
spaces(int level
)
90 std::string
indentStr(level
, ' ');
94 class TheoryArrays
: public Theory
{
96 /////////////////////////////////////////////////////////////////////////////
98 /////////////////////////////////////////////////////////////////////////////
102 /** True node for predicates = true */
105 /** True node for predicates = false */
110 /** number of Row lemmas */
112 /** number of Ext lemmas */
114 /** number of propagations */
116 /** number of explanations */
117 IntStat d_numExplain
;
118 /** calls to non-linear */
119 IntStat d_numNonLinear
;
120 /** splits on array variables */
121 IntStat d_numSharedArrayVarSplits
;
122 /** splits in getModelVal */
123 IntStat d_numGetModelValSplits
;
124 /** conflicts in getModelVal */
125 IntStat d_numGetModelValConflicts
;
126 /** splits in setModelVal */
127 IntStat d_numSetModelValSplits
;
128 /** conflicts in setModelVal */
129 IntStat d_numSetModelValConflicts
;
131 // Merge reason types
133 /** Merge tag for ROW applications */
134 unsigned d_reasonRow
;
135 /** Merge tag for ROW1 applications */
136 unsigned d_reasonRow1
;
137 /** Merge tag for EXT applications */
138 unsigned d_reasonExt
;
142 TheoryArrays(context::Context
* c
, context::UserContext
* u
, OutputChannel
& out
,
143 Valuation valuation
, const LogicInfo
& logicInfo
,
144 std::string name
= "");
147 void setMasterEqualityEngine(eq::EqualityEngine
* eq
) override
;
149 std::string
identify() const override
{ return std::string("TheoryArrays"); }
151 /////////////////////////////////////////////////////////////////////////////
153 /////////////////////////////////////////////////////////////////////////////
157 // PPNotifyClass: dummy template class for d_ppEqualityEngine - notifications not used
158 class PPNotifyClass
{
160 bool notify(TNode propagation
) { return true; }
161 void notify(TNode t1
, TNode t2
) { }
164 /** The notify class for d_ppEqualityEngine */
165 PPNotifyClass d_ppNotify
;
167 /** Equaltity engine */
168 eq::EqualityEngine d_ppEqualityEngine
;
170 // List of facts learned by preprocessor - needed for permanent ref for benefit of d_ppEqualityEngine
171 context::CDList
<Node
> d_ppFacts
;
173 Node
preprocessTerm(TNode term
);
174 Node
recursivePreprocessTerm(TNode term
);
175 bool ppDisequal(TNode a
, TNode b
);
176 Node
solveWrite(TNode term
, bool solve1
, bool solve2
, bool ppCheck
);
179 PPAssertStatus
ppAssert(TNode in
, SubstitutionMap
& outSubstitutions
) override
;
180 Node
ppRewrite(TNode atom
) override
;
182 /////////////////////////////////////////////////////////////////////////////
183 // T-PROPAGATION / REGISTRATION
184 /////////////////////////////////////////////////////////////////////////////
187 /** Literals to propagate */
188 context::CDList
<Node
> d_literalsToPropagate
;
190 /** Index of the next literal to propagate */
191 context::CDO
<unsigned> d_literalsToPropagateIndex
;
193 /** Should be called to propagate the literal. */
194 bool propagate(TNode literal
);
196 /** Explain why this literal is true by adding assumptions */
197 void explain(TNode literal
, std::vector
<TNode
>& assumptions
,
200 /** For debugging only- checks invariants about when things are preregistered*/
201 context::CDHashSet
<Node
, NodeHashFunction
> d_isPreRegistered
;
203 /** Helper for preRegisterTerm, also used internally */
204 void preRegisterTermInternal(TNode n
);
207 void preRegisterTerm(TNode n
) override
;
208 void propagate(Effort e
) override
;
209 Node
explain(TNode n
, eq::EqProof
* proof
);
210 Node
explain(TNode n
) override
;
212 /////////////////////////////////////////////////////////////////////////////
214 /////////////////////////////////////////////////////////////////////////////
217 class MayEqualNotifyClass
{
219 bool notify(TNode propagation
) { return true; }
220 void notify(TNode t1
, TNode t2
) { }
223 /** The notify class for d_mayEqualEqualityEngine */
224 MayEqualNotifyClass d_mayEqualNotify
;
226 /** Equaltity engine for determining if two arrays might be equal */
227 eq::EqualityEngine d_mayEqualEqualityEngine
;
229 // Helper for computeCareGraph
230 void checkPair(TNode r1
, TNode r2
);
233 void addSharedTerm(TNode t
) override
;
234 EqualityStatus
getEqualityStatus(TNode a
, TNode b
) override
;
235 void computeCareGraph() override
;
236 bool isShared(TNode t
)
238 return (d_sharedArrays
.find(t
) != d_sharedArrays
.end());
241 /////////////////////////////////////////////////////////////////////////////
243 /////////////////////////////////////////////////////////////////////////////
246 bool collectModelInfo(TheoryModel
* m
) override
;
248 /////////////////////////////////////////////////////////////////////////////
250 /////////////////////////////////////////////////////////////////////////////
253 Node
getNextDecisionRequest(unsigned& priority
) override
;
255 void presolve() override
;
256 void shutdown() override
{}
258 /////////////////////////////////////////////////////////////////////////////
260 /////////////////////////////////////////////////////////////////////////////
263 void check(Effort e
) override
;
266 TNode
weakEquivGetRep(TNode node
);
267 TNode
weakEquivGetRepIndex(TNode node
, TNode index
);
268 void visitAllLeaves(TNode reason
, std::vector
<TNode
>& conjunctions
);
269 void weakEquivBuildCond(TNode node
, TNode index
, std::vector
<TNode
>& conjunctions
);
270 void weakEquivMakeRep(TNode node
);
271 void weakEquivMakeRepIndex(TNode node
);
272 void weakEquivAddSecondary(TNode index
, TNode arrayFrom
, TNode arrayTo
, TNode reason
);
273 void checkWeakEquiv(bool arraysMerged
);
275 // NotifyClass: template helper class for d_equalityEngine - handles call-back from congruence closure module
276 class NotifyClass
: public eq::EqualityEngineNotify
{
277 TheoryArrays
& d_arrays
;
279 NotifyClass(TheoryArrays
& arrays
): d_arrays(arrays
) {}
281 bool eqNotifyTriggerEquality(TNode equality
, bool value
) override
283 Debug("arrays::propagate") << spaces(d_arrays
.getSatContext()->getLevel()) << "NotifyClass::eqNotifyTriggerEquality(" << equality
<< ", " << (value
? "true" : "false") << ")" << std::endl
;
284 // Just forward to arrays
286 return d_arrays
.propagate(equality
);
288 return d_arrays
.propagate(equality
.notNode());
292 bool eqNotifyTriggerPredicate(TNode predicate
, bool value
) override
294 Debug("arrays::propagate") << spaces(d_arrays
.getSatContext()->getLevel()) << "NotifyClass::eqNotifyTriggerEquality(" << predicate
<< ", " << (value
? "true" : "false") << ")" << std::endl
;
295 // Just forward to arrays
297 return d_arrays
.propagate(predicate
);
299 return d_arrays
.propagate(predicate
.notNode());
303 bool eqNotifyTriggerTermEquality(TheoryId tag
,
308 Debug("arrays::propagate") << spaces(d_arrays
.getSatContext()->getLevel()) << "NotifyClass::eqNotifyTriggerTermEquality(" << t1
<< ", " << t2
<< ", " << (value
? "true" : "false") << ")" << std::endl
;
310 if (t1
.getType().isArray()) {
311 if (!d_arrays
.isShared(t1
) || !d_arrays
.isShared(t2
)) {
315 // Propagate equality between shared terms
316 return d_arrays
.propagate(t1
.eqNode(t2
));
318 if (t1
.getType().isArray()) {
319 if (!d_arrays
.isShared(t1
) || !d_arrays
.isShared(t2
)) {
323 return d_arrays
.propagate(t1
.eqNode(t2
).notNode());
328 void eqNotifyConstantTermMerge(TNode t1
, TNode t2
) override
330 Debug("arrays::propagate") << spaces(d_arrays
.getSatContext()->getLevel()) << "NotifyClass::eqNotifyConstantTermMerge(" << t1
<< ", " << t2
<< ")" << std::endl
;
331 d_arrays
.conflict(t1
, t2
);
334 void eqNotifyNewClass(TNode t
) override
{}
335 void eqNotifyPreMerge(TNode t1
, TNode t2
) override
{}
336 void eqNotifyPostMerge(TNode t1
, TNode t2
) override
338 if (t1
.getType().isArray()) {
339 d_arrays
.mergeArrays(t1
, t2
);
342 void eqNotifyDisequal(TNode t1
, TNode t2
, TNode reason
) override
{}
345 /** The notify class for d_equalityEngine */
346 NotifyClass d_notify
;
348 /** Equaltity engine */
349 eq::EqualityEngine d_equalityEngine
;
351 /** Are we in conflict? */
352 context::CDO
<bool> d_conflict
;
354 /** Conflict when merging constants */
355 void conflict(TNode a
, TNode b
);
357 /** The conflict node */
361 * Context dependent map from a congruence class canonical representative of
362 * type array to an Info pointer that keeps track of information useful to axiom
366 Backtracker
<TNode
> d_backtracker
;
369 context::CDQueue
<Node
> d_mergeQueue
;
371 bool d_mergeInProgress
;
373 using RowLemmaType
= std::tuple
<TNode
, TNode
, TNode
, TNode
>;
375 context::CDQueue
<RowLemmaType
> d_RowQueue
;
376 context::CDHashSet
<RowLemmaType
, RowLemmaTypeHashFunction
> d_RowAlreadyAdded
;
378 typedef context::CDHashSet
<Node
, NodeHashFunction
> CDNodeSet
;
380 CDNodeSet d_sharedArrays
;
381 CDNodeSet d_sharedOther
;
382 context::CDO
<bool> d_sharedTerms
;
384 // Map from constant values to read terms that read from that values equal to that constant value in the current model
385 // When a new read term is created, we check the index to see if we know the model value. If so, we add it to d_constReads (and d_constReadsList)
386 // If not, we push it onto d_reads and figure out where it goes at computeCareGraph time.
387 // d_constReadsList is used as a backup in case we can't compute the model at computeCareGraph time.
388 typedef std::unordered_map
<Node
, CTNodeList
*, NodeHashFunction
> CNodeNListMap
;
389 CNodeNListMap d_constReads
;
390 context::CDList
<TNode
> d_reads
;
391 context::CDList
<TNode
> d_constReadsList
;
392 context::Context
* d_constReadsContext
;
393 /** Helper class to keep d_constReadsContext in sync with satContext */
394 class ContextPopper
: public context::ContextNotifyObj
{
395 context::Context
* d_satContext
;
396 context::Context
* d_contextToPop
;
398 void contextNotifyPop() override
400 if (d_contextToPop
->getLevel() > d_satContext
->getLevel())
402 d_contextToPop
->pop();
406 ContextPopper(context::Context
* context
, context::Context
* contextToPop
)
407 :context::ContextNotifyObj(context
), d_satContext(context
),
408 d_contextToPop(contextToPop
)
411 };/* class ContextPopper */
412 ContextPopper d_contextPopper
;
414 std::unordered_map
<Node
, Node
, NodeHashFunction
> d_skolemCache
;
415 context::CDO
<unsigned> d_skolemIndex
;
416 std::vector
<Node
> d_skolemAssertions
;
418 // The decision requests we have for the core
419 context::CDQueue
<Node
> d_decisionRequests
;
421 // List of nodes that need permanent references in this context
422 context::CDList
<Node
> d_permRef
;
423 context::CDList
<Node
> d_modelConstraints
;
424 context::CDHashSet
<Node
, NodeHashFunction
> d_lemmasSaved
;
425 std::vector
<Node
> d_lemmas
;
427 // Default values for each mayEqual equivalence class
428 typedef context::CDHashMap
<Node
,Node
,NodeHashFunction
> DefValMap
;
429 DefValMap d_defValues
;
431 typedef std::unordered_map
<std::pair
<TNode
, TNode
>, CTNodeList
*, TNodePairHashFunction
> ReadBucketMap
;
432 ReadBucketMap d_readBucketTable
;
433 context::Context
* d_readTableContext
;
434 context::CDList
<Node
> d_arrayMerges
;
435 std::vector
<CTNodeList
*> d_readBucketAllocations
;
437 Node
getSkolem(TNode ref
, const std::string
& name
, const TypeNode
& type
, const std::string
& comment
, bool makeEqual
= true);
438 Node
mkAnd(std::vector
<TNode
>& conjunctions
, bool invert
= false, unsigned startIndex
= 0);
439 void setNonLinear(TNode a
);
440 void checkRIntro1(TNode a
, TNode b
);
441 Node
removeRepLoops(TNode a
, TNode rep
);
442 Node
expandStores(TNode s
, std::vector
<TNode
>& assumptions
, bool checkLoop
= false, TNode a
= TNode(), TNode b
= TNode());
443 void mergeArrays(TNode a
, TNode b
);
444 void checkStore(TNode a
);
445 void checkRowForIndex(TNode i
, TNode a
);
446 void checkRowLemmas(TNode a
, TNode b
);
447 void propagate(RowLemmaType lem
);
448 void queueRowLemma(RowLemmaType lem
);
449 bool dischargeLemmas();
451 std::vector
<Node
> d_decisions
;
455 /** An equality-engine callback for proof reconstruction */
456 ArrayProofReconstruction d_proofReconstruction
;
459 eq::EqualityEngine
* getEqualityEngine() override
{ return &d_equalityEngine
; }
461 };/* class TheoryArrays */
463 }/* CVC4::theory::arrays namespace */
464 }/* CVC4::theory namespace */
465 }/* CVC4 namespace */
467 #endif /* __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_H */