From 9056890dfd7faf1800eb1ea7ff083ef69d004b41 Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Wed, 23 Jun 2010 14:13:31 +0000
Subject: [PATCH] Speedup/bugfix. Change how duplicate symbols are searched
 for. This fixed failing2.smt

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@869 e59a4935-1847-0410-ae03-e826735625c1
---
 src/simplifier/bvsolver.cpp   | 64 ++++++++++++++++++++++-------------
 src/simplifier/simplifier.cpp |  4 +--
 2 files changed, 43 insertions(+), 25 deletions(-)

diff --git a/src/simplifier/bvsolver.cpp b/src/simplifier/bvsolver.cpp
index 1496b7e..ffa1127 100644
--- a/src/simplifier/bvsolver.cpp
+++ b/src/simplifier/bvsolver.cpp
@@ -204,31 +204,49 @@ namespace BEEV
     for (ASTVec::const_iterator it = c.begin(), itend = c.end(); it != itend; it++)
       {
     	const ASTNode& monom = *it;
-        if (SYMBOL == monom.GetKind() 
+        if (
+        	(
+        	SYMBOL == monom.GetKind()
             && !chosen_symbol
        		&& !DoNotSolveThis(monom)
-            && count.single(monom)
-        )
-          {
-            outmonom = monom;
-            chosen_symbol = true;
-          }
-        else if (BVUMINUS == monom.GetKind() 
-         		&& SYMBOL == monom[0].GetKind()
-           		&& !chosen_symbol
-        		&& !DoNotSolveThis(monom[0])
-                && count.single(monom[0])
-                 )
-          {
-            //cerr << "Chosen Monom: " << monom << endl;
-            outmonom = monom;
-            chosen_symbol = true;
-          }
-        else
-          {
-            o.push_back(monom);
-          }
-      }
+            && !VarSeenInTerm(monom,rhs)
+            )
+            ||
+            (
+             BVUMINUS == monom.GetKind()
+             && SYMBOL == monom[0].GetKind()
+             && !chosen_symbol
+             && !DoNotSolveThis(monom[0])
+             && !VarSeenInTerm(monom[0],rhs)
+            )
+           )
+        {
+        	// Look through all the children of the BVPLUS and check
+        	// that the variable appears in none of them.
+
+        	ASTNode var = (SYMBOL == monom.GetKind())? monom: monom[0];
+        	bool duplicated = false;
+        	for (ASTVec::const_iterator it2 = c.begin(); it2 != itend; it2++)
+			{
+				if (it2 == it)
+					continue;
+				if (VarSeenInTerm(var,*it2))
+				{
+					duplicated = true;
+					break;
+				}
+			}
+			if (!duplicated)
+			{
+				outmonom = monom; //nb. monom not var.
+				chosen_symbol = true;
+			}
+			else
+				o.push_back(monom);
+        }
+    	else
+    		o.push_back(monom);
+	}
 
     //try to choose only odd coeffed variables first
     if (!chosen_symbol)
diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index 47271b9..540e7e7 100644
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -2743,7 +2743,7 @@ namespace BEEV
     for (ASTVec::const_iterator
            it = c.begin(), itend = c.end(); it != itend; it++)
       {
-        ASTNode aaa = *it;
+        const ASTNode& aaa = *it;
         if (SYMBOL == aaa.GetKind())
           {
             vars_to_consts[aaa].push_back(one);
@@ -2808,7 +2808,7 @@ namespace BEEV
            it = vars_to_consts.begin(), itend = vars_to_consts.end();
          it != itend; it++)
       {
-        ASTVec ccc = it->second;
+        const ASTVec& ccc = it->second;
 
         ASTNode constant;
         if (1 < ccc.size())
-- 
2.47.3