From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sat, 26 Jun 2010 04:16:34 +0000 (+0000)
Subject: Speedups.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=b311fc813f32f0ea4cbfd62a6fdedc27f1675b62;p=francis%2Fstp.git

Speedups.
* Call topLevel simplify only if something has changed.
* If there is a symbol on the rhs put it on the lhs, which simplifies more eqns.




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

diff --git a/src/simplifier/bvsolver.cpp b/src/simplifier/bvsolver.cpp
index 43c2676..5e3a687 100644
--- a/src/simplifier/bvsolver.cpp
+++ b/src/simplifier/bvsolver.cpp
@@ -282,9 +282,12 @@ namespace BEEV
     ASTNode lhs = eq[0];
     ASTNode rhs = eq[1];
 
-	// if only one side is a constant, it should be on the RHS.
-	if (((BVCONST == lhs.GetKind()) ^ (BVCONST == rhs.GetKind()))
-			&& (lhs.GetKind() == BVCONST)) {
+
+	if (
+			((BVCONST == lhs.GetKind()) && (BVCONST != rhs.GetKind()))  || // if only one side is a constant, it should be on the RHS.
+			((SYMBOL == rhs.GetKind()) &&  (SYMBOL != lhs.GetKind()))  // If there is only one variable. It should be on the left.
+	)
+			{
 		lhs = eq[1];
 		rhs = eq[0];
 		eq = _bm->CreateNode(EQ, lhs, rhs); // If "return eq" is called, return the arguments in the correct order.
@@ -318,7 +321,7 @@ namespace BEEV
         //construct:  rhs - (lhs without the chosen monom)
         unsigned int len = lhs.GetValueWidth();
         leftover_lhs = 
-          _simp->SimplifyTerm_TopLevel(_bm->CreateTerm(BVUMINUS,
+          _simp->SimplifyTerm(_bm->CreateTerm(BVUMINUS,
                                                        len, leftover_lhs));
         rhs =
           _simp->SimplifyTerm(_bm->CreateTerm(BVPLUS, len, rhs, leftover_lhs));
@@ -616,17 +619,32 @@ namespace BEEV
     bool any_solved = false;
     for (ASTVec::iterator it = c.begin(), itend = c.end(); it != itend; it++)
       {
-        //_bm->ASTNodeStats("Printing before calling simplifyformula
-        //inside the solver:", *it);
 
-    	// Calling simplifyFormula makes the required substitutions. For instance, if
-    	// first was : v = x,
-    	// then if the next formula is: x = v
-    	// calling simplify on the second formula will convert it into "true", avoiding a cycle.
+		 /*
+    	 Calling simplifyFormula makes the required substitutions. For instance, if
+    	 first was : v = x,
+    	 then if the next formula is: x = v
+    	 calling simplify on the second formula will convert it into "true", avoiding a cycle.
+
+    	 The problem with this is that Simplify___() doesn't normally simplify into array
+    	 operations. So given something like :
+    	 a = b
+    	 b = write(A,a,a)
+
+    	 It will replace (a=b) with true, and store (a=b) in the solverMap. Then it will
+    	 store b = write(A,a,a) in the solver map. Which is wrong. What it should do is
+    	 rewrite a=b through the second expression, giving:
+    	 b = write(A,b,b),
+    	 which shouldn't be simplified.
+
+    	 Simplifying through arrays is very expensive though. I know how to fix it, but
+    	 don't have time. Trev.
+		  */
+
     	ASTNode aaa =
           (any_solved
            && EQ == it->GetKind()) ?
-          _simp->SimplifyFormula(*it, false) :
+          _simp->SimplifyFormula_TopLevel(*it, false) :
           *it;
         //_bm->ASTNodeStats("Printing after calling simplifyformula
         //inside the solver:", aaa);