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

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

    00001 //========================================================================================
    00002 //
    00003 // Copyright (c) 2001           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 (MERS) group
    00007 // does not assume any responsibility.
    00008 //
    00009 // Author:                      Seung H. Chung
    00010 //
    00011 // Organization:        Model-based Embedded and Robotic Systems Group
    00012 //                                      Massachusetts Institute of Technology
    00013 //
    00014 // File:                        ISATPropositionDB.h
    00015 //
    00016 // Description:         Circularly linked list of proposition pointers. It follows the C++
    00017 //                                      Standard Template Library specifications. It is in charge of
    00018 //                                      allocating and deallocating the propositions (i.e. this maintains
    00019 //                                      a data base of propositions that ISAT uses).
    00020 //
    00021 //========================================================================================
    00022
    00023 #include <cassert>
    00024 #include <cstdio>
    00025 #include "ISATPropositionDescription.h"
    00026 #include "ISATProposition.h"
    00027 #include "ISATPropositionDB.h"
    00028 #include "ISATLiterals.h"
    00029
    00031
    00032 using namespace Mers::Solvers::SAT::ISAT;
    00033 using std::ostream;
    00034 using std::endl;
    00035
    00037 // Public Constructors, Copy Constructors, & Destructors
    00039
    00040 ISATPropositionDB::ISATPropositionDB()
    00041 {
    00042 }
    00043
    00044 ISATPropositionDB::~ISATPropositionDB()
    00045 {
    00046         ISATProposition *proposition_p;
    00047         ISATPropositionDB::iterator it = begin();
    00048         while (it != end())
    00049         {
    00050                 proposition_p = *it;
    00051                 erase(it);
    00052                 delete proposition_p;
    00053                 it = begin();
    00054         }
    00055 }
    00056
    00057 //----------------------------------------------------------------------------------------
    00058 // Public Function Members
    00059 //----------------------------------------------------------------------------------------
    00060
    00061 ISATProposition const *
    00062 ISATPropositionDB::get_proposition_p(ISATPropositionDescription const *description_p)
    00063 {
    00064         // Check if the proposition with the matching descprition already exists.
    00065         ISATProposition const *existing_proposition_p = find_proposition_p(description_p);
    00066
    00067         // If found proposition is not NULL, return it.
    00068         if (existing_proposition_p != NULL)
    00069         {
    00070                 delete description_p;
    00071                 return existing_proposition_p;
    00072         }
    00073         // Otherwise, a new proposition with the description must be created.
    00074         else
    00075         {
    00076                 // Create a new proposition with the description.
    00077                 ISATProposition *new_proposition_p = new ISATProposition(description_p);
    00078
    00079                 // Insert the new proposition into the database.
    00080                 push_back(new_proposition_p);
    00081
    00082                 // Return the new proposition.
    00083                 return new_proposition_p;
    00084         }
    00085 }
    00086 /*ISATProposition *
    00087 ISATPropositionDB::get_proposition_p(ISATProposition *proposition_p)
    00088 {
    00089 //      cout << *this << endl;
    00090 //      cout << "Searching for " << *proposition_p << "..." << endl;
    00091         for (ISATPropositionDB::iterator it = begin(); it != end(); it++)
    00092         {
    00093 //              cout << "Comparing with ";
    00094 //              (*it)->get_description_p()->print(cout);
    00095 //              cout << "... ";
    00096
    00097                 // If the proposition has the same description, return it.
    00098                 if (*((*it)->get_description_p()) == *proposition_p->get_description_p())
    00099                 {
    00100 //                      cout << "SAME" << endl;
    00101 //                      cout << "Search Finished" << endl << endl;
    00102                         return *it;
    00103                 }
    00104 //              cout << "DIFFERENT" << endl;
    00105         }
    00106 //      cout << "Not found" << endl;
    00107 //      cout << "Inserting into the database..." << endl << endl;;
    00108         push_back(proposition_p);
    00109 //      insert(end(), proposition_p);
    00110         return proposition_p;
    00111 }*/
    00112
    00113 /*
    00114 ISATProposition *
    00115 ISATPropositionDB::insert_proposition(ISATProposition *new_proposition_p)
    00116 {
    00117         // Check for duplicate
    00118         for (iterator it = begin(); it != end(); it++)
    00119         {
    00120                 // If a duplicate is found return the pointer to the proposition that is already
    00121                 // in the database.
    00122                 if (*it == *new_proposition_p)
    00123                 {
    00124                         return &*it;
    00125                 }
    00126         }
    00127
    00128         // Since there is no duplicate, insert the new proposition.
    00129         insert(end(), new_proposition_p);
    00130
    00131         // Return the pointer to the inserted proposition.
    00132         return new_proposition_p;
    00133 }*/
    00134
    00135 /*
    00136 ISATPropositionDB::iterator
    00137 ISATPropositionDB::find(isatProposition::descriptionType const
    00138                        isatProposition_description) {
    00139   for (iterator it = begin(); it != end(); it++) {
    00140     if (it->description() == isatProposition_description) {
    00141       return it;
    00142     }
    00143         }
    00144         return end();
    00145 }
    00146 ISATPropositionDB::const_iterator
    00147 ISATPropositionDB::find(isatProposition::descriptionType const
    00148                        isatProposition_description) const {
    00149   for (const_iterator const_it = begin(); const_it != end(); const_it++) {
    00150     if (const_it->description() == isatProposition_description) {
    00151       return const_it;
    00152     }
    00153         }
    00154         return end();
    00155 }
    00156 */
    00157
    00158 void
    00159 ISATPropositionDB::remove_proposition(ISATProposition *proposition_p)
    00160 {
    00161         assert(proposition_p->get_positive_literals_p()->empty());
    00162         assert(proposition_p->get_negative_literals_p()->empty());
    00163
    00164         remove(&*proposition_p);
    00165 }
    00166
    00167
    00168 void
    00169 ISATPropositionDB::reset()
    00170 {
    00171         for (ISATPropositionDB::iterator it = begin(); it != end(); it++)
    00172         {
    00173                 (*it)->set_truth_value(ISATProposition::UNKNOWNVAL);
    00174         }
    00175 }
    00176
    00177 //----------------------------------------------------------------------------------------
    00178 // Public Operators
    00179 //----------------------------------------------------------------------------------------
    00180
    00181 /*bool
    00182 ISATPropositionDB::operator ==(ISATPropositionDB const &other) const
    00183 {
    00184         ISATPropositionDB::const_iterator this_const_it;
    00185         ISATPropositionDB::const_iterator other_const_it;
    00186         if (this == &other)
    00187         {
    00188                 return true;
    00189         }
    00190         else
    00191         {
    00192                 if (this->size() != other.size())
    00193                 {
    00194                         return false;
    00195                 }
    00196                 else
    00197                 {
    00198                         for (this_const_it = begin(), other_const_it = other.begin();
    00199                         this_const_it != end() && other_const_it != other.end();
    00200                         this_const_it++, other_const_it++)
    00201                         {
    00202                                 if (*this_const_it != *other_const_it) return false;
    00203                         }
    00204                         return true;
    00205                 }
    00206         }
    00207 }
    00208
    00209 bool
    00210 ISATPropositionDB::operator !=(ISATPropositionDB const &other) const
    00211 {
    00212         return !(*this == other);
    00213 }*/
    00214 /*
    00215 ISATPropositionDB const &
    00216 ISATPropositionDB::operator =(ISATPropositionDB const &other)
    00217 {
    00218         if (this != &other)
    00219         {
    00220                 destroy();
    00221                 copy(other);
    00222         }
    00223         return (*this);
    00224 }
    00225 */
    00226
    00227 //----------------------------------------------------------------------------------------
    00228 // Private Function Members
    00229 //----------------------------------------------------------------------------------------
    00230
    00231 ISATProposition *
    00232 ISATPropositionDB::find_proposition_p(ISATPropositionDescription const *description_p) const
    00233 {
    00234         // Iterate through all propositions in the database and check if any have the same
    00235         // proposition description as the description given;
    00236         ISATPropositionDB::const_iterator const_it;
    00237         for (const_it = begin(); const_it != end(); const_it++)
    00238         {
    00239                 // If the proposition has the same description, return it.
    00240                 if (*(*const_it)->get_description_p() == *description_p)
    00241                 {
    00242                         // Since the description matches, return the proposition;
    00243                         return *const_it;
    00244                 }
    00245         }
    00246         // No proposition with the matching description was found. Return NULL.
    00247         return NULL;
    00248 }
    00249
    00250 void
    00251 ISATPropositionDB::unmark_all_propositions()
    00252 {
    00253         // Iterate through all propositions in the database and unmark them.
    00254         ISATPropositionDB::iterator it;
    00255         for (it = begin(); it != end(); it++)
    00256         {
    00257                 (*it)->set_marked(false);
    00258         }
    00259 }
    00260
    00261
    00262 namespace Mers {
    00263         namespace Solvers {
    00264                 namespace SAT {
    00265                         namespace ISAT {
    00266
    00267                                 ostream &
    00268                                 operator <<(ostream &stream, ISATPropositionDB const &proposition_database)
    00269                                 {
    00270                                         ISATPropositionDB::const_iterator const_it = proposition_database.begin();
    00271                                         if (const_it != proposition_database.end())
    00272                                         {
    00273                                                 stream << **const_it;
    00274                                                 const_it++;
    00275                                                 while (const_it != proposition_database.end())
    00276                                                 {
    00277                                                         stream << endl << **const_it;
    00278                                                         const_it++;
    00279                                                 }
    00280                                         }
    00281                                         return stream;
    00282                                 }
    00283                         }
    00284                 }
    00285         }
    00286 }
    00287