1		% (c) 2009-2022 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
2		% Heinrich Heine Universitaet Duesseldorf
3		% This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
5		:- module(chr_set_membership,[chr_subset/2, chr_not_subset/2,
6		chr_subset_strict/2, chr_not_subset_strict/2,
7		chr_member/2, chr_not_member/2]).
8
9		:- use_module(probsrc(module_information),[module_info/2]).
10		:- module_info(group,kernel).
11		:- module_info(description,'Provide interface to CHR set reasoning.').
12
13		:- use_module(library(chr)).
14		:- chr_option(check_guard_bindings,off).
15		:- chr_option(optimize,full).
16
17		% restore operators overwritten by chr library
18		% otherwise, unary operators might not be parseable
19		:- op(200, fy, [+,-]).
20		:- op(500, yfx, \).
21
22		% assumes we use CLP(FD) to complement it
23
24		chr_subset(S1,S2) :- subset(S1,S2).
25		chr_not_subset(S1,S2) :- not_subset(S1,S2).
26
27		chr_subset_strict(S1,S2) :- subset_strict(S1,S2) .
28		chr_not_subset_strict(S1,S2) :- not_subset_strict(S1,S2).
29
30		chr_member(E,S) :- member_of(E,S).
31		chr_not_member(E,S) :- not_member_of(E,S).
32		% TODO: reification-trigger: when can we infer membership or non-membership
33
34		:- chr_constraint subset/2, not_subset/2.
35		:- chr_constraint subset_strict/2, not_subset_strict/2.
36		:- chr_constraint member_of/2, not_member_of/2.
37
38
39		contradiction @ subset(X,Y), not_subset(X,Y) <=> fail.
40		reflexivity @ subset(X,X) <=> true.
41		antisymmetry @ subset(X,Y), subset(Y,X) <=> X = Y.
42		idempotence @ subset(X,Y) \ subset(X,Y) <=> true.
43		transitivity @ subset(X,Y), subset(Y,Z) ==> subset(X,Z).
44		%checking @ subset(X,Y) <=> nonvar(X),nonvar(Y) | X =< Y.
45
46		contradiction @ subset_strict(X,Y), not_subset_strict(X,Y) <=> fail.
47		contradiction @ subset_strict(X,Y), not_subset(X,Y) <=> fail.
48		antireflexivity @ subset_strict(X,X) <=> fail.
49		idempotence @ subset_strict(X,Y) \ subset_strict(X,Y) <=> true.
50		transitivity @ subset_strict(X,Y), subset(Y,Z) ==> subset_strict(X,Z).
51		transitivity @ subset(X,Y), subset_strict(Y,Z) ==> subset_strict(X,Z).
52		transitivity @ subset_strict(X,Y), subset_strict(Y,Z) ==> subset_strict(X,Z).
53		%checking @ lt(X,Y) <=> nonvar(X),nonvar(Y) | X < Y.
54
55		idempotence @ member_of(X,Y) \ member_of(X,Y) <=> true.
56		idempotence @ not_member_of(X,Y) \ not_member_of(X,Y) <=> true.
57		contradiction @ member_of(X,Y), not_member_of(X,Y) <=> fail.
58		contradiction @ member_of(X,Y), not_member_of(X,Z), subset(Y,Z) <=> fail.
59		contradiction @ member_of(X,Y), not_member_of(X,Z), subset_strict(Y,Z) <=> fail.
60
61		% member_of(X,Y) => not_empty(Y)
62		% not_empty(X), empty(X) <=> fail.
63		% subset(X,Y), not_empty(X) => not_empty(Y).
64		% subset_strict(X,Y) => not_empty(Y).