- Main Page
- Namespaces
- Classes
- Files
- Related Pages

# /Users/fpy/titan-1-5-MBARI/Mers/Solvers/SAT/GATSAT/CompileSAT/gen.cpp

    00001
    00002 #ifdef _MSC_VER
    00003 #pragma warning( disable : 4786 )
    00004 #endif
    00005
    00006 #include <cstdlib>
    00007 #include <cstdio>
    00008 #include <cassert>
    00009 #include <iostream>
    00010 #include <fstream>
    00011 #include <string>
    00012 #include <cmath>
    00013 #include <ctime>
    00014 #include <list>
    00015 #include <vector>
    00016
    00017 using namespace std;
    00018
    00019
    00020 class
    00021 DomainElement
    00022 {
    00023 public:
    00024         string value;
    00025         double probability;
    00026
    00027         DomainElement(string v, double p)
    00028         : value(v), probability(p)
    00029         {
    00030         }
    00031         DomainElement(DomainElement const & de)
    00032         : value(de.value), probability(de.probability)
    00033         {
    00034         }
    00035 };
    00036
    00037
    00038 class
    00039 ConstraintElement
    00040 {
    00041 public:
    00042         string variable;
    00043         string value;
    00044         bool sign;
    00045
    00046         ConstraintElement(string var, string val, bool s)
    00047         : variable(var), value(val), sign(s)
    00048         {
    00049         }
    00050         ConstraintElement(ConstraintElement const & ce)
    00051         : variable(ce.variable), value(ce.value), sign(ce.sign)
    00052         {
    00053         }
    00054 };
    00055
    00056
    00057 bool                        file_exist(char* filename);
    00058 list<unsigned int>          createCosts(unsigned int len, unsigned int maxCost);
    00059 vector<string>                createNames(unsigned int len, bool upperCase = true);
    00060 vector< DomainElement >       createDomain(unsigned int len);
    00061 vector< DomainElement >       createDomainRandom(unsigned int minDomain, unsigned int maxLen);
    00062 void                        printVariable(string name, vector< DomainElement > domain,
    00063                                           ostream & os = cout);
    00064 double                      randDouble();
    00065 int                         randRange(int low, int high);
    00066 int                         randRange(int high);
    00067 void                        printConstraintElement(ConstraintElement ce,
    00068                                                    ostream & os = cout);
    00069 void                        printConstraint(list< ConstraintElement > c,
    00070                                             ostream & os = cout);
    00071 list<ConstraintElement>     createConstraint(unsigned int minConstraint, unsigned int maxLen);
    00072 ConstraintElement           createConstraintElement();
    00073 list< list<ConstraintElement> >   createMEDEConstraints();
    00074
    00075
    00076 vector<string>  varNames;
    00077 vector< vector<DomainElement> > varDomains;
    00078
    00079 double
    00080 randDouble()
    00081 {
    00082         int n = rand();
    00083         if (n)
    00084                 n--;
    00085         double res = (((double)n) / RAND_MAX);
    00086         assert(res >= 0.0);
    00087         assert(res < 1.0);
    00088         return res;
    00089 }
    00090
    00091 int
    00092 randRange(int low, int high)
    00093 {
    00094         int res = low + (int)( randDouble() * (high - low + 1) );
    00095         assert(res >= low);
    00096         assert(res <= high);
    00097         return res;
    00098 }
    00099
    00100 int
    00101 randRange(int high)
    00102 {
    00103         return randRange(0, high);
    00104 }
    00105
    00106
    00107 bool
    00108 file_exist(char const * filename)
    00109 {
    00110         FILE *file;
    00111         if ( (file = fopen(filename,"r")) == NULL )
    00112                 return false;
    00113         fclose(file);
    00114         return true;
    00115 }
    00116
    00117
    00118 list<double>
    00119 createProbabilities(unsigned int len)
    00120 {
    00121         int * weight = new int[len];
    00122         double totalWeight = 0;
    00123         for (unsigned int i = 0; i < len; i++)
    00124         {
    00125                 weight[i] = rand();
    00126                 totalWeight += weight[i];
    00127                 //cout << "   total: " << totalWeight << endl;
    00128         }
    00129         list<double> res;
    00130         //double check = 0;
    00131         for (unsigned int i2 = 0; i2 < len; i2++)
    00132         {
    00133                 //cout << "weight: " << weight[i2] << "; total: " << totalWeight << endl;
    00134                 res.push_back( ((double)weight[i2]) / totalWeight );
    00135                 //check += ((double)weight[i2]) / totalWeight;
    00136         }
    00137         //cout << "   check: " << check << endl;
    00138         delete[] weight;
    00139         return res;
    00140 }
    00141
    00142
    00143 list<unsigned int>
    00144 createCosts(unsigned int len, unsigned int maxCost)
    00145 {
    00146         list<unsigned int> res;
    00147         for (unsigned int i = 0; i < len; i++)
    00148         {
    00149                 res.push_back( (unsigned int)randRange(0, maxCost) );
    00150         }
    00151         return res;
    00152 }
    00153
    00154
    00155 vector<string>
    00156 createNames(unsigned int len, bool upperCase)
    00157 {
    00158         char name[32];
    00159         char base = upperCase ? 'A' : 'a';
    00160         vector<string> res;
    00161         for (unsigned int i = 0; i < len; i++)
    00162         {
    00163                 unsigned int resid = i;
    00164                 char * pos = name;
    00165                 *pos = base + (resid % 26);
    00166                 pos++;
    00167                 resid /= 26;
    00168                 while (resid)
    00169                 {
    00170                         if(resid <= 26){
    00171                                 *pos = base + resid - 1;
    00172                                 resid /= 27;
    00173                         }else{
    00174                                 *pos = base + ((resid - 1) % 26);
    00175                                 resid /= 26;
    00176                         }
    00177                         pos++;
    00178                 }
    00179                 *pos = '\0';
    00180                 string nameStr(name);
    00181                 res.push_back(nameStr);
    00182         }
    00183         return res;
    00184 }
    00185
    00186
    00187 vector< DomainElement >
    00188 createDomain(unsigned int len)
    00189 {
    00190         vector< DomainElement > res;
    00191         vector<string> vals  = createNames(len, false);
    00192         list<double> probs = createProbabilities(len);
    00193
    00194         vector<string>::const_iterator vIter;
    00195         list<double>::const_iterator pIter;
    00196         for (vIter = vals.begin(), pIter = probs.begin(); vIter != vals.end(); vIter++, pIter++)
    00197         {
    00198                 string v = *vIter;
    00199                 double p = *pIter;
    00200                 res.push_back(DomainElement(v,p));
    00201         }
    00202         return res;
    00203 }
    00204
    00205
    00206 vector< DomainElement >
    00207 createDomainRandom(unsigned int minDomain, unsigned int maxLen)
    00208 {
    00209         unsigned int domainSize;
    00210         if(minDomain >= maxLen)
    00211                 domainSize = maxLen;
    00212         else
    00213                 domainSize = (unsigned int)randRange(minDomain, maxLen);
    00214         return createDomain(domainSize);
    00215 }
    00216
    00217
    00218 list<ConstraintElement>
    00219 createConstraint(unsigned int minConstraint, unsigned int maxLen)
    00220 {
    00221         unsigned int len;
    00222         if(minConstraint >= maxLen)
    00223                 len = maxLen;
    00224         else
    00225                 len = (unsigned int)randRange(minConstraint, maxLen);
    00226         list<ConstraintElement> res;
    00227         for (unsigned int i = 0; i < len; i++)
    00228         {
    00229                 ConstraintElement next = createConstraintElement();
    00230                 while (true)
    00231                 {
    00232                         bool ok = true;
    00233                         list<ConstraintElement>::const_iterator cIter;
    00234                         for (cIter = res.begin(); cIter != res.end(); cIter++)
    00235                         {
    00236                                 if ((next.variable == (*cIter).variable) && (next.value == (*cIter).value))
    00237                                         ok = false;
    00238                         }
    00239                         if (ok)
    00240                                 break;
    00241                         next = createConstraintElement();
    00242                 }
    00243                 res.push_back(next);
    00244         }
    00245         return res;
    00246 }
    00247
    00248
    00249 ConstraintElement
    00250 createConstraintElement()
    00251 {
    00252         bool sign = (randDouble() < 0.5);
    00253         unsigned int varIndex = (unsigned int)randRange(0, varNames.size() - 1);
    00254         vector<DomainElement> domain = varDomains[varIndex];
    00255         unsigned int valIndex = (unsigned int)randRange(0, domain.size() - 1);
    00256         string var = varNames[varIndex];
    00257         string val = domain[valIndex].value;
    00258         return ConstraintElement(var, val, sign);
    00259 }
    00260
    00261
    00262 void
    00263 printVariable(string name, vector< DomainElement > domain, ostream & os)
    00264 {
    00265         os << name << "  ";
    00266         vector<DomainElement>::const_iterator dIter;
    00267         for (dIter = domain.begin(); dIter != domain.end(); dIter++)
    00268         {
    00269                 os << (*dIter).value << " " << (*dIter).probability << " " ;
    00270         }
    00271         os << endl;
    00272 }
    00273
    00274
    00275 void
    00276 printConstraintElement(ConstraintElement ce, ostream & os)
    00277 {
    00278         if (!ce.sign)
    00279                 os << "!";
    00280         os << "[" << ce.variable << "=" << ce.value << "]";
    00281 }
    00282
    00283
    00284 void
    00285 printConstraint(list< ConstraintElement > c, ostream & os)
    00286 {
    00287         list<ConstraintElement>::const_iterator cIter;
    00288         for (cIter = c.begin(); cIter != c.end(); cIter++)
    00289         {
    00290                 printConstraintElement((*cIter), os);
    00291                 os << " " ;
    00292         }
    00293         os << endl;
    00294 }
    00295
    00296
    00297 list< list<ConstraintElement> >
    00298 createMEDEConstraints()
    00299 {
    00300         //unsigned int varIndex = (unsigned int)randRange(0, varNames.size() - 1);
    00301         //vector<DomainElement> domain = varDomains[varIndex];
    00302         //unsigned int valIndex = (unsigned int)randRange(0, domain.size() - 1);
    00303         //string var = varNames[varIndex];
    00304         //string val = domain[valIndex].value;
    00305         //ConstraintElement res = {var, val, sign};
    00306
    00307         list< list<ConstraintElement> >  res;
    00308         for (unsigned int i = 0; i < varNames.size(); i++)
    00309         {
    00310                 string var = varNames[i];
    00311                 vector<DomainElement> domain = varDomains[i];
    00312
    00313                 // domain exhaustion:
    00314                 list<ConstraintElement> con;
    00315                 for (unsigned int d = 0; d < domain.size(); d++)
    00316                 {
    00317                         ConstraintElement ce(var, domain[d].value, true);
    00318                         con.push_back(ce);
    00319                 }
    00320                 res.push_back(con);
    00321
    00322                 // mutual exclusion:
    00323                 for (unsigned int a1 = 0; a1 < domain.size(); a1++)
    00324                 {
    00325                         for (unsigned int a2 = a1+1; a2 < domain.size(); a2++)
    00326                         {
    00327                                 list<ConstraintElement> con2;
    00328                                 ConstraintElement ce1(var, domain[a1].value, false);
    00329                                 con2.push_back(ce1);
    00330                                 ConstraintElement ce2(var, domain[a2].value, false);
    00331                                 con2.push_back(ce2);
    00332                                 res.push_back(con2);
    00333                         }
    00334                 }
    00335         }
    00336         return res;
    00337 }
    00338
    00339
    00340
    00341 int
    00342 main(int argc, char** argv)
    00343 {
    00344         argc--;
    00345         argv++;
    00346
    00347         srand((unsigned int)time(NULL));
    00348
    00349         bool useProb = true;
    00350         unsigned int maxCost;
    00351         unsigned int minConstraint = 2;
    00352         unsigned int minDomain = 2;
    00353
    00354         for (; argc > 0 && argv[argc-1][0] == '-'; argc--)
    00355         {
    00356                 if (argv[argc-1][1] == 'c' || argv[argc-1][1] == 'C')
    00357                 {
    00358                         cout << "Using cost values instead of probabilities." << endl;
    00359                         useProb = false;
    00360                         if (argv[argc-1][2] == '\0')
    00361                         {
    00362                                 maxCost = 9;
    00363                         } else
    00364                         {
    00365                                 char * numStr = argv[argc-1]+2;
    00366                                 maxCost = (unsigned int)atoi(numStr);
    00367                         }
    00368                         cout << "Values range from 0 to " << maxCost << "." << endl;
    00369                 } else
    00370                 if (argv[argc-1][1] == 'm' || argv[argc-1][1] == 'M')
    00371                 {
    00372                         cout << "Minimum literals per clause specified." << endl;
    00373                         if (argv[argc-1][2] == '\0')
    00374                         {
    00375                                 minConstraint = 2;
    00376                         } else
    00377                         {
    00378                                 char * numStr = argv[argc-1]+2;
    00379                                 minConstraint = (unsigned int)atoi(numStr);
    00380                         }
    00381                         cout << "At least " << minConstraint << " literals per clause." << endl;
    00382                 } else
    00383                 if (argv[argc-1][1] == 'd' || argv[argc-1][1] == 'D')
    00384                 {
    00385                         cout << "Minimum values per domain specified." << endl;
    00386                         if (argv[argc-1][2] == '\0')
    00387                         {
    00388                                 minDomain = 2;
    00389                         } else
    00390                         {
    00391                                 char * numStr = argv[argc-1]+2;
    00392                                 minDomain = (unsigned int)atoi(numStr);
    00393                         }
    00394                         cout << "At least " << minDomain << " values per domain." << endl;
    00395                 } else
    00396                 {
    00397                         cerr << "Ignoring unrecognized option '" << argv[argc-1] << "'." << endl;
    00398                 }
    00399         }
    00400         if (argc != 3 && argc != 6 && argc != 5 && argc != 8)
    00401         {
    00402                 cout << "Arguments should be:" << endl << endl;
    00403                 cout << "   <num of variables> <max domain size> <filename> "
    00404                      << "[<num state vars> <filename>] "
    00405                      << "[<num constraints> <max constraint size> <filename>] "
    00406                      << "[-c[<max cost>]] [-m[<min literals/clause>]] [-d[<min values/domain>]]" << endl;
    00407                 cout << endl;
    00408                 cout << "-c   uses costs instead of probabilities." << endl;
    00409                 cout << "-m   minimum number of literals per claues." << endl;
    00410                 cout << "-d   minimum number of values per domain." << endl;
    00411                 cout << endl;
    00412                 exit(-1);
    00413         }
    00414         //cout << endl;
    00415
    00416         unsigned int numVars = (unsigned int)atoi(argv[0]);
    00417         unsigned int maxDomain = (unsigned int)atoi(argv[1]);
    00418         char const * varFilename = argv[2];
    00419         char const * constraintFilename = NULL;
    00420         char const * stateFilename = NULL;
    00421
    00422         unsigned int numState = 0;
    00423         if (argc == 5 || argc == 8)
    00424         {
    00425                 numState = (unsigned int)atoi(argv[3]);
    00426                 stateFilename = argv[4];
    00427         }
    00428
    00429         unsigned int numConstraints = 0;
    00430         unsigned int maxConstraint = 0;
    00431         if (argc == 6 || argc == 8)
    00432         {
    00433                 numConstraints = (unsigned int)atoi(argv[argc-3]);
    00434                 maxConstraint  = (unsigned int)atoi(argv[argc-2]);
    00435                 constraintFilename = argv[argc-1];
    00436         }
    00437
    00438         (void)useProb;
    00439         //cout << "Number of variables: " << numVars << ";  Maximum domain size: " << maxDomain
    00440         //     << endl << endl;
    00441
    00442         ofstream * out;
    00443         ofstream outdes(varFilename);
    00444         out = &outdes;
    00445         varNames = createNames(numVars, true);
    00446         unsigned int count = 0;
    00447         for (vector<string>::const_iterator vIter = varNames.begin(); vIter != varNames.end();
    00448              vIter++)
    00449         {
    00450                 if (stateFilename && (count == numVars - numState))  // switch from design file
    00451                 {
    00452                         out->close();
    00453                         out = new ofstream(stateFilename);
    00454                 }
    00455                 vector<DomainElement> domain = createDomainRandom(minDomain, maxDomain);
    00456                 varDomains.push_back(domain);
    00457                 printVariable((*vIter), domain, *out);
    00458                 count++;
    00459         }
    00460         out->close();
    00461
    00462         //cout << endl;
    00463
    00464         if (numConstraints > 0)
    00465         {
    00466                 ofstream outc(constraintFilename);
    00467                 ofstream outc2((string(constraintFilename) + "2").c_str());
    00468                 list< list<ConstraintElement> > mede = createMEDEConstraints();
    00469                 list< list<ConstraintElement> >::const_iterator medeIter;
    00470                 for (medeIter = mede.begin(); medeIter != mede.end(); medeIter++)
    00471                 {
    00472                         printConstraint((*medeIter), outc);
    00473                 }
    00474                 outc << endl;
    00475                 for (unsigned int i = 0; i < numConstraints; i++)
    00476                 {
    00477                         list<ConstraintElement> con = createConstraint(minConstraint, maxConstraint);
    00478                         printConstraint(con, outc);
    00479                         printConstraint(con, outc2);
    00480                 }
    00481                 outc.close();
    00482                 outc2.close();
    00483         }
    00484
    00485         exit(0);
    00486         return 0; // to make MSVC happy - yes, it's that stupid.
    00487 }
    00488