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

# /Users/fpy/titan-1-5-MBARI/Mers/Solvers/SAT/ISAT/ISATClauseDB.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:                        ISATClauseDB.h
    00015 //
    00016 // Description:
    00017 //
    00018 //
    00019 //========================================================================================
    00020
    00021 #include <cassert>
    00022 #include <cstdio>
    00023 #include "ISATClause.h"
    00024 #include "ISATClauseDB.h"
    00025
    00027
    00028 using namespace Mers::Solvers::SAT::ISAT;
    00029 using std::list;
    00030 using std::ostream;
    00031 using std::endl;
    00032
    00034 // Public Constructors, Copy Constructors, & Destructors
    00036
    00037 ISATClauseDB::ISATClauseDB()
    00038 {
    00039 }
    00040
    00041 ISATClauseDB::~ISATClauseDB()
    00042 {
    00043         for (iterator it = begin(); it != end(); it++)
    00044         {
    00045                 delete *it;
    00046         }
    00047 }
    00048
    00049 //----------------------------------------------------------------------------------------
    00050 // Public Function Members
    00051 //----------------------------------------------------------------------------------------
    00052
    00053 void
    00054 ISATClauseDB::remove_clause(ISATClause const *clause_p)
    00055 {
    00056         for (iterator it = begin(); it != end(); it++)
    00057         {
    00058                 if (*it == clause_p)
    00059                 {
    00060                         delete *it;
    00061                         erase(it);
    00062                         return;
    00063                 }
    00064         }
    00065 }
    00066
    00067 //----------------------------------------------------------------------------------------
    00068 // Public Operators
    00069 //----------------------------------------------------------------------------------------
    00070
    00071 void
    00072 ISATClauseDB::operator +=(ISATClause *clause_p)
    00073 {
    00074         push_back(clause_p);
    00075 }
    00076
    00077 bool
    00078 ISATClauseDB::operator ==(ISATClauseDB const &other) const
    00079 {
    00080         ISATClauseDB::const_iterator this_const_it;
    00081         ISATClauseDB::const_iterator other_const_it;
    00082         if (this == &other)
    00083         {
    00084                 return true;
    00085         }
    00086         else
    00087         {
    00088                 if (this->size() != other.size())
    00089                 {
    00090                         return false;
    00091                 }
    00092                 else
    00093                 {
    00094                         for (this_const_it = begin(), other_const_it = other.begin();
    00095                         this_const_it != end() && other_const_it != other.end();
    00096                         this_const_it++, other_const_it++)
    00097                         {
    00098                                 if (**this_const_it != **other_const_it)
    00099                                 {
    00100                                         return false;
    00101                                 }
    00102                         }
    00103                         return true;
    00104                 }
    00105         }
    00106 }
    00107
    00108 bool
    00109 ISATClauseDB::operator !=(ISATClauseDB const &other) const
    00110 {
    00111         return !(*this == other);
    00112 }
    00113
    00114 namespace Mers {
    00115         namespace Solvers {
    00116                 namespace SAT {
    00117                         namespace ISAT {
    00118
    00119                                 ostream &
    00120                                 operator <<(ostream &stream, ISATClauseDB const &clause_database)
    00121                                 {
    00122                                 //      stream << "(";
    00123                                         ISATClauseDB::const_iterator const_it;
    00124                                         stream << "Clauses:";
    00125                                         for(const_it = clause_database.begin(); const_it != clause_database.end(); const_it++)
    00126                                         {
    00127                                                 ISATClause const * clause = *const_it;
    00128                                                 stream << endl << *clause;
    00129                                                 if (clause->is_active())
    00130                                                 {
    00131                                                         switch(clause->get_consistency()){
    00132                                                         case ISATClause::CONSISTENT:
    00133                                                                 stream << "  [Consistent]";
    00134                                                                 break;
    00135                                                         case ISATClause::INCONSISTENT:
    00136                                                                 stream << "  [Inconsistent]";
    00137                                                                 break;
    00138                                                         case ISATClause::INDETERMINATE:
    00139                                                                 stream << "  [Indeterminate]";
    00140                                                                 break;
    00141                                                         }
    00142
    00143                                                         if(clause->is_unit_clause()){
    00144                                                                 stream << " <Unit>";
    00145                                                         }
    00146
    00147                                                         if(clause->was_unit_resolved()){
    00148                                                                 stream << " {Unit Resolved}";
    00149                                                         }
    00150                                                 }else{
    00151                                                         stream << " --> INACTIVE";
    00152                                                 }
    00153                                         }
    00154                                         stream << endl;
    00155                                 //      stream << ")";
    00156                                         return stream;
    00157                                 }
    00158                         }
    00159                 }
    00160         }
    00161 }