From: vijay_ganesh Date: Wed, 16 Sep 2009 00:50:50 +0000 (+0000) Subject: minor edits. Lot more work remains in optimizing FOR construct X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=d68d21e285710c8e30e1ced34f1ba7375e6c8637;p=francis%2Fstp.git minor edits. Lot more work remains in optimizing FOR construct git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@232 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/Makefile b/Makefile index d4fa64a..ad6a82a 100644 --- a/Makefile +++ b/Makefile @@ -68,12 +68,13 @@ clean: $(MAKE) clean -C $(SRC)/parser $(MAKE) clean -C $(SRC)/main -# this is make way too difficult because of the recursive Make junk, it -# should be removed -TAGS: FORCE - find . -name "*.[h]" -or -name "*.cpp" -or -name "*.C" | grep -v SCCS | etags - -FORCE: +.PHONY: regressall +regressall: + $(MAKE) regresscvc + $(MAKE) regresssmt + $(MAKE) regresscapi + $(MAKE) regressbigarray # The higher the level, the more tests are run (3 = all) REGRESS_LEVEL=4 diff --git a/scripts/Makefile.common b/scripts/Makefile.common index 66b2cb0..3277421 100644 --- a/scripts/Makefile.common +++ b/scripts/Makefile.common @@ -40,6 +40,7 @@ ifeq ($(shell uname -s), DarwinX) else LDFLAGS = $(LDFLAGS_BASE) CFLAGS = $(CFLAGS_BASE) -m32 + CFLAGS = $(CFLAGS_BASE) endif #CXXFLAGS = $(CFLAGS) -Wall -Wextra -DEXT_HASH_MAP -Wno-deprecated diff --git a/scripts/Makefile.in b/scripts/Makefile.in index d4fa64a..ad6a82a 100644 --- a/scripts/Makefile.in +++ b/scripts/Makefile.in @@ -68,12 +68,13 @@ clean: $(MAKE) clean -C $(SRC)/parser $(MAKE) clean -C $(SRC)/main -# this is make way too difficult because of the recursive Make junk, it -# should be removed -TAGS: FORCE - find . -name "*.[h]" -or -name "*.cpp" -or -name "*.C" | grep -v SCCS | etags - -FORCE: +.PHONY: regressall +regressall: + $(MAKE) regresscvc + $(MAKE) regresssmt + $(MAKE) regresscapi + $(MAKE) regressbigarray # The higher the level, the more tests are run (3 = all) REGRESS_LEVEL=4 diff --git a/src/AST/Makefile b/src/AST/Makefile index 5416feb..2201042 100644 --- a/src/AST/Makefile +++ b/src/AST/Makefile @@ -23,5 +23,5 @@ clean: depend: $(SRCS) @$(CXX) -MM -MG $(CXXFLAGS) $(SRCS) > $@ --include ./depend +#-include ./depend diff --git a/src/abstraction-refinement/AbstractionRefinement.cpp b/src/abstraction-refinement/AbstractionRefinement.cpp index 13f3c19..b8bdea9 100644 --- a/src/abstraction-refinement/AbstractionRefinement.cpp +++ b/src/abstraction-refinement/AbstractionRefinement.cpp @@ -227,6 +227,21 @@ namespace BEEV return arraywrite_axiom; }//end of Create_ArrayWriteAxioms() + + static void ReplaceOrAddToMap(ASTNodeMap * VarToConstMap, + const ASTNode& key, const ASTNode& value) + { + ASTNodeMap::iterator it = VarToConstMap->find(key); + if(it != VarToConstMap->end()) + { + VarToConstMap->erase(it); + } + + (*VarToConstMap)[key] = value; + return; + } + + /****************************************************************** * FINITE FORLOOP ABSTRACTION REFINEMENT * @@ -250,7 +265,7 @@ namespace BEEV BeevMgr::SATBased_AllFiniteLoops_Refinement(MINISAT::Solver& SatSolver, const ASTNode& original_input) { - //cout << "The number of abs-refinement limit is " << num_absrefine << endl; + cout << "The number of abs-refinement limit is " << num_absrefine << endl; for(int absrefine_count=0;absrefine_count < num_absrefine; absrefine_count++) { ASTVec Allretvec0; @@ -287,7 +302,7 @@ namespace BEEV return res; } } //end of absrefine count - + ASTVec Allretvec1; Allretvec1.push_back(ASTTrue); SOLVER_RETURN_TYPE res = SOLVER_UNDECIDED; @@ -355,11 +370,13 @@ namespace BEEV ASTNode exceptFormula = finiteloop[4]; ASTNode formulabody = finiteloop[5]; int paramCurrentValue = paramInit; + int width = finiteloop[1].GetValueWidth(); //Update ParamToCurrentValMap with parameter and its current //value. Here paramCurrentValue is the initial value - (*ParamToCurrentValMap)[parameter] = - CreateBVConst(finiteloop[1].GetValueWidth(),paramCurrentValue); + ASTNode value = + CreateBVConst(width,paramCurrentValue); + ReplaceOrAddToMap(ParamToCurrentValMap, parameter, value); //Go recursively thru' all the FOR-constructs. if(FOR == formulabody.GetKind()) @@ -383,11 +400,13 @@ namespace BEEV } //Update ParamToCurrentValMap with parameter and its - //current value. FIXME: Possible leak since I am not - //freeing the previous 'value' for the same 'key' - paramCurrentValue = paramCurrentValue + paramIncrement; - (*ParamToCurrentValMap)[parameter] = - CreateBVConst(finiteloop[1].GetValueWidth(),paramCurrentValue); + //current value. + paramCurrentValue = paramCurrentValue + paramIncrement; + value = CreateTerm(BVPLUS, + width, + (*ParamToCurrentValMap)[parameter], + CreateOneConst(width)); + ReplaceOrAddToMap(ParamToCurrentValMap, parameter, value); } //end of While return retvec; @@ -416,8 +435,10 @@ namespace BEEV //Check the currentformula against the model, and add it to the //SAT solver if it is false against the model - if(absrefine_flag && - ASTFalse == ComputeFormulaUsingModel(currentFormula)) + if(absrefine_flag + && + ASTFalse == ComputeFormulaUsingModel(currentFormula) + ) { ForloopVec.push_back(currentFormula); } @@ -435,11 +456,13 @@ namespace BEEV } //Update ParamToCurrentValMap with parameter and its current - //value. FIXME: Possible leak since I am not freeing the - //previous 'value' for the same 'key' + //value. paramCurrentValue = paramCurrentValue + paramIncrement; - (*ParamToCurrentValMap)[parameter] = - CreateBVConst(finiteloop[1].GetValueWidth(),paramCurrentValue); + value = CreateTerm(BVPLUS, + width, + (*ParamToCurrentValMap)[parameter], + CreateOneConst(width)); + ReplaceOrAddToMap(ParamToCurrentValMap, parameter, value); } //end of expanding the FOR loop return ForloopVec; @@ -477,12 +500,14 @@ namespace BEEV ASTNode exceptFormula = finiteloop[4]; ASTNode formulabody = finiteloop[5]; int paramCurrentValue = paramInit; + int width = finiteloop[1].GetValueWidth(); //Update ParamToCurrentValMap with parameter and its current //value. Here paramCurrentValue is the initial value - (*ParamToCurrentValMap)[parameter] = - CreateBVConst(finiteloop[1].GetValueWidth(),paramCurrentValue); - + ASTNode value = + CreateBVConst(width,paramCurrentValue); + ReplaceOrAddToMap(ParamToCurrentValMap, parameter, value); + ASTNode ret = ASTTrue; ASTVec returnVec; //Go recursively thru' all the FOR-constructs. @@ -504,16 +529,21 @@ namespace BEEV } //Update ParamToCurrentValMap with parameter and its - //current value. FIXME: Possible leak since I am not - //freeing the previous 'value' for the same 'key' + //current value. paramCurrentValue = paramCurrentValue + paramIncrement; - (*ParamToCurrentValMap)[parameter] = - CreateBVConst(finiteloop[1].GetValueWidth(),paramCurrentValue); + value = CreateTerm(BVPLUS, + width, + (*ParamToCurrentValMap)[parameter], + CreateOneConst(width)); + ReplaceOrAddToMap(ParamToCurrentValMap, parameter, value); } //end of While ASTNode retFormula = - (returnVec.size() != 1) ? - CreateNode(AND, returnVec) : returnVec[0]; + (returnVec.size() > 1) ? + CreateNode(AND, returnVec) : + (returnVec.size() == 1) ? + returnVec[0] : + ASTTrue; return retFormula; } @@ -560,12 +590,12 @@ namespace BEEV //Update ParamToCurrentValMap with parameter and its current //value - //FIXME: Possible leak since I am not freeing the previous - //'value' for the same 'key' paramCurrentValue = paramCurrentValue + paramIncrement; - (*ParamToCurrentValMap)[parameter] = - CreateBVConst(finiteloop[1].GetValueWidth(),paramCurrentValue); - //cout << (*ParamToCurrentValMap)[parameter]; + value = CreateTerm(BVPLUS, + width, + (*ParamToCurrentValMap)[parameter], + CreateOneConst(width)); + ReplaceOrAddToMap(ParamToCurrentValMap, parameter, value); } //end of For if(checkusingmodel_flag) @@ -575,9 +605,11 @@ namespace BEEV else { ASTNode retFormula = - (forloopFormulaVector.size() != 1) ? - CreateNode(AND, forloopFormulaVector) : - forloopFormulaVector[0]; + (forloopFormulaVector.size() > 1) ? + CreateNode(AND, forloopFormulaVector) : + (forloopFormulaVector.size() == 1) ? + forloopFormulaVector[0] : + ASTTrue; return retFormula; } } //end of the Check_FiniteLoop_UsingModel() @@ -601,7 +633,6 @@ namespace BEEV } //end of Check_FiniteLoop_UsingModel - // /****************************************************************** // * FINITE FORLOOP ABSTRACTION REFINEMENT // * diff --git a/src/sat/core/Makefile b/src/sat/core/Makefile index 78906ac..15b5666 100644 --- a/src/sat/core/Makefile +++ b/src/sat/core/Makefile @@ -2,6 +2,7 @@ MTL = ../mtl CHDRS = $(wildcard *.h) $(wildcard $(MTL)/*.h) EXEC = minisat CFLAGS = -I$(MTL) -Wall -DEXT_HASH_MAP -ffloat-store -m32 +CFLAGS = -I$(MTL) -Wall -DEXT_HASH_MAP -ffloat-store LFLAGS = -lz diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp index 2e4770e..e02340b 100644 --- a/src/to-sat/ToSAT.cpp +++ b/src/to-sat/ToSAT.cpp @@ -854,7 +854,7 @@ namespace BEEV output = ComputeFormulaUsingModel(output); break; case FOR: - output = Check_FiniteLoop_UsingModel(form); + output = Check_FiniteLoop_UsingModel(form); break; default: FatalError(" ComputeFormulaUsingModel: "\ @@ -1018,31 +1018,6 @@ namespace BEEV } TermsAlreadySeenMap.clear(); - // do -// { -// inputToSAT = simplified_solved_InputToSAT; - -// if(optimize_flag) -// { -// //simplified_solved_InputToSAT = -// //CreateSubstitutionMap(simplified_solved_InputToSAT); -// //Begin_RemoveWrites = true; ASTNodeStats("after pure -// //substitution: ", simplified_solved_InputToSAT); -// simplified_solved_InputToSAT = -// SimplifyFormula_TopLevel(simplified_solved_InputToSAT, false); -// //ASTNodeStats("after simplification: ", -// //simplified_solved_InputToSAT); -// // -// } - -// if(wordlevel_solve_flag) -// { -// simplified_solved_InputToSAT -// = bvsolver.TopLevelBVSolve(simplified_solved_InputToSAT); -// ASTNodeStats("after solving: ", -// simplified_solved_InputToSAT); -// } -// } while (inputToSAT != simplified_solved_InputToSAT); if (start_abstracting) { @@ -1068,7 +1043,6 @@ namespace BEEV } res = CallSAT_ResultCheck(newS, simplified_solved_InputToSAT, orig_input); - if (SOLVER_UNDECIDED != res) { CountersAndStats("print_func_stats"); diff --git a/tests/for-tests/for-boolean2.cvc b/tests/for-tests/for-boolean2.cvc new file mode 100644 index 0000000..cca2f54 --- /dev/null +++ b/tests/for-tests/for-boolean2.cvc @@ -0,0 +1,11 @@ +A,B : BOOLEAN; + +ASSERT A(0x00) <=> TRUE ; +ASSERT B(0x00) <=> FALSE; +ASSERT ( +FOR(j:BITVECTOR(8);0x00;0xFF;0x01){ + A(j) <=> B(j) +} +); + +QUERY FALSE; \ No newline at end of file