From 1c59521f5cbc9db18189dfbf4aa287bd923f567a Mon Sep 17 00:00:00 2001 From: vijay_ganesh Date: Tue, 17 Nov 2009 19:28:14 +0000 Subject: [PATCH] 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 --- src/STPManager/STP.cpp | 9 ++++ src/STPManager/STPManager.h | 1 + .../AbstractionRefinement.cpp | 45 +++++++++++++++++-- src/c_interface/c_interface.cpp | 8 ++-- src/c_interface/c_interface.h | 4 +- 5 files changed, 57 insertions(+), 10 deletions(-) diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp index ee69d10..9f3c730 100644 --- 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 4e94ec0..4f9b412 100644 --- 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 20e025c..bea6ec6 100644 --- 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 46c657f..4a928fd 100644 --- 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 253e1c4..cd57735 100644 --- 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); -- 2.47.3