From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Wed, 28 Jul 2010 13:23:12 +0000 (+0000)
Subject: Speedup. I've measured the performance of bit blasted comparisons on a (single) test... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=4e798d2ffb9d33e50c94175dffb15cac2f00d762;p=francis%2Fstp.git

Speedup. I've measured the performance of bit blasted comparisons on a (single) test case. I've selected the fastest encoding.



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

diff --git a/src/to-sat/BitBlaster.cpp b/src/to-sat/BitBlaster.cpp
index 73a5028..e25825d 100644
--- a/src/to-sat/BitBlaster.cpp
+++ b/src/to-sat/BitBlaster.cpp
@@ -1252,11 +1252,37 @@ BBNodeVec BitBlaster<BBNode,BBNodeManagerT>::BBITE(const BBNode& cond, const BBN
 	return result;
 }
 
+//  smt-test/transitive400.smt2
+// Cryptominsat 2:  bbbvle_variant1 = true.  220ms
+// Cryptominsat 2:  bbbvle_variant1 = false. 15 sec
+
+// Minisat 2:  bbbvle_variant1 = true. 13 ms
+// Minisat 2:  bbbvle_variant1 = false. 48 sec
+
+
+const bool bbbvle_variant1 = true;
+const bool bbbvle_variant2 = !bbbvle_variant1;
+
+// Workhorse for comparison routines.  This does a signed BVLE if is_signed
+// is true, else it's unsigned.  All other comparison operators can be reduced
+// to this by swapping args or complementing the result bit.
+template <class BBNode, class BBNodeManagerT>
+BBNode BitBlaster<BBNode,BBNodeManagerT>::BBBVLE(const BBNodeVec& left, const BBNodeVec& right,
+                bool is_signed, bool is_bvlt)
+{
+  if (bbbvle_variant1)
+    return BBBVLE_variant1(left,right,is_signed,is_bvlt);
+  else
+    return BBBVLE_variant2(left,right,is_signed,is_bvlt);
+}
+
 
-// On some cases I suspect this is better than the new variant.
 template <class BBNode, class BBNodeManagerT>
-BBNode BBBVLE_variant(const BBNodeVec& left, const BBNodeVec& right, bool is_signed, BBNodeManagerASTNode* nf)
+BBNode BitBlaster<BBNode,BBNodeManagerT>::BBBVLE_variant1(const BBNodeVec& left_, const BBNodeVec& right_, bool is_signed, bool is_bvlt)
 {
+  const BBNodeVec& left = !is_bvlt? left_: right_;
+  const BBNodeVec& right = !is_bvlt? right_: left_;
+
   // "thisbit" represents BVLE of the suffixes of the BVs
   // from that position .  if R < L, return TRUE, else if L < R
   // return FALSE, else return BVLE of lower-order bits.  MSB is
@@ -1283,16 +1309,16 @@ BBNode BBBVLE_variant(const BBNodeVec& left, const BBNodeVec& right, bool is_sig
     }
 
   BBNode msb = nf->CreateNode(ITE, nf->CreateNode(IFF, rmsb, lmsb), prevbit, rmsb);
+
+  if (is_bvlt)
+    {
+      msb = nf->CreateNode(NOT, msb);
+    }
   return msb;
 }
 
-
-
-// Workhorse for comparison routines.  This does a signed BVLE if is_signed
-// is true, else it's unsigned.  All other comparison operators can be reduced
-// to this by swapping args or complementing the result bit.
 template <class BBNode, class BBNodeManagerT>
-BBNode BitBlaster<BBNode,BBNodeManagerT>::BBBVLE(const BBNodeVec& left, const BBNodeVec& right,
+BBNode BitBlaster<BBNode,BBNodeManagerT>::BBBVLE_variant2(const BBNodeVec& left, const BBNodeVec& right,
 		bool is_signed, bool is_bvlt) {
 	typename BBNodeVec::const_reverse_iterator lit = left.rbegin();
 	const typename BBNodeVec::const_reverse_iterator litend = left.rend();
diff --git a/src/to-sat/BitBlaster.h b/src/to-sat/BitBlaster.h
index a580149..0e8c60a 100644
--- a/src/to-sat/BitBlaster.h
+++ b/src/to-sat/BitBlaster.h
@@ -112,6 +112,11 @@ class BitBlaster {
 	// Internal bit blasting routines.
 	BBNode BBBVLE(const vector<BBNode>& x, const vector<BBNode>& y, bool is_signed,
 			bool is_bvlt = false);
+        BBNode BBBVLE_variant1(const vector<BBNode>& x, const vector<BBNode>& y, bool is_signed,
+                        bool is_bvlt = false);
+        BBNode BBBVLE_variant2(const vector<BBNode>& x, const vector<BBNode>& y, bool is_signed,
+                        bool is_bvlt = false);
+
 
 	// Return bit-blasted form for BVLE, BVGE, BVGT, SBLE, etc.
 	BBNode BBcompare(const ASTNode& form, set<BBNode>& support);