From 22f666b61431d787542b6894c2edf11e1286ad45 Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sun, 24 Feb 2013 03:29:47 +0000
Subject: [PATCH] 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
---
 src/util/Functions.cpp | 73 ++++++++++++++++++++++++++++++++++
 src/util/Functions.h   | 90 ++++++++----------------------------------
 src/util/measure.cpp   | 10 +++--
 3 files changed, 96 insertions(+), 77 deletions(-)

diff --git a/src/util/Functions.cpp b/src/util/Functions.cpp
index c3cd3cf..a274478 100644
--- 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 2d8f791..67b99c8 100644
--- 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 f1f048f..0e7ddd5 100644
--- 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;
-- 
2.47.3