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

# /Users/fpy/titan-1-5-MBARI/Mers/Solvers/SAT/ISAT/ISATClause.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:                        ISATClause.cpp
    00015 //
    00016 // Description:         Circularly linked list of literal pointers. It follows the C++
    00017 //                                      Standard Template Library specifications. It is in charge of
    00018 //                                      allocating and deallocating the literals.
    00019 //
    00020 //========================================================================================
    00021
    00022 #include <cstdio>
    00023 #include <cassert>
    00024 #include "ISATClause.h"
    00025 #include "ISATLiteral.h"
    00026 #include "ISATProposition.h"
    00027 #include "ISATPropositionDescription.h"
    00028
    00029
    00030 #include "ISATStringDescription.h"
    00031
    00033
    00034 using namespace Mers::Solvers::SAT::ISAT;
    00035 using std::list;
    00036 using std::ostream;
    00037 using std::cerr;
    00038 using std::endl;
    00039
    00041 // Public Constructors, Copy Constructors, & Destructors
    00043
    00044 ISATClause::ISATClause()
    00045 {
    00046         satisfying_literal_p            = NULL;
    00047         numb_of_unresolved_literals     = 0;
    00048         unit_resolved                           = false;
    00049         active                                          = false;
    00050 }
    00051
    00052 ISATClause::ISATClause(ISATClause const &other)
    00053 : list<ISATLiteral *>(other)
    00054 {
    00055         *this = other;
    00056 }
    00057
    00058 ISATClause::~ISATClause()
    00059 {
    00060         // Delete all literals in the clause.
    00061         ISATLiteral *literal_p;
    00062         while (!empty())
    00063         {
    00064                 literal_p = front();
    00065                 pop_front();
    00066                 delete literal_p;
    00067         }
    00068 }
    00069
    00070 //----------------------------------------------------------------------------------------
    00071 // Public Function Members
    00072 //----------------------------------------------------------------------------------------
    00073
    00074 // Returns true if this clause is inconsistent (i.e. a clause with all false literals),
    00075 // and otherwise returns false.
    00076 bool
    00077 ISATClause::is_inconsistent() const
    00078 {
    00079         // It is an inconsistent clause if it has no unresolved literal and no literal that
    00080         // satisfies this clause.
    00081         if (get_numb_of_literals() > 0 && numb_of_unresolved_literals == 0 && get_satisfying_literal_p() == NULL)
    00082         {
    00083 //#if defined(_DEBUG)
    00084 //              ISATClause::const_iterator it;
    00085 //              for (it = begin(); it != end(); it++)
    00086 //              {
    00087 //                      assert((*it)->get_truth_value() == ISATLiteral::FALSEVAL);
    00088 //              }
    00089 //#endif // #if defined(_DEBUG)
    00090                 return true;
    00091         }
    00092         else
    00093         {
    00094 //#if defined(_DEBUG)
    00095 //              ISATClause::const_iterator it;
    00096 //              bool was_found_inconsistent = 1;
    00097 //              for (it = begin(); it != end(); it++)
    00098 //              {
    00099 //                      if ((*it)->get_truth_value() == ISATLiteral::TRUEVAL ||
    00100 //                              (*it)->get_truth_value() == ISATLiteral::UNKNOWNVAL)
    00101 //                      {
    00102 //                              was_found_inconsistent = 0;
    00103 //                      }
    00104 //              }
    00105 //              assert(!was_found_inconsistent);
    00106 //#endif // #if defined(_DEBUG)
    00107                 return false;
    00108         }
    00109 }
    00110
    00111 // Returns true if this clause is consistent (i.e. a clause with at least one true
    00112 // literal), and otherwise returns false.
    00113 bool
    00114 ISATClause::is_consistent() const
    00115 {
    00116         // If there is at least one true literal, one of them should be the clause's
    00117         // satisfying literal
    00118         if (get_numb_of_literals() == 0 || get_satisfying_literal_p() != NULL)
    00119         {
    00120 #if defined(_DEBUG)
    00121                 if (get_numb_of_literals() > 0)
    00122                 {
    00123                         // If this clause does have a satisfying literal the truth value of the
    00124                         // satisfying literal should be true.
    00125                         assert(get_satisfying_literal_p()->get_truth_value() == ISATLiteral::TRUEVAL);
    00126                 }
    00127 #endif //#if defined(_DEBUG)
    00128
    00129                 // Since at least on literal satisfies this clause, it is consistent.
    00130                 return true;
    00131         }
    00132         // Otherwise, no true literal exists in the clause
    00133         else
    00134         {
    00135 //#if defined(_DEBUG)
    00136 //              ISATClause::const_iterator it;
    00137 //              for (it = begin(); it != end(); it++)
    00138 //              {
    00139 //                      assert((*it)->get_truth_value() == ISATLiteral::FALSEVAL ||
    00140 //                              (*it)->get_truth_value() == ISATLiteral::UNKNOWNVAL);
    00141 //              }
    00142 //#endif // #if defined(_DEBUG)
    00143
    00144                 // No true literal in the clause implies that it is not consistent.
    00145                 return false;
    00146         }
    00147 }
    00148
    00149 // Returns the consistency of the clause. A clause may be CONSISTENT, INCONSISTENT,
    00150 // or INDETERMINATE.
    00151 //
    00152 //     o CONSISTENT:    At least one literal is true.
    00153 //     o INCONSISTENT:  ALL literals are false.
    00154 //     o INDETERMINATE: There are no true literals, but some unknown literals as well.
    00155 ISATClause::ConsistencyType
    00156 ISATClause::get_consistency() const
    00157 {
    00158         // If there is at least one true literal, one of them should be the clause's
    00159         // satisfying literal.
    00160         if (get_satisfying_literal_p() != NULL || get_numb_of_literals() == 0)
    00161         {
    00162 #if defined(_DEBUG)
    00163                 if (get_numb_of_literals() > 0)
    00164                 {
    00165                         // If this clause does have a satisfying literal the truth value of the
    00166                         // satisfying literal should be true.
    00167                         assert(get_satisfying_literal_p()->get_truth_value() == ISATLiteral::TRUEVAL);
    00168                 }
    00169 #endif // #if defined(_DEBUG)
    00170
    00171                 // Since at least on literal satisfies this clause, it is consistent.
    00172                 return CONSISTENT;
    00173         }
    00174         // Otherwise, if there are no unresolved literals, the clause must be INCONSISTENT.
    00175         else if (numb_of_unresolved_literals == 0)
    00176         {
    00177 #ifdef DEBUG
    00178                 for (const_iterator const_it = begin(); const_it != end(); const_it++)
    00179                 {
    00180                         // If the clause was unit resolved, it should also be consistent.
    00181                         assert((*const_it)->get_truth_value() == ISATProposition::FALSEVAL);
    00182                 }
    00183 #endif // #ifdef DEBUG
    00184
    00185                 return INCONSISTENT;
    00186         }
    00187         // Otherwise, nothing is know of the clauses consistency yet.
    00188         {
    00189                 return INDETERMINATE;
    00190         }
    00191 }
    00192
    00193 // Returns true if this clause is a unit clause (i.e. a clause with one unassigned
    00194 // literal and all other literals assigned FALSEVAL) otherwise return false.
    00195 bool
    00196 ISATClause::is_unit_clause() const
    00197 {
    00198         // It is a unit clause if it has only 1 unresolved literal and no literal that
    00199         // satisfies this clause.
    00200         if (numb_of_unresolved_literals == 1 && get_satisfying_literal_p() == NULL)
    00201         {
    00202                 return true;
    00203         }
    00204         else
    00205         {
    00206                 return false;
    00207         }
    00208 }
    00209
    00210 // Returns true if this clause was unit resolved otherwise returns false.
    00211 bool
    00212 ISATClause::was_unit_resolved() const
    00213 {
    00214 #ifdef DEBUG
    00215         if (unit_resolved)
    00216         {
    00217                 // If the clause was unit resolved, it should also be consistent.
    00218                 assert(get_consistency() == CONSISTENT);
    00219         }
    00220         else
    00221         {
    00222                 assert(get_consistency() != CONSISTENT);
    00223         }
    00224 #endif // #ifdef DEBUG
    00225
    00226         return unit_resolved;
    00227 }
    00228
    00229 void
    00230 ISATClause::set_unit_resolved(bool boolean_value)
    00231 {
    00232         unit_resolved = boolean_value;
    00233 #ifdef DEBUG
    00234         if (unit_resolved)
    00235         {
    00236                 // If the clause was unit resolved, it should also be consistent.
    00237                 assert(get_consistency() == CONSISTENT);
    00238         }
    00239         else
    00240         {
    00241                 assert(get_consistency() != CONSISTENT);
    00242         }
    00243 #endif // #ifdef DEBUG
    00244 }
    00245
    00246 // Returns the literal whose truth value was assinged by unit resolution of the
    00247 // clause (i.e. a consequent is the literal that satisfies the clause if the clasue
    00248 // was unit resolved). If the clause was not unit resolved it returns NULL.
    00249 ISATLiteral const *
    00250 ISATClause::get_consequent_literal_p() const
    00251 {
    00252         if (was_unit_resolved())
    00253         {
    00254                 return satisfying_literal_p;
    00255         }
    00256         else
    00257         {
    00258                 return NULL;
    00259         }
    00260 }
    00261
    00262 // Find a literal that has not been resolved (i.e. the truth value is unknown) and
    00263 // return it. If all literals have been resolved, return NULL.
    00264 ISATLiteral const *
    00265 ISATClause::get_unresolved_literal_p() const
    00266 {
    00267         if (numb_of_unresolved_literals > 0)
    00268         {
    00269                 for (const_iterator const_it = begin(); const_it != end(); const_it++)
    00270                 {
    00271                         if (!(*const_it)->has_been_resolved())
    00272                         {
    00273                                 return *const_it;
    00274                         }
    00275                 }
    00276                 cerr << "*** Error: ISATClause::get_unresolved_literal_p() " <<
    00277                             " - Unresolved literal cannot be found. ***" << endl;
    00278                 return NULL;
    00279         }
    00280         else
    00281         {
    00282                 return NULL;
    00283         }
    00284 }
    00285
    00286 // Returns the literal whose truth value satisfies this clause. If this clause has a
    00287 // consequent, resulting from unit propagation, then the consequent will always be the
    00288 // satisfying literal.  Otherwise, the satisfying literal can be any literal that
    00289 // makes this clause TRUEVAL."
    00290 ISATLiteral const *
    00291 ISATClause::get_satisfying_literal_p() const
    00292 {
    00293         return satisfying_literal_p;
    00294 }
    00295
    00296 void
    00297 ISATClause::set_satisfying_literal(ISATLiteral const *literal_p)
    00298 {
    00299         // Should never try to set NULL as the satisfying literal.
    00300         assert(literal_p != NULL);
    00301
    00302         // The "literal" should not be set as the literal that satisfies this clause if it
    00303         // does not belong to this clause.
    00304         assert(literal_p->get_parent_clause_p() == this);
    00305
    00306         // The "literal" should not be set as the literal that satisfies this clause if it
    00307         // does not have the truth value of TRUEVAL.
    00308         assert(literal_p->get_truth_value() == ISATLiteral::TRUEVAL);
    00309
    00310
    00311         // Only if this clause does not have a satisfying literal, set the "literal"
    00312         // as the satisfying literal.
    00313         if (satisfying_literal_p == NULL)
    00314         {
    00315                 satisfying_literal_p = literal_p;
    00316         }
    00317 }
    00318
    00319 void
    00320 ISATClause::remove_from_satisfying_literals(ISATLiteral const *literal_p)
    00321 {
    00322         // Proceed only if the "literal" is the literal that satisfies this clause.
    00323         if (get_satisfying_literal_p() == literal_p)
    00324         {
    00325                 // This function should not be called if the literal does satisfy this clause.
    00326                 assert(literal_p->get_truth_value() != ISATLiteral::TRUEVAL);
    00327
    00328                 // This function should not be called if the literal had satisfied this clause
    00329                 // by unit resolution. If it was unit resolved, the unit resolution should have
    00330                 // been undone before removing the literal from the list of satisfying literals.
    00331                 assert(!was_unit_resolved());
    00332
    00333                 satisfying_literal_p = NULL;
    00334
    00335                 // Check if there is another literal in this clause that satisfies this clause.
    00336                 for (const_iterator const_it = begin(); const_it != end(); const_it++)
    00337                 {
    00338                         // If there is another literal whose value is TRUEVAL, set it as the
    00339                         // satisfying literal.
    00340                         if ((*const_it)->get_truth_value() == ISATLiteral::TRUEVAL)
    00341                         {
    00342                                 set_satisfying_literal(*const_it);
    00343
    00344                                 // Since a literal that satisfyies this clause was found, the search can
    00345                                 // be stopped and the removal of "literal" as the satisfying literal is
    00346                                 // done.
    00347                                 return;
    00348                         }
    00349                 }
    00350 //#if defined(_DEBUG)
    00351 //              if (satisfying_literal_p == NULL)
    00352 //              {
    00353 //                      assert(!is_consistent());
    00354 //              }
    00355 //#endif // #if defined(_DEBUG)
    00356         }
    00357 }
    00358
    00359 unsigned int
    00360 ISATClause::get_numb_of_literals() const
    00361 {
    00362         return size();
    00363 }
    00364
    00365 void
    00366 ISATClause::reset_status()
    00367 {
    00368         // Reset all fields to their default value.
    00369         satisfying_literal_p            = NULL;
    00370         numb_of_unresolved_literals     = get_numb_of_literals();
    00371         unit_resolved                           = false;
    00372
    00373         // Find the number of unresolved literals and the literal that satisfies this clause
    00374         // if there are any.
    00375         for (const_iterator const_it = begin(); const_it != end(); const_it++)
    00376         {
    00377                 if ((*const_it)->has_been_resolved()) {
    00378                         decrement_numb_of_unresolved_literals();
    00379                         if ((*const_it)->get_truth_value() == ISATLiteral::TRUEVAL)
    00380                         {
    00381                                 set_satisfying_literal(*const_it);
    00382                         }
    00383                 }
    00384         }
    00385 }
    00386
    00387 //........................................................................................
    00388
    00389 void
    00390 ISATClause::increment_numb_of_unresolved_literals()
    00391 {
    00392         numb_of_unresolved_literals++;
    00393         assert(numb_of_unresolved_literals <= get_numb_of_literals());
    00394 }
    00395
    00396 void
    00397 ISATClause::decrement_numb_of_unresolved_literals()
    00398 {
    00399         numb_of_unresolved_literals--;
    00400         //assert(numb_of_unresolved_literals >= 0);
    00401 }
    00402
    00403 // Returns true if the clause is active in theory and false if it is not.
    00404 bool
    00405 ISATClause::is_active() const
    00406 {
    00407         return active;
    00408 }
    00409
    00410 // Sets active.
    00411 void ISATClause::set_active(bool boolean_value)
    00412 {
    00413         active = boolean_value;
    00414 }
    00415
    00416 //........................................................................................
    00417
    00418 bool
    00419 ISATClause::add_literal(ISATLiteral *new_literal_p) {
    00420
    00421         // Only insert the new literal if it is not NULL.
    00422         if (new_literal_p != NULL)
    00423         {
    00424                 // Only insert the new literal if its proposition is not NULL.
    00425                 if (((ISATLiteral const *)new_literal_p)->get_proposition_p() != NULL)
    00426                 {
    00427                         // Check to varify that no literal with the equivalent proposition to the new
    00428                         // literal's proposition already exists in the clause. Two propositions are
    00429                         // equivalent if they have the same proposition description.
    00430                         const_iterator clause_const_it;
    00431                         for (clause_const_it = begin(); clause_const_it != end(); clause_const_it++)
    00432                         {
    00433                                 // The new literal's proposition is equivalent to the proposition of a
    00434                                 // literal already in the clause.
    00435                                 if (*(*clause_const_it)->get_proposition_p()->get_description_p() ==
    00436                                         *new_literal_p->get_proposition_p()->get_description_p())
    00437                                 {
    00438                                         // The new literal should not be added to this clause for two
    00439                                         // reasons. Since the the new literal's proposition is equivalent to
    00440                                         // the proposition of a literal already in the clause:
    00441                                         //
    00442                                         //     1. The new literal is redundant if the polarity of the two
    00443                                         //        literals are the same.
    00444                                         //
    00445                                         //     2. Adding the new literal into the clause will result in an
    00446                                         //        inconsistent clause if the polarity of the two literals
    00447                                         //        are opposite.
    00448
    00449                                         // Two literals have the same polarity (case 1).
    00450                                         if ((*clause_const_it)->get_polarity() == new_literal_p->get_polarity())
    00451                                         {
    00452 #ifdef _DEBUG
    00453                                                 cerr << "*** REDUNDANT: " << *new_literal_p << " was not added to "
    00454                                                          << *this << ". ***" << endl;
    00455 #endif
    00456
    00457                                                 // Delete the new literal.
    00458                                                 delete new_literal_p;
    00459
    00460                                                 // Adding the new literal is complete.
    00461                                                 return false;
    00462                                         }
    00463                                         // Otherwise, the two literals have the opposite polarity (case 2).
    00464                                         else
    00465                                         {
    00466                                                 // Notify this as an error.
    00467                                                 cerr << "*** Error: " << *new_literal_p << " cannot be added to "
    00468                                                          << *this << ". ***" << endl;
    00469
    00470                                                 // Delete the new literal.
    00471                                                 delete new_literal_p;
    00472
    00473                                                 // Adding the new literal is complete.
    00474                                                 return false;
    00475                                         }
    00476                                 }
    00477                                 // Otherwise, the new literal's proposition is not the same as the literal
    00478                                 // already in the clause.
    00479                                 else
    00480                                 {
    00481                                         // If they are not the same, their descriptions should not be the same
    00482                                         // either, since proposition description uniqueness is guarenteed
    00483                                         // through the theory.
    00484                                         assert (*(*clause_const_it)->get_proposition_p()->get_description_p()
    00485                                                 != *new_literal_p->get_proposition_p()->get_description_p());
    00486                                 }
    00487                         }
    00488                         // Insert the new literal to the end of the list.
    00489                         push_back(new_literal_p);
    00490
    00491                         // The literal should not know which clause it is in yet.
    00492                         assert(new_literal_p->get_parent_clause_p() == NULL);
    00493
    00494                         // Since the new literal is a part of this claue, set the literal's
    00495                         // clause to this.
    00496                         new_literal_p->set_parent_clause_p(this);
    00497
    00498                         // If the new literal has not been resolved, increment the number of unresolved
    00499                         // literal counter.
    00500                         if (new_literal_p->has_been_resolved() == false)
    00501                         {
    00502                                 increment_numb_of_unresolved_literals();
    00503                         }
    00504                         // Otherwise, if the new literal already has the value of TRUEVAL
    00505                         // and this clause does not have a literal that satisfies it, set the
    00506                         // new literal as the satisfies literal.
    00507                         else if (new_literal_p->get_truth_value() == ISATLiteral::TRUEVAL &&
    00508                                 get_satisfying_literal_p() == NULL)
    00509                         {
    00510                                 set_satisfying_literal(new_literal_p);
    00511                         }
    00512                         return true;
    00513                 }
    00514                 // The new literal has NULL proposition.
    00515                 else
    00516                 {
    00517                         cerr << "*** Error: The literal has NULL proposition." << endl;
    00518                         cerr << "           Continuing without adding the literal. ***" << endl;
    00519                         return false;
    00520                 }
    00521         }
    00522         // The new literal is NULL.
    00523         else
    00524         {
    00525                 cerr << "*** Error: The literal is NULL." << endl;
    00526                 cerr << "           Continuing without adding the literal. ***" << endl;
    00527                 return false;
    00528         }
    00529 }
    00530
    00531 //----------------------------------------------------------------------------------------
    00532 // Public Operators
    00533 //----------------------------------------------------------------------------------------
    00534
    00535 bool
    00536 ISATClause::operator ==(ISATClause const &other) const
    00537 {
    00538 //      ISATClause::const_iterator this_const_it;
    00539 //      ISATClause::const_iterator other_const_it;
    00540         if (this == &other)
    00541         {
    00542                 return true;
    00543         }
    00544 //      else
    00545 //      {
    00546 //              // Check if the clause type and size are the same.
    00547 //              if (this->type() != other.type() || this->size() != other.size())
    00548 //              {
    00549                         return false;
    00550 //              }
    00551 //              // Loop through all literals and check that they are the same.
    00552 //              else
    00553 //              {
    00554 //                      for (this_const_it = begin(), other_const_it = other.begin();
    00555 //                      this_const_it != end() && other_const_it != other.end();
    00556 //                      this_const_it++, other_const_it++)
    00557 //                      {
    00558 //                              if (*this_const_it != *other_const_it) return false;
    00559 //                      }
    00560 //                      return true;
    00561 //              }
    00562 //      }
    00563 }
    00564
    00565 bool
    00566 ISATClause::operator !=(ISATClause const &other) const
    00567 {
    00568         return !(*this == other);
    00569 }
    00570
    00571 /*ISATClause const &
    00572 ISATClause::operator =(ISATClause const &other)
    00573 {
    00574         if (this != &other)
    00575         {
    00576 //              clear();
    00577
    00578                 satisfying_literal_p            = NULL;
    00579                 numb_of_unresolved_literals     = 0;
    00580                 unit_resolved                           = false;
    00581                 active                                          = false;
    00582 //              list_size                                       = 0;
    00583 //              for (const_iterator const_it = other.begin(); const_it != other.end(); const_it++)
    00584 //              {
    00585 //                      insert_literal(new ISATLiteral(*const_it));
    00586 //              }
    00587         }
    00588         return (*this);
    00589 }*/
    00590
    00591 ISATClause const &
    00592 ISATClause::operator +=(ISATClause const &other)
    00593 {
    00594         if (this != &other)
    00595         {
    00596 //              for (const_iterator const_it = other.begin(); const_it != other.end();
    00597 //              const_it++)
    00598 //              {
    00599 //                      insert_literal(new ISATLiteral(*const_it));
    00600 //              }
    00601         }
    00602         return (*this);
    00603 }
    00604
    00605 //........................................................................................
    00606
    00607
    00608 namespace Mers {
    00609         namespace Solvers {
    00610                 namespace SAT {
    00611                         namespace ISAT {
    00612                                 ostream &
    00613                                 operator <<(ostream &stream, ISATClause const &clause)
    00614                                 {
    00615                                 //      stream << "(OR ";
    00616                                         stream << "(";
    00617                                         ISATClause::const_iterator const_it = clause.begin();
    00618                                         if (!clause.empty())
    00619                                         {
    00620                                                 stream << **const_it;
    00621                                                 const_it++;
    00622                                                 while (const_it != clause.end())
    00623                                                 {
    00624                                                         stream << " " << **const_it;
    00625                                                         const_it++;
    00626                                                 }
    00627                                         }
    00628                                         else
    00629                                         {
    00630                                                 stream << "true";
    00631                                         }
    00632                                         stream << ")";
    00633                                         return stream;
    00634                                 }
    00635
    00636                                 ostream &
    00637                                 operator <<(ostream &stream, ISATClause::ConsistencyType const &clause_consistency)
    00638                                 {
    00639                                         switch (clause_consistency)
    00640                                         {
    00641                                         case ISATClause::CONSISTENT:
    00642                                                 stream << "consistent";
    00643                                                 break;
    00644                                         case ISATClause::INCONSISTENT:
    00645                                                 stream << "inconsistent";
    00646                                                 break;
    00647                                         case ISATClause::INDETERMINATE:
    00648                                                 stream << "indeterminate";
    00649                                                 break;
    00650                                         default:
    00651                                                 cerr << "*** ERROR: operator <<(ostream, ISATTheory::ConsistencyType)" << endl;
    00652                                                 cerr << "           - Invalid theory consistency type. ***" << endl;
    00653                                                 break;
    00654                                         }
    00655                                         return stream;
    00656                                 }
    00657                         }
    00658                 }
    00659         }
    00660 }