From 4bd7893ccc38109544ba510f882ca39236afee93 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Mon, 20 Jun 2011 14:15:13 +0000 Subject: [PATCH] Improvement. During abstraction refinement process arrays in order of the number of indexes. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1349 e59a4935-1847-0410-ae03-e826735625c1 --- .../AbstractionRefinement.cpp | 19 +++++++++++++++---- 1 file changed, 15 insertions(+), 4 deletions(-) diff --git a/src/absrefine_counterexample/AbstractionRefinement.cpp b/src/absrefine_counterexample/AbstractionRefinement.cpp index a7c6614..2a42159 100644 --- a/src/absrefine_counterexample/AbstractionRefinement.cpp +++ b/src/absrefine_counterexample/AbstractionRefinement.cpp @@ -193,6 +193,11 @@ Minisat::Var getEquals(SATSolver& SatSolver, const ASTNode& a, const ASTNode& b, toBe.clear(); } + bool sortBySize(const pair < ASTNode, ArrayTransformer::arrTypeMap >& a, const pair < ASTNode, ArrayTransformer::arrTypeMap >& b) + { + return a.second.size() < b.second.size(); + } + SOLVER_RETURN_TYPE AbsRefine_CounterExample:: SATBased_ArrayReadRefinement(SATSolver& SatSolver, @@ -207,19 +212,25 @@ Minisat::Var getEquals(SATSolver& SatSolver, const ASTNode& a, const ASTNode& b, // it produces isn't the number of times Array Read Refinement was entered. bm->GetRunTimes()->start(RunTimes::ArrayReadRefinement); - //in these loops we try to construct Leibnitz axioms and add it to + /// Check the arrays with the least indexes first. + vector < pair < ASTNode, ArrayTransformer::arrTypeMap > > arrayToIndex ; + arrayToIndex.insert(arrayToIndex.begin(),ArrayTransform->arrayToIndexToRead.begin(), ArrayTransform->arrayToIndexToRead.end() ); + sort(arrayToIndex.begin(), arrayToIndex.end(), sortBySize); + + //In these loops we try to construct Leibnitz axioms and add it to //the solve(). We add only those axioms that are false in the //current counterexample. we keep adding the axioms until there //are no more axioms to add // //for each array, fetch its list of indices seen so far - for (ArrayTransformer::ArrType::const_iterator - iset = ArrayTransform->arrayToIndexToRead.begin(), - iset_end = ArrayTransform->arrayToIndexToRead.end(); + for (vector < pair < ASTNode, ArrayTransformer::arrTypeMap > >::const_iterator + iset = arrayToIndex.begin(), + iset_end = arrayToIndex.end(); iset != iset_end; iset++) { const ASTNode& ArrName = iset->first; const map& mapper = iset->second; + cerr << "array Size" << mapper.size() << endl; vector listOfIndices; listOfIndices.reserve(mapper.size()); -- 2.47.3