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