* Abstraction Refinement related functions
******************************************************************/
-enum Polarity {LEFT_ONLY, RIGHT_ONLY, BOTH};
-
-void getSatVariables(const ASTNode & a, vector<unsigned> & 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<unsigned> & 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<unsigned > v_a;
- vector<unsigned > 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<unsigned > 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<unsigned> v_a;
+ vector<unsigned> 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<unsigned> 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..");
+
+ }
/******************************************************************
* 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<AxiomToBe> & toBe, SATSolver & SatSolver)
+ void
+ applyAxiomsToSolver(ToSATBase::ASTNodeToSATVar & satVar, vector<AxiomToBe> & 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<ASTNode, ArrayTransformer::arrTypeMap>& a,
+ const pair<ASTNode, ArrayTransformer::arrTypeMap>& b)
+ {
+ return a.second.size() < b.second.size();
+ }
- bool sortByIndexConstants(const pair<ASTNode,ArrayTransformer::ArrayRead> & a, const pair<ASTNode,ArrayTransformer::ArrayRead> & b)
+ bool
+ sortByIndexConstants(const pair<ASTNode, ArrayTransformer::ArrayRead> & a,
+ const pair<ASTNode, ArrayTransformer::ArrayRead> & 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<AxiomToBe> RemainingAxiomsVec;
- vector<AxiomToBe> 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<ASTNode, ArrayTransformer::ArrayRead>& mapper = iset->second;
-
- vector<ASTNode> listOfIndices;
- listOfIndices.reserve(mapper.size());
-
- // Make a vector of the read symbols.
- ASTVec read_node_symbols;
- read_node_symbols.reserve(listOfIndices.size());
-
- vector<Kind> jKind;
- jKind.reserve(mapper.size());
-
- vector<ASTNode> concreteIndexes;
- concreteIndexes.reserve(mapper.size());
-
- vector<ASTNode> 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<AxiomToBe> RemainingAxiomsVec;
+ vector<AxiomToBe> 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++)
{
- 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<ASTNode, ArrayTransformer::ArrayRead>& mapper = iset->second;
+
+ vector<ASTNode> listOfIndices;
+ listOfIndices.reserve(mapper.size());
+
+ // Make a vector of the read symbols.
+ ASTVec read_node_symbols;
+ read_node_symbols.reserve(listOfIndices.size());
+
+ vector<Kind> jKind;
+ jKind.reserve(mapper.size());
+
+ vector<ASTNode> concreteIndexes;
+ concreteIndexes.reserve(mapper.size());
+
+ vector<ASTNode> 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)
+ {
+ 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
/******************************************************************
projects / francis / stp.git / commitdiff