Improvements the the code for measuring the effect of propagators.

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

diff --git a/src/util/Relations.cpp b/src/util/Relations.cpp
new file mode 100644 (file)
index 0000000..6464497
--- /dev/null
+++ b/src/util/Relations.cpp
@@ -0,0 +1,20 @@
+/*
+ * Relations.cpp
+ *
+ *  Created on: 10/04/2012
+ *      Author: thansen
+ */
+
+#include "Relations.h"
+
+Relations::Relations()
+{
+  // TODO Auto-generated constructor stub
+
+}
+
+Relations::~Relations()
+{
+  // TODO Auto-generated destructor stub
+}
+

diff --git a/src/util/Relations.h b/src/util/Relations.h
new file mode 100644 (file)
index 0000000..3b927e8
--- /dev/null
+++ b/src/util/Relations.h
@@ -0,0 +1,80 @@
+/*
+ * Relations.h
+ *
+ *  Created on: 10/04/2012
+ *      Author: thansen
+ */
+
+#ifndef RELATIONS_H_
+#define RELATIONS_H_
+
+#include <ctime>
+#include <vector>
+#include "../AST/AST.h"
+#include "../simplifier/constantBitP/FixedBits.h"
+#include "../simplifier/constantBitP/MersenneTwister.h"
+
+#include "../simplifier/constantBitP/ConstantBitP_TransferFunctions.h"
+#include "../extlib-constbv/constantbv.h"
+
+#include "../AST/ASTKind.h"
+#include "../STPManager/STPManager.h"
+#include "../cpp_interface/cpp_interface.h"
+#include <list>
+
+using namespace std;
+using simplifier::constantBitP::FixedBits;
+using namespace simplifier::constantBitP;
+
+
+struct Relations
+{
+  struct Relation
+  {
+    FixedBits a,b,output;
+    int initial;
+    Relation(FixedBits a_, FixedBits b_, FixedBits output_)
+    : a(a_), b(b_), output(output_)
+    {
+      initial = a.countFixed() + b.countFixed() + output.countFixed();
+    }
+  };
+
+    list<Relation> relations;
+
+    Relations (int iterations, int bitWidth,Kind k, STPMgr*beev, int probabilityOfFixing)
+    {
+      MTRand rand;
+
+      for (int i = 0; i < iterations; i++)
+        {
+        FixedBits a = FixedBits::createRandom(bitWidth, 100, rand);
+        FixedBits b = FixedBits::createRandom(bitWidth, 100, rand);
+
+        assert(a.isTotallyFixed());
+        assert(b.isTotallyFixed());
+        ASTVec c;
+        c.push_back(beev->CreateBVConst(a.GetBVConst(), bitWidth));
+        c.push_back(beev->CreateBVConst(b.GetBVConst(), bitWidth));
+        ASTNode result = NonMemberBVConstEvaluator(beev, k, c, bitWidth);
+        FixedBits output = FixedBits::concreteToAbstract(result);
+
+        for (int i = 0; i < a.getWidth(); i++)
+          {
+          if (rand.randInt() % 100 >= probabilityOfFixing)
+            a.setFixed(i, false);
+          if (rand.randInt() % 100 >= probabilityOfFixing)
+            b.setFixed(i, false);
+          }
+        for (int i = 0; i < output.getWidth(); i++)
+          if (rand.randInt() % 100 >= probabilityOfFixing)
+            output.setFixed(i, false);
+
+        Relation r(a, b, output);
+        relations.push_back(r);
+        }
+    }
+};
+
+
+#endif /* RELATIONS_H_ */

diff --git a/src/util/StopWatch.h b/src/util/StopWatch.h
new file mode 100644 (file)
index 0000000..f00a4b4
--- /dev/null
+++ b/src/util/StopWatch.h
@@ -0,0 +1,36 @@
+/*
+ * StopWatch.h
+ *
+ *  Created on: 10/04/2012
+ *      Author: thansen
+ */
+
+#ifndef STOPWATCH_H_
+#define STOPWATCH_H_
+
+#include <ctime>
+
+class Stopwatch
+{
+public:
+        Stopwatch() :
+                start(std::clock())
+        {
+        }
+        void stop()
+        {
+                clock_t total = clock() - start;
+                cerr << "ticks: " << total << " " << (float(total) / CLOCKS_PER_SEC) << "s" << endl;
+        }
+        clock_t stop2()
+        {
+                clock_t total = clock() - start;
+                return total;
+        }
+
+private:
+        std::clock_t start;
+};
+
+
+#endif /* STOPWATCH_H_ */

diff --git a/src/util/test_cbitp.cpp b/src/util/test_cbitp.cpp
index 0da4c9efd4cd5a2fe775f6a4584383d9bfc35e3e..1c5198850a7ba96ca3763ef0596a273cfadfa322 100644 (file)
--- a/src/util/test_cbitp.cpp
+++ b/src/util/test_cbitp.cpp
@@ -21,6 +21,9 @@
 #include "../STPManager/STP.h"
 #include "../cpp_interface/cpp_interface.h"
 
