From bb725f86962ee960a11d417488dac13769842593 Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Fri, 18 Jun 2010 06:38:05 +0000
Subject: [PATCH] Refactor & slight performance improvement for the bvsolver.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@854 e59a4935-1847-0410-ae03-e826735625c1
---
 src/simplifier/bvsolver.cpp | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

diff --git a/src/simplifier/bvsolver.cpp b/src/simplifier/bvsolver.cpp
index 4e9883a..20f5e44 100644
--- a/src/simplifier/bvsolver.cpp
+++ b/src/simplifier/bvsolver.cpp
@@ -234,7 +234,6 @@ namespace BEEV
     if (!chosen_symbol)
       {
         ASTNode zero = _bm->CreateZeroConst(32);
-        bool chosen_odd = false;
 
     	o.clear();
         for (ASTVec::const_iterator
@@ -249,22 +248,24 @@ namespace BEEV
             if (BVMULT == monom.GetKind() 
                 && BVCONST == monom[0].GetKind() 
                 && _simp->BVConstIsOdd(monom[0]) 
-                && !chosen_odd
+                && !chosen_symbol
                 && !DoNotSolveThis(var)
                 && ((SYMBOL == var.GetKind() 
-                     && count.single(var))
+                     && count.single(var)
+                     && !VarSeenInTerm(var, rhs)
+                    )
                     || (BVEXTRACT == var.GetKind() 
                         && SYMBOL == var[0].GetKind() 
                         && BVCONST == var[1].GetKind() 
                         && zero == var[2]
                         && !DoNotSolveThis(var[0])
                         && !VarSeenInTerm(var[0], rhs)))
-                && !VarSeenInTerm(var, rhs)
+
                 )
               {
                 //monom[0] is odd.
                 outmonom = monom;
-                chosen_odd = true;
+                chosen_symbol = true;
               }
             else
               {
@@ -277,7 +278,7 @@ namespace BEEV
       (o.size() > 1) ? 
       _bm->CreateTerm(BVPLUS, lhs.GetValueWidth(), o) : 
       o[0];
-    return outmonom;
+    return outmonom; // can be SYMBOL or (BVUMINUS SYMBOL).
   } //end of choosemonom()
 
   //solver function which solves for variables with odd coefficient
-- 
2.47.3