From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Wed, 7 Jul 2010 13:17:57 +0000 (+0000)
Subject: Simplify (bvdiv x x ) to one. Likewise for the other multiplication like operations.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=3687628da66800a4a63cd5ea9e758be50bde9053;p=francis%2Fstp.git

Simplify (bvdiv x x ) to one. Likewise for the other multiplication like operations.

Other changes are for constant bit propagation (aren't active yet).




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

diff --git a/src/main/main.cpp b/src/main/main.cpp
index 04098e7..1893f57 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -106,8 +106,12 @@ int main(int argc, char ** argv) {
     "-c  : construct counterexample\n";
   helpstring +=  
     "-d  : check counterexample\n";
+
+#ifdef WITHCBITP
   helpstring +=  
       "--disable-cbitp  : disable constant bit propagation\n";
+#endif WITHCBITP
+
   helpstring +=
     "-e  : expand finite-for construct\n";
   helpstring +=  
diff --git a/src/simplifier/constantBitP/ConstantBitPropagation.cpp b/src/simplifier/constantBitP/ConstantBitPropagation.cpp
index 493d7fc..b048e70 100644
--- a/src/simplifier/constantBitP/ConstantBitPropagation.cpp
+++ b/src/simplifier/constantBitP/ConstantBitPropagation.cpp
@@ -1,11 +1,10 @@
+#include "ConstantBitPropagation.h"
 #include "../../AST/AST.h"
 #include "../../extlib-constbv/constantbv.h"
 #include "../../printer/printers.h"
-#include "ConstantBitPropagation.h"
 #include "../../AST/NodeFactory/NodeFactory.h"
 #include "../../simplifier/simplifier.h"
 #include "ConstantBitP_Utility.h"
-#include "MultiplicationStats.h"
 
 #ifdef WITHCBITP
   #include "ConstantBitP_TransferFunctions.h"
@@ -166,6 +165,13 @@ namespace simplifier
       // not fixing the topnode.
       propagate();
 
+      if (debug_cBitProp_messages)
+        {
+          cerr << "status:" << status <<endl;
+          cerr << "ended propagation" << endl;
+          printNodeWithFixings();
+        }
+
       // is there are good reason to clear out some of them??
 #if 0
       // remove constants, and things with nothing fixed.
@@ -212,16 +218,16 @@ namespace simplifier
 
       if (debug_cBitProp_messages)
         {
-          cout << "Number removed by bottom UP:" << fromTo.size() << endl;
+          cerr << "Number removed by bottom UP:" << fromTo.size() << endl;
         }
 
       setNodeToTrue(top);
 
       if (debug_cBitProp_messages)
         {
-          cout << "starting propagation" << endl;
+          cerr << "starting propagation" << endl;
           printNodeWithFixings();
-          cout << "Initial Tree:" << endl;
+          cerr << "Initial Tree:" << endl;
           cerr << top;
         }
 
@@ -346,10 +352,9 @@ namespace simplifier
     notHandled(const Kind& k)
     {
       if (READ != k && WRITE != k)
-      //if (debug_cBitProp_messages)
-
+      if (debug_cBitProp_messages)
         {
-          cout << "!" << k << endl;
+          cerr << "!" << k << endl;
         }
     }
 
diff --git a/src/simplifier/constantBitP/ConstantBitPropagation.h b/src/simplifier/constantBitP/ConstantBitPropagation.h
index 4a3d0b1..d9b62b5 100644
--- a/src/simplifier/constantBitP/ConstantBitPropagation.h
+++ b/src/simplifier/constantBitP/ConstantBitPropagation.h
@@ -5,6 +5,7 @@
 #include "Dependencies.h"
 #include "NodeToFixedBitsMap.h"
 #include "WorkList.h"
+#include "MultiplicationStats.h"
 
 namespace BEEV
 {
@@ -18,18 +19,6 @@ namespace simplifier
   namespace constantBitP
   {
 
-    enum Direction
-    {
-      UPWARDS_ONLY, BOTH_WAYS
-    };
-
-    // This is used for very specific purposes.
-    enum Type
-    {
-      BOOL_TYPE, VALUE_TYPE
-    };
-
-    // The only status that's correctly maintained at present is the conflict status.
     enum Result
     {
       NO_CHANGE = 1, CHANGED, CONFLICT, NOT_IMPLEMENTED
@@ -44,11 +33,11 @@ namespace simplifier
     class ConstantBitPropagation
     {
       NodeFactory *nf;
+      Simplifier *simplifier;
 
       Result status;
       WorkList *workList;
       Dependencies * dependents;
-      Simplifier *simplifier;
       MultiplicationStatsMap* msm;
 
       void
@@ -74,28 +63,9 @@ public:
       // propagates.
       ConstantBitPropagation(BEEV::Simplifier* _sm, NodeFactory* _nf, const ASTNode & top);
 
-      /*
-      ConstantBitPropagation(BEEV::Simplifier* _sm, NodeFactory* _nf)
-      {
-        status = NO_CHANGE;
-
-        workList = NULL;
-        dependents = NULL;
-        fixedMap = NULL; // ASTNodes mapped to which of their bits are fixed.
-        msm = NULL;
-
-        simplifier = _sm;
-        nf = _nf;
-      }
-      ;
-       */
-
-
       ~ConstantBitPropagation()
       {
-          delete fixedMap;
-          delete dependents;
-          delete workList;
+        clearTables();
       }
       ;
 
@@ -104,6 +74,17 @@ public:
       topLevelBothWays(const BEEV::ASTNode& top);
 
 
+      void clearTables()
+      {
+        delete fixedMap;
+        fixedMap = NULL;
+        delete dependents;
+        dependents = NULL;
+        delete workList;
+        workList = NULL;
+        delete msm;
+        msm = NULL;
+      }
 
       bool
       checkAtFixedPoint(const ASTNode& n, BEEV::ASTNodeSet & visited);
diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index 5fab425..93cee1e 100644
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -2577,8 +2577,25 @@ namespace BEEV
         }
         break;
 
+      case BVDIV:
+      if (inputterm[0] == inputterm[1])
+        {
+          output = _bm->CreateOneConst(inputValueWidth);
+          break;
+        }
+      output = inputterm;
+      break;
+
+    case BVMOD:
+      if (inputterm[0] == inputterm[1])
+        {
+          output = _bm->CreateZeroConst(inputValueWidth);
+          break;
+        }
+      output = inputterm;
+      break;
 
-      case BVXOR:
+    case BVXOR:
     	  {
     		  if (inputterm.Degree() ==2 && inputterm[0] == inputterm[1])
     		  {
@@ -2592,8 +2609,6 @@ namespace BEEV
       case BVNOR:
       case BVVARSHIFT:
       case BVSRSHIFT:
-      case BVDIV:
-      case BVMOD:
         {
           ASTVec c = inputterm.GetChildren();
           ASTVec o;
@@ -2670,9 +2685,25 @@ namespace BEEV
           break;
         }
       case SBVREM:
-      case SBVDIV:
       case SBVMOD:
         {
+          if (inputterm[0] == inputterm[1])
+          {
+            output = _bm->CreateZeroConst(inputValueWidth);
+            break;
+          }
+
+          // run on.
+        }
+      case SBVDIV:
+        {
+          if (inputterm[0] == inputterm[1])
+          {
+            output = _bm->CreateOneConst(inputValueWidth);
+            break;
+          }
+
+
           ASTVec c = inputterm.GetChildren();
           ASTVec o;
           for (ASTVec::iterator
diff --git a/src/to-sat/AIG/ToSATAIG.cpp b/src/to-sat/AIG/ToSATAIG.cpp
index ad8c8f4..88c21df 100644
--- a/src/to-sat/AIG/ToSATAIG.cpp
+++ b/src/to-sat/AIG/ToSATAIG.cpp
@@ -40,6 +40,9 @@ namespace BEEV
         }
       */
 
+      //Clear out all the constant bit stuff before sending the SAT.
+      cb->clearTables();
+
       bm->GetRunTimes()->start(RunTimes::SendingToSAT);
 
       for (int i = 0; i < cnfData->nVars; i++)