[mercury-users] Modes for partly uninstantiated list
Ralph Becket
rafe at csse.unimelb.edu.au
Fri Feb 9 15:58:53 AEDT 2007
Ralph Becket, Wednesday, 7 February 2007:
> Okay, when I get a spare couple of hours I'll try to write a simple
> sudoku solver using solver types.
Attached is:
- a module implementing a simple solver type, eqneq(T), supporting
equality and disequality constraints (this file could do with some
more comments...);
- a naive sudoku solver using the eqneq(T) type;
- a Makefile;
- a couple of input files.
You'll need to have a trailing grade installed to make this work.
Cheers,
-- Ralph
-------------- next part --------------
%-----------------------------------------------------------------------------%
% sudoku.m
% Ralph Becket <rafe at csse.unimelb.edu.au>
% Fri Feb 9 15:03:53 EST 2007
% vim: ft=mercury ts=4 sw=4 et wm=0 tw=0
%
% Sudoku test case for the eqneq type.
%
%-----------------------------------------------------------------------------%
:- module sudoku.
:- interface.
:- import_module io.
:- pred main(io :: di, io :: uo) is cc_multi.
%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%
:- implementation.
:- import_module eqneq.
:- import_module int.
:- import_module list.
:- import_module string.
%-----------------------------------------------------------------------------%
main(!IO) :-
io.command_line_arguments(Args, !IO),
( if Args = [InputFile] then
io.see(InputFile, SeeResult, !IO),
(
SeeResult = ok,
io.read_file_as_string(ReadResult, !IO),
(
ReadResult = ok(StartString),
Start = string.words(StartString),
( if solve_sudoku(Start, Solution) then
write_solution(9, Solution, !IO)
else
io.write_string("no solution\n", !IO)
)
;
ReadResult = error(_, Error),
io.write_string(io.error_message(Error), !IO),
io.nl(!IO),
io.set_exit_status(1, !IO)
)
;
SeeResult = error(Error),
io.write_string(io.error_message(Error), !IO),
io.nl(!IO),
io.set_exit_status(1, !IO)
)
else
io.write_string("usage: sudoku filename\n", !IO),
io.set_exit_status(1, !IO)
).
%-----------------------------------------------------------------------------%
:- pred solve_sudoku(list(string)::in, list(int)::out) is nondet.
solve_sudoku(Start, Solution) :-
init_board(Start, Board),
Board = [X11, X12, X13, X14, X15, X16, X17, X18, X19,
X21, X22, X23, X24, X25, X26, X27, X28, X29,
X31, X32, X33, X34, X35, X36, X37, X38, X39,
X41, X42, X43, X44, X45, X46, X47, X48, X49,
X51, X52, X53, X54, X55, X56, X57, X58, X59,
X61, X62, X63, X64, X65, X66, X67, X68, X69,
X71, X72, X73, X74, X75, X76, X77, X78, X79,
X81, X82, X83, X84, X85, X86, X87, X88, X89,
X91, X92, X93, X94, X95, X96, X97, X98, X99],
eqneq.all_different([X11, X12, X13, X14, X15, X16, X17, X18, X19]),
eqneq.all_different([X21, X22, X23, X24, X25, X26, X27, X28, X29]),
eqneq.all_different([X31, X32, X33, X34, X35, X36, X37, X38, X39]),
eqneq.all_different([X41, X42, X43, X44, X45, X46, X47, X48, X49]),
eqneq.all_different([X51, X52, X53, X54, X55, X56, X57, X58, X59]),
eqneq.all_different([X61, X62, X63, X64, X65, X66, X67, X68, X69]),
eqneq.all_different([X71, X72, X73, X74, X75, X76, X77, X78, X79]),
eqneq.all_different([X81, X82, X83, X84, X85, X86, X87, X88, X89]),
eqneq.all_different([X91, X92, X93, X94, X95, X96, X97, X98, X99]),
eqneq.all_different([X11, X21, X31, X41, X51, X61, X71, X81, X91]),
eqneq.all_different([X12, X22, X32, X42, X52, X62, X72, X82, X92]),
eqneq.all_different([X13, X23, X33, X43, X53, X63, X73, X83, X93]),
eqneq.all_different([X14, X24, X34, X44, X54, X64, X74, X84, X94]),
eqneq.all_different([X15, X25, X35, X45, X55, X65, X75, X85, X95]),
eqneq.all_different([X16, X26, X36, X46, X56, X66, X76, X86, X96]),
eqneq.all_different([X17, X27, X37, X47, X57, X67, X77, X87, X97]),
eqneq.all_different([X18, X28, X38, X48, X58, X68, X78, X88, X98]),
eqneq.all_different([X19, X29, X39, X49, X59, X69, X79, X89, X99]),
eqneq.all_different([X11, X12, X13, X21, X22, X23, X31, X32, X33]),
eqneq.all_different([X14, X15, X16, X24, X25, X26, X34, X35, X36]),
eqneq.all_different([X17, X18, X19, X27, X28, X29, X37, X38, X39]),
eqneq.all_different([X41, X42, X43, X51, X52, X53, X61, X62, X63]),
eqneq.all_different([X44, X45, X46, X54, X55, X56, X64, X65, X66]),
eqneq.all_different([X47, X48, X49, X57, X58, X59, X67, X68, X69]),
eqneq.all_different([X71, X72, X73, X81, X82, X83, X91, X92, X93]),
eqneq.all_different([X74, X75, X76, X84, X85, X86, X94, X95, X96]),
eqneq.all_different([X77, X78, X79, X87, X88, X89, X97, X98, X99]),
label_board(Board, Solution).
%-----------------------------------------------------------------------------%
:- pred init_board(list(string)::in, list(eqneq(int))::oa) is semidet.
init_board([], []).
init_board([Start | Starts], [EqNeq | EqNeqs]) :-
eqneq.new(EqNeq),
( if string.to_int(Start, X)
then eqneq.bind(EqNeq, X)
else true
),
init_board(Starts, EqNeqs).
%-----------------------------------------------------------------------------%
:- pred label_board(list(eqneq(int))::ia, list(int)::out) is nondet.
label_board([], []).
label_board([EqNeq | EqNeqs], [X | Xs]) :-
( X = 1 ; X = 2 ; X = 3
; X = 4 ; X = 5 ; X = 6
; X = 7 ; X = 8 ; X = 9
),
eqneq.bind(EqNeq, X),
label_board(EqNeqs, Xs).
%-----------------------------------------------------------------------------%
:- pred write_solution(int::in, list(int)::in, io::di, io::uo) is det.
write_solution(_, [], !IO) :-
io.nl(!IO).
write_solution(N, [X | Xs], !IO) :-
( if N = 0 then
io.nl(!IO),
write_solution(9, [X | Xs], !IO)
else
io.write_int(X, !IO),
io.write_char(' ', !IO),
write_solution(N - 1, Xs, !IO)
).
%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%
-------------- next part --------------
%-----------------------------------------------------------------------------%
% eqneq.m
% Ralph Becket <rafe at csse.unimelb.edu.au>
% Fri Feb 9 13:31:22 EST 2007
% vim: ft=mercury ts=4 sw=4 et wm=0 tw=0
%
% Simple solver type supporting equality and disequality constraints.
%
%-----------------------------------------------------------------------------%
:- module eqneq.
:- interface.
:- import_module list.
% An eqneq(T) value may be bound to a ground value of type T or it
% may be unbound. Equality and disequality constraints may be
% posted between eqneq(T) values.
%
:- solver type eqneq(T).
% Construct a new eqneq.
%
:- pred new(eqneq(T)::oa) is det.
% Construct N new eqneqs.
%
:- pred n_new(int::in, list(eqneq(T))::oa) is det.
% Post an equality/disequality constraint between two eqneqs.
%
:- pred eq(eqneq(T)::ia, eqneq(T)::ia) is semidet.
:- pred neq(eqneq(T)::ia, eqneq(T)::ia) is semidet.
% Bind an eqneq to a ground value.
%
:- pred bind(eqneq(T)::ia, T::in) is semidet.
% Ask for the value, if any, bound to an eqneq.
%
:- impure pred ask_value(eqneq(T)::ia, T::out) is semidet.
% Utility predicate.
%
:- pred all_different(list(eqneq(T))::ia) is semidet.
%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%
:- implementation.
:- import_module counter.
:- import_module int.
:- import_module map.
:- import_module set.
:- import_module univ.
:- solver type eqneq(T) where
representation is eqneq_id,
initialisation is new,
equality is eq.
:- type eqneq_rep
% A free eqneq node records the set of variables it is
% not equal to.
---> free_neq(set(eqneq_id))
% An aliased eqneq is represented by another eqneq.
; alias(eqneq_id)
% A bound eqneq has a value stored as a univ.
; bound(univ).
:- type eqneq_id == int.
:- mutable(constraint_store, constraint_store, map.init, ground).
:- type constraint_store == map(eqneq_id, eqneq_rep).
:- mutable(eqneq_id_counter, counter, counter.init(0), ground).
%-----------------------------------------------------------------------------%
% Create a new, free, eqneq.
%
new(EqNeq) :-
promise_pure (
semipure get_eqneq_id_counter(EqNeqIdCounter0),
semipure get_constraint_store(ConstraintStore0),
counter.allocate(EqNeqId, EqNeqIdCounter0, EqNeqIdCounter),
NeqSet = set.init,
ConstraintStore = ConstraintStore0 ^ elem(EqNeqId) := free_neq(NeqSet),
impure set_eqneq_id_counter(EqNeqIdCounter),
impure set_constraint_store(ConstraintStore),
impure EqNeq = 'representation to any eqneq/1'(EqNeqId)
).
%-----------------------------------------------------------------------------%
% Create a list of new, free, eqneqs.
%
n_new(N, EqNeqs) :-
( if N =< 0 then
EqNeqs = []
else
new(EqNeq),
n_new(N - 1, EqNeqs0),
EqNeqs = [EqNeq | EqNeqs0]
).
%-----------------------------------------------------------------------------%
% Follow the alias chain for an eqneq to the end, keeping track of
% the number of links in the chain.
%
:- pred deref(constraint_store::in, eqneq_id::in, eqneq_id::out,
eqneq_rep::out, int::out) is det.
deref(ConstraintStore, EqNeqId0, EqNeqId, EqNeqRep, Depth) :-
deref_2(ConstraintStore, EqNeqId0, EqNeqId, EqNeqRep, 0, Depth).
:- pred deref_2(constraint_store::in, eqneq_id::in, eqneq_id::out,
eqneq_rep::out, int::in, int::out) is det.
deref_2(ConstraintStore, EqNeqId0, EqNeqId, EqNeqRep, Depth0, Depth) :-
EqNeqRep0 = ConstraintStore ^ det_elem(EqNeqId0),
( if EqNeqRep0 = alias(EqNeqId1) then
deref_2(ConstraintStore, EqNeqId1, EqNeqId, EqNeqRep,
Depth0 + 1, Depth)
else
EqNeqId = EqNeqId0,
EqNeqRep = EqNeqRep0,
Depth = Depth0
).
%-----------------------------------------------------------------------------%
% Constrain two eqneqs to be equal.
%
eq(EqNeqA, EqNeqB) :-
promise_pure (
impure EqNeqIdA0 = 'representation of any eqneq/1'(EqNeqA),
impure EqNeqIdB0 = 'representation of any eqneq/1'(EqNeqB),
semipure get_constraint_store(ConstraintStore0),
deref(ConstraintStore0, EqNeqIdA0, EqNeqIdA, EqNeqRepA, DepthA),
deref(ConstraintStore0, EqNeqIdB0, EqNeqIdB, EqNeqRepB, DepthB),
( if EqNeqIdA = EqNeqIdB then
true
else
(
EqNeqRepA = free_neq(NeqSetA0),
EqNeqRepB = free_neq(NeqSetB0),
not set.member(EqNeqIdA, NeqSetB0),
not set.member(EqNeqIdB, NeqSetA0),
( if DepthB =< DepthA then
NeqSetA = set.union(NeqSetA0, NeqSetB0),
ConstraintStore =
(( ConstraintStore0
^ elem(EqNeqIdA) := free_neq(NeqSetA) )
^ elem(EqNeqIdB) := alias(EqNeqIdA) )
else
NeqSetB = set.union(NeqSetB0, NeqSetA0),
ConstraintStore =
(( ConstraintStore0
^ elem(EqNeqIdB) := free_neq(NeqSetB) )
^ elem(EqNeqIdA) := alias(EqNeqIdB) )
),
impure set_constraint_store(ConstraintStore)
;
EqNeqRepA = free_neq(NeqSetA),
EqNeqRepB = bound(_UnivB),
not set.member(EqNeqIdB, NeqSetA),
ConstraintStore =
ConstraintStore0 ^ elem(EqNeqIdA) := EqNeqRepB,
impure set_constraint_store(ConstraintStore)
;
EqNeqRepA = bound(_UnivA),
EqNeqRepB = free_neq(NeqSetB),
not set.member(EqNeqIdA, NeqSetB),
ConstraintStore =
ConstraintStore0 ^ elem(EqNeqIdB) := EqNeqRepA,
impure set_constraint_store(ConstraintStore)
;
EqNeqRepA = bound(UnivA),
EqNeqRepB = bound(UnivB),
UnivA = UnivB
)
)
).
%-----------------------------------------------------------------------------%
% Constrain two eqneqs to be different.
%
neq(EqNeqA, EqNeqB) :-
promise_pure (
impure EqNeqIdA0 = 'representation of any eqneq/1'(EqNeqA),
impure EqNeqIdB0 = 'representation of any eqneq/1'(EqNeqB),
semipure get_constraint_store(ConstraintStore0),
deref(ConstraintStore0, EqNeqIdA0, EqNeqIdA, EqNeqRepA, _DepthA),
deref(ConstraintStore0, EqNeqIdB0, EqNeqIdB, EqNeqRepB, _DepthB),
EqNeqIdA \= EqNeqIdB,
(
EqNeqRepA = free_neq(NeqSetA0),
EqNeqRepB = free_neq(NeqSetB0),
NeqSetA = set.insert(NeqSetA0, EqNeqIdB),
NeqSetB = set.insert(NeqSetB0, EqNeqIdA),
ConstraintStore =
(( ConstraintStore0 ^ elem(EqNeqIdA) := free_neq(NeqSetA) )
^ elem(EqNeqIdB) := free_neq(NeqSetB) ),
impure set_constraint_store(ConstraintStore)
;
EqNeqRepA = free_neq(NeqSetA0),
EqNeqRepB = bound(_UnivB),
NeqSetA = set.insert(NeqSetA0, EqNeqIdB),
ConstraintStore =
ConstraintStore0 ^ elem(EqNeqIdA) := free_neq(NeqSetA),
impure set_constraint_store(ConstraintStore)
;
EqNeqRepA = bound(_UnivA),
EqNeqRepB = free_neq(NeqSetB0),
NeqSetB = set.insert(NeqSetB0, EqNeqIdA),
ConstraintStore =
ConstraintStore0 ^ elem(EqNeqIdB) := free_neq(NeqSetB),
impure set_constraint_store(ConstraintStore)
;
EqNeqRepA = bound(UnivA),
EqNeqRepB = bound(UnivB),
UnivA \= UnivB
)
).
%-----------------------------------------------------------------------------%
% Bind an eqneq to a ground value.
%
bind(EqNeq, Value) :-
promise_pure (
impure EqNeqId0 = 'representation of any eqneq/1'(EqNeq),
semipure get_constraint_store(ConstraintStore0),
deref(ConstraintStore0, EqNeqId0, EqNeqId, EqNeqRep, _Depth),
(
EqNeqRep = free_neq(NeqSet),
not (
set.member(EqNeqIdX0, NeqSet),
deref(ConstraintStore0, EqNeqIdX0, _EqNeqIdX, EqNeqRepX,
_DepthX),
EqNeqRepX = bound(UnivX),
univ_to_type(UnivX, Value)
),
ConstraintStore =
ConstraintStore0 ^ elem(EqNeqId) := bound(univ(Value)),
impure set_constraint_store(ConstraintStore)
;
EqNeqRep = bound(Univ),
univ_to_type(Univ, Value)
)
).
%-----------------------------------------------------------------------------%
% Ask for the value bound to an eqneq, if any.
%
ask_value(EqNeq, Value) :-
impure EqNeqId0 = 'representation of any eqneq/1'(EqNeq),
semipure get_constraint_store(ConstraintStore0),
deref(ConstraintStore0, EqNeqId0, _EqNeqId, EqNeqRep, _Depth),
EqNeqRep = bound(Univ),
univ_to_type(Univ, Value).
%-----------------------------------------------------------------------------%
all_different([]).
all_different([X | Xs]) :-
all_different_2(X, Xs),
all_different(Xs).
:- pred all_different_2(eqneq(T)::ia, list(eqneq(T))::ia) is semidet.
all_different_2(_, []).
all_different_2(X, [Y | Ys]) :-
neq(X, Y),
all_different_2(X, Ys).
%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%
-------------- next part --------------
sudoku: sudoku.m eqneq.m
mmc --make sudoku --use-grade-subdirs --use-trail
-------------- next part --------------
6 . . 1 . 8 2 . 3
. 2 . . 4 . . 9 .
8 . 3 . . 5 4 . .
5 . 4 6 . 7 . . 9
. 3 . . . . . 5 .
7 . . 8 . 3 1 . 2
. . 1 7 . . 9 . 6
. 8 . . 3 . . 2 .
3 . 2 9 . 4 . . 5
-------------- next part --------------
3 . . . . 8 . . .
7 . 8 3 2 . . . 5
. . . 9 . . . 1 .
9 . . . . 4 . 2 .
. . . . 1 . . . .
. 7 . 8 . . . . 9
. 5 . . . 3 . . .
8 . . . 4 7 5 . 3
. . . 5 . . . . 6
More information about the users
mailing list