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

# /Users/fpy/titan-1-5-MBARI/Mers/Solvers/SAT/ISAT/ISATProposition.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:                        ISATProposition.cpp
    00015 //
    00016 // Description:         ISATProposition object holds information about a proposition
    00017 //
    00018 //========================================================================================
    00019
    00020 #include <cassert>
    00021 #include <cstdio>
    00022 #include "ISATPropositionDescription.h"
    00023 //#include "ISATClause.h"
    00024 #include "ISATLiteral.h"
    00025 #include "ISATLiterals.h"
    00026 #include "ISATProposition.h"
    00027
    00029
    00030 using namespace Mers::Solvers::SAT::ISAT;
    00031 using std::ostream;
    00032
    00034 // Public Constructors, Copy Constructors, & Destructors
    00036
    00037 ISATProposition::ISATProposition(ISATPropositionDescription const *new_description_p)
    00038 {
    00039         // A proposition with NULL description should never exist.
    00040         assert(new_description_p != NULL);
    00041
    00042         truth_value                     = UNKNOWNVAL;
    00043         description_p           = new_description_p;
    00044         positive_literals_p     = new ISATLiterals();
    00045         negative_literals_p     = new ISATLiterals();
    00046         guessed                         = false;
    00047         marked                          = false;
    00048 }
    00049
    00050 ISATProposition::~ISATProposition()
    00051 {
    00052         delete description_p;
    00053         delete positive_literals_p;
    00054         delete negative_literals_p;
    00055 }
    00056
    00057 //----------------------------------------------------------------------------------------
    00058 // Public Function Members
    00059 //----------------------------------------------------------------------------------------
    00060
    00061 // Returns the truth value of this proposition. The truth value may be TRUEVAL, FALSEVAL, or
    00062 // UNKNOWNVAL.
    00063 ISATProposition::TruthValueType
    00064 ISATProposition::get_truth_value() const
    00065 {
    00066         return truth_value;
    00067 }
    00068
    00069 // Sets the truth value of this proposition as TRUEVAL, FALSEVAL, or UNKNOWNVAL.
    00070 void
    00071 ISATProposition::set_truth_value(TruthValueType new_truth_value)
    00072 {
    00073         truth_value = new_truth_value;
    00074 }
    00075
    00076 // Returns this proposition's description. ISATDescription is an abstract class, and
    00077 // the real ISATDescription Type will depend on each ISAT application.
    00078 ISATPropositionDescription const *
    00079 ISATProposition::get_description_p() const
    00080 {
    00081         return description_p;
    00082 }
    00083 /*
    00084 // Returns the positive literals that contain this proposition.
    00085 ISATLiterals const *
    00086 ISATProposition::get_positive_literals_p() const
    00087 {
    00088         return positive_literals_p;
    00089 }
    00090 */
    00091 ISATLiterals *
    00092 ISATProposition::get_positive_literals_p() const
    00093 {
    00094         return positive_literals_p;
    00095 }
    00096 /*
    00097 // Returns the negative literals that contain this proposition.
    00098 ISATLiterals const *
    00099 ISATProposition::get_negative_literals_p() const
    00100 {
    00101         return negative_literals_p;
    00102 }
    00103 */
    00104 ISATLiterals *
    00105 ISATProposition::get_negative_literals_p() const
    00106 {
    00107         return negative_literals_p;
    00108 }
    00109
    00110 bool
    00111 ISATProposition::was_guessed() const
    00112 {
    00113         return guessed;
    00114 }
    00115
    00116 bool
    00117 ISATProposition::is_marked() const
    00118 {
    00119         return marked;
    00120 }
    00121 //----------------------------------------------------------------------------------------
    00122 // Public Operators
    00123 //----------------------------------------------------------------------------------------
    00124
    00125 bool
    00126 ISATProposition::operator ==(ISATProposition const &other) const
    00127 {
    00128         // A proposition with NULL description should never exist.
    00129         assert(description_p != NULL);
    00130         assert(other.get_description_p() != NULL);
    00131
    00132         // If the description and the truth value two propositions are equal, than they are
    00133         // also equal.
    00134         if (*description_p == *other.description_p && truth_value == other.truth_value)
    00135         {
    00136                 return true;
    00137         }
    00138         else
    00139         {
    00140                 return false;
    00141         }
    00142 }
    00143
    00144 bool ISATProposition::operator !=(ISATProposition const &other) const
    00145 {
    00146         return !(*this == other);
    00147 }
    00148
    00149 //----------------------------------------------------------------------------------------
    00150 // Private Function Members
    00151 //----------------------------------------------------------------------------------------
    00152
    00153 void
    00154 ISATProposition::insert_literal(ISATLiteral *literal_p)
    00155 {
    00156         // A literal must be either POSITIVE or NEGATIVE.
    00157         assert (literal_p->get_polarity() == ISATLiteral::POSITIVE ||
    00158                         literal_p->get_polarity() == ISATLiteral::NEGATIVE);
    00159
    00160         if (literal_p->get_polarity() == ISATLiteral::POSITIVE)
    00161         {
    00162                 positive_literals_p->insert_literal(literal_p);
    00163         }
    00164         else
    00165         {
    00166                 negative_literals_p->insert_literal(literal_p);
    00167         }
    00168 }
    00169
    00170 void
    00171 ISATProposition::remove_literal(ISATLiteral *literal_p)
    00172 {
    00173         // A literal must be either POSITIVE or NEGATIVE.
    00174         assert (literal_p->get_polarity() == ISATLiteral::POSITIVE ||
    00175                         literal_p->get_polarity() == ISATLiteral::NEGATIVE);
    00176
    00177         if (literal_p->get_polarity() == ISATLiteral::POSITIVE)
    00178         {
    00179                 positive_literals_p->remove_literal(literal_p);
    00180         }
    00181         else
    00182         {
    00183                 negative_literals_p->remove_literal(literal_p);
    00184         }
    00185 }
    00186
    00187 void
    00188 ISATProposition::set_guessed(bool guessed_truth_value)
    00189 {
    00190         guessed = guessed_truth_value;
    00191 }
    00192
    00193 void
    00194 ISATProposition::set_marked(bool mark)
    00195 {
    00196         marked = mark;
    00197 }
    00198
    00199 namespace Mers {
    00200         namespace Solvers {
    00201                 namespace SAT {
    00202                         namespace ISAT {
    00203
    00204                                 ostream &
    00205                                 operator <<(ostream &stream, ISATProposition const &proposition)
    00206                                 {
    00207                                         // A proposition with NULL description should never exist.
    00208                                         assert(proposition.get_description_p() != NULL);
    00209
    00210                                         proposition.get_description_p()->print(stream);
    00211                                         stream << " = ";
    00212                                         stream << proposition.get_truth_value();
    00213                                         return stream;
    00214                                 }
    00215
    00216                                 ostream &
    00217                                 operator <<(ostream &stream, ISATProposition::TruthValueType some_truth_value)
    00218                                 {
    00219                                         // A proposition's truth value should be one of TRUEVAL, FALSEVAL, or UNKNOWNVAL).
    00220                                         assert(some_truth_value == ISATProposition::TRUEVAL     ||
    00221                                                 some_truth_value == ISATProposition::FALSEVAL   ||
    00222                                                 some_truth_value == ISATProposition::UNKNOWNVAL);
    00223
    00224                                         switch (some_truth_value)
    00225                                         {
    00226                                         case ISATProposition::TRUEVAL:
    00227                                                 stream << "true";
    00228                                                 break;
    00229                                         case ISATProposition::FALSEVAL:
    00230                                                 stream << "false";
    00231                                                 break;
    00232                                         case ISATProposition::UNKNOWNVAL:
    00233                                                 stream << "unknown";
    00234                                                 break;
    00235                                         }
    00236                                         return stream;
    00237                                 }
    00238                         }
    00239                 }
    00240         }
    00241 }
    00242