From e251e275625b8199985c0a71548c8e5615ac3df5 Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Thu, 22 Oct 2009 13:10:32 +0000
Subject: [PATCH] Merge in changes from my branch r316 that remove redundant
 operations when building a counter example. This speeds up the CVC benchmarks
 by 10%.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@338 e59a4935-1847-0410-ae03-e826735625c1
---
 .../CounterExample.cpp                        | 27 ++++++++-----------
 1 file changed, 11 insertions(+), 16 deletions(-)

diff --git a/src/absrefine_counterexample/CounterExample.cpp b/src/absrefine_counterexample/CounterExample.cpp
index b4ad3c0..83e9b6e 100644
--- a/src/absrefine_counterexample/CounterExample.cpp
+++ b/src/absrefine_counterexample/CounterExample.cpp
@@ -439,7 +439,7 @@ namespace BEEV
   Expand_ReadOverWrite_UsingModel(const ASTNode& term, bool arrayread_flag)
   {
     if (READ != term.GetKind() 
-        && WRITE != term[0].GetKind())
+        || WRITE != term[0].GetKind())
       {
         FatalError("RemovesWrites: Input must be a READ over a WRITE", term);
       }
@@ -448,7 +448,7 @@ namespace BEEV
     ASTNodeMap::iterator it1;
     if ((it1 = CounterExampleMap.find(term)) != CounterExampleMap.end())
       {
-        ASTNode val = it1->second;
+        const ASTNode& val = it1->second;
         if (BVCONST != val.GetKind())
           {
             //recursion is fine here. There are two maps that are checked
@@ -468,39 +468,34 @@ namespace BEEV
           }
       }
 
-    unsigned int width = term.GetValueWidth();
-    ASTNode writeA = ASTTrue;
     ASTNode newRead = term;
-    ASTNode readIndex = TermToConstTermUsingModel(newRead[1], false);
+        const ASTNode readIndex = TermToConstTermUsingModel(newRead[1], false);
     //iteratively expand read-over-write, and evaluate against the
     //model at every iteration
+        ASTNode write = newRead[0];
     do
       {
-        ASTNode write = newRead[0];
-        writeA = write[0];
         ASTNode writeIndex = TermToConstTermUsingModel(write[1], false);
-        ASTNode writeVal = TermToConstTermUsingModel(write[2], false);
 
-        ASTNode cond = 
-          ComputeFormulaUsingModel(simp->CreateSimplifiedEQ(writeIndex, 
-                                                            readIndex));
-        if (ASTTrue == cond)
+            if (writeIndex == readIndex)
           {
             //found the write-value. return it
-            output = writeVal;
+                output = TermToConstTermUsingModel(write[2], false);
             CounterExampleMap[term] = output;
             return output;
           }
 
-        newRead = bm->CreateTerm(READ, width, writeA, readIndex);
-      } while (READ == newRead.GetKind() && WRITE == newRead[0].GetKind());
+            write = write[0];
+          } while (WRITE == write.GetKind());
 
+		const unsigned int width = term.GetValueWidth();
+        newRead = bm->CreateTerm(READ, width, write, readIndex);
     output = TermToConstTermUsingModel(newRead, arrayread_flag);
 
     //memoize
     CounterExampleMap[term] = output;
     return output;
-  } //Exand_ReadOverWrite_To_ITE_UsingModel()
+      } //Expand_ReadOverWrite_UsingModel()
 
   /* FUNCTION: accepts a non-constant formula, and checks if the
    * formula is ASTTrue or ASTFalse w.r.t to a model
-- 
2.47.3