Merged my changes from experimental branch (new array decision procedure,

translation to bit-vectors for QF_NIA).

1 files changed, 15 insertions, 11 deletions

diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 6a023c282..28d994835 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -257,6 +257,15 @@ class TheoryArrays : public Theory {
 
   private:
 
+  TNode weakEquivGetRep(TNode node);
+  TNode weakEquivGetRepIndex(TNode node, TNode index);
+  void visitAllLeaves(TNode reason, std::vector<TNode>& conjunctions);
+  void weakEquivBuildCond(TNode node, TNode index, std::vector<TNode>& conjunctions);
+  void weakEquivMakeRep(TNode node);
+  void weakEquivMakeRepIndex(TNode node);
+  void weakEquivAddSecondary(TNode index, TNode arrayFrom, TNode arrayTo, TNode reason);
+  void checkWeakEquiv(bool arraysMerged);
+
   // NotifyClass: template helper class for d_equalityEngine - handles call-back from congruence closure module
   class NotifyClass : public eq::EqualityEngineNotify {
     TheoryArrays& d_arrays;
@@ -394,6 +403,12 @@ class TheoryArrays : public Theory {
   typedef context::CDHashMap<Node,Node,NodeHashFunction> DefValMap;
   DefValMap d_defValues;
 
+  typedef std::hash_map<std::pair<TNode, TNode>, CTNodeList*, TNodePairHashFunction> ReadBucketMap;
+  ReadBucketMap d_readBucketTable;
+  context::Context* d_readTableContext;
+  context::CDList<Node> d_arrayMerges;
+  std::vector<CTNodeList*> d_readBucketAllocations;
+
   Node getSkolem(TNode ref, const std::string& name, const TypeNode& type, const std::string& comment, bool makeEqual = true);
   Node mkAnd(std::vector<TNode>& conjunctions, bool invert = false, unsigned startIndex = 0);
   void setNonLinear(TNode a);
@@ -411,17 +426,6 @@ class TheoryArrays : public Theory {
   std::vector<Node> d_decisions;
   bool d_inCheckModel;
   int d_topLevel;
-  void convertNodeToAssumptions(TNode node, std::vector<TNode>& assumptions, TNode nodeSkip);
-  void preRegisterStores(TNode s);
-  void checkModel(Effort e);
-  bool hasLoop(TNode node, TNode target);
-  typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
-  NodeMap d_getModelValCache;
-  NodeMap d_lastVal;
-  Node getModelVal(TNode node);
-  Node getModelValRec(TNode node);
-  bool setModelVal(TNode node, TNode val, bool invert,
-                   bool explain, std::vector<TNode>& assumptions);
 
   public: