user-defined abstraction refinement basic functions in place. More thorough testing TBD

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

diff --git a/src/STPManager/STPManager.cpp b/src/STPManager/STPManager.cpp
index a64557d0b3be800d2d2ddcadc212b79f8c0df37c..78d5f3588c1bbc89baf231477892feb881f6a764 100644 (file)
--- a/src/STPManager/STPManager.cpp
+++ b/src/STPManager/STPManager.cpp
@@ -631,6 +631,25 @@ namespace BEEV
     //     return v;
   }
 
+  const ASTVec STPMgr::GetAsserts_WithKey(int key)
+  {
+    vector<IntToASTVecMap *>::iterator it = _asserts.begin();
+    vector<IntToASTVecMap *>::iterator itend = _asserts.end();
+
+    ASTVec v;
+    for(; it != itend; it++)
+      {
+       IntToASTVecMap * assert_map = (*it);
+       ASTVec * cc = (*assert_map)[key];
+       if(!cc->empty())
+         {
+           v.insert(v.end(), cc->begin(), cc->end());
+         }
+      }
+
+    return v;   
+  }
+
   // //Create a new variable of ValueWidth 'n'
   //   ASTNode STPMgr::NewArrayVar(unsigned int index, unsigned int value)
   //   {
@@ -794,5 +813,7 @@ namespace BEEV
     return CurrentSymbol;
   } // End of NewParameterized_BooleanVar()
 
+  
+
 }; // end namespace beev
 

diff --git a/src/STPManager/STPManager.h b/src/STPManager/STPManager.h
index dcec9f6cf8269706384a7878c840ce6d1fb7e90b..4e94ec0b9d12921dc2415633910682a29e635f21 100644 (file)
--- a/src/STPManager/STPManager.h
+++ b/src/STPManager/STPManager.h
@@ -316,6 +316,8 @@ namespace BEEV
     const ASTNode PopQuery();
     const ASTNode GetQuery();
     const ASTVec GetAsserts(void);
+    const ASTVec GetAsserts_WithKey(int key);
+
     //add a query/assertion to the current logical context
     void AddQuery(const ASTNode& q);
     void AddAssert(const ASTNode& assert, int userguided_absrefine=0);

diff --git a/src/absrefine_counterexample/AbsRefine_CounterExample.h b/src/absrefine_counterexample/AbsRefine_CounterExample.h
index 71760e86820b380def2c4a838481366b7ec9aea9..53ab8527f35d68dca5a2b46b7f45f935fa1e1d50 100644 (file)
--- a/src/absrefine_counterexample/AbsRefine_CounterExample.h
+++ b/src/absrefine_counterexample/AbsRefine_CounterExample.h
@@ -153,6 +153,11 @@ namespace BEEV
     SOLVER_RETURN_TYPE 
     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,

diff --git a/src/absrefine_counterexample/AbstractionRefinement.cpp b/src/absrefine_counterexample/AbstractionRefinement.cpp
index 4a8cf3293eaddd7158ae70a9417bb0c7ac297c4c..20e025c76ff14cb9a85504d757bce5de8ac8a5b9 100644 (file)
--- a/src/absrefine_counterexample/AbstractionRefinement.cpp
+++ b/src/absrefine_counterexample/AbstractionRefinement.cpp
@@ -243,7 +243,7 @@ namespace BEEV
     return SOLVER_UNDECIDED;
   } //end of SATBased_ArrayWriteRefinement
   
-  //bm->Creates Array Write Axioms
+  //Creates Array Write Axioms
   ASTNode 
   AbsRefine_CounterExample::Create_ArrayWriteAxioms(const ASTNode& term, 
                                                     const ASTNode& newvar)
@@ -261,6 +261,35 @@ namespace BEEV
   }//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
+    
+
+
+    return res;
+  } //End of UserGuided_AbsRefine()
+
   //   static void ReplaceOrAddToMap(ASTNodeMap * VarToConstMap, 
   //                            const ASTNode& key, const ASTNode& value)
   //   {