[m-rev.] diff: add backjumping support to the standard library

[Ian MacLarty]

On Wed, Mar 05, 2008 at 04:54:09PM +1100, Julien Fischer wrote:
>
> Estimated hours taken: 1.5
> Branches: main
>
> Add G12's backjump module to the standard library.
> This will not be included in the library documentation or announced until
> more of the XXXs have been dealt with.
>
...
> Index: library/backjump.m
> ===================================================================
> RCS file: library/backjump.m
> diff -N library/backjump.m
> --- /dev/null	1 Jan 1970 00:00:00 -0000
> +++ library/backjump.m	5 Mar 2008 05:31:35 -0000
> @@ -0,0 +1,469 @@
> +%-----------------------------------------------------------------------------%
> +% vim: ft=mercury ts=4 sw=4 et wm=0 tw=0
> +%-----------------------------------------------------------------------------%
> +% Copyright (C) 2007-2008 The University of Melbourne.
> +% This file may only be copied under the terms of the GNU Library General
> +% Public License - see the file COPYING.LIB in the Mercury distribution.
> +%-----------------------------------------------------------------------------%
> +% +% File: backjump.m
> +% Author: Mark Brown <mark at csse.unimelb.edu.au>
> +% Stability: medium
> +% +% This module defines the Mercury interface for backjumping.
> +%
> +% An application can use this module to add backjumping to their search
> +% algorithms in the following way:
> +%
> +%   - At points in the search tree where you wish to backjump *to*, add a
> +%     call to get_choice_id/1.
> +%
> +%   - When in the search tree you discover that there are no further
> +%     solutions between the current execution point and the failure port
> +%     of an earlier call to get_choice_id/1, call backjump/1 with the
> +%     relevant choice_id.  This takes execution immediately to that 
> failure
> +%     port.
> +%
> +% It is important to avoid backjumping to a choicepoint that has already
> +% been pruned away, either on failure or due to a commit.  In the former
> +% case (which can occur if the choice_id is stored in a non-trailed 
> mutable,
> +% for example) the implementation throws an exception.  In the latter case
> +% behaviour is undefined but most likely will be a seg fault.  This can
> +% occur if multi/nondet code that returns a choice_id is called from a
> +% cc_multi/cc_nondet context, for example.
> +%
> +% Note that the definition of "solution" in the above means solution with
> +% respect to the search algorithm, and doesn't necessarily mean solution 
> of
> +% the immediate parent or any particular ancestor.
> +% 
> +%-----------------------------------------------------------------------------%
> +%-----------------------------------------------------------------------------%
> +
> +:- module backjump.
> +:- interface.
> +
> +%-----------------------------------------------------------------------------%
> +
> +    % Abstract type representing points in the search tree which can be
> +    % backjumped to.
> +    %
> +:- type choice_id.
> +
> +    % Returns a single unused choice_id, then fails.  We make this nondet
> +    % rather than det, however, so that:
> +    %    a) it leaves a nondet stack frame behind which can later be
> +    %       used by backjump/1, and
> +    %    b) the calling context is forced to deal with the case of no
> +    %       solutions, which may occur even if later conjuncts can never
> +    %       fail (since they may call backjump/1, which counts as an
> +    %       exceptional rather than a logical answer).
> +    %
> +:- impure pred get_choice_id(choice_id::out) is nondet.

Could you add a note about why this is impure?  Where would one usually
put a promise_pure?  What would such a promise_pure be promising
exactly?

> +
> +    % Backjump to the point where the choice_id was created.  That is,
> +    % jump immediately to the FAIL event of the corresponding call to
> +    % get_choice_id.
> +    %
> +:- impure pred backjump(choice_id::in) is erroneous.
> +

Same here.

Cheers,
Ian.
--------------------------------------------------------------------------
mercury-reviews mailing list
Post messages to:       mercury-reviews at csse.unimelb.edu.au
Administrative Queries: owner-mercury-reviews at csse.unimelb.edu.au
Subscriptions:          mercury-reviews-request at csse.unimelb.edu.au
--------------------------------------------------------------------------