From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Mon, 14 Mar 2011 00:46:02 +0000 (+0000)
Subject: Experimental. Simplify all the bit-vector children before simplifying the term. Conce... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=04b28f9b229e8129c850c6d00dd7b5c788281995;p=francis%2Fstp.git

Experimental. Simplify all the bit-vector children before simplifying the term. Conceptually this is better, but I don't know if it's faster.

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

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index 32c3f70..c691fde 100644
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -1779,6 +1779,27 @@ namespace BEEV
 		  }
     }
 
+
+    //Check that each of the bit-vector operands is simplified.
+    //I haven't measured if this is worth the expense.
+    {
+    	bool notSimplified= false;
+    	for (int i =0; i < inputterm.Degree();i++)
+    		if (inputterm[i].GetType() == BITVECTOR_TYPE)
+				if (!hasBeenSimplified(inputterm[i]))
+				{
+					notSimplified = true;
+					break;
+				}
+    	if (notSimplified)
+    	{
+    		ASTNode r = SimplifyTerm(inputterm);
+			UpdateSimplifyMap(actualInputterm,r,false,NULL);
+			UpdateSimplifyMap(inputterm,r,false,NULL);
+			return r;
+    	}
+    }
+
     switch (k)
       {
       case BVCONST:
@@ -2288,10 +2309,10 @@ namespace BEEV
               break;
             case ITE:
 			   if (a0[1].isConstant() && a0[2].isConstant()) {
-					ASTNode t = nf->CreateTerm(BVNEG, inputValueWidth,
-							a0[1]);
-					ASTNode f = nf->CreateTerm(BVNEG, inputValueWidth,
-							a0[2]);
+					ASTNode t = SimplifyTerm(nf->CreateTerm(BVNEG, inputValueWidth,
+							a0[1]));
+					ASTNode f = SimplifyTerm(nf->CreateTerm(BVNEG, inputValueWidth,
+							a0[2]));
 					output = nf->CreateTerm(ITE, inputValueWidth, a0[0],
 							BVConstEvaluator(t), BVConstEvaluator(f));
 					break;
@@ -2813,11 +2834,7 @@ namespace BEEV
             {
               if (WRITE == inputterm[0].GetKind())
                 {
-                  //get rid of all writes
-		  //_bm->ASTNodeStats("before RemoveWrites_TopLevel:", inputterm);
-                  ASTNode nowrites = RemoveWrites_TopLevel(inputterm);
-		  //_bm->ASTNodeStats("after RemoveWrites_TopLevel:", nowrites);
-                  out1 = nowrites;
+            	  out1 = RemoveWrites_TopLevel(inputterm);
                 }
               else if (ITE == inputterm[0].GetKind())
                 {