381 lines
13 KiB
Plaintext
381 lines
13 KiB
Plaintext
|
// -*- c++ -*-
|
||
|
|
//=============================================================================
|
||
|
|
// Copyright (C) 2011 by Denys Duchier
|
||
|
|
//
|
||
|
|
// This program is free software: you can redistribute it and/or modify it
|
||
|
|
// under the terms of the GNU Lesser General Public License as published by the
|
||
|
|
// Free Software Foundation, either version 3 of the License, or (at your
|
||
|
|
// option) any later version.
|
||
|
|
//
|
||
|
|
// This program is distributed in the hope that it will be useful, but WITHOUT
|
||
|
|
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
|
||
|
|
// FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for
|
||
|
|
// more details.
|
||
|
|
//
|
||
|
|
// You should have received a copy of the GNU Lesser General Public License
|
||
|
|
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||
|
|
//=============================================================================
|
||
|
|
#include "disjunctor.hh"
|
||
|
|
|
||
|
|
namespace Gecode { namespace Disjunctor_ {
|
||
|
|
|
||
|
|
//=========================================================================
|
||
|
|
// Disjunctor (following example in MPG)
|
||
|
|
//=========================================================================
|
||
|
|
|
||
|
|
struct DisjunctorObject: public LocalObject
|
||
|
|
{
|
||
|
|
int n;
|
||
|
|
DisjunctorObject(Space& home) : LocalObject(home), n(0) {}
|
||
|
|
DisjunctorObject(Space& home, bool share, DisjunctorObject& d)
|
||
|
|
: LocalObject(home, share, d), n(d.n) {}
|
||
|
|
virtual LocalObject* copy(Space& home, bool share)
|
||
|
|
{ return new (home) DisjunctorObject(home, share, *this); }
|
||
|
|
virtual size_t dispose(Space&) { return sizeof(*this); }
|
||
|
|
};
|
||
|
|
|
||
|
|
Disjunctor::Disjunctor(): LocalHandle() {}
|
||
|
|
Disjunctor::Disjunctor(Space& home)
|
||
|
|
: LocalHandle(new (home) DisjunctorObject(home)) {}
|
||
|
|
Disjunctor::Disjunctor(const Disjunctor& d): LocalHandle(d) {}
|
||
|
|
int Disjunctor::get() const { return static_cast<DisjunctorObject*>(object())->n; }
|
||
|
|
void Disjunctor::incr() { static_cast<DisjunctorObject*>(object())->n += 1; }
|
||
|
|
void Disjunctor::decr() { static_cast<DisjunctorObject*>(object())->n -= 1; }
|
||
|
|
void Disjunctor::dispose(Space& home)
|
||
|
|
{ static_cast<DisjunctorObject*>(object())->dispose(home); }
|
||
|
|
|
||
|
|
//=========================================================================
|
||
|
|
// Forwarder<View>
|
||
|
|
// used to forward the domain of a view V1 into a view V2 located in a
|
||
|
|
// subspace (the subspace of a speculative clause). V2 represents V1 in
|
||
|
|
// that space.
|
||
|
|
//
|
||
|
|
// BasicForwarder
|
||
|
|
// base class of all Forwarders. It declares the virtual functions
|
||
|
|
// that must be implemented to do the actual work, and contains the pointer
|
||
|
|
// implementing the singly-linked list of Forwarders associated with each
|
||
|
|
// clause. It also redefines new and delete to manage memory in the
|
||
|
|
// subspace.
|
||
|
|
//=========================================================================
|
||
|
|
|
||
|
|
struct BasicForwarder
|
||
|
|
{
|
||
|
|
BasicForwarder* next;
|
||
|
|
|
||
|
|
BasicForwarder() : next(NULL) {}
|
||
|
|
|
||
|
|
// forward V1's domain into V2. This is used each time the Clause (as a
|
||
|
|
// a propagator) is woken to perform propagation.
|
||
|
|
|
||
|
|
virtual ExecStatus forward_in(Space& inner_home) = 0;
|
||
|
|
|
||
|
|
// forward V2's domain into V1. This is used after propagation in the
|
||
|
|
// case where the Clause has been committed to (because it is the last
|
||
|
|
// one remaining).
|
||
|
|
|
||
|
|
virtual void forward_out(Space& outer_home) = 0;
|
||
|
|
|
||
|
|
// needed by delete to know how much to free
|
||
|
|
virtual size_t size() const = 0;
|
||
|
|
|
||
|
|
// usage: new (home) FRWRDR(...);
|
||
|
|
// to allocate the instance of FRWRDR on home's heap
|
||
|
|
|
||
|
|
static void* operator new(size_t n, Space& home)
|
||
|
|
{ return home.ralloc(n); }
|
||
|
|
|
||
|
|
// usage: delete (home) PTR;
|
||
|
|
// to free the instance pointed to by PTR from home's heap
|
||
|
|
|
||
|
|
static void operator delete(void* ptr, Space& home)
|
||
|
|
{ home.rfree(ptr, ((BasicForwarder*)ptr)->size()); }
|
||
|
|
|
||
|
|
virtual BasicForwarder*
|
||
|
|
copy(Space& outer_home, Space& inner_home, bool share) = 0;
|
||
|
|
|
||
|
|
virtual void cancel(Space& home, Clause&) = 0;
|
||
|
|
};
|
||
|
|
|
||
|
|
// Forwarder parametrized by View
|
||
|
|
|
||
|
|
template <typename View>
|
||
|
|
struct Forwarder: public BasicForwarder
|
||
|
|
{
|
||
|
|
View outer;
|
||
|
|
View inner;
|
||
|
|
Forwarder(View v1, View v2): outer(v1), inner(v2) {}
|
||
|
|
Forwarder() {}
|
||
|
|
virtual ExecStatus forward_in(Space& home);
|
||
|
|
virtual void forward_out(Space& home);
|
||
|
|
virtual size_t size() const { return sizeof(*this); }
|
||
|
|
virtual BasicForwarder* copy(Space& outer_home, Space& inner_home, bool share)
|
||
|
|
{
|
||
|
|
Forwarder<View>* fwd = new (inner_home) Forwarder<View>();
|
||
|
|
fwd->outer.update(outer_home, share, outer);
|
||
|
|
fwd->inner.update(inner_home, share, inner);
|
||
|
|
return fwd;
|
||
|
|
}
|
||
|
|
virtual void cancel(Space& home, Clause& c);
|
||
|
|
};
|
||
|
|
|
||
|
|
// instances of Forwarder that we actually use
|
||
|
|
|
||
|
|
typedef Forwarder<Int::IntView> IntForwarder;
|
||
|
|
typedef Forwarder<Int::BoolView> BoolForwarder;
|
||
|
|
typedef Forwarder<Set::SetView> SetForwarder;
|
||
|
|
|
||
|
|
//=========================================================================
|
||
|
|
// IntForwarder
|
||
|
|
//=========================================================================
|
||
|
|
|
||
|
|
template <>
|
||
|
|
ExecStatus IntForwarder::forward_in(Space& home) // inner home
|
||
|
|
{
|
||
|
|
Int::ViewRanges<Int::IntView> r(outer);
|
||
|
|
GECODE_ME_CHECK(inner.inter_r(home,r));
|
||
|
|
return ES_OK;
|
||
|
|
}
|
||
|
|
|
||
|
|
template <>
|
||
|
|
void IntForwarder::forward_out(Space& home) // outer home
|
||
|
|
{
|
||
|
|
// it is guaranteed by design that after successful propagation the
|
||
|
|
// domain of the inner variable is a non-empty narrowing of the domain of
|
||
|
|
// the outer variable. therefore, we can simply replace the domain of
|
||
|
|
// the outer variable with the domain of the inner variable.
|
||
|
|
Int::ViewRanges<Int::IntView> r(inner);
|
||
|
|
outer.narrow_r(home, r, false);
|
||
|
|
}
|
||
|
|
|
||
|
|
template <>
|
||
|
|
void IntForwarder::cancel(Space& home, Clause& c)
|
||
|
|
{ outer.cancel(home, c, Int::PC_INT_DOM); }
|
||
|
|
|
||
|
|
//=========================================================================
|
||
|
|
// BoolForwarder
|
||
|
|
//=========================================================================
|
||
|
|
|
||
|
|
template <>
|
||
|
|
ExecStatus BoolForwarder::forward_in(Space& home)
|
||
|
|
{
|
||
|
|
Int::ViewRanges<Int::BoolView> r(outer);
|
||
|
|
GECODE_ME_CHECK(inner.inter_r(home,r));
|
||
|
|
return ES_OK;
|
||
|
|
}
|
||
|
|
|
||
|
|
template <>
|
||
|
|
void BoolForwarder::forward_out(Space& home)
|
||
|
|
{
|
||
|
|
Int::ViewRanges<Int::BoolView> r(inner);
|
||
|
|
outer.narrow_r(home, r, false);
|
||
|
|
}
|
||
|
|
|
||
|
|
template <>
|
||
|
|
void BoolForwarder::cancel(Space& home, Clause& c)
|
||
|
|
{ outer.cancel(home, c, Int::PC_INT_DOM); }
|
||
|
|
|
||
|
|
//=========================================================================
|
||
|
|
// SetForwarder
|
||
|
|
//=========================================================================
|
||
|
|
|
||
|
|
template <>
|
||
|
|
ExecStatus SetForwarder::forward_in(Space& home)
|
||
|
|
{
|
||
|
|
Set::GlbRanges<SetView> gr(outer);
|
||
|
|
GECODE_ME_CHECK(inner.includeI(home,gr));
|
||
|
|
Set::LubRanges<SetView> lr(outer);
|
||
|
|
GECODE_ME_CHECK(inner.intersectI(home,lr));
|
||
|
|
GECODE_ME_CHECK(inner.cardMin(home, outer.cardMin()));
|
||
|
|
GECODE_ME_CHECK(inner.cardMax(home, outer.cardMax()));
|
||
|
|
return ES_OK;
|
||
|
|
}
|
||
|
|
|
||
|
|
template <>
|
||
|
|
void SetForwarder::forward_out(Space& home)
|
||
|
|
{
|
||
|
|
Set::GlbRanges<SetView> gr(inner);
|
||
|
|
outer.includeI(home, gr);
|
||
|
|
Set::LubRanges<SetView> lr(inner);
|
||
|
|
outer.intersectI(home, lr);
|
||
|
|
outer.cardMin(home, inner.cardMin());
|
||
|
|
outer.cardMax(home, inner.cardMax());
|
||
|
|
}
|
||
|
|
|
||
|
|
template <>
|
||
|
|
void SetForwarder::cancel(Space& home, Clause& c)
|
||
|
|
{ outer.cancel(home, c, Set::PC_SET_ANY); }
|
||
|
|
|
||
|
|
//=========================================================================
|
||
|
|
// SubSpace
|
||
|
|
//=========================================================================
|
||
|
|
|
||
|
|
void SubSpace::forward(IntView outer, IntView inner)
|
||
|
|
{
|
||
|
|
BasicForwarder* fwd = new (*this) IntForwarder(outer, inner);
|
||
|
|
fwd->next = forwarder;
|
||
|
|
forwarder = fwd;
|
||
|
|
}
|
||
|
|
|
||
|
|
void SubSpace::forward(BoolView outer, BoolView inner)
|
||
|
|
{
|
||
|
|
BasicForwarder* fwd = new (*this) BoolForwarder(outer, inner);
|
||
|
|
fwd->next = forwarder;
|
||
|
|
forwarder = fwd;
|
||
|
|
}
|
||
|
|
|
||
|
|
void SubSpace::forward(SetView outer, SetView inner)
|
||
|
|
{
|
||
|
|
BasicForwarder* fwd = new (*this) SetForwarder(outer, inner);
|
||
|
|
fwd->next = forwarder;
|
||
|
|
forwarder = fwd;
|
||
|
|
}
|
||
|
|
|
||
|
|
ExecStatus SubSpace::forward_in()
|
||
|
|
{
|
||
|
|
for (BasicForwarder* p=forwarder; p!=NULL; p=p->next)
|
||
|
|
GECODE_ES_CHECK(p->forward_in(*this));
|
||
|
|
return ES_OK;
|
||
|
|
}
|
||
|
|
|
||
|
|
ExecStatus SubSpace::forward_out(Space& home) // outer home
|
||
|
|
{
|
||
|
|
for (BasicForwarder* p=forwarder; p!=NULL; p=p->next)
|
||
|
|
p->forward_out(home);
|
||
|
|
return ES_OK;
|
||
|
|
}
|
||
|
|
|
||
|
|
SubSpace::SubSpace(): GenericSpace(), forwarder(NULL) {}
|
||
|
|
|
||
|
|
SubSpace::SubSpace(bool share, SubSpace& s)
|
||
|
|
: GenericSpace(share, s), forwarder(NULL)
|
||
|
|
{
|
||
|
|
BasicForwarder** prev = &forwarder;
|
||
|
|
for (BasicForwarder* p=s.forwarder; p!=NULL; p=p->next)
|
||
|
|
{
|
||
|
|
BasicForwarder* fwd = p->copy(*s.homeDuringCloning, *this, share);
|
||
|
|
*prev = fwd;
|
||
|
|
prev = &fwd->next;
|
||
|
|
}
|
||
|
|
}
|
||
|
|
|
||
|
|
Space* SubSpace::copy(bool share)
|
||
|
|
{ return new SubSpace(share,*this); }
|
||
|
|
|
||
|
|
SubSpace* SubSpace::copy(Space& home, bool share)
|
||
|
|
{ homeDuringCloning = &home; return static_cast<SubSpace*>(clone(share)); }
|
||
|
|
|
||
|
|
void SubSpace::cancel(Space& home, Clause& c)
|
||
|
|
{
|
||
|
|
for (BasicForwarder*p = forwarder; p!=NULL; p=p->next)
|
||
|
|
p->cancel(home, c);
|
||
|
|
}
|
||
|
|
|
||
|
|
//=========================================================================
|
||
|
|
// Clause
|
||
|
|
//=========================================================================
|
||
|
|
|
||
|
|
Clause::operator GenericSpace&() { return *subhome; }
|
||
|
|
Clause::operator Space&() { return *subhome; }
|
||
|
|
Clause::operator Home() { return *subhome; }
|
||
|
|
|
||
|
|
GenericSpace* Clause::generic_space() const { return subhome; }
|
||
|
|
Space* Clause::space() const { return subhome; }
|
||
|
|
|
||
|
|
Clause::Clause(Space& home_, Disjunctor disj_)
|
||
|
|
: Propagator(home_), disj(disj_), subhome(new SubSpace())
|
||
|
|
{
|
||
|
|
disj.incr();
|
||
|
|
}
|
||
|
|
|
||
|
|
Clause::Clause(Space& home, bool share, Clause& c)
|
||
|
|
: Propagator(home, share, c), subhome(c.subhome->copy(home, share))
|
||
|
|
{
|
||
|
|
disj.update(home, share, c.disj);
|
||
|
|
}
|
||
|
|
|
||
|
|
Propagator* Clause::copy(Space& home, bool share)
|
||
|
|
{ return new (home) Clause(home, share, *this); }
|
||
|
|
|
||
|
|
void Clause::forward(Space& home, IntVar outer, IntVar inner)
|
||
|
|
{
|
||
|
|
IntView oview(outer);
|
||
|
|
IntView iview(inner);
|
||
|
|
subhome->forward(oview, iview);
|
||
|
|
oview.subscribe(home, *this, Int::PC_INT_DOM);
|
||
|
|
}
|
||
|
|
|
||
|
|
void Clause::forward(Space& home, BoolVar outer, BoolVar inner)
|
||
|
|
{
|
||
|
|
BoolView oview(outer);
|
||
|
|
BoolView iview(inner);
|
||
|
|
subhome->forward(oview, iview);
|
||
|
|
oview.subscribe(home, *this, Int::PC_INT_DOM);
|
||
|
|
}
|
||
|
|
|
||
|
|
void Clause::forward(Space& home, SetVar outer, SetVar inner)
|
||
|
|
{
|
||
|
|
SetView oview(outer);
|
||
|
|
SetView iview(inner);
|
||
|
|
subhome->forward(oview, iview);
|
||
|
|
oview.subscribe(home, *this, Set::PC_SET_ANY);
|
||
|
|
}
|
||
|
|
|
||
|
|
ExecStatus Clause::forward_in()
|
||
|
|
{ return subhome->forward_in(); }
|
||
|
|
|
||
|
|
ExecStatus Clause::forward_out(Space& home) // outer home
|
||
|
|
{ return subhome->forward_out(home); }
|
||
|
|
|
||
|
|
inline bool Clause::committed() const { return disj.get() == 1; }
|
||
|
|
|
||
|
|
ExecStatus Clause::propagate(Space& home, const ModEventDelta&)
|
||
|
|
{
|
||
|
|
if (forward_in() == ES_FAILED ||
|
||
|
|
subhome->status() == SS_FAILED )
|
||
|
|
{
|
||
|
|
if (committed()) return ES_FAILED;
|
||
|
|
disj.decr();
|
||
|
|
return home.ES_SUBSUMED(*this);
|
||
|
|
}
|
||
|
|
if (committed()) forward_out(home);
|
||
|
|
// maybe do something clever about subsumption later
|
||
|
|
return ES_FIX;
|
||
|
|
}
|
||
|
|
|
||
|
|
size_t Clause::dispose(Space& home)
|
||
|
|
{
|
||
|
|
subhome->cancel(home, *this);
|
||
|
|
delete subhome;
|
||
|
|
// the memory for the disj's LocalObject is not recovered
|
||
|
|
(void) Propagator::dispose(home);
|
||
|
|
return sizeof(*this);
|
||
|
|
}
|
||
|
|
|
||
|
|
PropCost Clause::cost(const Space&, const ModEventDelta&) const
|
||
|
|
{
|
||
|
|
// consider a clause to be crazy expensive
|
||
|
|
return PropCost::crazy(PropCost::HI,10);
|
||
|
|
}
|
||
|
|
}
|
||
|
|
|
||
|
|
//===========================================================================
|
||
|
|
// Clause (user API)
|
||
|
|
//===========================================================================
|
||
|
|
|
||
|
|
Clause::Clause(generic_gecode::GenericSpace& home, Disjunctor disj)
|
||
|
|
: _home(home), _clause(new (home) Disjunctor_::Clause(home, disj)) {}
|
||
|
|
Clause::operator generic_gecode::GenericSpace&() { return *_clause; }
|
||
|
|
Clause::operator Space&() { return *_clause; }
|
||
|
|
Clause::operator Home() { return *_clause; }
|
||
|
|
generic_gecode::GenericSpace* Clause::generic_space() { return _clause->generic_space(); }
|
||
|
|
generic_gecode::GenericSpace* Clause::generic_parent() { return &_home; }
|
||
|
|
Space* Clause::space() { return _clause->space(); }
|
||
|
|
void Clause::forward(IntVar outer, IntVar inner)
|
||
|
|
{ _clause->forward(_home, outer, inner); }
|
||
|
|
void Clause::forward(BoolVar outer, BoolVar inner)
|
||
|
|
{ _clause->forward(_home, outer, inner); }
|
||
|
|
void Clause::forward(SetVar outer, SetVar inner)
|
||
|
|
{ _clause->forward(_home, outer, inner); }
|
||
|
|
|
||
|
|
}
|