added enum for Solver returntype

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

diff --git a/src/AST/AST.h b/src/AST/AST.h
index 0bbcb7749010f342a5b88fc479f2e0a43249d315..e7d84f9e49e919dc0682a2336ca635be03161cea 100644 (file)
--- a/src/AST/AST.h
+++ b/src/AST/AST.h
@@ -64,6 +64,12 @@ namespace BEEV
       BOOLEAN_TYPE = 0, BITVECTOR_TYPE, ARRAY_TYPE, UNKNOWN_TYPE
     };
 
+  enum SOLVER_RETURN_TYPE 
+    {
+      SOLVER_INVALID=0, SOLVER_VALID=1, SOLVER_UNDECIDED=2, SOLVER_ERROR=-100
+    };
+
+
   class BeevMgr;
   class ASTNode;
   class ASTInternal;
@@ -1218,15 +1224,20 @@ namespace BEEV
     void ClearAllTables(void);
     void ClearAllCaches(void);
     int  BeforeSAT_ResultCheck(const ASTNode& q);
-    int  CallSAT_ResultCheck(MINISAT::Solver& newS, 
-                            const ASTNode& q, const ASTNode& orig_input);
-    int  SATBased_ArrayReadRefinement(MINISAT::Solver& newS, 
-                                     const ASTNode& q, const ASTNode& orig_input);
-    int  SATBased_ArrayWriteRefinement(MINISAT::Solver& newS, const ASTNode& orig_input);
+    SOLVER_RETURN_TYPE  CallSAT_ResultCheck(MINISAT::Solver& newS,
+                                           const ASTNode& modified_input, 
+                                           const ASTNode& original_input);
+    SOLVER_RETURN_TYPE  SATBased_ArrayReadRefinement(MINISAT::Solver& newS, 
+                                                    const ASTNode& modified_input, 
+                                                    const ASTNode& original_input);
+    SOLVER_RETURN_TYPE  SATBased_ArrayWriteRefinement(MINISAT::Solver& newS,
+                                                     const ASTNode& orig_input);
         
-    int  SATBased_FiniteLoop_Refinement(MINISAT::Solver& newS, const ASTNode& orig_input);
+    SOLVER_RETURN_TYPE  SATBased_FiniteLoop_Refinement(MINISAT::Solver& newS, 
+                                                      const ASTNode& orig_input);
     void Expand_FiniteLoop(MINISAT::Solver& SatSolver, const ASTNode& original_input,
-                          const ASTNode& finiteloop,ASTNodeMap* ParamToCurrentValMap);
+                          const ASTNode& finiteloop,ASTNodeMap* ParamToCurrentValMap,
+                          bool AbstractionRefinement=true);
     ASTNode FiniteLoop_Extract_SingleFormula(const ASTNode& finiteloop_formulabody, 
                                              ASTNodeMap* VarConstMap);
 

diff --git a/src/AST/AbstractionRefinement.cpp b/src/AST/AbstractionRefinement.cpp
index 9b860fa75fa20a96fc2bb318ccf563a884609f72..51ae36147940ae72ed0d7f3d8be6cc52d2b95d2f 100644 (file)
--- a/src/AST/AbstractionRefinement.cpp
+++ b/src/AST/AbstractionRefinement.cpp
@@ -17,9 +17,9 @@ namespace BEEV
    * Abstraction Refinement related functions
    ******************************************************************/  
   
