| 1 | % (c) 2009-2024 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_cardinality_attr,[finite_cardinality_as_int_wf/3, | |
| 6 | finite_cardinality_as_int_with_type_wf/5, | |
| 7 | clpfd_card_domain_for_var/3 | |
| 8 | ]). | |
| 9 | ||
| 10 | :- use_module(module_information,[module_info/2]). | |
| 11 | :- module_info(group,kernel). | |
| 12 | :- module_info(description,'This module provides operations for cardinality of sets, storing them as attributes.'). | |
| 13 | ||
| 14 | ||
| 15 | :- use_module(custom_explicit_sets,[explicit_set_cardinality_wf/3, is_interval_closure/3]). | |
| 16 | :- use_module(kernel_waitflags,[add_wd_error/3, add_wd_error_span/4, add_abort_error_span/5]). | |
| 17 | :- use_module(kernel_objects,[empty_set_wf/2, max_cardinality/2, | |
| 18 | disjoint_sets/3, add_new_element_wf/4, not_element_of_wf/3, | |
| 19 | exhaustive_kernel_check_wf/2]). | |
| 20 | :- use_module(library(clpfd)). | |
| 21 | :- use_module(clpfd_interface,[clpfd_max_bounded/1]). | |
| 22 | :- use_module(self_check). | |
| 23 | :- use_module(tools_portability, [exists_source/1]). | |
| 24 | ||
| 25 | ||
| 26 | ||
| 27 | /* | |
| 28 | Examples: | |
| 29 | x<:1..200000 & card(x) = 2*card(y) & card(y):3..44 & x/\y = {} & card(x) = 130-card(y) | |
| 30 | 3.8 seconds before, now 1 ms to detect failure | |
| 31 | card(x) : 10..200 & card(y) : card(x)..300 & card(y)+card(x) = 500 & x : POW(1..10000) & y: POW(1..10000) | |
| 32 | now solved much faster 1 second vs ??? | |
| 33 | ||
| 34 | STATUS: | |
| 35 | TO DO: replace cardinality_as_int in kernel_objects completely and add version here that returns inf/... | |
| 36 | TO DO: call finite_cardinality_as_int_with_type_wf if possible | |
| 37 | TO DO: Test 1631 NBishops has become slower (943d37585be8eeac46c93705d51c2392fde0fda3) | |
| 38 | ||
| 39 | failed tests: | |
| 40 | ** Failed tests: | |
| 41 | 33 without SMT mode | |
| 42 | x:POW(7..8) & card(x)=1 & x /= {7} --> no longer deterministically sets x={8} with SMT=FALSE | |
| 43 | calls: kernel_objects:not_equal_explicit_set/2: AVL{int(7)}: VARIABLE: _17573 | |
| 44 | ||
| 45 | now fixed: | |
| 46 | 1627 | |
| 47 | 1828 Check card operator does not generate solutions with repeated entries | |
| 48 | union(s) = {} & x<:INTEGER & x:s & card(s)=2 succeeds | |
| 49 | union(s) = {} & x<:INTEGER & x:s & card(s)=2 succeeds | |
| 50 | 38 -> probably we need to set up list skel before infinite enumeration | |
| 51 | 223 -> overflow | |
| 52 | 496 Many explicit computations which check that all operators work as expected on various concrete data. | |
| 53 | 1187 Ensure proper enumeration of sequences (CLPFD=FALSE). | |
| 54 | 1418 Test this is solved quickly using new ordered_value check for card. | |
| 55 | card(x)=10 & !y.(y:x & y<50 => y+1:x) & x<:1..50 | |
| 56 | 1419 Test this is solved quickly using new ordered_value check for card & avoid bug in expand all quantifeir. | |
| 57 | 1611 Ensure proper enumeration of sequences (CLPFD=TRUE). | |
| 58 | 1625 Check card of interval propagates | |
| 59 | 568 ProZ test | |
| 60 | 1540 Test Integer Z laws and that the division semantics of Z is preserved. | |
| 61 | 1850 Test loading .tex file works | |
| 62 | 1776 Check compilation of while with op call and inner while works | |
| 63 | */ | |
| 64 | ||
| 65 | ||
| 66 | % Portable attributed variable handling. | |
| 67 | % Use SICStus-style library(atts) and verify_attributes/3 if available, | |
| 68 | % otherwise the SWI/hProlog-style attr builtins and attr_unify_hook/2. | |
| 69 | :- if(\+ exists_source(library(atts))). | |
| 70 | ||
| 71 | get_kernel_card_attr(Var,Card,WF) :- get_attr(Var,kernel_cardinality_attr,kernel_card_attr(Card,WF)). | |
| 72 | put_kernel_card_attr(Var,Card,WF) :- put_attr(Var,kernel_cardinality_attr,kernel_card_attr(Card,WF)). | |
| 73 | ||
| 74 | :- use_module(library(lists), [maplist/2]). | |
| 75 | attr_unify_hook(kernel_card_attr(Card,WF),Value) :- | |
| 76 | update_card(Value,Card,Goal,WF), | |
| 77 | maplist(call, Goal). | |
| 78 | ||
| 79 | :- else. | |
| 80 | ||
| 81 | :- use_module(library(atts)). | |
| 82 | ||
| 83 | :- attribute kernel_card_attr/2. | |
| 84 | ||
| 85 | get_kernel_card_attr(Var,Card,WF) :- get_atts(Var,+kernel_card_attr(Card,WF)). | |
| 86 | put_kernel_card_attr(Var,Card,WF) :- put_atts(Var,+kernel_card_attr(Card,WF)). | |
| 87 | ||
| 88 | % Attribute unification: | |
| 89 | % verify_attributes is called whenever a variable Var that might have attributes is about to be bound to Value (it might have none). | |
| 90 | % verify_attributes/3 may invoke arbitrary Prolog goals, but Var should not be bound by it. | |
| 91 | % verify(VariableBeforeUnification, ValueWithWhichVariableUnifies, GoalWhichSICStusShouldCallAfterUnif) | |
| 92 | verify_attributes(ThisVar,Value,Goal) :- | |
| 93 | get_atts(ThisVar,+kernel_card_attr(Card,WF)),!, | |
| 94 | update_card(Value,Card,Goal,WF). | |
| 95 | verify_attributes(_, _, [] ). | |
| 96 | ||
| 97 | :- endif. | |
| 98 | ||
| 99 | ||
| 100 | finite_cardinality_as_int_with_type_wf(Set,ObjectType,Info,int(Card),WF) :- | |
| 101 | max_cardinality(ObjectType,MaxCard), | |
| 102 | %format('card with type=~w, maxcard=~w, Info=~w~n',[ObjectType,MaxCard,Info]), | |
| 103 | %tools_printing:print_term_summary(Set), | |
| 104 | finite_card_wf(Set,0,MaxCard,Info,[],Card,WF). | |
| 105 | % print('card = '),tools_printing:print_integer(Card),nl,print(set(Set)),nl,nl. | |
| 106 | ||
| 107 | ||
| 108 | :- assert_must_succeed((finite_cardinality_as_int_wf(Y,int(X),_WF), Y = [fd(1,'Name'),fd(2,'Name')],X==2)). | |
| 109 | :- assert_must_succeed(exhaustive_kernel_check_wf(kernel_cardinality_attr:finite_cardinality_as_int_wf([int(2),int(4),int(1)],int(3),WF),WF)). | |
| 110 | :- assert_must_succeed((finite_cardinality_as_int_wf(Y,int(2),no_wf_available), Y = [fd(1,'Name'),fd(2,'Name')])). | |
| 111 | :- assert_must_fail((finite_cardinality_as_int_wf(Y,int(3),no_wf_available), Y = [fd(1,'Name'),fd(2,'Name')])). | |
| 112 | :- assert_must_succeed((finite_cardinality_as_int_wf(Y,int(X),no_wf_available), | |
| 113 | Y = [H1|YY], YY=[H2], X==2, H1=int(0), H2=int(3) )). | |
| 114 | :- assert_must_succeed((finite_cardinality_as_int_wf([A|Y],int(3),no_wf_available), | |
| 115 | Y = [B|YY], YY=[C], kernel_objects:equal_object([A,B,C], [int(1),int(3),int(2)]) | |
| 116 | %,A=int(1),B=int(3),C=int(2) not possible because of ordered list skeleton setup below | |
| 117 | )). | |
| 118 | :- assert_must_succeed((finite_cardinality_as_int_wf(Y,int(1),no_wf_available), Y = [fd(1,'Name')])). | |
| 119 | :- assert_must_succeed((finite_cardinality_as_int_wf(Y,int(0),no_wf_available), Y = [])). | |
| 120 | :- assert_must_succeed((finite_cardinality_as_int_wf(X,int(3),no_wf_available), kernel_objects:equal_object(X,global_set('Name')))). | |
| 121 | :- assert_must_fail((finite_cardinality_as_int_wf(Y,int(X),no_wf_available), Y = [fd(1,'Name'),fd(2,'Name')],dif(X,2))). | |
| 122 | :- assert_must_succeed_any((preferences:preference(use_clpfd_solver,false) ; | |
| 123 | finite_cardinality_as_int_wf(S,int(C),no_wf_available), clpfd_interface:force_post_constraint('#='(C,2)), nonvar(S),S=[A|T],nonvar(T),A=int(1),T=[int(2)])). | |
| 124 | % does not work yet: | |
| 125 | %:- assert_must_succeed_any((preferences:preference(use_clpfd_solver,false) ; | |
| 126 | % finite_cardinality_as_int_wf(S,int(C),no_wf_available), clpfd_interface:force_post_constraint('#>='(C,2)), nonvar(S),S=[_|T],nonvar(T))). | |
| 127 | :- assert_must_succeed((finite_cardinality_as_int_wf([int(1)|avl_set(node(int(3),true,0,empty,empty))],int(2),no_wf_available))). | |
| 128 | :- assert_must_succeed((finite_cardinality_as_int_wf([int(1)|avl_set(node(int(3),true,0,empty,empty))],X,no_wf_available),X==int(2))). | |
| 129 | % check that we deal with repeated elements, in case no other predicate sets up a list ! | |
| 130 | :- assert_must_fail((finite_cardinality_as_int_wf([int(1),int(1)],int(2),no_wf_available))). | |
| 131 | :- assert_must_fail((finite_cardinality_as_int_wf([int(1),int(1)],_,no_wf_available))). | |
| 132 | :- assert_must_fail((finite_cardinality_as_int_wf(X,int(2),no_wf_available),X=[int(1),int(1)])). | |
| 133 | :- assert_must_fail((finite_cardinality_as_int_wf([int(3)|avl_set(node(int(3),true,0,empty,empty))],_,no_wf_available))). | |
| 134 | :- assert_must_fail((finite_cardinality_as_int_wf([X|avl_set(node(int(3),true,0,empty,empty))],int(2),no_wf_available),X=int(3))). | |
| 135 | ||
| 136 | :- assert_must_succeed(( finite_cardinality_as_int_wf(V,int(X),no_wf_available), X in 1..5, finite_cardinality_as_int_wf(V,int(X2),no_wf_available), X2 in 5..10, X2==5 , V=[int(1),int(2),int(3),int(4),int(5)])). | |
| 137 | :- assert_must_succeed(( finite_cardinality_as_int_wf(V,int(X),no_wf_available), X in 1..5, finite_cardinality_as_int_wf(V,int(X2),no_wf_available), X2 in 5..10, V=[_A,_B,_C,_D,_E|T], T==[], | |
| 138 | V=[int(1),int(2),int(3),int(4),int(5)])). | |
| 139 | ||
| 140 | ||
| 141 | finite_cardinality_as_int_wf(Set,int(Card),WF) :- | |
| 142 | finite_card_wf(Set,0,inf,[contains_wd_condition],[],Card,WF). | |
| 143 | ||
| 144 | finite_card_wf(Var,Acc,MaxCard,_Info,ElementsSoFar,Card,WF) :- var(Var), | |
| 145 | !, | |
| 146 | Card #= VCard+Acc, | |
| 147 | card_for_var(Var,VCard,ElementsSoFar,WF), | |
| 148 | check_no_duplicates(Var,ElementsSoFar,WF), | |
| 149 | restrict_card(Card,MaxCard). | |
| 150 | finite_card_wf([],Acc,_,_Info,_,Card,_WF) :- !, Card=Acc. | |
| 151 | finite_card_wf([H|T],Acc,MaxCard,Info,ElementsSoFar,Card,WF) :- !, A1 is Acc+1, | |
| 152 | check_and_add_new_element(H,ElementsSoFar,ElementsSoFar2,WF), | |
| 153 | finite_card_wf(T,A1,MaxCard,Info,ElementsSoFar2,Card,WF). | |
| 154 | finite_card_wf(CS,Acc,MaxCard,Info,ElementsSoFar,Card,WF) :- | |
| 155 | explicit_set_cardinality_wf(CS,CSCard,WF), %print(cs_card(Acc,CSCard)),nl, | |
| 156 | add_cs_card(CS,CSCard,Acc,MaxCard,Info,Card,WF), | |
| 157 | disjoint_sets(ElementsSoFar,CS,WF). | |
| 158 | ||
| 159 | :- block check_no_duplicates(-,?,?). | |
| 160 | check_no_duplicates([],_,_) :- !. | |
| 161 | check_no_duplicates([H|T],ElementsSoFar,WF) :- !, | |
| 162 | check_and_add_new_element(H,ElementsSoFar,ElementsSoFar2,WF), | |
| 163 | check_no_duplicates(T,ElementsSoFar2,WF). | |
| 164 | check_no_duplicates(CS,ElementsSoFar,WF) :- | |
| 165 | disjoint_sets(CS,ElementsSoFar,WF). | |
| 166 | % we have to check here that the list is really a set if we return cardinality | |
| 167 | % sometimes the outer predicates do not ensure this | |
| 168 | % e.g. for test 1828 we have that union(s) = {} & x<:INTEGER & x:s & card(s)=2 may otherwise succeed | |
| 169 | % and generate a list with two identical elements: [ [], [] ] | |
| 170 | % ideally the rest of the kernel should ensure that such lists are not generated; we may generate some redundant work here | |
| 171 | check_and_add_new_element(H,ElementSoFar,SoFar2,WF) :- | |
| 172 | not_element_of_wf(H,ElementSoFar,WF), | |
| 173 | add_new_element_wf(H,ElementSoFar,SoFar2,WF). | |
| 174 | ||
| 175 | card_for_var(Var,Card,_ElementsSoFar,_WF) :- get_kernel_card_attr(Var,StoredCard,_), % could be other WF ! | |
| 176 | !, | |
| 177 | Card=StoredCard. | |
| 178 | card_for_var(Var,Card,ElementsSoFar,WF) :- Card #>= 0, put_kernel_card_attr(Var,Card,WF), | |
| 179 | force_empty_and_set_skel(Card,Var,ElementsSoFar,WF). | |
| 180 | ||
| 181 | % Note : it is important to not instantiate variables or trigger co-routines which could instantiate top-level Variable | |
| 182 | update_card(Value,Card,Goal,WF) :- var(Value),!, | |
| 183 | (get_kernel_card_attr(Value,Card2,_) % could be other WF | |
| 184 | -> Goal = [Card=Card2] | |
| 185 | ; put_kernel_card_attr(Value,Card,WF), Goal=[] | |
| 186 | ). | |
| 187 | update_card([],Card,Goal,_WF) :- !, Goal=[Card=0]. | |
| 188 | update_card([_|T],Card,Goal,WF) :- !, get_list_tail(T,1,Tail,Delta), | |
| 189 | % calling the following directly resulted in errors for test 402 (co-routines not being activated) | |
| 190 | (number(Card) | |
| 191 | % optimisation is important for performance of test 32 (SETUP_CONSTANTS) | |
| 192 | -> C1 is Card-Delta, | |
| 193 | (C1=0 -> Goal = [empty_set_wf(Tail,WF)] | |
| 194 | ; C1<0 -> %print(inconsistent_card(Card,Delta,C1)),nl, fail, | |
| 195 | Goal =[fail] % it seems ok to call fail directly; occurs in tests 974, 1962 | |
| 196 | ; update_card(Tail,C1,Goal,WF) | |
| 197 | ) | |
| 198 | ; Goal = [Card #= C1+Delta, C1 #>= 0, force_empty(C1,Tail,WF) |TGoal], | |
| 199 | update_card(Tail,C1,TGoal,WF) | |
| 200 | ). | |
| 201 | update_card(CS,Card,Goal,WF) :- | |
| 202 | Goal = [safe_explicit_set_cardinality_wf(CS,Card,WF)]. | |
| 203 | ||
| 204 | ||
| 205 | get_list_tail(Tail,Acc,Tail,Res) :- var(Tail),!,Res=Acc. | |
| 206 | get_list_tail([_|T],Acc,Tail,Res) :- !, A1 is Acc+1, get_list_tail(T,A1,Tail,Res). | |
| 207 | get_list_tail(Tail,Acc,Tail,Res) :- !,Res=Acc. | |
| 208 | ||
| 209 | :- block force_empty(-,-,?). | |
| 210 | force_empty(Card,Set,WF) :- %print(emp(Card,Set)),nl, | |
| 211 | Card==0, | |
| 212 | !, | |
| 213 | empty_set_wf(Set,WF). | |
| 214 | force_empty(_,_,_). | |
| 215 | ||
| 216 | ||
| 217 | :- use_module(kernel_waitflags,[get_wait_flag/4]). | |
| 218 | % wake up if Card is set and then force empty set or setup list skeleton | |
| 219 | :- block force_empty_and_set_skel(-,-,?,?). | |
| 220 | force_empty_and_set_skel(Card,Set,_ElementsSoFar,WF) :- % print(force_empty_and_set_skel(Card,Set)),nl, | |
| 221 | Card==0, | |
| 222 | !, | |
| 223 | empty_set_wf(Set,WF). | |
| 224 | force_empty_and_set_skel(Card,Set,ElementsSoFar,WF) :- var(Set), number(Card), | |
| 225 | !, | |
| 226 | (preferences:preference(use_smt_mode,true) | |
| 227 | -> Prio is Card*2 % instantiate skeleton earlier, relevant for propagation in test 33 | |
| 228 | ; Prio is Card*100), | |
| 229 | get_wait_flag(Prio,allow_reuse(force_empty_and_set_skel(Set,Card)),WF,LWF2), | |
| 230 | % we allow reuse as instantiate_set does not create a choice point itself: it just instantiates the set skeleton | |
| 231 | % and we just delay this as it can be counter-productive (leading to multiple solutions in different order) | |
| 232 | % see tests 33, 34 where multiple calls to force_empty_and_set_skel are made | |
| 233 | instantiate_set(Set,Card,ElementsSoFar,LWF2,WF). | |
| 234 | force_empty_and_set_skel(_,_,_,_). % note hat verify_attributes will call update_card and check cardinality! | |
| 235 | ||
| 236 | ||
| 237 | % instantiate a variable | |
| 238 | :- block instantiate_set(-,?,?,-,?). | |
| 239 | instantiate_set(Var,Card,ElementsSoFar,LWF2,WF) :- %print(instantiate_set(Var,Card,ElementsSoFar,LWF2)),nl, | |
| 240 | var(Var),!, | |
| 241 | (Card>1 | |
| 242 | -> instantiate_var_set(Var,Card,ElementsSoFar,LWF2,WF) | |
| 243 | ; Var = [H], | |
| 244 | not_element_of_wf(H,ElementsSoFar,WF)). %, print(instantiated_set(Var,Card,LWF2)),nl. | |
| 245 | instantiate_set([H|T],Card,ElementsSoFar,LWF2,WF) :- !, | |
| 246 | (Card>1 | |
| 247 | -> check_and_add_new_element(H,ElementsSoFar,ElementsSoFar2,WF), | |
| 248 | C1 is Card-1, | |
| 249 | instantiate_set(T,C1,ElementsSoFar2,LWF2,WF) | |
| 250 | ; empty_set_wf(T,WF)). | |
| 251 | instantiate_set(_,_,_,_,_WF). % TO DO: what if we have an open list skeleton? should we instantiate end? | |
| 252 | % note hat verify_attributes will call update_card and check cardinality! | |
| 253 | ||
| 254 | instantiate_var_set(VarSet,Card,ElementsSoFar,_LWF2,WF) :- | |
| 255 | kernel_objects:unbound_variable_for_card(VarSet), | |
| 256 | !, | |
| 257 | kernel_objects:setup_ordered_list_skeleton(Card,Skel,closed,WF), | |
| 258 | disjoint_sets(ElementsSoFar,Skel,WF), | |
| 259 | %print(skel(Card,Skel)),nl, | |
| 260 | VarSet = Skel. % bypass equal_object: assign variable in one-go | |
| 261 | instantiate_var_set(VarSet,Card,ElementsSoFar,LWF2,WF) :- | |
| 262 | C1 is Card-1, VarSet = [H|TVar], | |
| 263 | check_and_add_new_element(H,ElementsSoFar,ElementsSoFar2,WF), | |
| 264 | instantiate_set(TVar,C1,ElementsSoFar2,LWF2,WF). | |
| 265 | ||
| 266 | :- public safe_explicit_set_cardinality_wf/3. | |
| 267 | safe_explicit_set_cardinality_wf(CS,Card,WF) :- | |
| 268 | explicit_set_cardinality_wf(CS,CSCard,WF), % TO DO: use finite version which itself raises WD error when inf and use clpfd addition | |
| 269 | add_cs_card(CS,CSCard,0,inf,[contains],Card,WF). | |
| 270 | ||
| 271 | ||
| 272 | add_cs_card(_CS,CSCard,Acc,_MaxCard,_Info,Res,_WF) :- number(CSCard),!, | |
| 273 | Res is Acc+CSCard. | |
| 274 | add_cs_card(CS,CSCard,Acc,MaxCard,Info,Res,_WF) :- | |
| 275 | (clpfd_max_bounded(CSCard) | |
| 276 | ; var(CSCard), | |
| 277 | (nonmember(contains_wd_condition,Info) | |
| 278 | ; is_interval_closure(CS,_,_) % checks if the closure is guaranteed to be finite; relevant for test 1625 | |
| 279 | )), | |
| 280 | !, | |
| 281 | % no risk of CLPFD error with inf -> we can unify straightaway; better for propagation | |
| 282 | % We could also look at CS itself: e.g., interval closure: no risk of infinite card | |
| 283 | Res #= Acc+CSCard, | |
| 284 | restrict_card(Res,MaxCard). | |
| 285 | add_cs_card(CS,CSCard,_Acc,_MaxCard,Info,_Res,WF) :- CSCard == inf,!, | |
| 286 | add_wd_error_span('card applied to infinite set, cardinality not representable as a natural number: ',CS,Info,WF). | |
| 287 | add_cs_card(CS,CSCard,_Acc,_MaxCard,Info,_Res,WF) :- CSCard == inf_overflow,!, | |
| 288 | add_abort_error_span(card_overflow_error, | |
| 289 | 'card applied to very large set, cardinality not representable in ProB: ',CS,Info,WF). | |
| 290 | add_cs_card(CS,CSCard,Acc,MaxCard,Info,Res,WF) :- | |
| 291 | Res #>= Acc, | |
| 292 | restrict_card(Res,MaxCard), | |
| 293 | block_add_cs_card(CS,CSCard,Acc,Info,Res,WF). | |
| 294 | ||
| 295 | :- block block_add_cs_card(?,-,?,?,?,?). | |
| 296 | block_add_cs_card(_CS,CSCard,Acc,_,Res,_WF) :- number(CSCard),!,Res #= Acc+CSCard. | |
| 297 | block_add_cs_card(CS,CSCard,_Acc,_,_Res,WF) :- CSCard == inf, !, | |
| 298 | add_wd_error('card applied to infinite set: ',CS,WF). | |
| 299 | block_add_cs_card(CS,_,_Acc,Info,_Res,WF) :- % inf_overflow | |
| 300 | add_abort_error_span(card_overflow_error, | |
| 301 | 'card applied to very large set, cardinality not representable in ProB: ',CS,Info,WF). | |
| 302 | ||
| 303 | :- use_module(tools_platform, [max_tagged_integer/1]). | |
| 304 | % restrict Card to be smaller or equal to MaxCard | |
| 305 | restrict_card(Card,MaxCard) :- var(Card), | |
| 306 | number(MaxCard), | |
| 307 | max_tagged_integer(Max), MaxCard =< Max, % check if CLP(FD) overflow would occur when posting constraint | |
| 308 | !, | |
| 309 | Card #=< MaxCard. | |
| 310 | restrict_card(_,_). | |
| 311 | ||
| 312 | ||
| 313 | ||
| 314 | /* | |
| 315 | | ?- finite_cardinality_as_int_wf(Var,C,WF), Var=[a,b,c|T], finite_cardinality_as_int_wf(T,CT,WF), C=int(3). | |
| 316 | update([b,c|_1241],_1241,3) | |
| 317 | emp([a,b,c|_3493],_2855) | |
| 318 | emp(0,_3493) | |
| 319 | Var = [a,b,c], | |
| 320 | C = 3, | |
| 321 | T = [], | |
| 322 | CT = 0 ? | |
| 323 | yes | |
| 324 | ||
| 325 | ||
| 326 | */ | |
| 327 | ||
| 328 | ||
| 329 | :- use_module(clpfd_interface,[clpfd_domain/3]). | |
| 330 | ||
| 331 | % obtain the CLP(FD) variable bounds for a cardinality variable | |
| 332 | clpfd_card_domain_for_var(Var,MinCard,MaxCard) :- | |
| 333 | var(Var), | |
| 334 | (get_kernel_card_attr(Var,StoredCard,_) | |
| 335 | -> clpfd_domain(StoredCard,MinCard,MaxCard) %, print(clpfd_domain(Var,MinCard,MaxCard)),nl | |
| 336 | ; (MinCard,MaxCard) = (0,sup) | |
| 337 | ). | |
| 338 | ||
| 339 | % ----------------- | |
| 340 | ||
| 341 | % to do: implement and ensure that it also works for infinite sets | |
| 342 | %not_empty_set_wf(X,WF) :- var(X), !, | |
| 343 | % card_not_empty_set(X,WF). | |
| 344 | %not_empty_set_wf([_|_]). | |
| 345 | ||
| 346 | :- use_module(library(clpfd),[fd_min/2]). | |
| 347 | % check if a variable is annotated with cardinality which implies that the set is not empty | |
| 348 | clpfd_card_is_gt0_for_var(Var) :- var(Var), | |
| 349 | get_kernel_card_attr(Var,StoredCard,_), | |
| 350 | fd_min(StoredCard,Low), | |
| 351 | number(Low), Low>0. | |
| 352 | ||
| 353 | card_not_empty_set(Set,WF) :- var(Set), | |
| 354 | card_for_var(Set,Card,[],WF), | |
| 355 | Card #>0. | |
| 356 | ||
| 357 | reify_empty_set_test(Set,PredRes,WF) :- var(Set), | |
| 358 | card_for_var(Set,Card,[],WF), | |
| 359 | (Card #> 0) #<=> R01, | |
| 360 | b_interpreter_check:prop_pred_01(PredRes,R01). | |
| 361 | ||
| 362 | % ---------------------- | |
| 363 |