Remove signed division, modulus and remainder when creating nodes via the simplifying...

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

diff --git a/src/AST/ArrayTransformer.cpp b/src/AST/ArrayTransformer.cpp
index 332fd69844932d70ffddd744ded42811085d0a12..4a8a3bacf92caebf9e0ffe9cdb140fc1e3fb7df0 100644 (file)
--- a/src/AST/ArrayTransformer.cpp
+++ b/src/AST/ArrayTransformer.cpp
@@ -52,7 +52,7 @@ namespace BEEV
   }
 
   //Translates signed BVDIV,BVMOD and BVREM into unsigned variety
-  ASTNode ArrayTransformer::TranslateSignedDivModRem(const ASTNode& in)
+  ASTNode ArrayTransformer::TranslateSignedDivModRem(const ASTNode& in,  NodeFactory* nf, STPMgr *bm)
   {
     assert(in.GetChildren().size() ==2);
 
@@ -99,11 +99,6 @@ namespace BEEV
                          cond_dividend, 
                          nf->CreateTerm(BVUMINUS, len, modnode),
                          modnode);
-
-        //put everything together, simplify, and return
-        if (bm->UserFlags.optimize_flag)
-            return simp->SimplifyTerm_TopLevel(n);
-        else
                return n;
       }
 
@@ -154,9 +149,6 @@ namespace BEEV
                          nf->CreateTerm(BVPLUS, len, rev_node, divisor),
                          rev_node);
 
-        if (bm->UserFlags.optimize_flag)
-            return simp->SimplifyTerm_TopLevel(n);
-        else
                return n;
       }
     else if (SBVDIV == in.GetKind())
@@ -200,15 +192,12 @@ namespace BEEV
                          nf->CreateTerm(BVUMINUS, len, divnode),
                          divnode);
 
-        if (bm->UserFlags.optimize_flag)
-            return simp->SimplifyTerm_TopLevel(n);
-        else
                return n;
       }
 
     FatalError("TranslateSignedDivModRem:"\
                "input must be signed DIV/MOD/REM", in);
-    return ASTUndefined;
+    return bm->ASTUndefined;
 
   }//end of TranslateSignedDivModRem()
 
@@ -452,7 +441,13 @@ namespace BEEV
                   || SBVREM == result.GetKind() 
                   || SBVMOD == result.GetKind())
                 {
-                  result = TranslateSignedDivModRem(result);
+                  ASTNode r = TranslateSignedDivModRem(result,nf,bm);
+                  if (r != result && bm->UserFlags.optimize_flag)
+                    {
+                      result = simp->SimplifyTerm_TopLevel(r);
+                    }
+                  else
+                    result = r;
                 }
         }
         break;

diff --git a/src/AST/ArrayTransformer.h b/src/AST/ArrayTransformer.h
index 660ebd9a8e379204264ec8ead9f2070518ca9971..62d5d1b1b6456ef79ed9d6f390565c406bb403b2 100644 (file)
--- a/src/AST/ArrayTransformer.h
+++ b/src/AST/ArrayTransformer.h
@@ -85,7 +85,6 @@ namespace BEEV
      * Private Member Functions                                     *
      ****************************************************************/
     
-    ASTNode TranslateSignedDivModRem(const ASTNode& in);
     ASTNode TransformTerm(const ASTNode& inputterm);
     void assertTransformPostConditions(const ASTNode & term, ASTNodeSet& visited);
 
@@ -94,6 +93,7 @@ namespace BEEV
     ASTNode TransformFormula(const ASTNode& form);
 
   public:
+    static ASTNode TranslateSignedDivModRem(const ASTNode& in, NodeFactory*nf, STPMgr *bm);
 
     //fill the arrayname_readindices vector if e0 is a READ(Arr,index)
     //and index is a BVCONST

diff --git a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
index a3ef9b9b65a21d62bb3be94a5f0af864976dbe85..0fad7593b1109d06491994ff5da03aec10fe5b81 100644 (file)
--- a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
+++ b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
@@ -25,6 +25,7 @@
 #include <cassert>
 #include "SimplifyingNodeFactory.h"
 #include "../../simplifier/simplifier.h"
+#include "../ArrayTransformer.h"
 #include <cmath>
 
 using BEEV::Kind;
@@ -977,12 +978,14 @@ ASTNode SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width,
         break;
 
        case BEEV::SBVMOD:
-               if (children[1].isConstant() && CONSTANTBV::BitVector_is_empty(
-                               children[1].GetBVConst()))
-                       result = children[0];
-               if (children[0] == children[1])
-                       result = bm.CreateZeroConst(width);
-               break;
+          if (children[1].isConstant() && CONSTANTBV::BitVector_is_empty(
+                          children[1].GetBVConst()))
+                  result = children[0];
+          else if (children[0] == children[1])
+                  result = bm.CreateZeroConst(width);
+          else
+            result = BEEV::ArrayTransformer::TranslateSignedDivModRem(hashing.CreateTerm(kind, width, children),this,&bm);
+          break;
 
 
        case BEEV::BVDIV:
@@ -993,23 +996,27 @@ ASTNode SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width,
         case BEEV::SBVDIV:
           if (children[1].isConstant() && children[1] == bm.CreateOneConst(width))
             result = children[0];
+          else
+            result = BEEV::ArrayTransformer::TranslateSignedDivModRem(hashing.CreateTerm(kind, width, children),this,&bm);
           break;
 
 
        case BEEV::SBVREM:
                if (children[0] == children[1])
                        result = bm.CreateZeroConst(width);
-               if (children[0].isConstant() && CONSTANTBV::BitVector_is_empty(
+               else if (children[0].isConstant() && CONSTANTBV::BitVector_is_empty(
                                children[0].GetBVConst()))
                        result = bm.CreateZeroConst(width);
-               if (children[1].isConstant() && CONSTANTBV::BitVector_is_full(
+               else if (children[1].isConstant() && CONSTANTBV::BitVector_is_full(
                                children[1].GetBVConst()))
                        result = bm.CreateZeroConst(width);
-               if (children[1].isConstant() && CONSTANTBV::BitVector_is_empty(
+               else if (children[1].isConstant() && CONSTANTBV::BitVector_is_empty(
                                children[1].GetBVConst()))
                        result = children[0];
-               if (children[1].isConstant() && bm.CreateOneConst(width) == children[1])
+               else if (children[1].isConstant() && bm.CreateOneConst(width) == children[1])
                        result = bm.CreateZeroConst(width);
+                else
+                  result = BEEV::ArrayTransformer::TranslateSignedDivModRem(hashing.CreateTerm(kind, width, children),this,&bm);
                break;
 
        case BEEV::BVMOD: