From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Thu, 10 Mar 2011 14:35:13 +0000 (+0000)
Subject: Bugfix. r1194 didn't preserve the doubly linked list.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=0226f4968f3acb09eb4ede6186e306e30f5a3efb;p=francis%2Fstp.git

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 77aecff..1969f4d 100644
--- 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 16290f5..d24de2f 100644
--- 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;