From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sun, 2 Jan 2011 12:08:03 +0000 (+0000)
Subject: Speedup. Experimental. Caching was disabled when converting a term to a constant... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=3de517d685dfe50b79c73ad1d35953038bf999cc;p=francis%2Fstp.git

Speedup. Experimental. Caching was disabled when converting a term to a constant using the model, IF the arrayReadFlag was false. Without caching it runs very slowly when building the counter example.

I've yet to find an instance where caching all the time  gives the wrong example??


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

diff --git a/src/absrefine_counterexample/CounterExample.cpp b/src/absrefine_counterexample/CounterExample.cpp
index b3d0889..6b30fa0 100644
--- a/src/absrefine_counterexample/CounterExample.cpp
+++ b/src/absrefine_counterexample/CounterExample.cpp
@@ -66,19 +66,13 @@ namespace BEEV
             else
               {
                 assert (symbol.GetType() == BOOLEAN_TYPE);
-                //const char * zz = symbol.GetName();
-                //if the variables are not cnf variables then add
-                //them to the counterexample
-                //if (0 != strncmp("cnf", zz, 3) && 0
-                //  != strcmp("*TrueDummy*", zz))
-                  {
-                  if (newS.modelValue(sat_variable_index) == newS.true_literal())
-                      CounterExampleMap[symbol] = ASTTrue;
-                    else if (newS.modelValue(sat_variable_index) == newS.false_literal())
-                      CounterExampleMap[symbol] = ASTFalse;
-                    else
-                      FatalError("never heres.");
-                  }
+ 			    if (newS.modelValue(sat_variable_index) == newS.true_literal())
+				  CounterExampleMap[symbol] = ASTTrue;
+				else if (newS.modelValue(sat_variable_index) == newS.false_literal())
+				  CounterExampleMap[symbol] = ASTFalse;
+				else
+				  FatalError("never heres.");
+
               }
           }
 
@@ -339,7 +333,7 @@ namespace BEEV
     //when this flag is false, we should compute the arrayread to a
     //constant. this constant is stored in the counter_example
     //datastructure
-    if (!ArrayReadFlag)
+    //if (!ArrayReadFlag)
       {
         CounterExampleMap[term] = output;
       }