fixed some issues with FOR-construct

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

diff --git a/src/AST/AST.h b/src/AST/AST.h
index 26ece48d6b63dbb6a9528a0e3a536aa9ac8dd59a..85ad53d4bd10096865feeb700db67ed1fb3a589f 100644 (file)
--- a/src/AST/AST.h
+++ b/src/AST/AST.h
@@ -1231,13 +1231,16 @@ namespace BEEV
                                                    const ASTNode& original_input);
     SOLVER_RETURN_TYPE SATBased_ArrayWriteRefinement(MINISAT::Solver& newS,
                                                     const ASTNode& orig_input);        
-    SOLVER_RETURN_TYPE SATBased_FiniteLoop_Refinement(MINISAT::Solver& SatSolver, 
-                                                     const ASTNode& original_input,                                              
-                                                     const ASTNode& finiteloop,
-                                                     ASTNodeMap* ParamToCurrentValMap);    
+   
     SOLVER_RETURN_TYPE SATBased_AllFiniteLoops_Refinement(MINISAT::Solver& newS, 
                                                          const ASTNode& orig_input);
-
+    
+    ASTVec SATBased_FiniteLoop_Refinement(MINISAT::Solver& SatSolver, 
+                                         const ASTNode& original_input,                                                  
+                                         const ASTNode& finiteloop,
+                                         ASTNodeMap* ParamToCurrentValMap,
+                                         bool absrefine_flag=false);    
+    
     ASTNode Check_FiniteLoop_UsingModel(const ASTNode& finiteloop,
                                        ASTNodeMap* ParamToCurrentValMap,
                                        bool CheckUsingModel_Or_Expand);

