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

diff --git a/src/simplifier/bvsolver.cpp b/src/simplifier/bvsolver.cpp
index 4e9883a15003c293e37cd698b96d1747d5dc0a5f..20f5e44885180ec8d1a5b56586afe4ad3f7b7d73 100644 (file)
--- 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