+#include "StopWatch.h"
+#include "Relations.h"
+
 using simplifier::constantBitP::FixedBits;
 using namespace simplifier::constantBitP;
 
@@ -379,9 +382,6 @@ namespace simplifier
     runSomeRandom(Result
     (*transfer)(vector<FixedBits*>&, FixedBits&), const Kind kind, int prob)
     {
-      MTRand mtrand(1);
-      srand(0);
-
       vector<FixedBits*> children;
 
       int conflicts =0;
@@ -390,36 +390,49 @@ namespace simplifier
       int max =0;
 
       int count = 1000;
-      long st = getCurrentTime();
-          const int width =32;
+      const int width =32;
+
+      Relations r(count,width,kind, beev, prob);
 
-      for (int i = 0; i < count; i++)
+      Stopwatch s;
+      list<Relations::Relation>::iterator it = r.relations.begin();
+      while(it != r.relations.end())
         {
+        Relations::Relation& rel = *it;
+        FixedBits& a = rel.a;
+        FixedBits& b = rel.b;
+        FixedBits& output = rel.output;
+
         children.clear();
-        FixedBits a = FixedBits::createRandom(width, prob, mtrand);
         children.push_back(&a);
-        FixedBits b = FixedBits::createRandom(width, prob, mtrand);
         children.push_back(&b);
-        FixedBits output = FixedBits::createRandom(width, prob, mtrand);
 
         Detail d;
         bool imprecise = false;
         if (kind == BVDIV || kind == BVMULT || kind == BVMOD || kind == SBVDIV || kind == SBVREM)
           imprecise = true;
         checkEqual(children, output, transfer, kind, imprecise,d);
-        if (d.conflict)
-          conflicts++;
-        else
-          {
-            initial += d.initial;
-            transferC += d.transferFixed;
-            max += d.maxFixed;
-          }
+
+        assert(!d.conflicts);
+
+        initial += d.initial;
+        transferC += d.transferFixed;
+        max += d.maxFixed;
+
+        it++;
         }
 
+      assert(max >= transferC);
+      assert(transferC >= initial);
+
+      int percent = 100* ((float)transferC - initial) / (max - initial);
+      if ((max-initial) ==0)
+        percent = 100;
+      clock_t t = s.stop2();
       cerr.setf(ios::fixed);
       cerr << "% Count" << count << " prob" << prob << " bits" << width << endl;
-      cerr << setprecision(2) << (getCurrentTime() - st)/1000.0 << "s&" << conflicts << "&" << initial << "&" << transferC << "&" << max << endl;
+      cerr << "&" << setprecision(2) << (float(t) / CLOCKS_PER_SEC) << "s";
+      cerr << "&" << initial << "&" << transferC << "&" << max << "&" << percent << "\\%\n" ;
 
       return;
     }
@@ -699,13 +712,35 @@ void
 go(Result (*transfer)(vector<FixedBits*>&, FixedBits&), const Kind kind)
 {
     runSomeRandom(transfer, kind, 1 );
-    cerr << "&";
     runSomeRandom(transfer, kind, 5 );
-    cerr << "&";
     runSomeRandom(transfer, kind, 50 );
     cerr << "\\\\";
 }
 
+void g()
+{
+        FixedBits a(3,false);
+        FixedBits b(3,false);
+        a.setFixed(0,true);
+        a.setValue(0,true);
+
+        b.setFixed(1,true);
+        b.setValue(1,true);
+
+        vector<FixedBits*> c;
+        c.push_back(&a);
+        c.push_back(&b);
+
+        FixedBits output(3,false);
+        output.setFixed(0,true);
+        output.setValue(0,true);
+        output.setFixed(2,true);
+        output.setValue(2,true);
+
+
+        multiply(c,output);
+}
+
 
 int
 main(void)
