userguided abstraction-refinement is now at the toplevel

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

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index 9f3c730e1088bc78adf5822c4bf9d8c1449f5712..a6a4265020b5d218bd9d8ad3ba7a3581ce91610a 100644 (file)
--- a/src/STPManager/STP.cpp
+++ b/src/STPManager/STP.cpp
@@ -11,13 +11,51 @@
 
 namespace BEEV {
 
+   // The absolute TopLevel function that invokes STP on the input
+    // formula
+  SOLVER_RETURN_TYPE STP::TopLevelSTP(const ASTNode& inputasserts, 
+                                     const ASTNode& query)
+  {      
+    ASTNode original_input = bm->CreateNode(AND, 
+                                           inputasserts, 
+                                           bm->CreateNode(NOT, query));
+    ASTNode modified_input = original_input;
+    
+    //solver instantiated here
+#ifdef CORE
+    MINISAT::Solver NewSolver;
+#endif
+#ifdef CRYPTOMINISAT
+    MINISAT::Solver NewSolver;
+#endif
+#ifdef SIMP
+    MINISAT::SimpSolver NewSolver;
+#endif
+#ifdef UNSOUND
+    MINISAT::UnsoundSimpSolver NewSolver;
+#endif
+    
+    if(bm->UserFlags.num_absrefine_flag)
+      {
+       return UserGuided_AbsRefine(NewSolver,
+                                   original_input);
+      }
+    else 
+      {
+       return TopLevelSTPAux(NewSolver, 
+                             modified_input, original_input);
+      }
+  } //End of TopLevelSTP()
+  
   //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 UNDECIDED
-  SOLVER_RETURN_TYPE STP::TopLevelSTPAux(const ASTNode& inputasserts_and_query)
+  SOLVER_RETURN_TYPE STP::TopLevelSTPAux(MINISAT::Solver& NewSolver,
+                                        const ASTNode& modified_input,
+                                        const ASTNode& original_input)
   {
-    ASTNode inputToSAT = inputasserts_and_query;
-    ASTNode orig_input = inputToSAT;
+    ASTNode inputToSAT = modified_input;
+    ASTNode orig_input = original_input;
     bm->ASTNodeStats("input asserts and query: ", inputToSAT);
 
     ASTNode simplified_solved_InputToSAT = inputToSAT;
@@ -127,37 +165,13 @@ namespace BEEV {
     bm->TermsAlreadySeenMap_Clear();
 
     SOLVER_RETURN_TYPE res;
-    
-    //solver instantiated here
-#ifdef CORE
-    MINISAT::Solver newS;
-#endif
-#ifdef CRYPTOMINISAT
-    MINISAT::Solver newS;
-#endif
-#ifdef SIMP
-    MINISAT::SimpSolver newS;
-#endif
-#ifdef UNSOUND
-    MINISAT::UnsoundSimpSolver newS;
-#endif
-
-    if(bm->UserFlags.num_absrefine_flag 
-       && !bm->UserFlags.arrayread_refinement_flag)
-      {
-       res =
-         Ctr_Example->UserGuided_AbsRefine(newS,
-                                           orig_input);
-       return res;
-      }
-
     if (bm->UserFlags.arrayread_refinement_flag)
       {
         bm->counterexample_checking_during_refinement = true;
       }
 
     res = 
-      Ctr_Example->CallSAT_ResultCheck(newS, 
+      Ctr_Example->CallSAT_ResultCheck(NewSolver, 
                                        simplified_solved_InputToSAT, 
                                        orig_input);
     if (SOLVER_UNDECIDED != res)
@@ -166,7 +180,7 @@ namespace BEEV {
         return res;
       }
 
-    // res = SATBased_AllFiniteLoops_Refinement(newS, orig_input);
+    // res = SATBased_AllFiniteLoops_Refinement(NewSolver, orig_input);
     //     if (SOLVER_UNDECIDED != res)
     //       {
     //  CountersAndStats("print_func_stats");
@@ -174,7 +188,7 @@ namespace BEEV {
     //       }
 
     res = 
-      Ctr_Example->SATBased_ArrayReadRefinement(newS,
+      Ctr_Example->SATBased_ArrayReadRefinement(NewSolver,
                                                 simplified_solved_InputToSAT, 
                                                 orig_input);
     if (SOLVER_UNDECIDED != res)
@@ -184,7 +198,7 @@ namespace BEEV {
       }
 
     res = 
-      Ctr_Example->SATBased_ArrayWriteRefinement(newS, orig_input);
+      Ctr_Example->SATBased_ArrayWriteRefinement(NewSolver, orig_input);
     if (SOLVER_UNDECIDED != res)
       {
         CountersAndStats("print_func_stats", bm);
@@ -192,7 +206,7 @@ namespace BEEV {
       }
 
     res = 
-      Ctr_Example->SATBased_ArrayReadRefinement(newS,
+      Ctr_Example->SATBased_ArrayReadRefinement(NewSolver,
                                                 simplified_solved_InputToSAT,
                                                 orig_input);
     if (SOLVER_UNDECIDED != res)
@@ -206,4 +220,73 @@ namespace BEEV {
     //bogus return to make the compiler shut up
     return SOLVER_ERROR;
   } //End of TopLevelSTPAux
+
+  //UserGuided abstraction refinement
+  SOLVER_RETURN_TYPE
+  STP::
+  UserGuided_AbsRefine(MINISAT::Solver& NewSolver,
+                      const ASTNode& original_input)
+  {
+    ASTVec v = bm->GetAsserts_WithKey(0);
+    if(v.empty())
+      {
+       FatalError("UserGuided_AbsRefine: Something is seriously wrong."\
+                  "The input set is empty");
+      }
+    ASTNode sureAddInput = 
+      (v.size() == 1) ? v[0] : bm->CreateNode(AND, v); 
+
+    SOLVER_RETURN_TYPE res = SOLVER_UNDECIDED;
+    res = TopLevelSTPAux(NewSolver, sureAddInput, original_input);
+    if(SOLVER_UNDECIDED != res)
+      {
+       return res;
+      }
+    
+    //Do refinement here
+    if(AND != original_input.GetKind())
+      {
+       FatalError("UserGuided_AbsRefine: The input must be an AND");
+      }
+
+    ASTVec RefineFormulasVec;
+    ASTVec RemainingFormulasVec;
+    ASTNode asttrue = bm->CreateNode(TRUE);
+    ASTNode astfalse = bm->CreateNode(FALSE);
+    for(int count=0; count < bm->UserFlags.num_absrefine; count++)
+      {
+       RemainingFormulasVec.clear();
+       RemainingFormulasVec.push_back(asttrue);
+       RefineFormulasVec.clear();      
+       RefineFormulasVec.push_back(asttrue);
+       ASTVec InputKids = original_input.GetChildren();
+       for(ASTVec::iterator it = InputKids.begin(), itend = InputKids.end();
+           it!=itend;it++)
+         {
+           Ctr_Example->ClearComputeFormulaMap();
+           if(astfalse == Ctr_Example->ComputeFormulaUsingModel(*it))
+             {
+               RefineFormulasVec.push_back(*it);
+             }
+           else
+             {
+               RemainingFormulasVec.push_back(*it);
+             }
+         }
+       ASTNode RefineFormulas =
+         (RefineFormulasVec.size() == 1) ?
+         RefineFormulasVec[0] : bm->CreateNode(AND, RefineFormulasVec);
+       res = TopLevelSTPAux(NewSolver, RefineFormulas, original_input);
+       if(SOLVER_UNDECIDED != res)
+         {
+           return res;
+         }
+      }
+
+    ASTNode RemainingFormulas = 
+      (RemainingFormulasVec.size() == 1) ?
+      RemainingFormulasVec[0] : bm->CreateNode(AND, RemainingFormulasVec);
+    res = TopLevelSTPAux(NewSolver, RemainingFormulas, original_input);
+    return res;
+  } //End of UserGuided_AbsRefine()
 }; //end of namespace

diff --git a/src/STPManager/STP.h b/src/STPManager/STP.h
index ee051b39037991dbcd957c0c4155ce98df400481..8e1f519c8c2803cf5fa0cca0fd17df90efb0cdb4 100644 (file)
--- a/src/STPManager/STP.h
+++ b/src/STPManager/STP.h
@@ -77,22 +77,20 @@ namespace BEEV
     // The absolute TopLevel function that invokes STP on the input
     // formula
     SOLVER_RETURN_TYPE TopLevelSTP(const ASTNode& inputasserts, 
-                                   const ASTNode& query)
-    {      
-      ASTNode q = bm->CreateNode(AND, 
-                                 inputasserts, 
-                                 bm->CreateNode(NOT, query));
-      return TopLevelSTPAux(q);
-    } //End of TopLevelSTP()    
+                                   const ASTNode& query);
 
     // Accepts query and returns the answer. if query is valid,
     // returns VALID, else returns INVALID. Automatically constructs
     // counterexample for invalid queries, and prints them upon
-    // request.    
-    SOLVER_RETURN_TYPE TopLevelSTPAux(const ASTNode& inputasserts_and_query);
+    // request.
+    SOLVER_RETURN_TYPE TopLevelSTPAux(MINISAT::Solver& NewSolver,
+                                     const ASTNode& modified_input,
+                                     const ASTNode& original_input);
 
-    //void ClearAllCaches(void);
-    
+    SOLVER_RETURN_TYPE
+    UserGuided_AbsRefine(MINISAT::Solver& SatSolver,
+                        const ASTNode& original_input);
+         
     void ClearAllTables(void)
     {
       simp->ClearAllTables();

diff --git a/src/absrefine_counterexample/AbsRefine_CounterExample.h b/src/absrefine_counterexample/AbsRefine_CounterExample.h
index 53ab8527f35d68dca5a2b46b7f45f935fa1e1d50..a858a2893a3f127042bd642bcf36cf25c0ddd94b 100644 (file)
--- a/src/absrefine_counterexample/AbsRefine_CounterExample.h
+++ b/src/absrefine_counterexample/AbsRefine_CounterExample.h
@@ -154,11 +154,6 @@ namespace BEEV
     SATBased_ArrayWriteRefinement(MINISAT::Solver& newS,
                                   const ASTNode& orig_input);        
     
-    SOLVER_RETURN_TYPE
-    UserGuided_AbsRefine(MINISAT::Solver& SatSolver,   
-                        const ASTNode& original_input);
-  
-   
     //     SOLVER_RETURN_TYPE
     // SATBased_AllFiniteLoops_Refinement(MINISAT::Solver& newS,
     // const ASTNode& orig_input);

diff --git a/src/absrefine_counterexample/AbstractionRefinement.cpp b/src/absrefine_counterexample/AbstractionRefinement.cpp
index bea6ec6cccf32951a7f6cf491cf8cf25f47a8d25..f922a9bcbd34b4883d4eb6dcd97927c9d501d6d6 100644 (file)
--- a/src/absrefine_counterexample/AbstractionRefinement.cpp
+++ b/src/absrefine_counterexample/AbstractionRefinement.cpp
@@ -259,74 +259,6 @@ namespace BEEV
     return arraywrite_axiom;
   }//end of Create_ArrayWriteAxioms()
 
-  //UserGuided abstraction refinement
-  SOLVER_RETURN_TYPE
-  AbsRefine_CounterExample::
-  UserGuided_AbsRefine(MINISAT::Solver& SatSolver,
-                      //const ASTNode& modified_input,
-                      const ASTNode& original_input)
-  {
-    ASTVec v = bm->GetAsserts_WithKey(0);
-    if(v.empty())
-      {
-       FatalError("UserGuided_AbsRefine: Something is seriously wrong."\
-                  "The input set is empty");
-      }
-    ASTNode sureAddInput = 
-      (v.size() == 1) ? v[0] : bm->CreateNode(AND, v); 
-
-    SOLVER_RETURN_TYPE res = SOLVER_UNDECIDED;
-    res = CallSAT_ResultCheck(SatSolver, sureAddInput, original_input);
-    if(SOLVER_UNDECIDED != res)
-      {
-       return res;
-      }
-    
-    //Do refinement here
-    if(AND != original_input.GetKind())
-      {
-       FatalError("UserGuided_AbsRefine: The input must be an AND");
-      }
-
-    ASTVec RefineFormulasVec;
-    ASTVec RemainingFormulasVec;
-    for(int count=0; count < bm->UserFlags.num_absrefine; count++)
-      {
-       RemainingFormulasVec.clear();
-       RemainingFormulasVec.push_back(ASTTrue);
-       RefineFormulasVec.clear();      
-       RefineFormulasVec.push_back(ASTTrue);
-       ASTVec InputKids = original_input.GetChildren();
-       for(ASTVec::iterator it = InputKids.begin(), itend = InputKids.end();
-           it!=itend;it++)
-         {
-           ClearComputeFormulaMap();
-           if(ASTFalse == ComputeFormulaUsingModel(*it))
-             {
-               RefineFormulasVec.push_back(*it);
-             }
-           else
-             {
-               RemainingFormulasVec.push_back(*it);
-             }
-         }
-       ASTNode RefineFormulas =
-         (RefineFormulasVec.size() == 1) ?
-         RefineFormulasVec[0] : bm->CreateNode(AND, RefineFormulasVec);
-       res = CallSAT_ResultCheck(SatSolver, RefineFormulas, original_input);
-       if(SOLVER_UNDECIDED != res)
-         {
-           return res;
-         }
-      }
-
-    ASTNode RemainingFormulas = 
-      (RemainingFormulasVec.size() == 1) ?
-      RemainingFormulasVec[0] : bm->CreateNode(AND, RemainingFormulasVec);
-    res = CallSAT_ResultCheck(SatSolver, RemainingFormulas, original_input);
-    return res;
-  } //End of UserGuided_AbsRefine()
-
   //   static void ReplaceOrAddToMap(ASTNodeMap * VarToConstMap, 
   //                            const ASTNode& key, const ASTNode& value)
   //   {