int compute(const std::vector<std::pair<std::string, int> > & Indexes)
{
int f = 0;
for (int k = 0; k < Indexes.size(); ++k)
{
f += Indexes[k].second;
}
return f;
}
int min(const std::vector<int>& valueVector)
{
int temp = valueVector[0];
for (int i = 1; i < valueVector.size(); ++i)
{
if (valueVector[i] < temp)
temp = valueVector[i];
}
return temp;
}
int max(const std::vector<int>& valueVector)
{
int temp = valueVector[0];
for (int i = 1; i < valueVector.size(); ++i)
{
if (valueVector[i] > temp)
temp = valueVector[i];
}
return temp;
}
std::vector<std::pair<std::string, int> > myVector;
std::vector<std::string> operatorType;
std::pair<std::string, int> element1("x", 2);
std::pair<std::string, int> element2("y", 3);
std::pair<std::string, int> element3("z", 2);
myVector.push_back(element1);
myVector.push_back(element2);
myVector.push_back(element3);
operatorType.push_back("forall");
operatorType.push_back("exists");
operatorType.push_back("exists");
unsigned long cardinality = 1;
std::vector<std::vector<int> > tempResults;
std::vector<std::vector<int> > finalResults;
// new "cardinality", index
std::vector<std::pair<int, int> > cardinalityIndexVector;
// reverse the order of the vector of the variables
reverse(myVector.begin(), myVector.end());
reverse(operatorType.begin(), operatorType.end());
std::vector<int> temp(0);
std::cout << "Function " << std::endl;
for (int i = 0; i < myVector.size(); ++i)
{
cardinality *= myVector[i].second;
cardinalityIndexVector.push_back(std::pair<int, int> (cardinality, 0));
tempResults.push_back(temp);
finalResults.push_back(temp);
std::cout << operatorType[i] << " " << myVector[i].first << " (" << myVector[i].second << ") ";
}
std::cout << "f() =" << std::endl;
finalResults.push_back(temp);
for (int i = 0; i < cardinalityIndexVector.size(); ++i)
{
cardinalityIndexVector[i].first = cardinalityIndexVector[i].first / myVector[i].second;
}
std::cout << "Cardinality " << cardinality << std::endl;
for (unsigned long i = 0; i < cardinality; ++i)
{
std::vector<std::pair<std::string, int> > Indexes;
std::vector<std::pair<std::string, int> > domainsVector;
// loop over the vector of the quantified variable
for (int j = 0; j < myVector.size(); ++j)
{
if (j == 0)
{
// first variable, initialization
Indexes.push_back(std::pair<std::string, int> (myVector[j].first, i % myVector[j].second));
domainsVector.push_back(std::pair<std::string, int> (myVector[j].first, i / myVector[j].second));
}
else if (j < myVector.size())
{
Indexes.push_back(std::pair<std::string, int> (myVector[j].first, domainsVector[j - 1].second % myVector[j].second));
domainsVector.push_back(std::pair<std::string, int> (myVector[j].first, domainsVector[j - 1].second / myVector[j].second));
}
if (i == 0)
{
std::cout << myVector[j].first << " ";
}
}
if (i == 0)
std::cout << std::endl;
for (int k = 0; k < Indexes.size(); ++k)
{
std::cout << Indexes[k].second << " ";
}
std::cout << std::endl;
// loop over the vector of the quantified variable
for (int j = 0; j < myVector.size(); ++j)
{
//std::cout << "i " << i << "j " << j << std::endl;
// check if the current for loop is termined
if (cardinalityIndexVector[j].second == cardinalityIndexVector[j].first - 1)
{
// compute the value of the function
if (j == 0)
{
//std::cout << "Compute " << compute(Indexes) << std::endl;
tempResults[j].push_back(compute(Indexes));
finalResults[j].push_back(compute(Indexes));
}
if (j > 0)
{
if (operatorType[j - 1] == "forall")
{
//std::cout << "Max " << max(tempResults[j - 1]) << std::endl;
tempResults[j].push_back(max(tempResults[j - 1]));
finalResults[j].push_back(max(tempResults[j - 1]));
tempResults[j - 1].clear();
}
else if (operatorType[j - 1] == "exists")
{
//std::cout << "Min " << min(tempResults[j - 1]) << std::endl;
tempResults[j].push_back(min(tempResults[j - 1]));
finalResults[j].push_back(min(tempResults[j - 1]));
tempResults[j - 1].clear();
}
}
cardinalityIndexVector[j].second = 0;
}
else
cardinalityIndexVector[j].second++;
}
if (i == cardinality - 1)
{
if (operatorType.back() == "forall")
{
// std::cout << "Final Max " << max(tempResults[myVector.size() - 1]) << std::endl;
finalResults.back().push_back(max(tempResults[myVector.size() - 1]));
}
else if (operatorType.back() == "exists")
{
//std::cout << "Final Min " << min(tempResults[myVector.size() - 1]) << std::endl;
finalResults.back().push_back(min(tempResults[myVector.size() - 1]));
}
}
}
std::cout << "Results " << std::endl;
for (int i = 0; i < finalResults.size(); ++i)
{
for (int j = 0; j < finalResults[i].size(); ++j)
std::cout << finalResults[i][j] << " ";
std::cout << std::endl;
}
std::cout << std::endl;