diff --git a/src/abstraction-refinement/AbstractionRefinement.cpp b/src/abstraction-refinement/AbstractionRefinement.cpp
index 852a076ff12784b91c3bb63c8c423a1986686e44..d441d43a88a68c2165e5be8e4e33394b64b0471b 100644 (file)
--- a/src/abstraction-refinement/AbstractionRefinement.cpp
+++ b/src/abstraction-refinement/AbstractionRefinement.cpp
@@ -251,45 +251,64 @@ namespace BEEV
   BeevMgr::SATBased_AllFiniteLoops_Refinement(MINISAT::Solver& SatSolver, 
                                              const ASTNode& original_input)
   {
-    SOLVER_RETURN_TYPE ret = SOLVER_UNDECIDED;
-    std::vector<SOLVER_RETURN_TYPE> retvec;
+    ASTVec retvec;
+    ASTVec Allretvec;
+    Allretvec.push_back(ASTTrue);
+    SOLVER_RETURN_TYPE res = SOLVER_UNDECIDED;
     for(ASTVec::iterator i = GlobalList_Of_FiniteLoops.begin(),
          iend=GlobalList_Of_FiniteLoops.end(); i!=iend; i++)
-      {
-        //ASTNodeMap * ParamToCurrentValMap = new ASTNodeMap;
-       ASTNodeMap ParamToCurrentValMap;
-       ret =  SATBased_FiniteLoop_Refinement(SatSolver,
-                                             original_input,
-                                             *i,
-                                             &ParamToCurrentValMap);
-        if(SOLVER_VALID == ret)
-          {
-            return ret;
-          }
-       retvec.push_back(ret);
+    {
+      //cout << "The number of abs-refinement limit is " << num_absrefine << endl;
+      for(int absrefine_count=0;absrefine_count < num_absrefine; absrefine_count++) 
+       {
+         ASTNodeMap ParamToCurrentValMap;
+         retvec =  SATBased_FiniteLoop_Refinement(SatSolver,
+                                                  original_input,
+                                                  *i,
+                                                  &ParamToCurrentValMap,
+                                                  true); //absrefine flag
+         ASTNode retformula = 
+           (retvec.size() == 1) ?
+           retvec[0] : CreateNode(AND,retvec);
+         //SimplifyFormula(CreateNode(AND,Allretvec),false,NULL);
+         retformula = TransformFormula_TopLevel(retformula);
+
+         //Add the return value of all loops to the SAT Solver
+         res = 
+           CallSAT_ResultCheck(SatSolver, retformula, original_input);
+         if(SOLVER_UNDECIDED != res) 
+           {
+             return res;
+           }     
+       } //end of absrefine count
+
+      ASTNodeMap ParamToCurrentValMap;
+      retvec =  SATBased_FiniteLoop_Refinement(SatSolver,
+                                              original_input,
+                                              *i,
+                                              &ParamToCurrentValMap,
+                                              false); //absrefine flag
+       
+      ASTNode retformula = 
+      (retvec.size() == 1) ?
+      retvec[0] : CreateNode(AND,retvec);
+      retformula = TransformFormula_TopLevel(retformula);
+      //Add the return value of all loops to the SAT Solver
+      SOLVER_RETURN_TYPE res = 
+       CallSAT_ResultCheck(SatSolver, retformula, original_input);
+      if(SOLVER_UNDECIDED != res) 
+       {
+         return res;
+       }               
       } //End of For()
 
-    //Even if one of the for loops results in SOLVER_UNDECIDED, then
-    //it means that the constructed model is bogus. Return this fact.
-    for(vector<SOLVER_RETURN_TYPE>::iterator i=retvec.begin(),
-         iend=retvec.end();i!=iend;i++) 
-      {
-       if(SOLVER_UNDECIDED == *i) 
-         {
-           return SOLVER_UNDECIDED;
-         }
-      }
-
-    //All for loops are true in the model
-    //return CallSAT_ResultCheck(SatSolver, ASTTrue, original_input);
-    return ret;
+    return res;
   } //end of SATBased_AllFiniteLoops_Refinement()
   
   
   /*****************************************************************
    * SATBased_FiniteLoop_Refinement
    *
-   *
    * 'finiteloop' is the finite loop to be expanded
    * Every finiteloop has three parts:
    * 0) Parameter Name
@@ -308,11 +327,12 @@ namespace BEEV
   //
   //Expand the finite loop, check against model, and add false
   //formulas to the SAT solver
-  SOLVER_RETURN_TYPE 
+  ASTVec
   BeevMgr::SATBased_FiniteLoop_Refinement(MINISAT::Solver& SatSolver, 
                                          const ASTNode& original_input,
                                          const ASTNode& finiteloop,
-                                         ASTNodeMap* ParamToCurrentValMap)
+                                         ASTNodeMap* ParamToCurrentValMap,
+                                         bool absrefine_flag)
   {     
     //BVTypeCheck should have already checked the sanity of the input
     //FOR-formula
@@ -329,23 +349,27 @@ namespace BEEV
     (*ParamToCurrentValMap)[parameter] = 
       CreateBVConst(finiteloop[1].GetValueWidth(),paramCurrentValue);
     
-    SOLVER_RETURN_TYPE ret = SOLVER_UNDECIDED;
     //Go recursively thru' all the FOR-constructs.
     if(FOR == formulabody.GetKind()) 
       { 
+       ASTVec retvec;
+       ASTVec retvec_innerfor;
+       retvec.push_back(ASTTrue);
         while(paramCurrentValue < paramLimit) 
           {
-            ret = SATBased_FiniteLoop_Refinement(SatSolver, 
-                                                original_input,
-                                                formulabody, 
-                                                ParamToCurrentValMap);
-           if(SOLVER_VALID == ret) 
+            retvec_innerfor = 
+             SATBased_FiniteLoop_Refinement(SatSolver, 
+                                            original_input,
+                                            formulabody, 
+                                            ParamToCurrentValMap,
+                                            absrefine_flag);
+
+           for(ASTVec::iterator i=retvec_innerfor.begin(),
+                 iend=retvec_innerfor.end();i!=iend;i++)
              {
-               //If formula is valid, return immediately
-               return ret;
+               retvec.push_back(*i);
              }
 
-
             //Update ParamToCurrentValMap with parameter and its
             //current value. FIXME: Possible leak since I am not
             //freeing the previous 'value' for the same 'key'
@@ -354,16 +378,14 @@ namespace BEEV
              CreateBVConst(finiteloop[1].GetValueWidth(),paramCurrentValue);
           } //end of While
 
-       //The last 'ret' value is the truthvalue of the formula. If it
-       //is SOLVER_INVALID then the formula is indeed INVALID, else
-       //ret can only be SOLVER_UNDECIDED at this point. Hence return
-       //UNDECIDED.
-       return ret;
+       return retvec;
       } //end of recursion FORs
 
     //Expand the leaf level FOR-construct completely
     //increment of paramCurrentValue done inside loop
     int ThisForLoopAllTrue = 0;
+    ASTVec ForloopVec;
+    ForloopVec.push_back(ASTTrue);
     for(;paramCurrentValue < paramLimit;) 
       {
         ASTNode currentFormula;
@@ -381,40 +403,33 @@ namespace BEEV
 
         //Check the currentformula against the model, and add it to the
         //SAT solver if it is false against the model
-        if(ASTFalse == ComputeFormulaUsingModel(currentFormula)) 
-          {
-            currentFormula = TransformFormula_TopLevel(currentFormula);
-           SOLVER_RETURN_TYPE result = 
-              CallSAT_ResultCheck(SatSolver, currentFormula, original_input);
-            if(result != SOLVER_UNDECIDED)           
-              {
-                return result;
-              }
+        if(absrefine_flag && 
+          ASTFalse == ComputeFormulaUsingModel(currentFormula)) 
+         {
+           ForloopVec.push_back(currentFormula);
           }
        else 
          {
-           //ComputeFormulaUsingModel can either return ASTFalse or
-           //ASTTrue
-           ThisForLoopAllTrue++;           
+           if(ASTTrue != currentFormula)
+             {
+               ForloopVec.push_back(currentFormula);
+             }
+           if(ASTFalse == currentFormula)
+             {
+               ForloopVec.push_back(ASTFalse);
+               return ForloopVec;
+             }
          }
         
         //Update ParamToCurrentValMap with parameter and its current
-        //value 
-        //
-        //FIXME: Possible leak since I am not freeing the previous
-        //'value' for the same 'key'
+        //value. FIXME: Possible leak since I am not freeing the
+        //previous 'value' for the same 'key'
        paramCurrentValue = paramCurrentValue + paramIncrement;
         (*ParamToCurrentValMap)[parameter] = 
-         CreateBVConst(finiteloop[1].GetValueWidth(),paramCurrentValue);
-       //cout << (*ParamToCurrentValMap)[parameter];
+         CreateBVConst(finiteloop[1].GetValueWidth(),paramCurrentValue);       
       } //end of expanding the FOR loop
     
-    if(ThisForLoopAllTrue == paramLimit) 
-      {
-       return SOLVER_INVALID;
-      }
-
-    return SOLVER_UNDECIDED;
+    return ForloopVec;
   } //end of the SATBased_FiniteLoop_Refinement()
 
   //SATBased_FiniteLoop_Refinement_UsingModel  

diff --git a/src/main/Globals.cpp b/src/main/Globals.cpp
index dd359476d91f95920d28713ff9296a2df30029c8..cc6e725b70008f370843c3a419dd0255d128fbc2 100644 (file)
--- a/src/main/Globals.cpp
+++ b/src/main/Globals.cpp
@@ -42,7 +42,13 @@ namespace BEEV
   bool print_binary_flag = false;
 
   //Expands out the finite for-construct completely
-  bool expand_finitefor_flag;
+  bool expand_finitefor_flag = false;
+
+  //Determines the number of abstraction-refinement loop count for the
+  //for-construct
+  bool num_absrefine_flag = false;
+  int num_absrefine = 0;
+
 
   //if this option is true then print the way dawson wants using a
   //different printer. do not use this printer.

diff --git a/src/main/Globals.h b/src/main/Globals.h
index 6d1b4ae1692da64864cce42c3812a4d8b6c069f5..fca9d4095b045d5b78d6b19c0d316bf7b3d33d7d 100644 (file)
--- a/src/main/Globals.h
+++ b/src/main/Globals.h
@@ -70,6 +70,11 @@ namespace BEEV
   //Expands out the finite for-construct completely
   extern bool expand_finitefor_flag;
 
+  //Determines the number of abstraction-refinement loop count for the
+  //for-construct
+  extern bool num_absrefine_flag;
+  extern int num_absrefine;
+
   //if this option is true then print the way dawson wants using a
   //different printer. do not use this printer.
   extern bool print_arrayval_declaredorder_flag;

diff --git a/src/main/main.cpp b/src/main/main.cpp
index 16cc0eb85823fd5d6d2b0ec2a21a24ccb96155c2..76c1c29275676cbfc2d73ed2227316acb34472ba 100644 (file)
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -51,6 +51,7 @@ int main(int argc, char ** argv) {
   helpstring +=  "-c  : construct counterexample\n";
   helpstring +=  "-d  : check counterexample\n";
   helpstring +=  "-e  : expand finite-for construct\n";
+  helpstring +=  "-f  : number of abstraction-refinement loops\n";
   helpstring +=  "-h  : help\n";
   helpstring +=  "-m  : use the SMTLIB parser\n";
   helpstring +=  "-p  : print counterexample\n";
@@ -65,6 +66,13 @@ int main(int argc, char ** argv) {
     {
       if(argv[i][0] == '-')
         {
+          if(argv[i][2]) {
+            fprintf(stderr, "Multiple character options are not allowed.\n");
+            fprintf(stderr, "(for example: -ab is not an abbreviation for -a -b)\n");
+            fprintf(stderr,usage,prog);
+            cout << helpstring;
+            return -1;
+          }
           switch(argv[i][1])
             {
             case 'a' :
@@ -83,6 +91,10 @@ int main(int argc, char ** argv) {
            case 'e':
              expand_finitefor_flag = true;
              break;
+           case 'f':
+             num_absrefine_flag = true;
+             num_absrefine = atoi(argv[++i]);
+             break;            
             case 'h':
               fprintf(stderr,usage,prog);
               cout << helpstring;
@@ -133,16 +145,8 @@ int main(int argc, char ** argv) {
               return -1;
               break;
             }
-          if(argv[i][2]) {
-            fprintf(stderr, "Multiple character options are not allowed.\n");
-            fprintf(stderr, "(for example: -ab is not an abbreviation for -a -b)\n");
-            fprintf(stderr,usage,prog);
-            cout << helpstring;
-            return -1;
-          }
-        } else {
+        } else {         
           infile = argv[i];
-
           if (smtlib_parser_flag)
             {
               smtin = fopen(infile,"r");

diff --git a/src/sat/sat.h b/src/sat/sat.h
index f17456c62997b62ccdaccde07c662a236e4bc371..c6e9224805dbbcd7f0360775a3a9c42eb55d45a2 100644 (file)
--- a/src/sat/sat.h
+++ b/src/sat/sat.h
@@ -3,17 +3,7 @@
 
 #include "core/Solver.h"
 #include "core/SolverTypes.h"
-//#include "../sat/simp/SimpSolver.h"
-//#include "../sat/unsound/UnsoundSimpSolver.h"
-
-
-#endif /* SAT_H_ */
-#ifndef SAT_H_
-#define SAT_H_
-
-#include "core/Solver.h"
-#include "core/SolverTypes.h"
-//#include "../sat/simp/SimpSolver.h"
+#include "../sat/simp/SimpSolver.h"
 //#include "../sat/unsound/UnsoundSimpSolver.h"
 
 

diff --git a/src/sat/unsound/UnsoundSimpSolver.C b/src/sat/unsound/UnsoundSimpSolver.C
index 72f40cce2ad98f418a6e7de696e65820f5d9afbd..1901ccca0d776a42703fba6fa85bf704a99f261b 100644 (file)
--- a/src/sat/unsound/UnsoundSimpSolver.C
+++ b/src/sat/unsound/UnsoundSimpSolver.C
@@ -491,30 +491,32 @@ bool UnsoundSimpSolver::eliminateVar(Var v, bool fail, bool stop_unsoundness)
                 return false;
 
 
-    if(!stop_unsoundness) {
-      //abductive logic
-      vec<Lit > resolvedClauses;
-      for (int i = 0; i < pos.size(); i++) {
-       for (int j = 0; j < pos.size(); j++) {
+    if(!stop_unsoundness) 
+      {
+       //abductive logic
+       vec<Lit > resolvedClauses;
+       for (int i = 0; i < pos.size(); i++) {
+         for (int j = 0; j < pos.size(); j++) {
+           if(i == j) 
+             continue;
+           abductive_merge(*pos[i], *pos[j], v, resolvedClauses, true);          
+           if(!addClause(resolvedClauses))
+             return false;
+         }
+       }
+       //}
+
+      resolvedClauses.clear();
+      for (int i = 0; i < neg.size(); i++) {
+       for (int j = 0; j < neg.size(); j++) {
          if(i == j) 
            continue;
-         abductive_merge(*pos[i], *pos[j], v, resolvedClauses, true);    
+         abductive_neg_merge(*neg[i], *neg[j], v, resolvedClauses,true);
          if(!addClause(resolvedClauses))
-           return false;
+           return false;       
        }
-      }
-    }
-//       resolvedClauses.clear();
-//       for (int i = 0; i < neg.size(); i++) {
-//     for (int j = 0; j < neg.size(); j++) {
-//       if(i == j) 
-//         continue;
-//       abductive_neg_merge(*neg[i], *neg[j], v, resolvedClauses,true);
-//       if(!addClause(resolvedClauses))
-//         return false;       
-//     }
-//      }
-//    }
+     }
+   }
 
     // DEBUG: For checking that a clause set is saturated with respect
     //        to variable elimination.  If the clause set is expected

diff --git a/src/simplifier/bvsolver.cpp b/src/simplifier/bvsolver.cpp
index 4d68ab63fdd7416ea7b3ef5496874602cc18521d..a51549d59f083b7cdff37babfb4cc5fac1ec140e 100644 (file)
--- a/src/simplifier/bvsolver.cpp
+++ b/src/simplifier/bvsolver.cpp
@@ -310,7 +310,7 @@ namespace BEEV
   {
     ASTNode eq = input;
     //cerr << "Input to BVSolve_Odd()" << eq << endl;
-    if (!(wordlevel_solve_flag && EQ == eq.GetKind()))
+    if (!(EQ == eq.GetKind()))
       {
         return input;
       }
@@ -524,10 +524,10 @@ namespace BEEV
   //the formula
   ASTNode BVSolver::TopLevelBVSolve(const ASTNode& input)
   {
-    if (!wordlevel_solve_flag)
-      {
-        return input;
-      }
+    //    if (!wordlevel_solve_flag)
+    //       {
+    //         return input;
+    //       }
 
     Kind k = input.GetKind();
     if (!(EQ == k || AND == k))
@@ -596,7 +596,7 @@ namespace BEEV
   {
     ASTNode eq = input;
     //cerr << "Input to BVSolve_Odd()" << eq << endl;
-    if (!(wordlevel_solve_flag && EQ == eq.GetKind()))
+    if (!(EQ == eq.GetKind()))
       {
         evenflag = false;
         return eq;
@@ -652,10 +652,10 @@ namespace BEEV
   //solve an eqn whose monomials have only even coefficients
   ASTNode BVSolver::BVSolve_Even(const ASTNode& input)
   {
-    if (!wordlevel_solve_flag)
-      {
-        return input;
-      }
+    //     if (!wordlevel_solve_flag)
+    //       {
+    //         return input;
+    //       }
 
     if (!(EQ == input.GetKind() || AND == input.GetKind()))
       {

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index 5e8f8647307660cc9cefa631632ed60490dac0d2..187e40a64ea2f11bd5c40f9875e94848e7223240 100644 (file)
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -324,8 +324,8 @@ ASTNode Flatten(const ASTNode& a)
   BeevMgr::SimplifyFormula(const ASTNode& b, 
                           bool pushNeg, ASTNodeMap* VarConstMap)
   {
-    if (!optimize_flag)
-      return b;
+//     if (!optimize_flag)
+//       return b;
 
     Kind kind = b.GetKind();
     if (BOOLEAN_TYPE != b.GetType())
@@ -404,8 +404,8 @@ ASTNode Flatten(const ASTNode& a)
   BeevMgr::SimplifyAtomicFormula(const ASTNode& a, 
                                 bool pushNeg, ASTNodeMap* VarConstMap)
   {
-    if (!optimize_flag)
-      return a;
+//     if (!optimize_flag)
+//       return a;
 
     ASTNode output;
     if (CheckSimplifyMap(a, output, pushNeg, VarConstMap))
@@ -686,7 +686,7 @@ ASTNode Flatten(const ASTNode& a)
   {
     CountersAndStats("ITEOpts_InEqs");
 
-    if (!(EQ == in.GetKind() && optimize_flag))
+    if (!(EQ == in.GetKind()))
       {
         return in;
       }
@@ -1258,8 +1258,8 @@ ASTNode Flatten(const ASTNode& a)
 
   ASTNode BeevMgr::SimplifyIteFormula(const ASTNode& b, bool pushNeg, ASTNodeMap* VarConstMap)
   {
-    if (!optimize_flag)
-      return b;
+ //    if (!optimize_flag)
+//       return b;
 
     ASTNode output;
     if (CheckSimplifyMap(b, output, pushNeg, VarConstMap))
@@ -1395,10 +1395,10 @@ ASTNode Flatten(const ASTNode& a)
     ASTNode inputterm(actualInputterm); // mutable local copy.
 
     //cout << "SimplifyTerm: input: " << a << endl;
-    if (!optimize_flag)
-      {
-        return inputterm;
-      }
+    // if (!optimize_flag)
+    //       {
+    //         return inputterm;
+    //       }
 
     ASTNode output;
     assert(BVTypeCheck(inputterm));

diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp
index 76232f011b83d39ebe14c1184d38d03c07783ad9..d7b96c5145bb1505e0758384fd4c7af9045054f2 100644 (file)
--- a/src/to-sat/ToSAT.cpp
+++ b/src/to-sat/ToSAT.cpp
@@ -938,23 +938,32 @@ namespace BEEV
       {
         inputToSAT = simplified_solved_InputToSAT;
 
-        simplified_solved_InputToSAT = 
-          CreateSubstitutionMap(simplified_solved_InputToSAT);
-        //printf("##################################################\n");
-        ASTNodeStats("after pure substitution: ", simplified_solved_InputToSAT);
-
-        simplified_solved_InputToSAT = 
-          SimplifyFormula_TopLevel(simplified_solved_InputToSAT, false);
-        ASTNodeStats("after simplification: ", simplified_solved_InputToSAT);
-
-        simplified_solved_InputToSAT = 
-          bvsolver->TopLevelBVSolve(simplified_solved_InputToSAT);
-        ASTNodeStats("after solving: ", simplified_solved_InputToSAT);
+       if(optimize_flag) 
+         {
+
+           simplified_solved_InputToSAT = 
+             CreateSubstitutionMap(simplified_solved_InputToSAT);
+           //printf("##################################################\n");
+           ASTNodeStats("after pure substitution: ", simplified_solved_InputToSAT);
+
+           simplified_solved_InputToSAT = 
+             SimplifyFormula_TopLevel(simplified_solved_InputToSAT, false);
+           ASTNodeStats("after simplification: ", simplified_solved_InputToSAT);
+         }
+
+       if(wordlevel_solve_flag)
+         {
+           simplified_solved_InputToSAT = 
+             bvsolver->TopLevelBVSolve(simplified_solved_InputToSAT);
+           ASTNodeStats("after solving: ", simplified_solved_InputToSAT);
+         }
 
       } 
     while (inputToSAT != simplified_solved_InputToSAT);
 
-    ASTNodeStats("Before SimplifyWrites_Inplace begins: ", simplified_solved_InputToSAT);
+    ASTNodeStats("Before SimplifyWrites_Inplace begins: ", 
+                simplified_solved_InputToSAT);
+
     SimplifyWrites_InPlace_Flag = true;
     Begin_RemoveWrites = false;
     start_abstracting = false;
@@ -962,22 +971,27 @@ namespace BEEV
     do
       {
         inputToSAT = simplified_solved_InputToSAT;
-        simplified_solved_InputToSAT = 
-          CreateSubstitutionMap(simplified_solved_InputToSAT);
-        ASTNodeStats("after pure substitution: ", simplified_solved_InputToSAT);
+
+       if(optimize_flag) 
+         {
+           simplified_solved_InputToSAT = 
+             CreateSubstitutionMap(simplified_solved_InputToSAT);
+           ASTNodeStats("after pure substitution: ", simplified_solved_InputToSAT);
+
+           simplified_solved_InputToSAT = 
+             SimplifyFormula_TopLevel(simplified_solved_InputToSAT, false);
+           ASTNodeStats("after simplification: ", simplified_solved_InputToSAT);
+         }
+       
+       if(wordlevel_solve_flag)
+         {
+           simplified_solved_InputToSAT = 
+             bvsolver->TopLevelBVSolve(simplified_solved_InputToSAT);
+           ASTNodeStats("after solving: ", simplified_solved_InputToSAT);
+         }
+      } while (inputToSAT != simplified_solved_InputToSAT);
     
-       simplified_solved_InputToSAT = 
-          SimplifyFormula_TopLevel(simplified_solved_InputToSAT, false);
-        ASTNodeStats("after simplification: ", simplified_solved_InputToSAT);
-        
-       simplified_solved_InputToSAT = 
-          bvsolver->TopLevelBVSolve(simplified_solved_InputToSAT);
-        ASTNodeStats("after solving: ", simplified_solved_InputToSAT);
-      
-      } 
-    while (inputToSAT != simplified_solved_InputToSAT);
     ASTNodeStats("After SimplifyWrites_Inplace: ", simplified_solved_InputToSAT);
-
     delete bvsolver;
     bvsolver = NULL;
 
@@ -990,21 +1004,31 @@ namespace BEEV
       }
 
     TermsAlreadySeenMap.clear();
-    do
-      {
-        inputToSAT = simplified_solved_InputToSAT;
-        //simplified_solved_InputToSAT =
-        //CreateSubstitutionMap(simplified_solved_InputToSAT);
-        //Begin_RemoveWrites = true; ASTNodeStats("after pure
-        //substitution: ", simplified_solved_InputToSAT);
-        simplified_solved_InputToSAT = 
-          SimplifyFormula_TopLevel(simplified_solved_InputToSAT, false);
-        //ASTNodeStats("after simplification: ",
-        //simplified_solved_InputToSAT); simplified_solved_InputToSAT
-        //= bvsolver.TopLevelBVSolve(simplified_solved_InputToSAT);
-        //ASTNodeStats("after solving: ",
-        //simplified_solved_InputToSAT);
-      } while (inputToSAT != simplified_solved_InputToSAT);
+    // do
+//       {
+//         inputToSAT = simplified_solved_InputToSAT;
+
+//     if(optimize_flag) 
+//       {
+//         //simplified_solved_InputToSAT =
+//         //CreateSubstitutionMap(simplified_solved_InputToSAT);
+//         //Begin_RemoveWrites = true; ASTNodeStats("after pure
+//         //substitution: ", simplified_solved_InputToSAT);
+//         simplified_solved_InputToSAT = 
+//           SimplifyFormula_TopLevel(simplified_solved_InputToSAT, false);
+//         //ASTNodeStats("after simplification: ",
+//         //simplified_solved_InputToSAT); 
+//         //
+//       }
+
+//     if(wordlevel_solve_flag)
+//       {
+//         simplified_solved_InputToSAT
+//           = bvsolver.TopLevelBVSolve(simplified_solved_InputToSAT);
+//         ASTNodeStats("after solving: ",
+//                      simplified_solved_InputToSAT);
+//       }
+//       } while (inputToSAT != simplified_solved_InputToSAT);
 
     if (start_abstracting)
       {