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

# /Users/fpy/titan-1-5-MBARI/Mers/Solvers/SAT/GATSAT/OpSAT/opsat_driver.cpp

    00001
    00002 //
    00003 // Copyright (c) 2004           Model-based Embedded and Robotic Systems Group
    00004 // All Rights Reserved          Massachusetts Institute of Technology
    00005 //
    00006 // This software is provided as is. Model-based Embedded and Robotic Systems
    00007 // (MERS) group does not assume any responsibility.
    00008 //
    00009 // Organization:        Model-based Embedded and Robotic Systems Group
    00010 //                                      Massachusetts Institute of Technology
    00011 //
    00013 //# CHECKED MJP 08-07-2002
    00014
    00015 #ifdef _MSC_VER
    00016 #pragma warning( disable : 4786 )
    00017 #endif
    00018
    00019 #include "Opsat.h"
    00020
    00021 #include <cstdlib>
    00022 #include <cstdio>
    00023 #include <iostream>
    00024 #include <fstream>
    00025 #include <cmath>
    00026 #include <sstream>
    00027
    00028 #ifdef USE_DEPENDENCY_GENERATOR
    00029 #include <Mers/Generators/IDSetGenerator/IDSetGenerator.h>
    00030 #else
    00031 #include <Mers/Generators/BFIG/BFIGVariable.h>
    00032 #include <Mers/Generators/BFIG/BFIGAssignment.h>
    00033 #include <Mers/Generators/BFIG/BFIGImplicant.h>
    00034 #include <Mers/Generators/BFIG/BFIGConstraint.h>
    00035 #endif
    00036
    00037 #include <Mers/Models/Base/BaseModelVariable.h>
    00038 #include <Mers/Models/Base/BaseModelAssignment.h>
    00039 #include <Mers/Models/Base/BaseModelSentence.h>
    00040 #include <Mers/Models/Base/BaseModel.h>
    00041
    00042 #include <Mers/Utils/Containers/DynamicArrayTemplate.h>
    00043
    00044 // needed for the probability listing
    00045 #include <vector>
    00046
    00048
    00049 using namespace Mers::Solvers::SAT::GATSAT::OpSAT;
    00050 using Mers::Models::Base::BaseModel;
    00051 using Mers::Models::Base::BaseModelValueArray;
    00052 using Mers::Models::Base::BaseModelValue;
    00053 using Mers::Models::Base::BaseModelClauseArray;
    00054 using Mers::Models::Base::BaseModelClause;
    00055 using Mers::Models::Base::BaseModelSentence;
    00056 using Mers::Models::Base::BaseModelVariableArray;
    00057 using Mers::Models::Base::BaseModelVariable;
    00058 using Mers::Models::Base::BaseModelAssignment;
    00059 using Mers::Utils::Containers::IntegerArray;
    00060 using std::endl;
    00061 using std::cerr;
    00062 using std::cout;
    00063 using std::vector;
    00064 using std::ifstream;
    00065 using std::istringstream;
    00066 using std::ws;
    00067
    00069
    00070 bool file_exist(char* filename);
    00071 void readVariables(char const * filename, bool useProb,
    00072         BaseModel &model, vector<double> &probabilities);
    00073 void readConstraints(char const * filename, BaseModel &model,
    00074         BaseModelSentence &res);
    00075
    00077
    00078 bool
    00079 file_exist(char const * filename)
    00080 {
    00081         FILE *file;
    00082         if ( (file = fopen(filename,"r")) == NULL )
    00083                 return false;
    00084         fclose(file);
    00085         return true;
    00086 }
    00087
    00089
    00090 void readVariables(char const * filename, bool useProb, BaseModel &model,
    00091         IntegerArray &probabilityMap, vector<double> &probabilities)
    00092 {
    00093         char next;
    00094         char tmp[400];
    00095
    00096         if (!file_exist(filename))
    00097         {
    00098                 cerr << "File " << filename << " does not exist." << endl;
    00099                 exit(-1);
    00100         }
    00101
    00102         ifstream in(filename);
    00103
    00104         // skip comment lines
    00105         while (!in.eof() && (next=in.peek()) == '#')
    00106                 in.getline(tmp,400);
    00107
    00108         if (in.eof())
    00109         {
    00110                 cout << "Data file contains no variables. " << endl;
    00111                 return;  // try anyway, for testing...
    00112         }
    00113
    00114         in >> ws;
    00115         while (!in.eof())
    00116         {
    00117                 in.getline(tmp,399);  // read variable
    00118                 in >> ws;
    00119                 if (strlen(tmp) == 0)
    00120                         continue;
    00121                 istringstream line(tmp);
    00122                 char varname[400];
    00123                 line >> varname;
    00124                 line >> ws;
    00125                 BaseModelValueArray domain(true);
    00126                 probabilityMap.pushBack(probabilities.size());
    00127                 while (!line.eof())
    00128                 {
    00129                         char val[400];
    00130                         double p;
    00131
    00132                         line >> val;
    00133                         //::cout << "   val: " << val << ", " ;
    00134                         line >> p;
    00135                         //::cout << "prob: " << p << endl;
    00136                         line >> ws;
    00137                         domain.pushBack(new BaseModelValue(val));
    00138                         probabilities.push_back(p);
    00139                 }
    00140                 model.addDomain(varname, domain);
    00141
    00142                 model.addVariable(varname, BaseModelVariable::State, model.getDomain(varname));
    00143                 //cout << "Read variable: " << *var << endl ;
    00144                 //::cout << "(num values: " << values.size() << ")" << endl;
    00146         }
    00147
    00148         in.close();
    00149
    00150         //cout << "Read file with " << (res.size()) << " variables." << endl;
    00151         //cout << endl;
    00152 }
    00153
    00155
    00156 void
    00157 readConstraints(char const * filename, BaseModel &model, BaseModelSentence &res)
    00158 {
    00159         char next;
    00160         char tmp[400];
    00161
    00162         if (!file_exist(filename))
    00163         {
    00164                 cerr << "File " << filename << " does not exist." << endl;
    00165                 exit(-1);
    00166         }
    00167
    00168         ifstream in(filename);
    00169
    00170         // skip comment lines
    00171         while (!in.eof() && (next=in.peek()) == '#')
    00172                 in.getline(tmp,400);
    00173
    00174         in >> ws;
    00175         if (in.eof())
    00176         {
    00177                 cout << "Data file contains no constraints." << endl;
    00178                 return;  // try anyway, for testing...
    00179         }
    00180
    00181         while (!in.eof())
    00182         {
    00183                 in.getline(tmp,399);  // read constraint
    00184                 in >> ws;
    00185                 if (strlen(tmp) == 0)
    00186                         continue;
    00187                 istringstream line(tmp);
    00188                 BaseModelClause * constraint =
    00189                         new BaseModelClause(BaseModelClause::DISJUNCTIVE, true);
    00190                 while (!line.eof())
    00191                 {
    00192                         char   tmpChar;
    00193                         char   token[400];
    00194                         char   vala[400];
    00195                         char * val = vala;  // is this safe?
    00196                         bool   parity = true;
    00197                         line >> tmpChar;
    00198                         if (tmpChar == '!')
    00199                         {
    00200                                 parity = false;
    00201                                 line >> ws;
    00202                                 line >> tmpChar;
    00203                         }
    00204                         bool bracketOpened = false;  // Allow for either form
    00205                         if (tmpChar == '[')
    00206                         {
    00207                                 bracketOpened = true;
    00208                                 line >> ws;
    00209                                 line >> token;
    00210                         } else
    00211                         {
    00212                                 token[0] = tmpChar;
    00213                                 line >> (token+1);
    00214                         }
    00215                         for (unsigned int i = 0; i < sizeof(token); i++)
    00216                         {
    00217                                 char cur = token[i];
    00218                                 if (cur == '\0')  // end of string - assume whitespace separated.
    00219                                 {
    00220                                         line >> ws;
    00221                                         line >> tmpChar;
    00222                                         if (tmpChar != '=')
    00223                                         {
    00224                                                 cerr << "Error in reading from constraint file." << endl;
    00225                                                 cerr << "Choked on line: \"" << tmp << "\"" << endl;
    00226                                                 exit(-1);
    00227                                         }
    00228                                         line >> ws;
    00229                                         line >> vala;
    00230                                         val = vala;
    00231                                         if (val[strlen(val) - 1] == ']')  // closing bracket - always ignore?
    00232                                         {
    00233                                                 val[strlen(val) - 1] = '\0';
    00234                                         }
    00235                                         if (!(*val))  // no string left to find!
    00236                                         {
    00237                                                 cerr << "Error in reading from constraint file.." << endl;
    00238                                                 exit(-1);
    00239                                         }
    00240                                         break;
    00241                                 }
    00242
    00243                                 // whitespace handling below is not needed, since it can never occur...
    00244                                 if (cur == '=' || cur == ' ' || cur == '\t')
    00245                                 {
    00246                                         token[i] = '\0';
    00247                                         if (cur != '=')
    00248                                         {
    00249                                                 for (i++; i < sizeof(token); i++)
    00250                                                 {
    00251                                                         if (token[i] == '=')
    00252                                                                 break;
    00253                                                 }
    00254                                         }
    00255                                         for (i++; i < sizeof(token); i++)
    00256                                         {
    00257                                                 if (token[i] != ' ' && token[i] != '\t')
    00258                                                         break;
    00259                                         }
    00260                                         if (!(i < sizeof(token)))  // no string left to find!
    00261                                         {
    00262                                                 cerr << "Error in reading from constraint file..." << endl;
    00263                                                 exit(-1);
    00264                                         }
    00265                                         val = &(token[i]);
    00266                                         if (val[strlen(val) - 1] == ']')  // closing bracket - always ignore?
    00267                                         {
    00268                                                 val[strlen(val) - 1] = '\0';
    00269                                         }
    00270                                         if (!(*val))  // no string left to find!
    00271                                         {
    00272                                                 cerr << "Error in reading from constraint file...." << endl;
    00273                                                 exit(-1);
    00274                                         }
    00275                                         break;
    00276                                 }
    00277                         }
    00278                         line >> ws;
    00279
    00280                         // get the corresponding assignment:
    00281                         BaseModelAssignment * a;
    00282                         if(parity)
    00283                                 a = model.getAssignment(token, val, BaseModelAssignment::Positive);
    00284                         else
    00285                                 a = model.getAssignment(token, val, BaseModelAssignment::Negative);
    00286                         constraint->pushBack(a);
    00287                 }
    00288                 //cout << "Read constraint: " << (*constraint) << endl ;
    00289                 res.pushBack(constraint);
    00290         }
    00291
    00292         in.close();
    00293
    00294         //cout << "Read file with " << (res.size()) << " constraints." << endl;
    00295         //cout << endl;
    00296 }
    00297
    00299
    00300 int
    00301 opsat_test()
    00302 {
    00303
    00304         return 0;
    00305 }
    00306
    00308
    00309 void printTestResults(FILE * testFile, BaseModelClauseArray * results)
    00310 {
    00311         for (unsigned int r = 0; r < results->getLength(); r++)
    00312         {
    00313                 BaseModelClause &res = *((*results)[r]);
    00314
    00315                 if(r != 0) {
    00316                         fprintf(testFile, "\n");
    00317                 }
    00318                 for(unsigned int a = 0; a < res.getLength(); a++) {
    00319                         BaseModelAssignment &asg = *(res[a]);
    00320                         if(a != 0) {
    00321                                 fprintf(testFile, ", ");
    00322                         }
    00323                         fprintf(testFile, "(%s = %s)", asg.getVariable()->getName(),
    00324                                 asg.getValue()->getName());
    00325                 }
    00326         }
    00327 }
    00328
    00330
    00331 int
    00332 main(int argc, char** argv)
    00333 {
    00334         argc--;
    00335         argv++;
    00336
    00337         unsigned int useDebug = 0;
    00338         bool useCD = true;
    00339         bool useDPLL = false;
    00340         bool satisfy = true;
    00341         bool useProb = false;
    00342         int numResults = 1;
    00343         bool usePedantic = false;
    00344         bool saveTest = false;
    00345         char const * testSaveFileName = "test.out";
    00346
    00347         for (; argc > 0 && argv[argc-1][0] == '-'; argc--)
    00348         {
    00349                 if (argv[argc-1][1] == 'c' || argv[argc-1][1] == 'C')
    00350                 {
    00351                         cout << "Using non-Conflict-Directed search." << endl;
    00352                         useCD = false;
    00353                 } else
    00354                 if (argv[argc-1][1] == 'x' || argv[argc-1][1] == 'X')
    00355                 {
    00356                         cout << "Using pedantic conflict generation." << endl;
    00357                         usePedantic = true;
    00358                 } else
    00359                 if (argv[argc-1][1] == 'b' || argv[argc-1][1] == 'B')
    00360                 {
    00361                         cout << "Showing debug info." << endl;
    00362                         useDebug = 10;
    00363                 } else
    00364                 if (argv[argc-1][1] == 'u' || argv[argc-1][1] == 'U')
    00365                 {
    00366                         cout << "Trying for UNSAT problem instead of SAT." << endl;
    00367                         satisfy = false;
    00368                 } else
    00369                 if (argv[argc-1][1] == 'd' || argv[argc-1][1] == 'D')
    00370                 {
    00371                         cout << "Using DPLL in SAT." << endl;
    00372                         useDPLL = true;
    00373                 } else
    00374                 if (argv[argc-1][1] == 'p' || argv[argc-1][1] == 'P')
    00375                 {
    00376                         cout << "Treating costs as probabilities." << endl;
    00377                         useProb = true;
    00378                 } else
    00379                 if (argv[argc-1][1] == 'n' || argv[argc-1][1] == 'N')
    00380                 {
    00381                         char * numStr = argv[argc-1]+2;
    00382                         numResults = atoi(numStr);
    00383                         cout << "Searching for best " << numResults << " results." << endl;
    00384                 } else if (argv[argc - 1][1] == 't') {
    00385                         cout << "Building test output file." << endl;
    00386                         saveTest = true;
    00387                 } else
    00388                 {
    00389                         cout << "Ignoring unrecognized option '" << argv[argc-1] << "'." << endl;
    00390                 }
    00391         }
    00392         if (argc < 3 || argc > 4)
    00393         {
    00394                 cout << "Arguments should be:" << endl << endl;
    00395                 cout << "   <design_var_file> <state_var_file> "
    00396                      << "<constraint_file> [<extra_constraint_file>] [-c][-e][-d][-n]" << endl;
    00397                 cout << endl;
    00398                 cout << "<extra_constraint_file> does not need to be provided." << endl;
    00399                 cout << endl;
    00400                 cout << "-u   tries for UNSAT instead of SAT." << endl;
    00401                 cout << "-c   does not use conflict-direction." << endl;
    00402                 cout << "-d   uses DPLL in the SAT engine." << endl;
    00403                 cout << "-b   show debug info." << endl;
    00404                 cout << "-p   treats costs as probabilities." << endl;
    00405                 cout << "-n#  specifies the number to find (default is 1)." << endl;
    00406                 cout << "-t   writes results of the run to test.out for verification." << endl;
    00407                 cout << endl;
    00408                 exit(-1);
    00409         }
    00410         cout << endl;
    00411
    00412         char const * designVariableFile = argv[0];
    00413         char const * stateVariableFile = argv[1];
    00414         char const * constraintFile = argv[2];
    00415         char const * extraConstraintFile = (argc > 3) ? argv[3] : NULL;
    00416
    00417         BaseModel model(designVariableFile);
    00418         vector<double> probabilities;
    00419         IntegerArray probabilityMap;
    00420
    00421         readVariables(designVariableFile, useProb, model, probabilityMap, probabilities);
    00422         unsigned int numDesignVariables = model.getVariables()->getLength();
    00423
    00424         readVariables(stateVariableFile, useProb, model, probabilityMap, probabilities);
    00425         //unsigned int numOtherVariables = model.getVariables()->getLength() - numDesignVariables;
    00426
    00427         BaseModelVariableArray designVariables(false);
    00428         {
    00429                 BaseModelVariableArray &allVars = *(model.getVariables());
    00430                 designVariables.resize(numDesignVariables);
    00431                 for(unsigned int v = 0; v < numDesignVariables; v++){
    00432                         designVariables[v] = allVars[v];
    00433                 }
    00434         }
    00435
    00436         BaseModelSentence constraints(BaseModelSentence::CNF, true);
    00437         readConstraints(constraintFile, model, constraints);
    00438         BaseModelSentence extraConstraints(BaseModelSentence::CNF, true);
    00439         if (extraConstraintFile)
    00440                 readConstraints(extraConstraintFile, model, extraConstraints);
    00441
    00442         //float cutoff = 0.999F;
    00443         int maxStatesTime = 2000000;
    00444         int maxStatesSize = 1500000;
    00445
    00446 #ifdef USE_DEPENDENCY_GENERATOR
    00447         if (useDebug)
    00448                 cout << "Constructing Dependecy-Based Opsat..." << endl;
    00449         BaseModelVariableArrayArray searchGroups(false);
    00450         searchGroups.pushBack(&designVariables);
    00451
    00452         IDSetGenerator * gen = new IDSetGenerator(searchGroups);
    00453         Opsat * opsat = new Opsat(gen, designVariables.getLength(),
    00454                 *model.getVariables(), constraints, useDPLL);
    00455         opsat->skipExpanding(true);
    00456 #else
    00457         if (useDebug)
    00458                 cout << "Constructing opsat..." << endl;
    00459         Opsat * opsat = new Opsat(designVariables, probabilityMap, probabilities, *model.getVariables(),
    00460                 constraints, useDPLL);
    00461 #endif
    00462         opsat->setDebug(useDebug);
    00463
    00464 #ifdef _DEBUG
    00465         if (useDebug)
    00466                 cout << "Initial Opsat:" << endl << (*opsat) << endl;
    00467 #endif
    00468
    00469         FILE * testFile = NULL;
    00470
    00471         if(saveTest) {
    00472                 testFile = fopen(testSaveFileName, "w");
    00473                 if(testFile == NULL) {
    00474                         perror(testSaveFileName);
    00475                         cout << "Warning: Unable to open test file, test data will not be saved" << endl;
    00476                         saveTest = false;
    00477                 }
    00478         }
    00479
    00480         if (extraConstraints.getLength() == 0)  // only one problem...
    00481         {
    00482                 BaseModelClauseArray * results;
    00483                 if(satisfy)
    00484                         results = opsat->findSatisfyingSolutions(numResults, maxStatesTime,
    00485                                 maxStatesSize);
    00486                 else
    00487                         results = opsat->findUnsatisfyingSolutions(numResults, maxStatesTime,
    00488                                 maxStatesSize);
    00489
    00490                 //cout << "Final Opsat:" << endl << (*opsat) << endl;
    00491                 if(results != NULL){
    00492                         cout << "Results generated (" << results->getLength() << "): " << endl;
    00493                         for (unsigned int r = 0; r < results->getLength(); r++)
    00494                         {
    00495                                 cout << "    " << *((*results)[r]) << endl ;
    00496                         }
    00497                         if(saveTest) {
    00498                                 printTestResults(testFile, results);
    00499                         }
    00500                 }else{
    00501                         cout << "Results generated (0): " << endl;
    00502                 }
    00503
    00504                 cout << endl;
    00505                 opsat->printStatistics();
    00506
    00507         } else
    00508         {
    00509                 BaseModelSentence::Iterator cIter;
    00510                 for (cIter = extraConstraints.begin(); cIter != extraConstraints.end(); cIter++)
    00511                 {
    00512                         BaseModelClause * clause = &(*cIter);
    00513                         cout << endl << endl
    00514                              << "Trying with  constraint: " << *clause << endl << endl;
    00515                         opsat->setTemporaryConstraint(clause);
    00516
    00517                         BaseModelClauseArray * results;
    00518                         if(satisfy)
    00519                                 results = opsat->findSatisfyingSolutions(numResults, maxStatesTime,
    00520                                 maxStatesSize);
    00521                         else
    00522                                 results = opsat->findUnsatisfyingSolutions(numResults, maxStatesTime,
    00523                                 maxStatesSize);
    00524
    00525                         //cout << "Final Opsat:" << endl << opsat << endl;
    00526                         if(results != NULL){
    00527                                 cout << "Results generated (" << results->getLength() << "): " << endl;
    00528                                 for (unsigned int r = 0; r < results->getLength(); r++)
    00529                                 {
    00530                                         cout << "    " << *((*results)[r]) << endl ;
    00531                                 }
    00532                                 if(saveTest) {
    00533                                         printTestResults(testFile, results);
    00534                                 }
    00535                         }else{
    00536                                 cout << "Results generated (0): " << endl;
    00537                         }
    00538                 }
    00539         }
    00540
    00541         if(saveTest)
    00542                 fclose(testFile);
    00543
    00544         delete opsat;
    00545
    00546         //exit(0);
    00547         return 0; //# to make MSVC happy - yes, it's that stupid.
    00548 }
    00549