/Users/fpy/titan-1-5-MBARI/Mers/Generators/BFIG/BFIGImplicant.cpp

//
// Copyright (c) 2004           Model-based Embedded and Robotic Systems Group
// All Rights Reserved          Massachusetts Institute of Technology
//
// This software is provided as is. Model-based Embedded and Robotic Systems
// (MERS) group does not assume any responsibility.
//
// Organization:        Model-based Embedded and Robotic Systems Group
//                                      Massachusetts Institute of Technology
//

#include "BFIGImplicant.h"

#ifdef _MSC_VER
#pragma warning( disable : 4786 )
#endif

#include <cassert>
#include "BFIGAssignment.h"
#include "BFIGVariable.h"
#include "BFIGConstraint.h"
#include "BFIGObjectiveFunction.h"
#include "ListManipulator.h"

using namespace std;
using Mers::Generators::BFIG::BFIGImplicant;
using Mers::Generators::BFIG::BFIGVariable;
using Mers::Generators::BFIG::BFIGAssignment;
using Mers::Generators::BFIG::BFIGConstraint;
using Mers::Generators::BFIG::ListManipulator;
using Mers::Generators::BFIG::BFIGObjectiveFunction;



typedef bool (*assignment_comp_func)(BFIGAssignment const *, BFIGAssignment const *);
typedef bool (*constraint_comp_func)(BFIGConstraint const *, BFIGConstraint const *);


static bool
assignment_less(BFIGAssignment const * a1, BFIGAssignment const * a2)
{
        return ( (*a1) < (*a2) );
}


#ifdef IMPLICANT_EXTEND_ALL
static bool
assignment_cost_less(BFIGAssignment const * a1, BFIGAssignment const * a2)
{
        return ( a1->getCost() < a2->getCost() );
}
#endif


static bool
constraint_shorter_fallback(BFIGConstraint const * c1, BFIGConstraint const * c2)
{
        return ( (c1->primeImplicantSize() + (c1->getSize()<<1)) <
                 (c2->primeImplicantSize() + (c2->getSize()<<1)) );

}


static constraint_comp_func constraint_order = constraint_shorter_fallback;


static void
printAssignmentList(vector<BFIGAssignment const *> const & as)
{
        (void)printAssignmentList;
        cout << "(";
        vector<BFIGAssignment const *>::const_iterator aIter;
        bool start = true;
        for (aIter = as.begin(); aIter != as.end(); aIter++)
        {
                if (start)
                        start = false;
                else
                        cout << ", ";
                if (*aIter)
                        cout << *(*aIter);
                else
                        cout << "NULL";
        }
        cout << ")";
}


bool BFIGImplicant::terse = false;
Logger BFIGImplicant::mLogger(
        Logger::getInstance("Mers.Generators.BFIG.BFIGImplicant"));

//      CONSTRUCTOR

BFIGImplicant::BFIGImplicant(vector<BFIGAssignment const *> const & assignments_pList)
: assignments(assignments_pList), objectiveFunction(NULL),
  #ifdef IMPLICANT_ENABLE_UNSORTED
  assignmentsUnsorted(assignments_pList),
  #endif
  unentailedConflicts(), essentialConflict(false), markedFeasible(false),
  siblingAssignments(), siblingParent(NULL)
{
        // sort the assignments for comparison
        {
                ListManipulator<BFIGAssignment const *> lm;
                lm.sort(assignments, assignment_less);
        }
        //cout << endl << "  Imp Assignments:  "; printAssignmentList(assignments); cout << endl;
        bestCost = 0.0;
        vector<BFIGAssignment const *>::const_iterator assignmentIter;
        for (assignmentIter = assignments.begin(); assignmentIter != assignments.end();
             assignmentIter++)
        {
                assert(*assignmentIter);
                bestCost = bestCost + (*assignmentIter)->getCost();
        }
}


BFIGImplicant::BFIGImplicant(vector<BFIGConstraint const *> const & unentailedConflictsList, 
                BFIGObjectiveFunction const * of)
: assignments(), objectiveFunction(of),
#ifdef IMPLICANT_ENABLE_UNSORTED
  assignmentsUnsorted(),
#endif
  unentailedConflicts(unentailedConflictsList),
  essentialConflict(false), markedFeasible(false),
  siblingAssignments(), siblingParent(NULL)
{
        bestCost = 0.0;
}


