[gecode-users] Feature support of gecode for SMT system

[Guido Tack]

Max wrote:

> I tried to experiment a bit, but it is very hard to find the needed
> functionality because of the missing documentation. (If the tutorial  
> is
> already in work, maybe you could send me a draft version of it)

I'm afraid it's not yet in a state to be sent around.

> My question is, is gecode capable of the following things:
>
> Comparing boolean values with integer equations:
> I need constraints of the following syntax,
> b1 == X > Y
> b2 == W <= Z*X + 14
> etc...
> All variables on the right side are integer values. The b's on the  
> left
> side shall be boolean variables.
> So if the constraint X > Y is fullfilled, b1 must be true, if b1 is  
> set
> to false, then X > Y does not hold.
> I tried to post this, but it does not seem to be supported this way:
> [...]
> IntVarArray x;
> BoolVar y;
> post(this, x[0] > x[1] + 30 == y);
> [...]

It's called "reified propagators", and it's supported.  If you want to  
use the post syntax from minimodel.hh, you can do as follows:
post(this, eqv(~(x[0] > x[1] + 30), y));

Many constraints have reified versions, you can identify them in the  
reference documentation by their additional BoolVar argument.

> Backtracking in means of manual, incremental variable assignment.
> I want to set my constraints and restrict the domains of the variables
> without a choicepoint,
> then i manually set my (boolean) variables to be true or false.
> Sometimes i want to backtrack this setting of variables, undoing the
> setting of the variables.
> Is there another way than copying my Space and having a copy of each
> assignment manually?
> Or maybe you know a way to do this a better way, i dont want to set  
> all
> variables to a new value, since  everything would have to be  
> recomputed.

There's no other way than copying and recomputation in Gecode to undo  
changes in variable domains.

> Post Division:
> [...]
> post(this, x[0] / x[1] == 42);
> [...]
> Why is division not supported?

It's an oversight, we'll add it to the next version.  You can still  
post division directly, without the minimodel interface:
div(this, x0, x1, IntVar(this, 42, 42));
There's no specialized version for constant integers (yet).

> Learning: Which constraint failed:
> If there is no solution for my problem, can gecode deliver me a reason
> (for learning)?
> So which constraints failed or something like that?

No, that's currently not possible (and IIRC has been discussed here  
before, maybe you want to have a look at the archives).

Cheers,
	Guido