Bugfix. The prior revision sometimes returned the wrong result (very rarely).

In the prior revision I removed some explicit calls to simplifyTerm.
Wrongly believing that the term was already simplified at the point.
To check that it was simplified I asserted the "hasBeenSimplified" function.
But the hasBeenSimplified function only checked that the term was present in the simplifyMap.
That is that simplifyTerm had been called on it.
Which isn't the same thing as being simplified.
i.e. term A is not simplified if in the SimplifyMap it's mapped to term B.
It's only simplified if A maps to A.

Some simplification functions expect their children to already be simplified.
This wasn't the case so we'd get the wrong answer.

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

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index 075a1019d2c5f41ae08afaaa127dbf7a8ad0cfdf..7f7f746d2a1ee44a453c202f9a59b1f13b3eddf9 100644 (file)
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -1625,9 +1625,10 @@ namespace BEEV
     return nf->CreateTerm(k, a.GetValueWidth(), a, b);
   }
 
-
+  // If a node is not a leaf, it has only been simplified  if it
+  // maps to itself in the simplifyMap.
   bool
-  Simplifier::hasBeenSimplified(ASTNode n)
+  Simplifier::hasBeenSimplified(const ASTNode& n)
   {
     //n has been simplified if, it's a constant:
     if (n.isConstant())
@@ -1640,8 +1641,12 @@ namespace BEEV
     if (n.GetKind() == SYMBOL)
        return true;
 
+    ASTNodeMap::const_iterator it;
     //If it's in the simplification map, it has been simplified.
-    return  (SimplifyMap->find(n) != SimplifyMap->end());
+    if ((it = SimplifyMap->find(n)) == SimplifyMap->end())
+      return false;
+
+    return (it->second == n);
   }
 
   //This function simplifies terms based on their kind
@@ -1656,7 +1661,7 @@ namespace BEEV
 
        ASTNode inputterm(actualInputterm); // mutable local copy.
 
-    //cout << "SimplifyTerm: input: " << a << endl;
+    //cout << "SimplifyTerm: input: " << actualInputterm << endl;
     // if (!optimize_flag)
     //       {
     //         return inputterm;
@@ -1714,10 +1719,7 @@ namespace BEEV
                        else
                                output = actualInputterm;
 
-                       if (inputterm != output) {
-                               UpdateSimplifyMap(inputterm, output, false, VarConstMap);
-                               inputterm = output;
-                       }
+                       inputterm = output;
                }
 
                const ASTVec& children = inputterm.GetChildren();
@@ -2860,6 +2862,7 @@ namespace BEEV
        output = SimplifyTerm(output);
     //memoize
     UpdateSimplifyMap(inputterm, output, false, VarConstMap);
+    UpdateSimplifyMap(actualInputterm, output, false, VarConstMap);
     //cerr << "SimplifyTerm: output" << output << endl;
     // CheckSimplifyInvariant(inputterm,output);
 

diff --git a/src/simplifier/simplifier.h b/src/simplifier/simplifier.h
index b1e4a141d971708889c2a4920d5f6f1447d88d62..5731f38d4c72202f7138e32527a7f0e3ca99c201 100644 (file)
--- a/src/simplifier/simplifier.h
+++ b/src/simplifier/simplifier.h
@@ -134,9 +134,8 @@ namespace BEEV
                             bool pushNeg, 
                             ASTNodeMap* VarConstMap=NULL);
 
-    bool
-    hasBeenSimplified(ASTNode n);
 
+    bool hasBeenSimplified(const ASTNode& n);
 
     ASTNode SimplifyTerm(const ASTNode& inputterm, 
                          ASTNodeMap* VarConstMap=NULL);