/Users/fpy/titan-1-5-MBARI/Mers/Generators/BFIG/BFIGConstraint.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
//
//# CHECKED MJP 08-07-2002

#include "BFIGConstraint.h"

#include <cassert>
#include <iostream>
#include <vector>

#include "BFIGAssignment.h"
#include "BFIGImplicant.h"
#include "BFIGConstraintUnit.h"


using namespace Mers::Generators::BFIG;
using std::list;
using std::vector;
using std::ostream;


#ifdef _MSC_VER
#include "ListManipulator.h"
using Mers::Generators::BFIG::ListManipulator;
template ListManipulator<BFIGAssignment const *>;
#else
typedef bool (*assignment_comp_func)(BFIGAssignment const *, BFIGAssignment const *);
#endif


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


bool BFIGConstraint::terse = false;


BFIGConstraint::BFIGConstraint(bool noEssentialConflict_)
: constraintUnits(), essentialConflict(!noEssentialConflict_),
  primeImplicants(), primed(false)
{
}


BFIGConstraint::BFIGConstraint(BFIGAssignment const * a, bool positive)
: constraintUnits(), essentialConflict(false),
  primeImplicants(), primed(false)
{
        assert(a);
        addUnit(a, positive);
}


BFIGConstraint::BFIGConstraint(BFIGConstraintUnit const & cu)
: constraintUnits(), essentialConflict(false),
  primeImplicants(), primed(false)
{
        addUnit(cu);
}


/*#
//BFIGConstraint::BFIGConstraint(BFIGConstraint const & c)
//: constraintUnits(c.constraintUnits), essentialConflict(c.essentialConflict),
//  primeImplicants(c.primeImplicants), primed(c.primed)
//{
//}
*/


BFIGConstraint::BFIGConstraint(BFIGConstraint const & c)
: constraintUnits(), essentialConflict(c.essentialConflict),
  primeImplicants(), primed(c.primed)
{
        list<BFIGConstraintUnit>::const_iterator cIter;
        for (cIter = c.constraintUnits.begin(); cIter != c.constraintUnits.end(); cIter++)
        {
                constraintUnits.push_back(*cIter);
        }
        if (primed)
        {
                list<BFIGAssignment const *>::const_iterator aIter;
                for (aIter = c.primeImplicants.begin(); aIter != c.primeImplicants.end(); aIter++)
                {
                        primeImplicants.push_back((*aIter));
                }
        }
}


// Conflict constructor
BFIGConstraint::BFIGConstraint(vector<BFIGAssignment const *> const & inconsistentAssignments)
: constraintUnits(), essentialConflict(false),
  primeImplicants(), primed(false)
{
        vector<BFIGAssignment const *>::const_iterator aIter;
        for (aIter = inconsistentAssignments.begin();
             aIter != inconsistentAssignments.end(); aIter++)
        {
                assert((*aIter));
                addUnit((*aIter), false);
        }
}




BFIGConstraint::~BFIGConstraint()
{
}


BFIGConstraint
BFIGConstraint::withoutEnd()  const
{
        BFIGConstraint c(*this);
        if (!c.empty())
                c.constraintUnits.pop_back();
        c.primed = false;
        return c;
}


void
BFIGConstraint::addUnit(BFIGConstraintUnit const & unit)
{
        constraintUnits.push_back(unit);
        if (primed)
                addPrimeImplicants(unit);
}


void
BFIGConstraint::addUnit(BFIGAssignment const * a, bool parity)
{
        addUnit(BFIGConstraintUnit(a, parity));
}


bool
BFIGConstraint::isEmpty()  const
{
        return empty();
}

bool
BFIGConstraint::empty()  const
{
        return (!essentialConflict) && constraintUnits.empty();
}


unsigned int
BFIGConstraint::getSize()  const
{
        return size();
}

unsigned int
BFIGConstraint::size()  const
{
        return constraintUnits.size();
}


unsigned int
BFIGConstraint::primeImplicantSize()  const
{
        if (!primed)
                ((BFIGConstraint *)this)->makePrimeImplicants();
        return primeImplicants.size();
}


vector<BFIGAssignment const *>
BFIGConstraint::getAssignments()  const
{
        vector<BFIGAssignment const *> res;
        list<BFIGConstraintUnit>::const_iterator cIter;
        for (cIter = constraintUnits.begin(); cIter != constraintUnits.end(); cIter++)
        {
                assert((*cIter).getAssignment());
                res.push_back((*cIter).getAssignment());
        }
        return res;
}


