Cleanup / Refactor. Will call the sat solver fewer times.

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

diff --git a/src/absrefine_counterexample/AbstractionRefinement.cpp b/src/absrefine_counterexample/AbstractionRefinement.cpp
index 90f64bfb1c223bb74daf99f5b079bbeb99bd8c37..f868259132ccc2ac1e848d015f6bde9149005efb 100644 (file)
--- a/src/absrefine_counterexample/AbstractionRefinement.cpp
+++ b/src/absrefine_counterexample/AbstractionRefinement.cpp
@@ -169,13 +169,8 @@ namespace BEEV
     ASTNode writeAxiom;
     ASTNodeMap::const_iterator it = simp->ReadOverWriteMap()->begin();
     ASTNodeMap::const_iterator itend = simp->ReadOverWriteMap()->end();
-    unsigned int oldFalseAxiomsSize = 0;
-    //int count = 0;
-    //int num_write_axioms = ReadOverWrite_NewName_Map.size();
 
     ASTVec FalseAxioms, RemainingAxioms;
-    FalseAxioms.push_back(ASTTrue);
-    RemainingAxioms.push_back(ASTTrue);
     for (; it != itend; it++)
       {
         //Guided refinement starts here
@@ -193,38 +188,32 @@ namespace BEEV
           }
       }
 
-    writeAxiom = 
-      (FalseAxioms.size() != 1) ? 
-      bm->CreateNode(AND, FalseAxioms) : FalseAxioms[0];
-    bm->ASTNodeStats("adding false writeaxiom to SAT: ", writeAxiom);
     SOLVER_RETURN_TYPE res2 = SOLVER_UNDECIDED;
-    if (FalseAxioms.size() > oldFalseAxiomsSize)
-      {
-        res2 = CallSAT_ResultCheck(SatSolver, 
-                                   writeAxiom, 
-                                   original_input,
-                                   tosat);
-        oldFalseAxiomsSize = FalseAxioms.size();
-      }
-    if (SOLVER_UNDECIDED != res2)
-      {
-        return res2;
-      }
+    if (FalseAxioms.size() > 0)
+    {
+               writeAxiom = (FalseAxioms.size() != 1) ? bm->CreateNode(AND,
+                               FalseAxioms) : FalseAxioms[0];
+               bm->ASTNodeStats("adding false writeaxiom to SAT: ", writeAxiom);
+               res2 = CallSAT_ResultCheck(SatSolver, writeAxiom, original_input, tosat);
+       }
 
-    writeAxiom = 
-      (RemainingAxioms.size() != 1) ? 
-      bm->CreateNode(AND, RemainingAxioms) : RemainingAxioms[0];
-    bm->ASTNodeStats("adding remaining writeaxiom to SAT: ", writeAxiom);
-    res2 = CallSAT_ResultCheck(SatSolver, 
-                               writeAxiom, 
-                               original_input,
-                               tosat);
     if (SOLVER_UNDECIDED != res2)
       {
         return res2;
       }
 
-    return SOLVER_UNDECIDED;
+    if (RemainingAxioms.size() > 0)
+    {
+               writeAxiom =
+                 (RemainingAxioms.size() != 1) ?
+                 bm->CreateNode(AND, RemainingAxioms) : RemainingAxioms[0];
+               bm->ASTNodeStats("adding remaining writeaxiom to SAT: ", writeAxiom);
+               res2 = CallSAT_ResultCheck(SatSolver,
+                                                                  writeAxiom,
+                                                                  original_input,
+                                                                  tosat);
+    }
+    return res2;
   } //end of SATBased_ArrayWriteRefinement
   
   //Creates Array Write Axioms