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

# /Users/fpy/titan-1-5-MBARI/Mers/Solvers/SAT/GATSAT/OpSAT/opsat_dll.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 <cstdlib>
    00020 #include <cstdio>
    00021 #include <iostream>
    00022 #include <fstream>
    00023 #include <string>
    00024 #include <cmath>
    00025 //#include <ctime>
    00026 #include <list>
    00027 #include <sstream>
    00028 #include <windows.h>
    00029
    00030 #include "Opsat.h"
    00031 #include <Mers/Generators/BFIG/BFIGVariable.h>
    00032 #include <Mers/Generators/BFIG/BFIGAssignment.h>
    00033 #include <Mers/Generators/BFIG/BFIGImplicant.h>
    00034 //#include "VSAT/Constraint.h"
    00035 //#include "VSAT/ConstraintUnit.h"
    00036 //#include "../../ISAT/ISATConstraint.h"
    00037 //#include "../../ISAT/ISATConstraintUnit.h"
    00038
    00039 #include <jni.h>
    00040 #ifdef __cplusplus
    00041 extern "C" {
    00042 #endif
    00043 JNIEXPORT void JNICALL Java_Opsat_createOpsat (JNIEnv *env, jobject obj, jstring designFile,
    00044                                          jstring stateFile, jstring constraintFile);
    00045 JNIEXPORT void JNICALL Java_Opsat_deleteOpsat (JNIEnv *env, jobject obj);
    00046
    00047 #ifdef __cplusplus
    00048 }
    00049 #endif
    00050
    00051 using namespace std;
    00052
    00053 bool                      file_exist(char* filename);
    00054 list<Variable *>          readVariables(char const * filename, bool useProb = false);
    00055 list<Constraint const *>  readConstraints(char const * filename,
    00056                                           list<Variable *> vars);
    00057 Opsat *                   loadOpsat(char const * designName, char const * stateName,
    00058                                     char const * constraintName);
    00059
    00060
    00061 static Opsat * dllOpsat;
    00062
    00063 extern "C"
    00064 {
    00065
    00066 int WINAPI
    00067 opsat_init(HANDLE h, DWORD reason, void *foo)
    00068 {
    00069         (void)h; (void)reason; (void)foo;
    00070         dllOpsat = NULL;
    00071         /*#
    00072         ofstream outlog;
    00073         streambuf * cout_buffer = 0;
    00074         streambuf * cerr_buffer = 0;
    00075         outlog.open("opsatdll.log");
    00076         cout_buffer = cout.rdbuf(outlog.rdbuf());
    00077         cerr_buffer = cerr.rdbuf(outlog.rdbuf());
    00078         */
    00079         return 1;
    00080 }
    00081
    00082 int
    00083 run_demo()
    00084 {
    00085         //# cout << "This works... I guess...." << endl;
    00086         return 7;
    00087 }
    00088
    00089 }
    00090
    00091 JNIEXPORT void JNICALL
    00092 Java_Opsat_createOpsat (JNIEnv *env, jobject obj, jstring designFile,
    00093                   jstring stateFile, jstring constraintFile)
    00094 {
    00095         (void)obj;
    00096         //readVariables("design.in", true);
    00097         dllOpsat = new Opsat(list<Variable *>(), list<Constraint const *>());
    00098         char const * designName     = env->GetStringUTFChars(designFile, 0);
    00099         char const * stateName      = env->GetStringUTFChars(stateFile, 0);
    00100         char const * constraintName = env->GetStringUTFChars(constraintFile, 0);
    00101         //dllOpsat = loadOpsat(designName, stateName, constraintName);
    00102         env->ReleaseStringUTFChars(designFile, designName);
    00103         env->ReleaseStringUTFChars(stateFile, stateName);
    00104         env->ReleaseStringUTFChars(constraintFile, constraintName);
    00105 }
    00106
    00107
    00108 JNIEXPORT void JNICALL
    00109 Java_Opsat_destroyOpsat (JNIEnv *env, jobject obj)
    00110 {
    00111         (void)env;
    00112         (void)obj;
    00113         if (dllOpsat)
    00114         {
    00115                 delete dllOpsat;
    00116                 dllOpsat = NULL;
    00117         }
    00118 }
    00119
    00120
    00121 bool
    00122 file_exist(char const * filename)
    00123 {
    00124         FILE *file;
    00125         if ( (file = fopen(filename,"r")) == NULL )
    00126                 return false;
    00127         fclose(file);
    00128         return true;
    00129 }
    00130
    00131
    00132 list<Variable *>
    00133 readVariables(char const * filename, bool useProb)
    00134 {
    00135         list<Variable *> res;
    00136
    00137         char next;
    00138         char tmp[400];
    00139
    00140         if (!file_exist(filename))
    00141         {
    00142                 //cout << "File " << filename << " does not exist." << endl;
    00143                 //exit(-1);
    00144                 return res;
    00145         }
    00146
    00147         ifstream in(filename);
    00148
    00149         // skip comment lines
    00150         while (!in.eof() && (next=in.peek()) == '#')
    00151                 in.getline(tmp,400);
    00152
    00153         if (in.eof())
    00154         {
    00155                 //cout << "Data file contains no variables. " << endl;
    00156                 return res;  // try anyway, for testing...
    00157         }
    00158
    00159         in >> ws;
    00160         while (!in.eof())
    00161         {
    00162                 in.getline(tmp,399);  // read variable
    00163                 in >> ws;
    00164                 if (strlen(tmp) == 0)
    00165                         continue;
    00166                 string tmp_s(tmp);
    00167                 istringstream line(tmp_s);
    00168                 char varname[400];
    00169                 line >> varname;
    00170                 line >> ws;
    00171                 list<string> values;
    00172                 list<double>  probs;
    00173                 while (!line.eof())
    00174                 {
    00175                         char val[400];
    00176                         double p;
    00177
    00178                         line >> val;
    00179                         //::cout << "   val: " << val << ", " ;
    00180                         line >> p;
    00181                         //::cout << "prob: " << p << endl;
    00182                         line >> ws;
    00183                         values.push_front(val);
    00185                         probs.push_front(p);
    00186                 }
    00187                 Variable * var = new Variable(varname, values, probs, useProb);
    00188                 //cout << "Read variable: " << *var << endl ;
    00189                 //::cout << "(num values: " << values.size() << ")" << endl;
    00190                 res.push_front(var);
    00192         }
    00193
    00194         in.close();
    00195
    00196         //cout << "Read file with " << (res.size()) << " variables." << endl;
    00197         //cout << endl;
    00198
    00199         return res;
    00200 }
    00201
    00202
    00203 list<Constraint const *>
    00204 readConstraints(char const * filename, list<Variable *> vars)
    00205 {
    00206         list<Constraint const *> res;
    00207
    00208         char next;
    00209         char tmp[400];
    00210
    00211         if (!file_exist(filename))
    00212         {
    00213                 //cout << "File " << filename << " does not exist." << endl;
    00214                 //exit(-1);
    00215                 return res;
    00216         }
    00217
    00218         ifstream in(filename);
    00219
    00220         // skip comment lines
    00221         while (!in.eof() && (next=in.peek()) == '#')
    00222                 in.getline(tmp,400);
    00223
    00224         in >> ws;
    00225         if (in.eof())
    00226         {
    00227                 //cout << "Data file contains no constraints." << endl;
    00228                 return res;  // try anyway, for testing...
    00229         }
    00230
    00231         while (!in.eof())
    00232         {
    00233                 in.getline(tmp,399);  // read constraint
    00234                 in >> ws;
    00235                 if (strlen(tmp) == 0)
    00236                         continue;
    00237                 string tmp_s(tmp);
    00238                 istringstream line(tmp_s);
    00239                 Constraint * constraint = new Constraint();
    00240                 while (!line.eof())
    00241                 {
    00242                         char   tmpChar;
    00243                         char   token[400];
    00244                         char   vala[400];
    00245                         char * val = vala;  // is this safe?
    00246                         bool   parity = true;
    00247                         line >> tmpChar;
    00248                         if (tmpChar == '!')
    00249                         {
    00250                                 parity = false;
    00251                                 line >> ws;
    00252                                 line >> tmpChar;
    00253                         }
    00254                         bool bracketOpened = false;  // Allow for either form
    00255                         if (tmpChar == '[')
    00256                         {
    00257                                 bracketOpened = true;
    00258                                 line >> ws;
    00259                                 line >> token;
    00260                         } else
    00261                         {
    00262                                 token[0] = tmpChar;
    00263                                 line >> (token+1);
    00264                         }
    00265                         for (unsigned int i = 0; i < sizeof(token); i++)
    00266                         {
    00267                                 char cur = token[i];
    00268                                 if (cur == '\0')  // end of string - assume whitespace separated.
    00269                                 {
    00270                                         line >> ws;
    00271                                         line >> tmpChar;
    00272                                         if (tmpChar != '=')
    00273                                         {
    00274                                                 //cout << "Error in reading from constraint file." << endl;
    00275                                                 //cout << "Choked on line: \"" << tmp << "\"" << endl;
    00276                                                 //exit(-1);
    00277                                                 return res;
    00278                                         }
    00279                                         line >> ws;
    00280                                         line >> vala;
    00281                                         val = vala;
    00282                                         if (val[strlen(val) - 1] == ']')  // closing bracket - always ignore?
    00283                                         {
    00284                                                 val[strlen(val) - 1] = '\0';
    00285                                         }
    00286                                         if (!(*val))  // no string left to find!
    00287                                         {
    00288                                                 //cout << "Error in reading from constraint file.." << endl;
    00289                                                 //exit(-1);
    00290                                                 return res;
    00291                                         }
    00292                                         break;
    00293                                 }
    00294
    00295                                 // whitespace handling below is not needed, since it can never occur...
    00296                                 if (cur == '=' || cur == ' ' || cur == '\t')
    00297                                 {
    00298                                         token[i] = '\0';
    00299                                         if (cur != '=')
    00300                                         {
    00301                                                 for (i++; i < sizeof(token); i++)
    00302                                                 {
    00303                                                         if (token[i] == '=')
    00304                                                                 break;
    00305                                                 }
    00306                                         }
    00307                                         for (i++; i < sizeof(token); i++)
    00308                                         {
    00309                                                 if (token[i] != ' ' && token[i] != '\t')
    00310                                                         break;
    00311                                         }
    00312                                         if (!(i < sizeof(token)))  // no string left to find!
    00313                                         {
    00314                                                 //cout << "Error in reading from constraint file..." << endl;
    00315                                                 //exit(-1);
    00316                                                 return res;
    00317                                         }
    00318                                         val = &(token[i]);
    00319                                         if (val[strlen(val) - 1] == ']')  // closing bracket - always ignore?
    00320                                         {
    00321                                                 val[strlen(val) - 1] = '\0';
    00322                                         }
    00323                                         if (!(*val))  // no string left to find!
    00324                                         {
    00325                                                 //cout << "Error in reading from constraint file...." << endl;
    00326                                                 //exit(-1);
    00327                                                 return res;
    00328                                         }
    00329                                         break;
    00330                                 }
    00331                         }
    00332                         line >> ws;
    00333
    00334                         // find the corresponding assignment:
    00335                         Assignment const * a = NULL;
    00336                         list<Variable *>::const_iterator variableIter;
    00337                         for (variableIter = vars.begin();
    00338                              variableIter != vars.end(); variableIter++)
    00339                         {
    00340                                 if ((*variableIter)->getNameString() == string(token))
    00341                                 {
    00342                                         a = (*variableIter)->getAssignmentByValue(string(val));
    00343                                         break;
    00344                                 }
    00345                         }
    00346                         if (a != NULL)
    00347                         {
    00348                                 constraint->addUnit(ConstraintUnit(a, parity));
    00349                         } else
    00350                         {
    00351                                 //cout << "    Error: could not find conflict assignment "
    00352                                 //     << token << ", " << val << "!!" << endl;
    00353                         }
    00354                 }
    00355                 //cout << "Read constraint: " << (*constraint) << endl ;
    00356                 res.push_front(constraint);
    00357         }
    00358
    00359         in.close();
    00360
    00361         //cout << "Read file with " << (res.size()) << " constraints." << endl;
    00362         //cout << endl;
    00363
    00364         return res;
    00365 }
    00366
    00367
    00368 int
    00369 main(int argc, char ** argv)
    00370 {
    00371         argc--;
    00372         argv++;
    00373
    00374         if (argc < 3 || argc > 4)
    00375         {
    00376                 /*#
    00377                 //cout << "Arguments should be:" << endl << endl;
    00378                 //cout << "   <design_var_file> <state_var_file> "
    00379                 //     << "<constraint_file> [<extra_constraint_file>] [-e][-d][-n]" << endl;
    00380                 //cout << endl;
    00381                 //cout << "<extra_constraint_file> does not need to be provided." << endl;
    00382                 //cout << endl;
    00383                 //cout << "-u   tries for UNSAT instead of SAT." << endl;
    00384                 //cout << "-e   uses an entropy-directed search method." << endl;
    00385                 //cout << "-d   uses DPLL in the SAT engine." << endl;
    00386                 //cout << "-p   treats costs as probabilities." << endl;
    00387                 //cout << "-n#  specifies the number to find (default is 1)." << endl;
    00388                 //cout << endl;
    00389                 */
    00390                 exit(-1);
    00391         }
    00392         cout << endl;
    00393
    00394         char const * designName = argv[0];
    00395         char const * stateName = argv[1];
    00396         char const * constraintName = argv[2];
    00397         dllOpsat = loadOpsat(designName, stateName, constraintName);
    00398         exit(0);
    00399         return 0;
    00400 }
    00401
    00402
    00403 Opsat *
    00404 loadOpsat(char const * designName, char const * stateName, char const * constraintName)
    00405 {
    00406         bool useCD = true;
    00407         bool useDPLL = false;
    00408         bool satisfy = true;
    00409         bool useProb = false;
    00410
    00411         //int numResults = 1;
    00412
    00413         char const * extraConstraintName = NULL;
    00414
    00415         list<Variable *> designVariables = readVariables(designName, useProb);
    00416         list<Variable *>  stateVariables = readVariables(stateName, useProb);
    00417         list<Variable *> allVariables(stateVariables);
    00418         list<Variable *>::const_iterator vIter;
    00419         for (vIter = designVariables.begin(); vIter != designVariables.end(); vIter++)
    00420         {
    00421                 allVariables.push_back((*vIter));
    00422         }
    00423         list<Constraint const *>   constraints = readConstraints(constraintName, allVariables);
    00424         list<Constraint const *>   extraConstraints;
    00425         if (extraConstraintName)
    00426                 extraConstraints = readConstraints(extraConstraintName, allVariables);
    00427
    00428         //float cutoff = 0.999F;
    00429         //int maxStatesTime = 2000000;
    00430         //int maxStatesSize = 1500000;
    00431
    00432
    00433         //cout << "Constructing opsat..." << endl;
    00434         Opsat * res = new Opsat(designVariables, stateVariables, constraints,
    00435                                 satisfy, useDPLL, useCD);
    00436         res->setDebug(false);
    00437         //cout << "Initial Opsat:" << endl << opsat << endl;
    00438
    00439         return res;
    00440 }
    00441
    00442 /*#
    00443 {
    00444         list<Implicant>  results;
    00445         list<Implicant>::const_iterator impIter;
    00446         if (extraConstraints.size() == 0)  // only one problem...
    00447         {
    00448                 results = opsat.findBest(numResults, maxStatesTime, maxStatesSize);
    00449
    00450                 cout << "Final Opsat:" << endl << opsat << endl;
    00451                 cout << "Implicants generated: " << endl;
    00452                 for (impIter = results.begin(); impIter != results.end(); impIter++)
    00453                 {
    00454                         cout << (*impIter) << endl ;
    00455                 }
    00456         } else
    00457         {
    00458                 list<Constraint const *>::const_iterator cIter;
    00459                 for (cIter = extraConstraints.begin(); cIter != extraConstraints.end(); cIter++)
    00460                 {
    00461                         cout << endl << endl
    00462                              << "Trying with  constraint: " << *(*cIter) << endl << endl;
    00463                         opsat.setTemporaryConstraint((*cIter));
    00464                         results = opsat.findBest(numResults, maxStatesTime, maxStatesSize);
    00465
    00466                         cout << "Final Opsat:" << endl << opsat << endl;
    00467                         cout << "Implicants generated: " << endl;
    00468                         for (impIter = results.begin(); impIter != results.end(); impIter++)
    00469                         {
    00470                                 cout << (*impIter) << endl ;
    00471                         }
    00472                 }
    00473         }
    00474
    00475         exit(0);
    00476         return 0; //# to make MSVC happy - yes, it's that stupid.
    00477 }
    00478 */
    00479