[m-rev.] Added solver_types directory to samples
Ralph Becket
rafe at csse.unimelb.edu.au
Mon Feb 12 15:00:56 AEDT 2007
Estimated hours taken: 4
Branches: main
Added a sample solver type implementation to samples.
NEWS:
Report the addition.
samples/solver_types:
samples/solver_types/README:
samples/solver_types/Makefile:
samples/solver_types/eqneq.m:
samples/solver_types/sudoku.m:
samples/solver_types/sudoku_puzzle.easy:
samples/solver_types/sudoku_puzzle.hard:
samples/solver_types/test_eqneq.m:
Added.
Index: NEWS
===================================================================
RCS file: /home/mercury1/repository/mercury/NEWS,v
retrieving revision 1.443
diff -u -r1.443 NEWS
--- NEWS 11 Feb 2007 04:05:22 -0000 1.443
+++ NEWS 12 Feb 2007 03:55:09 -0000
@@ -91,6 +91,11 @@
clock interrupts, this can yield useful profiles for shorter-running
programs.
+Changes to the samples directory:
+
+* The samples directory now includes an example of how to implement a
+ solver type.
+
DETAILED LISTING
================
Index: samples/README
===================================================================
RCS file: /home/mercury1/repository/mercury/samples/README,v
retrieving revision 1.8
diff -u -r1.8 README
--- samples/README 7 Sep 2006 08:32:20 -0000 1.8
+++ samples/README 12 Feb 2007 03:53:53 -0000
@@ -63,3 +63,6 @@
muz This directory contains a syntax checker / type checker
for the specification language Z.
+
+solver_types This directory contains an example solver type
+ implementation and some sample applications.
Index: samples/solver_types/Makefile
===================================================================
RCS file: samples/solver_types/Makefile
diff -N samples/solver_types/Makefile
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ samples/solver_types/Makefile 12 Feb 2007 03:47:42 -0000
@@ -0,0 +1,9 @@
+.PHONY: all
+
+all: sudoku test_eqneq
+
+sudoku: sudoku.m eqneq.m
+ mmc --make sudoku --use-grade-subdirs --use-trail
+
+test_eqneq: test_eqneq.m eqneq.m
+ mmc --make test_eqneq --use-grade-subdirs --use-trail
Index: samples/solver_types/README
===================================================================
RCS file: samples/solver_types/README
diff -N samples/solver_types/README
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ samples/solver_types/README 12 Feb 2007 03:50:58 -0000
@@ -0,0 +1,15 @@
+eqneq.m:
+ An implementation of a solver type admitting equality and
+ disequality constraints for variables ranging over ground
+ values. This provides some of the functionality of Prolog
+ variables.
+
+sudoku.m:
+ A naive sudoku solver.
+
+sudoku_puzzle.easy:
+sudoku_puzzle.hard:
+ Sample input for the sudoku solver.
+
+test_eqneq.m:
+ A test case.
Index: samples/solver_types/eqneq.m
===================================================================
RCS file: samples/solver_types/eqneq.m
diff -N samples/solver_types/eqneq.m
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ samples/solver_types/eqneq.m 12 Feb 2007 03:52:52 -0000
@@ -0,0 +1,375 @@
+%-----------------------------------------------------------------------------%
+% 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) variable 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) variables.
+ %
+:- 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.
+
+
+
+ % An eqneq is represented by an eqneq_id, which is a key in the
+ % mutable constraint_store map.
+ %
+:- solver type eqneq(T) where
+ representation is eqneq_id,
+ initialisation is new,
+ equality is eq.
+
+:- type eqneq_id == int.
+
+ % The constraint_store mutable maps eqneq_ids to eqneq_reps.
+ %
+:- mutable(constraint_store, constraint_store, map.init, ground).
+
+:- type constraint_store == map(eqneq_id, eqneq_rep).
+
+ % The eqneq_id_counter mutable is used to allocate new eqneq_ids.
+ %
+:- mutable(eqneq_id_counter, counter, counter.init(0), ground).
+
+ % Each eqneq is either free, bound, or aliased to another eqneq.
+ %
+:- 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).
+
+%-----------------------------------------------------------------------------%
+
+ % 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 (this information helps keep alias chains
+ % short).
+ %
+:- 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. We ensure that neq sets are kept
+ % up-to-date after unifications.
+ %
+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
+
+ % eqneqs with the same id are already equated.
+ %
+ true
+
+ else
+
+ (
+ % If both are free, then check the neq constraints and
+ % make one an alias of the other, unifying the neq
+ % constraints. We use the depth information to keep
+ % alias chains short.
+ %
+ EqNeqRepA = free_neq(NeqSetA0),
+ EqNeqRepB = free_neq(NeqSetB0),
+
+ NeqSetA = update_neq_set(ConstraintStore0, NeqSetA0),
+ not set.member(EqNeqIdA, NeqSetB0),
+ NeqSetB = update_neq_set(ConstraintStore0, NeqSetB0),
+ not set.member(EqNeqIdB, NeqSetA0),
+ NeqSetAB = set.union(NeqSetA, NeqSetB),
+
+ ( if DepthB =< DepthA then
+ ConstraintStore =
+ (( ConstraintStore0
+ ^ elem(EqNeqIdA) := free_neq(NeqSetAB) )
+ ^ elem(EqNeqIdB) := alias(EqNeqIdA) )
+ else
+ ConstraintStore =
+ (( ConstraintStore0
+ ^ elem(EqNeqIdB) := free_neq(NeqSetAB) )
+ ^ elem(EqNeqIdA) := alias(EqNeqIdB) )
+ ),
+ impure set_constraint_store(ConstraintStore)
+
+ ;
+
+ % A is free, B is bound: we need only check the
+ % neq constraints.
+ %
+ EqNeqRepA = free_neq(NeqSetA0),
+ EqNeqRepB = bound(_UnivB),
+
+ NeqSetA = update_neq_set(ConstraintStore0, NeqSetA0),
+ not set.member(EqNeqIdB, NeqSetA),
+ ConstraintStore =
+ ConstraintStore0 ^ elem(EqNeqIdA) := EqNeqRepB,
+ impure set_constraint_store(ConstraintStore)
+
+ ;
+
+ % B is free, A is bound: we need only check the
+ % neq constraints.
+ %
+ EqNeqRepA = bound(_UnivA),
+ EqNeqRepB = free_neq(NeqSetB0),
+
+ NeqSetB = update_neq_set(ConstraintStore0, NeqSetB0),
+ not set.member(EqNeqIdA, NeqSetB),
+ ConstraintStore =
+ ConstraintStore0 ^ elem(EqNeqIdB) := EqNeqRepA,
+ impure set_constraint_store(ConstraintStore)
+
+ ;
+
+ % Both are bound.
+ %
+ EqNeqRepA = bound(UnivA),
+ EqNeqRepB = bound(UnivB),
+
+ UnivA = UnivB
+ )
+ )
+ ).
+
+
+:- func update_neq_set(constraint_store, set(eqneq_id)) = set(eqneq_id).
+
+update_neq_set(ConstraintStore, Neqs0) = Neqs :-
+ P = ( func(EqNeqId0, NeqSet0) = NeqSet :-
+ deref(ConstraintStore, EqNeqId0, EqNeqId, _EqNeqRep, _Depth),
+ NeqSet = set.insert(NeqSet0, EqNeqId)
+ ),
+ Neqs = set.fold(P, Neqs0, set.init).
+
+%-----------------------------------------------------------------------------%
+
+ % 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,
+
+ (
+ % Both eqneqs are free.
+ %
+ 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)
+
+ ;
+
+ % A is free, B is bound.
+ %
+ EqNeqRepA = free_neq(NeqSetA0),
+ EqNeqRepB = bound(_UnivB),
+
+ NeqSetA = set.insert(NeqSetA0, EqNeqIdB),
+ ConstraintStore =
+ ConstraintStore0 ^ elem(EqNeqIdA) := free_neq(NeqSetA),
+ impure set_constraint_store(ConstraintStore)
+
+ ;
+
+ % A is bound, B is free.
+ %
+ EqNeqRepA = bound(_UnivA),
+ EqNeqRepB = free_neq(NeqSetB0),
+
+ NeqSetB = set.insert(NeqSetB0, EqNeqIdA),
+ ConstraintStore =
+ ConstraintStore0 ^ elem(EqNeqIdB) := free_neq(NeqSetB),
+ impure set_constraint_store(ConstraintStore)
+
+ ;
+
+ % A and B are bound.
+ %
+ 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).
+
+%-----------------------------------------------------------------------------%
+%-----------------------------------------------------------------------------%
Index: samples/solver_types/sudoku.m
===================================================================
RCS file: samples/solver_types/sudoku.m
diff -N samples/solver_types/sudoku.m
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ samples/solver_types/sudoku.m 12 Feb 2007 03:47:42 -0000
@@ -0,0 +1,184 @@
+%-----------------------------------------------------------------------------%
+% 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)
+ ).
+
+%-----------------------------------------------------------------------------%
+
+ % Solve a sudoko problem.
+ %
+:- pred solve_sudoku(list(string)::in, list(int)::out) is nondet.
+
+solve_sudoku(Start, Solution) :-
+
+ % Set up the board.
+ %
+ 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],
+
+ % The digits in each row must be different.
+ %
+ 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]),
+
+ % The digits in each column must be different.
+ %
+ 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]),
+
+ % The digits in each subsquare must be different.
+ %
+ 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]),
+
+ % Assign a digit to each square on the board.
+ %
+ label_board(Board, Solution).
+
+%-----------------------------------------------------------------------------%
+
+ % Convert a board description into a board representation. Each "word" in
+ % the board description is either a digit, in which case we fix that board
+ % entry in the representation, or a non-digit, in which case we leave that
+ % board entry unconstrained.
+ %
+:- 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).
+
+%-----------------------------------------------------------------------------%
+
+ % Assign a digit to each square on the board.
+ %
+:- 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).
+
+%-----------------------------------------------------------------------------%
+
+ % Pretty-print a solution.
+ %
+:- 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)
+ ).
+
+%-----------------------------------------------------------------------------%
+%-----------------------------------------------------------------------------%
Index: samples/solver_types/sudoku_puzzle.easy
===================================================================
RCS file: samples/solver_types/sudoku_puzzle.easy
diff -N samples/solver_types/sudoku_puzzle.easy
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ samples/solver_types/sudoku_puzzle.easy 12 Feb 2007 03:47:53 -0000
@@ -0,0 +1,11 @@
+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
Index: samples/solver_types/sudoku_puzzle.hard
===================================================================
RCS file: samples/solver_types/sudoku_puzzle.hard
diff -N samples/solver_types/sudoku_puzzle.hard
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ samples/solver_types/sudoku_puzzle.hard 12 Feb 2007 03:47:53 -0000
@@ -0,0 +1,11 @@
+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
Index: samples/solver_types/test_eqneq.m
===================================================================
RCS file: samples/solver_types/test_eqneq.m
diff -N samples/solver_types/test_eqneq.m
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ samples/solver_types/test_eqneq.m 12 Feb 2007 03:47:42 -0000
@@ -0,0 +1,71 @@
+%-----------------------------------------------------------------------------%
+% test_eqneq.m
+% Ralph Becket <rafe at csse.unimelb.edu.au>
+% Mon Feb 12 12:33:57 EST 2007
+% vim: ft=mercury ts=4 sw=4 et wm=0 tw=0
+%
+% Test case.
+%
+%-----------------------------------------------------------------------------%
+
+:- module test_eqneq.
+
+:- 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) :-
+ ( if solve(Solution) then
+ io.print(Solution, !IO),
+ io.nl(!IO)
+ else
+ io.print("no solution\n", !IO)
+ ).
+
+%-----------------------------------------------------------------------------%
+
+:- pred solve(list(int)::out) is nondet.
+
+solve(Solution) :-
+ eqneq.n_new(9, Xs),
+ Xs = [X1, X2, X3, X4, X5, X6, X7, X8, X9],
+ X1 = X4, X4 = X7,
+ X2 = X5, X5 = X8,
+ X3 = X6, X6 = X9,
+ neq(X1, X2),
+ neq(X1, X3),
+ neq(X2, X3),
+ label(Xs, Solution).
+
+%-----------------------------------------------------------------------------%
+
+:- pred label(list(eqneq(int))::ia, list(int)::out) is nondet.
+
+label([], []).
+
+label([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(EqNeqs, Xs).
+
+%-----------------------------------------------------------------------------%
+%-----------------------------------------------------------------------------%
--------------------------------------------------------------------------
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