matsc@sics.se (Mats Carlsson) (12/13/88)
I would like to share a way of representing sets of integers which I
have found useful in a theorem proving application. The sets are
represented as binary trees. The integers appear as markers in the
tree i.e. the values don't appear; instead, the value is implicitly
given by the position of the marker. The tree is really a
discrimination tree, starting with the least significant bit.
This representation isn't particularly good for doing set operations,
but it can be very efficient for searching for an element having some
property, like the subsumption test of a propositional theorem prover.
I'm sure others have come up with this representation of sets before,
but I don't recall seeing it anywhere.
% Module : isets
% Author : Mats Carlsson
% Updated: 881213
% Purpose: Integer set manipulation utilities
% In this module, sets of integers are built from the constructors
% [] - the empty set,
% $ - the set {0}, and
% $(A,B,C,D) - the set {4i | member(i,A)} U {4i+1 | member(i,B)} U
% {4i+2 | member(i,C)} U {4i+3 | member(i,D)}
% list_to_iset(+List, ?Set) :-
% Set represents the set of integers in List.
list_to_iset(List, Set) :-
list_to_iset(List, [], Set).
list_to_iset([], Set, Set).
list_to_iset([X|Xs], Set0, Set) :-
i_insert(Set0, X, Set1),
list_to_iset(Xs, Set1, Set).
% i_member(+Set, ?Element) :-
% Set contains Element.
i_member(Set, Element) :-
i_member(Set, 0, 1, Element).
i_member($, I, _, I).
i_member($(A,B,C,D), I, J, Element) :-
J1 is J<<2,
( i_member(A, I, J1, Element)
; I1 is I+J,
i_member(B, I1, J1, Element)
; I1 is I+2*J,
i_member(C, I1, J1, Element)
; I1 is I+3*J,
i_member(D, I1, J1, Element)
).
% i_contains(+Set, +Element) :-
% Set contains Element. Same as above, but searches for a given
% element. This routine is easily adapted to seach for an element
% having some property.
i_contains($, 0).
i_contains($(A,B,C,D), Label) :-
Label1 is Label/\3, Label2 is Label>>2,
i_contains(Label1, Label2, A, B, C, D).
i_contains(0, Label, A, _, _, _) :- i_contains(A, Label).
i_contains(1, Label, _, A, _, _) :- i_contains(A, Label).
i_contains(2, Label, _, _, A, _) :- i_contains(A, Label).
i_contains(3, Label, _, _, _, A) :- i_contains(A, Label).
% i_insert(+Set1, +Element, ?Set2) :-
% Set2 is the set Set1 with Element added.
i_insert(Set1, 0, Set2) :- !,
i_insert(Set1, Set2).
i_insert($(A,B,C,D), Label, Set) :-
Label1 is Label/\3, Label2 is Label>>2,
i_insert(Label1, Label2, Set, A, B, C, D).
i_insert([], Label, Set) :-
Label1 is Label/\3, Label2 is Label>>2,
i_insert(Label1, Label2, Set, [], [], [], []).
i_insert($, Label, Set) :-
Label1 is Label/\3, Label2 is Label>>2,
i_insert(Label1, Label2, Set, $, [], [], []).
i_insert(0, Label, $(A1,B,C,D), A, B, C, D) :- i_insert(A, Label, A1).
i_insert(1, Label, $(A,B1,C,D), A, B, C, D) :- i_insert(B, Label, B1).
i_insert(2, Label, $(A,B,C1,D), A, B, C, D) :- i_insert(C, Label, C1).
i_insert(3, Label, $(A,B,C,D1), A, B, C, D) :- i_insert(D, Label, D1).
i_insert([], $).
i_insert($, $).
i_insert($(A,B,C,D), $(A1,B,C,D)) :- i_insert(A, A1).
% i_delete(+Set1, +Element, ?Set2) :-
% Set2 is the set Set1 with Element removed.
i_delete($, 0, []).
i_delete($(A,B,C,D), Label, Set) :-
Label1 is Label/\3, Label2 is Label>>2,
i_delete(Label1, Label2, Set, A, B, C, D).
i_delete(0, Label, Set, A, B, C, D) :-
i_delete(A, Label, A1),
i_cons(A1, B, C, D, Set).
i_delete(1, Label, Set, A, B, C, D) :-
i_delete(B, Label, B1),
i_cons(A, B1, C, D, Set).
i_delete(2, Label, Set, A, B, C, D) :-
i_delete(C, Label, C1),
i_cons(A, B, C1, D, Set).
i_delete(3, Label, Set, A, B, C, D) :-
i_delete(D, Label, D1),
i_cons(A, B, C, D1, Set).
i_cons([], [], [], [], []) :- !.
i_cons($, [], [], [], $) :- !.
i_cons(A, B, C, D, $(A,B,C,D)).
% i_disjoint(+Set1, +Set2) :-
% The two sets have no element in common.
i_disjoint(Set1, Set2) :-
\+ i_intersect(Set1, Set2).
% i_intersect(+Set1, +Set2) :-
% The two sets have at least one element in common.
i_intersect($, Set) :- !, i_intersect(Set).
i_intersect(Set, $) :- !, i_intersect(Set).
i_intersect($(A,B,C,D), $(A1,B1,C1,D1)) :-
( i_intersect(A, A1) -> true
; i_intersect(B, B1) -> true
; i_intersect(C, C1) -> true
; i_intersect(D, D1) -> true
).
i_intersect($).
i_intersect($(A,_,_,_)) :- i_intersect(A).
% i_intersection(+Set1, +Set2, ?Intersection) :-
% Intersection is the set representing the intersection of Set1
% and Set2.
i_intersection([], _, []) :- !.
i_intersection(_, [], []) :- !.
i_intersection($, Set, Inter) :- !, i_intersection(Set, Inter).
i_intersection(Set, $, Inter) :- !, i_intersection(Set, Inter).
i_intersection($(A,B,C,D), $(A1,B1,C1,D1), Inter) :-
i_intersection(A, A1, A2),
i_intersection(B, B1, B2),
i_intersection(C, C1, C2),
i_intersection(D, D1, D2),
i_cons(A2, B2, C2, D2, Inter).
i_intersection([], []).
i_intersection($, $).
i_intersection($(A,_,_,_), Inter) :- i_intersection(A, Inter).
% i_seteq(+Set1, +Set2) :-
% The two arguments represent the same set.
i_seteq(Set, Set).
% i_subset(+Set1, +Set2)
% Every element of the set Set1 appears in the set Set2.
i_subset([], _).
i_subset($, Set) :- i_intersect(Set).
i_subset($(A,B,C,D), $(A1,B1,C1,D1)) :-
i_subset(A, A1),
i_subset(B, B1),
i_subset(C, C1),
i_subset(D, D1).
% i_difference(+Set1, +Set2, ?Difference) :-
% Difference contains all and only the elements of Set1
% which are not also in Set2.
i_difference([], _, []) :- !.
i_difference(Set, [], Set) :- !.
i_difference($, Set, Diff) :- !, i_subtract_1(Set, Diff).
i_difference(Set, $, Diff) :- !, i_subtract_2(Set, Diff).
i_difference($(A,B,C,D), $(A1,B1,C1,D1), Diff) :-
i_difference(A, A1, A2),
i_difference(B, B1, B2),
i_difference(C, C1, C2),
i_difference(D, D1, D2),
i_cons(A2, B2, C2, D2, Diff).
i_subtract_1([], $).
i_subtract_1($, []).
i_subtract_1($(A,_,_,_), Diff) :- i_subtract_1(A, Diff).
i_subtract_2([], []).
i_subtract_2($, []).
i_subtract_2($(A,B,C,D), $(A1,B,C,D)) :- i_subtract_2(A, A1).
% i_symdiff(+Set1, +Set2, ?Difference) :-
% Difference is the symmetric difference of Set1 and Set2.
i_symdiff([], Set, Set) :- !.
i_symdiff(Set, [], Set) :- !.
i_symdiff($, Set, Diff) :- !, i_symdiff(Set, Diff).
i_symdiff(Set, $, Diff) :- !, i_symdiff(Set, Diff).
i_symdiff($(A,B,C,D), $(A1,B1,C1,D1), Diff) :-
i_symdiff(A, A1, A2),
i_symdiff(B, B1, B2),
i_symdiff(C, C1, C2),
i_symdiff(D, D1, D2),
i_cons(A2, B2, C2, D2, Diff).
i_symdiff([], $).
i_symdiff($, []).
i_symdiff($(A,B,C,D), $(A1,B,C,D)) :- i_symdiff(A, A1).
% i_union(+Set1, +Set2, ?Union) :-
% Union is the union of Set1 and Set2.
i_union([], Set, Set) :- !.
i_union(Set, [], Set) :- !.
i_union($, Set, Union) :- !, i_insert(Set, Union).
i_union(Set, $, Union) :- !, i_insert(Set, Union).
i_union($(A,B,C,D), $(A1,B1,C1,D1), $(A2,B2,C2,D2)) :-
i_union(A, A1, A2),
i_union(B, B1, B2),
i_union(C, C1, C2),
i_union(D, D1, D2).
% i_union(+OldSet, +NewSet, ?Union, ?ReallyNew)
% Union is NewSet U OldSet and ReallyNew is NewSet \ OldSet.
i_union([], Set, Set, Set) :- !.
i_union(Set, [], Set, []) :- !.
i_union($, Set, Union, New) :- !, i_insert_1(Set, Union, New).
i_union(Set, $, Union, New) :- !, i_insert_2(Set, Union, New).
i_union($(A,B,C,D), $(A1,B1,C1,D1), $(A2,B2,C2,D2), New) :-
i_union(A, A1, A2, A3),
i_union(B, B1, B2, B3),
i_union(C, C1, C2, C3),
i_union(D, D1, D2, D3),
i_cons(A3, B3, C3, D3, New).
i_insert_1([], $, []).
i_insert_1($, $, []).
i_insert_1($(A,B,C,D), $(A1,B,C,D), $(A2,B,C,D)) :- i_insert_1(A, A1, A2).
i_insert_2([], $, $).
i_insert_2($, $, []).
i_insert_2($(A,B,C,D), $(A1,B,C,D), New) :- i_insert_2(A, A1, New).
--
Mats Carlsson
SICS, PO Box 1263, S-164 28 KISTA, Sweden
Internet: matsc@sics.se EAN: matsc@sics.sunet
Phone: +46 8 7521543 Fax: +46 8 7517230ok@quintus.uucp (Richard A. O'Keefe) (12/16/88)
In article <MATSC.88Dec13114720@skarabe.sics.se> matsc@sics.se (Mats Carlsson) writes: >I would like to share a way of representing sets of integers which I >have found useful in a theorem proving application. The sets are >represented as binary trees. Actually, they are 4-way trees. The method is a special case of David H.D. Warren's and Fernando Pereira's "logarithmic arrays" method, see LOGARR.PL in the DEC-10 Prolog library or library(logarr) in the Quintus Prolog library. The tree is just an array of bits.