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

# /Users/fpy/titan-1-5-MBARI/Mers/Solvers/SAT/ISAT/VSAT_test.cpp

    00001 //==============================================================================
    00002 // Copyright (c) 2001           Model-based Embedded and Robotic Systems Group
    00003 // All Rights Reserved          Massachusetts Institute of Technology
    00004 //
    00005 // This software is provided as is. Model-based Embedded and Robotic Systems
    00006 // (MERS) group does not assume any responsibility.
    00007 //==============================================================================
    00008 //# CHECKED MJP 08-07-2002
    00009
    00010 #ifdef _MSC_VER
    00011 #pragma warning( disable : 4786 )
    00012 #endif
    00013
    00014 #include <cstdlib>
    00015 #include <cstdio>
    00016 #include <iostream>
    00017 #include <fstream>
    00018 #include <string>
    00019 #include <cmath>
    00020 //#include <ctime>
    00021 #include <list>
    00022 #include <sstream>
    00023
    00024 #include "VSAT.h"
    00025 //#include "Osat.h"
    00026 #include "../bfig/Constraint.h"
    00027 #include "../bfig/Implicant.h"
    00028 #include "../bfig/Variable.h"
    00029 #include "../bfig/Assignment.h"
    00030
    00031 using namespace std;
    00032
    00033 bool                      file_exist(char* filename);
    00034 list<Variable const *>    readVariables(char const * filename);
    00035 list<Constraint const *>  readConstraints(char const * filename,
    00036                                            list<Variable const *> const & vars);
    00037 list<Implicant const *>   readImplicants(char const * filename,
    00038                                          list<Variable const *> const & variables);
    00039
    00040 list<Variable *>          readVariablesUnconst(char const * filename);
    00041 list<Constraint const *>  readConstraints(char const * filename,
    00042                                            list<Variable *> const & vars);
    00043 list<Implicant const *>   readImplicants(char const * filename,
    00044                                          list<Variable *> const & variables);
    00045 void                      loadDIMACS(char const * fileName,
    00046                                      list<Variable *> * vars,
    00047                                      list<Constraint const *> * clauses);
    00048
    00049
    00050
    00051 void
    00052 loadDIMACS(char const * fileName,
    00053            list<Variable *> * vars, list<Constraint const *> * clauses)
    00054 {
    00055         /*
    00056                 This method reads a SAT Ascii file with the format described in the DIMACS challenge
    00057                 ftp://dimacs.rutgers.edu/pub/challenge/satisfiability/doc/satformat.dvi
    00058                 Only the CNF format is supported.
    00059         */
    00060         string inputLine;
    00061         int inputValue = 0;
    00062         int counter = 0;
    00063
    00064         int numPropositions;
    00065         int numClauses;
    00066
    00067         // Open the Input File
    00068         ifstream satFile(fileName);
    00069
    00070         // Make sure the File Exists
    00071         if (satFile.bad()) {
    00072                 cout << "Error: Couldn't open SAT File '" << fileName << "'." << endl;
    00073                 return;
    00074         }
    00075
    00076         // Skip Comment Lines: c Comments
    00077         while (satFile.peek() == 'c' && !satFile.eof())
    00078         {
    00079                 getline(satFile, inputLine);
    00080         }
    00081
    00082         // Read in Problem Line: p FORMAT VARIABLES CLAUSES
    00083         if (satFile.peek() == 'p')
    00084         {
    00085                 // Skip p
    00086                 satFile >> inputLine;
    00087
    00088                 // Read FORMAT
    00089                 satFile >> inputLine;
    00090                 if (inputLine != "cnf")
    00091                 {
    00092                         cout << "Error: Only CNF format files supported." << endl;
    00093                         return;
    00094                 }
    00095
    00096                 // Read VARIABLES
    00097                 satFile >> numPropositions;
    00098
    00099                 // Read CLAUSES
    00100                 satFile >> numClauses;
    00101         }
    00102
    00103         // Verify that Clauses and Propositions are Within Range
    00104         //if (numClauses > MAX_CLAUSES)
    00105         //{
    00106         //      cout << "Error: Number of clauses exceeds maximum allowed." << endl;
    00107         //      return;
    00108         //} else
    00109         if (numClauses < 0)
    00110         {
    00111                 cout << "Error: Number of clauses must be non-negative." << endl;
    00112                 return;
    00113         }
    00114         //if (numPropositions > MAX_PROPOSITIONS)
    00115         //{
    00116         //      cout << "Error: Number of propositions exceeds maximum allowed." << endl;
    00117         //      return;
    00118         //} else
    00119         if (numPropositions < 0)
    00120         {
    00121                 cout << "Error: Number of propositions must be non-negative." << endl;
    00122                 return;
    00123         }
    00124
    00125         // constant lists:
    00126         list<unsigned int> vals;
    00127         vals.push_back(0); vals.push_back(1);
    00128         list<double> costs;
    00129         costs.push_back(0.0); costs.push_back(0.0);
    00130
    00131         // list of resulting clauses:
    00132         //list<Constraint const *> clauses;
    00133         //list<Variable *> vars;
    00134
    00135         // Create a Clause
    00136         Constraint * newClause = NULL;
    00137
    00138         // Read in All Clauses
    00139         while (!satFile.eof() && counter < numClauses)
    00140         {
    00141                 // Read in a Literal
    00142                 satFile >> inputValue;
    00143
    00144                 // Check if Literal signals end of the Clause
    00145                 if (inputValue == 0)
    00146                 {
    00147                         // End of Clause, so Add Clause to Theory
    00148                         clauses->push_back(newClause);
    00149                         counter++;
    00150
    00151                         newClause = NULL;
    00152                 } else
    00153                 {
    00154                         if (!newClause)
    00155                                 newClause = new Constraint();
    00156                         // Create New Literal and Add it to the Clause
    00157                         bool parity = (inputValue > 0);
    00158                         if (inputValue < 0)
    00159                                 inputValue = -inputValue;
    00160
    00161                         // find variable, assignment
    00162                         Variable * var = NULL;
    00163                         list<Variable *>::iterator vIter;
    00164                         for (vIter = vars->begin(); vIter != vars->end(); vIter++)
    00165                         {
    00166                                 if ((*vIter)->getName() == (unsigned int)inputValue)
    00167                                 {
    00168                                         var = (*vIter);
    00169                                         break;
    00170                                 }
    00171                                 if ((*vIter)->getName() > (unsigned int)inputValue)
    00172                                 {
    00173                                         var = new Variable((unsigned int)inputValue, vals, costs);
    00174                                         vars->insert(vIter, var);
    00175                                         break;
    00176                                 }
    00177                         }
    00178                         if (!var)
    00179                         {
    00180                                 var = new Variable((unsigned int)inputValue, vals, costs);
    00181                                 vars->push_back(var);
    00182                         }
    00183
    00184                         Assignment const * assign = var->getAssignmentByValue(1);
    00185                         newClause->addUnit(ConstraintUnit(assign, parity));
    00187                         //Assignment const * assign = var->getAssignmentByValue(parity ? 1 : 0);
    00188                         //newClause->addUnit(ConstraintUnit(assign, true));
    00189                 }
    00190
    00191                 // This code prints out the Progress of Loading the File
    00192                 if ((counter % 1000) == 0)
    00193                 {
    00194                         if (counter == 0)
    00195                         {
    00196                                 //cout << "Reading file " << fileName << " with " << numPropositions
    00197                                 //      << " propositions and " << numClauses << " clauses... " << endl;
    00198                         } else
    00199                         {
    00200                                 cout << (int)(100.0*counter/(double)(numClauses)) << "%" << endl;
    00201                         }
    00202                 }
    00203         }
    00204
    00205         cout << "Reading file " << fileName << " with " << numPropositions
    00206                 << " propositions and " << numClauses << " clauses... Done." << endl;
    00207
    00208         satFile.close();
    00209
    00210         return;
    00211 }
    00212
    00213
    00214
    00215 bool
    00216 file_exist(char const * filename)
    00217 {
    00218         FILE *file;
    00219         if ( (file = fopen(filename,"r")) == NULL )
    00220                 return false;
    00221         fclose(file);
    00222         return true;
    00223 }
    00224
    00225
    00226 list<Variable const *>
    00227 readVariables(char const * filename)
    00228 {
    00229         list<Variable const *> res;
    00230
    00231         char next;
    00232         char tmp[400];
    00233
    00234         if (!file_exist(filename))
    00235         {
    00236                 cout << "File " << filename << " does not exist." << endl;
    00237                 exit(-1);
    00238         }
    00239
    00240         ifstream in(filename);
    00241
    00242         // skip comment lines
    00243         while (!in.eof() && (next=in.peek()) == '#')
    00244                 in.getline(tmp,400);
    00245
    00246         if (in.eof())
    00247         {
    00248                 cout << "(Data file contains no variables.)" << endl;
    00249                 return res;  // try anyway, for testing...
    00250         }
    00251
    00252         in >> ws;
    00253         while (!in.eof())
    00254         {
    00255                 if (in.peek() == ';')
    00256                 {
    00257                         in.ignore(399, '\n');  // skip comment
    00258                         in >> ws;
    00259                         continue;
    00260                 }
    00261                 in.getline(tmp,399);  // read variable
    00262                 in >> ws;
    00263                 if (strlen(tmp) == 0)
    00264                         continue;
    00265                 string tmp_s(tmp);
    00266                 istringstream line(tmp_s);
    00267                 char varname[400];
    00268                 line >> varname;
    00269                 line >> ws;
    00270                 list<string> vals;
    00271                 list<double>  probs;
    00272                 while (!line.eof())
    00273                 {
    00274                         char val[400];
    00275                         double p;
    00276
    00277                         line >> val;
    00278                         //::cout << "   val: " << val << ", " ;
    00279                         line >> p;
    00280                         //::cout << "prob: " << p << endl;
    00281                         line >> ws;
    00282                         vals.push_back(val);
    00284                         probs.push_back(p);
    00285                 }
    00286                 Variable * var = new Variable(varname, vals, probs);
    00287                 cout << "Read variable: " << *var << endl ;
    00288                 //::cout << "(num values: " << values.size() << ")" << endl;
    00289                 res.push_back(var);
    00291         }
    00292
    00293         in.close();
    00294
    00295         cout << "Read file with " << (res.size()) << " variables." << endl;
    00296         cout << endl;
    00297
    00298         return res;
    00299 }
    00300
    00301
    00302 list<Variable *>
    00303 readVariablesUnconst(char const * filename)
    00304 {
    00305         list<Variable *> res;
    00306
    00307         char next;
    00308         char tmp[400];
    00309
    00310         if (!file_exist(filename))
    00311         {
    00312                 cout << "File " << filename << " does not exist." << endl;
    00313                 exit(-1);
    00314         }
    00315
    00316         ifstream in(filename);
    00317
    00318         // skip comment lines
    00319         while (!in.eof() && (next=in.peek()) == '#')
    00320                 in.getline(tmp,400);
    00321
    00322         if (in.eof())
    00323         {
    00324                 cout << "(Data file contains no variables.)" << endl;
    00325                 return res;  // try anyway, for testing...
    00326         }
    00327
    00328         in >> ws;
    00329         while (!in.eof())
    00330         {
    00331                 if (in.peek() == ';')
    00332                 {
    00333                         in.ignore(399, '\n');  // skip comment
    00334                         in >> ws;
    00335                         continue;
    00336                 }
    00337                 in.getline(tmp,399);  // read variable
    00338                 in >> ws;
    00339                 if (strlen(tmp) == 0)
    00340                         continue;
    00341                 string tmp_s(tmp);
    00342                 istringstream line(tmp_s);
    00343                 char varname[400];
    00344                 line >> varname;
    00345                 line >> ws;
    00346                 list<string> vals;
    00347                 list<double>  probs;
    00348                 while (!line.eof())
    00349                 {
    00350                         char val[400];
    00351                         double p;
    00352
    00353                         line >> val;
    00354                         //::cout << "   val: " << val << ", " ;
    00355                         line >> p;
    00356                         //::cout << "prob: " << p << endl;
    00357                         line >> ws;
    00358                         vals.push_back(val);
    00360                         probs.push_back(p);
    00361                 }
    00362                 Variable * var = new Variable(varname, vals, probs);
    00363                 cout << "Read variable: " << *var << endl ;
    00364                 //::cout << "(num values: " << values.size() << ")" << endl;
    00365                 res.push_back(var);
    00367         }
    00368
    00369         in.close();
    00370
    00371         cout << "Read file with " << (res.size()) << " variables." << endl;
    00372         cout << endl;
    00373
    00374         return res;
    00375 }
    00376
    00377
    00378 list<Constraint const *>
    00379 readConstraints(char const * filename, list<Variable const *> const & vars)
    00380 {
    00381         list<Constraint const *> res;
    00382
    00383         char next;
    00384         char tmp[400];
    00385
    00386         if (!file_exist(filename))
    00387         {
    00388                 cout << "File " << filename << " does not exist." << endl;
    00389                 exit(-1);
    00390         }
    00391
    00392         ifstream in(filename);
    00393
    00394         // skip comment lines
    00395         while (!in.eof() && (next=in.peek()) == '#')
    00396                 in.getline(tmp,400);
    00397
    00398         in >> ws;
    00399         if (in.eof())
    00400         {
    00401                 cout << "Data file contains no constraints." << endl;
    00402                 return res;  // try anyway, for testing...
    00403         }
    00404
    00405         while (!in.eof())
    00406         {
    00407                 in.getline(tmp,399);  // read constraint
    00408                 in >> ws;
    00409                 if (strlen(tmp) == 0)
    00410                         continue;
    00411                 string tmp_s(tmp);
    00412                 istringstream line(tmp_s);
    00413                 Constraint * constraint = new Constraint();
    00414                 while (!line.eof())
    00415                 {
    00416                         char   tmpChar;
    00417                         char   token[400];
    00418                         char   vala[400];
    00419                         char * val = vala;  // is this safe?
    00420                         bool   parity = true;
    00421                         line >> tmpChar;
    00422                         if (tmpChar == '!')
    00423                         {
    00424                                 parity = false;
    00425                                 line >> ws;
    00426                                 line >> tmpChar;
    00427                         }
    00428                         bool bracketOpened = false;  // Allow for either form
    00429                         if (tmpChar == '[')
    00430                         {
    00431                                 bracketOpened = true;
    00432                                 line >> ws;
    00433                                 line >> token;
    00434                         } else
    00435                         {
    00436                                 token[0] = tmpChar;
    00437                                 line >> (token+1);
    00438                         }
    00439                         for (unsigned int i = 0; i < sizeof(token); i++)
    00440                         {
    00441                                 char cur = token[i];
    00442                                 if (cur == '\0')  // end of string - assume whitespace separated.
    00443                                 {
    00444                                         line >> ws;
    00445                                         line >> tmpChar;
    00446                                         if (tmpChar != '=')
    00447                                         {
    00448                                                 cout << "Error in reading from constraint file." << endl;
    00449                                                 cout << "Choked on line: \"" << tmp << "\"" << endl;
    00450                                                 exit(-1);
    00451                                         }
    00452                                         line >> ws;
    00453                                         line >> vala;
    00454                                         val = vala;
    00455                                         if (val[strlen(val) - 1] == ']')  // closing bracket - always ignore?
    00456                                         {
    00457                                                 val[strlen(val) - 1] = '\0';
    00458                                         }
    00459                                         if (!(*val))  // no string left to find!
    00460                                         {
    00461                                                 cout << "Error in reading from constraint file.." << endl;
    00462                                                 exit(-1);
    00463                                         }
    00464                                         break;
    00465                                 }
    00466
    00467                                 // whitespace handling below is not needed, since it can never occur...
    00468                                 if (cur == '=' || cur == ' ' || cur == '\t')
    00469                                 {
    00470                                         token[i] = '\0';
    00471                                         if (cur != '=')
    00472                                         {
    00473                                                 for (i++; i < sizeof(token); i++)
    00474                                                 {
    00475                                                         if (token[i] == '=')
    00476                                                                 break;
    00477                                                 }
    00478                                         }
    00479                                         for (i++; i < sizeof(token); i++)
    00480                                         {
    00481                                                 if (token[i] != ' ' && token[i] != '\t')
    00482                                                         break;
    00483                                         }
    00484                                         if (!(i < sizeof(token)))  // no string left to find!
    00485                                         {
    00486                                                 cout << "Error in reading from constraint file..." << endl;
    00487                                                 exit(-1);
    00488                                         }
    00489                                         val = &(token[i]);
    00490                                         if (val[strlen(val) - 1] == ']')  // closing bracket - always ignore?
    00491                                         {
    00492                                                 val[strlen(val) - 1] = '\0';
    00493                                         }
    00494                                         if (!(*val))  // no string left to find!
    00495                                         {
    00496                                                 cout << "Error in reading from constraint file...." << endl;
    00497                                                 exit(-1);
    00498                                         }
    00499                                         break;
    00500                                 }
    00501                         }
    00502                         line >> ws;
    00503
    00504                         // find the corresponding assignment:
    00505                         Assignment const * a = NULL;
    00506                         list<Variable const *>::const_iterator variableIter;
    00507                         for (variableIter = vars.begin();
    00508                              variableIter != vars.end(); variableIter++)
    00509                         {
    00510                                 if ((*variableIter)->getNameString() == string(token))
    00511                                 {
    00512                                         a = (*variableIter)->getAssignmentByValue(string(val));
    00513                                         break;
    00514                                 }
    00515                         }
    00516                         if (a != NULL)
    00517                         {
    00518                                 constraint->addUnit(a, parity);
    00519                         } else
    00520                         {
    00521                                 cout << "    Error: could not find conflict assignment "
    00522                                      << token << ", " << val << "!!" << endl;
    00523                         }
    00524                 }
    00525                 cout << "Read constraint: " << (*constraint) << endl ;
    00526                 res.push_back(constraint);
    00527         }
    00528
    00529         in.close();
    00530
    00531         cout << "Read file with " << (res.size()) << " constraints." << endl;
    00532         cout << endl;
    00533
    00534         return res;
    00535 }
    00536
    00537
    00538 list<Implicant const *>
    00539 readImplicants(char const * filename, list<Variable const *> const & vars)
    00540 {
    00541         list<Implicant const *> res;
    00542
    00543         char next;
    00544         char tmp[400];
    00545
    00546         if (!file_exist(filename))
    00547         {
    00548                 cout << "File " << filename << " does not exist." << endl;
    00549                 exit(-1);
    00550         }
    00551
    00552         ifstream in(filename);
    00553
    00554         // skip comment lines
    00555         while (!in.eof() && (next=in.peek()) == '#')
    00556                 in.getline(tmp,400);
    00557
    00558         in >> ws;
    00559         if (in.eof())
    00560         {
    00561                 cout << "(Data file contains no implicants.)" << endl;
    00562                 return res;  // try anyway, for testing...
    00563         }
    00564
    00565         while (!in.eof())
    00566         {
    00567                 if (in.peek() == ';')
    00568                 {
    00569                         in.ignore(399, '\n');  // skip comment
    00570                         in >> ws;
    00571                         continue;
    00572                 }
    00573                 in.getline(tmp,399);  // read constraint
    00574                 in >> ws;
    00575                 if (strlen(tmp) == 0)
    00576                         continue;
    00577                 string tmp_s(tmp);
    00578                 istringstream line(tmp_s);
    00579                 list<Assignment const *> assigns;
    00580                 while (!line.eof())
    00581                 {
    00582                         char   tmpChar;
    00583                         char   token[400];
    00584                         char   vala[400];
    00585                         char * val = NULL;
    00586                         if (line.peek() == '[')  // allow for bracketed assignments
    00587                         {
    00588                                 line.ignore(1);
    00589                                 line >> ws;
    00590                         }
    00591                         line >> token;
    00592                         for (unsigned int i = 0; i < sizeof(token); i++)
    00593                         {
    00594                                 char cur = token[i];
    00595                                 if (cur == '\0')  // end of string - assume whitespace separated.
    00596                                 {
    00597                                         line >> ws;
    00598                                         line >> tmpChar;
    00599                                         if (tmpChar != '=')
    00600                                         {
    00601                                                 cout << "Error in reading from implicant file." << endl;
    00602                                                 cout << "Choked on line: \"" << tmp << "\"" << endl;
    00603                                                 exit(-1);
    00604                                         }
    00605                                         line >> ws;
    00606                                         line >> vala;
    00607                                         val = vala;
    00608                                         if (val[strlen(val) - 1] == ']')  // closing bracket - always ignore?
    00609                                         {
    00610                                                 val[strlen(val) - 1] = '\0';
    00611                                         }
    00612                                         if (!(*val))  // no string left to find!
    00613                                         {
    00614                                                 cout << "Error in reading from implicant file.." << endl;
    00615                                                 exit(-1);
    00616                                         }
    00617                                         break;
    00618                                 }
    00619
    00620                                 // whitespace handling below is not needed, since it can never occur...
    00621                                 if (cur == '=' || cur == ' ' || cur == '\t')
    00622                                 {
    00623                                         token[i] = '\0';
    00624                                         if (cur != '=')
    00625                                         {
    00626                                                 for (i++; i < sizeof(token); i++)
    00627                                                 {
    00628                                                         if (token[i] == '=')
    00629                                                                 break;
    00630                                                 }
    00631                                         }
    00632                                         for (i++; i < sizeof(token); i++)
    00633                                         {
    00634                                                 if (token[i] != ' ' && token[i] != '\t')
    00635                                                         break;
    00636                                         }
    00637                                         if (!(i < sizeof(token)))  // no string left to find!
    00638                                         {
    00639                                                 cout << "Error in reading from implicant file..." << endl;
    00640                                                 exit(-1);
    00641                                         }
    00642                                         val = &(token[i]);
    00643                                         if (val[strlen(val) - 1] == ']')  // closing bracket - always ignore?
    00644                                         {
    00645                                                 val[strlen(val) - 1] = '\0';
    00646                                         }
    00647                                         if (!(*val))  // no string left to find!
    00648                                         {
    00649                                                 cout << "Error in reading from implicant file...." << endl;
    00650                                                 exit(-1);
    00651                                         }
    00652                                         break;
    00653                                 }
    00654                         }
    00655                         line >> ws;
    00656                         // locate assignment:
    00657                         list<Variable const *>::const_iterator varIter;
    00658                         Variable const * match = NULL;
    00659                         for (varIter = vars.begin(); varIter != vars.end(); varIter++)
    00660                         {
    00661                                 if ((*varIter)->getNameString() == string(token))
    00662                                 {
    00663                                         match = *varIter;
    00664                                         break;
    00665                                 }
    00666                         }
    00667                         if (match == NULL)
    00668                         {
    00669                                 cout << "Error in implicant file: Variable '" << string(token)
    00670                                      << "' not found." << endl;
    00671                                 exit(-1);
    00672                         }
    00673                         Assignment const * matchAssignment = match->getAssignmentByValue(string(val));
    00674                         if (matchAssignment == NULL)
    00675                         {
    00676                                 cout << "Error in implicant file: Value '" << string(val)
    00677                                      << "' not found for variable '" << string(token) << "'." << endl;
    00678                                 exit(-1);
    00679                         }
    00680                         assigns.push_back(matchAssignment);
    00681                 }
    00682                 Implicant const * newImplicant = new Implicant(assigns);
    00683                 cout << "Read implicant: " << (*newImplicant) << endl ;
    00684                 res.push_back(newImplicant);
    00685         }
    00686
    00687         in.close();
    00688
    00689         cout << "Read file with " << (res.size()) << " implicants." << endl;
    00690         cout << endl;
    00691
    00692         return res;
    00693 }
    00694
    00695
    00696 list<Constraint const *>
    00697 readConstraints(char const * filename, list<Variable *> const & vars)
    00698 {
    00699         list<Constraint const *> res;
    00700
    00701         char next;
    00702         char tmp[400];
    00703
    00704         if (!file_exist(filename))
    00705         {
    00706                 cout << "File " << filename << " does not exist." << endl;
    00707                 exit(-1);
    00708         }
    00709
    00710         ifstream in(filename);
    00711
    00712         // skip comment lines
    00713         while (!in.eof() && (next=in.peek()) == '#')
    00714                 in.getline(tmp,400);
    00715
    00716         in >> ws;
    00717         if (in.eof())
    00718         {
    00719                 cout << "Data file contains no constraints." << endl;
    00720                 return res;  // try anyway, for testing...
    00721         }
    00722
    00723         while (!in.eof())
    00724         {
    00725                 in.getline(tmp,399);  // read constraint
    00726                 in >> ws;
    00727                 if (strlen(tmp) == 0)
    00728                         continue;
    00729                 string tmp_s(tmp);
    00730                 istringstream line(tmp_s);
    00731                 Constraint * constraint = new Constraint();
    00732                 while (!line.eof())
    00733                 {
    00734                         char   tmpChar;
    00735                         char   token[400];
    00736                         char   vala[400];
    00737                         char * val = vala;  // is this safe?
    00738                         bool   parity = true;
    00739                         line >> tmpChar;
    00740                         if (tmpChar == '!')
    00741                         {
    00742                                 parity = false;
    00743                                 line >> ws;
    00744                                 line >> tmpChar;
    00745                         }
    00746                         bool bracketOpened = false;  // Allow for either form
    00747                         if (tmpChar == '[')
    00748                         {
    00749                                 bracketOpened = true;
    00750                                 line >> ws;
    00751                                 line >> token;
    00752                         } else
    00753                         {
    00754                                 token[0] = tmpChar;
    00755                                 line >> (token+1);
    00756                         }
    00757                         for (unsigned int i = 0; i < sizeof(token); i++)
    00758                         {
    00759                                 char cur = token[i];
    00760                                 if (cur == '\0')  // end of string - assume whitespace separated.
    00761                                 {
    00762                                         line >> ws;
    00763                                         line >> tmpChar;
    00764                                         if (tmpChar != '=')
    00765                                         {
    00766                                                 cout << "Error in reading from constraint file." << endl;
    00767                                                 cout << "Choked on line: \"" << tmp << "\"" << endl;
    00768                                                 exit(-1);
    00769                                         }
    00770                                         line >> ws;
    00771                                         line >> vala;
    00772                                         val = vala;
    00773                                         if (val[strlen(val) - 1] == ']')  // closing bracket - always ignore?
    00774                                         {
    00775                                                 val[strlen(val) - 1] = '\0';
    00776                                         }
    00777                                         if (!(*val))  // no string left to find!
    00778                                         {
    00779                                                 cout << "Error in reading from constraint file.." << endl;
    00780                                                 exit(-1);
    00781                                         }
    00782                                         break;
    00783                                 }
    00784
    00785                                 // whitespace handling below is not needed, since it can never occur...
    00786                                 if (cur == '=' || cur == ' ' || cur == '\t')
    00787                                 {
    00788                                         token[i] = '\0';
    00789                                         if (cur != '=')
    00790                                         {
    00791                                                 for (i++; i < sizeof(token); i++)
    00792                                                 {
    00793                                                         if (token[i] == '=')
    00794                                                                 break;
    00795                                                 }
    00796                                         }
    00797                                         for (i++; i < sizeof(token); i++)
    00798                                         {
    00799                                                 if (token[i] != ' ' && token[i] != '\t')
    00800                                                         break;
    00801                                         }
    00802                                         if (!(i < sizeof(token)))  // no string left to find!
    00803                                         {
    00804                                                 cout << "Error in reading from constraint file..." << endl;
    00805                                                 exit(-1);
    00806                                         }
    00807                                         val = &(token[i]);
    00808                                         if (val[strlen(val) - 1] == ']')  // closing bracket - always ignore?
    00809                                         {
    00810                                                 val[strlen(val) - 1] = '\0';
    00811                                         }
    00812                                         if (!(*val))  // no string left to find!
    00813                                         {
    00814                                                 cout << "Error in reading from constraint file...." << endl;
    00815                                                 exit(-1);
    00816                                         }
    00817                                         break;
    00818                                 }
    00819                         }
    00820                         line >> ws;
    00821
    00822                         // find the corresponding assignment:
    00823                         Assignment const * a = NULL;
    00824                         list<Variable *>::const_iterator variableIter;
    00825                         for (variableIter = vars.begin();
    00826                              variableIter != vars.end(); variableIter++)
    00827                         {
    00828                                 if ((*variableIter)->getNameString() == string(token))
    00829                                 {
    00830                                         a = (*variableIter)->getAssignmentByValue(string(val));
    00831                                         break;
    00832                                 }
    00833                         }
    00834                         if (a != NULL)
    00835                         {
    00836                                 constraint->addUnit(a, parity);
    00837                         } else
    00838                         {
    00839                                 cout << "    Error: could not find conflict assignment "
    00840                                      << token << ", " << val << "!!" << endl;
    00841                         }
    00842                 }
    00843                 cout << "Read constraint: " << (*constraint) << endl ;
    00844                 res.push_back(constraint);
    00845         }
    00846
    00847         in.close();
    00848
    00849         cout << "Read file with " << (res.size()) << " constraints." << endl;
    00850         cout << endl;
    00851
    00852         return res;
    00853 }
    00854
    00855
    00856 list<Implicant const *>
    00857 readImplicants(char const * filename, list<Variable *> const & vars)
    00858 {
    00859         list<Implicant const *> res;
    00860
    00861         char next;
    00862         char tmp[400];
    00863
    00864         if (!file_exist(filename))
    00865         {
    00866                 cout << "File " << filename << " does not exist." << endl;
    00867                 exit(-1);
    00868         }
    00869
    00870         ifstream in(filename);
    00871
    00872         // skip comment lines
    00873         while (!in.eof() && (next=in.peek()) == '#')
    00874                 in.getline(tmp,400);
    00875
    00876         in >> ws;
    00877         if (in.eof())
    00878         {
    00879                 cout << "(Data file contains no implicants.)" << endl;
    00880                 return res;  // try anyway, for testing...
    00881         }
    00882
    00883         while (!in.eof())
    00884         {
    00885                 if (in.peek() == ';')
    00886                 {
    00887                         in.ignore(399, '\n');  // skip comment
    00888                         in >> ws;
    00889                         continue;
    00890                 }
    00891                 in.getline(tmp,399);  // read constraint
    00892                 in >> ws;
    00893                 if (strlen(tmp) == 0)
    00894                         continue;
    00895                 string tmp_s(tmp);
    00896                 istringstream line(tmp_s);
    00897                 list<Assignment const *> assigns;
    00898                 while (!line.eof())
    00899                 {
    00900                         char   tmpChar;
    00901                         char   token[400];
    00902                         char   vala[400];
    00903                         char * val = NULL;
    00904                         if (line.peek() == '[')  // allow for bracketed assignments
    00905                         {
    00906                                 line.ignore(1);
    00907                                 line >> ws;
    00908                         }
    00909                         line >> token;
    00910                         for (unsigned int i = 0; i < sizeof(token); i++)
    00911                         {
    00912                                 char cur = token[i];
    00913                                 if (cur == '\0')  // end of string - assume whitespace separated.
    00914                                 {
    00915                                         line >> ws;
    00916                                         line >> tmpChar;
    00917                                         if (tmpChar != '=')
    00918                                         {
    00919                                                 cout << "Error in reading from implicant file." << endl;
    00920                                                 cout << "Choked on line: \"" << tmp << "\"" << endl;
    00921                                                 exit(-1);
    00922                                         }
    00923                                         line >> ws;
    00924                                         line >> vala;
    00925                                         val = vala;
    00926                                         if (val[strlen(val) - 1] == ']')  // closing bracket - always ignore?
    00927                                         {
    00928                                                 val[strlen(val) - 1] = '\0';
    00929                                         }
    00930                                         if (!(*val))  // no string left to find!
    00931                                         {
    00932                                                 cout << "Error in reading from implicant file.." << endl;
    00933                                                 exit(-1);
    00934                                         }
    00935                                         break;
    00936                                 }
    00937
    00938                                 // whitespace handling below is not needed, since it can never occur...
    00939                                 if (cur == '=' || cur == ' ' || cur == '\t')
    00940                                 {
    00941                                         token[i] = '\0';
    00942                                         if (cur != '=')
    00943                                         {
    00944                                                 for (i++; i < sizeof(token); i++)
    00945                                                 {
    00946                                                         if (token[i] == '=')
    00947                                                                 break;
    00948                                                 }
    00949                                         }
    00950                                         for (i++; i < sizeof(token); i++)
    00951                                         {
    00952                                                 if (token[i] != ' ' && token[i] != '\t')
    00953                                                         break;
    00954                                         }
    00955                                         if (!(i < sizeof(token)))  // no string left to find!
    00956                                         {
    00957                                                 cout << "Error in reading from implicant file..." << endl;
    00958                                                 exit(-1);
    00959                                         }
    00960                                         val = &(token[i]);
    00961                                         if (val[strlen(val) - 1] == ']')  // closing bracket - always ignore?
    00962                                         {
    00963                                                 val[strlen(val) - 1] = '\0';
    00964                                         }
    00965                                         if (!(*val))  // no string left to find!
    00966                                         {
    00967                                                 cout << "Error in reading from implicant file...." << endl;
    00968                                                 exit(-1);
    00969                                         }
    00970                                         break;
    00971                                 }
    00972                         }
    00973                         line >> ws;
    00974                         // locate assignment:
    00975                         list<Variable *>::const_iterator varIter;
    00976                         Variable const * match = NULL;
    00977                         for (varIter = vars.begin(); varIter != vars.end(); varIter++)
    00978                         {
    00979                                 if ((*varIter)->getNameString() == string(token))
    00980                                 {
    00981                                         match = *varIter;
    00982                                         break;
    00983                                 }
    00984                         }
    00985                         if (match == NULL)
    00986                         {
    00987                                 cout << "Error in implicant file: Variable '" << string(token)
    00988                                      << "' not found." << endl;
    00989                                 exit(-1);
    00990                         }
    00991                         Assignment const * matchAssignment = match->getAssignmentByValue(string(val));
    00992                         if (matchAssignment == NULL)
    00993                         {
    00994                                 cout << "Error in implicant file: Value '" << string(val)
    00995                                      << "' not found for variable '" << string(token) << "'." << endl;
    00996                                 exit(-1);
    00997                         }
    00998                         assigns.push_back(matchAssignment);
    00999                 }
    01000                 Implicant const * newImplicant = new Implicant(assigns);
    01001                 cout << "Read implicant: " << (*newImplicant) << endl ;
    01002                 res.push_back(newImplicant);
    01003         }
    01004
    01005         in.close();
    01006
    01007         cout << "Read file with " << (res.size()) << " implicants." << endl;
    01008         cout << endl;
    01009
    01010         return res;
    01011 }
    01012
    01013
    01014 int
    01015 main(int argc, char** argv)
    01016 {
    01017         argc--;
    01018         argv++;
    01019
    01020         bool satisfy = true;
    01021         bool useDPLL = false;
    01022         //bool useOsat = false;
    01023         bool debug = false;
    01024         char const * candidateFile = NULL;  // don't test one, by default
    01025         for (; argc > 1 && argv[argc-1][0] == '-'; argc--)
    01026         {
    01027                 if (argv[argc-1][1] == 'd' || argv[argc-1][1] == 'D')
    01028                 {
    01029                         cout << "Using DPLL in SAT." << endl;
    01030                         useDPLL = true;
    01031                 } else
    01032                 if (argv[argc-1][1] == 'c' || argv[argc-1][1] == 'C')
    01033                 {
    01034                         candidateFile = argv[argc-1]+2;
    01035                         cout << "Testing candidates from file '" << candidateFile << "'." << endl;
    01036                 } else
    01037                 if (argv[argc-1][1] == 'u' || argv[argc-1][1] == 'U')
    01038                 {
    01039                         cout << "Trying for UNSAT problem instead of SAT." << endl;
    01040                         satisfy = false;
    01041                 } else
    01042                 //if (argv[argc-1][1] == 'o' || argv[argc-1][1] == 'O')
    01043                 //{
    01044                 //      cout << "Using Osat for engine instead of VSAT." << endl;
    01045                 //      useOsat = true;
    01046                 //} else
    01047                 if (argv[argc-1][1] == 'b' || argv[argc-1][1] == 'B')
    01048                 {
    01049                         cout << "Showing debug info." << endl;
    01050                         debug = true;
    01051                 } else
    01052                 {
    01053                         cout << "Ignoring unrecognized option '" << argv[argc-1] << "'." << endl;
    01054                 }
    01055         }
    01056
    01057         if (argc < 1 || argc > 3)
    01058         {
    01059                 cout << "Arguments should be:" << endl << endl;
    01060                 cout << "    <dimacs_file> [-d][-u][-o][-b]" << endl;
    01061                 cout << " or" << endl;
    01062                 cout << "    <variable_file> <constraint_file> [<extra_constraint_file>]"
    01063                      << " [-c<candidate_file>] [-d][-u][-o][-b]" << endl;
    01064                 cout << endl;
    01065                 cout << "<unsat_file> and <sat_file> don't have to exist." << endl;
    01066                 cout << endl;
    01067                 cout << "-c   specifies file of candidates to test; otherwise, only"
    01068                      << " checks consistency." << endl;
    01069                 cout << "-d   makes the SAT engine use DPLL." << endl;
    01070                 cout << "-u   tries for UNSAT instead of SAT." << endl;
    01071                 //cout << "-o   uses Osat for engine instead of VSAT." << endl;
    01072                 cout << "-b   show debug info." << endl;
    01073                 cout << endl;
    01074                 exit(-1);
    01075         }
    01076         cout << endl;
    01077
    01078 /*#
    01079         //if (useOsat && !satisfy)
    01080         //{
    01081         //      cerr << "Warning: Osat does not do unsat yet - switching to sat..." << endl;
    01082         //      satisfy = true;
    01083         //}
    01084 */
    01085         char const * variableFile = argv[0];
    01086         char const * constraintFile = (argc > 1) ? argv[1] : NULL;
    01087         char const * extraFile = (argc > 2) ? argv[2] : NULL;
    01088
    01089 /*#
    01090         //if (useOsat)
    01091         //{
    01092         //      list<Variable *>  vars;
    01093         //      list<Constraint const *>  constraints;
    01094         //      list<Implicant const *>  candidates;
    01095         //      if (!constraintFile)
    01096         //      {
    01097         //              loadDIMACS(variableFile, &vars, &constraints);
    01098         //      } else
    01099         //      {
    01100         //              vars = readVariablesUnconst(variableFile);
    01101         //              constraints = readConstraints(constraintFile, vars);
    01102         //      }
    01103         //      if (candidateFile)
    01104         //              candidates = readImplicants(candidateFile, vars);
    01105     //
    01106         //      Osat osat(vars, constraints);
    01107         //      osat.setDebug(debug);
    01108         //      if (debug)
    01109         //              cout << "Initial Osat:" << endl << osat << endl << endl;
    01110     //
    01111         //      if (osat.consistent())
    01112         //      {
    01113         //              cout << "vsat_driver: Theory is ok. " << (satisfy ? "(consistent)" : "(inconsistent)")
    01114         //                   << endl;
    01115         //      } else
    01116         //      {
    01117         //              cout << "vsat_driver: Theory is not ok! "
    01118         //                   << (satisfy ? "(inconsistent)" : "(consistent)") << endl;
    01119         //      }
    01120         //      cout << endl;
    01121     //
    01122         //      list<Implicant const *>::const_iterator candidateIter;
    01123         //      for (candidateIter = candidates.begin(); candidateIter != candidates.end();
    01124         //           candidateIter++)
    01125         //      {
    01126         //              cout << "Candidate:  " << (*(*candidateIter)) << endl;
    01127         //              if (candidateIter != candidates.begin())
    01128         //                      osat.clearTemporaryConstraint();
    01129         //              osat.addTemporaryConstraints((*candidateIter)->getConstraints());
    01130         //              bool cons = osat.consistent();
    01131         //              if (cons)
    01132         //                      cout << "    is ok. " << (satisfy ? "(consistent)" : "(inconsistent)") << endl;
    01133         //              else
    01134         //                      cout << "    generates conflict.  " << endl ;
    01135         //              cout << endl;
    01136         //      }
    01137     //
    01138         //      exit(0);
    01139         //}
    01140 */
    01141
    01142         list<Variable *>  vars;
    01143         list<Constraint const *>  constraints;
    01144         list<Implicant const *>  candidates;
    01145         list<Constraint const *>  extraConstraints;
    01146         //list<Constraint const *>  dummyConstraints;
    01147         if (!constraintFile)
    01148         {
    01149                 loadDIMACS(variableFile, &vars, &constraints);
    01150         } else
    01151         {
    01152                 vars = readVariablesUnconst(variableFile);
    01153                 constraints = readConstraints(constraintFile, vars);
    01154         }
    01155         if (candidateFile)
    01156                 candidates = readImplicants(candidateFile, vars);
    01157         if (extraFile)
    01158         {
    01159                 extraConstraints = readConstraints(extraFile, vars);
    01160                 cerr << "Ignoring extra constraints..." << endl << endl;
    01161         }
    01162
    01163         VSAT vsat(vars, constraints);
    01164         vsat.setDebug(debug);
    01165         if (debug)
    01166                 cout << "Initial VSAT:" << endl << vsat << endl << endl;
    01167
    01168         //cout << "vsat_driver: checking (in)consistency..." << endl << endl;
    01169         if (vsat.consistent(satisfy, useDPLL))
    01170         {
    01171                 cout << "vsat_driver: Theory is ok. " << (satisfy ? "(consistent)" : "(inconsistent)")
    01172                      << endl;
    01173         } else
    01174         {
    01175                 cout << "vsat_driver: Theory is not ok! "
    01176                      << (satisfy ? "(inconsistent)" : "(consistent)") << endl;
    01177         }
    01178         cout << endl;
    01179 /*#
    01180         //if (vsat.inconsistent(useDPLL))
    01181         //{
    01182         //      cout << "Theory is INconsistent." << endl;
    01183         //} else
    01184         //{
    01185         //      cout << "Theory is not INconsistent!" << endl;
    01186         //}
    01187         //cout << endl;
    01188 */
    01189
    01190         list<Implicant const *>::const_iterator candidateIter;
    01191         for (candidateIter = candidates.begin(); candidateIter != candidates.end();
    01192              candidateIter++)
    01193         {
    01194                 cout << "Candidate:  " << (*(*candidateIter)) << endl;
    01195                 Constraint conf = vsat.tryAssignment((*candidateIter), satisfy, useDPLL);
    01196                 if (conf.isEmpty())
    01197                         cout << "    is ok. " << (satisfy ? "(consistent)" : "(inconsistent)") << endl;
    01198                 else
    01199                         cout << "    generates conflict:  " << conf << endl ;
    01200                 cout << endl;
    01201         }
    01202
    01203         exit(0);
    01204         return 0; //# to make MSVC happy - yes, it's that stupid.
    01205 }
    01206