[m-rev.] diff: add backjumping support to the standard library
Julien Fischer
juliensf at csse.unimelb.edu.au
Wed Mar 5 16:54:09 AEDT 2008
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.
I've included a diff between the G12 version of the backjump
module and this one below.
library/backjump.m:
A module (from G12) that provides support for backjumping.
There are a number of minor modifications from the G12 version in
order to make this compile in .par and .profdeep grades but it is
otherwise unchanged.
library/library.m:
Include the new module.
doc/Mmakefile:
Do not include the backjump module in the library reference guide
for now.
tests/hard_coded/Mmakefile:
tests/hard_coded/backjump_test.{m,exp}:
Test backjumping (from the G12 nogood example.)
Julien.
--- /Users/juliensf/g12/ws-feature-set/common/g12_util/backjump.m 2008-03-04 15:00:13.000000000 +1100
+++ library/backjump.m 2008-03-05 15:31:33.000000000 +1100
@@ -1,7 +1,7 @@
%-----------------------------------------------------------------------------%
% vim: ft=mercury ts=4 sw=4 et wm=0 tw=0
%-----------------------------------------------------------------------------%
-% Copyright (C) 2007 The University of Melbourne.
+% 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.
%-----------------------------------------------------------------------------%
@@ -35,9 +35,6 @@
% 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.
-%
-% Code in this module is derived from library/exception.m in the Mercury
-% distribution.
%
%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%
@@ -70,13 +67,19 @@
:- impure pred backjump(choice_id::in) is erroneous.
%-----------------------------------------------------------------------------%
+%-----------------------------------------------------------------------------%
+
+:- implementation.
+
+%-----------------------------------------------------------------------------%
+
+:- interface.
% Debugging support.
%
:- func to_int(choice_id) = int.
%-----------------------------------------------------------------------------%
-%-----------------------------------------------------------------------------%
:- implementation.
@@ -139,34 +142,22 @@
} ML_BackJumpHandler;
-#ifdef MR_THREAD_SAFE
- /*
- ** XXX .par grades are not yet supported. We need to add the global
- ** ML_backjump_handler to the Mercury context, and define these macros
- ** to get the globals from there.
- */
- #define ML_GET_BACKJUMP_HANDLER() \
- MR_GETSPECIFIC(MR_backjump_handler_key)
- #define ML_SET_BACKJUMP_HANDLER(val) \
- pthread_setspecific(MR_backjump_handler_key, (val))
-#else /* !MR_THREAD_SAFE */
-
- #define ML_GET_BACKJUMP_HANDLER() ML_backjump_handler
- #define ML_SET_BACKJUMP_HANDLER(val) ML_backjump_handler = (val)
- #define ML_GET_NEXT_CHOICE_ID() (ML_next_choice_id++)
+/*
+** XXX Does not work properly in grades that support multiple threads.
+*/
+#define ML_GET_BACKJUMP_HANDLER() ML_backjump_handler
+#define ML_SET_BACKJUMP_HANDLER(val) ML_backjump_handler = (val)
+#define ML_GET_NEXT_CHOICE_ID() (ML_next_choice_id++)
- extern ML_BackJumpHandler *ML_backjump_handler;
- extern ML_Choice_Id ML_next_choice_id;
+extern ML_BackJumpHandler *ML_backjump_handler;
+extern ML_Choice_Id ML_next_choice_id;
-#endif /* !MR_THREAD_SAFE */
").
:- pragma foreign_code("C", "
-#ifndef MR_THREAD_SAFE
ML_BackJumpHandler *ML_backjump_handler;
ML_Choice_Id ML_next_choice_id = 0;
-#endif /* !MR_THREAD_SAFE */
").
%-----------------------------------------------------------------------------%
@@ -197,10 +188,10 @@
#endif
void MR_CALL
-backjump__builtin_choice_id_1_p_0(ML_Choice_Id *id, MR_CONT_PARAMS);
+mercury__backjump__builtin_choice_id_1_p_0(ML_Choice_Id *id, MR_CONT_PARAMS);
void MR_CALL
-backjump__builtin_backjump_1_p_0(ML_Choice_Id id);
+mercury__backjump__builtin_backjump_1_p_0(ML_Choice_Id id);
#endif /* MR_HIGHLEVEL_CODE */
#endif /* ML_BACKJUMP_GUARD */
@@ -219,7 +210,8 @@
#endif /* MR_NATIVE_GC */
-void MR_CALL backjump__builtin_choice_id_1_p_0(MR_Integer *id, MR_CONT_PARAMS)
+void MR_CALL
+mercury__backjump__builtin_choice_id_1_p_0(MR_Integer *id, MR_CONT_PARAMS)
{
ML_BackJumpHandler this_handler;
@@ -243,7 +235,8 @@
ML_SET_BACKJUMP_HANDLER(this_handler.prev);
}
-void MR_CALL backjump__builtin_backjump_1_p_0(ML_Choice_Id id)
+void MR_CALL
+mercury__backjump__builtin_backjump_1_p_0(ML_Choice_Id id)
{
ML_BackJumpHandler *backjump_handler = ML_GET_BACKJUMP_HANDLER();
@@ -310,6 +303,10 @@
"
void mercury_sys_init_backjumps_init(void);
void mercury_sys_init_backjumps_init_type_tables(void);
+#ifdef MR_DEEP_PROFILING
+void mercury_sys_init_backjumps_write_out_proc_statics(FILE *deep_fp,
+ FILE *procrep_fp);
+#endif
#ifndef MR_HIGHLEVEL_CODE
@@ -436,6 +433,18 @@
/* no types to register */
}
+#ifdef MR_DEEP_PROFILING
+void
+mercury_sys_init_backjumps_write_out_proc_statics(FILE *deep_fp,
+ FILE *procrep_fp)
+{
+ MR_write_out_user_proc_static(deep_fp, procrep_fp,
+ &MR_proc_layout_user_name(backjump, builtin_choice_id, 1, 0));
+ MR_write_out_user_proc_static(deep_fp, procrep_fp,
+ &MR_proc_layout_user_name(backjump, builtin_backjump, 1, 0));
+}
+#endif /* MR_DEEP_PROFILING */
+
").
%-----------------------------------------------------------------------------%
@@ -456,3 +465,5 @@
to_int(P) = P.
%-----------------------------------------------------------------------------%
+:- end_module backjump.
+%-----------------------------------------------------------------------------%
=================================================================================
Index: doc/Mmakefile
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/doc/Mmakefile,v
retrieving revision 1.51
diff -u -r1.51 Mmakefile
--- doc/Mmakefile 18 Dec 2007 04:28:53 -0000 1.51
+++ doc/Mmakefile 5 Mar 2008 05:31:35 -0000
@@ -269,6 +269,8 @@
;; \
$(LIBRARY_DIR)/mutvar.m) \
;; \
+ $(LIBRARY_DIR)/backjump.m) \
+ ;; \
*) \
echo "* `basename $$filename .m`::"; \
;; \
@@ -305,6 +307,8 @@
;; \
$(LIBRARY_DIR)/mutvar.m) \
;; \
+ $(LIBRARY_DIR)/backjump.m) \
+ ;; \
*) \
file="`basename $$filename .m`"; \
echo "@node $$file"; \
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.
+
+ % 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.
+
+%-----------------------------------------------------------------------------%
+%-----------------------------------------------------------------------------%
+
+:- implementation.
+
+%-----------------------------------------------------------------------------%
+
+:- interface.
+
+ % Debugging support.
+ %
+:- func to_int(choice_id) = int.
+
+%-----------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module io.
+:- import_module list.
+:- import_module string.
+
+:- type choice_id == int.
+
+get_choice_id(Id) :-
+ impure builtin_choice_id(Id).
+
+backjump(Id) :-
+ impure builtin_backjump(Id).
+
+%-----------------------------------------------------------------------------%
+
+% builtin_choice_id and builtin_backjump are implemented below using
+% hand-coded low-level C code.
+%
+:- pragma terminates(builtin_choice_id/1).
+:- impure pred builtin_choice_id(choice_id::out) is nondet.
+
+:- pragma terminates(builtin_backjump/1).
+:- impure pred builtin_backjump(choice_id::in) is erroneous.
+
+%
+% IMPORTANT: any changes or additions to external predicates should be
+% reflected in the definition of pred_is_external in
+% mdbcomp/program_representation.m. The debugger needs to know what predicates
+% are defined externally, so that it knows not to expect events for those
+% predicates.
+%
+% XXX we haven't done this yet.
+%
+
+:- external(builtin_choice_id/1).
+:- external(builtin_backjump/1).
+
+%-----------------------------------------------------------------------------%
+
+:- pragma foreign_decl("C", "
+
+typedef MR_Integer ML_Choice_Id;
+
+typedef struct ML_BackJumpHandler_struct {
+ struct ML_BackJumpHandler_struct *prev;
+ ML_Choice_Id id;
+
+#ifdef MR_HIGHLEVEL_CODE
+
+ jmp_buf handler;
+
+#else /* !MR_HIGHLEVEL_CODE */
+
+ MR_Word *saved_sp;
+ MR_Word *saved_fr;
+
+#endif /* !MR_HIGHLEVEL_CODE */
+
+} ML_BackJumpHandler;
+
+
+/*
+** XXX Does not work properly in grades that support multiple threads.
+*/
+#define ML_GET_BACKJUMP_HANDLER() ML_backjump_handler
+#define ML_SET_BACKJUMP_HANDLER(val) ML_backjump_handler = (val)
+#define ML_GET_NEXT_CHOICE_ID() (ML_next_choice_id++)
+
+extern ML_BackJumpHandler *ML_backjump_handler;
+extern ML_Choice_Id ML_next_choice_id;
+
+").
+
+:- pragma foreign_code("C", "
+ ML_BackJumpHandler *ML_backjump_handler;
+ ML_Choice_Id ML_next_choice_id = 0;
+").
+
+%-----------------------------------------------------------------------------%
+%
+% The --high-level-code implementation.
+%
+
+:- pragma foreign_decl("C",
+"
+/* protect against multiple inclusion */
+#ifndef ML_BACKJUMP_GUARD
+#define ML_BACKJUMP_GUARD
+
+#ifdef MR_HIGHLEVEL_CODE
+
+#include <setjmp.h>
+
+#ifdef MR_USE_GCC_NESTED_FUNCTIONS
+ #define MR_CONT_PARAMS MR_NestedCont cont
+ #define MR_CONT_PARAM_TYPES MR_NestedCont
+ #define MR_CONT_ARGS cont
+ #define MR_CONT_CALL() (*cont)()
+#else
+ #define MR_CONT_PARAMS MR_Cont cont, void *cont_env
+ #define MR_CONT_PARAM_TYPES MR_Cont, void *
+ #define MR_CONT_ARGS cont, cont_env
+ #define MR_CONT_CALL() cont(cont_env)
+#endif
+
+void MR_CALL
+mercury__backjump__builtin_choice_id_1_p_0(ML_Choice_Id *id, MR_CONT_PARAMS);
+
+void MR_CALL
+mercury__backjump__builtin_backjump_1_p_0(ML_Choice_Id id);
+
+#endif /* MR_HIGHLEVEL_CODE */
+#endif /* ML_BACKJUMP_GUARD */
+").
+
+:- pragma foreign_code("C",
+"
+#ifdef MR_HIGHLEVEL_CODE
+
+#ifdef MR_NATIVE_GC
+
+/*
+** XXX code is needed to trace the local variables
+** in the builtin_choice_id predicate for accurate GC.
+*/
+
+#endif /* MR_NATIVE_GC */
+
+void MR_CALL
+mercury__backjump__builtin_choice_id_1_p_0(MR_Integer *id, MR_CONT_PARAMS)
+{
+ ML_BackJumpHandler this_handler;
+
+ this_handler.prev = ML_GET_BACKJUMP_HANDLER();
+ this_handler.id = ML_GET_NEXT_CHOICE_ID();
+ ML_SET_BACKJUMP_HANDLER(&this_handler);
+
+ if (setjmp(this_handler.handler) == 0) {
+ #ifdef MR_DEBUG_JMPBUFS
+ fprintf(stderr, ""choice setjmp %p\\n"", this_handler.handler);
+ #endif
+
+ *id = this_handler.id;
+ MR_CONT_CALL();
+ } else {
+ #ifdef MR_DEBUG_JMPBUFS
+ fprintf(stderr, ""choice caught jmp %p\\n"", this_handler.handler);
+ #endif
+ }
+
+ ML_SET_BACKJUMP_HANDLER(this_handler.prev);
+}
+
+void MR_CALL
+mercury__backjump__builtin_backjump_1_p_0(ML_Choice_Id id)
+{
+ ML_BackJumpHandler *backjump_handler = ML_GET_BACKJUMP_HANDLER();
+
+ /*
+ ** XXX when we commit and prune away nondet stack frames, we leave the
+ ** backjump handlers on the stack. If the caller tries to backjump to
+ ** a frame that has been pruned away, the handler may still be on the
+ ** stack and we won't detect the problem.
+ **
+ ** We could avoid this problem by adding a trailing function which
+ ** prunes back the handler stack on a commit, which would mean that in
+ ** this case we will reach the bottom of the stack and call
+ ** ML_report_invalid_backjump rather than seg faulting. But that would
+ ** require trailing to be always available. Instead, we just rely on
+ ** the caller only backjumping to frames that actually do exist.
+ **
+ ** (The same problem would occur if the caller tries to backjump to a
+ ** frame that has already failed. In this case, though, the choice ID
+ ** will also no longer be live since the call to get_choice_id would have
+ ** been bactracked over, so this isn't as much of a problem as with
+ ** commits.)
+ */
+ while (backjump_handler != NULL) {
+ if (backjump_handler->id == id) {
+ break;
+ }
+ backjump_handler = backjump_handler->prev;
+ }
+
+ if (backjump_handler == NULL) {
+ ML_report_invalid_backjump(id);
+ exit(EXIT_FAILURE);
+ } else {
+
+ #ifdef MR_DEBUG_JMPBUFS
+ fprintf(stderr, ""backjump longjmp %p\\n"", backjump_handler->handler);
+ #endif
+ longjmp(backjump_handler->handler, 1);
+ }
+}
+
+#endif /* MR_HIGHLEVEL_CODE */
+").
+
+%-----------------------------------------------------------------------------%
+%
+% The --no-high-level-code implementation.
+%
+
+:- pragma foreign_decl("C",
+"
+#ifndef MR_HIGHLEVEL_CODE
+
+#include ""mercury_stacks.h""
+#include ""mercury_stack_trace.h""
+#include ""mercury_trace_base.h""
+#include ""mercury_layout_util.h""
+#include ""mercury_deep_profiling_hand.h""
+
+#endif /* !MR_HIGHLEVEL_CODE */
+").
+
+:- pragma foreign_code("C",
+"
+void mercury_sys_init_backjumps_init(void);
+void mercury_sys_init_backjumps_init_type_tables(void);
+#ifdef MR_DEEP_PROFILING
+void mercury_sys_init_backjumps_write_out_proc_statics(FILE *deep_fp,
+ FILE *procrep_fp);
+#endif
+
+#ifndef MR_HIGHLEVEL_CODE
+
+#define ML_DUMMY_LINE 0
+
+#define ML_BACKJUMP_STRUCT \
+ (((ML_BackJumpHandler *) (MR_curfr + 1 - MR_NONDET_FIXED_SIZE)) - 1)
+
+#ifdef ML_DEBUG_BACKJUMPS
+#define ML_BACKJUMP_CHECKPOINT(s, p) \
+ do { \
+ fflush(stdout); \
+ fprintf(stderr, ""backjumps (%s): "" \
+ ""loc %p, prev %p, id %d, sp %p, fr %p\\n"", \
+ s, p, p->prev, p->id, p->saved_sp, p->saved_fr); \
+ } while (0)
+#else
+#define ML_BACKJUMP_CHECKPOINT(s, p)
+#endif
+
+MR_define_extern_entry(mercury__backjump__builtin_choice_id_1_0);
+MR_define_extern_entry(mercury__backjump__builtin_backjump_1_0);
+
+MR_declare_label(mercury__backjump__builtin_choice_id_1_0_i1);
+
+MR_proc_static_user_no_site(backjump, builtin_choice_id, 1, 0,
+ ""backjump.m"", ML_DUMMY_LINE, MR_TRUE);
+MR_proc_static_user_no_site(backjump, builtin_backjump, 1, 0,
+ ""backjump.m"", ML_DUMMY_LINE, MR_TRUE);
+
+MR_EXTERN_USER_PROC_STATIC_PROC_LAYOUT(MR_DETISM_NON,
+ MR_PROC_NO_SLOT_COUNT, -1, MR_PREDICATE, backjump, builtin_choice_id,
+ 1, 0);
+MR_EXTERN_USER_PROC_STATIC_PROC_LAYOUT(MR_DETISM_DET, 1,
+ MR_LONG_LVAL_STACKVAR_INT(1), MR_PREDICATE, backjump,
+ builtin_backjump, 1, 0);
+
+MR_MAKE_USER_INTERNAL_LAYOUT(backjump, builtin_choice_id, 1, 0, 1);
+
+MR_BEGIN_MODULE(hand_written_backjump_module)
+ MR_init_entry_sl(mercury__backjump__builtin_choice_id_1_0);
+ MR_init_entry_sl(mercury__backjump__builtin_backjump_1_0);
+
+ MR_init_label_sl(mercury__backjump__builtin_choice_id_1_0_i1);
+MR_BEGIN_CODE
+
+MR_define_entry(mercury__backjump__builtin_choice_id_1_0);
+{
+ MR_mkpragmaframe(""builtin_choice_id/1"", 0, ML_BackJumpHandler_struct,
+ MR_LABEL(mercury__backjump__builtin_choice_id_1_0_i1));
+
+ ML_BACKJUMP_STRUCT->prev = ML_GET_BACKJUMP_HANDLER();
+ ML_BACKJUMP_STRUCT->id = ML_GET_NEXT_CHOICE_ID();
+ ML_BACKJUMP_STRUCT->saved_sp = MR_sp;
+ ML_BACKJUMP_STRUCT->saved_fr = MR_curfr;
+ ML_SET_BACKJUMP_HANDLER(ML_BACKJUMP_STRUCT);
+
+ ML_BACKJUMP_CHECKPOINT(""create"", ML_BACKJUMP_STRUCT);
+
+ MR_r1 = (MR_Word) ML_BACKJUMP_STRUCT->id;
+ MR_succeed();
+}
+MR_define_label(mercury__backjump__builtin_choice_id_1_0_i1);
+{
+ /* Restore the previous handler. */
+ ML_SET_BACKJUMP_HANDLER(ML_BACKJUMP_STRUCT->prev);
+ MR_fail();
+}
+
+MR_define_entry(mercury__backjump__builtin_backjump_1_0);
+{
+ ML_Choice_Id id = MR_r1;
+ ML_BackJumpHandler *backjump_handler = ML_GET_BACKJUMP_HANDLER();
+
+ /*
+ ** XXX see comments in the high-level implementation.
+ */
+ while (backjump_handler != NULL) {
+ if (backjump_handler->id == id) {
+ break;
+ }
+
+ ML_BACKJUMP_CHECKPOINT(""scan"", backjump_handler);
+
+ backjump_handler = backjump_handler->prev;
+ }
+
+ if (backjump_handler == NULL) {
+ ML_report_invalid_backjump(id);
+ exit(EXIT_FAILURE);
+ } else {
+ ML_BACKJUMP_CHECKPOINT(""found"", backjump_handler);
+
+ /*
+ ** XXX we should produce some EXCP trace events here, to give
+ ** the user an opportunity to retry a goal that calculated a
+ ** (possibly incorrect) backjump.
+ */
+
+ ML_SET_BACKJUMP_HANDLER(backjump_handler->prev);
+ MR_sp_word = (MR_Word) backjump_handler->saved_sp;
+ MR_maxfr_word = (MR_Word) backjump_handler->saved_fr;
+ MR_fail();
+ }
+}
+
+MR_END_MODULE
+
+#endif /* !MR_HIGHLEVEL_CODE */
+
+/*
+INIT mercury_sys_init_backjumps
+*/
+
+void mercury_sys_init_backjumps_init(void)
+{
+#ifndef MR_HIGHLEVEL_CODE
+ hand_written_backjump_module();
+#endif
+}
+
+void mercury_sys_init_backjumps_init_type_tables(void)
+{
+ /* no types to register */
+}
+
+#ifdef MR_DEEP_PROFILING
+void
+mercury_sys_init_backjumps_write_out_proc_statics(FILE *deep_fp,
+ FILE *procrep_fp)
+{
+ MR_write_out_user_proc_static(deep_fp, procrep_fp,
+ &MR_proc_layout_user_name(backjump, builtin_choice_id, 1, 0));
+ MR_write_out_user_proc_static(deep_fp, procrep_fp,
+ &MR_proc_layout_user_name(backjump, builtin_backjump, 1, 0));
+}
+#endif /* MR_DEEP_PROFILING */
+
+").
+
+%-----------------------------------------------------------------------------%
+
+:- pragma foreign_export("C", report_invalid_backjump(in, di, uo),
+ "ML_report_invalid_backjump").
+
+:- pred report_invalid_backjump(int::in, io::di, io::uo) is det.
+
+report_invalid_backjump(Id, !IO) :-
+ io.flush_output(!IO),
+ io.stderr_stream(StdErr, !IO),
+ io.format(StdErr, "Uncaught Mercury backjump (%d)\n", [i(Id)], !IO),
+ io.flush_output(StdErr, !IO).
+
+%-----------------------------------------------------------------------------%
+
+to_int(P) = P.
+
+%-----------------------------------------------------------------------------%
+:- end_module backjump.
+%-----------------------------------------------------------------------------%
Index: library/library.m
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/library/library.m,v
retrieving revision 1.118
diff -u -r1.118 library.m
--- library/library.m 31 Dec 2007 10:04:00 -0000 1.118
+++ library/library.m 5 Mar 2008 05:31:35 -0000
@@ -46,6 +46,7 @@
:- import_module array.
:- import_module array2d.
:- import_module assoc_list.
+:- import_module backjump.
:- import_module bag.
:- import_module benchmarking.
:- import_module bimap.
@@ -215,6 +216,7 @@
mercury_std_library_module("array").
mercury_std_library_module("array2d").
mercury_std_library_module("assoc_list").
+mercury_std_library_module("backjump").
mercury_std_library_module("bag").
mercury_std_library_module("benchmarking").
mercury_std_library_module("bimap").
Index: tests/hard_coded/Mmakefile
===================================================================
RCS file: /home/mercury/mercury1/repository/tests/hard_coded/Mmakefile,v
retrieving revision 1.341
diff -u -r1.341 Mmakefile
--- tests/hard_coded/Mmakefile 27 Feb 2008 09:46:08 -0000 1.341
+++ tests/hard_coded/Mmakefile 5 Mar 2008 05:31:35 -0000
@@ -464,18 +464,21 @@
# The following tests are passed only in some grades.
# The following tests do not work in the .profdeep grades.
-# All of them, aside from backend_external, don't work because
-# deep profiling cannot yet handle exceptions being caught and
+# All of them, aside from backend_external and backjump_test, don't work
+# because deep profiling cannot yet handle exceptions being caught and
# these test cases do that.
#
# backend_external fails because the predicates whose implementation
# is handwritten in C do not have the necessary proc_statics etc,
# defined.
+#
+# backjump_test fails because deep profiler cannot yet handle backjumps.
ifeq "$(findstring profdeep,$(GRADE))" ""
NON_PROFDEEP_PROGS = \
allow_stubs \
backend_external \
+ backjump_test \
bitmap_test \
bit_buffer_test \
dir_test \
Index: tests/hard_coded/backjump_test.exp
===================================================================
RCS file: tests/hard_coded/backjump_test.exp
diff -N tests/hard_coded/backjump_test.exp
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ tests/hard_coded/backjump_test.exp 5 Mar 2008 05:31:35 -0000
@@ -0,0 +1,25 @@
+label A = 1, (0)
+label B = 1, (1)
+label C = 1, (2)
+label C = 2, (3)
+backjump (3)
+label C = 3, (4)
+solution 1, 1, 3
+label B = 2, (5)
+label C = 1, (6)
+backjump (0)
+label A = 2, (7)
+label B = 1, (8)
+label C = 1, (9)
+solution 2, 1, 1
+label C = 2, (10)
+backjump (8)
+label B = 2, (11)
+label C = 1, (12)
+label C = 2, (13)
+solution 2, 2, 2
+label C = 3, (14)
+Solutions:
+{1, 1, 3},
+{2, 1, 1},
+{2, 2, 2}
Index: tests/hard_coded/backjump_test.m
===================================================================
RCS file: tests/hard_coded/backjump_test.m
diff -N tests/hard_coded/backjump_test.m
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ tests/hard_coded/backjump_test.m 5 Mar 2008 05:31:35 -0000
@@ -0,0 +1,88 @@
+%---------------------------------------------------------------------------%
+% vim: ft=mercury ts=4 sw=4 et
+%---------------------------------------------------------------------------%
+%
+% Author: Mark Brown <mark at csse.unimelb.edu.au>.
+%
+% Simulate nogood pruning using the backjump module.
+%
+%---------------------------------------------------------------------------%
+%---------------------------------------------------------------------------%
+
+:- module backjump_test.
+:- interface.
+
+:- import_module io.
+
+:- pred main(io::di, io::uo) is det.
+
+:- implementation.
+
+:- import_module backjump.
+:- import_module list.
+:- import_module solutions.
+:- import_module string.
+
+main(!IO) :-
+ solutions(problem, Sols),
+ (
+ Sols = [],
+ io.write_string("No solutions!\n", !IO)
+ ;
+ Sols = [_ | _],
+ io.write_string("Solutions:\n", !IO),
+ io.write_list(Sols, ",\n", io.write, !IO),
+ io.nl(!IO)
+ ).
+
+:- pred problem({int, int, int}::out) is nondet.
+
+problem({A, B, C}) :-
+ promise_pure (
+ impure label("A", [1, 2], A, PA),
+ impure label("B", [1, 2], B, PB),
+ impure label("C", [1, 2, 3], C, PC),
+ impure check(A, B, C, PA, PB, PC)
+ ).
+
+:- impure pred label(string::in, list(int)::in, int::out, choice_id::out)
+ is nondet.
+
+label(Name, [N | _], N, P) :-
+ impure get_choice_id(P),
+ trace [io(!IO)] (
+ io.format("label %s = %d, (%d)\n", [s(Name), i(N), i(to_int(P))], !IO),
+ true
+ ).
+label(Name, [_ | Ns], N, P) :-
+ impure label(Name, Ns, N, P).
+
+:- impure pred check(int::in, int::in, int::in, choice_id::in, choice_id::in,
+ choice_id::in) is semidet.
+
+check(A, B, C, PA, PB, PC) :-
+ ( is_nogood(A, B, C, PA, PB, PC, P) ->
+ trace [io(!IO)] (
+ io.format("backjump (%d)\n", [i(to_int(P))], !IO)
+ ),
+ impure backjump(P)
+ ;
+ is_solution(A, B, C),
+ trace [io(!IO)] (
+ io.format("solution %d, %d, %d\n", [i(A), i(B), i(C)], !IO)
+ )
+ ).
+
+:- pred is_nogood(int::in, int::in, int::in, choice_id::in, choice_id::in,
+ choice_id::in, choice_id::out) is semidet.
+
+is_nogood(1, 1, 2, _, _, P, P).
+is_nogood(1, 2, 1, P, _, _, P).
+is_nogood(2, 1, 2, _, P, _, P).
+
+:- pred is_solution(int::in, int::in, int::in) is semidet.
+
+is_solution(1, 1, 3).
+is_solution(2, 1, 1).
+is_solution(2, 2, 2).
+
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------
More information about the reviews
mailing list