1 % (c) 2021-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(kernel_non_empty_attr,[
6 mark_var_set_as_non_empty/1,
7 get_empty_set_attr/3
8 ]).
9
10 :- use_module(tools_portability, [exists_source/1]).
11
12 :- use_module(module_information,[module_info/2]).
13 :- module_info(group,kernel).
14 :- module_info(description,'This module provides operations for non-emptyness of sets, storing them as attributes.').
15
16
17 % TO DO: link with kernel_cardinality attributes, either by calling reify_empty_set_test or clpfd_card_is_gt0_for_var
18 % or by propagating information back from kernel_cardinality_attr
19
20 % Note: setting the Empty Variable itself will not instantiate the corresponding set
21 % this is still done e.g. in kernel_equality by eq_empty_set when calling get_empty_set_attr
22 % or by not_empty_set_lwf in case of mark_var_set_as_non_empty
23
24 % relevant tests:
25 % test 2021 : from 5 seconds to 15 ms (second run)
26
27 % Portable attributed variable handling.
28 % Use SICStus-style library(atts) and verify_attributes/3 if available,
29 % otherwise the SWI/hProlog-style attr builtins and attr_unify_hook/2.
30 :- if(\+ exists_source(library(atts))).
31
32 mark_var_set_as_non_empty(Set) :- get_attr(Set,kernel_non_empty_attr,kernel_is_empty_attr(EmptyRes)),!,
33 EmptyRes=pred_false.
34 mark_var_set_as_non_empty(Set) :- put_attr(Set,kernel_non_empty_attr,kernel_is_empty_attr(pred_false)).
35
36 get_empty_set_attr(Set,Empty,Exists) :- get_attr(Set,kernel_non_empty_attr,kernel_is_empty_attr(EmptyRes)),!,
37 Empty=EmptyRes,Exists=is_empty_attr_exists.
38 get_empty_set_attr(Set,Empty,new) :- put_attr(Set,kernel_non_empty_attr,kernel_is_empty_attr(Empty)).
39
40 attr_unify_hook(kernel_is_empty_attr(EmptyRes),Value) :- !,
41 update_non_empty(Value,EmptyRes).
42
43 update_non_empty(Value,EmptyRes) :-
44 var(Value),!,
45 (get_attr(Value,kernel_non_empty_attr,kernel_is_empty_attr(EmptyRes2))
46 -> EmptyRes=EmptyRes2 % unify attributes
47 ; put_attr(Value,kernel_non_empty_attr,kernel_is_empty_attr(EmptyRes)) % copy attribute to new variable
48 ).
49 update_non_empty(_,_).
50
51 :- else.
52
53 :- use_module(library(atts)).
54
55 :- attribute kernel_is_empty_attr/1.
56
57
58 % mark a variable set as non empty
59 % (marking as empty is not necessary; simply instantiate to [])
60 mark_var_set_as_non_empty(Set) :- get_atts(Set,+kernel_is_empty_attr(EmptyRes)),!,
61 EmptyRes=pred_false.
62 mark_var_set_as_non_empty(Set) :- put_atts(Set,+kernel_is_empty_attr(pred_false)).
63
64
65 % get the empty set attribute for a variable; create if no attribute exists
66 get_empty_set_attr(Set,Empty,Exists) :- get_atts(Set,+kernel_is_empty_attr(EmptyRes)),!,
67 Empty=EmptyRes,Exists=is_empty_attr_exists.
68 get_empty_set_attr(Set,Empty,new) :- put_atts(Set,+kernel_is_empty_attr(Empty)).
69
70
71
72 % Attribute unification:
73 % verify_attributes is called whenever a variable Var that might have attributes is about to be bound to Value (it might have none).
74 % verify(VariableBeforeUnification, ValueWithWhichVariableUnifies, GoalWhichSICStusShouldCallAfterUnif)
75 verify_attributes(ThisVar,Value,Goal) :-
76 get_atts(ThisVar,+kernel_is_empty_attr(EmptyRes)),!,
77 %print(update(ThisVar,empty(EmptyRes),Value)),nl,
78 update_non_empty(Value,EmptyRes,Goal).
79 verify_attributes(_, _, [] ).
80
81 update_non_empty(Value,EmptyRes,Goal) :-
82 var(Value),!,
83 (get_atts(Value,+kernel_is_empty_attr(EmptyRes2))
84 -> Goal = [EmptyRes=EmptyRes2] % unify attributes
85 ; put_atts(Value,+kernel_is_empty_attr(EmptyRes)), % copy attribute to new variable
86 Goal=[]
87 ).
88 update_non_empty(_,_,[]).
89
90
91 :- endif.
92
93 :- use_module(error_manager).
94
95 % we assume the attribute variable will be set outside of this module, e.g., by eq_empty_set
96 % if not : we could add this code here:
97 %update_non_empty([],EmptyRes,_,Goal) :- !, Goal=[EmptyRes=pred_true].
98 %update_non_empty([_|_],EmptyRes,_,Goal) :- !, Goal = [EmptyRes=pred_false].
99 %update_non_empty(avl_set(_),EmptyRes,_,Goal) :- !, Goal = [EmptyRes=pred_false].
100 %update_non_empty(CS,EmptyRes,WF,Goal) :- is_custom_explicit_set(CS,update_non_empty),!,
101 % Goal = [test_empty(CS,EmptyRes,WF)].
102 %update_non_empty(S,E,WF,Goal) :-
103 % add_internal_error('Illegal Set: ',update_non_empty(S,E,WF,Goal)),Goal=[].
104 %
105 %test_empty(CS,EmptyRes,WF) :- EmptyRes == pred_false,!,
106 % is_non_empty_explicit_set_wf(CS,WF).
107 %test_empty(CS,EmptyRes,WF) :- EmptyRes == pred_true,!,
108 % is_empty_explicit_set_wf(CS,WF).
109 %test_empty(CS,EmptyRes,WF) :-
110 % test_empty_explicit_set_wf(CS,EmptyRes,WF).
111
112
113 :- use_module(self_check).
114 :- assert_must_succeed( ( mark_var_set_as_non_empty(X), get_empty_set_attr(X,E,is_empty_attr_exists), E==pred_false) ).
115 :- assert_must_succeed( ( mark_var_set_as_non_empty(X), get_empty_set_attr(R,E,new), R=X, E==pred_false)).
116 :- assert_must_succeed( ( get_empty_set_attr(R,E,new), var(E), mark_var_set_as_non_empty(X), var(E), R=X, E==pred_false)).
117 :- assert_must_succeed( ( get_empty_set_attr(R,E,new), R=[], var(E), E=pred_true)).
118 :- assert_must_succeed( ( get_empty_set_attr(R,E,new), R=[int(1)], var(E), E=pred_false)).