BFIGImplicant::BFIGImplicant(vector<BFIGAssignment const *> const & assignments_pList,
                     vector<BFIGConstraint const *> const & unentailedConflictsList)
: assignments(assignments_pList), objectiveFunction(NULL),
#ifdef IMPLICANT_ENABLE_UNSORTED
  assignmentsUnsorted(assignments_pList),
#endif
  unentailedConflicts(unentailedConflictsList),
  essentialConflict(false), markedFeasible(false),
  siblingAssignments(), siblingParent(NULL)
{
        // sort the assignments for comparison
        {
                ListManipulator<BFIGAssignment const *> lm;
                lm.sort(assignments, assignment_less);
        }

        bestCost = 0.0;
        vector<BFIGAssignment const *>::const_iterator assignmentIter;
        for (assignmentIter = assignments.begin(); assignmentIter != assignments.end();
             assignmentIter++)
        {
                assert(*assignmentIter);
                bestCost = bestCost + (*assignmentIter)->getCost();
        }
}


BFIGImplicant::BFIGImplicant(bool noConflicts)
: assignments(), objectiveFunction(NULL),
  #ifdef IMPLICANT_ENABLE_UNSORTED
  assignmentsUnsorted(),
  #endif
  unentailedConflicts(),
  markedFeasible(false), siblingAssignments(), siblingParent(NULL)
{
        bestCost = 0.0;
        essentialConflict = !noConflicts;
}


BFIGImplicant::BFIGImplicant(const BFIGImplicant & i)
: assignments(i.assignments), objectiveFunction(i.objectiveFunction),
  #ifdef IMPLICANT_ENABLE_UNSORTED
  assignmentsUnsorted(i.assignmentsUnsorted),
  #endif
  unentailedConflicts(i.unentailedConflicts), bestCost(i.bestCost),
  essentialConflict(i.essentialConflict), markedFeasible(i.markedFeasible),
  siblingAssignments(i.siblingAssignments), siblingParent(NULL)
{
        if (i.siblingParent)
        {
                siblingParent = new BFIGImplicant(*(i.siblingParent));
        }
}


BFIGImplicant::~BFIGImplicant()
{
        if (siblingParent)
        {
                delete siblingParent;
        }
}


//private
// does not preserve the siblings of the source implicant!! Intentional.
BFIGImplicant::BFIGImplicant(BFIGImplicant const * parent, 
        BFIGAssignment const * extraAssign)
: assignments(parent->assignments), objectiveFunction(parent->objectiveFunction), 
#ifdef IMPLICANT_ENABLE_UNSORTED
  assignmentsUnsorted(parent->assignmentsUnsorted),
#endif
  unentailedConflicts(parent->unentailedConflicts), bestCost(parent->bestCost),
  essentialConflict(parent->essentialConflict), markedFeasible(false),
  siblingAssignments(vector<BFIGAssignment const *>()), siblingParent(NULL)
{
        LOG4CPLUS_DEBUG(mLogger, "BFIGImplicantCreateS: conflicts(" << 
                unentailedConflicts.size() << ')');

        addAssignment(extraAssign);

        LOG4CPLUS_DEBUG(mLogger, "Created BFIGImplicant: " << *this);
        LOG4CPLUS_DEBUG(mLogger, "With conflicts(" << unentailedConflicts.size() 
                << ')');
}


BFIGImplicant::BFIGImplicant(BFIGImplicant * parent, 
        BFIGAssignment const * extraAssign,
        vector<BFIGAssignment const *> siblingAssigns)
: assignments(parent->assignments), objectiveFunction(parent->objectiveFunction),
#ifdef IMPLICANT_ENABLE_UNSORTED
  assignmentsUnsorted(parent->assignmentsUnsorted),
#endif
        unentailedConflicts(parent->unentailedConflicts), bestCost(parent->bestCost),
  essentialConflict(parent->essentialConflict), markedFeasible(false),
  siblingAssignments(siblingAssigns), siblingParent(NULL)
{
        LOG4CPLUS_DEBUG(mLogger, "BFIGImplicantCreateS: conflicts(" << 
                unentailedConflicts.size() << ')');

        if (!siblingAssignments.empty())
        {
                siblingParent = parent;
#ifdef IMPLICANT_BASED_DP
                // rule out extensions that overlap this branch...
                siblingParent->addUnentailedConflict(extraAssign->getNegativeConstraint());
#endif
        } else {
                LOG4CPLUS_WARN(mLogger, "It is inefficient to create a sibling Implicant "
                        "with no siblings!");
                delete parent;
        }
        addAssignment(extraAssign);

        LOG4CPLUS_DEBUG(mLogger, "Created BFIGImplicantS: " << *this);
        LOG4CPLUS_DEBUG(mLogger, "With conflicts(" << unentailedConflicts.size() 
                << ')');
}

