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

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