src/theory/arrays/array_info.h

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Morgan Deters, Clark Barrett, Tim King
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   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.
  11  * ****************************************************************************
  12  *
  13  * Contains additional classes to store context dependent information
  14  * for each term of type array.
  15  */
  16
  17 #include "cvc5_private.h"
  18
  19 #ifndef CVC5__THEORY__ARRAYS__ARRAY_INFO_H
  20 #define CVC5__THEORY__ARRAYS__ARRAY_INFO_H
  21
  22 #include <tuple>
  23 #include <unordered_map>
  24
  25 #include "context/backtrackable.h"
  26 #include "context/cdlist.h"
  27 #include "expr/node.h"
  28 #include "util/statistics_stats.h"
  29
  30 namespace cvc5 {
  31 namespace theory {
  32 namespace arrays {
  33
  34 typedef context::CDList<TNode> CTNodeList;
  35 using RowLemmaType = std::tuple<TNode, TNode, TNode, TNode>;
  36
  37 struct RowLemmaTypeHashFunction {
  38   size_t operator()(const RowLemmaType& q) const {
  39     TNode n1, n2, n3, n4;
  40     std::tie(n1, n2, n3, n4) = q;
  41     return (size_t) (n1.getId()*0x9e3779b9 + n2.getId()*0x30000059 +
  42         n3.getId()*0x60000005 + n4.getId()*0x07FFFFFF);
  43
  44   }
  45 };/* struct RowLemmaTypeHashFunction */
  46
  47 void printList (CTNodeList* list);
  48 void printList( List<TNode>* list);
  49
  50 bool inList(const CTNodeList* l, const TNode el);
  51
  52 /**
  53  * Small class encapsulating the information
  54  * in the map. It's a class and not a struct to
  55  * call the destructor.
  56  */
  57
  58 class Info {
  59 public:
  60   context::CDO<bool> isNonLinear;
  61   context::CDO<bool> rIntro1Applied;
  62   context::CDO<TNode> modelRep;
  63   context::CDO<TNode> constArr;
  64   context::CDO<TNode> weakEquivPointer;
  65   context::CDO<TNode> weakEquivIndex;
  66   context::CDO<TNode> weakEquivSecondary;
  67   context::CDO<TNode> weakEquivSecondaryReason;
  68   CTNodeList* indices;
  69   CTNodeList* stores;
  70   CTNodeList* in_stores;
  71
  72   Info(context::Context* c, Backtracker<TNode>* bck);
  73   ~Info();
  74
  75   /**
  76    * prints the information
  77    */
  78   void print() const {
  79     Assert(indices != NULL && stores != NULL && in_stores != NULL);
  80     Trace("arrays-info")<<"  indices   ";
  81     printList(indices);
  82     Trace("arrays-info")<<"  stores ";
  83     printList(stores);
  84     Trace("arrays-info")<<"  in_stores ";
  85     printList(in_stores);
  86   }
  87 };/* class Info */
  88
  89 typedef std::unordered_map<Node, Info*> CNodeInfoMap;
  90
  91 /**
  92  * Class keeping track of the following information for canonical
  93  * representatives of type array [a] :
  94  *    indices at which it is being read (all i for which there is a
  95  *            term of the form SELECT a i)
  96  *    all store terms in the congruence class
  97  *    stores in which it appears (terms of the form STORE a _ _ )
  98  *
  99  */
 100 class ArrayInfo {
 101 private:
 102   context::Context* ct;
 103   Backtracker<TNode>* bck;
 104   CNodeInfoMap info_map;
 105
 106   CTNodeList* emptyList;
 107
 108   /* == STATISTICS == */
 109
 110   /** time spent in preregisterTerm() */
 111   TimerStat d_mergeInfoTimer;
 112   AverageStat d_avgIndexListLength;
 113   AverageStat d_avgStoresListLength;
 114   AverageStat d_avgInStoresListLength;
 115   IntStat d_listsCount;
 116   IntStat d_callsMergeInfo;
 117   IntStat d_maxList;
 118   SizeStat<CNodeInfoMap> d_tableSize;
 119
 120   /**
 121    * checks if a certain element is in the list l
 122    * FIXME: better way to check for duplicates?
 123    */
 124
 125   /**
 126    * helper method that merges two lists into the first
 127    * without adding duplicates
 128    */
 129   void mergeLists(CTNodeList* la, const CTNodeList* lb) const;
 130
 131 public:
 132   const Info* emptyInfo;
 133 /*
 134   ArrayInfo(): ct(NULl), info
 135     d_mergeInfoTimer("theory::arrays::mergeInfoTimer"),
 136     d_avgIndexListLength("theory::arrays::avgIndexListLength"),
 137     d_avgStoresListLength("theory::arrays::avgStoresListLength"),
 138     d_avgInStoresListLength("theory::arrays::avgInStoresListLength"),
 139     d_listsCount("theory::arrays::listsCount",0),
 140     d_callsMergeInfo("theory::arrays::callsMergeInfo",0),
 141     d_maxList("theory::arrays::maxList",0),
 142     d_tableSize("theory::arrays::infoTableSize", info_map) {
 143   currentStatisticsRegistry()->registerStat(&d_mergeInfoTimer);
 144   currentStatisticsRegistry()->registerStat(&d_avgIndexListLength);
 145   currentStatisticsRegistry()->registerStat(&d_avgStoresListLength);
 146   currentStatisticsRegistry()->registerStat(&d_avgInStoresListLength);
 147   currentStatisticsRegistry()->registerStat(&d_listsCount);
 148   currentStatisticsRegistry()->registerStat(&d_callsMergeInfo);
 149   currentStatisticsRegistry()->registerStat(&d_maxList);
 150   currentStatisticsRegistry()->registerStat(&d_tableSize);
 151   }*/
 152
 153   ArrayInfo(context::Context* c, Backtracker<TNode>* b, std::string statisticsPrefix = "");
 154
 155   ~ArrayInfo();
 156
 157   /**
 158    * adds the node a to the map if it does not exist
 159    * and it initializes the info. checks for duplicate i's
 160    */
 161   void addIndex(const Node a, const TNode i);
 162   void addStore(const Node a, const TNode st);
 163   void addInStore(const TNode a, const TNode st);
 164
 165   void setNonLinear(const TNode a);
 166   void setRIntro1Applied(const TNode a);
 167   void setModelRep(const TNode a, const TNode rep);
 168
 169   void setConstArr(const TNode a, const TNode constArr);
 170   void setWeakEquivPointer(const TNode a, const TNode pointer);
 171   void setWeakEquivIndex(const TNode a, const TNode index);
 172   void setWeakEquivSecondary(const TNode a, const TNode secondary);
 173   void setWeakEquivSecondaryReason(const TNode a, const TNode reason);
 174   /**
 175    * Returns the information associated with TNode a
 176    */
 177
 178   const Info* getInfo(const TNode a) const;
 179
 180   const bool isNonLinear(const TNode a) const;
 181
 182   const bool rIntro1Applied(const TNode a) const;
 183
 184   const TNode getModelRep(const TNode a) const;
 185
 186   const TNode getConstArr(const TNode a) const;
 187   const TNode getWeakEquivPointer(const TNode a) const;
 188   const TNode getWeakEquivIndex(const TNode a) const;
 189   const TNode getWeakEquivSecondary(const TNode a) const;
 190   const TNode getWeakEquivSecondaryReason(const TNode a) const;
 191
 192   const CTNodeList* getIndices(const TNode a) const;
 193
 194   const CTNodeList* getStores(const TNode a) const;
 195
 196   const CTNodeList* getInStores(const TNode a) const;
 197
 198   /**
 199    * merges the information of  nodes a and b
 200    * the nodes do not have to actually be in the map.
 201    * pre-condition
 202    *  a should be the canonical representative of b
 203    */
 204   void mergeInfo(const TNode a, const TNode b);
 205 };/* class ArrayInfo */
 206
 207 }  // namespace arrays
 208 }  // namespace theory
 209 }  // namespace cvc5
 210
 211 #endif /* CVC5__THEORY__ARRAYS__ARRAY_INFO_H */