Speedup. Experimental. Caching was disabled when converting a term to a constant...

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 b3d0889170eeb669f488619a9af3eaa490c7e778..6b30fa015d031625f48c0f29aee9547ef761ef94 100644 (file)
--- 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;
       }