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

# /Users/fpy/titan-1-5-MBARI/Mers/Solvers/SAT/ISAT/ISATLiteral.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:                        ISATLiteral.cpp
    00015 //
    00016 // Description:
    00017 //
    00018 //
    00019 //
    00020 //========================================================================================
    00021
    00022 #include <cstdio>
    00023 #include <cassert>
    00024 #include "ISATPropositionDescription.h"
    00025 #include "ISATProposition.h"
    00026 #include "ISATLiteral.h"
    00027
    00029
    00030 using namespace Mers::Solvers::SAT::ISAT;
    00031 using std::ostream;
    00032
    00034 // Public Constructors, Copy Constructors, & Destructors
    00036
    00037 ISATLiteral::ISATLiteral(ISATProposition *new_proposition_p, PolarityType literal_type)
    00038 {
    00039         polarity                = literal_type;
    00040         proposition_p   = new_proposition_p;
    00041         parent_clause_p = NULL;
    00042 }
    00043
    00044 ISATLiteral::ISATLiteral(ISATLiteral const &other)
    00045 {
    00046         polarity                = other.polarity;
    00047         proposition_p   = other.proposition_p;
    00048         parent_clause_p = other.parent_clause_p;
    00049 }
    00050
    00051 ISATLiteral::~ISATLiteral()
    00052 {
    00053         proposition_p   = NULL;
    00054         parent_clause_p = NULL;
    00055 }
    00056
    00057 //----------------------------------------------------------------------------------------
    00058 // Public Function Members
    00059 //----------------------------------------------------------------------------------------
    00060
    00061 // Returns true if the truth value of this literal is TRUEVAL or FALSEVAL, otherwise,
    00062 // returns false.
    00063 bool ISATLiteral::has_been_resolved() const
    00064 {
    00065         // A literal with NULL proposition should never exist.
    00066         assert(proposition_p != NULL);
    00067
    00068         // If the proposition has been assigned with a truth value, the literal has been
    00069         // resolved.
    00070         if (proposition_p->get_truth_value() != ISATProposition::UNKNOWNVAL)
    00071         {
    00072                 return true;
    00073         }
    00074         else
    00075         {
    00076                 return false;
    00077         }
    00078 }
    00079
    00080 // Returns the truth value of this literal (i.e. returns TRUEVAL if the proposition
    00081 // truth value is TRUEVAL and this literal is POSITIVE or if the proposition truth value
    00082 // is FALSEVAL and this literal is NEGATIVE). The truth value of the literal may be
    00083 // TRUEVAL, FALSEVAL, or UNKNOWNVAL.
    00084 ISATLiteral::TruthValueType
    00085 ISATLiteral::get_truth_value() const
    00086 {
    00087         // A literal must always be either POSITIVE or NEGATIVE.
    00088         assert(polarity == POSITIVE || polarity == NEGATIVE);
    00089
    00090         // A literal with NULL proposition should never exist.
    00091         assert(proposition_p != NULL);
    00092
    00093         // A proposition must have a truth value of TRUEVAL, FALSEVAL, or UNKNOWNVAL.
    00094         assert(proposition_p->get_truth_value() == ISATProposition::TRUEVAL     ||
    00095                    proposition_p->get_truth_value() == ISATProposition::FALSEVAL        ||
    00096                    proposition_p->get_truth_value() == ISATProposition::UNKNOWNVAL);
    00097
    00098         switch (proposition_p->get_truth_value())
    00099         {
    00100         case ISATProposition::TRUEVAL:
    00101                 // If the proposition's truth value is TRUEVAL and the literal is POSITIVE, the
    00102                 // truth value of the literal is TRUEVAL.
    00103                 if (polarity == POSITIVE)
    00104                 {
    00105                         return TRUEVAL;
    00106                 }
    00107                 // If the proposition's truth value is TRUEVAL and the literal is not POSITIVE
    00108                 // (i.e. NEGATIVE), the truth value of the literal is FALSEVAL.
    00109                 else
    00110                 {
    00111                         return FALSEVAL;
    00112                 }
    00113                 break;
    00114         case ISATProposition::FALSEVAL:
    00115                 // If the proposition's truth value is FALSEVAL and the literal is POSITIVE, the
    00116                 // truth value of the literal is FALSEVAL.
    00117                 if (polarity == POSITIVE)
    00118                 {
    00119                         return FALSEVAL;
    00120                 }
    00121                 // If the proposition's truth value is FALSEVAL and the literal is not POSITIVE
    00122                 // (i.e. NEGATIVE), the truth value of the literal is TRUEVAL.
    00123                 else
    00124                 {
    00125                         return TRUEVAL;
    00126                 }
    00127                 break;
    00128         default:
    00129                 // IF the propositoin's truth value is not TRUEVAL or FALSEVAL, it should be UNKNOWNVAL.
    00130                 // Then, the truth value of the literal is also UNKNOWNVAL regardless of the literal
    00131                 // polarity.
    00132                 return UNKNOWNVAL;
    00133         }
    00134 }
    00135
    00136 // Returns the polarity of this literal. A literal may be POSITIVE or NEGATIVE.
    00137 ISATLiteral::PolarityType
    00138 ISATLiteral::get_polarity() const
    00139 {
    00140         return polarity;
    00141 }
    00142
    00143 // Returns the proposition of this literal. This should never be NULL.
    00144 ISATProposition *
    00145 ISATLiteral::get_proposition_p() const
    00146 {
    00147         // A literal with NULL proposition should never exist.
    00148         assert(proposition_p != NULL);
    00149
    00150         return proposition_p;
    00151 }
    00152
    00153 //........................................................................................
    00154
    00155 // Returns the clause this literal belongs to. If this literal does not belong to any
    00156 // clause, it returns NULL.
    00157 ISATClause *
    00158 ISATLiteral::get_parent_clause_p() const
    00159 {
    00160         return parent_clause_p;
    00161 }
    00162
    00163 // Sets literal's owner to be the "clause".
    00164 void ISATLiteral::set_parent_clause_p(ISATClause *clause_p)
    00165 {
    00166         parent_clause_p = clause_p;
    00167 }
    00168
    00169
    00170 /*
    00171 // Returns the proposition of this literal. This should never be NULL.
    00172 ISATProposition *
    00173 ISATLiteral::get_proposition_p()
    00174 {
    00175         // A literal with NULL proposition should never exist.
    00176         assert(proposition_p != NULL);
    00177
    00178         return proposition_p;
    00179 }
    00180
    00181 //........................................................................................
    00182
    00183 // Returns the clause this literal belongs to. If this literal does not belong to any
    00184 // clause, it returns NULL.
    00185 ISATClause *
    00186 ISATLiteral::get_parent_clause_p()
    00187 {
    00188         return parent_clause_p;
    00189 }
    00190
    00191
    00192 */
    00193
    00194 //----------------------------------------------------------------------------------------
    00195 // Public Operators
    00196 //----------------------------------------------------------------------------------------
    00197
    00198 bool ISATLiteral::operator ==(ISATLiteral const &other) const
    00199 {
    00200         if (proposition_p == other.proposition_p && polarity == other.polarity)
    00201         {
    00202                 return true;
    00203         }
    00204         else
    00205         {
    00206                 return false;
    00207         }
    00208 }
    00209
    00210 bool
    00211 ISATLiteral::operator !=(ISATLiteral const &other) const
    00212 {
    00213         return !(*this == other);
    00214 }
    00215
    00216 ISATLiteral const &ISATLiteral::operator =(ISATLiteral const &other)
    00217 {
    00218         if (*this != other)
    00219         {
    00220                 polarity                        = other.polarity;
    00221                 proposition_p   = other.proposition_p;
    00222                 parent_clause_p = other.parent_clause_p;
    00223         }
    00224         return (*this);
    00225 }
    00226
    00227 //........................................................................................
    00228
    00229 namespace Mers {
    00230         namespace Solvers {
    00231                 namespace SAT {
    00232                         namespace ISAT {
    00233
    00234                                 ostream &
    00235                                 operator <<(ostream &stream, ISATLiteral const &literal)
    00236                                 {
    00237                                         if (literal.get_polarity() == ISATLiteral::NEGATIVE)
    00238                                         {
    00239                                 //              stream << "(NOT ";
    00240                                                 stream << "-";
    00241                                         }
    00242                                         else
    00243                                         {
    00244                                 //              stream << "(";
    00245                                         }
    00246                                         literal.get_proposition_p()->get_description_p()->print(stream);
    00247                                 //      stream << ")";
    00248                                         return stream;
    00249                                 }
    00250
    00251                                 ostream &
    00252                                 operator <<(ostream &stream, ISATLiteral::TruthValueType some_truth_value)
    00253                                 {
    00254                                         // A proposition's truth value should be one of TRUEVAL, FALSEVAL, or UNKNOWNVAL).
    00255                                         assert(some_truth_value == ISATLiteral::TRUEVAL ||
    00256                                                 some_truth_value == ISATLiteral::FALSEVAL       ||
    00257                                                 some_truth_value == ISATLiteral::UNKNOWNVAL);
    00258
    00259                                         switch (some_truth_value)
    00260                                         {
    00261                                         case ISATLiteral::TRUEVAL:
    00262                                                 stream << "true";
    00263                                                 break;
    00264                                         case ISATLiteral::FALSEVAL:
    00265                                                 stream << "false";
    00266                                                 break;
    00267                                         case ISATLiteral::UNKNOWNVAL:
    00268                                                 stream << "unknown";
    00269                                                 break;
    00270                                         }
    00271                                         return stream;
    00272                                 }
    00273                         }
    00274                 }
    00275         }
    00276 }
    00277
    00278
    00279 //----------------------------------------------------------------------------------------
    00280 // Private Constructors, Copy Constructors, & Destructors
    00281 //----------------------------------------------------------------------------------------
    00282
    00283 ISATLiteral::ISATLiteral()
    00284 {
    00285         parent_clause_p = NULL;
    00286         proposition_p   = NULL;
    00287         polarity                = POSITIVE;
    00288 }
    00289
    00290 //----------------------------------------------------------------------------------------
    00291 // Private Function Members
    00292 //----------------------------------------------------------------------------------------
    00293
    00294 /*
    00295 void
    00296 ISATLiteral::set_proposition(ISATProposition *new_proposition_p)
    00297 {
    00298         if (proposition_p != new_proposition_p)
    00299         {
    00300                 delete proposition_p;
    00301                 proposition_p = new_proposition_p;
    00302         }
    00303 }
    00304 */