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

[Max]

Hi
i'm currently working on integrating a CSP Solver into another solver 
(ASP), similar to SMT (Sat Modulo Theories).
I want to use gecode, as it seems free and flexible.

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)

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);
[...]

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.


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

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?


Thank you in advance,
Max Ostrowski