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

diff --git a/src/simplifier/bvsolver.cpp b/src/simplifier/bvsolver.cpp
index 1496b7ef74a877dd1dcb4384bf2b09f588f2ca4f..ffa1127f29f1ccde665ab0f47cf8cfb8220beafb 100644 (file)
--- 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 47271b99454b863e28e5d96b453b378db70b510d..540e7e79eee7133f767817193f98a031916ff9d9 100644 (file)
--- 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())