* Make the arguments to ==, !=, > for ASTNode references to reduce unnecessary copies.

* Include the BBVLE from r254 for later experimentation.

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

diff --git a/src/AST/ASTNode.h b/src/AST/ASTNode.h
index 5fadc30cb031264da5bae72adaebfc9db6113799..3f4c6b0d447dd4ba2036dcf35944237ac780d9e5 100644 (file)
--- a/src/AST/ASTNode.h
+++ b/src/AST/ASTNode.h
@@ -46,19 +46,19 @@ namespace BEEV
     ASTNode(ASTInternal *in);
 
     //Equal iff ASTIntNode pointers are the same.
-    friend bool operator==(const ASTNode node1, const ASTNode node2)
+    friend bool operator==(const ASTNode& node1, const ASTNode& node2)
     {
       return 
         ((size_t) node1._int_node_ptr) == 
         ((size_t) node2._int_node_ptr);
     }
 
-    friend bool operator!=(const ASTNode node1, const ASTNode node2)
+    friend bool operator!=(const ASTNode& node1, const ASTNode& node2)
     {
       return !(node1 == node2);
     }
 
-    friend bool operator<(const ASTNode node1, const ASTNode node2)
+    friend bool operator<(const ASTNode& node1, const ASTNode& node2)
     {
       return 
         ((size_t) node1._int_node_ptr) < 

diff --git a/src/to-sat/BitBlastNew.cpp b/src/to-sat/BitBlastNew.cpp
index 3a60152f7298ae9cf76959e33881efbbe2f38545..5ca7c051069b7ab06c6e8d80ad4e272022f28e92 100644 (file)
--- a/src/to-sat/BitBlastNew.cpp
+++ b/src/to-sat/BitBlastNew.cpp
@@ -686,6 +686,41 @@ BBNodeVec BitBlasterNew::BBITE(const BBNode& cond, const BBNodeVec& thn,
        return result;
 }
 
+
+// On some cases I suspect this is better than the new variant.
+ASTNode BBBVLE_variant(const BBNodeVec& left, const BBNodeVec& right, bool is_signed, BBNodeManager* nf)
+{
+  // "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
+  // treated separately, because signed comparison is done by
+  // complementing the MSB of each BV, then doing an unsigned
+  // comparison.
+  BBNodeVec::const_iterator lit = left.begin();
+  BBNodeVec::const_iterator litend = left.end();
+  BBNodeVec::const_iterator rit = right.begin();
+  BBNode prevbit = nf->getTrue();
+  for (; lit < litend - 1; lit++, rit++)
+    {
+      BBNode thisbit = nf->CreateNode(ITE, nf->CreateNode(IFF, *rit, *lit), prevbit, *rit);
+      prevbit = thisbit;
+    }
+
+  // Handle MSB -- negate MSBs if signed comparison
+  BBNode lmsb = *lit;
+  BBNode rmsb = *rit;
+  if (is_signed)
+    {
+      lmsb = nf->CreateNode(NOT, *lit);
+      rmsb = nf->CreateNode(NOT, *rit);
+    }
+
+  BBNode msb = nf->CreateNode(ITE, nf->CreateNode(IFF, rmsb, lmsb), prevbit, rmsb);
+  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.

diff --git a/src/to-sat/ToCNF.cpp b/src/to-sat/ToCNF.cpp
index 7d67fe881eb2a3e4b9d45e776362d6b70341df41..96b5bd5cfdfec48446f297b8919a17213cf7c8a0 100644 (file)
--- a/src/to-sat/ToCNF.cpp
+++ b/src/to-sat/ToCNF.cpp
@@ -117,13 +117,7 @@ namespace BEEV
   //########################################
   //utilities for control bits.
 
-  void CNFMgr::initializeCNFInfo(CNFInfo& x)
-  {
-    x.control = 0;
-    x.clausespos = NULL;
-    x.clausesneg = NULL;
-  } //End of initlializeCNFInfo()
-  
+
   void CNFMgr::incrementSharesPos(CNFInfo& x)
   {
     x.control += ((x.control & 3) < 2) ? 1 : 0;
@@ -280,7 +274,6 @@ namespace BEEV
     if (info.find(varphi) == info.end())
       {
         x = new CNFInfo();
-        initializeCNFInfo(*x);
         info[varphi] = x;
       }
     else
@@ -366,7 +359,6 @@ namespace BEEV
     if (info.find(varphi) == info.end())
       {
         x = new CNFInfo();
-        initializeCNFInfo(*x);
         info[varphi] = x;
       }
     else
@@ -609,6 +601,8 @@ namespace BEEV
   {
     CNFInfo* x = info[varphi];
     
+    assert(!wasRenamedPos(*x));
+
     //########################################
     // step 1, calc new variable
     //########################################

diff --git a/src/to-sat/ToCNF.h b/src/to-sat/ToCNF.h
index 9428785929869a9babb4d6a18124b05a3de8d3fb..865ca7afd3fa954432ae9ac2234060a4ce45ad6f 100644 (file)
--- a/src/to-sat/ToCNF.h
+++ b/src/to-sat/ToCNF.h
@@ -36,7 +36,7 @@ namespace BEEV
 
     // for the meaning of control bits, see "utilities for contol
     // bits".
-    typedef struct
+    struct CNFInfo
     {
       int control;
       ClauseList* clausespos;
@@ -45,7 +45,14 @@ namespace BEEV
         ClauseList* clausesneg;
         ASTNode* termforcnf;
       };
-    } CNFInfo;
+
+      CNFInfo()
+      {
+       control = 0;
+       clausespos = NULL;
+               clausesneg = NULL;
+      }
+    } ;
 
     //Collect all XOR Clauses here
     ClauseList* clausesxor;