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

# /Users/fpy/titan-1-5-MBARI/Mers/Solvers/SAT/ISAT/ISATLiteral.h

    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.h
    00015 //
    00016 // Description:         ISATLiteral object holds either positive or negative proposition
    00017 //                                      and a pointer to the clause it belongs to.
    00018 //
    00019 //========================================================================================
    00020 #ifndef ISAT_LITERAL_H__
    00021 #define ISAT_LITERAL_H__
    00022
    00023 #ifdef _MSC_VER
    00024 #pragma warning(disable:4786)
    00025 #endif // #if defined _MSC_VER
    00026
    00027 #include <iostream>
    00028
    00029 namespace Mers {
    00030         namespace Solvers {
    00031                 namespace SAT {
    00032                         namespace ISAT {
    00033
    00034                                 class ISATClause;
    00035                                 class ISATProposition;
    00036                                 class ISATTheory;
    00037
    00038
    00042                                 class ISATLiteral
    00043                                 {
    00044                                 public:
    00045                                         //------------------------------------------------------------------------------------
    00046                                         // Public Type Definitions, Constants, & Class Declarations
    00047                                         //------------------------------------------------------------------------------------
    00048
    00049                                         enum PolarityType               {POSITIVE, NEGATIVE};
    00050                                         enum TruthValueType     {TRUEVAL, FALSEVAL, UNKNOWNVAL};
    00051
    00052                                         //------------------------------------------------------------------------------------
    00053                                         // Friends
    00054                                         //------------------------------------------------------------------------------------
    00055
    00056                                 //      friend ISATTheory;
    00057                                         friend std::ostream &operator <<(std::ostream &stream, ISATLiteral::TruthValueType some_truth_value);
    00058                                         friend std::ostream &operator <<(std::ostream &_ostream, ISATLiteral const &literal);
    00059
    00060                                         //------------------------------------------------------------------------------------
    00061                                         // Public Constructors, Copy Constructors, & Destructors
    00062                                         //------------------------------------------------------------------------------------
    00063
    00064                                         ISATLiteral(ISATProposition *new_proposition_p, PolarityType literal_type);
    00065                                         ISATLiteral(ISATLiteral const &other);
    00066                                         virtual ~ISATLiteral();
    00067
    00068                                         //------------------------------------------------------------------------------------
    00069                                         // Public Function Members
    00070                                         //------------------------------------------------------------------------------------
    00071
    00072                                         // Returns true if the truth value of this literal is TRUEVAL or FALSEVAL, otherwise,
    00073                                         // returns false.
    00074                                         bool                    has_been_resolved() const;
    00075
    00076                                         // Returns the truth value of this literal (i.e. returns TRUEVAL if the proposition
    00077                                         // truth value is TRUEVAL and this literal is POSITIVE or if the proposition truth value
    00078                                         // is FALSEVAL and this literal is NEGATIVE). The truth value of the literal may be
    00079                                         // TRUEVAL, FALSEVAL, or UNKNOWNVAL.
    00080                                         TruthValueType          get_truth_value() const;
    00081
    00082                                         // Returns the type of this literal. A literal may be of POSITIVE or NEGATIVE type.
    00083                                         PolarityType                    get_polarity() const;
    00084
    00085                                         // Returns the proposition of this literal. This should never be NULL.
    00086                                         ISATProposition *               get_proposition_p() const;
    00087
    00088                                         //....................................................................................
    00089
    00090                                         // Returns the clause this literal belongs to. If this literal does not belong to any
    00091                                         // clause, it returns NULL.
    00092                                         ISATClause *                    get_parent_clause_p() const;
    00093
    00094                                         // Sets literal's owner to be the "clause".
    00095                                         void                    set_parent_clause_p(ISATClause *clause_p);
    00096
    00097                                         //------------------------------------------------------------------------------------
    00098                                         // Public Operators
    00099                                         //------------------------------------------------------------------------------------
    00100
    00101                                         bool                                    operator ==	(ISATLiteral const &other) const;
    00102                                         bool                                    operator !=	(ISATLiteral const &other) const;
    00103                                         ISATLiteral const &             operator =	(ISATLiteral const &other);
    00104
    00105                                 private:
    00106                                         //------------------------------------------------------------------------------------
    00107                                         // Private Constructors, Copy Constructors, & Destructors
    00108                                         //------------------------------------------------------------------------------------
    00109
    00110                                         // Since a literal with no proposition or type information is meaningless, this
    00111                                         // constructor with an empty argument should never be called. This was made private so
    00112                                         // that this can never be called from outside.
    00113                                         ISATLiteral();
    00114
    00115                                         //------------------------------------------------------------------------------------
    00116                                         // Private Function Members
    00117                                         //------------------------------------------------------------------------------------
    00118
    00119                                 //      void                                    set_proposition(ISATProposition const *new_proposition_p);
    00120
    00121                                         // Returns the proposition of this literal. This should never be NULL.
    00122                                 //      ISATProposition *               get_proposition_p();
    00123
    00124
    00125                                         // Returns the clause this literal belongs to. If this literal does not belong to any
    00126                                         // clause, it returns NULL.
    00127                                 //      ISATClause *                    get_parent_clause_p();
    00128
    00129                                         //------------------------------------------------------------------------------------
    00130                                         // Private Object & Data Members
    00131                                         //------------------------------------------------------------------------------------
    00132
    00133                                         // "type" is the type of this Literal. A literal may be of POSITIVE or NEGATIVE type.
    00134                                         PolarityType                    polarity;
    00135
    00136                                         // "proposition_p" is the pointer to the proposition of this literal. This should
    00137                                         // never be NULL.
    00138                                         ISATProposition *               proposition_p;
    00139
    00140                                         //....................................................................................
    00141
    00142                                         // "parent_clause_p" is the pointer to the clause this literal belongs to. If this
    00143                                         // literal does not belong to any clause, then the value is NULL.
    00144                                         ISATClause *                    parent_clause_p;
    00145
    00146                                 };
    00147                         }
    00148                 }
    00149         }
    00150 }
    00151
    00152 #endif // #if !defined ISAT_LITERAL