From: vijay_ganesh <vijay_ganesh@e59a4935-1847-0410-ae03-e826735625c1>
Date: Tue, 17 Nov 2009 02:52:22 +0000 (+0000)
Subject: user-defined abstraction refinement basic functions in place. More thorough testing TBD
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=51ff427fafff123c5198d47c88a4c8e544d6f7f2;p=francis%2Fstp.git

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 a64557d..78d5f35 100644
--- 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 dcec9f6..4e94ec0 100644
--- 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 71760e8..53ab852 100644
--- 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 4a8cf32..20e025c 100644
--- 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)
   //   {