From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Wed, 9 Jun 2010 04:00:08 +0000 (+0000)
Subject: Bugfix. Simplify the proposition of array-ITEs. I don't simplify the "then" and ... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=c2e890bb788b4604747f77bbd7beedfcc7e06602;p=francis%2Fstp.git

Bugfix. Simplify the proposition of array-ITEs. I don't simplify the "then" and "else" branch so I'm not sure if this fixes all the problems.



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

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index 5ee80ad..6d43598 100644
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -3227,6 +3227,16 @@ namespace BEEV
         write = write[0];
       } while (WRITE == write.GetKind());
 
+    // todo write[1] and write[2] should be simplified too.
+    if(ITE == write.GetKind())
+      {
+    	ASTNode prop = SimplifyFormula(write[0],false, VarConstMap);
+    	int indexW = write.GetIndexWidth();
+    	write = nf->CreateTerm(ITE, write.GetValueWidth(), prop,write[1],write[2]);
+    	write.SetIndexWidth(indexW);
+      }
+
+
     ASTVec::reverse_iterator it_index = writeIndices.rbegin();
     ASTVec::reverse_iterator itend_index = writeIndices.rend();
     ASTVec::reverse_iterator it_values = writeValues.rbegin();
@@ -3241,10 +3251,6 @@ namespace BEEV
 
     output = nf->CreateTerm(READ, width, write, readIndex);
     assert(BVTypeCheck(output));
-    if(ITE == write.GetKind())
-      {
-	output = SimplifyTerm(output, VarConstMap);
-      }
 
     //UpdateSimplifyMap(original_write, write, false);
     UpdateSimplifyMap(term, output, false);