Hi Everyone, I would like to put another Propagation Condition in BoolVarImp. You gave me good advice on how to process. For a first step, I just wanted to make some test. So I first modified bool.vis and add this new Propagation Condition. Then I tried to make existing propagators subscribe to this new propagation condition (without scheduling propagators and sending the corresponding events). Unfortunately, I failed to achieved this first step. Indeed, some problems occur during cloning.
I first thought that It was a problem with the rewriting of propagator during cloning. Indeed, I didn't update all propagators, so it can't be possible to change a propagator by another one which doesn't subscribe to the same propagation conditions than the original one. I disabled the rewrite of a propagator by another propagator from a different class during cloning. But I still have problems. I tried many things, without success and now I have no more ideas. For now, I just want to understand why I can't make it work. For this purpose, I designed an example to make gecode crash. I used the "sat" example given with Gecode, and only deal with this example (no matter if the other examples don't work anymore). My problem is reproducible by applying the patch attached in this mail to Gecode 3.2.2. Then, I configured and compiled Gecode with the following commands: ./configure --enable-debug --enable-audit make The test problem can be launched by copying the test2.cnf file (attached in the mail) in the gecode directory and executing the command: ./examples/sat test2.cnf If I use a debugger I get: Program received signal EXC_BAD_ACCESS, Could not access memory. Reason: KERN_INVALID_ADDRESS at address: 0x000000020000001b 0x000000010146d908 in Gecode::ActorLink::prev (this=0x200000013) at core.hpp:2328 2328 return _prev; (gdb) bt #0 0x000000010146d908 in Gecode::ActorLink::prev (this=0x200000013) at core.hpp:2328 #1 0x000000010146e0be in Gecode::VarImp<Gecode::Int::BoolVarImpConf>::update (this=0x101896350, x=0x101877698, s...@0x7fff5fbfece0) at core.hpp:3295 #2 0x000000010146e1d9 in Gecode::VarImp<Gecode::Int::BoolVarImpConf>::update (ho...@0x101503f80, s...@0x7fff5fbfece0) at core.hpp:3314 #3 0x000000010146e4b4 in Gecode::Space::update (this=0x101503f80, sub=0x101888798) at var-imp.hpp:343 #4 0x000000010146bae7 in Gecode::Space::_clone (this=0x101503e20, share=true) at gecode/kernel/core.cpp:481 #5 0x000000010011b58b in Gecode::Space::clone (this=0x101503e20, share=true) at core.hpp:2465 #6 0x000000010011c2c0 in Gecode::Search::Sequential::Path::recompute (this=0x101503798, d...@0x1015037b8, a_d=2, st...@0x101503718) at path.hh:305 #7 0x000000010011c5be in Gecode::Search::Sequential::DFS::next (this=0x101503718) at dfs.hh:146 #8 0x000000010011c615 in Gecode::Search::WorkerToEngine<Gecode::Search::Sequential::DFS>::next (this=0x101503710) at support.hh:74 #9 0x0000000100007ed2 in Gecode::DFS<Sat>::next (this=0x7fff5fbff070) at dfs.hpp:53 #10 0x000000010000811b in Gecode::Driver::ScriptBase<Gecode::Space>::run<Sat, Gecode::DFS, SatOptions> (o...@0x7fff5fbff1a0) at script.hpp:198 #11 0x0000000100001a34 in main (argc=1, argv=0x7fff5fbff4f0) at examples/sat.cpp:256 I probably made an obvious mistake, but I can not see. Thanks for your help, Cheers, Vincent Vincent Barichard Université d'Angers (LERIA) Tel: 02 41 73 52 06 Département Informatique Fax: 02 41 73 50 73 H203
diff -ru gecode/int/bool/clause.hpp gecode/int/bool/clause.hpp
--- gecode/int/bool/clause.hpp 2009-10-14 12:19:49.000000000 +0200
+++ gecode/int/bool/clause.hpp 2009-12-13 23:46:53.000000000 +0100
@@ -50,6 +50,8 @@
(home,x0[x0.size()-1],y0[y0.size()-1]), x(x0), y(y0) {
assert((x.size() > 0) && (y.size() > 0));
x.size(x.size()-1); y.size(y.size()-1);
+ x0.subscribe(home,*this,PC_BOOL_SAME,false);
+ x1.subscribe(home,*this,PC_BOOL_SAME,false);
}
template<class VX, class VY>
@@ -99,9 +101,9 @@
y.size(n);
}
}
- if ((x.size() == 0) && (y.size() == 0))
- return new (home) BinOrTrue<VX,VY>(home,share,*this,x0,x1);
- else
+// if ((x.size() == 0) && (y.size() == 0))
+// return new (home) BinOrTrue<VX,VY>(home,share,*this,x0,x1);
+// else
return new (home) ClauseTrue<VX,VY>(home,share,*this);
}
@@ -153,6 +155,7 @@
x0=x[i]; x[i]=x[--n];
x.size(n);
x0.subscribe(home,p,PC_BOOL_VAL,false);
+ x0.subscribe(home,p,PC_BOOL_SAME,false);
return ES_FIX;
}
// All x-views have been assigned!
@@ -178,6 +181,8 @@
template<class VX, class VY>
size_t
ClauseTrue<VX,VY>::dispose(Space& home) {
+ x0.cancel(home,*this,PC_BOOL_SAME);
+ x1.cancel(home,*this,PC_BOOL_SAME);
(void) MixBinaryPropagator<VX,PC_BOOL_VAL,VY,PC_BOOL_VAL>::dispose(home);
return sizeof(*this);
}
diff -ru gecode/int/bool/or.hpp gecode/int/bool/or.hpp
--- gecode/int/bool/or.hpp 2009-10-14 12:19:49.000000000 +0200
+++ gecode/int/bool/or.hpp 2009-12-13 23:46:36.000000000 +0100
@@ -105,7 +105,19 @@
template<class BVA, class BVB>
forceinline
BinOrTrue<BVA,BVB>::BinOrTrue(Home home, BVA b0, BVB b1)
- : BoolBinary<BVA,BVB>(home,b0,b1) {}
+ : BoolBinary<BVA,BVB>(home,b0,b1) {
+ x0.subscribe(home,*this,PC_BOOL_SAME,false);
+ x1.subscribe(home,*this,PC_BOOL_SAME,false);
+ }
+
+ template<class BVA, class BVB>
+ forceinline size_t
+ BinOrTrue<BVA,BVB>::dispose(Space& home) {
+ x0.cancel(home,*this,PC_BOOL_SAME);
+ x1.cancel(home,*this,PC_BOOL_SAME);
+ (void) BoolBinary<BVA,BVB>::dispose(home);
+ return sizeof(*this);
+ }
template<class BVA, class BVB>
forceinline
@@ -158,6 +170,7 @@
case GECODE_INT_STATUS(NONE,ZERO):
GECODE_ME_CHECK(x0.one_none(home)); break;
case GECODE_INT_STATUS(NONE,ONE):
+ x0.cancel(home,*this,PC_BOOL_SAME);
x0.cancel(home,*this,PC_BOOL_VAL); break;
case GECODE_INT_STATUS(ZERO,NONE):
GECODE_ME_CHECK(x1.one_none(home)); break;
@@ -166,6 +179,7 @@
case GECODE_INT_STATUS(ZERO,ONE):
break;
case GECODE_INT_STATUS(ONE,NONE):
+ x1.cancel(home,*this,PC_BOOL_SAME);
x1.cancel(home,*this,PC_BOOL_VAL); break;
case GECODE_INT_STATUS(ONE,ZERO):
break;
@@ -186,11 +200,16 @@
template<class BV>
forceinline
TerOrTrue<BV>::TerOrTrue(Home home, BV b0, BV b1, BV b2)
- : BoolBinary<BV,BV>(home,b0,b1), x2(b2) {}
+ : BoolBinary<BV,BV>(home,b0,b1), x2(b2) {
+ x0.subscribe(home,*this,PC_BOOL_SAME,false);
+ x1.subscribe(home,*this,PC_BOOL_SAME,false);
+ }
template<class BV>
forceinline size_t
TerOrTrue<BV>::dispose(Space& home) {
+ x0.cancel(home,*this,PC_BOOL_SAME);
+ x1.cancel(home,*this,PC_BOOL_SAME);
(void) BoolBinary<BV,BV>::dispose(home);
return sizeof(*this);
}
@@ -214,11 +233,11 @@
Actor*
TerOrTrue<BV>::copy(Space& home, bool share) {
assert(x0.none() && x1.none());
- if (x2.one())
- return new (home) OrTrueSubsumed<BV>(home,share,*this,x0,x1);
- else if (x2.zero())
- return new (home) BinOrTrue<BV,BV>(home,share,*this,x0,x1);
- else
+// if (x2.one())
+// return new (home) OrTrueSubsumed<BV>(home,share,*this,x0,x1);
+// else if (x2.zero())
+// return new (home) BinOrTrue<BV,BV>(home,share,*this,x0,x1);
+// else
return new (home) TerOrTrue<BV>(home,share,*this);
}
@@ -242,6 +261,7 @@
GECODE_NEVER;
case GECODE_INT_STATUS(NONE,ZERO,NONE):
std::swap(x1,x2); x1.subscribe(home,*this,PC_BOOL_VAL);
+ x1.subscribe(home,*this,PC_BOOL_SAME,false);
return ES_FIX;
case GECODE_INT_STATUS(NONE,ZERO,ZERO):
GECODE_ME_CHECK(x0.one_none(home)); break;
@@ -249,13 +269,16 @@
case GECODE_INT_STATUS(NONE,ONE,NONE):
case GECODE_INT_STATUS(NONE,ONE,ZERO):
case GECODE_INT_STATUS(NONE,ONE,ONE):
+ x0.cancel(home,*this,PC_BOOL_SAME);
x0.cancel(home,*this,PC_BOOL_VAL); break;
case GECODE_INT_STATUS(ZERO,NONE,NONE):
std::swap(x0,x2); x0.subscribe(home,*this,PC_BOOL_VAL);
+ x0.subscribe(home,*this,PC_BOOL_SAME,false);
return ES_FIX;
case GECODE_INT_STATUS(ZERO,NONE,ZERO):
GECODE_ME_CHECK(x1.one_none(home)); break;
case GECODE_INT_STATUS(ZERO,NONE,ONE):
+ x1.cancel(home,*this,PC_BOOL_SAME);
x1.cancel(home,*this,PC_BOOL_VAL); break;
case GECODE_INT_STATUS(ZERO,ZERO,NONE):
GECODE_ME_CHECK(x2.one_none(home)); break;
@@ -269,6 +292,7 @@
case GECODE_INT_STATUS(ONE,NONE,NONE):
case GECODE_INT_STATUS(ONE,NONE,ZERO):
case GECODE_INT_STATUS(ONE,NONE,ONE):
+ x1.cancel(home,*this,PC_BOOL_SAME);
x1.cancel(home,*this,PC_BOOL_VAL); break;
case GECODE_INT_STATUS(ONE,ZERO,NONE):
case GECODE_INT_STATUS(ONE,ZERO,ZERO):
diff -ru gecode/int/bool.hh gecode/int/bool.hh
--- gecode/int/bool.hh 2009-10-12 17:36:53.000000000 +0200
+++ gecode/int/bool.hh 2009-12-13 23:42:46.000000000 +0100
@@ -213,6 +213,8 @@
virtual ExecStatus propagate(Space& home, const ModEventDelta& med);
/// Post propagator \f$ b_0 \lor b_1 = 1 \f$
static ExecStatus post(Home home, BVA b0, BVB b1);
+ /// Delete propagator and return its size
+ virtual size_t dispose(Space& home);
};
/**
diff -ru gecode/int/var-imp/bool.hpp gecode/int/var-imp/bool.hpp
--- gecode/int/var-imp/bool.hpp 2009-09-08 21:10:29.000000000 +0200
+++ gecode/int/var-imp/bool.hpp 2009-12-13 23:42:46.000000000 +0100
@@ -401,15 +401,15 @@
*
*/
forceinline void
- BoolVarImp::subscribe(Space& home, Propagator& p, PropCond,
+ BoolVarImp::subscribe(Space& home, Propagator& p, PropCond pc,
bool process) {
// Subscription can be used with integer propagation conditions,
// which must be remapped to the single Boolean propagation condition.
- BoolVarImpBase::subscribe(home,p,PC_BOOL_VAL,assigned(),process);
+ BoolVarImpBase::subscribe(home,p,pc,assigned(),process);
}
forceinline void
- BoolVarImp::cancel(Space& home, Propagator& p, PropCond) {
- BoolVarImpBase::cancel(home,p,PC_BOOL_VAL,assigned());
+ BoolVarImp::cancel(Space& home, Propagator& p, PropCond pc) {
+ BoolVarImpBase::cancel(home,p,pc,assigned());
}
forceinline void
diff -ru gecode/int/var-imp/bool.vis gecode/int/var-imp/bool.vis
--- gecode/int/var-imp/bool.vis 2008-02-01 12:10:00.000000000 +0100
+++ gecode/int/var-imp/bool.vis 2009-12-13 23:42:46.000000000 +0100
@@ -52,8 +52,17 @@
/// Domain operation has not changed domain
[ModEvent]
Name: VAL=ASSIGNED
-Combine: VAL=VAL
+Combine: VAL=VAL INIT=VAL SAME=SAME
/// Domain operation has resulted in a value (assigned variable)
+[ModEvent]
+Name: INIT=SUBSCRIBE
+Combine: INIT=INIT VAL=VAL SAME=SAME
+ /// If a propagator subscribes to this variable, it will be processed
assuming a ME_BOOL_INIT modification event.
+[ModEvent]
+Name: SAME
+Combine: SAME=SAME VAL=SAME INIT=SAME
+ /// Two variables must be in the same equivalence class
+
[PropCond]
Name: VAL=ASSIGNED
ModEvents: VAL
@@ -64,6 +73,16 @@
* condition PC_BOOL_VAL, then \a p is propagated when a domain
* update operation on \a x returns the modification event ME_BOOL_VAL.
*/
+[PropCond]
+Name: SAME
+ModEvents: SAME
+# /**
+# * \brief Propagate when a view must enter an equivalence class
+# *
+# * If a propagator \a p depends on a view \a x with propagation
+# * condition PC_BOOL_SAME, then \a p is propagated when a variable
+# * update operation on \a x returns the modification event ME_BOOL_SAME.
+# */
[PropCondFooter]
//@}
[End]
test2.cnf
Description: Binary data
_______________________________________________ Gecode users mailing list [email protected] https://www.gecode.org/mailman/listinfo/gecode-users
