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

# /Users/fpy/titan-1-5-MBARI/Mers/Solvers/SAT/ISAT/ISATUnassignedPropositions.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:                        ISATUnassignedPropositions.cpp
    00015 //
    00016 // Description:         Circularly linked list of proposition pointers. It follows the C++
    00017 //                                      Standard Template Library specifications.
    00018 //
    00019 //========================================================================================
    00020
    00021 #include <cstdio>
    00022 #include <cassert>
    00023 #include "ISATProposition.h"
    00024 #include "ISATUnassignedPropositions.h"
    00025
    00027
    00028 using namespace Mers::Solvers::SAT::ISAT;
    00029 using std::ostream;
    00030 using std::endl;
    00031
    00033 // Public Constructors, Copy Constructors, & Destructors
    00035
    00036 ISATUnassignedPropositions::ISATUnassignedPropositions()
    00037 {
    00038 }
    00039
    00040 /*
    00041 ISATUnassignedPropositions::ISATUnassignedPropositions(ISATUnassignedPropositions const &other)
    00042 {
    00043         for (const_iterator it = other.begin(); it != other.end(); it++)
    00044         {
    00045                 push_back(*it);
    00046         }
    00047 }
    00048 */
    00049
    00050 ISATUnassignedPropositions::~ISATUnassignedPropositions()
    00051 {
    00052 }
    00053
    00054 //----------------------------------------------------------------------------------------
    00055 // Public Function Members
    00056 //----------------------------------------------------------------------------------------
    00057
    00058 bool
    00059 ISATUnassignedPropositions::is_empty()
    00060 {
    00061         if (!empty())
    00062         {
    00063                 int s = size();
    00064                 assert(front() != NULL);
    00065                 while (s > 0 && front()->get_truth_value() != ISATProposition::UNKNOWNVAL)
    00066                 {
    00067                         pop_front();
    00068                         s--;
    00069                 }
    00070                 while (s > 0 && back()->get_truth_value() != ISATProposition::UNKNOWNVAL)
    00071                 {
    00072                         pop_back();
    00073                         s--;
    00074                 }
    00075                 return s == 0;
    00076         }else{
    00077                 return true;
    00078         }
    00079 }
    00080
    00081 void
    00082 ISATUnassignedPropositions::insert_proposition(ISATProposition *proposition_p)
    00083 {
    00084         assert(proposition_p->get_truth_value() == ISATProposition::UNKNOWNVAL);
    00085
    00086
    00087         //xx this is anothe quick fix similar to the one in ISATUnitClauses
    00088         for (iterator it = begin(); it != end(); it++)
    00089         {
    00090                 if (*it == proposition_p)
    00091                 {
    00092                         erase(it);
    00093                         break;
    00094                 }
    00095         }
    00096
    00097         push_front(proposition_p);
    00098
    00099         return;
    00100 }
    00101
    00102
    00103 void
    00104 ISATUnassignedPropositions::remove_proposition(ISATProposition *proposition_p)
    00105 {
    00106         for (iterator it = begin(); it != end(); it++)
    00107         {
    00108                 if (*it == proposition_p)
    00109                 {
    00110                         erase(it);
    00111                         return;
    00112                 }
    00113         }
    00114 }
    00115
    00116 ISATProposition *
    00117 ISATUnassignedPropositions::get_proposition_p()
    00118 {
    00119         if (is_empty())
    00120         {
    00121                 return NULL;
    00122         }
    00123         else
    00124         {
    00125                 assert(front() != NULL);
    00126                 assert(front()->get_truth_value() == ISATProposition::UNKNOWNVAL);
    00127                 return front();
    00128         }
    00129 }
    00130
    00131 //----------------------------------------------------------------------------------------
    00132 // Public Operators
    00133 //----------------------------------------------------------------------------------------
    00134 /*
    00135 ISATUnassignedPropositions const &
    00136 ISATUnassignedPropositions::operator =(ISATUnassignedPropositions const &other)
    00137 {
    00138         if (this != &other)
    00139         {
    00140                 clear();
    00141                 for (const_iterator it = other.begin(); it != other.end(); it++)
    00142                 {
    00143                         push_back(*it);
    00144                 }
    00145         }
    00146         return (*this);
    00147 }
    00148
    00149 ISATUnassignedPropositions const &
    00150 ISATUnassignedPropositions::operator +=(ISATUnassignedPropositions const &other)
    00151 {
    00152         if (this != &other)
    00153         {
    00154                 for (const_iterator it = other.begin(); it != other.end(); it++)
    00155                 {
    00156                         push_back(*it);
    00157                 }
    00158         }
    00159         return (*this);
    00160 }
    00161 */
    00162
    00163 namespace Mers {
    00164         namespace Solvers {
    00165                 namespace SAT {
    00166                         namespace ISAT {
    00167
    00168                                 ostream &
    00169                                 operator <<(ostream &stream, ISATUnassignedPropositions const &propositions)
    00170                                 {
    00171                                         stream << "(";
    00172                                         ISATUnassignedPropositions::const_iterator const_it = propositions.begin();
    00173                                         if (const_it != propositions.end())
    00174                                         {
    00175                                                 stream << **const_it << endl;
    00176                                                 const_it++;
    00177                                                 while (const_it != propositions.end())
    00178                                                 {
    00179                                                         stream << " " << **const_it << endl;
    00180                                                         const_it++;
    00181                                                 }
    00182                                         }
    00183                                         stream << ")";
    00184                                         return stream;
    00185                                 }
    00186                         }
    00187                 }
    00188         }
    00189 }
    00190