src/theory/arrays/theory_arrays.h

   1 /*********************                                                        */
   2 /*! \file theory_arrays.h
   3  ** \verbatim
   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
  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/array_proof_reconstruction.h"
  30 #include "theory/theory.h"
  31 #include "theory/uf/equality_engine.h"
  32 #include "util/statistics_registry.h"
  33
  34 namespace CVC4 {
  35 namespace theory {
  36 namespace arrays {
  37
  38 /**
  39  * Decision procedure for arrays.
  40  *
  41  * Overview of decision procedure:
  42  *
  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
  48  *   current context.
  49  *
  50  * The rules implemented are the following:
  51  *             store(b i v)
  52  *     Row1 -------------------
  53  *          store(b i v)[i] = v
  54  *
  55  *           store(b i v)  a'[j]
  56  *     Row ---------------------- [ a' ~ store(b i v) or a' ~ b ]
  57  *           i = j OR a[j] = b[j]
  58  *
  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
  62  *
  63  *
  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
  69  *
  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
  78  *        Row lemma
  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
  82  *
  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.
  86  */
  87
  88 static inline std::string spaces(int level)
  89 {
  90   std::string indentStr(level, ' ');
  91   return indentStr;
  92 }
  93
  94 class TheoryArrays : public Theory {
  95
  96   /////////////////////////////////////////////////////////////////////////////
  97   // MISC
  98   /////////////////////////////////////////////////////////////////////////////
  99
 100  private:
 101
 102   /** True node for predicates = true */
 103   Node d_true;
 104
 105   /** True node for predicates = false */
 106   Node d_false;
 107
 108   // Statistics
 109
 110   /** number of Row lemmas */
 111   IntStat d_numRow;
 112   /** number of Ext lemmas */
 113   IntStat d_numExt;
 114   /** number of propagations */
 115   IntStat d_numProp;
 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;
 130
 131   // Merge reason types
 132
 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;
 139
 140  public:
 141
 142   TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out,
 143                Valuation valuation, const LogicInfo& logicInfo,
 144                std::string name = "");
 145   ~TheoryArrays();
 146
 147   void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
 148
 149   std::string identify() const override { return std::string("TheoryArrays"); }
 150
 151   /////////////////////////////////////////////////////////////////////////////
 152   // PREPROCESSING
 153   /////////////////////////////////////////////////////////////////////////////
 154
 155  private:
 156
 157   // PPNotifyClass: dummy template class for d_ppEqualityEngine - notifications not used
 158   class PPNotifyClass {
 159   public:
 160     bool notify(TNode propagation) { return true; }
 161     void notify(TNode t1, TNode t2) { }
 162   };
 163
 164   /** The notify class for d_ppEqualityEngine */
 165   PPNotifyClass d_ppNotify;
 166
 167   /** Equaltity engine */
 168   eq::EqualityEngine d_ppEqualityEngine;
 169
 170   // List of facts learned by preprocessor - needed for permanent ref for benefit of d_ppEqualityEngine
 171   context::CDList<Node> d_ppFacts;
 172
 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);
 177
 178  public:
 179   PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
 180   Node ppRewrite(TNode atom) override;
 181
 182   /////////////////////////////////////////////////////////////////////////////
 183   // T-PROPAGATION / REGISTRATION
 184   /////////////////////////////////////////////////////////////////////////////
 185
 186  private:
 187   /** Literals to propagate */
 188   context::CDList<Node> d_literalsToPropagate;
 189
 190   /** Index of the next literal to propagate */
 191   context::CDO<unsigned> d_literalsToPropagateIndex;
 192
 193   /** Should be called to propagate the literal.  */
 194   bool propagate(TNode literal);
 195
 196   /** Explain why this literal is true by adding assumptions */
 197   void explain(TNode literal, std::vector<TNode>& assumptions,
 198                eq::EqProof* proof);
 199
 200   /** For debugging only- checks invariants about when things are preregistered*/
 201   context::CDHashSet<Node, NodeHashFunction > d_isPreRegistered;
 202
 203   /** Helper for preRegisterTerm, also used internally */
 204   void preRegisterTermInternal(TNode n);
 205
 206  public:
 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;
 211
 212   /////////////////////////////////////////////////////////////////////////////
 213   // SHARING
 214   /////////////////////////////////////////////////////////////////////////////
 215
 216  private:
 217   class MayEqualNotifyClass {
 218   public:
 219     bool notify(TNode propagation) { return true; }
 220     void notify(TNode t1, TNode t2) { }
 221   };
 222
 223   /** The notify class for d_mayEqualEqualityEngine */
 224   MayEqualNotifyClass d_mayEqualNotify;
 225
 226   /** Equaltity engine for determining if two arrays might be equal */
 227   eq::EqualityEngine d_mayEqualEqualityEngine;
 228
 229   // Helper for computeCareGraph
 230   void checkPair(TNode r1, TNode r2);
 231
 232  public:
 233   void addSharedTerm(TNode t) override;
 234   EqualityStatus getEqualityStatus(TNode a, TNode b) override;
 235   void computeCareGraph() override;
 236   bool isShared(TNode t)
 237   {
 238     return (d_sharedArrays.find(t) != d_sharedArrays.end());
 239   }
 240
 241   /////////////////////////////////////////////////////////////////////////////
 242   // MODEL GENERATION
 243   /////////////////////////////////////////////////////////////////////////////
 244
 245  public:
 246   bool collectModelInfo(TheoryModel* m) override;
 247
 248   /////////////////////////////////////////////////////////////////////////////
 249   // NOTIFICATIONS
 250   /////////////////////////////////////////////////////////////////////////////
 251
 252  public:
 253   Node getNextDecisionRequest(unsigned& priority) override;
 254
 255   void presolve() override;
 256   void shutdown() override {}
 257
 258   /////////////////////////////////////////////////////////////////////////////
 259   // MAIN SOLVER
 260   /////////////////////////////////////////////////////////////////////////////
 261
 262  public:
 263   void check(Effort e) override;
 264
 265  private:
 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);
 274
 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;
 278   public:
 279     NotifyClass(TheoryArrays& arrays): d_arrays(arrays) {}
 280
 281     bool eqNotifyTriggerEquality(TNode equality, bool value) override
 282     {
 283       Debug("arrays::propagate") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false") << ")" << std::endl;
 284       // Just forward to arrays
 285       if (value) {
 286         return d_arrays.propagate(equality);
 287       } else {
 288         return d_arrays.propagate(equality.notNode());
 289       }
 290     }
 291
 292     bool eqNotifyTriggerPredicate(TNode predicate, bool value) override
 293     {
 294       Debug("arrays::propagate") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::eqNotifyTriggerEquality(" << predicate << ", " << (value ? "true" : "false") << ")" << std::endl;
 295       // Just forward to arrays
 296       if (value) {
 297         return d_arrays.propagate(predicate);
 298       } else {
 299         return d_arrays.propagate(predicate.notNode());
 300       }
 301     }
 302
 303     bool eqNotifyTriggerTermEquality(TheoryId tag,
 304                                      TNode t1,
 305                                      TNode t2,
 306                                      bool value) override
 307     {
 308       Debug("arrays::propagate") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::eqNotifyTriggerTermEquality(" << t1 << ", " << t2 << ", " << (value ? "true" : "false") << ")" << std::endl;
 309       if (value) {
 310         if (t1.getType().isArray()) {
 311           if (!d_arrays.isShared(t1) || !d_arrays.isShared(t2)) {
 312             return true;
 313           }
 314         }
 315         // Propagate equality between shared terms
 316         return d_arrays.propagate(t1.eqNode(t2));
 317       } else {
 318         if (t1.getType().isArray()) {
 319           if (!d_arrays.isShared(t1) || !d_arrays.isShared(t2)) {
 320             return true;
 321           }
 322         }
 323         return d_arrays.propagate(t1.eqNode(t2).notNode());
 324       }
 325       return true;
 326     }
 327
 328     void eqNotifyConstantTermMerge(TNode t1, TNode t2) override
 329     {
 330       Debug("arrays::propagate") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
 331       d_arrays.conflict(t1, t2);
 332     }
 333
 334     void eqNotifyNewClass(TNode t) override {}
 335     void eqNotifyPreMerge(TNode t1, TNode t2) override {}
 336     void eqNotifyPostMerge(TNode t1, TNode t2) override
 337     {
 338       if (t1.getType().isArray()) {
 339         d_arrays.mergeArrays(t1, t2);
 340       }
 341     }
 342     void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override {}
 343   };
 344
 345   /** The notify class for d_equalityEngine */
 346   NotifyClass d_notify;
 347
 348   /** Equaltity engine */
 349   eq::EqualityEngine d_equalityEngine;
 350
 351   /** Are we in conflict? */
 352   context::CDO<bool> d_conflict;
 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   class ContextPopper : public context::ContextNotifyObj {
 395     context::Context* d_satContext;
 396     context::Context* d_contextToPop;
 397   protected:
 398    void contextNotifyPop() override
 399    {
 400      if (d_contextToPop->getLevel() > d_satContext->getLevel())
 401      {
 402        d_contextToPop->pop();
 403      }
 404     }
 405   public:
 406     ContextPopper(context::Context* context, context::Context* contextToPop)
 407       :context::ContextNotifyObj(context), d_satContext(context),
 408        d_contextToPop(contextToPop)
 409     {}
 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, 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();
 450
 451   std::vector<Node> d_decisions;
 452   bool d_inCheckModel;
 453   int d_topLevel;
 454
 455   /** An equality-engine callback for proof reconstruction */
 456   ArrayProofReconstruction d_proofReconstruction;
 457
 458  public:
 459   eq::EqualityEngine* getEqualityEngine() override { return &d_equalityEngine; }
 460
 461 };/* class TheoryArrays */
 462
 463 }/* CVC4::theory::arrays namespace */
 464 }/* CVC4::theory namespace */
 465 }/* CVC4 namespace */
 466
 467 #endif /* __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_H */