-  int BeevMgr::SATBased_ArrayReadRefinement(MINISAT::Solver& SatSolver, 
-                                            const ASTNode& inputAlreadyInSAT, 
-                                           const ASTNode& original_input) {
+  SOLVER_RETURN_TYPE BeevMgr::SATBased_ArrayReadRefinement(MINISAT::Solver& SatSolver, 
+                                                          const ASTNode& inputAlreadyInSAT, 
+                                                          const ASTNode& original_input) {
     //go over the list of indices for each array, and generate Leibnitz
     //axioms. Then assert these axioms into the SAT solver. Check if the
     //addition of the new constraints has made the bogus counterexample
@@ -116,7 +116,7 @@ namespace BEEV
               CreateNode(AND, FalseAxiomsVec) : FalseAxiomsVec[0];
             ASTNodeStats("adding false readaxioms to SAT: ", FalseAxioms);
             //printf("spot 01\n");
-            int res2 = 2;
+            SOLVER_RETURN_TYPE res2 = SOLVER_UNDECIDED;
             //if (FalseAxiomsVec.size() > 0)
             if (FalseAxiomsVec.size() > oldFalseAxiomsSize)
               {
@@ -124,7 +124,7 @@ namespace BEEV
                 oldFalseAxiomsSize = FalseAxiomsVec.size();
               }
             //printf("spot 02, res2 = %d\n", res2);
-            if (2 != res2)
+            if (SOLVER_UNDECIDED != res2)
               {
                 return res2;
               }
@@ -150,7 +150,8 @@ namespace BEEV
     return arraywrite_axiom;
   }//end of Create_ArrayWriteAxioms()
 
-  int BeevMgr::SATBased_ArrayWriteRefinement(MINISAT::Solver& SatSolver, const ASTNode& original_input)
+  SOLVER_RETURN_TYPE BeevMgr::SATBased_ArrayWriteRefinement(MINISAT::Solver& SatSolver, 
+                                                           const ASTNode& original_input)
   {
     ASTNode writeAxiom;
     ASTNodeMap::iterator it = ReadOverWrite_NewName_Map.begin();
@@ -183,13 +184,13 @@ namespace BEEV
       (FalseAxioms.size() != 1) ? 
       CreateNode(AND, FalseAxioms) : FalseAxioms[0];
     ASTNodeStats("adding false writeaxiom to SAT: ", writeAxiom);
-    int res2 = 2;
+    SOLVER_RETURN_TYPE res2 = SOLVER_UNDECIDED;
     if (FalseAxioms.size() > oldFalseAxiomsSize)
       {
         res2 = CallSAT_ResultCheck(SatSolver, writeAxiom, original_input);
         oldFalseAxiomsSize = FalseAxioms.size();
       }
-    if (2 != res2)
+    if (SOLVER_UNDECIDED != res2)
       {
         return res2;
       }
@@ -199,18 +200,18 @@ namespace BEEV
       CreateNode(AND, RemainingAxioms) : RemainingAxioms[0];
     ASTNodeStats("adding remaining writeaxiom to SAT: ", writeAxiom);
     res2 = CallSAT_ResultCheck(SatSolver, writeAxiom, original_input);
-    if (2 != res2)
+    if (SOLVER_UNDECIDED != res2)
       {
         return res2;
       }
 
-    return 2;
+    return SOLVER_UNDECIDED;
   } //end of SATBased_ArrayWriteRefinement
 
   //Expands all finite-for-loops using counterexample-guided
   //abstraction-refinement.
-  int BeevMgr::SATBased_FiniteLoop_Refinement(MINISAT::Solver& SatSolver, 
-                                              const ASTNode& original_input)
+  SOLVER_RETURN_TYPE BeevMgr::SATBased_FiniteLoop_Refinement(MINISAT::Solver& SatSolver, 
+                                                            const ASTNode& original_input)
   {
     /*
      * For each 'finiteloop' in the global list 'List_Of_FiniteLoops'
@@ -231,10 +232,9 @@ namespace BEEV
      */
   }
 
-  void BeevMgr::Expand_FiniteLoop(MINISAT::Solver& SatSolver,
-                                 const ASTNode& original_input,
-                                 const ASTNode& finiteloop,
-                                 ASTNodeMap* ParamToCurrentValMap) {
+  void BeevMgr::Expand_FiniteLoop(MINISAT::Solver& SatSolver, const ASTNode& original_input,
+                                 const ASTNode& finiteloop, ASTNodeMap* ParamToCurrentValMap,
+                                 bool AbstractionRefinement) {
     /*
      * 'finiteloop' is the finite loop to be expanded
      * 
@@ -316,33 +316,43 @@ namespace BEEV
          (*ParamToCurrentValMap)[parameter] = CreateBVConst(32,paramCurrentValue);
        } //end of While
       }
-    else 
+
+    ASTVec forloopFormulaVector;
+    //Expand the leaf level FOR-construct completely
+    for(; 
+       paramCurrentValue < paramLimit; 
+       paramCurrentValue = paramCurrentValue + paramIncrement) 
       {
-      //Expand the leaf level FOR-construct completely
-      for(; 
-          paramCurrentValue < paramLimit; 
-          paramCurrentValue = paramCurrentValue + paramIncrement) 
-       {
         ASTNode currentFormula = 
           FiniteLoop_Extract_SingleFormula(formulabody, ParamToCurrentValMap);
-      
-        //Check the currentformula against the model, and add it to the
-        //SAT solver if it is false against the model
-       ASTNode formulaInModel = ComputeFormulaUsingModel(currentFormula);
-
-       int result = 0;
-       if(ASTFalse == formulaInModel) {
-         result = CallSAT_ResultCheck(SatSolver, currentFormula, original_input);
-       }
-
-        //Update ParamToCurrentValMap with parameter and its current
-        //value 
-        //
-        //FIXME: Possible leak since I am not freeing the previous
-        //'value' for the same 'key'
-        (*ParamToCurrentValMap)[parameter] = CreateBVConst(32,paramCurrentValue);
-      }
-    } //end of else
+       
+       if(AbstractionRefinement) 
+         {
+           int result = 0;
+           //Check the currentformula against the model, and add it to the
+           //SAT solver if it is false against the model
+           if(ASTFalse == ComputeFormulaUsingModel(currentFormula)) {
+             forloopFormulaVector.push_back(currentFormula);
+           }
+       
+           //Update ParamToCurrentValMap with parameter and its current
+           //value 
+           //
+           //FIXME: Possible leak since I am not freeing the previous
+           //'value' for the same 'key'
+           (*ParamToCurrentValMap)[parameter] = CreateBVConst(32,paramCurrentValue);
+         } //end of if
+       else 
+         {
+           forloopFormulaVector.push_back(currentFormula);
+         }
+      } //end of for
+    
+    ASTNode forloopFormulas = 
+      (forloopFormulaVector.size() != 1) ?
+      CreateNode(AND, forloopFormulaVector) : forloopFormulaVector[0];
+    
+    //result = CallSAT_ResultCheck(SatSolver, forloopFormulas, original_input);
   } //end of the Expand_FiniteLoop()
 
   ASTNode BeevMgr::FiniteLoop_Extract_SingleFormula(const ASTNode& formulabody, 

diff --git a/src/AST/ToCNF.cpp b/src/AST/ToCNF.cpp
index 3ceb73c45bd95b124355a5bf4188547f5114c837..dc90b51952a372dcdb3d7758d9293c94645b4255 100644 (file)
--- a/src/AST/ToCNF.cpp
+++ b/src/AST/ToCNF.cpp
@@ -1777,37 +1777,42 @@ namespace BEEV
     delete cllp;
   }
 
-  int BeevMgr::CallSAT_ResultCheck(MINISAT::Solver& newS, 
-                                   const ASTNode& q, const ASTNode& orig_input)
+  //Call the SAT solver, and check the result before returning. This
+  //can return one of 3 values, SOLVER_VALID, SOLVER_INVALID or SOLVER_UNDECIDED
+  SOLVER_RETURN_TYPE BeevMgr::CallSAT_ResultCheck(MINISAT::Solver& SatSolver, 
+                                                 const ASTNode& modified_input, 
+                                                 const ASTNode& original_input)
   {
-    ASTNode BBFormula = BBForm(q);
+    ASTNode BBFormula = BBForm(modified_input);
     CNFMgr* cm = new CNFMgr(this);
     ClauseList* cl = cm->convertToCNF(BBFormula);
     if (stats_flag)
+      {
       cerr << "Number of clauses:" << cl->size() << endl;
+      }
     //PrintClauseList(cout, *cl);
-    bool sat = toSATandSolve(newS, *cl);
+    bool sat = toSATandSolve(SatSolver, *cl);
     cm->DELETE(cl);
     delete cm;
 
     if (!sat)
       {
         PrintOutput(true);
-        return 1;
+        return SOLVER_VALID;
       }
-    else if (newS.okay())
+    else if (SatSolver.okay())
       {
         CounterExampleMap.clear();
-        ConstructCounterExample(newS);
+        ConstructCounterExample(SatSolver);
         if (stats_flag && print_nodes_flag)
           {
-            PrintSATModel(newS);
+            PrintSATModel(SatSolver);
           }
         //check if the counterexample is good or not
         ComputeFormulaMap.clear();
         if (counterexample_checking_during_refinement)
           bvdiv_exception_occured = false;
-        ASTNode orig_result = ComputeFormulaUsingModel(orig_input);
+        ASTNode orig_result = ComputeFormulaUsingModel(original_input);
         if (!(ASTTrue == orig_result || ASTFalse == orig_result))
           FatalError("TopLevelSat: Original input must compute to "\
                     "true or false against model");
@@ -1816,11 +1821,11 @@ namespace BEEV
         // invalid
         if (ASTTrue == orig_result)
           {
-            //CheckCounterExample(newS.okay());
+            //CheckCounterExample(SatSolver.okay());
             PrintOutput(false);
-            PrintCounterExample(newS.okay());
-            PrintCounterExample_InOrder(newS.okay());
-            return 0;
+            PrintCounterExample(SatSolver.okay());
+            PrintCounterExample_InOrder(SatSolver.okay());
+            return SOLVER_INVALID;
           }
         // counterexample is bogus: flag it
         else
@@ -1834,13 +1839,14 @@ namespace BEEV
                 print_counterexample_flag = tmp;
               }
 
-            return 2;
+            return SOLVER_UNDECIDED;
           }
       }
     else
       {
+       //Control should never reach here
         PrintOutput(true);
-        return -100;
+        return SOLVER_ERROR;
       }
   } //end of CALLSAT_ResultCheck
 

diff --git a/src/AST/ToSAT.cpp b/src/AST/ToSAT.cpp
index f716c6a199ffa9c3721fe3cd0a9e7f55b0445e14..bf4bc2641817e877071a454996a404e660935fae 100644 (file)
--- a/src/AST/ToSAT.cpp
+++ b/src/AST/ToSAT.cpp
@@ -909,11 +909,9 @@ namespace BEEV
   //##################################################
   //##################################################
 
-  // FIXME:  Don't use numeric codes.  Use an enum type!
   //Acceps a query, calls the SAT solver and generates Valid/InValid.
-  //if returned 0 then input is INVALID
-  //if returned 1 then input is VALID
-  //if returned 2 then ERROR
+  //if returned 0 then input is INVALID if returned 1 then input is
+  //VALID if returned 2 then UNDECIDED
   int BeevMgr::TopLevelSATAux(const ASTNode& inputasserts)
   {
     ASTNode inputToSAT = inputasserts;
@@ -998,10 +996,7 @@ namespace BEEV
     ASTNodeStats("after transformation: ", simplified_solved_InputToSAT);
     TermsAlreadySeenMap.clear();
 
-    //if(stats_flag)
-    //  printCacheStatus();
-
-    int res;
+    SOLVER_RETURN_TYPE res;
     //solver instantiated here
     MINISAT::Solver newS;
     //MINISAT::SimpSolver newS;
@@ -1012,28 +1007,28 @@ namespace BEEV
       }
 
     res = CallSAT_ResultCheck(newS, simplified_solved_InputToSAT, orig_input);
-    if (2 != res)
+    if (SOLVER_UNDECIDED != res)
       {
         CountersAndStats("print_func_stats");
         return res;
       }
 
     res = SATBased_ArrayReadRefinement(newS, simplified_solved_InputToSAT, orig_input);
-    if (2 != res)
+    if (SOLVER_UNDECIDED != res)
       {
         CountersAndStats("print_func_stats");
         return res;
       }
 
     res = SATBased_ArrayWriteRefinement(newS, orig_input);
-    if (2 != res)
+    if (SOLVER_UNDECIDED != res)
       {
         CountersAndStats("print_func_stats");
         return res;
       }
 
     res = SATBased_ArrayReadRefinement(newS, simplified_solved_InputToSAT, orig_input);
-    if (2 != res)
+    if (SOLVER_UNDECIDED != res)
       {
         CountersAndStats("print_func_stats");
         return res;
@@ -1042,8 +1037,8 @@ namespace BEEV
     FatalError("TopLevelSATAux: reached the end without proper conclusion:"
                "either a divide by zero in the input or a bug in STP");
     //bogus return to make the compiler shut up
-    return 2;
-  } //End of TopLevelSAT
+    return SOLVER_ERROR;
+  } //End of TopLevelSATAux
 
   /*******************************************************************
    * Helper Functions

diff --git a/src/AST/printer/AssortedPrinters.cpp b/src/AST/printer/AssortedPrinters.cpp
index 42aa67ae9766991a6909b979545ef98ee1b079a2..2a56271cff36f4707c4200d45b8883d47ce9685a 100644 (file)
--- a/src/AST/printer/AssortedPrinters.cpp
+++ b/src/AST/printer/AssortedPrinters.cpp
@@ -279,11 +279,13 @@ namespace BEEV
       {
         if (smtlib_parser_flag)
           {
-            if (true_iff_valid && (BEEV::input_status == TO_BE_SATISFIABLE))
+            if (true_iff_valid && 
+               (BEEV::input_status == TO_BE_SATISFIABLE))
               {
                 cerr << "Warning. Expected satisfiable, FOUND unsatisfiable" << endl;
               }
-            else if (!true_iff_valid && (BEEV::input_status == TO_BE_UNSATISFIABLE))
+            else if (!true_iff_valid && 
+                    (BEEV::input_status == TO_BE_UNSATISFIABLE))
               {
                 cerr << "Warning. Expected unsatisfiable, FOUND satisfiable" << endl;
               }