//      PUBLIC METHODS

void
BFIGImplicant::addAssignment(BFIGAssignment const * a)
{

#ifdef IMPLICANT_ENABLE_UNSORTED
        assignmentsUnsorted.push_back(a);
#endif
        vector<BFIGAssignment const *>::iterator aIter;
        for (aIter = assignments.begin(); aIter != assignments.end(); aIter++)
        {
                if ( (*a) < (*(*aIter)) )
                {
                        assignments.insert(aIter, a);
                        break;
                }
        }
        if (aIter == assignments.end())
        {
                assignments.push_back(a);
        }

        if(objectiveFunction != NULL)
                bestCost = objectiveFunction->getCost(assignments);
        else
                bestCost += a->getCost();

        // could fix unentailed conflicts here...
}


vector<BFIGAssignment const *>
BFIGImplicant::getAssignments() const
{
        return assignments;
}


vector<BFIGAssignment const *>
BFIGImplicant::getAssignmentsUnsorted() const
{
#ifdef IMPLICANT_ENABLE_UNSORTED
        return assignmentsUnsorted;
#else
        return assignments;
#endif
}


double
BFIGImplicant::getBestCost() const
{
        return bestCost;
}


double
BFIGImplicant::getTrueCost() const
{
        double res = 0.0;
        vector<BFIGAssignment const *>::const_iterator assignmentIter;
        for (assignmentIter = assignments.begin();
             assignmentIter != assignments.end();
             assignmentIter++)
        {
                res += (*assignmentIter)->getTrueCost();
        }
        return res;
}


void
BFIGImplicant::addUnentailedConflict(BFIGConstraint const * c)
{
        // Inefficent to merge in place here - temporary.
        vector<BFIGConstraint const *>::iterator iter;

        for (iter = unentailedConflicts.begin();
                iter != unentailedConflicts.end(); iter++)
        {
                if ( constraint_order(c, (*iter)) )
                {
                        unentailedConflicts.insert(iter, c);
                        break;
                }
        }

        if(iter == unentailedConflicts.end()) {
                unentailedConflicts.push_back(c);
        }

        if(siblingParent != NULL) {
                siblingParent->addUnentailedConflict(c);
        }

        LOG4CPLUS_DEBUG(mLogger, "Added 1 conflict to " << *this);
        LOG4CPLUS_DEBUG(mLogger, "Conf(" << unentailedConflicts.size() << ')');
}


void
BFIGImplicant::addUnentailedConflicts(vector<BFIGConstraint const *> const & cs)
{
        LOG4CPLUS_DEBUG(mLogger, "Conf(" << unentailedConflicts.size() << ')');

        vector<BFIGConstraint const *>::const_iterator iter;
        for (iter = cs.begin(); iter != cs.end(); iter++)
        {
                unentailedConflicts.push_back((*iter));
        }

        {
                ListManipulator<BFIGConstraint const *> lm;
                lm.sort(unentailedConflicts, constraint_order);
        }

        if(siblingParent != NULL) {
                siblingParent->addUnentailedConflicts(cs);
        }

        LOG4CPLUS_DEBUG(mLogger, "Added " << cs.size() << " conflicts to " << *this);
        LOG4CPLUS_DEBUG(mLogger, "Conf(" << unentailedConflicts.size() << ')');
}


bool
BFIGImplicant::entailsAllConflicts()  const
{
        if (essentialConflict)
                return false;
#ifdef CONFLICT_CHECK_STRICT
        return ((BFIGImplicant *)this)->entailsAllConflictsCheck();
#else
        return (unentailedConflicts.size() == 0);
#endif
}


bool
BFIGImplicant::entailsAllConflictsCheck()
{
        for (vector<BFIGConstraint const *>::iterator conflictIter = 
                                 unentailedConflicts.begin();
             conflictIter != unentailedConflicts.end();
             conflictIter = unentailedConflicts.erase(conflictIter))
        {
                assert(*conflictIter);
                if (!(*conflictIter)->supportedBy(this))
                        break;
        }

        return unentailedConflicts.empty();
}