list<BFIGConstraintUnit>
BFIGConstraint::getConstraintUnits()  const
{
        return constraintUnits;
}

/*
bool
BFIGConstraint::isSatisfiedCurrent(bool conjunctive)  const
{
        if (essentialConflict)
                return false;
        if (empty())
                return true;
        list<BFIGConstraintUnit>::const_iterator cIter;
        for (cIter = constraintUnits.begin(); cIter != constraintUnits.end(); cIter++)
        {
                if (!(*cIter).isSatisfiedCurrent())
                {
                        if (conjunctive)
                                return false;
                } else
                {
                        if (!conjunctive)
                                return true;
                }

        }
        if (conjunctive)
                return true;
        else
                return false;
}


bool
BFIGConstraint::maybeSatisfiedCurrent(bool conjunctive)  const
{
        if (essentialConflict)
                return false;
        if (empty())
                return true;
        list<BFIGConstraintUnit>::const_iterator cIter;
        for (cIter = constraintUnits.begin(); cIter != constraintUnits.end(); cIter++)
        {
                if (!(*cIter).maybeSatisfiedCurrent())
                {
                        if (conjunctive)
                                return false;
                } else
                {
                        if (!conjunctive)
                                return true;
                }

        }
        if (conjunctive)
                return true;
        else
                return false;
}
*/

vector<BFIGConstraint>
BFIGConstraint::negated()  const
{
        vector<BFIGConstraint> res;
        if (essentialConflict)  // should be empty constraint, then...
                return res;
        list<BFIGConstraintUnit>::const_iterator cIter;
        for (cIter = constraintUnits.begin(); cIter != constraintUnits.end(); cIter++)
        {
                res.push_back(BFIGConstraint((*cIter).negated()));
        }
        return res;
}


bool
BFIGConstraint::contains(BFIGAssignment const * a)  const
{
        list<BFIGConstraintUnit>::const_iterator cIter;
        for (cIter = constraintUnits.begin(); cIter != constraintUnits.end(); cIter++)
        {
                if ((*cIter).getAssignment() == a)
                        return true;
        }
        return false;
}


bool
BFIGConstraint::reduce(BFIGConstraintUnit const & cu)
{
        bool reduced = false;
        list<BFIGConstraintUnit>::iterator cIter;
        for (cIter = constraintUnits.begin(); cIter != constraintUnits.end(); )
        {
                if ((*cIter).getAssignment() == cu.getAssignment())
                {
                        if ((*cIter).getParity() == cu.getParity())  // satisfies it
                        {
                                constraintUnits.clear();
                                primed = false;
                                return true;
                        } else
                        {
                                cIter = constraintUnits.erase(cIter);
                                reduced = true;
                        }
                } else
                {
                        cIter++;
                }
        }
        if (reduced)
                primed = false;
        if (constraintUnits.empty())  // oops! violated...
        {
                essentialConflict = true;
        }
        return reduced;
}

/*
void
BFIGConstraint::sort()
{
        constraintUnits.sort();
}
*/


void
BFIGConstraint::clear()
{
        constraintUnits.clear();
        primed = false;
}


bool
BFIGConstraint::isEssentialConflict()  const
{
        return essentialConflict;
}


bool
BFIGConstraint::supportedBy(BFIGImplicant const * implicant) const
{
        vector<BFIGAssignment const *> assigns = implicant->getAssignments();
        vector<BFIGAssignment const *>::const_iterator aIter;
        for (aIter = assigns.begin(); aIter != assigns.end(); aIter++)
        {
                assert(*aIter);
                if (supportedBy((*aIter)))
                {
                        return true;
                }
        }
        return false;
}


bool
BFIGConstraint::supportedBy(BFIGAssignment const * a) const
{
        assert(a);
        BFIGVariable const * v = a->getVariable();
        list<BFIGConstraintUnit>::const_iterator cIter;
        for (cIter = constraintUnits.begin(); cIter != constraintUnits.end(); cIter++)
        {
                assert((*cIter).getAssignment());
                if ((*cIter).getAssignment()->getVariable() == v)
                {
                        if ((*cIter).getParity())
                        {
                                if ((*cIter).getAssignment() == a)
                                        return true;
                        } else
                        {
                                if ((*cIter).getAssignment() != a)
                                        return true;
                        }
                }
        }
        return false;
}


