From 3de517d685dfe50b79c73ad1d35953038bf999cc Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Sun, 2 Jan 2011 12:08:03 +0000 Subject: [PATCH] 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 --- .../CounterExample.cpp | 22 +++++++------------ 1 file changed, 8 insertions(+), 14 deletions(-) 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; } -- 2.47.3