void
BFIGImplicant::updateBestCost()
{
        bestCost = 0.0;
        vector<BFIGAssignment const *>::const_iterator assignmentIter;
        for (assignmentIter = assignments.begin(); assignmentIter != assignments.end();
             assignmentIter++)
        {
                bestCost += (*assignmentIter)->getCost();
        }
}


vector<BFIGImplicant *>
BFIGImplicant::generateChildren(vector<BFIGVariable *> const * varSet)
{
        vector<BFIGImplicant *> ext;
        
        // expand to children
        list<BFIGAssignment const *> supports;
        if (entailsAllConflictsCheck())
        {
                // No conflict needs to be covered, so...
                if (varSet)
                {
                        // extend to unspecified assignments - no particular order...
                        vector<BFIGVariable *>::const_iterator vIter;
                        for (vIter = varSet->begin(); vIter != varSet->end(); vIter++)
                        {
                                if(*vIter == NULL)
                                        continue;
                                if (!contains(*vIter))
                                {
#ifdef IMPLICANT_EXTEND_ALL
                                        vector<BFIGAssignment const *> newSupports = (*vIter)->getAssignmentsSorted();
#ifdef _MSC_VER
                                        ListManipulator<BFIGAssignment const *> lm;
                                        lm.merge(supports, newSupports, assignment_cost_less);
#else
                                        supports.merge<assignment_comp_func>(newSupports, assignment_cost_less);
#endif
#else
                                        // this one is free...
                                        vector<BFIGAssignment const *> vSupports = (*vIter)->getAssignmentsSorted();
                                        for(unsigned int v = 0; v < vSupports.size(); v++){
                                                supports.push_back(vSupports[v]);
                                        }
                                        // could search for smallest one here...
                                        break;
#endif
                                }
                        }
/*#
                        //#ifdef IMPLICANT_EXTEND_ALL
                        //ListManipulator<BFIGAssignment const *> lm;
                        //lm.sort(supports, assignment_cost_less);
                        //#endif
                        // else, all variables are already in implicant...
*/
                } else
                {
                        // can't extend to non-conflict-resolving assigns without knowing the variables.
                }
        } else
        {
                // we will cover another conflict
                BFIGConstraint const * firstConflict = unentailedConflicts.front();
                supports = firstConflict->getPrimeImplicants();
        }
/*#
        //      ListManipulator<BFIGAssignment *> lm;
        //      lm.sort(supports, assignment_cost_less);
*/
        // find first consistent support
        BFIGAssignment const * bestExtension = NULL;
        list<BFIGAssignment const *>::iterator sIter = supports.begin();
        while(sIter != supports.end())
        {
                bestExtension = *sIter;
                sIter = supports.erase(sIter);
                if (bestExtension->compatible(assignments))
                        break;
                else
                        bestExtension = NULL;
        }
        //unsigned int x = 0;
        //while (x < supports.size())
        //{
        //      bestExtension = supports[x++];
        //      if (bestExtension->compatible(assignments))
        //              break;
        //      else
        //              bestExtension = NULL;
        //}
        //supports.erase(supports.begin(), supports.begin() + x - 1);
        if (bestExtension)
        {
                BFIGImplicant * imp;
                if (supports.empty())
                {
                        imp = new BFIGImplicant(this, bestExtension);
                } else
                {
                        assert(!siblingParent);
                        BFIGImplicant * newParent = new BFIGImplicant(*this);
                        vector<BFIGAssignment const *> vSupports;
                        for(sIter = supports.begin(); sIter != supports.end(); sIter++){
                                vSupports.push_back(*sIter);
                        }
                        imp = new BFIGImplicant(newParent, bestExtension, vSupports);
                        // imp now owns the new memory...
                }

                // merge in order of cost
                if (ext.empty())
                {
                        ext.push_back(imp);
                } else
                {
                        assert(ext.size() == 1);
                        if (ext.front()->getBestCost() < imp->getBestCost())
                                ext.push_back(imp);
                        else{
                                ext.push_back(ext.front());
                                ext[0] = imp;
                        }
                }
        }

        return ext;
}