@@ -727,40 +762,49 @@ main(void)
 
   if (true)
     {
-      output << "bit-vector or&" << endl;
-      go(&bvOrBothWays, BVOR);
+    output << "signed greater than equals" << endl;
+    go(&bvSignedGreaterThanEqualsBothWays, BVSGE);
+
+    output << "unsigned less than" << endl;
+    go(&bvLessThanEqualsBothWays, BVLT);
 
-      output << "bit-vector xor&" << endl;
-      go(&bvXorBothWays, BVXOR);
+    output << "equals" << endl;
+    go(&bvEqualsBothWays, EQ);
+
+    output << "bit-vector xor" << endl;
+    go(&bvXorBothWays, BVXOR);
+
+    output << "bit-vector or" << endl;
+      go(&bvOrBothWays, BVOR);
 
-      output << "bit-vector and&" << endl;
+      output << "bit-vector and" << endl;
       go(&bvAndBothWays, BVAND);
 
-      output << "right shift&" << endl;
+      output << "right shift" << endl;
       go(&bvRightShiftBothWays, BVRIGHTSHIFT);
 
-      output << "left shift&" << endl;
+      output << "left shift" << endl;
       go(&bvLeftShiftBothWays, BVLEFTSHIFT);
 
-      output << "arithmetic shift&" << endl;
+      output << "arithmetic shift" << endl;
       go(&bvArithmeticRightShiftBothWays, BVSRSHIFT);
 
-      output << "addition&" << endl;
+      output << "addition" << endl;
       go(&bvAddBothWays, BVPLUS);
 
-      output << "multiplication&" << endl;
+      output << "multiplication" << endl;
       go(&multiply, BVMULT);
 
-      output << "unsigned division&" << endl;
+      output << "unsigned division" << endl;
       go(&unsignedDivide, BVDIV);
 
-      output << "unsigned remainder&" << endl;
+      output << "unsigned remainder" << endl;
       go(&unsignedModulus, BVMOD);
 
-      output << "signed division&" << endl;
+      output << "signed division" << endl;
       go(&signedDivide, SBVDIV);
 
-      output << "signed remainder&" << endl;
+      output << "signed remainder" << endl;
       go(&signedRemainder, SBVREM);
 
       exit(1);

diff --git a/src/util/time_cbitp.cpp b/src/util/time_cbitp.cpp
index eb4cfb15c91ec2d0e49ea8d1262bf92a8f2d9332..24fc6101d9b755877c0aa318bd1e3e9cc34b5944 100644 (file)
--- a/src/util/time_cbitp.cpp
+++ b/src/util/time_cbitp.cpp
@@ -12,40 +12,20 @@
 #include "../cpp_interface/cpp_interface.h"
 #include <list>
 
+#include "StopWatch.h"
+#include "Relations.h"
+
 using namespace std;
 using simplifier::constantBitP::FixedBits;
 using namespace simplifier::constantBitP;
 
 
-const int iterations = 100000;
+const int iterations = 500000;
 const unsigned bitWidth = 64;
 
 BEEV::STPMgr* beev;
 
 
-class Stopwatch
-{
-public:
-       Stopwatch() :
-               start(std::clock())
-       {
-       }
-       void stop()
-       {
-               clock_t total = clock() - start;
-               cerr << "ticks: " << total << " " << (float(total) / CLOCKS_PER_SEC) << "s" << endl;
-       }
-       clock_t stop2()
-       {
-               clock_t total = clock() - start;
-               return total;
-          //cerr.setf(ios::fixed);
-//             cerr << setprecision(2)  <<  (float(total) / CLOCKS_PER_SEC) << "s";
-       }
-
-private:
-       std::clock_t start;
-};
 
 
 
@@ -146,18 +126,6 @@ void run(Result(*transfer)(vector<FixedBits*>&, FixedBits&), const int probabili
        return;
 }
 
-struct Relation
-{
-  FixedBits a,b,output;
-  int initial;
-  Relation(FixedBits a_, FixedBits b_, FixedBits output_)
-  : a(a_), b(b_), output(output_)
-  {
-    initial = a.countFixed() + b.countFixed() + output.countFixed();
-  }
-
-};
-
 void
 runSimple(Result
 (*transfer)(vector<FixedBits*>&, FixedBits&), const int probabilityOfFixing, ostream& output, Kind k)
@@ -165,47 +133,17 @@ runSimple(Result
 
   int conflicts = 0;
 
-  MTRand rand;
-
   int initially_fixed = 0;
   int finally_fixed = 0;
 
-  list<Relation> relations;
-
-  for (int i = 0; i < iterations; i++)
-    {
-    FixedBits a = FixedBits::createRandom(bitWidth, 100, rand);
-    FixedBits b = FixedBits::createRandom(bitWidth, 100, rand);
-
-    assert(a.isTotallyFixed());
-    assert(b.isTotallyFixed());
-    ASTVec c;
-    c.push_back(beev->CreateBVConst(a.GetBVConst(), bitWidth));
-    c.push_back(beev->CreateBVConst(b.GetBVConst(), bitWidth));
-    ASTNode result = NonMemberBVConstEvaluator(beev, k, c, bitWidth);
-    FixedBits output = FixedBits::concreteToAbstract(result);
-
-    for (int i = 0; i < a.getWidth(); i++)
-      {
-      if (rand.randInt() % 100 >= probabilityOfFixing)
-        a.setFixed(i, false);
-      if (rand.randInt() % 100 >= probabilityOfFixing)
-        b.setFixed(i, false);
-      }
-    for (int i = 0; i < output.getWidth(); i++)
-      if (rand.randInt() % 100 >= probabilityOfFixing)
-        output.setFixed(i, false);
-
-    Relation r(a, b, output);
-    relations.push_back(r);
-    }
+  Relations r(iterations,bitWidth,k, beev, probabilityOfFixing);
 
   Stopwatch s;
 
-  for (int i = 0; i < iterations; i++)
+  list<Relations::Relation>::iterator it = r.relations.begin();
+  while(it != r.relations.end())
     {
-
-    Relation& rel = relations.back();
+    Relations::Relation& rel = *it;
     FixedBits& a = rel.a;
     FixedBits& b = rel.b;
     FixedBits& output = rel.output;
@@ -223,7 +161,7 @@ runSimple(Result
     finally_fixed += final;
     initially_fixed += rel.initial;
 
-    relations.pop_back();
+    it++;
     }
 
   clock_t t = s.stop2();