Fix the utilities for measuring the precision of propagators.

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

diff --git a/src/util/Functions.cpp b/src/util/Functions.cpp
index c3cd3cfee22ff51a2626952f73f465edae9ff4eb..a274478ed36464dadc9ba9c25136c2b53bdb4e74 100644 (file)
--- a/src/util/Functions.cpp
+++ b/src/util/Functions.cpp
@@ -42,3 +42,76 @@ unsignedModulus(vector<FixedBits*>& children, FixedBits& output)
 {
   return bvUnsignedModulusBothWays(children, output, ParserBM);
 }
+
+
+
+int bvOrF(int a, int b)
+{
+  return a | b;
+}
+
+int bvXOrF(int a, int b)
+{
+  return a ^ b;
+}
+
+int bvAndF(int a, int b)
+{
+  return a &b;
+}
+
+int rightSF(int a, int b)
+{
+  if (b >= sizeof(int)*8)
+    return 0;
+
+  return a>>b;
+}
+
+int leftSF(int a, int b)
+{
+  if (b >= sizeof(int)*8)
+    return 0;
+
+  return a<<b;
+}
+
+int plusF(int a, int b)
+{
+  return a+b;
+}
+
+int multiplyF(int a, int b)
+{
+  return a*b;
+}
+
+int divideF(int a, int b)
+{
+  if (b==0)
+    return 1;
+  return a/b;
+}
+
+
+int subF(int a, int b)
+{
+  return a-b;
+}
+
+int eqF(int a, int b)
+{
+  return (a==b)? 1:0;
+}
+
+int ltF(int a, int b)
+{
+  return (a<b)? 1:0;
+}
+
+int remF(int a, int b)
+{
+  if (b ==0)
+    return a;
+  return (a %b);
+}

diff --git a/src/util/Functions.h b/src/util/Functions.h
index 2d8f791db90c0cd004a46e77bcbe3a9510b03cd2..67b99c861aa2660d379776e82b8d3a49a2b828c0 100644 (file)
--- a/src/util/Functions.h
+++ b/src/util/Functions.h
@@ -40,77 +40,20 @@ signedModulus(vector<FixedBits*>& children, FixedBits& output);
 Result
 unsignedModulus(vector<FixedBits*>& children, FixedBits& output);
 
-int bvOrF(int a, int b)
-{
-  return a | b;
-}
-
-int bvXOrF(int a, int b)
-{
-  return a ^ b;
-}
-
-int bvAndF(int a, int b)
-{
-  return a &b;
-}
-
-int rightSF(int a, int b)
-{
-  if (b >= sizeof(int)*8)
-    return 0;
-
-  return a>>b;
-}
-
-int leftSF(int a, int b)
-{
-  if (b >= sizeof(int)*8)
-    return 0;
-
-  return a<<b;
-}
-
-int plusF(int a, int b)
-{
-  return a+b;
-}
-
-int multiplyF(int a, int b)
-{
-  return a*b;
-}
-
-int divideF(int a, int b)
-{
-  if (b==0)
-    return 1;
-  return a/b;
-}
+int bvOrF(int a, int b);
+int bvXOrF(int a, int b);
+int bvAndF(int a, int b);
+int rightSF(int a, int b);
+int leftSF(int a, int b);
+int plusF(int a, int b);
+int multiplyF(int a, int b);
+int divideF(int a, int b);
+int subF(int a, int b);
+int eqF(int a, int b);
+int ltF(int a, int b);
+int remF(int a, int b);
 
 
-int subF(int a, int b)
-{
-  return a-b;
-}
-
-int eqF(int a, int b)
-{
-  return (a==b)? 1:0;
-}
-
-int ltF(int a, int b)
-{
-  return (a<b)? 1:0;
-}
-
-int remF(int a, int b)
-{
-  if (b ==0)
-    return a;
-  return (a %b);
-}
-
 
 struct Functions
 {
@@ -130,6 +73,7 @@ struct Functions
     }
   };
 
+
   std::list<Function> l;
 
   /*
@@ -144,7 +88,7 @@ struct Functions
 
   Functions()
   {
-    //l.push_back(Function(BVSGE, "signed greater than equals", &bvSignedGreaterThanEqualsBothWays));
+    l.push_back(Function(BVSGE, "signed greater than equals", &bvSignedGreaterThanEqualsBothWays, NULL));
     l.push_back(Function(BVLT, "unsigned less than", &bvLessThanBothWays, &ltF));
     l.push_back(Function(EQ, "equals", &bvEqualsBothWays, &eqF));
     l.push_back(Function(BVXOR, "bit-vector xor", &bvXorBothWays, &bvXOrF));
@@ -152,14 +96,14 @@ struct Functions
     l.push_back(Function(BVAND, "bit-vector and", &bvAndBothWays, &bvAndF));
     l.push_back(Function(BVRIGHTSHIFT, "right shift", &bvRightShiftBothWays, &rightSF));
     l.push_back(Function(BVLEFTSHIFT, "left shift", &bvLeftShiftBothWays, &leftSF));
-    //l.push_back(Function(BVSRSHIFT, "arithmetic shift", &bvArithmeticRightShiftBothWays));
+    l.push_back(Function(BVSRSHIFT, "arithmetic shift", &bvArithmeticRightShiftBothWays, NULL));
     l.push_back(Function(BVPLUS, "addition", &bvAddBothWays, &plusF));
     l.push_back(Function(BVSUB, "subtraction", &bvSubtractBothWays, &subF));
     l.push_back(Function(BVMULT, "multiplication", &multiply, &multiplyF));
     l.push_back(Function(BVDIV, "unsigned division", &unsignedDivide, &divideF));
     l.push_back(Function(BVMOD, "unsigned remainder", &unsignedModulus, &remF));
-    //l.push_back(Function(SBVDIV, "signed division", &signedDivide));
-    //l.push_back(Function(SBVREM, "signed remainder",&signedRemainder ));
+    l.push_back(Function(SBVDIV, "signed division", &signedDivide, NULL));
+    l.push_back(Function(SBVREM, "signed remainder",&signedRemainder,NULL ));
   }
 
 

diff --git a/src/util/measure.cpp b/src/util/measure.cpp
index f1f048f890e08cbf15824c044b08d8f7dc4ed843..0e7ddd50775d26912651d74bf9608506dc3a25e0 100644 (file)
--- a/src/util/measure.cpp
+++ b/src/util/measure.cpp
@@ -44,6 +44,7 @@ go(Kind k, Result
 {
 
   BBAsProp bbP(k,mgr,bits);
+  bbP.numberClauses();
 
   Relations relations(iterations, bits, k, mgr, prob);
 
@@ -78,7 +79,7 @@ go(Kind k, Result
 
       // After unit propagation.
       int clauseCount = 0;
-      clauseCount = bbP.addToClauseCount();
+      clauseCount = bbP.fixedCount();
 
       clause += clauseCount;
 
@@ -162,12 +163,13 @@ main()
   mgr = new STPMgr;
   Cpp_interface interface(*mgr);
   mgr->UserFlags.division_by_zero_returns_one_flag=true;
+  //mgr->UserFlags.set("simple-cnf","1");
 
   out << "\\begin{subtables}" << endl;
-  work(1);
-  work(5);
+  //work(1);
+ // work(5);
   work(50);
-  work(95);
+ // work(95);
   out << "\\end{subtables}" << endl;
 
   out << "% Iterations:" << iterations << " bit-width:" << bits << endl;