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

# /Users/fpy/titan-1-5-MBARI/Mers/Solvers/SAT/ISAT/ISATProposition.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:                        ISATProposition.h
    00015 //
    00016 // Description:         ISATProposition object holds information about a proposition
    00017 //
    00018 //========================================================================================
    00019 #ifndef ISAT_PROPOSITION_H__
    00020 #define ISAT_PROPOSITION_H__
    00021
    00022 #ifdef _MSC_VER
    00023 #pragma warning(disable:4786)
    00024 #endif // #if defined _MSC_VER
    00025
    00026 #include <iostream>
    00027
    00028 namespace Mers {
    00029         namespace Solvers {
    00030                 namespace SAT {
    00031                         namespace ISAT {
    00032
    00033                                 class ISATPropositionDescription;
    00034                                 class ISATPropositionDB;
    00035                                 class ISATLiteral;
    00036                                 class ISATLiterals;
    00037                                 class ISATTheory;
    00038
    00039
    00045                                 class ISATProposition
    00046                                 {
    00047                                 public:
    00048                                         //------------------------------------------------------------------------------------
    00049                                         // Type Definitions and Constants
    00050                                         //------------------------------------------------------------------------------------
    00051
    00052                                         // The truth value of a proposition may be TRUEVAL, FALSEVAL, or UNKNOWNVAL.
    00053                                         enum TruthValueType                     {TRUEVAL, FALSEVAL, UNKNOWNVAL};
    00054
    00055                                         //------------------------------------------------------------------------------------
    00056                                         // Friends
    00057                                         //------------------------------------------------------------------------------------
    00058
    00059                                         friend class ISATTheory;
    00060                                         friend class ISATPropositionDB;
    00061                                         friend std::ostream &operator <<	(std::ostream &stream, ISATProposition const &proposition);
    00062                                         friend std::ostream &operator <<	(std::ostream &stream, TruthValueType some_truth_value);
    00063
    00064                                         //------------------------------------------------------------------------------------
    00065                                         // Public Constructors, Copy Constructors, & Destructors
    00066                                         //------------------------------------------------------------------------------------
    00067
    00068                                         ISATProposition(ISATPropositionDescription const *new_description_p);
    00069                                         virtual ~ISATProposition();
    00070
    00071                                         //------------------------------------------------------------------------------------
    00072                                         // Public Function Members
    00073                                         //------------------------------------------------------------------------------------
    00074
    00075                                         // Returns the truth value of this proposition. The truth value may be TRUEVAL, FALSEVAL, or
    00076                                         // UNKNOWNVAL.
    00077                                         TruthValueType                          get_truth_value() const;
    00078
    00079                                         // Returns this proposition's description. ISATDescription is an abstract class, and
    00080                                         // the real ISATDescription Type will depend on each ISAT application.
    00081                                         ISATPropositionDescription const *get_description_p() const;
    00082
    00083                                         // Returns the positive literals that contain this proposition.
    00084                                 //      ISATLiterals const *            get_positive_literals_p() const;
    00085
    00086                                         // Returns the negative literals that contain this proposition.
    00087                                 //      ISATLiterals const *            get_negative_literals_p() const;
    00088
    00089                                         bool                                            was_guessed() const;
    00090
    00091                                         bool                                            is_marked() const;
    00092                                         //------------------------------------------------------------------------------------
    00093                                         // Public Operators
    00094                                         //------------------------------------------------------------------------------------
    00095
    00096                                         ISATProposition const &         operator =      (ISATProposition const &other);
    00097                                         bool                                            operator ==	(ISATProposition const &other) const;
    00098                                         bool                                            operator !=	(ISATProposition const &other) const;
    00099
    00100                                 private:
    00101                                         //------------------------------------------------------------------------------------
    00102                                         // Private Constructors, Copy Constructors, & Destructors
    00103                                         //------------------------------------------------------------------------------------
    00104
    00105                                         ISATProposition() {};
    00106                                         ISATProposition(ISATProposition const &other) { (void)other; };
    00107
    00108                                         //------------------------------------------------------------------------------------
    00109                                         // Private Function Members
    00110                                         //------------------------------------------------------------------------------------
    00111
    00112                                         // Returns the positive literals that contain this proposition.
    00113                                         ISATLiterals *                          get_positive_literals_p() const;
    00114
    00115                                         // Returns the negative literals that contain this proposition.
    00116                                         ISATLiterals *                          get_negative_literals_p() const;
    00117
    00118                                         // Inserts the literal into the corresponding positive or negative literals.
    00119                                         void                                            insert_literal(ISATLiteral *literal_p);
    00120
    00121                                         // Removes the literal from the corresponding positive or negative literals.
    00122                                         void                                            remove_literal(ISATLiteral *literal_p);
    00123
    00124                                         // Sets the truth value of this proposition as TRUEVAL, FALSEVAL, or UNKNOWNVAL.
    00125                                         void                                            set_truth_value(TruthValueType new_truth_value);
    00126
    00127                                         void                                            set_guessed(bool guessed_truth_value);
    00128
    00129                                         void                                            set_marked(bool mark);
    00130                                         //------------------------------------------------------------------------------------
    00131                                         // Private Object Members
    00132                                         //------------------------------------------------------------------------------------
    00133
    00134                                         // "truth_value" stores the current truth assignment to this proposition. The
    00135                                         // possible values are TRUEVAL, FALSEVAL, or UNKNOWNVAL.
    00136                                         TruthValueType                          truth_value;
    00137
    00138                                         // "description_p" is the proposition's description pointer. A theory may have at
    00139                                         // most one proposition with a given description. ISATDescription is an abstract
    00140                                         // class, and for each ISAT application a decription object must be defined by
    00141                                         // inheriting ISATDescription class.
    00142                                         ISATPropositionDescription const *      description_p;
    00143
    00144                                         // "positive_literals" is the list of literals in clauses that contain this
    00145                                         // proposition as a positive literal.
    00146                                         ISATLiterals *                          positive_literals_p;
    00147
    00148                                         // "negative_literals" is the list of literals in clauses that contain this
    00149                                         // proposition as a negative literal.
    00150                                         ISATLiterals *                          negative_literals_p;
    00151
    00152                                         bool                                            guessed;
    00153
    00154                                         bool                                            marked;
    00155
    00156                                 };
    00157                         }
    00158                 }
    00159         }
    00160 }
    00161
    00162 #endif // #if !defined ISAT_PROPOSITION
    00163