From c2e890bb788b4604747f77bbd7beedfcc7e06602 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Wed, 9 Jun 2010 04:00:08 +0000 Subject: [PATCH] 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 --- src/simplifier/simplifier.cpp | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) 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); -- 2.47.3