Improvement. If refinement is disabled, and the number of array reads is small, then...

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1440 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/src/AST/AST.h b/src/AST/AST.h
index bd5be699c57457bd669186c526ce6d9254547009..81ed69b2007f0c4d287883d500530399bdab64ae 100644 (file)
--- a/src/AST/AST.h
+++ b/src/AST/AST.h
@@ -27,6 +27,7 @@ namespace BEEV
   bool isAtomic(Kind k);
   bool isCommutative(const Kind k);
   bool containsArrayOps(const ASTNode&n);
+  bool  numberOfReadsLessThan(const ASTNode&n, int v);
 
   // If (a > b) in the termorder, then return 1 elseif (a < b) in the
   // termorder, then return -1 else return 0

diff --git a/src/AST/ASTmisc.cpp b/src/AST/ASTmisc.cpp
index 94f95a9e75597d1553f4499b8d5505d122b6df2c..84c1da06b0e3818a8f623633cc85b1d3ba668c19 100644 (file)
--- a/src/AST/ASTmisc.cpp
+++ b/src/AST/ASTmisc.cpp
@@ -63,6 +63,39 @@ namespace BEEV
   } //end of arithless
 
 
+  // counts the number of reads. Shortcut when we get to the limit.
+  void
+  numberOfReadsLessThan(const ASTNode& n, hash_set<int> & visited, int& soFar, const int limit)
+  {
+    if (n.isAtom())
+      return;
+
+    if (visited.find(n.GetNodeNum()) != visited.end())
+      return;
+
+    if (n.GetKind() == READ)
+      soFar++;
+
+    if (soFar > limit)
+      return;
+
+    visited.insert(n.GetNodeNum());
+
+    for (int i = 0; i < n.Degree(); i++)
+      numberOfReadsLessThan(n[i], visited, soFar,limit);
+  }
+
+  // True if the number of reads in "n" is less than "limit"
+  bool
+  numberOfReadsLessThan(const ASTNode&n, int limit)
+  {
+    hash_set<int> visited;
+    int reads = 0;
+    numberOfReadsLessThan(n, visited, reads,limit);
+    return reads < limit;
+  }
+
+
 bool containsArrayOps(const ASTNode& n, hash_set<int> & visited)
 {
         if (n.GetIndexWidth() > 0)

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index a4d585cc7a22547629ad38efca45a599293cdbe1..084a1f6c2880151a0ff3a526ebf7ca69947ce5ba 100644 (file)
--- a/src/STPManager/STP.cpp
+++ b/src/STPManager/STP.cpp
@@ -205,10 +205,29 @@ namespace BEEV {
     // A heap object so I can easily control its lifetime.
     BVSolver* bvSolver = new BVSolver(bm, simp);
 
-    const bool arrayops = containsArrayOps(original_input);
+    ASTNode simplified_solved_InputToSAT = original_input;
+
+    // If the number of array reads is small. We rewrite them through.
+    // The bit-vector simplifications are more thorough than the array simplifications. For example,
+    // we don't currently do unconstrained elimination on arrays--- but we do for bit-vectors.
+    // A better way to do this would be to estimate the number of axioms introduced.
+    // TODO: Should be enabled irrespective of whether refinement is enabled.
+    // TODO: I chose the number of reads we perform this operation at randomly.
+    bool removed = false;
+    if (!bm->UserFlags.arrayread_refinement_flag && numberOfReadsLessThan(simplified_solved_InputToSAT,50))
+      {
+          // If the number of axioms that would be added it small. Remove them.
+              simplified_solved_InputToSAT = arrayTransformer->TransformFormula_TopLevel(simplified_solved_InputToSAT);
+              if (bm->UserFlags.stats_flag)
+                cerr << "Have removed array operations" << endl;
+              removed = true;
+      }
+
+    const bool arrayops = containsArrayOps(simplified_solved_InputToSAT);
+    if (removed)
+      assert(!arrayops);
 
     // Run size reducing just once.
-    ASTNode simplified_solved_InputToSAT = original_input;
     simplified_solved_InputToSAT = sizeReducing(simplified_solved_InputToSAT, bvSolver);
 
     unsigned initial_difficulty_score = difficulty.score(simplified_solved_InputToSAT);