Puzzle Utilities: Difference between revisions
Created page with "The following predicates are used in the puzzle solutions. ==Higher-order Predicates== ====unique_solution( +Goal )==== holds when <var>Goal</var> has one ground solution. ..." |
|||
| (4 intermediate revisions by the same user not shown) | |||
| Line 5: | Line 5: | ||
====unique_solution( +Goal )==== | ====unique_solution( +Goal )==== | ||
holds when <var>Goal</var> has one ground solution. Operationally, <var>Goal</var> | holds when <var>Goal</var> has one ground solution. Operationally, <var>Goal</var> may produce several proofs of the solution, ("don't care" non-deterministically), but they must all be identical (<code>==</code>). | ||
may produce several | |||
they must all be identical (<code>==</code>). | |||
< | <pre class="prolog">unique_solution( Goal ) :- | ||
findall( Goal, Goal, [Solution| | findall( Goal, Goal, [Solution|Proofs] ), | ||
same_solution( | same_solution( Proofs, Solution ), | ||
Solution = Goal. | Solution = Goal. | ||
same_solution( [], _Solution ). | same_solution( [], _Solution ). | ||
same_solution( [ | same_solution( [Proof|Proofs], Solution ) :- | ||
Proof == Solution, | |||
same_solution( | same_solution( Proofs, Solution ).</pre> | ||
====forall( +Enumerator, +Test )==== | ====forall( +Enumerator, +Test )==== | ||
| Line 24: | Line 22: | ||
holds everywhere that <var>Enumerator</var> does. NB: forall/2 does not instantiate arguments further. | holds everywhere that <var>Enumerator</var> does. NB: forall/2 does not instantiate arguments further. | ||
< | <pre class="prolog">forall( Enumerator, Test ) :- | ||
\+ (call(Enumerator), \+ call(Test)).</ | \+ (call(Enumerator), \+ call(Test)).</pre> | ||
====count_solutions( +Goal, ?Count )==== | ====count_solutions( +Goal, ?Count )==== | ||
| Line 33: | Line 31: | ||
<code>count_solutions/2</code> enumerates the possible solutions to <var>Goal</var> but does not instantiate <var>Goal</var>'s arguments further. | <code>count_solutions/2</code> enumerates the possible solutions to <var>Goal</var> but does not instantiate <var>Goal</var>'s arguments further. | ||
< | <pre class="prolog"> | ||
count_solutions( Goal, Count ) :- | count_solutions( Goal, Count ) :- | ||
findall( x, Goal, Xs ), | findall( x, Goal, Xs ), | ||
length( Xs, Count ). | length( Xs, Count ). | ||
</ | </pre> | ||
==Lists== | ==Lists== | ||
| Line 44: | Line 42: | ||
holds when <var>Element</var> is a member of <var>List</var>. | holds when <var>Element</var> is a member of <var>List</var>. | ||
< | <pre class="prolog">member( H, [H|_] ). | ||
member( H, [_|T] ) :- | member( H, [_|T] ) :- | ||
member( H, T ).</ | member( H, T ).</pre> | ||
====select( ?Element, ?List0, ?List1 )==== | ====select( ?Element, ?List0, ?List1 )==== | ||
| Line 52: | Line 50: | ||
is true if <var>List1</var> is equal to <var>List0</var> with <var>Element</var> removed. | is true if <var>List1</var> is equal to <var>List0</var> with <var>Element</var> removed. | ||
< | <pre class="prolog">select( H, [H|T], T ). | ||
select( Element, [H|T0], [H|T1] ) :- | select( Element, [H|T0], [H|T1] ) :- | ||
select( Element, T0, T1 ).</ | select( Element, T0, T1 ).</pre> | ||
====memberchk( +Element, +List )==== | ====memberchk( +Element, +List )==== | ||
| Line 60: | Line 58: | ||
succeeds (once) if <var>Element</var> is a member of <var>List</var>. | succeeds (once) if <var>Element</var> is a member of <var>List</var>. | ||
< | <pre class="prolog">memberchk( Element, List ) :- | ||
member( Element, List ), | member( Element, List ), | ||
!.</ | !.</pre> | ||
====append( ?Front, ?Back, ?List )==== | |||
succeeds if <var>Front</var>, <var>Back</var> and <var>List</var> are all lists | |||
and <var>List</var> is the concatenation of <var>Front</var> and <var>Back</var>. | |||
<pre class="prolog">append( [], L, L ). | |||
append( [H|T], L, [H|L1] ) :- | |||
append( T, L, L1 ). | |||
</pre> | |||
====length( ?List, ?N )==== | |||
succeeds if <var>N</var> is the length of <var>List</var>. | |||
<pre class="prolog">length( List, N ) :- | |||
len1( List, 0, N ). | |||
len1( [], N, N ). | |||
len1( [_H|T], N0, N ) :- | |||
N1 is N0+1, | |||
len1( T, N1, N ). | |||
</pre> | |||
==Arithmetic== | ==Arithmetic== | ||
| Line 72: | Line 94: | ||
* <var>Index</var> is a logical variable: a series of alternative solutions may be generated as the monotonic sequence of values between <var>Lower</var> and <var>Upper</var> (non-deterministic generator). | * <var>Index</var> is a logical variable: a series of alternative solutions may be generated as the monotonic sequence of values between <var>Lower</var> and <var>Upper</var> (non-deterministic generator). | ||
< | <pre class="prolog">between( Lower, Upper, Index ) :- | ||
integer( Lower ), | integer( Lower ), | ||
integer( Upper ), | integer( Upper ), | ||
| Line 90: | Line 112: | ||
Next =< Upper, | Next =< Upper, | ||
generate_between( Next, Upper, Index ) | generate_between( Next, Upper, Index ) | ||
).</ | ).</pre> | ||
====sum( +List, ?Sum )==== | ====sum( +List, ?Sum )==== | ||
| Line 96: | Line 118: | ||
holds when the <var>List</var> of numbers sum to <var>Sum</var>. | holds when the <var>List</var> of numbers sum to <var>Sum</var>. | ||
< | <pre class="prolog">sum( [H|T], Sum ) :- | ||
sum1( T, H, Sum ). | sum1( T, H, Sum ). | ||
| Line 102: | Line 124: | ||
sum1( [H|T], Sum0, Sum ):- | sum1( [H|T], Sum0, Sum ):- | ||
Sum1 is Sum0 + H, | Sum1 is Sum0 + H, | ||
sum1( T, Sum1, Sum ).</ | sum1( T, Sum1, Sum ).</pre> | ||
==Character Input/Output== | ==Character Input/Output== | ||
| Line 110: | Line 132: | ||
if <var>Chars</var> is a (possibly empty) list of character codes and the corresponding characters are written to the current output stream. | if <var>Chars</var> is a (possibly empty) list of character codes and the corresponding characters are written to the current output stream. | ||
< | <pre class="prolog">put_chars( [] ). | ||
put_chars( [Char|Chars] ) :- | put_chars( [Char|Chars] ) :- | ||
put( Char ), | put( Char ), | ||
put_chars( Chars ).</ | put_chars( Chars ).</pre> | ||
====get_chars( ?Chars )==== | ====get_chars( ?Chars )==== | ||
| Line 119: | Line 141: | ||
if <var>Chars</var> is a (possibly empty) list of character codes read from the current input stream. | if <var>Chars</var> is a (possibly empty) list of character codes read from the current input stream. | ||
< | <pre class="prolog">get_chars( Input ) :- | ||
get0( Char ), | get0( Char ), | ||
( Char > -1 -> | ( Char > -1 -> | ||
| Line 126: | Line 148: | ||
; otherwise -> | ; otherwise -> | ||
Input = [] | Input = [] | ||
).</ | ).</pre> | ||
The code is available as plain text [https://binding-time.co.uk/download/misc.txt here]. | The code is available as plain text [https://binding-time.co.uk/download/misc.txt here]. | ||
Latest revision as of 18:36, 5 April 2020
The following predicates are used in the puzzle solutions.
Higher-order Predicates
unique_solution( +Goal )
holds when Goal has one ground solution. Operationally, Goal may produce several proofs of the solution, ("don't care" non-deterministically), but they must all be identical (==).
unique_solution( Goal ) :-
findall( Goal, Goal, [Solution|Proofs] ),
same_solution( Proofs, Solution ),
Solution = Goal.
same_solution( [], _Solution ).
same_solution( [Proof|Proofs], Solution ) :-
Proof == Solution,
same_solution( Proofs, Solution ).
forall( +Enumerator, +Test )
is true if Enumerator and Test are goals and Test holds everywhere that Enumerator does. NB: forall/2 does not instantiate arguments further.
forall( Enumerator, Test ) :-
\+ (call(Enumerator), \+ call(Test)).
count_solutions( +Goal, ?Count )
is true if Count is the number of solutions for Goal. The solutions might not be distinct.
count_solutions/2 enumerates the possible solutions to Goal but does not instantiate Goal's arguments further.
count_solutions( Goal, Count ) :-
findall( x, Goal, Xs ),
length( Xs, Count ).
Lists
member( ?Element, ?List )
holds when Element is a member of List.
member( H, [H|_] ).
member( H, [_|T] ) :-
member( H, T ).
select( ?Element, ?List0, ?List1 )
is true if List1 is equal to List0 with Element removed.
select( H, [H|T], T ).
select( Element, [H|T0], [H|T1] ) :-
select( Element, T0, T1 ).
memberchk( +Element, +List )
succeeds (once) if Element is a member of List.
memberchk( Element, List ) :-
member( Element, List ),
!.
append( ?Front, ?Back, ?List )
succeeds if Front, Back and List are all lists and List is the concatenation of Front and Back.
append( [], L, L ).
append( [H|T], L, [H|L1] ) :-
append( T, L, L1 ).
length( ?List, ?N )
succeeds if N is the length of List.
length( List, N ) :-
len1( List, 0, N ).
len1( [], N, N ).
len1( [_H|T], N0, N ) :-
N1 is N0+1,
len1( T, N1, N ).
Arithmetic
between( +Lower, +Upper, ?Index )
is true if Lower =< Index =< Upper. Two valid cases are possible:
- Index is already instantiated to an integer, so the checks on order are applied (test).
- Index is a logical variable: a series of alternative solutions may be generated as the monotonic sequence of values between Lower and Upper (non-deterministic generator).
between( Lower, Upper, Index ) :-
integer( Lower ),
integer( Upper ),
Lower =< Upper,
( integer( Index ) -> % Case 1: "test"
Index >= Lower,
Index =< Upper
; var( Index ) -> % Case 2: "generate".
generate_between( Lower, Upper, Index )
).
generate_between( Lower, Upper, Index ) :-
( Lower =:= Upper ->
Index = Lower
; Index = Lower
; Next is Lower + 1,
Next =< Upper,
generate_between( Next, Upper, Index )
).
sum( +List, ?Sum )
holds when the List of numbers sum to Sum.
sum( [H|T], Sum ) :-
sum1( T, H, Sum ).
sum1( [], Sum, Sum ).
sum1( [H|T], Sum0, Sum ):-
Sum1 is Sum0 + H,
sum1( T, Sum1, Sum ).
Character Input/Output
put_chars( +Chars )
if Chars is a (possibly empty) list of character codes and the corresponding characters are written to the current output stream.
put_chars( [] ).
put_chars( [Char|Chars] ) :-
put( Char ),
put_chars( Chars ).
get_chars( ?Chars )
if Chars is a (possibly empty) list of character codes read from the current input stream.
get_chars( Input ) :-
get0( Char ),
( Char > -1 ->
Input = [Char|Chars],
get_chars( Chars )
; otherwise ->
Input = []
).
The code is available as plain text here.