Bugfix. Recursively simplify array ITES.

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

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index 62b06db58c35356fe32f6d831fdacf7ce13512b9..838c0f7550969dfddf65b56f9d149ac95134304e 100644 (file)
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -3155,6 +3155,54 @@ namespace BEEV
       }
   } //end of RemoveWrites_TopLevel()
 
+
+  // recursively simplify things that are of type array.
+
+  ASTNode Simplifier::SimplifyArrayTerm(const ASTNode& term,
+               ASTNodeMap* VarConstMap) {
+
+       assert(term.GetIndexWidth() > 0);
+
+       ASTNode output;
+       if (CheckSimplifyMap(term, output, false)) {
+               return output;
+       }
+
+       switch (term.GetKind()) {
+       case SYMBOL:
+               return term;
+       case ITE: {
+               unsigned iw = term.GetIndexWidth();
+               output = CreateSimplifiedTermITE(
+                               SimplifyFormula(term[0],VarConstMap),
+                               SimplifyArrayTerm(term[1], VarConstMap),
+                               SimplifyArrayTerm(term[2], VarConstMap));
+               output.SetIndexWidth(iw);
+       }
+               break;
+       case WRITE: {
+               unsigned iw = term.GetIndexWidth();
+               ASTNode array = SimplifyArrayTerm(term[0], VarConstMap);
+               ASTNode idx = SimplifyTerm(term[1]);
+               ASTNode val = SimplifyTerm(term[2]);
+
+               output = nf->CreateTerm(WRITE, term.GetValueWidth(), array, idx, val);
+               output.SetIndexWidth(iw); // save the value and set, otherwise it sometimes fails.
+       }
+
+               break;
+       default:
+               FatalError("2313456331");
+       }
+
+       UpdateSimplifyMap(term, output, false);
+       assert(term.GetIndexWidth() == output.GetIndexWidth());
+       assert(BVTypeCheck(output));
+       return output;
+}
+
+
+
   ASTNode Simplifier::SimplifyWrites_InPlace(const ASTNode& term,
                                              ASTNodeMap* VarConstMap)
   {
@@ -3182,7 +3230,7 @@ namespace BEEV
 
     do
       {
-        ASTNode writeIndex = SimplifyTerm(write[1]);
+        ASTNode writeIndex = SimplifyTerm(write[1]);
         ASTNode writeVal = SimplifyTerm(write[2]);
 
         //compare the readIndex and the current writeIndex and see if they
@@ -3226,14 +3274,13 @@ namespace BEEV
         //Setup the write for the new iteration, one level inner write
         write = write[0];
       } while (WRITE == write.GetKind());
+    assert(BVTypeCheck(write));
+    assert(write.GetIndexWidth() >0);
 
     // 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);
+       write = SimplifyArrayTerm(write,VarConstMap);
       }
 
 
@@ -3254,6 +3301,7 @@ namespace BEEV
 
     if (ITE == write.GetKind()) {
                output = SimplifyTerm(output, VarConstMap);
+               assert(BVTypeCheck(output));
        }
 
 

diff --git a/src/simplifier/simplifier.h b/src/simplifier/simplifier.h
index d7524937383a050de4f54e1ef776e33f72064222..99d431b7a117838ed39ca719d4ab5b4d8bd39248 100644 (file)
--- a/src/simplifier/simplifier.h
+++ b/src/simplifier/simplifier.h
@@ -218,6 +218,9 @@ namespace BEEV
     ASTNode RemoveWrites(const ASTNode& term);
     ASTNode SimplifyWrites_InPlace(const ASTNode& term, 
                                    ASTNodeMap* VarConstMap=NULL);
+
+    ASTNode SimplifyArrayTerm(const ASTNode& term,ASTNodeMap* VarConstMap);
+
     ASTNode ReadOverWrite_To_ITE(const ASTNode& term, 
                                  ASTNodeMap* VarConstMap=NULL);