added an experimental user-guided abstraction-refinement loop

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

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index ee69d1089a8f07ac42db8d565a13a27360807cf0..9f3c730e1088bc78adf5822c4bf9d8c1449f5712 100644 (file)
--- a/src/STPManager/STP.cpp
+++ b/src/STPManager/STP.cpp
@@ -142,6 +142,15 @@ namespace BEEV {
     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;

diff --git a/src/STPManager/STPManager.h b/src/STPManager/STPManager.h
index 4e94ec0b9d12921dc2415633910682a29e635f21..4f9b412853e5c4e1c49f462e6064c8df8178ec1a 100644 (file)
--- a/src/STPManager/STPManager.h
+++ b/src/STPManager/STPManager.h
@@ -181,6 +181,7 @@ namespace BEEV
       letmgr       = new LETMgr(ASTUndefined);
       runTimes     = new RunTimes();
       _current_query = ASTUndefined;
+      UserFlags.num_absrefine = 2;
     }    
 
     //Return ptr to let-variables manager (see parser/let-funcs.h)

diff --git a/src/absrefine_counterexample/AbstractionRefinement.cpp b/src/absrefine_counterexample/AbstractionRefinement.cpp
index 20e025c76ff14cb9a85504d757bce5de8ac8a5b9..bea6ec6cccf32951a7f6cf491cf8cf25f47a8d25 100644 (file)
--- a/src/absrefine_counterexample/AbstractionRefinement.cpp
+++ b/src/absrefine_counterexample/AbstractionRefinement.cpp
@@ -15,7 +15,6 @@
 
 namespace BEEV
 {
-
   /******************************************************************
    * Abstraction Refinement related functions
    ******************************************************************/  
@@ -260,7 +259,6 @@ namespace BEEV
     return arraywrite_axiom;
   }//end of Create_ArrayWriteAxioms()
 
-
   //UserGuided abstraction refinement
   SOLVER_RETURN_TYPE
   AbsRefine_CounterExample::
@@ -274,7 +272,8 @@ namespace BEEV
        FatalError("UserGuided_AbsRefine: Something is seriously wrong."\
                   "The input set is empty");
       }
-    ASTNode sureAddInput = (v.size() == 1) ? v[0] : bm->CreateNode(AND, v); 
+    ASTNode sureAddInput = 
+      (v.size() == 1) ? v[0] : bm->CreateNode(AND, v); 
 
     SOLVER_RETURN_TYPE res = SOLVER_UNDECIDED;
     res = CallSAT_ResultCheck(SatSolver, sureAddInput, original_input);
@@ -284,9 +283,47 @@ namespace BEEV
       }
     
     //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()
 

diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp
index 46c657f67650091481b9f5ba29175a93e773d39a..4a928fdd259435a7dfc64c31ffbbafbc579f6a05 100644 (file)
--- a/src/c_interface/c_interface.cpp
+++ b/src/c_interface/c_interface.cpp
@@ -36,7 +36,7 @@ bool cinterface_exprdelete_on_flag = false;
 extern int cvcparse(void*);
 extern int smtparse(void*);
 
-void vc_setFlags(VC vc, char c) {
+void vc_setFlags(VC vc, char c, int num_absrefine) {
   bmstar b = (bmstar)(((stpstar)vc)->bm);
   
   std::string helpstring = 
@@ -88,7 +88,7 @@ void vc_setFlags(VC vc, char c) {
     break;
   case 'f':
     b->UserFlags.num_absrefine_flag = true;
-    //b->UserFlags.num_absrefine = atoi(argv[++i]);
+    b->UserFlags.num_absrefine = num_absrefine;
     break;
   case 'h':
     fprintf(stderr,BEEV::usage,BEEV::prog);
@@ -464,7 +464,7 @@ Expr vc_writeExpr(VC vc, Expr array, Expr index, Expr newValue) {
 /////////////////////////////////////////////////////////////////////////////
 //! Assert a new formula in the current context.
 /*! The formula must have Boolean type. */
-void vc_assertFormula(VC vc, Expr e, int absrefine_num) {
+void vc_assertFormula(VC vc, Expr e, int absrefine_bucket_num) {
   nodestar a = (nodestar)e;
   bmstar b = (bmstar)(((stpstar)vc)->bm);
 
@@ -472,7 +472,7 @@ void vc_assertFormula(VC vc, Expr e, int absrefine_num) {
     BEEV::FatalError("Trying to assert a NON formula: ",*a);
 
   BVTypeCheck(*a);
-  b->AddAssert(*a);
+  b->AddAssert(*a, absrefine_bucket_num);
 }
 
 

diff --git a/src/c_interface/c_interface.h b/src/c_interface/c_interface.h
index 253e1c49bc02525df87e4b293193c408a491c2b5..cd57735452478e08578a7bcb9a62f06c20e8b6d6 100644 (file)
--- a/src/c_interface/c_interface.h
+++ b/src/c_interface/c_interface.h
@@ -42,7 +42,7 @@ extern "C" {
   // h  : help
   // s  : stats
   // v  : print nodes
-  void vc_setFlags(VC vc, char c);
+  void vc_setFlags(VC vc, char c, int num_absrefine=0);
 
   //! Flags can be NULL
   VC vc_createValidityChecker(void);
@@ -170,7 +170,7 @@ extern "C" {
 
   //! Assert a new formula in the current context.
   /*! The formula must have Boolean type. */
-  void vc_assertFormula(VC vc, Expr e, int absrefine_num=0);
+  void vc_assertFormula(VC vc, Expr e, int absrefine_bucket_num=0);
 
   //! Simplify e with respect to the current context
   Expr vc_simplify(VC vc, Expr e);