Improvement. The start of an unsigned interval simplification.

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

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index c7f137a4e974763e5ed2c7ba4f9338975c152d60..cb453718823517dccaff68724cbd4f7c481ce252 100644 (file)
--- a/src/STPManager/STP.cpp
+++ b/src/STPManager/STP.cpp
@@ -17,6 +17,7 @@
 #include "../sat/CryptoMinisat.h"
 #include "../simplifier/RemoveUnconstrained.h"
 #include "../simplifier/FindPureLiterals.h"
+#include "../simplifier/EstablishIntervals.h"
 #include <memory>
 
 namespace BEEV {
@@ -170,9 +171,14 @@ namespace BEEV {
 
         if (cb.isUnsatisfiable())
           simplified_solved_InputToSAT = bm->ASTFalse;
-
       }
 
+    {
+      EstablishIntervals intervals(*bm);
+      simplified_solved_InputToSAT = intervals.topLevel_unsignedIntervals(simplified_solved_InputToSAT );
+    }
+
+
     // Find pure literals.
         if (bm->UserFlags.isSet("pure-literals","1"))
         {
@@ -212,7 +218,7 @@ namespace BEEV {
             bm->ASTNodeStats("after pure substitution: ",
                              simplified_solved_InputToSAT);
 
-            simplified_solved_InputToSAT = 
+            simplified_solved_InputToSAT =
               simp->SimplifyFormula_TopLevel(simplified_solved_InputToSAT, 
                                              false);
             bm->ASTNodeStats("after simplification: ", 
@@ -236,13 +242,14 @@ namespace BEEV {
 
     if (bm->UserFlags.isSet("enable-unconstrained","1"))
       {
-    // Remove unconstrained.
-    RemoveUnconstrained r(*bm);
-    simplified_solved_InputToSAT = r.topLevel(simplified_solved_InputToSAT, simp);
-    bm->ASTNodeStats("After Unconstrained Remove begins: ",
-            simplified_solved_InputToSAT);
+        // Remove unconstrained.
+        RemoveUnconstrained r(*bm);
+        simplified_solved_InputToSAT = r.topLevel(simplified_solved_InputToSAT, simp);
+        bm->ASTNodeStats("After Unconstrained Remove begins: ",
+                simplified_solved_InputToSAT);
       }
 
+
     bm->TermsAlreadySeenMap_Clear();
 
     bm->start_abstracting = false;

diff --git a/src/simplifier/EstablishIntervals.cpp b/src/simplifier/EstablishIntervals.cpp
new file mode 100644 (file)
index 0000000..eafde83
--- /dev/null
+++ b/src/simplifier/EstablishIntervals.cpp
@@ -0,0 +1,8 @@
+#include "EstablishIntervals.h"
+namespace BEEV
+{
+
+  vector<EstablishIntervals::IntervalType * > EstablishIntervals::toDeleteLater;
+  vector<CBV> EstablishIntervals::likeAutoPtr;
+
+};

diff --git a/src/simplifier/EstablishIntervals.h b/src/simplifier/EstablishIntervals.h
new file mode 100644 (file)
index 0000000..dff603d
--- /dev/null
+++ b/src/simplifier/EstablishIntervals.h
@@ -0,0 +1,169 @@
+/*
+ * Performs a very basic unsigned interval analysis.
+ * Currently it only has a couple of basic operations.
+ */
+
+#ifndef ESTABLISHINTERVALS_H_
+#define ESTABLISHINTERVALS_H_
+#include "../AST/AST.h"
+#include "../STPManager/STPManager.h"
+#include "simplifier.h"
+
+
+namespace BEEV
+{
+
+  class EstablishIntervals
+  {
+  public:
+    struct IntervalType
+    {
+      CBV minV;
+      CBV maxV;
+      IntervalType(CBV _min, CBV _max)
+      {
+        minV = _min;
+        maxV = _max;
+      }
+
+      void print()
+      {
+        cout << *(minV) << " " << *(maxV) << endl;
+      }
+    };
+
+    static vector<IntervalType * > toDeleteLater;
+    static vector<CBV> likeAutoPtr;
+
+private:
+
+    IntervalType * freshUnsignedInterval(int width)
+    {
+      IntervalType *it = createInterval(makeCBV(width), makeCBV(width));
+      CONSTANTBV::BitVector_Fill(it->maxV);
+      return it;
+    }
+
+    static IntervalType * createInterval(CBV min, CBV max)
+    {
+      IntervalType *it = new IntervalType(min,max);
+      toDeleteLater.push_back(it);
+      return it ;
+    }
+
+    CBV makeCBV(int width)
+    {
+        CBV result = CONSTANTBV::BitVector_Create(width, true);
+        likeAutoPtr.push_back(result);
+        return result;
+    }
+
+
+  public:
+    // Replace some of the things that unsigned intervals can figure out for us.
+    ASTNode topLevel_unsignedIntervals(const ASTNode&top)
+    {
+      map<const ASTNode, IntervalType*> visited;
+      visit(top,visited);
+      ASTNodeMap fromTo;
+      for (map<const ASTNode, IntervalType*>::const_iterator it = visited.begin(); it != visited.end(); it++)
+      {
+          const ASTNode& n = it->first;
+          IntervalType *interval = it->second;
+
+          if (interval == NULL)
+            continue;
+          if (n.isConstant())
+            continue;
+          if (interval->maxV == interval->minV && n.GetType() == BOOLEAN_TYPE)
+            {
+              if (0== CONSTANTBV::BitVector_Lexicompare(interval->maxV,littleOne))
+                fromTo.insert(make_pair(n,bm.ASTTrue));
+                else
+                  fromTo.insert(make_pair(n,bm.ASTFalse));
+            }
+      }
+
+      if (fromTo.size() > 0)
+        {
+          //cerr << "intervals found" << fromTo.size() << endl;
+          ASTNodeMap cache;
+          return SubstitutionMap::replace(top,fromTo,cache,bm.defaultNodeFactory);
+        }
+
+      return top;
+    }
+
+  private:
+    // A single pass through the problem replacing things that must be true of false.
+    IntervalType* visit(const ASTNode& n, map<const ASTNode, IntervalType*> & visited)
+    {
+      if (visited.find(n) != visited.end())
+        return visited.find(n)->second;
+
+      vector<IntervalType* > children_intervals;
+      children_intervals.reserve(n.Degree());
+      for (int i=0; i < n.Degree();i++)
+        {
+          children_intervals.push_back(visit(n[i],visited));
+        }
+
+      IntervalType * result = NULL;
+
+      if (BVCONST == n.GetKind() || BITVECTOR == n.GetKind())       // If it's a constant, make it.
+        {
+          // the CBV doesn't leak. it is a copy of the cbv inside the node.
+          CBV cbv = n.GetBVConst();
+          result = createInterval(cbv,cbv);
+        }
+      else if (BVGE == n.GetKind() && children_intervals[0] != NULL && children_intervals[1] != NULL)
+        {
+          if (CONSTANTBV::BitVector_Lexicompare(children_intervals[0]->minV,children_intervals[1]->maxV) >=0)
+            result = createInterval(littleOne, littleOne);
+        }
+      else if (BVMOD == n.GetKind() && children_intervals[1] != NULL)
+        {
+          // When we're dividing by zero, we know nothing.
+          if (!CONSTANTBV::BitVector_is_empty(children_intervals[1]->maxV))
+            {
+              result = freshUnsignedInterval(n.GetValueWidth());
+              CONSTANTBV::BitVector_Copy(result->maxV , children_intervals[1]->maxV);
+              CONSTANTBV::BitVector_decrement(result->maxV);
+            }
+        }
+
+      // result will often be null (which we take to mean the maximum range).
+        visited.insert(make_pair(n,result));
+        return result;
+    }
+
+    STPMgr& bm;
+    CBV littleOne;
+    CBV littleZero;
+  public:
+    EstablishIntervals(STPMgr& _bm) : bm(_bm)
+    {
+      littleZero = makeCBV(1);
+      littleOne = makeCBV(1);
+      CONSTANTBV::BitVector_Fill(littleOne);
+    }
+
+    ~EstablishIntervals()
+    {
+      for (int i =0; i < toDeleteLater.size();i++)
+        delete toDeleteLater[i];
+
+      for (int i =0; i < likeAutoPtr.size();i++)
+        CONSTANTBV::BitVector_Destroy(likeAutoPtr[i]);
+
+      likeAutoPtr.clear();
+      toDeleteLater.clear();
+    }
+
+
+
+
+  };
+}
+;
+#endif /* ESTABLISHINTERVALS_H_ */