Re: "circular" fd constraints and the soft cut conditional

Hi,

On Tue, Oct 30, 2001 at 04:05:22PM +0100, Alexander Pretschner wrote:
> Hi-
> given the code below, Eclipse 5.3 (linux) crashes while executing
> predicate query/0 (the code is generated automatically).
> 
> Tracking down the problem, there's two things:
> (a) ?- X-Y #>=1, Y-X #>=0.
> takes roughly 90 seconds to compute the correct answer "no" (while the
> solution seems trivial to a human).

You're not giving any domains to the variables.  ECLiPSe's FD solver
defaults to bounds of -10000000 to 10000000 if you do not impose any
yourself.  When you impose those constraints, the FD solver starts to
propagate the bounds, using the constraints.  E.g. Y #>= -10000000 combined
with X-Y #>= 1 implies X #>= -9999999.  This combined with Y-X #>= 0 implies
Y #>= -9999999.  And so on.  Eventually it deduces that there are no values
which satisfy the constraints and it fails, but this takes a while.

You should either provide some reasonable bounds, or use a solver that does
the kind of global reasoning you want.

I suspect there are other ways in which the FD solver is not doing what you
want.  For instance, while FD realises that `X #\= X' should fail, it does
not realise that `X #\= Y, X #= Y' should fail.  It is not designed for
reasoning about variables with no other information available.  Part of the
reason for this is that it's a partial solver: until all variables become
ground, sometimes the best answer it can give is "maybe" (the presence of
any delayed goal indicates that the solver has not been able to solve the
problem completely).  So to be sure you get correct answers, you must make
sure that every FD variable is assigned a fixed value before the end of the
query.

> (b) If I replace the soft cut conditional (*->) from sepia_kernel by an
> actual "hard" cut conditional (->), predicate "query" takes about 90
> seconds to yield the (correct?) result "no" rather than a crash.
> However, I do indeed need the "soft" semantics where all positive
> answers are tried.

There does indeed appear to be a bug in `*->'.  I suspect that the overflow
of one of the stacks is not being caught correctly --- I'm told the
implementation of `*->' is a bit of a hack, and does not properly reclaim
space that is no longer needed.  We'll look into fixing the crash, but
you'll still need to reformulate your problem at least a bit to avoid
running out of memory (with the right formulation of your problem, memory
should not be an issue).

Perhaps if you explain the problem you are trying to solve, somebody can
suggest a better way to do what you want.  As an example, you may find
reified constraints useful.  E.g. instead of

    isFunc(#=,(A,B),true):- fd:(A#=B).
    isFunc(#=,(A,B),false):- fd:(A#\=B).

you could write

    isFunc(#=,(A,B),T):- #=(A,B,T).	% or T isd (A #= B) if you prefer

What this does is set up a boolean variable T which reflects the truth of
the constraint A #= B.  With this change (and changing an occurrence of
`true' to `1'), `query' actually runs to completion without crashing or
using excessive amounts of memory --- most likely due to the fact that calls
to isFunc/3 with the first argument being `#=' no longer create a choice
point.


One last point:

> isFunc(cwd, cWithdraw(X0), _P):-  _P = X0.

Note that variable names starting with `_' are intended to be used only for
variables which appear only once in a clause; it is bad style to use such
names for variables which are not singletons (programmers see the underscore
and tend to assume it's the only reference to the variable).

Cheers,
Warwick