BFIGImplicant * BFIGImplicant::generateSibling()
{
        BFIGImplicant * sibimp = NULL;

        // this one has been expanded before...
        if (siblingParent != NULL)
        {
                BFIGAssignment const * nextSiblingAssign = NULL;
                unsigned int x = 0;

                while (x < siblingAssignments.size())
                {
                        nextSiblingAssign = siblingAssignments[x++];
                        if (nextSiblingAssign->compatible(siblingParent->assignments))
                                break;
                        else
                                nextSiblingAssign = NULL;
                }

                siblingAssignments.erase(siblingAssignments.begin(), 
                        siblingAssignments.begin() + x);

                if (nextSiblingAssign == NULL)
                {
                        // all done with siblings
                        // let it go...
                        delete siblingParent;
                } else {
                        if (!siblingAssignments.empty())
                        {
                                sibimp = new BFIGImplicant(siblingParent, nextSiblingAssign,
                                        siblingAssignments);
                                // sibimp now owns siblingParent memory...
                        } else {
                                sibimp = new BFIGImplicant(siblingParent, nextSiblingAssign);
                                delete siblingParent;
                        }
                }
                
                siblingParent = NULL;
                siblingAssignments.clear();
        }

        return sibimp;
}


vector<BFIGConstraint const *>
BFIGImplicant::getConstraints()  const
{
        vector<BFIGConstraint const *> res;
        vector<BFIGAssignment const *>::const_iterator aIter;
        for (aIter = assignments.begin(); aIter != assignments.end(); aIter++)
        {
                res.push_back((*aIter)->getConstraint());
        }
        return res;
}


void
BFIGImplicant::markFeasible()
{
        markedFeasible = true;
}


bool
BFIGImplicant::isMarkedFeasible()  const
{
        return markedFeasible;
}


BFIGImplicant *
BFIGImplicant::extendByAssignment(BFIGAssignment const * a) const
{
        BFIGImplicant * ext = new BFIGImplicant(this, a);
        return ext;
}


bool
BFIGImplicant::isEmpty() const
{
        return (assignments.size() == 0);
}


unsigned int
BFIGImplicant::getLength() const
{
        return assignments.size();
}


bool
BFIGImplicant::contains(BFIGAssignment const * a)  const
{
        vector<BFIGAssignment const *>::const_iterator aIter;
        for (aIter = assignments.begin(); aIter != assignments.end(); aIter++)
        {
                if (a == (*aIter))  // pointer comparison
                        return true;
        }

        return false;
}


bool
BFIGImplicant::contains(BFIGVariable const * v)  const
{
        vector<BFIGAssignment const *>::const_iterator aIter;
        for (aIter = assignments.begin(); aIter != assignments.end(); aIter++)
        {
                if (v == (*aIter)->getVariable())  // pointer comparison
                        return true;
        }

        return false;
}


bool
BFIGImplicant::compatible(BFIGAssignment const * a)  const
{
        vector<BFIGAssignment const *>::const_iterator aIter;
        for (aIter = assignments.begin(); aIter != assignments.end(); aIter++)
        {
                if (!a->compatible((*aIter)))
                        return false;
        }

        return true;
}


bool
BFIGImplicant::compatible(BFIGImplicant const & i)  const
{
        vector<BFIGAssignment const *>::const_iterator aIter;
        for (aIter = assignments.begin(); aIter != assignments.end(); aIter++)
        {
                if (!i.compatible((*aIter)))
                        return false;
        }

        return true;
}


void
BFIGImplicant::eliminateSiblings()
{
        if (siblingParent)
                delete siblingParent;
        siblingParent = NULL;
        siblingAssignments.clear();
}


bool
BFIGImplicant::hasSiblings()  const
{
        return !siblingAssignments.empty();
}


