From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sun, 27 Jun 2010 13:52:41 +0000 (+0000)
Subject: Speedup. Sort EQ nodes. This prevents duplicate nodes like (= 0 a), (=a 0), from... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=e4c9afc7287159d9032a919977e54000c6598d87;p=francis%2Fstp.git

Speedup. Sort EQ nodes. This prevents duplicate nodes like (= 0 a), (=a 0), from being created. The bvsolver expected nodes reversed to how they are now created.




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

diff --git a/src/AST/NodeFactory/HashingNodeFactory.cpp b/src/AST/NodeFactory/HashingNodeFactory.cpp
index 8034834..57f0337 100644
--- a/src/AST/NodeFactory/HashingNodeFactory.cpp
+++ b/src/AST/NodeFactory/HashingNodeFactory.cpp
@@ -21,7 +21,7 @@ BEEV::ASTNode HashingNodeFactory::CreateNode(const Kind kind,	const BEEV::ASTVec
 	ASTVec children(back_children);
 	// The Bitvector solver seems to expect constants on the RHS, variables on the LHS.
 	// We leave the order of equals children as we find them.
-	if (BEEV::isCommutative(kind) && kind != BEEV::EQ && kind != BEEV::AND)
+	if (BEEV::isCommutative(kind) && kind != BEEV::AND)
 	{
 		SortByArith(children);
 	}
diff --git a/src/simplifier/bvsolver.cpp b/src/simplifier/bvsolver.cpp
index ca53ebc..d9413c2 100644
--- a/src/simplifier/bvsolver.cpp
+++ b/src/simplifier/bvsolver.cpp
@@ -145,16 +145,18 @@ namespace BEEV
   //chooses a variable in the lhs and returns the chosen variable
   ASTNode BVSolver::ChooseMonom(const ASTNode& eq, ASTNode& modifiedlhs)
   {
-    if (!(EQ == eq.GetKind() && BVPLUS == eq[0].GetKind()))
-      {
-        FatalError("ChooseMonom: input must be a EQ", eq);
-      }
+	  assert(EQ == eq.GetKind());
+	  assert(BVPLUS == eq[0].GetKind() || BVPLUS== eq[1].GetKind());
 
-    const ASTNode& lhs = eq[0];
-    const ASTNode& rhs = eq[1];
+	// Unfortunately, the bvsolver is written to expect nodes in the
+	// reverse order to how the simplifying node factory produces them.
+	// That is, the simplifying node factory sorts by arithless, i.e.
+	// with constants or symbols on the left.
+    const bool lhsIsPlus = (BVPLUS == eq[0].GetKind());
+    const ASTNode& lhs = lhsIsPlus? eq[0] : eq[1];
+    const ASTNode& rhs = lhsIsPlus? eq[1] : eq[0];
 
     //collect all the vars in the lhs and rhs
-
     BuildSymbolGraph(eq);
     CountOfSymbols count(symbol_graph[eq]);
 
@@ -711,10 +713,13 @@ namespace BEEV
         return eq;
       }
 
-    ASTNode lhs = eq[0];
-    ASTNode rhs = eq[1];
-    const ASTNode zero = _bm->CreateZeroConst(rhs.GetValueWidth());
+    const ASTNode zero = _bm->CreateZeroConst(eq[0].GetValueWidth());
+
     //lhs must be a BVPLUS, and rhs must be a BVCONST
+	const bool lhsIsPlus = (BVPLUS == eq[0].GetKind());
+	 ASTNode lhs = lhsIsPlus? eq[0] : eq[1];
+	 ASTNode rhs = lhsIsPlus? eq[1] : eq[0];
+
     if (!(BVPLUS == lhs.GetKind() && zero == rhs))
       {
         evenflag = false;
@@ -803,8 +808,12 @@ namespace BEEV
       {
         ASTNode eq = *jt;
         assert(EQ == eq.GetKind());
-        ASTNode lhs = eq[0];
-        ASTNode rhs = eq[1];
+
+  	  const bool lhsIsPlus = (BVPLUS == eq[0].GetKind());
+       ASTNode lhs = lhsIsPlus? eq[0] : eq[1];
+       ASTNode rhs = lhsIsPlus? eq[1] : eq[0];
+
+
         ASTNode zero = _bm->CreateZeroConst(rhs.GetValueWidth());
         //lhs must be a BVPLUS, and rhs must be a BVCONST
         if (!(BVPLUS == lhs.GetKind() && zero == rhs))
@@ -855,8 +864,12 @@ namespace BEEV
            jt = input_c.begin(), jtend = input_c.end(); jt != jtend; jt++)
       {
         ASTNode eq = *jt;
-        ASTNode lhs = eq[0];
-        ASTNode rhs = eq[1];
+
+        // Want the plus on the lhs.
+      	  const bool lhsIsPlus = (BVPLUS == eq[0].GetKind());
+          ASTNode lhs = lhsIsPlus? eq[0] : eq[1];
+          ASTNode rhs = lhsIsPlus? eq[1] : eq[0];
+
         ASTNode zero = _bm->CreateZeroConst(rhs.GetValueWidth());
         //lhs must be a BVPLUS, and rhs must be a BVCONST
         if (!(BVPLUS == lhs.GetKind() && zero == rhs))