From: trevor_hansen Date: Tue, 21 Jun 2011 14:06:48 +0000 (+0000) Subject: Automatically format this code. No semantic change. X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=a596ba058f58d273f5b4a39cbe50357c5cf40fc4;p=francis%2Fstp.git Automatically format this code. No semantic change. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1351 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/absrefine_counterexample/AbstractionRefinement.cpp b/src/absrefine_counterexample/AbstractionRefinement.cpp index d5b2559..f2ec4da 100644 --- a/src/absrefine_counterexample/AbstractionRefinement.cpp +++ b/src/absrefine_counterexample/AbstractionRefinement.cpp @@ -19,133 +19,140 @@ namespace BEEV * Abstraction Refinement related functions ******************************************************************/ -enum Polarity {LEFT_ONLY, RIGHT_ONLY, BOTH}; - -void getSatVariables(const ASTNode & a, vector & v_a, SATSolver & SatSolver, ToSATBase::ASTNodeToSATVar & satVar) - { - ToSATBase::ASTNodeToSATVar::iterator it = satVar.find(a); - if (it != satVar.end()) - v_a = it->second; - else - if (!a.isConstant()) - { - assert(a.GetKind() == SYMBOL); - // It was ommitted from the initial problem, so assign it freshly. - for(int i = 0;i < a.GetValueWidth();i++) - v_a.push_back(SatSolver.newVar()); - satVar.insert(make_pair(a,v_a)); - } - } + enum Polarity + { + LEFT_ONLY, RIGHT_ONLY, BOTH + }; + + void + getSatVariables(const ASTNode & a, vector & v_a, SATSolver & SatSolver, + ToSATBase::ASTNodeToSATVar & satVar) + { + ToSATBase::ASTNodeToSATVar::iterator it = satVar.find(a); + if (it != satVar.end()) + v_a = it->second; + else if (!a.isConstant()) + { + assert(a.GetKind() == SYMBOL); + // It was ommitted from the initial problem, so assign it freshly. + for (int i = 0; i < a.GetValueWidth(); i++) + v_a.push_back(SatSolver.newVar()); + satVar.insert(make_pair(a, v_a)); + } + } // This function adds the clauses to constrain (a=b)->c. -// Because it's used to create array axionms (a=b)-> (c=d), it can be -// used to only add one of the polarities.. -Minisat::Var getEquals(SATSolver& SatSolver, const ASTNode& a, const ASTNode& b, ToSATBase::ASTNodeToSATVar& satVar, Polarity polary= BOTH) -{ - const int width = a.GetValueWidth(); - assert(width == b.GetValueWidth()); - assert(!a.isConstant() || !b.isConstant()); - - vector v_a; - vector v_b; - - getSatVariables(a,v_a,SatSolver,satVar); - getSatVariables(b,v_b,SatSolver,satVar); - - // The only time v_a or v_b will be empty is if a resp. b is a constant. - - if (v_a.size() == width && v_b.size() == width) - { - SATSolver::vec_literals all; - const int result = SatSolver.newVar(); - - for (int i=0; i < width; i++) - { - SATSolver::vec_literals s; - int nv0 = SatSolver.newVar(); - - if (polary != RIGHT_ONLY) - { - s.push(SATSolver::mkLit(v_a[i], true)); - s.push(SATSolver::mkLit(v_b[i], true)); - s.push(SATSolver::mkLit(nv0, false)); - SatSolver.addClause(s); - s.clear(); - - s.push(SATSolver::mkLit(v_a[i], false)); - s.push(SATSolver::mkLit(v_b[i], false)); - s.push(SATSolver::mkLit(nv0, false)); - SatSolver.addClause(s); - s.clear(); - } - - if (polary != LEFT_ONLY) - { - s.push(SATSolver::mkLit(v_a[i], true)); - s.push(SATSolver::mkLit(v_b[i], false)); - s.push(SATSolver::mkLit(nv0, true)); - SatSolver.addClause(s); - s.clear(); - - s.push(SATSolver::mkLit(v_a[i], false)); - s.push(SATSolver::mkLit(v_b[i], true)); - s.push(SATSolver::mkLit(nv0, true)); - SatSolver.addClause(s); - s.clear(); - - // result -> nv0 .. new. - s.push(SATSolver::mkLit(result, true)); - s.push(SATSolver::mkLit(nv0, false)); - SatSolver.addClause(s); - s.clear(); - } - - all.push(SATSolver::mkLit(nv0, true)); - } - all.push(SATSolver::mkLit(result, false)); - - SatSolver.addClause(all); - return result; - } - else if (v_a.size() == 0 ^ v_b.size() ==0) - { - ASTNode constant = a.isConstant()? a:b; - vector vec = v_a.size() == 0? v_b : v_a; - assert(constant.isConstant()); - assert(vec.size() == width); - - SATSolver::vec_literals all; - const int result = SatSolver.newVar(); - all.push(SATSolver::mkLit(result, false)); - - CBV v = constant.GetBVConst(); - for (int i=0; i < width; i++) - { - if (CONSTANTBV::BitVector_bit_test(v,i)) - all.push(SATSolver::mkLit(vec[i], true)); - else - all.push(SATSolver::mkLit(vec[i], false)); - - if (polary != LEFT_ONLY) - { - SATSolver::vec_literals p; - p.push(SATSolver::mkLit(result, true)); - if (CONSTANTBV::BitVector_bit_test(v,i)) - p.push(SATSolver::mkLit(vec[i], false)); - else - p.push(SATSolver::mkLit(vec[i], true)); - - SatSolver.addClause(p); - } - - } - SatSolver.addClause(all); - return result; - }else - FatalError("Unexpected, both must be constants.."); - -} + // Because it's used to create array axionms (a=b)-> (c=d), it can be + // used to only add one of the polarities.. + Minisat::Var + getEquals(SATSolver& SatSolver, const ASTNode& a, const ASTNode& b, ToSATBase::ASTNodeToSATVar& satVar, + Polarity polary = BOTH) + { + const int width = a.GetValueWidth(); + assert(width == b.GetValueWidth()); + assert(!a.isConstant() || !b.isConstant()); + + vector v_a; + vector v_b; + + getSatVariables(a, v_a, SatSolver, satVar); + getSatVariables(b, v_b, SatSolver, satVar); + + // The only time v_a or v_b will be empty is if a resp. b is a constant. + + if (v_a.size() == width && v_b.size() == width) + { + SATSolver::vec_literals all; + const int result = SatSolver.newVar(); + + for (int i = 0; i < width; i++) + { + SATSolver::vec_literals s; + int nv0 = SatSolver.newVar(); + + if (polary != RIGHT_ONLY) + { + s.push(SATSolver::mkLit(v_a[i], true)); + s.push(SATSolver::mkLit(v_b[i], true)); + s.push(SATSolver::mkLit(nv0, false)); + SatSolver.addClause(s); + s.clear(); + + s.push(SATSolver::mkLit(v_a[i], false)); + s.push(SATSolver::mkLit(v_b[i], false)); + s.push(SATSolver::mkLit(nv0, false)); + SatSolver.addClause(s); + s.clear(); + } + + if (polary != LEFT_ONLY) + { + s.push(SATSolver::mkLit(v_a[i], true)); + s.push(SATSolver::mkLit(v_b[i], false)); + s.push(SATSolver::mkLit(nv0, true)); + SatSolver.addClause(s); + s.clear(); + + s.push(SATSolver::mkLit(v_a[i], false)); + s.push(SATSolver::mkLit(v_b[i], true)); + s.push(SATSolver::mkLit(nv0, true)); + SatSolver.addClause(s); + s.clear(); + + // result -> nv0 .. new. + s.push(SATSolver::mkLit(result, true)); + s.push(SATSolver::mkLit(nv0, false)); + SatSolver.addClause(s); + s.clear(); + } + + all.push(SATSolver::mkLit(nv0, true)); + } + all.push(SATSolver::mkLit(result, false)); + + SatSolver.addClause(all); + return result; + } + else if (v_a.size() == 0 ^ v_b.size() == 0) + { + ASTNode constant = a.isConstant() ? a : b; + vector vec = v_a.size() == 0 ? v_b : v_a; + assert(constant.isConstant()); + assert(vec.size() == width); + + SATSolver::vec_literals all; + const int result = SatSolver.newVar(); + all.push(SATSolver::mkLit(result, false)); + + CBV v = constant.GetBVConst(); + for (int i = 0; i < width; i++) + { + if (CONSTANTBV::BitVector_bit_test(v, i)) + all.push(SATSolver::mkLit(vec[i], true)); + else + all.push(SATSolver::mkLit(vec[i], false)); + + if (polary != LEFT_ONLY) + { + SATSolver::vec_literals p; + p.push(SATSolver::mkLit(result, true)); + if (CONSTANTBV::BitVector_bit_test(v, i)) + p.push(SATSolver::mkLit(vec[i], false)); + else + p.push(SATSolver::mkLit(vec[i], true)); + + SatSolver.addClause(p); + } + + } + SatSolver.addClause(all); + return result; + } + else + FatalError("Unexpected, both must be constants.."); + + } /****************************************************************** @@ -168,226 +175,232 @@ Minisat::Var getEquals(SATSolver& SatSolver, const ASTNode& a, const ASTNode& b, * time or all the false axioms each time). *****************************************************************/ struct AxiomToBe - { - AxiomToBe(ASTNode i0, ASTNode i1, ASTNode v0, ASTNode v1) - { - index0 = i0; - index1 = i1; - value0 = v0; - value1 = v1; - } - ASTNode index0, index1; - ASTNode value0, value1; - - int numberOfConstants() const - { - return ((index0.isConstant()? 1:0) + - (index1.isConstant()? 1:0) + - (index0.isConstant()? 1:0) + - (index1.isConstant()? 1:0) ); - } - - }; - - void applyAxiomToSAT(SATSolver & SatSolver, AxiomToBe& toBe, ToSATBase::ASTNodeToSATVar & satVar) - { + { + AxiomToBe(ASTNode i0, ASTNode i1, ASTNode v0, ASTNode v1) + { + index0 = i0; + index1 = i1; + value0 = v0; + value1 = v1; + } + ASTNode index0, index1; + ASTNode value0, value1; + + int + numberOfConstants() const + { + return ((index0.isConstant() ? 1 : 0) + (index1.isConstant() ? 1 : 0) + (index0.isConstant() ? 1 : 0) + + (index1.isConstant() ? 1 : 0)); + } + + }; + + void + applyAxiomToSAT(SATSolver & SatSolver, AxiomToBe& toBe, ToSATBase::ASTNodeToSATVar & satVar) + { Minisat::Var a = getEquals(SatSolver, toBe.index0, toBe.index1, satVar, LEFT_ONLY); Minisat::Var b = getEquals(SatSolver, toBe.value0, toBe.value1, satVar, RIGHT_ONLY); - SATSolver::vec_literals satSolverClause; - satSolverClause.push(SATSolver::mkLit(a, true)); - satSolverClause.push(SATSolver::mkLit(b, false)); - SatSolver.addClause(satSolverClause); - } + SATSolver::vec_literals satSolverClause; + satSolverClause.push(SATSolver::mkLit(a, true)); + satSolverClause.push(SATSolver::mkLit(b, false)); + SatSolver.addClause(satSolverClause); + } - void applyAxiomsToSolver(ToSATBase::ASTNodeToSATVar & satVar, vector & toBe, SATSolver & SatSolver) + void + applyAxiomsToSolver(ToSATBase::ASTNodeToSATVar & satVar, vector & toBe, SATSolver & SatSolver) { - for(int i = 0;i < toBe.size();i++){ - applyAxiomToSAT(SatSolver, toBe[i], satVar); - } + for (int i = 0; i < toBe.size(); i++) + { + applyAxiomToSAT(SatSolver, toBe[i], satVar); + } toBe.clear(); - } + } - bool sortBySize(const pair < ASTNode, ArrayTransformer::arrTypeMap >& a, const pair < ASTNode, ArrayTransformer::arrTypeMap >& b) - { - return a.second.size() < b.second.size(); - } + bool + sortBySize(const pair& a, + const pair& b) + { + return a.second.size() < b.second.size(); + } - bool sortByIndexConstants(const pair & a, const pair & b) + bool + sortByIndexConstants(const pair & a, + const pair & b) { int aCount = ((a.second.index_symbol.isConstant()) ? 2 : 0) + (a.second.symbol.isConstant() ? 1 : 0); int bCount = ((b.second.index_symbol.isConstant()) ? 2 : 0) + (b.second.symbol.isConstant() ? 1 : 0); return aCount > bCount; } - bool sortbyConstants(const AxiomToBe & a, const AxiomToBe & b) + bool + sortbyConstants(const AxiomToBe & a, const AxiomToBe & b) { return a.numberOfConstants() > b.numberOfConstants(); } - SOLVER_RETURN_TYPE AbsRefine_CounterExample::SATBased_ArrayReadRefinement(SATSolver & SatSolver, const ASTNode & inputAlreadyInSAT, const ASTNode & original_input, ToSATBase *tosat) + SOLVER_RETURN_TYPE + AbsRefine_CounterExample::SATBased_ArrayReadRefinement(SATSolver & SatSolver, const ASTNode & inputAlreadyInSAT, + const ASTNode & original_input, ToSATBase *tosat) { - vector RemainingAxiomsVec; - vector FalseAxiomsVec; - // NB. Because we stop this timer before entering the SAT solver, the count - // it produces isn't the number of times Array Read Refinement was entered. - bm->GetRunTimes()->start(RunTimes::ArrayReadRefinement); - /// 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 (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; - - vector listOfIndices; - listOfIndices.reserve(mapper.size()); - - // Make a vector of the read symbols. - ASTVec read_node_symbols; - read_node_symbols.reserve(listOfIndices.size()); - - vector jKind; - jKind.reserve(mapper.size()); - - vector concreteIndexes; - concreteIndexes.reserve(mapper.size()); - - vector concreteValues; - concreteValues.reserve(mapper.size()); - - ASTVec index_symbols; - - vector < pair < ASTNode, ArrayTransformer::ArrayRead > > indexToRead ; - indexToRead.insert(indexToRead.begin(),mapper.begin(), mapper.end() ); - sort(indexToRead.begin(), indexToRead.end(), sortByIndexConstants); - - for (vector < pair < ASTNode, ArrayTransformer::ArrayRead > >::const_iterator it =indexToRead.begin() ; it != indexToRead.end();it++) - { - const ASTNode& the_index = it->first; - listOfIndices.push_back(the_index); - - ASTNode arrsym = it->second.symbol; - read_node_symbols.push_back(arrsym); - - index_symbols.push_back(it->second.index_symbol); - - assert(read_node_symbols[0].GetValueWidth() == arrsym.GetValueWidth()); - assert(listOfIndices[0].GetValueWidth() == the_index.GetValueWidth()); - - jKind.push_back(the_index.GetKind()); - - concreteIndexes.push_back(TermToConstTermUsingModel(the_index)); - concreteValues.push_back(TermToConstTermUsingModel(arrsym)); - } - - assert(listOfIndices.size() == mapper.size()); - - //loop over the list of indices for the array and create LA, - //and add to inputAlreadyInSAT - for (int i = 0; i < listOfIndices.size(); i++) - { - const ASTNode& index_i = listOfIndices[i]; - const Kind iKind = index_i.GetKind(); - - // Create all distinct pairs of indexes. - for (int j = i+1; j < listOfIndices.size(); j++) - { - const ASTNode& index_j = listOfIndices[j]; - - // If the index is a constant, and different, then there's no reason to check. - // Sometimes we get the same index stored multiple times in the array. Not sure why... - if (BVCONST == iKind && jKind[j] == BVCONST && index_i != index_j) - continue; - - if (ASTFalse == simp->CreateSimplifiedEQ(index_i, index_j)) - continue; // shortcut. - - AxiomToBe o (index_symbols[i],index_symbols[j], read_node_symbols[i], read_node_symbols[j]); - - if (concreteIndexes[i] == concreteIndexes[j] && concreteValues[i] != concreteValues[j]) - { - FalseAxiomsVec.push_back(o); - //ToSATBase::ASTNodeToSATVar & satVar = tosat->SATVar_to_SymbolIndexMap(); - //applyAxiomsToSolver(satVar, FalseAxiomsVec, SatSolver); - } - else - RemainingAxiomsVec.push_back(o); - } - if ( FalseAxiomsVec.size() > 0) + vector RemainingAxiomsVec; + vector FalseAxiomsVec; + // NB. Because we stop this timer before entering the SAT solver, the count + // it produces isn't the number of times Array Read Refinement was entered. + bm->GetRunTimes()->start(RunTimes::ArrayReadRefinement); + /// Check the arrays with the least indexes first. + + + vector > 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 (vector >::const_iterator iset = arrayToIndex.begin(), + iset_end = arrayToIndex.end(); iset != iset_end; iset++) { - ToSATBase::ASTNodeToSATVar & satVar = tosat->SATVar_to_SymbolIndexMap(); - applyAxiomsToSolver(satVar, FalseAxiomsVec, SatSolver); - - SOLVER_RETURN_TYPE res2; - bm->GetRunTimes()->stop(RunTimes::ArrayReadRefinement); - res2 = CallSAT_ResultCheck(SatSolver, - ASTTrue, - original_input, - tosat, - true); - - if (SOLVER_UNDECIDED != res2) - return res2; - bm->GetRunTimes()->start(RunTimes::ArrayReadRefinement); + const ASTNode& ArrName = iset->first; + const map& mapper = iset->second; + + vector listOfIndices; + listOfIndices.reserve(mapper.size()); + + // Make a vector of the read symbols. + ASTVec read_node_symbols; + read_node_symbols.reserve(listOfIndices.size()); + + vector jKind; + jKind.reserve(mapper.size()); + + vector concreteIndexes; + concreteIndexes.reserve(mapper.size()); + + vector concreteValues; + concreteValues.reserve(mapper.size()); + + ASTVec index_symbols; + + vector > indexToRead; + indexToRead.insert(indexToRead.begin(), mapper.begin(), mapper.end()); + sort(indexToRead.begin(), indexToRead.end(), sortByIndexConstants); + + for (vector >::const_iterator it = indexToRead.begin(); it + != indexToRead.end(); it++) + { + const ASTNode& the_index = it->first; + listOfIndices.push_back(the_index); + + ASTNode arrsym = it->second.symbol; + read_node_symbols.push_back(arrsym); + + index_symbols.push_back(it->second.index_symbol); + + assert(read_node_symbols[0].GetValueWidth() == arrsym.GetValueWidth()); + assert(listOfIndices[0].GetValueWidth() == the_index.GetValueWidth()); + + jKind.push_back(the_index.GetKind()); + + concreteIndexes.push_back(TermToConstTermUsingModel(the_index)); + concreteValues.push_back(TermToConstTermUsingModel(arrsym)); + } + + assert(listOfIndices.size() == mapper.size()); + + //loop over the list of indices for the array and create LA, + //and add to inputAlreadyInSAT + for (int i = 0; i < listOfIndices.size(); i++) + { + const ASTNode& index_i = listOfIndices[i]; + const Kind iKind = index_i.GetKind(); + + // Create all distinct pairs of indexes. + for (int j = i + 1; j < listOfIndices.size(); j++) + { + const ASTNode& index_j = listOfIndices[j]; + + // If the index is a constant, and different, then there's no reason to check. + // Sometimes we get the same index stored multiple times in the array. Not sure why... + if (BVCONST == iKind && jKind[j] == BVCONST && index_i != index_j) + continue; + + if (ASTFalse == simp->CreateSimplifiedEQ(index_i, index_j)) + continue; // shortcut. + + AxiomToBe o(index_symbols[i], index_symbols[j], read_node_symbols[i], + read_node_symbols[j]); + + if (concreteIndexes[i] == concreteIndexes[j] && concreteValues[i] != concreteValues[j]) + { + FalseAxiomsVec.push_back(o); + //ToSATBase::ASTNodeToSATVar & satVar = tosat->SATVar_to_SymbolIndexMap(); + //applyAxiomsToSolver(satVar, FalseAxiomsVec, SatSolver); + } + else + RemainingAxiomsVec.push_back(o); + } + if (FalseAxiomsVec.size() > 0) + { + ToSATBase::ASTNodeToSATVar & satVar = tosat->SATVar_to_SymbolIndexMap(); + applyAxiomsToSolver(satVar, FalseAxiomsVec, SatSolver); + + SOLVER_RETURN_TYPE res2; + bm->GetRunTimes()->stop(RunTimes::ArrayReadRefinement); + res2 = CallSAT_ResultCheck(SatSolver, ASTTrue, original_input, tosat, true); + + if (SOLVER_UNDECIDED != res2) + return res2; + bm->GetRunTimes()->start(RunTimes::ArrayReadRefinement); + } + } } - } - } - if (RemainingAxiomsVec.size() > 0) - { - ToSATBase::ASTNodeToSATVar & satVar = tosat->SATVar_to_SymbolIndexMap(); - applyAxiomsToSolver(satVar, RemainingAxiomsVec, SatSolver); + if (RemainingAxiomsVec.size() > 0) + { + ToSATBase::ASTNodeToSATVar & satVar = tosat->SATVar_to_SymbolIndexMap(); + applyAxiomsToSolver(satVar, RemainingAxiomsVec, SatSolver); - bm->GetRunTimes()->stop(RunTimes::ArrayReadRefinement); - return CallSAT_ResultCheck(SatSolver, ASTTrue, original_input, - tosat,true); - } + bm->GetRunTimes()->stop(RunTimes::ArrayReadRefinement); + return CallSAT_ResultCheck(SatSolver, ASTTrue, original_input, tosat, true); + } - // I suspect this is the better way to do it. I.e. + // I suspect this is the better way to do it. I.e. #if 0 if(RemainingAxiomsVec.size() > 0) - { - // Add the axioms in order of how many constants there are in each. - - ToSATBase::ASTNodeToSATVar & satVar = tosat->SATVar_to_SymbolIndexMap(); - sort(RemainingAxiomsVec.begin(), RemainingAxiomsVec.end(), sortbyConstants); - int current_position = 0; - for(int n_const = 4;n_const >= 0;n_const--){ - while(current_position < RemainingAxiomsVec.size() && RemainingAxiomsVec[current_position].numberOfConstants() == n_const) - { - AxiomToBe & toBe = RemainingAxiomsVec[current_position]; - applyAxiomToSAT(SatSolver, toBe,satVar); - current_position++; - } - bm->GetRunTimes()->stop(RunTimes::ArrayReadRefinement); - SOLVER_RETURN_TYPE res2; - res2 = CallSAT_ResultCheck(SatSolver, ASTTrue, original_input, tosat, true); - if(SOLVER_UNDECIDED != res2) - return res2; - - bm->GetRunTimes()->start(RunTimes::ArrayReadRefinement); + { + // Add the axioms in order of how many constants there are in each. + + ToSATBase::ASTNodeToSATVar & satVar = tosat->SATVar_to_SymbolIndexMap(); + sort(RemainingAxiomsVec.begin(), RemainingAxiomsVec.end(), sortbyConstants); + int current_position = 0; + for(int n_const = 4;n_const >= 0;n_const--) + { + while(current_position < RemainingAxiomsVec.size() && RemainingAxiomsVec[current_position].numberOfConstants() == n_const) + { + AxiomToBe & toBe = RemainingAxiomsVec[current_position]; + applyAxiomToSAT(SatSolver, toBe,satVar); + current_position++; + } + bm->GetRunTimes()->stop(RunTimes::ArrayReadRefinement); + SOLVER_RETURN_TYPE res2; + res2 = CallSAT_ResultCheck(SatSolver, ASTTrue, original_input, tosat, true); + if(SOLVER_UNDECIDED != res2) + return res2; + + bm->GetRunTimes()->start(RunTimes::ArrayReadRefinement); + } + assert(current_position == RemainingAxiomsVec.size()); + RemainingAxiomsVec.clear(); + assert(SOLVER_UNDECIDED == CallSAT_ResultCheck(SatSolver, ASTTrue, original_input, tosat, true)); } - assert(current_position == RemainingAxiomsVec.size()); - RemainingAxiomsVec.clear(); - assert(SOLVER_UNDECIDED == CallSAT_ResultCheck(SatSolver, ASTTrue, original_input, tosat, true)); - } #endif bm->GetRunTimes()->stop(RunTimes::ArrayReadRefinement); - return SOLVER_UNDECIDED; - } //end of SATBased_ArrayReadRefinement + return SOLVER_UNDECIDED; + } //end of SATBased_ArrayReadRefinement /******************************************************************