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

# /Users/fpy/titan-1-5-MBARI/Mers/Solvers/SAT/GATSAT/CompileSAT/CompileSATDriver.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
    00011 #ifdef _MSC_VER
    00012 #pragma warning( disable : 4786 )
    00013 #endif
    00014
    00015 #include <cstdlib>
    00016 #include <cstdio>
    00017 #include <iostream>
    00018 #include <fstream>
    00019 #include <cmath>
    00020 #include <sstream>
    00021 #include <ctime>
    00022
    00023 #include "CompileSAT.h"
    00024 #include <Mers/Models/Base/BaseModelVariable.h>
    00025 #include <Mers/Models/Base/BaseModelAssignment.h>
    00026 #include <Mers/Models/Base/BaseModelSentence.h>
    00027 #include <Mers/Models/Base/BaseModel.h>
    00028 #include <Mers/Utils/Containers/DynamicArrayTemplate.h>
    00029
    00030 /*
    00031 void * operator new(size_t size) throw (std::bad_alloc)
    00032 {
    00033         return NULL;
    00034 }
    00035 extern void * operator new[](size_t size) throw (std::bad_alloc);
    00036 extern void operator delete(void * p) throw ();
    00037 extern void operator delete[](void * p) throw ();
    00038 */
    00039
    00041
    00042 using namespace Mers::Solvers::SAT::GATSAT::CompileSAT;
    00043 using Mers::Models::Base::BaseModelSentence;
    00044 using Mers::Models::Base::BaseModelClauseArray;
    00045 using Mers::Models::Base::BaseModelClause;
    00046 using Mers::Models::Base::BaseModelAssignment;
    00047 using Mers::Models::Base::BaseModelDomain;
    00048 using Mers::Models::Base::BaseModelValue;
    00049 using Mers::Models::Base::BaseModelValueArray;
    00050 using Mers::Models::Base::BaseModelVariable;
    00051 using Mers::Models::Base::BaseModelVariableArray;
    00052 using Mers::Models::Base::BaseModelVariableArrayArray;
    00053 using Mers::Models::Base::BaseModel;
    00054 using Mers::Utils::Containers::DynamicArrayTemplate;
    00055 using Mers::Utils::Lang::BaseModelObject;
    00056 using std::ifstream;
    00057 using std::ostream;
    00058 using std::istringstream;
    00059 using std::cout;
    00060 using std::cerr;
    00061 using std::endl;
    00062 using std::ws;
    00063
    00065
    00066 bool file_exist(char* filename);
    00067 void readVariables(char const * filename, bool useProb, BaseModel &model);
    00068 void readConstraints(char const * filename, BaseModel &model,
    00069         BaseModelSentence &res);
    00070
    00072
    00073 bool
    00074 file_exist(char const * filename)
    00075 {
    00076         FILE *file;
    00077         if ( (file = fopen(filename,"r")) == NULL )
    00078                 return false;
    00079         fclose(file);
    00080         return true;
    00081 }
    00082
    00084
    00085 void readVariables(char const * filename, bool useProb, BaseModel &model)
    00086 {
    00087         char next;
    00088         char tmp[400];
    00089
    00090         if (!file_exist(filename))
    00091         {
    00092                 cerr << "File " << filename << " does not exist." << endl;
    00093                 exit(-1);
    00094         }
    00095
    00096         ifstream in(filename);
    00097
    00098         // skip comment lines
    00099         while (!in.eof() && (next=in.peek()) == '#')
    00100                 in.getline(tmp,400);
    00101
    00102         if (in.eof())
    00103         {
    00104                 cout << "Data file contains no variables. " << endl;
    00105                 return;  // try anyway, for testing...
    00106         }
    00107
    00108         in >> ws;
    00109         while (!in.eof())
    00110         {
    00111                 in.getline(tmp,399);  // read variable
    00112                 in >> ws;
    00113                 if (strlen(tmp) == 0)
    00114                         continue;
    00115                 istringstream line(tmp);
    00116                 char varname[400];
    00117                 line >> varname;
    00118                 line >> ws;
    00119                 BaseModelValueArray domain(true);
    00120                 while (!line.eof())
    00121                 {
    00122                         char val[400];
    00123                         double p;
    00124
    00125                         line >> val;
    00126                         //::cout << "   val: " << val << ", " ;
    00127                         line >> p;
    00128                         //::cout << "prob: " << p << endl;
    00129                         line >> ws;
    00130                         domain.pushBack(new BaseModelValue(val));
    00132                         // p
    00133                 }
    00134                 model.addDomain(varname, domain);
    00135
    00136                 model.addVariable(varname, BaseModelVariable::State, model.getDomain(varname));
    00137                 //cout << "Read variable: " << *var << endl ;
    00138                 //::cout << "(num values: " << values.size() << ")" << endl;
    00140         }
    00141
    00142         in.close();
    00143
    00144         //cout << "Read file with " << (res.size()) << " variables." << endl;
    00145         //cout << endl;
    00146 }
    00147
    00149
    00150 void
    00151 readConstraints(char const * filename, BaseModel &model, BaseModelSentence &res)
    00152 {
    00153         char next;
    00154         char tmp[400];
    00155
    00156         if (!file_exist(filename))
    00157         {
    00158                 cerr << "File " << filename << " does not exist." << endl;
    00159                 exit(-1);
    00160         }
    00161
    00162         ifstream in(filename);
    00163
    00164         // skip comment lines
    00165         while (!in.eof() && (next=in.peek()) == '#')
    00166                 in.getline(tmp,400);
    00167
    00168         in >> ws;
    00169         if (in.eof())
    00170         {
    00171                 cout << "Data file contains no constraints." << endl;
    00172                 return;  // try anyway, for testing...
    00173         }
    00174
    00175         while (!in.eof())
    00176         {
    00177                 in.getline(tmp,399);  // read constraint
    00178                 in >> ws;
    00179                 if (strlen(tmp) == 0)
    00180                         continue;
    00181                 istringstream line(tmp);
    00182                 BaseModelClause * constraint =
    00183                         new BaseModelClause(BaseModelClause::DISJUNCTIVE, true);
    00184                 while (!line.eof())
    00185                 {
    00186                         char   tmpChar;
    00187                         char   token[400];
    00188                         char   vala[400];
    00189                         char * val = vala;  // is this safe?
    00190                         bool   parity = true;
    00191                         line >> tmpChar;
    00192                         if (tmpChar == '!')
    00193                         {
    00194                                 parity = false;
    00195                                 line >> ws;
    00196                                 line >> tmpChar;
    00197                         }
    00198                         bool bracketOpened = false;  // Allow for either form
    00199                         if (tmpChar == '[')
    00200                         {
    00201                                 bracketOpened = true;
    00202                                 line >> ws;
    00203                                 line >> token;
    00204                         } else
    00205                         {
    00206                                 token[0] = tmpChar;
    00207                                 line >> (token+1);
    00208                         }
    00209                         for (unsigned int i = 0; i < sizeof(token); i++)
    00210                         {
    00211                                 char cur = token[i];
    00212                                 if (cur == '\0')  // end of string - assume whitespace separated.
    00213                                 {
    00214                                         line >> ws;
    00215                                         line >> tmpChar;
    00216                                         if (tmpChar != '=')
    00217                                         {
    00218                                                 cerr << "Error in reading from constraint file." << endl;
    00219                                                 cerr << "Choked on line: \"" << tmp << "\"" << endl;
    00220                                                 exit(-1);
    00221                                         }
    00222                                         line >> ws;
    00223                                         line >> vala;
    00224                                         val = vala;
    00225                                         if (val[strlen(val) - 1] == ']')  // closing bracket - always ignore?
    00226                                         {
    00227                                                 val[strlen(val) - 1] = '\0';
    00228                                         }
    00229                                         if (!(*val))  // no string left to find!
    00230                                         {
    00231                                                 cerr << "Error in reading from constraint file.." << endl;
    00232                                                 exit(-1);
    00233                                         }
    00234                                         break;
    00235                                 }
    00236
    00237                                 // whitespace handling below is not needed, since it can never occur...
    00238                                 if (cur == '=' || cur == ' ' || cur == '\t')
    00239                                 {
    00240                                         token[i] = '\0';
    00241                                         if (cur != '=')
    00242                                         {
    00243                                                 for (i++; i < sizeof(token); i++)
    00244                                                 {
    00245                                                         if (token[i] == '=')
    00246                                                                 break;
    00247                                                 }
    00248                                         }
    00249                                         for (i++; i < sizeof(token); i++)
    00250                                         {
    00251                                                 if (token[i] != ' ' && token[i] != '\t')
    00252                                                         break;
    00253                                         }
    00254                                         if (!(i < sizeof(token)))  // no string left to find!
    00255                                         {
    00256                                                 cerr << "Error in reading from constraint file..." << endl;
    00257                                                 exit(-1);
    00258                                         }
    00259                                         val = &(token[i]);
    00260                                         if (val[strlen(val) - 1] == ']')  // closing bracket - always ignore?
    00261                                         {
    00262                                                 val[strlen(val) - 1] = '\0';
    00263                                         }
    00264                                         if (!(*val))  // no string left to find!
    00265                                         {
    00266                                                 cerr << "Error in reading from constraint file...." << endl;
    00267                                                 exit(-1);
    00268                                         }
    00269                                         break;
    00270                                 }
    00271                         }
    00272                         line >> ws;
    00273
    00274                         // get the corresponding assignment:
    00275                         BaseModelAssignment * a;
    00276                         if(parity)
    00277                                 a = model.getAssignment(token, val, BaseModelAssignment::Positive);
    00278                         else
    00279                                 a = model.getAssignment(token, val, BaseModelAssignment::Negative);
    00280                         constraint->pushBack(a);
    00281                 }
    00282                 //cout << "Read constraint: " << (*constraint) << endl ;
    00283                 res.pushBack(constraint);
    00284         }
    00285
    00286         in.close();
    00287
    00288         //cout << "Read file with " << (res.size()) << " constraints." << endl;
    00289         //cout << endl;
    00290 }
    00291
    00293
    00296 class DependencyArrayIndexOutOfBoundsException
    00297 {
    00298 public:
    00308         DependencyArrayIndexOutOfBoundsException(unsigned int myIndex,
    00309                 unsigned int myBound, char const * myFile, unsigned int myLine)
    00310         {
    00311                 index = myIndex;
    00312                 bound = myBound;
    00313                 file = myFile;
    00314                 line = myLine;
    00315         }
    00319         ~DependencyArrayIndexOutOfBoundsException()
    00320         {
    00321         };
    00322         public:
    00324         unsigned int index;
    00326         unsigned int bound;
    00328         char const * file;
    00330         unsigned int line;
    00331         private:
    00335         DependencyArrayIndexOutOfBoundsException();
    00336 };
    00337
    00339
    00340 class DependencyNode;
    00341
    00346 class DependencyHyperedge : public BaseModelObject
    00347 {
    00348 public:
    00352         DependencyHyperedge();
    00356         virtual ~DependencyHyperedge();
    00357
    00363         void addReference();
    00364
    00369         void releaseReference();
    00370
    00378         int addNode(DependencyNode * node);
    00379
    00386         DependencyNode & operator[](unsigned int index)
    00387                 throw (DependencyArrayIndexOutOfBoundsException)
    00388         {
    00389                 if(index >= nodes.getLength()){
    00390                         throw DependencyArrayIndexOutOfBoundsException(index,
    00391                                 nodes.getLength(), __FILE__, __LINE__);
    00392                 }
    00393                 return *(nodes[index]);
    00394         }
    00395
    00400         unsigned int getNumberOfNodes() const {return nodes.getLength();};
    00401
    00406         bool isVisited() const;
    00407
    00412         void setVisited(bool newVisited = true);
    00413
    00419         bool operator==(DependencyHyperedge const &other) const;
    00420
    00421 #ifndef EMBEDDED
    00422
    00426         void print(ostream &out) const;
    00427 #endif
    00428
    00429 protected:
    00431         DynamicArrayTemplate<DependencyNode> nodes;
    00432
    00434         bool visited;
    00435
    00437         unsigned int references;
    00438
    00439 private:
    00443         DependencyHyperedge(DependencyHyperedge &otherNode);
    00447         DependencyHyperedge const & operator =(DependencyHyperedge const &other);
    00448 };
    00449
    00450
    00455 class DependencyNode : public BaseModelObject
    00456 {
    00457 public:
    00464         DependencyNode(BaseModelVariable * myVariable);
    00468         virtual ~DependencyNode();
    00469
    00474         BaseModelVariable * getVariable() {return variable;};
    00475
    00480         BaseModelVariable const * getVariable() const {return variable;};
    00481
    00486         bool isSettable() const;
    00491         void setSettable(bool newSettable = true);
    00492
    00497         bool isVisited() const;
    00498
    00503         void setVisited(bool newVisited = true);
    00504
    00516         int addConnection(DependencyHyperedge * hyperedge);
    00527         int removeConnection(DependencyHyperedge * hyperedge);
    00528
    00534         DependencyHyperedge & operator[](unsigned int index)
    00535                 throw (DependencyArrayIndexOutOfBoundsException)
    00536         {
    00537                 if(index >= hyperedges.getLength()){
    00538                         throw DependencyArrayIndexOutOfBoundsException(index,
    00539                                 hyperedges.getLength(), __FILE__, __LINE__);
    00540                 }
    00541                 return *(hyperedges[index]);
    00542         }
    00543
    00548         unsigned int getNumberOfHyperedges() const {return hyperedges.getLength();};
    00549
    00555         bool operator==(DependencyNode const &other) const;
    00556
    00557 #ifndef EMBEDDED
    00558
    00562         void print(ostream &out) const;
    00563 #endif
    00564
    00565 protected:
    00567         BaseModelVariable * variable;
    00568
    00571         bool settable;
    00572
    00574         bool visited;
    00575
    00577         DynamicArrayTemplate<DependencyHyperedge> hyperedges;
    00578
    00579 private:
    00583         DependencyNode();
    00587         DependencyNode(DependencyNode &otherNode);
    00591         DependencyNode const & operator =(DependencyNode const &other);
    00592 };
    00593
    00594
    00596
    00597 DependencyHyperedge::DependencyHyperedge()
    00598 : BaseModelObject(BaseModelObject::oHaDMoReDependencyHyperedge),
    00599 nodes(false)
    00600 {
    00601         visited = false;
    00602         references = 0;
    00603 }
    00604
    00606
    00607 DependencyHyperedge::~DependencyHyperedge()
    00608 {
    00609 }
    00610
    00612
    00613 void DependencyHyperedge::addReference()
    00614 {
    00615         references++;
    00616 }
    00617
    00619
    00620 void DependencyHyperedge::releaseReference()
    00621 {
    00622         if(references > 0)
    00623                 references--;
    00624         if(references == 0){
    00625                 delete this;
    00626         }
    00627 }
    00628
    00630
    00631 int
    00632 DependencyHyperedge::addNode(DependencyNode * node)
    00633 {
    00634         unsigned int insertPoint = nodes.getLength();
    00635         // we insert NULL because we don't want node to be deleted if
    00636         // our insertion failed.
    00637         if(FAILED(nodes.pushBack(NULL))){
    00638                 fprintf(stderr,
    00639                         "Error, unable to add a new node to the hyperedge\n");
    00640                 return 1;
    00641         }
    00642         nodes[insertPoint] = node;
    00643         return 0;
    00644 }
    00645
    00647
    00648 bool DependencyHyperedge::isVisited() const
    00649 {
    00650         return visited;
    00651 }
    00652
    00654
    00655 void DependencyHyperedge::setVisited(bool newVisited)
    00656 {
    00657         visited = newVisited;
    00658 }
    00659
    00661
    00662 bool DependencyHyperedge::operator==
    00663         (DependencyHyperedge const &other) const
    00664 {
    00665         // same if they have the same pointer
    00666         return (this == &other);
    00667 }
    00668
    00670
    00671 #ifndef EMBEDDED
    00672
    00673 void DependencyHyperedge::print(ostream &out) const
    00674 {
    00675         out << "(Hyperedge";
    00676         if(visited)
    00677                 out << "<Visited>";
    00678         out << ": ";
    00679         for(unsigned int x = 0; x < nodes.getLength(); x++){
    00680                 if(x != 0)
    00681                         out << ", ";
    00682                 out << nodes[x]->getVariable()->getName();
    00683         }
    00684         out << ')';
    00685 }
    00686
    00687 #endif
    00688
    00690
    00691 DependencyNode::DependencyNode(BaseModelVariable * myVariable)
    00692 : BaseModelObject(BaseModelObject::oHaDMoReDependencyNode),
    00693         hyperedges(false)
    00694 {
    00695         variable = myVariable;
    00696         settable = false;
    00697         visited = true;
    00698 }
    00699
    00701
    00702 DependencyNode::~DependencyNode()
    00703 {
    00704         // we only dereference all of our edges
    00705         for(unsigned int x = 0; x < hyperedges.getLength(); x++){
    00706                 hyperedges[x]->releaseReference();
    00707         }
    00708 }
    00709
    00711
    00712 bool DependencyNode::isSettable() const
    00713 {
    00714         return settable;
    00715 }
    00716
    00718
    00719 void DependencyNode::setSettable(bool newSettable)
    00720 {
    00721         settable = newSettable;
    00722 }
    00723
    00725
    00726 bool DependencyNode::isVisited() const
    00727 {
    00728         return visited;
    00729 }
    00730
    00732
    00733 void DependencyNode::setVisited(bool newVisited)
    00734 {
    00735         visited = newVisited;
    00736 }
    00737
    00739
    00740 int DependencyNode::addConnection(DependencyHyperedge * hyperedge)
    00741 {
    00742         unsigned int insertPoint = hyperedges.getLength();
    00743         // we insert NULL because we don't want node to be deleted if
    00744         // our insertion failed.
    00745         // We're going to prematurely add a reference so the object will get
    00746         // deleted if we fail to add it to ourself and we were the only
    00747         // reference
    00748         hyperedge->addReference();
    00749
    00750         if(FAILED(hyperedges.pushBack(NULL))){
    00751                 hyperedge->releaseReference();
    00752                 fprintf(stderr,
    00753                         "Error, unable to add a new hyperedge to the node\n");
    00754                 return 1;
    00755         }
    00756         hyperedges[insertPoint] = hyperedge;
    00757         return 0;
    00758 }
    00759
    00761
    00762 int DependencyNode::removeConnection(DependencyHyperedge * hyperedge)
    00763 {
    00764         unsigned int deletionPoint = hyperedges.getLength() - 1;
    00765
    00766         // compare pointers
    00767         if(hyperedges[deletionPoint] == hyperedge){
    00768                 hyperedges.popBack();
    00769                 hyperedge->releaseReference();
    00770                 return 0;
    00771         }else{
    00772                 fprintf(stderr, "Failed to remove hyperedge: Was not at back\n");
    00773                 return 1;
    00774         }
    00775 }
    00776
    00778
    00779 bool
    00780 DependencyNode::operator ==(DependencyNode const &other) const
    00781 {
    00782         return ((*variable) == (*(other.variable)) &&
    00783                 hyperedges.getLength() == other.hyperedges.getLength());
    00784 }
    00785
    00787
    00788 #ifndef EMBEDDED
    00789
    00790 void DependencyNode::print(ostream &out) const
    00791 {
    00792         out << "Hyper Node";
    00793         if(settable)
    00794                 out << "<settable>";
    00795         out << ": " << variable << endl;
    00796         for(unsigned int x = 0; x < hyperedges.getLength(); x++){
    00797                 out << "  " << hyperedges[x] << endl;
    00798         }
    00799 }
    00800
    00801 #endif
    00802
    00804
    00805 int addHyperedge(DynamicArrayTemplate<DependencyNode> &hypergraphNodes,
    00806         BaseModelClause &clause, DependencyHyperedge * hyperedge)
    00807 {
    00808         // loop over all assignments in the clause
    00809         unsigned int a;
    00810         for(a = 0; a < clause.getLength(); a++){
    00811                 BaseModelAssignment &assignment = *(clause[a]);
    00812                 // we know this is not a const pointer, so remove the const from it.
    00813                 BaseModelVariable * variable =
    00814                         (BaseModelVariable *) assignment.getVariable();
    00815                 unsigned int varUID = variable->getUID();
    00816                 DependencyNode * node = NULL;
    00817
    00818                 // if the node might already exist, look it up
    00819                 if(varUID < hypergraphNodes.getLength())
    00820                         node = hypergraphNodes[varUID];
    00821                 else
    00822                         hypergraphNodes.resize(varUID + 1);
    00823                 // if this is a new node/variable, add the node to the list
    00824                 if(node == NULL){
    00825                         node = new DependencyNode(variable);
    00826                         if(!node){
    00827                                 fprintf(stderr, "Error: a new DependencyNode could not "
    00828                                         "be created\n");
    00829                                 return 1;
    00830                         }
    00831
    00832                         // add the node to the list
    00833                         hypergraphNodes[varUID] = node;
    00834                 }
    00835
    00836                 // add this node to the edge for this clause
    00837                 if(FAILED(hyperedge->addNode(node))){
    00838                         fprintf(stderr, "Failed to add a node to a hyperedge\n");
    00839                         return 1;
    00840                 }
    00841         }
    00842
    00843         // loop back over the clause and add the complete hyperedge
    00844         // back into each clause
    00845         for(a = 0; a < clause.getLength(); a++){
    00846                 BaseModelAssignment &assignment = *(clause[a]);
    00847                 unsigned int varUID = assignment.getVariable()->getUID();
    00848
    00849                 // Get our node back (it should exist since we created it above
    00850                 // it didn't)
    00851                 DependencyNode * node = hypergraphNodes[varUID];
    00852                 // Add it to the node.  It will manage the number of references
    00853                 // to this edge so it will get deleted when everybody is done with it.
    00854                 if(FAILED(node->addConnection(hyperedge))){
    00855                         fprintf(stderr, "Failed to add a hyperedge to a node\n");
    00856                         return 1;
    00857                 }
    00858         }
    00859         return 0;
    00860 }
    00861
    00863
    00873 int bfind(BaseModelVariableArray &variables,
    00874         BaseModelVariable const * variable)
    00875 {
    00876         unsigned int l, m, r;
    00877         unsigned int varUID = variable->getUID();
    00878         unsigned int sVarUID;
    00879
    00880         l = 0;
    00881         r = variables.getLength();
    00882         while(l < r){
    00883                 // note that l <= m < r
    00884                 m = (l + r) >> 1;
    00885                 sVarUID = variables[m]->getUID();
    00886                 if(sVarUID == varUID)
    00887                         return m;
    00888                 else if(sVarUID < varUID)
    00889                         // the thing we're looking for is after m
    00890                         l = m + 1;
    00891                 else
    00892                         // the thing we're looking for is before m
    00893                         r = m;
    00894         }
    00895         return l;
    00896 }
    00897
    00899
    00907 void insertList(BaseModelVariableArray &variables,
    00908         BaseModelVariable * variable)
    00909 {
    00910         unsigned int insPoint;
    00911
    00912         insPoint = bfind(variables, variable);
    00913         // if it doesn't already exist, insert it
    00914         if(insPoint >= variables.getLength() ||
    00915                 variables[insPoint]->getUID() != variable->getUID())
    00916                 variables.insert(insPoint, variable);
    00917 }
    00918
    00920
    00921 int
    00922 generateHypergraph(DynamicArrayTemplate<DependencyNode> &hypergraphNodes,
    00923         BaseModelSentence &clauses)
    00924 {
    00925         // delete any nodes we had before
    00926         hypergraphNodes.makeEmpty();
    00927
    00928         //loop over all clauses/hyperedges
    00929         for(unsigned int c = 0; c < clauses.getLength(); c++){
    00930                 BaseModelClause &clause = *(clauses[c]);
    00931                 // we generate a hyperedge for each clause
    00932                 DependencyHyperedge * hyperedge = new DependencyHyperedge();
    00933                 if(!hyperedge){
    00934                         fprintf(stderr, "Error: a new DependencyHyperedge could "
    00935                                 "not be created\n");
    00936                         return 1;
    00937                 }
    00938                 if(FAILED(addHyperedge(hypergraphNodes, clause, hyperedge)))
    00939                         return 1;
    00940         }
    00941
    00942         return 0;
    00943 }
    00944
    00946
    00947 void gatherReachable(BaseModelVariableArray &variableSet,
    00948         DependencyHyperedge &edge)
    00949 {
    00950         unsigned int v;
    00951         unsigned int numberOfNodes = edge.getNumberOfNodes();
    00952
    00953         // search over all the nodes of these edges
    00954         for(v = 0; v < numberOfNodes; v++){
    00955                 DependencyNode &hNode = edge[v];
    00956                 // if we cannot set this variable
    00957                 if(!hNode.isSettable()){
    00958                         if(!hNode.isVisited()){
    00959                                 hNode.setVisited();
    00960                                 unsigned int numberOfHyperedges = hNode.getNumberOfHyperedges();
    00961                                 // then expand all of its edges
    00962                                 for(unsigned int e = 0; e < numberOfHyperedges; e++){
    00963                                         DependencyHyperedge &hEdge = hNode[e];
    00964                                         // if we haven't visited this node yet, then expand it
    00965                                         if(!hEdge.isVisited()){
    00966                                                 // we only visit each edge once.
    00967                                                 hEdge.setVisited();
    00968                                                 // expand this edge and add it to our list
    00969                                                 gatherReachable(variableSet, hEdge);
    00970                                         }
    00971                                 }
    00972                         }
    00973                 }else{
    00974                         insertList(variableSet, hNode.getVariable());
    00975                 }
    00976         }
    00977 }
    00978
    00980
    00981 void removeRedundantSets
    00982         (DynamicArrayTemplate<BaseModelVariableArray> &variableSets)
    00983 {
    00984         unsigned int s1;
    00985         for(s1 = 0; s1 < variableSets.getLength(); s1++){
    00986                 BaseModelVariableArray &varSet1 = *(variableSets[s1]);
    00987                 for(unsigned int s2 = s1 + 1; s2 < variableSets.getLength(); s2++){
    00988                         BaseModelVariableArray &varSet2 = *(variableSets[s2]);
    00989                         unsigned int v1, v2, vs1Length, vs2Length;
    00990                         bool vs1IsSubset = true, vs2IsSubset = true;
    00991
    00992                         for(v1 = 0, vs1Length = varSet1.getLength(),
    00993                                 v2 = 0, vs2Length = varSet2.getLength();
    00994                         v1 < vs1Length && v2 < vs2Length &&
    00995                                 (vs1IsSubset || vs2IsSubset);)
    00996                         {
    00997                                 unsigned int v1UID = varSet1[v1]->getUID();
    00998                                 unsigned int v2UID = varSet2[v2]->getUID();
    00999                                 if(v1UID < v2UID){
    01000                                         // we have something in v1 that isn't in v2
    01001                                         vs1IsSubset = false;
    01002                                         v1++;
    01003                                 }else if(v1UID > v2UID){
    01004                                         // we have something in v2 that isn't in v1
    01005                                         vs2IsSubset = false;
    01006                                         v2++;
    01007                                 }else{
    01008                                         // the both have this, skip it
    01009                                         v1++;
    01010                                         v2++;
    01011                                 }
    01012                         }
    01013                         if(v1 < vs1Length)
    01014                                 vs1IsSubset = false;
    01015                         if(v2 < vs2Length)
    01016                                 vs2IsSubset = false;
    01017                         if(vs2IsSubset){
    01018                                 // eliminate s2
    01019                                 if(s2 + 1 == variableSets.getLength()){
    01020                                         BaseModelVariableArray * last = variableSets.popBack();
    01021                                         last->makeEmpty();
    01022                                         delete last;
    01023                                 }else{
    01024                                         variableSets[s2]->makeEmpty();
    01025                                         delete variableSets[s2];
    01026                                         BaseModelVariableArray * last = variableSets.popBack();
    01027                                         variableSets[s2] = last;
    01028                                 }
    01029                                 s2--;
    01030                         }else if(vs1IsSubset){
    01031                                 // eliminate s1
    01032                                 variableSets[s1]->makeEmpty();
    01033                                 delete variableSets[s1];
    01034                                 BaseModelVariableArray * last = variableSets.popBack();
    01035                                 variableSets[s1] = last;
    01036                                 s1--;
    01037                                 break;
    01038                         }
    01039                 }
    01040         }
    01041 }
    01042
    01044
    01045 DynamicArrayTemplate<BaseModelVariableArray> * generatePartitionSpace(
    01046         DynamicArrayTemplate<DependencyNode> &hypergraphNodes,
    01047         BaseModelVariableArray &partitionVariables)
    01048 {
    01049         // Initially we start without any partition sets
    01050         DynamicArrayTemplate<BaseModelVariableArray> * partitionSets =
    01051                 new DynamicArrayTemplate<BaseModelVariableArray>(true);
    01052         unsigned int v;
    01053
    01054         for(v = 0; v < hypergraphNodes.getLength(); v++){
    01055                 DependencyNode &hNode = *(hypergraphNodes[v]);
    01056                 if(&hNode == NULL)
    01057                         continue;
    01058
    01059                 // clear all the edges to unvisited
    01060                 for(unsigned int e = 0; e < hNode.getNumberOfHyperedges(); e++){
    01061                         hNode[e].setVisited(false);
    01062                 }
    01063
    01064                 // update the settable information about each node
    01065                 hNode.setSettable(false);
    01066                 hNode.setVisited(false);
    01067                 for(unsigned int pv = 0; pv < partitionVariables.getLength(); pv++){
    01068                         BaseModelVariable &partitionVariable = *(partitionVariables[pv]);
    01069                         if(partitionVariable == *(hNode.getVariable())){
    01070                                 hNode.setSettable();
    01071                                 break;
    01072                         }
    01073                 }
    01074         }
    01075
    01076         // find all search sets from each variable
    01077         for(v = 0; v < hypergraphNodes.getLength(); v++){
    01078                 DependencyNode &hNode = *(hypergraphNodes[v]);
    01079                 // only expand nodes that we can keep
    01080                 if((&hNode != NULL) && hNode.isSettable()){
    01081                         // look at all outbound edges
    01082                         for(unsigned int e = 0; e < hNode.getNumberOfHyperedges(); e++){
    01083                                 DependencyHyperedge &hEdge = hNode[e];
    01084                                 // only expand the edge if we haven't done so already
    01085                                 if(!hEdge.isVisited()){
    01086                                         // we only want to expand each edge once.
    01087                                         hEdge.setVisited();
    01088                                         // our new search list
    01089                                         BaseModelVariableArray * variableSet =
    01090                                                 new BaseModelVariableArray(false);
    01091                                         // gather all reachable settable states from this edge
    01092                                         gatherReachable(*variableSet, hEdge);
    01093                                         // if we found some
    01094                                         if(variableSet->getLength() > 0){
    01095                                                 // record this set
    01096                                                 partitionSets->pushBack(variableSet);
    01097                                         }else{
    01098                                                 // otherwise delete it since it's empty and the empty
    01099                                                 // set will always be a subset (even if there aren't any
    01100                                                 // other sets).
    01101                                                 delete variableSet;
    01102                                         }
    01103                                 }
    01104                         }
    01105                 }
    01106         }
    01107
    01108         // remove any redundant sets
    01109         removeRedundantSets(*partitionSets);
    01110         return partitionSets;
    01111 }
    01112
    01114
    01115 int
    01116 main(int argc, char** argv)
    01117 {
    01118         argc--;
    01119         argv++;
    01120
    01121         bool useDebug = false;
    01122         bool useProb = false;
    01123         int numResults = 1;
    01124         bool exitOnly = false;
    01125         bool testForValid = true;
    01126         bool useDecomposition = false;
    01127         bool generateTiming = false;
    01128         char const * timingFileName = "timing.out";
    01129
    01130         for (; argc > 0 && argv[argc-1][0] == '-'; argc--)
    01131         {
    01132                 switch(argv[argc - 1][1]){
    01133                 case 'd':
    01134                 case 'D':
    01135                         cout << "Showing debug info." << endl;
    01136                         useDebug = true;
    01137                         break;
    01138                 case 'u':
    01139                 case 'U':
    01140                         cout << "Trying for UNSAT problem instead of SAT (not implemented)."
    01141                                 << endl;
    01142                         break;
    01143                 case 'p':
    01144                 case 'P':
    01145                         cout << "Treating costs as probabilities." << endl;
    01146                         useProb = true;
    01147                         break;
    01148                 case 'x':
    01149                 case 'X':
    01150                         cout << "Exiting after problem setup." << endl;
    01151                         exitOnly = true;
    01152                         break;
    01153                 case 'n':
    01154                 case 'N':
    01155                         {
    01156                                 char * numStr = argv[argc-1]+2;
    01157                                 numResults = atoi(numStr);
    01158                                 cout << "Searching for best " << numResults << " results." << endl;
    01159                         }
    01160                         break;
    01161                 case 's':
    01162                 case 'S':
    01163                         cout << "Not testing for Valid" << endl;
    01164                         testForValid = false;
    01165                         break;
    01166                 case 'H':
    01167                         cout << "Using hypergraph decomposition" << endl;
    01168                         useDecomposition = true;
    01169                         break;
    01170                 case 'T':
    01171                         if(argv[argc - 1][2] != '\0')
    01172                                 timingFileName = argv[argc - 1] + 2;
    01173                         generateTiming = true;
    01174                         cout << "Filtering timing information to '" << timingFileName << "'." << endl;
    01175                         break;
    01176                 default:
    01177                         cout << "Ignoring unrecognized option '" << argv[argc-1] << "'." << endl;
    01178                 }
    01179         }
    01180         if (argc < 3 || argc > 4)
    01181         {
    01182                 cout << "Arguments should be:" << endl << endl;
    01183                 cout << "   <design_var_file> <state_var_file> "
    01184                      << "<constraint_file> [<extra_constraint_file>] [-d][-n]" << endl;
    01185                 cout << endl;
    01186                 cout << "<extra_constraint_file> does not need to be provided." << endl;
    01187                 cout << endl;
    01188                 cout << "-u   tries for UNSAT instead of SAT." << endl;
    01189                 cout << "-d   show debug info." << endl;
    01190                 cout << "-p   treats costs as probabilities." << endl;
    01191                 cout << "-n#  specifies the number to find (default is 1)." << endl;
    01192                 cout << "-x   exit after problem setup (for timing)." << endl;
    01193                 cout << "-s   test for satisfiability only (Not Valid)." << endl;
    01194                 cout << "-H   uses the hypertree decomposition method." << endl;
    01195                 cout << "-T<debugFile>   appends running time to the file. (Defaults to "
    01196                         << timingFileName << ")" << endl;
    01197                 cout << endl;
    01198                 exit(-1);
    01199         }
    01200         cout << endl;
    01201
    01202         char const * designVariableFile = argv[0];
    01203         char const * stateVariableFile = argv[1];
    01204         char const * constraintFile = argv[2];
    01205         char const * extraConstraintFile = (argc > 3) ? argv[3] : NULL;
    01206
    01207         BaseModel model(designVariableFile);
    01208
    01209         readVariables(designVariableFile, useProb, model);
    01210         unsigned int numDesignVariables = model.getVariables()->getLength();
    01211
    01212         readVariables(stateVariableFile, useProb, model);
    01213         // unsigned int numOtherVariables = model.getVariables()->getLength() - numDesignVariables;
    01214
    01215         BaseModelVariableArray designVariables(false);
    01216         {
    01217                 BaseModelVariableArray &allVars = *(model.getVariables());
    01218                 designVariables.resize(numDesignVariables);
    01219                 for(unsigned int v = 0; v < numDesignVariables; v++){
    01220                         designVariables[v] = allVars[v];
    01221                 }
    01222         }
    01223
    01224         BaseModelSentence constraints(BaseModelSentence::CNF, true);
    01225         readConstraints(constraintFile, model, constraints);
    01226         BaseModelSentence extraConstraints(BaseModelSentence::CNF, true);
    01227         if (extraConstraintFile)
    01228                 readConstraints(extraConstraintFile, model, extraConstraints);
    01229
    01230         //float cutoff = 0.999F;
    01231         int maxStatesTime = 2000000;
    01232         int maxStatesSize = 1500000;
    01233
    01234         BaseModelVariableArrayArray variableGroups(true);
    01235
    01236         if (useDebug)
    01237                 cout << "Constructing CompileSAT*..." << endl;
    01238
    01239         clock_t startTime = clock();
    01240         if(useDecomposition){
    01241                 DynamicArrayTemplate<DependencyNode> hypergraph(true);
    01242
    01243                 if(FAILED(generateHypergraph(hypergraph, constraints))){
    01244                         fprintf(stderr, "Error, could not create hypergraph\n");
    01245                         return 0;
    01246                 }
    01247
    01248                 DynamicArrayTemplate<BaseModelVariableArray> * groups =
    01249                         generatePartitionSpace(hypergraph, designVariables);
    01250
    01251                 printf("Generated partion groups:\n");
    01252                 while(groups->getLength() > 0){
    01253                         BaseModelVariableArray * group = groups->popBack();
    01254                         fputc('{', stdout);
    01255                         for(unsigned int x = 0; x < group->getLength(); x++){
    01256                                 if(x != 0)
    01257                                         fputs(", ", stdout);
    01258                                 printf("%s", (*group)[x]->getName());
    01259                         }
    01260                         fputs("}\n", stdout);
    01261                         if(FAILED(variableGroups.pushBack(group))){
    01262                                 fprintf(stderr, "Error, could not transfer the variable groups\n");
    01263                                 return 0;
    01264                         }
    01265                 }
    01266         }else{
    01267                 BaseModelVariableArray * group = new BaseModelVariableArray(designVariables);
    01268                 variableGroups.pushBack(group);
    01269         }
    01270
    01271         // is this construction varying in expense for baseline comparison?
    01272         CompileSAT * clas = new CompileSAT(variableGroups, designVariables, *(model.getVariables()),
    01273                 constraints, testForValid);
    01274         if(useDebug)
    01275                 clas->setDebug(10);
    01276
    01277         if (useDebug)
    01278                 cout << "Initial ClA*:" << endl << (*clas) << endl;
    01279
    01280         if (!exitOnly)
    01281         {
    01282                 if (extraConstraints.getLength() == 0)  // only one problem...
    01283                 {
    01284                         BaseModelClauseArray * results =
    01285                                 clas->findUnsatisfyingSolutions(numResults, maxStatesTime, maxStatesSize);
    01286
    01287                         if(results){
    01288                                 //cout << "Final ClA*:" << endl << (*clas) << endl;
    01289                                 cout << "Conflicts generated (" << results->getLength() << "): " << endl;
    01290                                 for (unsigned int x = 0; x < results->getLength(); x++)
    01291                                 {
    01292                                         cout << "    " << *((*results)[x]) << endl ;
    01293                                 }
    01294                                 delete results;
    01295
    01296                                 cout << endl;
    01297                                 clas->printStatistics();
    01298                         }else{
    01299                                 cout << "Did not generate any conflicts." << endl;
    01300                         }
    01301
    01302                 } else
    01303                 {
    01304                         BaseModelSentence::ConstantIterator cIter;
    01305                         for (cIter = extraConstraints.begin(); cIter != extraConstraints.end(); cIter++)
    01306                         {
    01307                                 cout << endl << endl
    01308                                      << "Trying with  constraint: " << (*cIter) << endl << endl;
    01309                                 clas->addTemporaryConstraint(&(*cIter));
    01310                                 BaseModelClauseArray * results =
    01311                                         clas->findUnsatisfyingSolutions(numResults, maxStatesTime, maxStatesSize);
    01312
    01313                                 //cout << "Final ClA*:" << endl << clas << endl;
    01314                                 cout << "Conflicts generated (" << results->getLength() << "): " << endl;
    01315                                 for (unsigned int x = 0; x < results->getLength(); x++)
    01316                                 {
    01317                                         cout << "    " << *((*results)[x]) << endl ;
    01318                                 }
    01319                                 delete results;
    01320                         }
    01321                 }
    01322         }
    01323
    01324         clock_t timeDiff = clock() - startTime;
    01325         if(generateTiming){
    01326                 FILE * timingFile = fopen(timingFileName, "a");
    01327                 double totalTime = timeDiff;
    01328                 totalTime /= CLOCKS_PER_SEC;
    01329
    01330                 if(timingFile == NULL){
    01331                         perror(timingFileName);
    01332                         fprintf(stdout, "Elapsed Time: %f seconds\n", totalTime);
    01333                 }else{
    01334                         fprintf(timingFile, "Elapsed Time: %f seconds\n", totalTime);
    01335                         fclose(timingFile);
    01336                 }
    01337         }
    01338
    01339         //cout << "Deleting CompileSAT" << endl;
    01340         delete clas;
    01341
    01342         return 0;
    01343 }
    01344
    01346