Improvement. The bitblaster now handled signed div/mod/rem. They don't need to be...

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

diff --git a/src/AST/ArrayTransformer.cpp b/src/AST/ArrayTransformer.cpp
index 42eb09e2e8edb0ad70f204bee2f3be76a1891684..0507c7a44fd4d21843d0a47161474f4cde6b6bd3 100644 (file)
--- a/src/AST/ArrayTransformer.cpp
+++ b/src/AST/ArrayTransformer.cpp
@@ -35,7 +35,7 @@ namespace BEEV
     TransformMap = new ASTNodeMap(100);
     ASTNode result = TransformFormula(form);
 
-#ifndef NDEBUG
+#if 0
     {
        ASTNodeSet visited;
        assertTransformPostConditions(result,visited);
@@ -49,7 +49,6 @@ namespace BEEV
     if (bm->UserFlags.stats_flag)
       printArrayStats();
 
-
     // This establishes equalities between every indexes, and a fresh variable.
     if (!bm->UserFlags.ackermannisation)
     {
@@ -271,11 +270,6 @@ namespace BEEV
 
     const Kind k = term.GetKind();
 
-    // Check the signed operations have been removed.
-    assert( SBVDIV != k);
-    assert( SBVMOD != k);
-    assert( SBVREM !=k);
-
     // Check the array reads / writes have been removed
     assert( READ !=k );
     assert( WRITE !=k);
@@ -488,19 +482,6 @@ namespace BEEV
           }
           else
                  result = term;
-
-              if (SBVDIV == result.GetKind() 
-                  || SBVREM == result.GetKind() 
-                  || SBVMOD == result.GetKind())
-                {
-                  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/NodeFactory/SimplifyingNodeFactory.cpp b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
index 2c0379ad7041e013ac63bde3535ee6cd2c1c1955..45871f3bdf0ba8b789926873ce9c3d3f872ff539 100644 (file)
--- a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
+++ b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
@@ -50,8 +50,6 @@ using BEEV::BVDIV;
 
 static bool debug_simplifyingNodeFactory = false;
 
-static const bool translate_signed = true;
-
 ASTNode
 SimplifyingNodeFactory::CreateNode(Kind kind, const ASTVec & children)
 {
@@ -1311,8 +1309,6 @@ SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width, const ASTVec &
       result = bm.CreateZeroConst(width);
     else if (children[1].GetKind() == BVUMINUS && children[1][0] == children[0])
       result = bm.CreateZeroConst(width);
-    else if (translate_signed)
-      result = BEEV::ArrayTransformer::TranslateSignedDivModRem(hashing.CreateTerm(kind, width, children), this, &bm);
     break;
 
   case BEEV::BVDIV:
@@ -1350,8 +1346,6 @@ SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width, const ASTVec &
           bm.CreateOneConst(width), bm.CreateZeroConst(width));
     if (children[1].isConstant() && CONSTANTBV::BitVector_is_full(children[1].GetBVConst()))
       result = NodeFactory::CreateTerm(BVUMINUS, width, children[0]);
-    else if (translate_signed)
-      result = BEEV::ArrayTransformer::TranslateSignedDivModRem(hashing.CreateTerm(kind, width, children), this, &bm);
     break;
 
   case SBVREM:
@@ -1369,8 +1363,6 @@ SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width, const ASTVec &
       result = NodeFactory::CreateTerm(SBVREM, width, children[0], children[1][0]);
     else if (children[0].GetKind() == BVUMINUS && children[0][0] == children[1])
       result = bm.CreateZeroConst(width);
-    else if (translate_signed)
-      result = BEEV::ArrayTransformer::TranslateSignedDivModRem(hashing.CreateTerm(kind, width, children), this, &bm);
     break;
 
   case BEEV::BVMOD:

diff --git a/src/simplifier/constantBitP/ConstantBitPropagation.cpp b/src/simplifier/constantBitP/ConstantBitPropagation.cpp
index ae229898138220f03afae10f3ccaa57cd98ce70e..0190a567ce29f3687d29da2f622c719eb410ed88 100644 (file)
--- a/src/simplifier/constantBitP/ConstantBitPropagation.cpp
+++ b/src/simplifier/constantBitP/ConstantBitPropagation.cpp
@@ -742,15 +742,12 @@ namespace simplifier
           result = bvSignedRemainderBothWays(children, output, n.GetSTPMgr());
           mult_like=true;
         }
-
-      // This propagator is very slow. It needs to be reimplemented.
-      #if 0
       else if (k == SBVMOD)
         {
-          result = bvSignedModulusBothWays(children, output, n.GetSTPMgr());
+          // This propagator is very slow. It needs to be reimplemented.
+          //result = bvSignedModulusBothWays(children, output, n.GetSTPMgr());
           mult_like=true;
         }
-      #endif
       else
 
 

diff --git a/src/to-sat/BitBlaster.cpp b/src/to-sat/BitBlaster.cpp
index dc798f2379ad9c0e9c3aae8032bedec7a86f08ba..959566333e51eca5edb94bfeca065beddc67ab4e 100644 (file)
--- a/src/to-sat/BitBlaster.cpp
+++ b/src/to-sat/BitBlaster.cpp
@@ -15,6 +15,7 @@
 #include "../simplifier/constantBitP/ConstantBitPropagation.h"
 #include "../simplifier/constantBitP/NodeToFixedBitsMap.h"
 #include "../simplifier/simplifier.h"
+#include "../AST/ArrayTransformer.h"
 
 namespace BEEV
 {
@@ -347,6 +348,8 @@ namespace BEEV
 
       if (n.isConstant())
         {
+        // This doesn't hold any longer because we convert BVSDIV and friends to ASTNodes.
+#if 0
         simplifier::constantBitP::NodeToFixedBitsMap::NodeToFixedBitsMapType::const_iterator it;
         it = cb->fixedMap->map->find(n);
         if (it == cb->fixedMap->map->end())
@@ -354,6 +357,7 @@ namespace BEEV
           cerr << n;
           assert(it != cb->fixedMap->map->end());
           }assert(it->second->isTotallyFixed());
+#endif
         return;
         }
 
@@ -829,6 +833,15 @@ namespace BEEV
         result = BBMult(mpcd1, mpcd2, support, term);
         break;
         }
+      case SBVREM:
+      case SBVMOD:
+      case SBVDIV:
+        {
+        ASTNode p = ArrayTransformer::TranslateSignedDivModRem(term,ASTNF,term.GetSTPMgr());
+        result = BBTerm(p,support);
+        break;
+        }
+
       case BVDIV:
       case BVMOD:
         {