list<BFIGAssignment const *>
BFIGConstraint::getPrimeImplicants()  const
{
        if (!primed)
        {
                ((BFIGConstraint *)this)->makePrimeImplicants();
        }
        return primeImplicants;
}


void
BFIGConstraint::makePrimeImplicants()
{
        primeImplicants.clear();
        list<BFIGConstraintUnit>::const_iterator cIter;
        for (cIter = constraintUnits.begin(); cIter != constraintUnits.end(); cIter++)
        {
                if ((*cIter).getParity())
                {
                        primeImplicants.push_back((*cIter).getAssignment());
                } else
                {
                        list<BFIGAssignment const *> newAssigns =
                                (*cIter).getAssignment()->alternateAssignments();
                        primeImplicants.merge(newAssigns);
                }
        }
        // remove duplicates...
#ifdef _MSC_VER
        ListManipulator<BFIGAssignment const *> lm;
        lm.sort(primeImplicants, assignment_cost_less);
#else
        primeImplicants.sort<assignment_comp_func>(assignment_cost_less);
#endif
        primeImplicants.unique();

        primed = true;
}



void
BFIGConstraint::addPrimeImplicants(BFIGConstraintUnit const & cu)
{
        if (cu.getParity())
        {
                primeImplicants.push_back(cu.getAssignment());
        } else
        {
                list<BFIGAssignment const *> newAssigns =
                        cu.getAssignment()->alternateAssignments();
                primeImplicants.merge(newAssigns);
        }
        // remove duplicates...
#ifdef _MSC_VER
        ListManipulator<BFIGAssignment const *> lm;
        lm.sort(primeImplicants, assignment_cost_less);
#else
        primeImplicants.sort<assignment_comp_func>(assignment_cost_less);
#endif
        primeImplicants.unique();
}


bool
BFIGConstraint::operator==(BFIGConstraint const & c)  const
{
        // Assumes constraints are in minimal form:
        if (constraintUnits.size() != c.constraintUnits.size())
                return false;

        // Could also fail if they are not minimal:
        list<BFIGConstraintUnit> c1 = c.constraintUnits;
        c1.sort();
        list<BFIGConstraintUnit> c2 = constraintUnits;
        c2.sort();
        list<BFIGConstraintUnit>::const_iterator cu1Iter;
        list<BFIGConstraintUnit>::const_iterator cu2Iter;
        for (cu1Iter = c1.begin(), cu2Iter = c2.begin();
             cu1Iter != c1.end(); cu1Iter++, cu2Iter++)
        {
                if (!( (*cu1Iter) == (*cu2Iter) ))
                        return false;
        }

        return true;
}


bool
BFIGConstraint::operator<(BFIGConstraint const & c)  const
{
        if (size() < c.size())
                return true;
        if (size() > c.size())
                return false;

        list<BFIGConstraintUnit> c1 = constraintUnits;
        c1.sort();
        list<BFIGConstraintUnit> c2 = c.constraintUnits;
        c2.sort();
        list<BFIGConstraintUnit>::const_iterator c1Iter;
        list<BFIGConstraintUnit>::const_iterator c2Iter;
        for (c1Iter = c1.begin(), c2Iter = c2.begin();
             c1Iter != c1.end(); c1Iter++, c2Iter++)
        {
                if ((*c1Iter) == (*c2Iter))
                        continue;
                if ((*c1Iter) < (*c2Iter))
                        return true;
                return false;
        }

        return false;
}

namespace Mers {
        namespace Generators {
                namespace BFIG {

                        ostream&
                        operator<<(ostream& os, BFIGConstraint const & c)
                        {
                                //if (!c.terse)
                                os << "(";
                                if (c.constraintUnits.size() != 0)
                                {
                                        list<BFIGConstraintUnit>::const_iterator cIter;
                                        cIter = c.constraintUnits.begin();
                                        if (c.terse)
                                                os << (*cIter).getDescription();
                                        else
                                                os << (*cIter);
                                        for (cIter++; cIter != c.constraintUnits.end(); cIter++)
                                        {
                                                if (c.terse)
                                                        os << " ";
                                                else
                                                        os << " OR ";
                                                if (c.terse)
                                                        os << (*cIter).getDescription();
                                                else
                                                        os << (*cIter);
                                        }
                                }
                                if (c.isEssentialConflict())
                                        os << "X";
                                //if (!c.terse)
                                os << ")";
                                return os;
                        }
                }
        }
}

---