bool
BFIGImplicant::removeCurrentSibling()
{
        if (siblingAssignments.empty())  // invalid! no more siblings!
        {
                if (siblingParent)
                        delete siblingParent;
                clear(false);
                return false;
        }

        if (!siblingParent)
        {
                cerr << "Implicant cannot removeCurrentSibling with no parent!" << endl;
                clear(false);
                return false;
        }

        BFIGAssignment const * nextSiblingAssign = NULL;
        unsigned int sib = 0;
        while (sib < siblingAssignments.size())
        {
                nextSiblingAssign = siblingAssignments[sib++];
                if (nextSiblingAssign->compatible(siblingParent->assignments))
                        break;
        }
        siblingAssignments.erase(siblingAssignments.begin(),
                siblingAssignments.begin() + sib);
        if (!nextSiblingAssign)  // all done with siblings
        {
                delete siblingParent;
                clear(false);
                return false;
        }

        // replace the current sibling
        assignments = siblingParent->assignments;
#ifdef IMPLICANT_ENABLE_UNSORTED
        assignmentsUnsorted = siblingParent->assignmentsUnsorted;
#endif
        unentailedConflicts = siblingParent->unentailedConflicts;
        bestCost = siblingParent->bestCost;
        essentialConflict = siblingParent->essentialConflict;
        markedFeasible = false;  // ???
        sib = 0;
        if (!siblingAssignments.empty())
        {
                // add in conflict to prevent redundant searching
#ifdef IMPLICANT_BASED_DP
                siblingParent->addUnentailedConflict(nextSiblingAssign->getNegativeConstraint());
#endif
        } else
        {
                delete siblingParent;
                siblingParent = NULL;
        }
        addAssignment(nextSiblingAssign);

        return true;
}


// leaves it invalid, really:
void
BFIGImplicant::clear(bool noConflict)
{
        eliminateSiblings();
        assignments.clear();
#ifdef IMPLICANT_ENABLE_UNSORTED
        assignmentsUnsorted.clear();
#endif
        unentailedConflicts.clear();
        essentialConflict = noConflict;
}


bool
BFIGImplicant::operator==(BFIGImplicant const * i)  const
{
        if (!i)
                return false;
        return (*this) == (*i);
}


bool
BFIGImplicant::operator==(BFIGImplicant const & i)  const
{
        if (assignments.size() != i.assignments.size())
                return false;
        if (essentialConflict != i.essentialConflict)
                return false;
        /*# hack, for speed. Very distasteful...: */
        double diff = getBestCost() - i.getBestCost();
        if (diff < 0.0)  diff = -diff;
        if (diff > 0.0000001)  //# ugly... even if both best costs are right...
                return false;

        // assignments are sorted:
        vector<BFIGAssignment const *>::const_iterator a1Iter;
        vector<BFIGAssignment const *>::const_iterator a2Iter;
        for (a1Iter = assignments.begin(), a2Iter = i.assignments.begin();
             a1Iter != assignments.end(); a1Iter++, a2Iter++)
        {
                //if (!( (*(*a1Iter)) == (*(*a2Iter)) ))
                if (!( (*a1Iter) == (*a2Iter) ))  // just use pointer comparison
                        return false;
        }

        return true;
}


bool
BFIGImplicant::operator <(BFIGImplicant const &other)  const
{
        double cost = getBestCost();
        double otherCost = other.getBestCost();
        if(cost < otherCost)
                return true;
        if(cost > otherCost)
                return false;

        bool entailsAll = entailsAllConflicts();
        bool otherEntailsAll = other.entailsAllConflicts();
        if (entailsAll && !otherEntailsAll)
                return true;

        return false;
}


bool
BFIGImplicant::operator >(BFIGImplicant const &other)  const
{
        double cost = getBestCost();
        double otherCost = other.getBestCost();
        if(cost > otherCost)
                return true;
        if(cost < otherCost)
                return false;

        bool entailsAll = entailsAllConflicts();
        bool otherEntailsAll = other.entailsAllConflicts();
        if (!entailsAll && otherEntailsAll)
                return true;

        return false;
}


namespace Mers {
        namespace Generators {
                namespace BFIG {
                        ostream&
                        operator<<(ostream& os, BFIGImplicant const & in)
                        {
                                os << "[" ;
                                if (!in.terse)
                                        os << in.getBestCost() << ": " ;

                                vector<BFIGAssignment const *> assigns = in.assignments;
                                {
                                        ListManipulator<BFIGAssignment const *> lm;
                                        lm.sort(assigns, assignment_less);
                                }
                                bool first = true;
                                vector<BFIGAssignment const *>::const_iterator assignmentIter;
                                for (assignmentIter = assigns.begin();
                                                 assignmentIter != assigns.end(); assignmentIter++)
                                {
                                        if (first)
                                                first = false;
                                        else
                                                if (in.terse)
                                                        os << " ";
                                                else
                                                        os << ", ";
                                        os << *(*assignmentIter) ;
                                }
                                if (in.essentialConflict)
                                        os << " X";
                                if(!in.terse) {
                                        if(!in.entailsAllConflicts())
                                                os << " C";
                                }
                                os << "]";
                                return os;
                        }
                }
        }
}

---