GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arrays/theory_arrays.h Lines: 39 40 97.5 %
Date: 2021-03-23 Branches: 59 106 55.7 %

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