Add a simplification so that (ite(p,5,7) <= 8) is always true is detected.

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

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index 7681da8a972e8a381ae1aecdcd1a5fdbbf881a72..f0c9be9263e0e432a9654c9043e1cd8dda80bc65 100644 (file)
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -450,6 +450,62 @@ namespace BEEV
     }
 
 
+    bool getPossibleValues(const ASTNode&n, ASTNodeSet& visited, vector<ASTNode>& found, int maxCount = 15)
+    {
+       if (maxCount <=0)
+               return false;
+
+       ASTNodeSet::iterator it = visited.find(n);
+       if (it != visited.end())
+               return true;
+       visited.insert(n);
+
+       if (n.GetKind() == BVCONST)
+       {
+               found.push_back(n);
+               return true;
+       }
+
+       if (n.GetKind() == ITE)
+       {
+               bool a = getPossibleValues(n[1],visited,found,maxCount-1);
+               if (!a)
+                               return a;
+
+               bool b = getPossibleValues(n[2],visited,found,maxCount-1);
+               if (!b)
+                               return b;
+               return true;
+       }
+
+       return false;
+    }
+
+
+    bool unsignedGreaterThan(const ASTNode& n1, const ASTNode& n2)
+    {
+               assert(n1.isConstant());
+               assert(n2.isConstant());
+               assert(n1.GetValueWidth() == n2.GetValueWidth());
+
+               int comp = CONSTANTBV::BitVector_Lexicompare(n1.GetBVConst(),
+                               n2.GetBVConst());
+               return comp == 1;
+       }
+
+     bool signedGreaterThan(const ASTNode& n1, const ASTNode& n2)
+    {
+               assert(n1.isConstant());
+               assert(n2.isConstant());
+               assert(n1.GetValueWidth() == n2.GetValueWidth());
+
+               int comp = CONSTANTBV::BitVector_Compare(n1.GetBVConst(),
+                               n2.GetBVConst());
+               return comp == 1;
+       }
+
+
+
   ASTNode Simplifier::CreateSimplifiedINEQ(const Kind k_i,
                                            const ASTNode& left_i,
                                            const ASTNode& right_i, bool pushNeg)
@@ -538,6 +594,41 @@ namespace BEEV
        return pushNeg ?  _bm->CreateNode(NOT, status) : status;
     }
 
+    {
+               ASTNodeSet visited0, visited1;
+               vector<ASTNode> l0,l1;
+
+               // Sound overapproximation. Doesn't consider the equalities.
+               if (getPossibleValues(left, visited0, l0) && getPossibleValues(right,visited1, l1))
+               {
+                       {
+                               bool (*comp)(const ASTNode&, const ASTNode&);
+                               if (k == BVSGT || k == BVSGE)
+                                       comp = signedGreaterThan;
+                               else
+                                       comp = unsignedGreaterThan;
+                               {
+                                       ASTNode minLHS = *max_element(l0.begin(), l0.end(),
+                                                       comp);
+                                       ASTNode maxRHS = *min_element(l1.begin(), l1.end(),
+                                                       comp);
+
+                                       if (comp(minLHS, maxRHS))
+                                               return pushNeg ? ASTFalse : ASTTrue;
+                               }
+                               {
+                                       ASTNode maxLHS = *min_element(l0.begin(), l0.end(),
+                                                       comp);
+                                       ASTNode minRHS = *max_element(l1.begin(), l1.end(),
+                                                       comp);
+
+                                       if (comp(minRHS, maxLHS))
+                                               return pushNeg ? ASTTrue : ASTFalse;
+                               }
+                       }
+               }
+       }
+
     const ASTNode unsigned_min = _bm->CreateZeroConst(len);
     const ASTNode one = _bm->CreateOneConst(len);
     const ASTNode unsigned_max = _bm->CreateMaxConst(len);