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

# /Users/fpy/titan-1-5-MBARI/Mers/Solvers/SAT/ISAT/ISATUnitClauses.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:                        ISATUnitClauses.cpp
    00015 //
    00016 // Description:
    00017 //
    00018 //
    00019 //========================================================================================
    00020
    00021 #include <cassert>
    00022 #include <cstdio>
    00023 #include "ISATClause.h"
    00024 #include "ISATUnitClauses.h"
    00025
    00027
    00028 using namespace Mers::Solvers::SAT::ISAT;
    00029 using std::ostream;
    00030
    00032 // Public Constructors, Copy Constructors, & Destructors
    00034
    00035 ISATUnitClauses::ISATUnitClauses()
    00036 {
    00037 }
    00038
    00039 ISATUnitClauses::~ISATUnitClauses()
    00040 {
    00041 }
    00042
    00043 //----------------------------------------------------------------------------------------
    00044 // Public Function Members
    00045 //----------------------------------------------------------------------------------------
    00046
    00047 bool
    00048 ISATUnitClauses::is_empty()
    00049 {
    00050         if (!empty())
    00051         {
    00052                 assert(front() != NULL);
    00053                 while (!empty() && (!front()->is_unit_clause() || !front()->is_active()))
    00054                 {
    00055                         pop_front();
    00056                 }
    00057                 while (!empty() && (!back()->is_unit_clause() || !back()->is_active()))
    00058                 {
    00059                         pop_back();
    00060                 }
    00061                 return (empty());
    00062         }else{
    00063                 return true;
    00064         }
    00065 }
    00066
    00067 void
    00068 ISATUnitClauses::insert_clause(ISATClause *clause_p)
    00069 {
    00070         // A clause that is not a unit clause should not be inserted.
    00071         assert(clause_p->is_unit_clause());
    00072
    00073         /*This is a quick fix!  Although the loop shouldn't added bugs to the code,
    00074         it may not be the most efficient way of solving the problem
    00075
    00076         removed_clause() (below) only removes the first instance of a clause
    00077         thus if a clause appears in the list of unit clauses more than once,
    00078         removed_clause() will not completely remove all instances of that clause from the list
    00079
    00080         added loop to check whether clause_p is already in the list of unit clauses
    00081         if yes, the function does not do anything
    00082         if not clause_p gets inserted
    00083         this ensures that a clause does not get inserted more than once
    00084
    00085         This loop is added because there are 2 lists of unit clauses in ISATTheory:
    00086         unit_clauses_p and current_unit_clauses_p
    00087         the latter is most used, however, unassigned_proposition() inserts to the first.
    00088         Thus the list, unit_clauses_p can end up with many pointers to 1 clause
    00089
    00090         This becomes a problem when removing clauses from the theory.  The list
    00091         of unit_clauses_p could point to a clause that's already been erased from
    00092         the database, which would cause the program to fail during the next propagation step.
    00093
    00094         May want to consider removing the unit_clauses_p list,
    00095         or keep better track of its elements.
    00096         In which case, the loop below may no longer be necessary.
    00097         */
    00098
    00099         for (iterator it = begin(); it != end(); it++)
    00100         {
    00101                 if (*it == clause_p)
    00102                 {
    00103                         return;
    00104                 }
    00105         }
    00106
    00107         push_back(clause_p);
    00108 }
    00109
    00110 void
    00111 ISATUnitClauses::remove_clause(ISATClause const *clause_p)
    00112 {
    00113         for (iterator it = begin(); it != end(); it++)
    00114         {
    00115                 if (*it == clause_p)
    00116                 {
    00117                         erase(it);
    00118                         return;
    00119
    00120                 }
    00121         }
    00122 }
    00123
    00124 ISATClause *
    00125 ISATUnitClauses::get_clause_p()
    00126 {
    00127         if (!is_empty())
    00128         {
    00129                 assert(front()->is_unit_clause());
    00130                 return front();
    00131         }
    00132         else
    00133         {
    00134                 // Since there are no unit clauses, return NULL.
    00135                 return NULL;
    00136         }
    00137 }
    00138
    00139 //----------------------------------------------------------------------------------------
    00140 // Ostream Operator <<
    00141 //----------------------------------------------------------------------------------------
    00142
    00143 namespace Mers {
    00144         namespace Solvers {
    00145                 namespace SAT {
    00146                         namespace ISAT {
    00147
    00148                                 ostream &
    00149                                 operator <<(ostream &stream, ISATUnitClauses const &clauses)
    00150                                 {
    00151                                         stream << "(";
    00152                                         ISATUnitClauses:: const_iterator const_it = clauses.begin();
    00153                                         if (const_it != clauses.end())
    00154                                         {
    00155                                                 stream << **const_it;
    00156                                                 const_it++;
    00157                                                 while (const_it != clauses.end())
    00158                                                 {
    00159                                                         stream << " " << **const_it;
    00160                                                         const_it++;
    00161                                                 }
    00162                                         }
    00163                                         stream << ")";
    00164                                         return stream;
    00165                                 }
    00166                         }
    00167                 }
    00168         }
    00169 }
    00170