src/theory/arrays/theory_arrays.h

   1 /*********************                                                        */
   2 /*! \file theory_arrays.h
   3  ** \verbatim
   4  ** Original author: mdeters
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): barrett
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
   9  ** Courant Institute of Mathematical Sciences
  10  ** New York University
  11  ** See the file COPYING in the top-level source directory for licensing
  12  ** information.\endverbatim
  13  **
  14  ** \brief Theory of arrays
  15  **
  16  ** Theory of arrays.
  17  **/
  18
  19 #include "cvc4_private.h"
  20
  21 #ifndef __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_H
  22 #define __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_H
  23
  24 #include "theory/theory.h"
  25 #include "theory/arrays/union_find.h"
  26 #include "util/congruence_closure.h"
  27 #include "theory/arrays/array_info.h"
  28 #include "util/hash.h"
  29 #include "util/ntuple.h"
  30 #include "util/stats.h"
  31 #include "util/backtrackable.h"
  32 #include "theory/arrays/static_fact_manager.h"
  33
  34 #include <iostream>
  35 #include <map>
  36
  37 namespace CVC4 {
  38 namespace theory {
  39 namespace arrays {
  40
  41 /**
  42  * Decision procedure for arrays.
  43  *
  44  * Overview of decision procedure:
  45  *
  46  * Preliminary notation:
  47  *   Stores(a)  = {t | a ~ t and t = store( _ _ _ )}
  48  *   InStores(a) = {t | t = store (b _ _) and a ~ b }
  49  *   Indices(a) = {i | there exists a term b[i] such that a ~ b or store(b i v)}
  50  *   ~ represents the equivalence relation based on the asserted equalities in the
  51  *   current context.
  52  *
  53  * The rules implemented are the following:
  54  *             store(b i v)
  55  *     Row1 -------------------
  56  *          store(b i v)[i] = v
  57  *
  58  *           store(b i v)  a'[j]
  59  *     Row ---------------------- [ a' ~ store(b i v) or a' ~ b ]
  60  *           i = j OR a[j] = b[j]
  61  *
  62  *          a  b same kind arrays
  63  *     Ext ------------------------ [ a!= b in current context, k new var]
  64  *           a = b OR a[k] != b[k]p
  65  *
  66  *
  67  *  The Row1 one rule is implemented implicitly as follows:
  68  *     - for each store(b i v) term add the following equality to the congruence
  69  *       closure store(b i v)[i] = v
  70  *     - if one of the literals in a conflict is of the form store(b i v)[i] = v
  71  *       remove it from the conflict
  72  *
  73  *  Because new store terms are not created, we need to check if we need to
  74  *  instantiate a new Row axiom in the following cases:
  75  *     1. the congruence relation changes (i.e. two terms get merged)
  76  *         - when a new equality between array terms a = b is asserted we check if
  77  *           we can instantiate a Row lemma for all pairs of indices i where a is
  78  *           being read and stores
  79  *         - this is only done during full effort check
  80  *     2. a new read term is created either as a consequences of an Ext lemma or a
  81  *        Row lemma
  82  *         - this is implemented in the checkRowForIndex method which is called
  83  *           when preregistering a term of the form a[i].
  84  *         - as a consequence lemmas are instantiated even before full effort check
  85  *
  86  *  The Ext axiom is instantiated when a disequality is asserted during full effort
  87  *  check. Ext lemmas are stored in a cache to prevent instantiating essentially
  88  *  the same lemma multiple times.
  89  */
  90 class TheoryArrays : public Theory {
  91
  92 private:
  93
  94
  95   class CongruenceChannel {
  96     TheoryArrays* d_arrays;
  97
  98   public:
  99     CongruenceChannel(TheoryArrays* arrays) : d_arrays(arrays) {}
 100     void notifyCongruent(TNode a, TNode b) {
 101       d_arrays->notifyCongruent(a, b);
 102     }
 103   }; /* class CongruenceChannel*/
 104   friend class CongruenceChannel;
 105
 106   /**
 107    * Output channel connected to the congruence closure module.
 108    */
 109   CongruenceChannel d_ccChannel;
 110
 111   /**
 112    * Instance of the congruence closure module.
 113    */
 114   CongruenceClosure<CongruenceChannel, CONGRUENCE_OPERATORS_1
 115                                  (kind::SELECT)> d_cc;
 116
 117   /**
 118    * (Temporary) fact manager for preprocessing - eventually handle this with
 119    * something more standard (like congruence closure module)
 120    */
 121   StaticFactManager d_staticFactManager;
 122
 123   /**
 124    * Cache for proprocessing of atoms.
 125    */
 126   typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
 127   NodeMap d_ppCache;
 128
 129   /**
 130    * Union find for storing the equalities.
 131    */
 132
 133   UnionFind<Node, NodeHashFunction> d_unionFind;
 134
 135   Backtracker<TNode> d_backtracker;
 136
 137
 138   /**
 139    * Context dependent map from a congruence class canonical representative of
 140    * type array to an Info pointer that keeps track of information useful to axiom
 141    * instantiation
 142    */
 143
 144   ArrayInfo d_infoMap;
 145
 146   /**
 147    * Received a notification from the congruence closure algorithm that the two
 148    * nodes a and b have become congruent.
 149    */
 150
 151   void notifyCongruent(TNode a, TNode b);
 152
 153
 154   typedef context::CDList<TNode, context::ContextMemoryAllocator<TNode> > CTNodeListAlloc;
 155   typedef context::CDMap<Node, CTNodeListAlloc*, NodeHashFunction> CNodeTNodesMap;
 156   typedef context::CDMap<TNode, List<TNode>*, TNodeHashFunction > EqLists;
 157
 158
 159   typedef __gnu_cxx::hash_map<TNode, CTNodeList*, TNodeHashFunction> NodeTNodesMap;
 160   /**
 161    * List of all disequalities this theory has seen. Maintains the invariant that
 162    * if a is in the disequality list of b, then b is in that of a. FIXME? make non context dep map
 163    * */
 164   CNodeTNodesMap d_disequalities;
 165   EqLists d_equalities;
 166   context::CDList<TNode> d_prop_queue;
 167
 168   void checkPropagations(TNode a, TNode b);
 169
 170   /** List of all atoms the SAT solver knows about and are candidates for
 171    *  propagation. */
 172   __gnu_cxx::hash_set<TNode, TNodeHashFunction> d_atoms;
 173
 174   /** List of disequalities needed to construct explanations for propagated
 175    * row lemmas */
 176
 177   context::CDMap<TNode, std::pair<TNode, TNode>, TNodeHashFunction> d_explanations;
 178
 179   /**
 180    * stores the conflicting disequality (still need to call construct
 181    * conflict to get the actual explanation)
 182    */
 183   Node d_conflict;
 184
 185   typedef context::CDList< quad<TNode, TNode, TNode, TNode > > QuadCDList;
 186
 187
 188   /**
 189    * Ext lemma workslist that stores extensionality lemmas that still need to be added
 190    */
 191   std::hash_set<std::pair<TNode, TNode>, TNodePairHashFunction> d_extQueue;
 192
 193   /**
 194    * Row Lemma worklist, stores lemmas that can still be added to the SAT solver
 195    * to be emptied during full effort check
 196    */
 197   std::hash_set<quad<TNode, TNode, TNode, TNode>, TNodeQuadHashFunction > d_RowQueue;
 198
 199   /**
 200    * Extensionality lemma cache which stores the array pair (a,b) for which
 201    * a lemma of the form (a = b OR a[k]!= b[k]) has been added to the SAT solver.
 202    */
 203   std::hash_set<std::pair<TNode, TNode>, TNodePairHashFunction> d_extAlreadyAdded;
 204
 205   /**
 206    * Read-over-write lemma cache storing a quadruple (a,b,i,j) for which a
 207    * the lemma (i = j OR a[j] = b[j]) has been added to the SAT solver. Needed
 208    * to prevent infinite recursion in addRowLemma.
 209    */
 210   std::hash_set<quad<TNode, TNode, TNode, TNode>, TNodeQuadHashFunction > d_RowAlreadyAdded;
 211
 212   /*
 213    * Congruence helper methods
 214    */
 215
 216   void addDiseq(TNode diseq);
 217   void addEq(TNode eq);
 218
 219   void appendToDiseqList(TNode of, TNode eq);
 220   void appendToEqList(TNode a, TNode b);
 221   Node constructConflict(TNode diseq);
 222
 223   /**
 224    * Merges two congruence classes in the internal union-find and checks for a
 225    * conflict.
 226    */
 227
 228   void merge(TNode a, TNode b);
 229   inline TNode find(TNode a);
 230   inline TNode debugFind(TNode a) const;
 231
 232   inline void setCanon(TNode a, TNode b);
 233
 234   void queueRowLemma(TNode a, TNode b, TNode i, TNode j);
 235   inline void queueExtLemma(TNode a, TNode b);
 236
 237   /**
 238    * Adds a Row lemma of the form:
 239    *    i = j OR a[j] = b[j]
 240    */
 241   void addRowLemma(TNode a, TNode b, TNode i, TNode j);
 242
 243   /**
 244    * Adds a new Ext lemma of the form
 245    *    a = b OR a[k]!=b[k], for a new variable k
 246    */
 247   void addExtLemma(TNode a, TNode b);
 248
 249   /**
 250    * Because Row1 axioms of the form (store a i v) [i] = v are not added as
 251    * explicitly but are kept track of internally, is axiom recognizez an axiom
 252    * of the above form given the two terms in the equality.
 253    */
 254   bool isAxiom(TNode lhs, TNode rhs);
 255
 256
 257   bool isRedundantRowLemma(TNode a, TNode b, TNode i, TNode j);
 258   bool isRedundantInContext(TNode a, TNode b, TNode i, TNode j);
 259
 260
 261
 262   bool alreadyAddedRow(TNode a, TNode b, TNode i, TNode j) {
 263     //Trace("arrays-lem")<<"alreadyAddedRow check for "<<a<<" "<<b<<" "<<i<<" "<<j<<"\n";
 264     std::hash_set<quad<TNode, TNode, TNode, TNode>, TNodeQuadHashFunction >::const_iterator it = d_RowAlreadyAdded.begin();
 265     a = find(a);
 266     b = find(b);
 267     i = find(i);
 268     j = find(j);
 269
 270     for( ; it!= d_RowAlreadyAdded.end(); it++) {
 271
 272       TNode a_ = find((*it).first);
 273       TNode b_ = find((*it).second);
 274       TNode i_ = find((*it).third);
 275       TNode j_ = find((*it).fourth);
 276       if( a == a_ && b == b_ && i==i_ && j==j_) {
 277         //Trace("arrays-lem")<<"alreadyAddedRow found "<<a_<<" "<<b_<<" "<<i_<<" "<<j_<<"\n";
 278         return true;
 279       }
 280     }
 281     return false;
 282   }
 283
 284
 285   bool isNonLinear(TNode n);
 286
 287   /**
 288    * Checks if any new Row lemmas need to be generated after merging arrays a
 289    * and b; called after setCanon.
 290    */
 291   void checkRowLemmas(TNode a, TNode b);
 292
 293   /**
 294    * Called after a new select term a[i] is created to check whether new Row
 295    * lemmas need to be instantiated.
 296    */
 297   void checkRowForIndex(TNode i, TNode a);
 298
 299   void checkStore(TNode a);
 300   /**
 301    * Lemma helper functions to prevent changing the list we are iterating through.
 302    */
 303
 304   void insertInQuadQueue(std::set<quad<TNode, TNode, TNode, TNode> >& queue, TNode a, TNode b, TNode i, TNode j){
 305     if(i != j) {
 306       queue.insert(make_quad(a,b,i,j));
 307     }
 308   }
 309
 310   void dischargeLemmas() {
 311     // we need to swap the temporary lists because adding a lemma calls preregister
 312     // which might modify the d_RowQueue we would be iterating through
 313     std::hash_set<quad<TNode, TNode, TNode, TNode>, TNodeQuadHashFunction > temp_Row;
 314     temp_Row.swap(d_RowQueue);
 315
 316     std::hash_set<quad<TNode, TNode, TNode, TNode>, TNodeQuadHashFunction >::const_iterator it1 = temp_Row.begin();
 317     for( ; it1!= temp_Row.end(); it1++) {
 318       if(!isRedundantInContext((*it1).first, (*it1).second, (*it1).third, (*it1).fourth)) {
 319         addRowLemma((*it1).first, (*it1).second, (*it1).third, (*it1).fourth);
 320       }
 321       else {
 322         // add it to queue may be needed later
 323         queueRowLemma((*it1).first, (*it1).second, (*it1).third, (*it1).fourth);
 324       }
 325     }
 326
 327     std::hash_set<std::pair<TNode, TNode>, TNodePairHashFunction>  temp_ext;
 328     temp_ext.swap(d_extQueue);
 329
 330     std::hash_set<std::pair<TNode, TNode>, TNodePairHashFunction> ::const_iterator it2 = temp_ext.begin();
 331     for(; it2 != temp_ext.end(); it2++) {
 332       addExtLemma((*it2).first, (*it2).second);
 333     }
 334   }
 335
 336   /** Checks if instead of adding a lemma of the form i = j OR  a[j] = b[j]
 337    * we can propagate either i = j or NOT a[j] = b[j] and does the propagation.
 338    * Returns whether it did propagate.
 339    */
 340   bool propagateFromRow(TNode a, TNode b, TNode i, TNode j);
 341
 342   TNode areDisequal(TNode a, TNode b);
 343
 344
 345
 346   /*
 347    * === STATISTICS ===
 348    */
 349
 350   /** number of Row lemmas */
 351   IntStat d_numRow;
 352   /** number of Ext lemmas */
 353   IntStat d_numExt;
 354
 355   /** number of propagations */
 356   IntStat d_numProp;
 357   IntStat d_numExplain;
 358   /** time spent in check() */
 359   TimerStat d_checkTimer;
 360
 361   bool d_donePreregister;
 362
 363   Node preprocessTerm(TNode term);
 364   Node recursivePreprocessTerm(TNode term);
 365
 366 public:
 367   TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation);
 368   ~TheoryArrays();
 369
 370   /**
 371    * Stores in d_infoMap the following information for each term a of type array:
 372    *
 373    *    - all i, such that there exists a term a[i] or a = store(b i v)
 374    *      (i.e. all indices it is being read atl; store(b i v) is implicitly read at
 375    *      position i due to the implicit axiom store(b i v)[i] = v )
 376    *
 377    *    - all the stores a is congruent to (this information is context dependent)
 378    *
 379    *    - all store terms of the form store (a i v) (i.e. in which a appears
 380    *      directly; this is invariant because no new store terms are created)
 381    *
 382    * Note: completeness depends on having pre-register called on all the input
 383    *       terms before starting to instantiate lemmas.
 384    */
 385   void preRegisterTerm(TNode n) {
 386     //TimerStat::CodeTimer codeTimer(d_preregisterTimer);
 387     Trace("arrays-preregister")<<"Arrays::preRegisterTerm "<<n<<"\n";
 388     //TODO: check non-linear arrays with an AlwaysAssert!!!
 389     //if(n.getType().isArray())
 390
 391     switch(n.getKind()) {
 392     case kind::EQUAL:
 393       // stores the seen atoms for propagation
 394       Trace("arrays-preregister")<<"atom "<<n<<"\n";
 395       d_atoms.insert(n);
 396       // add to proper equality lists
 397       addEq(n);
 398       break;
 399     case kind::SELECT:
 400       //Trace("arrays-preregister")<<"at level "<<getContext()->getLevel()<<"\n";
 401       d_infoMap.addIndex(n[0], n[1]);
 402       checkRowForIndex(n[1], find(n[0]));
 403       //Trace("arrays-preregister")<<"n[0] \n";
 404       //d_infoMap.getInfo(n[0])->print();
 405       //Trace("arrays-preregister")<<"find(n[0]) \n";
 406       //d_infoMap.getInfo(find(n[0]))->print();
 407       break;
 408
 409     case kind::STORE:
 410     {
 411       // this should always be called at level0 since we do not create new store terms
 412       TNode a = n[0];
 413       TNode i = n[1];
 414       TNode v = n[2];
 415
 416       NodeManager* nm = NodeManager::currentNM();
 417       Node ni = nm->mkNode(kind::SELECT, n, i);
 418       Node eq = nm->mkNode(kind::EQUAL, ni, v);
 419
 420       d_cc.addEquality(eq);
 421
 422       d_infoMap.addIndex(n, i);
 423       d_infoMap.addStore(n, n);
 424       d_infoMap.addInStore(a, n);
 425
 426       checkStore(n);
 427
 428       break;
 429     }
 430     default:
 431       Trace("darrays")<<"Arrays::preRegisterTerm non-array term. \n";
 432     }
 433   }
 434
 435   //void registerTerm(TNode n) {
 436   //  Trace("arrays-register")<<"Arrays::registerTerm "<<n<<"\n";
 437   //}
 438
 439   void presolve() {
 440     Trace("arrays")<<"Presolving \n";
 441     d_donePreregister = true;
 442   }
 443
 444   void addSharedTerm(TNode t);
 445   void notifyEq(TNode lhs, TNode rhs);
 446   void check(Effort e);
 447
 448   void propagate(Effort e) {
 449
 450     Trace("arrays-prop")<<"Propagating \n";
 451
 452     context::CDList<TNode>::const_iterator it = d_prop_queue.begin();
 453     /*
 454     for(; it!= d_prop_queue.end(); it++) {
 455       TNode eq = *it;
 456       if(d_valuation.getSatValue(eq).isNull()) {
 457         //FIXME remove already propagated literals?
 458         d_out->propagate(eq);
 459         ++d_numProp;
 460       }
 461     }*/
 462     //d_prop_queue.deleteSelf();
 463     /*
 464     __gnu_cxx::hash_set<TNode, TNodeHashFunction>::const_iterator it = d_atoms.begin();
 465
 466     for(; it!= d_atoms.end(); it++) {
 467       TNode eq = *it;
 468       Assert(eq.getKind()==kind::EQUAL);
 469       Trace("arrays-prop")<<"value of "<<eq<<" ";
 470       Trace("arrays-prop")<<d_valuation.getSatValue(eq);
 471       if(find(eq[0]) == find(eq[1])) {
 472         Trace("arrays-prop")<<" eq \n";
 473         ++d_numProp;
 474       }
 475     }
 476     */
 477
 478   }
 479   Node explain(TNode n);
 480
 481   Node getValue(TNode n);
 482   SolveStatus solve(TNode in, SubstitutionMap& outSubstitutions);
 483   Node preprocess(TNode atom);
 484   void shutdown() { }
 485   std::string identify() const { return std::string("TheoryArrays"); }
 486
 487 };/* class TheoryArrays */
 488
 489 inline void TheoryArrays::setCanon(TNode a, TNode b) {
 490   d_unionFind.setCanon(a, b);
 491 }
 492
 493 inline TNode TheoryArrays::find(TNode a) {
 494   return d_unionFind.find(a);
 495 }
 496
 497 inline TNode TheoryArrays::debugFind(TNode a) const {
 498   return d_unionFind.debugFind(a);
 499 }
 500
 501 }/* CVC4::theory::arrays namespace */
 502 }/* CVC4::theory namespace */
 503 }/* CVC4 namespace */
 504
 505 #endif /* __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_H */