Bugfix. r1194 didn't preserve the doubly linked list.

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

diff --git a/src/simplifier/MutableASTNode.h b/src/simplifier/MutableASTNode.h
index 77aecff0eb1f62be0e48bef606775a44a594ae5c..1969f4dd4702848833dffb0f898ce86328652cf7 100644 (file)
--- a/src/simplifier/MutableASTNode.h
+++ b/src/simplifier/MutableASTNode.h
@@ -64,6 +64,42 @@ private:
 
   public:
 
+    bool checkInvariant()
+    {
+       // Symbols have no children.
+       if (n.GetKind() == SYMBOL)
+       {
+               assert(children.size() ==0);
+       }
+
+       // all my parents have me as a child.
+        for (ParentsType::iterator it = parents.begin(); it != parents.end() ; it++)
+        {
+               vector<MutableASTNode *>::iterator it2 = (*it)->children.begin();
+               bool found = false;
+               for (;it2!= (*it)->children.end();it2++)
+               {
+                       assert (*it2 != NULL);
+                       if (*it2 == this)
+                               found = true;
+               }
+               assert(found);
+        }
+
+        for (int i = 0; i < children.size(); i++)
+        {
+               // call check on all the children.
+               children[i]->checkInvariant();
+
+               // all my children have me as a parent.
+               assert (children[i]->parents.find(this) != children[i]->parents.end());
+        }
+
+        return true; // ignored.
+    }
+
+
+
   MutableASTNode&  getParent()
     {
       assert (parents.size() == 1);
@@ -147,7 +183,12 @@ private:
       removeChildren(vars); // ignore the result
       children.clear();
       children.insert(children.begin(), newN->children.begin(), newN->children.end());
+      for (int i = 0; i < children.size(); i++)
+         children[i]->parents.insert(this);
+
       propagateUpDirty();
+      assert(newN->parents.size() == 0); // we don't copy 'em in you see.
+      newN->removeChildren(vars);
     }
 
 

diff --git a/src/simplifier/RemoveUnconstrained.cpp b/src/simplifier/RemoveUnconstrained.cpp
index 16290f5a2cc1528151a4de4907c9ac5b0b8c4dd6..d24de2f9d68e0459f415a71dcda14744090b996b 100644 (file)
--- a/src/simplifier/RemoveUnconstrained.cpp
+++ b/src/simplifier/RemoveUnconstrained.cpp
@@ -39,6 +39,9 @@ namespace BEEV
 
     result = topLevel_other(result, simplifier);
 
+    // There should be no unapplied substitutions.
+    assert(result == simplifier->applySubstitutionMap(result));
+
     // It is idempotent if there are no big ANDS (we have a special hack), and,
     // if we don't introduced any new "disjoint extracts."
 
@@ -379,7 +382,7 @@ namespace BEEV
               }
             else // One side is a variable. The other is anything.
               {
-                bool varOnLHS = (var == children[0]);
+                bool varOnLHS = (var == children[0]);
 
                 // All the ASTNode vars need to map to their existing MutableASTNodes. So we collect all the variables
                 vector<MutableASTNode*> vars;
@@ -404,7 +407,7 @@ namespace BEEV
                       n= nf->CreateNode(OR, v, nf->CreateNode(EQ, mutable_children[1]->toASTNode(nf), c1));
                     else
                       n= nf->CreateNode(AND, v, nf->CreateNode(NOT,nf->CreateNode(EQ, mutable_children[1]->toASTNode(nf), c1)));
-          }
+                  }
                 else
                   {
                     rhs = nf->CreateTerm(ITE, width, v, smallestNumber, biggestNumber);
@@ -414,10 +417,10 @@ namespace BEEV
                     else
                       n= nf->CreateNode(AND, v, nf->CreateNode(NOT,nf->CreateNode(EQ, mutable_children[0]->toASTNode(nf), c2)));
                   }
-
                 replace(var, rhs);
                 MutableASTNode *newN = MutableASTNode::build(n,create);
                 muteParent.replaceWithAnotherNode(newN);
+                assert(muteParent.checkInvariant());
               }
           }
           break;