1% BEGIN LICENSE BLOCK 2% Version: CMPL 1.1 3% 4% The contents of this file are subject to the Cisco-style Mozilla Public 5% License Version 1.1 (the "License"); you may not use this file except 6% in compliance with the License. You may obtain a copy of the License 7% at www.eclipse-clp.org/license. 8% 9% Software distributed under the License is distributed on an "AS IS" 10% basis, WITHOUT WARRANTY OF ANY KIND, either express or implied. See 11% the License for the specific language governing rights and limitations 12% under the License. 13% 14% The Original Code is The Cardinal Constraint Solver for ECLiPSe. 15% The Initial Developer of the Original Code is Francisco M.C.A. Azevedo. 16% Portions created by the Initial Developer are Copyright (C) 2004. 17% All Rights Reserved. 18% 19% Contributor(s): Francisco M. C. A. Azevedo <fa@di.fct.unl.pt>. 20% 21% Alternatively, the contents of this file may be used under the terms of 22% either of the GNU General Public License Version 2 or later (the "GPL"), 23% or the GNU Lesser General Public License Version 2.1 or later (the "LGPL"), 24% in which case the provisions of the GPL or the LGPL are applicable instead 25% of those above. If you wish to allow use of your version of this file only 26% under the terms of either the GPL or the LGPL, and not to allow others to 27% use your version of this file under the terms of the MPL, indicate your 28% decision by deleting the provisions above and replace them with the notice 29% and other provisions required by the GPL or the LGPL. If you do not delete 30% the provisions above, a recipient may use your version of this file under 31% the terms of any one of the MPL, the GPL or the LGPL. 32% END LICENSE BLOCK 33 34%icompile(cardinal), ecis_to_htmls('.','.','') 35 36:-comment(desc, html("Cardinal is a sets constraints library with especial inferences 37 on sets cardinality and other optional set functions (minimum and maximum for 38 sets of integers, and union for sets of sets.) 39 <P> 40 A set is naturally used to collect distinct elements sharing some property. 41 Combinatorial search problems over these data structures can thus be naturally 42 modelled by high level languages with set abstraction facilities, and efficiently 43 solved if constraint reasoning prunes search space when the sets are not fully 44 known a priori (i.e. they are variables ranging over a set domain). 45 <P> 46 Many complex relations between sets can be expressed with constraints such as set 47 inclusion, disjointness and equality over set expressions that may include such 48 operators as intersection, union or difference of sets. Also, as it is often the 49 case, one is not interested simply on these relations but on some attribute or 50 function of one or more sets (e.g. the cardinality of a set). For instance, the 51 goal of many problems is to maximise or minimise the cardinality of a set. Even 52 for satisfaction problems, some sets, although still variables, may be constrained 53 to a fixed cardinality or a stricter cardinality domain than just the one inferred 54 by the domain of a set variable (for instance, the cardinality of a set may have 55 to be restricted to be an even number). 56 <P> 57 Cardinal represents set variables by set intervals with a lower and an upper bound 58 considering set inclusion as a partial ordering. Consistency techniques are then 59 applied to set constraints by interval reasoning. A set domain variable S may be 60 specified by an interval [A,B] where A and B are known sets ordered by set inclusion, 61 representing the greatest lower bound and the lowest upper bound of S, respectively. 62 <P> 63 The cardinality of a set S, given as a finite domain variable C (#S=C), is not a 64 bijective function since two distinct sets may have the same cardinality. Still, 65 it can be constrained by the cardinalities of the set bounds. 66 <P> 67 A simple inference that can be done using cardinality information is to instantiate 68 the set to one of the set bounds, when it is known that the set cardinality must be 69 equal to the cardinality of that bound. But Cardinal does much more than that. 70 For instance, consider two set variables 71 S1,S2, that can assume either set value {} (empty set) or {a,b}. Their set domain 72 is thus [{},{a,b}] with cardinality 0 or 2. The intersection of S1 and S2 also 73 yelds set domain [{},{a,b}]. But we need a special inference to conclude that the 74 intersection cardinality is also either 0 or 2 (it can not be 1). Set solvers 75 other than Cardinal do not make such inferences. 76 <P> 77 Inferences using cardinalities can be very useful to deduce more rapidly the 78 non-satisfiability of a set of constraints, thus improving efficiency of 79 combinatorial search problem solving. As another simple example, if Z is known to be 80 the set difference between Y and X, both contained in set {a,b,c,d}, and it is known 81 that X has exactly 2 elements, it should be inferred that the cardinality of Z can 82 never exceed 2 elements (i.e. from X,Y in {a,b,c,d}, #X=2, Z=Y\\X it should be 83 inferred that #Z =< 2). A failure could thus be immediately detected upon the 84 posting of a constraint such as #Z=3. 85 <P> 86 Inference capabilities such as these are particularly important when solving set 87 problems where cardinality plays a special role. Cardinal thus fully uses 88 constraint propagation on sets cardinality. 89 <P> 90 91<B>Intervals and Lattices</B> 92 <P> 93 Set intervals define a lattice of sets. The set inclusion relation between two 94 sets defines a partial order on P(U), the powerset over a certain universe U, 95 the set of all subsets of U. 96 <P> 97 Due to the transitivity rule, the top set, U, includes all sets of P(U); 98 while the bottom set, {}, is included in all sets of P(U). Consequently, 99 sets U and {} constitute an upper bound and a lower bound of P(U), respectively. 100 In addition, they are the least upper bound (lub) or join, and the greatest lower 101 bound (glb) or meet of P(U), since there is no other upper bound contained in 102 (�less� than) U nor other lower bound containing (�greater� than) the empty set {}. 103 <P> 104 Let us now consider for U={a,b,c,d}, the sub-lattice connecting {a,b,d} and {b} 105 (thus also including sets {a,b} and {b,d}). Sets {} and {a,b,c,d} are still a 106 lower and an upper bound, but this time the glb is {b} and the lub is {a,b,d}. 107 <P> 108 The two bounds (glb and lub) define a set interval (e.g. [{b},{a,b,d}]) and may 109 form the domain of a set variable S, meaning that set S is one of those defined 110 by its interval (lattice); all other sets outside this domain are excluded from 111 the solution. Thus, b is definitely an element of S, while a and d are the only 112 other possible elements. 113 <P> 114 Set interval reasoning allows us to apply consistency techniques such as Bounded 115 Arc Consistency, due to the monotonic property of set inclusion. 116 <P> 117 Any set variable must then have a domain consisting of a set interval. In addition, 118 this interval should be kept as small as possible, in order to discard all sets 119 that are known not to belong to the solution, while not loosing any of the still 120 possible values (sets). The smallest such domain is the one with equal glb and lub, 121 i.e. a domain of the form [B,B], corresponding to a constant set B. For a set 122 variable that can assume any set value from a collection of known sets, such as 123 {{a,b},{a,c},{d}}, the corresponding interval is the convex closure of such 124 collection (which in this case is the set interval [{},{a,b,c,d}]). In general, 125 for n possible arbitrary sets S1...Sn, the corresponding set variable X has an 126 interval domain [glb, lub] where glb is the intersection of all S1...Sn, and lub 127 is their union. 128 <P> 129<B>Implementation Notes</B> 130 <P> 131 In Cardinal, all sets are represented as sorted lists, which eases working with 132 sets and lists interchangeably. 133 <P> 134 Set variable bounds are represented by its glb and its lub\\glb, the set of 135 additional possible elements, which we refer to as poss. 136 <P> 137 Cardinal implements a number of set constraints such as inclusion, equality, 138 inequality, membership, disjointness, and even complement, together with set 139 operations (union, intersection and difference), as built-in. 140 <P> 141 As mentioned, Cardinal also allows the definition and use of optional set functions 142 (other than cardinality): minimum and maximum, for sets of integers, and union, 143 for sets of sets. Refer to the available predicates for details. 144")). 145 146 147 148 149 150:-comment(cardinality/2, [ 151 amode: cardinality(?,?), 152 args: ["SetVariable": "A Set (variable or ground).", 153 "Cardinality": "An integer or an FD variable."], 154 summary: "Cardinality of a set", 155 desc: html("Cardinality is the cardinality of SetVariable. If Cardinality is given 156 (as an integer or FD variable), then SetVariable is constrained to have such cardinality. 157 If Cardinality is a free variable, then it is unified with the set's cardinality as 158 an FD variable or an integer (if it is already known)."), 159 resat: "No.", 160 fail_if: "Fails if Cardinality can not be the cardinality of SetVariable.", 161 eg:" 162?- S `::[]..[a,b], cardinality(S,C). 163?- S `::[]..[a,b], cardinality(S,1). 164?- S `::[]+[a,b]:1, cardinality(S,C). 165C = 1 166 167?- cardinality([a,b],C). 168C = 2 169 170?- S `::[c]+[a,b]:[1,3], C #> 1, cardinality(S,C). 171S = [a,b,c] 172C = 3", 173 see_also:[(#)/2] 174 ]). 175 176 177:-comment((#)/2, [ 178 amode: #(?,?), 179 args: ["SetExpression": "A Set expression.", 180 "Cardinality": "An integer or an FD variable."], 181 summary: "Cardinality of a set expression", 182 desc: html("Cardinality is the cardinality of SetExpression, a set term possibly 183 including set operators `/\\, `\\/ and `\\ (or \\). <P> 184 SetExpression is first evaluated into a ground set or a set variable and then 185 its Cardinality is applied as in cardinality/2."), 186 resat: "No.", 187 fail_if: "Fails if Cardinality can not be the cardinality of SetExpression.", 188 eg:" 189?- S `::[]..[a,b], #(S,C). 190?- S `::[]..[a,b], #(S `/\\ [b,c],1). 191?- S `::[]..[a,b], #([b,c] `\\/ S `\\ [a,z] `/\\ [g], C). 192C = 2, 193?- S `::[]..[a,b], #(([b,c] `\\/ S `\\ [a,z]) `/\\ [g], C). 194C = 0 195?- S1 `::[]..[a,b], S2 `::[]..[b,c,d], #(S1 `/\\ S2, 2). 196no 197", 198 see_also:[cardinality/2,(`=)/2] 199 ]). 200 201 202 203:-comment(glb/2, [ 204 amode: glb(?,-), 205 args: ["SetVariable": "A set variable.", 206 "Glb": "A set."], 207 summary: "Obtaining a set's glb", 208 desc: html("Glb is unified with the (greatest) lower bound of SetVariable."), 209 resat: "No.", 210 fail_if: "Fails if Glb can not be unified with the current glb of SetVariable.", 211 eg:" 212?- S `::[c]+[a,b], glb(S,G). 213G = [c] 214", 215 see_also:[glb_poss/3,domain/2,domain/3,lub/2,lub/4,poss/2] 216 ]). 217 218 219:-comment(poss/2, [ 220 amode: poss(?,-), 221 args: ["SetVariable": "A set variable.", 222 "Poss": "A set."], 223 summary: "Obtaining the still possible elements of a set (lub\\glb)", 224 desc: html("Poss is unified with the set of still possible elements of SetVariable 225 (i.e. its lub\\glb).<P> 226 If SetVariable is a set of sets and a union function attribute has been set, 227 then each element of Poss comes annotated with its respective length."), 228 resat: "No.", 229 fail_if: "Fails if Poss can not be unified with the current poss (lub\\glb) of SetVariable.", 230 eg:" 231?- S `::[c]+[a,b], poss(S,P). 232P = [a,b] 233 234?- S `::[[c]]+[[a,b]], poss(S,P). 235P = [[a,b]] 236 237?- set(S, [],[[a,b],[b,c],[a,c],[b]],[union:[a,b,c]]), poss(S,P). 238P = [[a, b] : 2, [a, c] : 2, [b] : 1, [b, c] : 2] 239", 240 see_also:[glb/2,glb_poss/3,domain/2,domain/3,lub/2,lub/4] 241 ]). 242 243 244:-comment(glb_poss/3, [ 245 amode: glb_poss(?,-,-), 246 args: ["SetVariable": "A set variable.", 247 "Glb": "A set.", 248 "Poss": "A set."], 249 summary: "Obtaining both the glb and the still possible elements of a set", 250 desc: html("Glb is unified with the (greatest) lower bound of SetVariable.<P> 251 Poss is unified with the set of still possible elements of SetVariable 252 (i.e. its lub\\glb).<P> 253 If SetVariable is a set of sets and a union function attribute has been set, 254 then each element of Poss comes annotated with its respective length."), 255 resat: "No.", 256 fail_if: "Fails if Glb can not be unified with the current glb of SetVariable or 257 if Poss can not be unified with the current poss (lub\\glb) of SetVariable.", 258 eg:" 259?- S `::[c]+[a,b], glb_poss(S,G,P). 260G = [c] 261P = [a,b] 262 263?- set(S, [],[[a,b],[b,c],[a,c],[b]],[union:[a,b,c]]), glb_poss(S,G,P). 264G = [] 265P = [[a, b] : 2, [a, c] : 2, [b] : 1, [b, c] : 2] 266", 267 see_also:[glb/2,poss/2,domain/2,domain/3,lub/2,lub/4] 268 ]). 269 270 271:-comment(domain/2, [ 272 amode: domain(?,-), 273 args: ["SetVariable": "A set variable.", 274 "Domain": "A list (pair) with glb and poss."], 275 summary: "Accessing the domain of a set", 276 desc: html("Domain is unified with the domain of SetVariable in the form [Glb:NIn,Poss:NMax], 277 where Glb is the (greatest) lower bound of SetVariable, and NIn its length, 278 Poss is the set of still possible elements of SetVariable (i.e. its lub\\glb), 279 and NMax is the lub's cardinality (i.e. NIn + #(Poss)).<P> 280 If SetVariable is a set of sets and a union function attribute has been set, 281 then each element of Poss comes annotated with its respective length."), 282 resat: "No.", 283 fail_if: "Fails if Domain can not be unified with the current domain of SetVariable.", 284 eg:" 285?- S `::[c]+[a,b], domain(S,D). 286D = [[c]:1, [a,b]:3] 287 288?- set(S, [],[[a,b],[b,c],[a,c],[b]],[union:[a,b,c]]), domain(S,D). 289D = [[]:0, [[a,b]:2, [a,c]:2, [b]:1, [b,c]:2]:4] 290", 291 see_also:[domain/3,glb/2,poss/2,glb_poss/3,lub/2,lub/4] 292 ]). 293 294 295:-comment(domain/3, [ 296 amode: domain(?,?,?), 297 args: ["SetVariable": "A set variable.", 298 "Cardinality": "An FD variable", 299 "Domain": "A list (pair) with glb and poss."], 300 summary: "Accessing the domain of a set", 301 desc: html("Domain is unified with the domain of SetVariable (which has cardinality 302 Cardinality) in the form [Glb:NIn,Poss:NMax], 303 where Glb is the (greatest) lower bound of SetVariable, and NIn its length, 304 Poss is the set of still possible elements of SetVariable (i.e. its lub\\glb), 305 and NMax is the lub's cardinality (i.e. NIn + #(Poss)). 306 <P> 307 If SetVariable is a set of sets and a union function attribute has been set, 308 then each element of Poss comes annotated with its respective length. 309 <P> 310 Use domain/3 instead of domain/2 whenever Cardinality variable is available, 311 for efficiency reasons, since in the case of SetVariable being already 312 ground, it is not neccessary to recalculate its length (to retrieve 313 [Setvariable:Cardinality,[]:Cardinality]. This is due to the loss of 314 attributes of variables when these become instantiated. 315 <P> 316 Cardinality should be input to domain/3. Do not use this predicate to 317 retrieve the cardinality of a set, for it will only work when set is ground."), 318 resat: "No.", 319 fail_if: "Fails if Domain can not be unified with the current domain of SetVariable.", 320 eg:" 321?- S `::[c]+[a,b]:C, domain(S,C,D). 322D = [[c]:1, [a,b]:3] 323 324?- S `::[c]+[a,b]:C, S=[a,c], domain(S,C,D). 325D = [[a,c]:2, []:2] 326 327?- set(S, [],[[a,b],[b,c],[a,c],[b]],[union:[a,b,c],cardinality:C]), domain(S,C,D). 328D = [[]:0, [[a,b]:2, [a,c]:2, [b]:1, [b,c]:2]:4] 329", 330 see_also:[domain/2,glb/2,poss/2,glb_poss/3,lub/2,lub/4,cardinality/2,(#)/2] 331 ]). 332 333 334:-comment(lub/2, [ 335 amode: lub(?,-), 336 args: ["SetVariable": "A set variable.", 337 "Lub": "A set."], 338 summary: "Obtaining a set's lub", 339 desc: html("Lub is unified with the (least) upper bound of SetVariable."), 340 resat: "No.", 341 fail_if: "Fails if Lub can not be unified with the current lub of SetVariable.", 342 eg:" 343?- S `::[c]+[a,b], lub(S,L). 344L = [a,b,c] 345", 346 see_also:[lub/4,glb/2,poss/2,glb_poss/3,domain/2,domain/3] 347 ]). 348 349 350:-comment(lub/4, [ 351 amode: lub(?,-,-,-), 352 args: ["SetVariable": "A set variable.", 353 "Glb": "A set.", 354 "Poss": "A set.", 355 "Lub": "A set."], 356 summary: "Obtaining a set's lub, together with its glb and poss (lub\\glb)", 357 desc: html("Lub is unified with the (least) upper bound of SetVariable.<P> 358 Glb is unified with the (greatest) lower bound of SetVariable.<P> 359 Poss is unified with the set of still possible elements of SetVariable 360 (i.e. its lub\\glb).<P> 361 If SetVariable is a set of sets and a union function attribute has been set, 362 then each element of Poss comes annotated with its respective length."), 363 resat: "No.", 364 fail_if: "Fails if Lub can not be unified with the current lub of SetVariable or 365 if Glb can not be unified with the current glb of SetVariable or 366 if Poss can not be unified with the current poss (lub\\glb) of SetVariable.", 367 eg:" 368?- S `::[c]+[a,b], lub(S,G,P,L). 369G = [c] 370P = [a,b] 371L = [a,b,c] 372 373?- set(S, [],[[a,b],[b,c],[a,c],[b]],[union:[a,b,c]]), lub(S,G,P,L). 374G = [] 375P = [[a, b] : 2, [a, c] : 2, [b] : 1, [b, c] : 2] 376L = [[a, b], [a, c], [b], [b, c]] 377", 378 see_also:[lub/2,glb_poss/3,glb/2,poss/2,domain/2,domain/3] 379 ]). 380 381 382:-comment(maximum/2, [ 383 amode: maximum(?,?), 384 args: ["SetVariable": "A Set (variable or ground) of integers.", 385 "Max": "An integer or an FD variable."], 386 summary: "Maximum of a set of integers", 387 desc: html("Max is the maximum (i.e. the highest element) of SetVariable.<P> 388 If Max is given (as an integer or FD variable) then SetVariable is 389 constrained to have such maximum. 390 If Max is a free variable, then it is unified with the set's maximum as 391 an FD variable or an integer (if it is already known).<P> 392 maximum/2 can thus be used either to declare (or constrain) a maximum 393 function or to retrieve it."), 394 resat: "No.", 395 fail_if: "Fails if Max can not be the maximum of SetVariable.", 396 eg:" 397?- S`::[]..[1,2], maximum(S,M). 398?- set(S,[],[1,2],[maximum:2], maximum(S,M). 399M = 2 400 401?- S`::[]+[1,2], maximum(S,1). 402S = [1] 403 404?- set(S,[],[1,2],[maximum:1], maximum(S,M). 405S = [1] 406M = 1", 407 see_also:[minimum/2,set/4,sets/4,cardinality/2] 408 ]). 409 410 411:-comment(minimum/2, [ 412 amode: minimum(?,?), 413 args: ["SetVariable": "A Set (variable or ground) of integers.", 414 "Min": "An integer or an FD variable."], 415 summary: "Minimum of a set of integers", 416 desc: html("Min is the minimum (i.e. the lowest element) of SetVariable.<P> 417 If Min is given (as an integer or FD variable) then SetVariable is 418 constrained to have such minimum. 419 If Min is a free variable, then it is unified with the set's minimum as 420 an FD variable or an integer (if it is already known).<P> 421 minimum/2 can thus be used either to declare (or constrain) a minimum 422 function or to retrieve it."), 423 resat: "No.", 424 fail_if: "Fails if Min can not be the minimum of SetVariable.", 425 eg:" 426?- S`::[]..[1,2], minimum(S,M). 427?- set(S,[],[1,2],[minimum:1], minimum(S,M). 428M = 1 429 430?- S`::[]+[1,2], minimum(S,2). 431S = [2] 432 433?- set(S,[],[1,2],[minimum:2], minimum(S,M). 434S = [2] 435M = 2", 436 see_also:[maximum/2,set/4,sets/4,cardinality/2] 437 ]). 438 439 440:-comment(union_var/2, [ 441 amode: union_var(?,?), 442 args: ["SetVariable": "A Set (variable or ground) of sets.", 443 "UnionVar": "A Set (variable or ground)."], 444 summary: "Union of a set of sets", 445 desc: html("UnionVar is the union of sets in SetVariable. If UnionVar is given 446 (as a ground set or a set variable), then SetVariable is constrained to have such union. 447 If UnionVar is a free variable, then it is unified with the set's union as 448 a set variable or a ground set (if it is already known).<P> 449 union_var/2 can thus be used either to declare (or constrain) a union 450 function or to retrieve it."), 451 resat: "No.", 452 fail_if: "Fails if UnionVar can not be the union of SetVariable.", 453 eg:" 454?- S `::[]..[[a],[b]], union_var(S,U). 455?- S `::[]..[[a],[b],[a,b]], union_var(S,[a,b]). 456?- union_var([[a,b],[b,c]], U). 457U = [a,b,c]", 458 see_also:[set/4,sets/4,cardinality/2] 459 ]). 460 461 462/* 463:-comment(union_att/2, [ 464 amode: union_att(?,-), 465 args: ["SetVariable": "A Set (variable or ground) of sets.", 466 "UnionAtt": "A Set in the form [UnionVar,GlbU+PossU,Singles,Lengths]."], 467 summary: "Union Attribute of a set of sets", 468 desc: html("UnionAtt is the union attribute of SetVariable, concerning its union function, 469 a list with the following data:<P> 470 UnionVar: union of sets in SetVariable<P> 471 GlbU: set union of SetVariable's glb<P> 472 PossU: set of possible union elements with counters (X:N), i.e. an ordered 473 list of all elements in the sets of SetVariable's poss (lub\\glb) 474 with the number of occurrences attached<P> 475 Singles: elements where N=1 in PossU<P>"), 476 resat: "No.", 477 fail_if: "Fails if SetVariable is not a set of sets or if its union attributte 478 does not unify with UnionAtt.", 479 eg:" 480?- S `::[]..[[a],[b]], union_att(S,UAtt). 481?- union_att([[a],[b]], UAtt). 482UAtt = [[a,b],[a,b]+[],[],[]] 483 484?- S `::[]..[[a],[b],[a,b],[c]], union_att(S,[_,GlbU+PossU,Singles,Lengths]). 485Glb = [] 486PossU = [a:2,b:2,c:1] 487Singles = [c] 488Lengths = [2:1, 1:3]", 489 see_also:[union_var/2,union_att/3,set/4,sets/4,cardinality/2] 490 ]). 491 492%:-comment(union_att/3, [... 493 494*/ 495 496 497 498 499:-comment((`::)/2, [ 500% amode: `::(?,+), 501% amode: (? `:: +), 502 template: "?SetVariable `:: ?Domain", 503 args: ["SetVariable": "A variable.", 504 "Domain": "A set domain with optional cardinality declaration."], 505 summary: "Set variable declaration", 506 desc: html("Declare or constrain a set domain variable to have Domain as domain.<P> 507 Domain may assume 3 forms: Glb..Lub, Glb+Poss or Glb+Poss:Cardinality.<P> 508 Glb is a ground set denoting the SetVariable's glb. Lub is a ground set 509 denoting the SetVariable's lub. Poss is a ground set denoting the SetVariable's 510 poss (lub\\glb). Cardinality is the SetVariable's cardinality, which may be 511 an integer, an FD variable, or an integer domain (list or range)."), 512 resat: "No.", 513 fail_if: "Fails if SetVariable can not be constrained accordingly.", 514 eg:" 515?- S `:: []..[a,b]. 516?- S `:: []+[a,b]. 517?- S `:: []+[a,b]:1. 518?- S `:: [x]+[a,b]:C. 519?- S `:: []+[a,b]:[0,2]. 520?- S `:: [c]+[a,b,d,e,f,g,h,i,j,k]:[2,4..7]. 521", 522 see_also:[set/4,sets/4,cardinality/2,union_var/2,minimum/2,maximum/2,set_labeling/1] 523 ]). 524 525 526 527:-comment(set/4, [ 528 amode: set(?,++,++,+), 529 args: ["SetVariable": "A variable.", 530 "Glb": "A ground set.", 531 "Poss": "A ground set.", 532 "Functions": "A list."], 533 summary: "Set variable declaration with optional functions", 534 desc: html("Declare or constrain a set domain variable to have Glb as assured 535 elements and Poss as the possible additional elements.<P> 536 Functions is a list of functions over SetVariable in the form 537 FunctionName:FunctionValue, where FunctionName can be 'cardinality', 538 'minimum', 'maximum' or 'union': 539<PRE> 540 cardinality: FunctionValue can be an integer, an FD variable or an integer domain (list or range) 541 union: (SetVariable must be a set of sets.) FunctionValue can be a set, a set variable 542 or a set domain in the form GlbUnion+PossUnion, representing the glb and poss of 543 the union of SetVariable 544 minimum and maximum: (SetVariable must be a nonempty set of integers.) 545 FunctionValue can be an integer, an FD variable or an integer domain 546</PRE> 547 Cardinal inferences over SetVariable and its union, minimum and maximum 548 functions will be performed only if these functions are explicitly 549 declared, whereas the cardinality function and respective inferences 550 will always be present even if this (cardinality) function is not 551 explicitly declared. Note that a simple function declaration such as 552 minimum:_ is sufficient to make it 'active'."), 553 resat: "No.", 554 fail_if: "Fails if SetVariable can not be constrained accordingly.", 555 eg:" 556?- set(S,[],[a,b],[]). 557?- set(S,[],[a,b],[cardinality:1]). 558?- set(S,[],[a,b],[cardinality:C]). 559?- set(S,[],[a,b],[cardinality:[0,2]]). 560?- set(S,[c],[a,b,d,e,f,g,h,i,j,k],[cardinality:[2,4..7]]). 561?- set(S,[],[1,3,4,5,7],[minimum:Min,maximum:Max]), fd:(Max #> Min+2). 562?- set(S, [], [[1,2,5],[2,4],[3,5],[1,3,4]], 563 [cardinality:2, union:[1,2,3,4,5]]). %set-covering 564?- set(S, [], [[1,2,5],[2,4],[3,5],[1,3,4]], [union:[1]+[2,4,5]]). 565", 566 see_also:[sets/4,(`::)/2,cardinality/2,union_var/2,minimum/2,maximum/2,set_labeling/1] 567 ]). 568 569 570:-comment(sets/4, [ 571 amode: sets(+,++,++,+), 572 args: ["SetVariables": "A list of variables.", 573 "Glb": "A ground set.", 574 "Poss": "A ground set.", 575 "Functions": "A list."], 576 summary: "Set variables declaration with optional functions", 577 desc: html("Declare or constrain set domain variables to have Glb as assured 578 elements and Poss as the possible additional elements.<P> 579 Functions is a list of functions over each SetVariable in SetVariables in the form 580 FunctionName:FunctionValue, where FunctionName can be 'cardinality', 581 'minimum', 'maximum' or 'union':<P> 582<PRE> 583 cardinality: FunctionValue can be an integer, an FD variable or an integer domain (list or range) 584 union: (SetVariable must be a set of sets.) FunctionValue can be a set, a set variable 585 or a set domain in the form GlbUnion+PossUnion, representing the glb and poss of 586 the union of SetVariable 587 minimum and maximum: (SetVariable must be a nonempty set of integers.) 588 FunctionValue can be an integer, an FD variable or an integer domain 589</PRE> 590 Cardinal inferences over SetVariable and its union, minimum and maximum 591 functions will be performed only if these functions are explicitly 592 declared, whereas the cardinality function and respective inferences 593 will always be present even if this (cardinality) function is not 594 explicitly declared. Note that a simple function declaration such as 595 minimum:_ is sufficient to make it 'active'.<P> 596 If a FunctionValue is given as a variable or as a fixed (integer or set) 597 value, then it will be the same for all of SetVariables. If it is given 598 as a domain, then function values for SetVariables may be different 599 (a different domain variable is created for each SetVariable)."), 600 resat: "No.", 601 fail_if: "Fails if SetVariables can not be constrained accordingly.", 602 eg:" 603?- sets([S],[],[a,b],[]). 604?- sets([S,T],[],[a,b],[cardinality:1]). 605?- sets([X,Y,Z],[],[a,b],[cardinality:C]). 606?- sets([X,Y,Z],[],[a,b],[cardinality:[0,2]]). 607?- sets([X,Y,Z],[c],[a,b,d,e,f,g,h,i,j,k],[cardinality:[2,4..7]]). 608?- sets([X,Y,Z],[],[1,3,4,5,7],[minimum:Min,maximum:1..9]), fd:(Max #> Min+2). 609?- sets([X,Y,Z], [], [[1,2,5],[2,4],[3,5],[1,3,4]], [union:[1]+[2,4,5]]). 610", 611 see_also:[set/4,(`::)/2,cardinality/2,union_var/2,minimum/2,maximum/2,set_labeling/1] 612 ]). 613 614 615 616:-comment(refine/2, [ 617 amode: refine(++,?), 618 args: ["UpDown": "Atom ('up' or 'down').", 619 "SetVar": "A set variable."], 620 summary: "Refine a set variable's domain", 621 desc: html("Pick the first element of SetVar's poss (lub\\glb) and try to include it 622 in its glb, or to definitely exclude it from the domain.<P> 623 If heuristic UpDown is 'up' then inclusion is tried first; otherwise (down) 624 exclusion is tried first."), 625 resat: "Yes.", 626 fail_if: "Fails if Var can not be refined (it is either ground or both the inclusion 627 and exclusion of the first element of its poss leads to a failure due to 628 unsatisfied constraints).", 629 eg:" 630?- S `:: [a]+[b,c], refine(up,S), glb_poss(S,G,P). 631G = [a,b], P = [c] ; 632G = [a], P = [c] ; 633no 634 635?- S `:: [a]+[b,c], refine(down,S), glb_poss(S,G,P). 636G = [a], P = [c] ; 637G = [a,b], P = [c] ; 638no 639", 640 see_also:[set_labeling/2,set_labeling/1] 641 ]). 642 643 644:-comment(set_labeling/2, [ 645 amode: set_labeling(++,+), 646 args: ["UpDown": "Atom: 'up' or 'down'.", 647 "SetVars": "List of set variables."], 648 summary: "Label set variables", 649 desc: html("Instantiate all variables in SetVars from first to last, with 650 consecutive refinements of their domains until they are ground.<P> 651 If heuristic UpDown is 'up' then, for each set variable, for each element 652 in its poss (lub\\glb), inclusion is tried first; otherwise (down) 653 exclusion is tried first."), 654 resat: "Yes.", 655 fail_if: "Fails if SetVars can not be labeled (there is no solution to the CSP).", 656 eg:" 657?- S `:: [a] + [b, c], T `:: [1] + [2], set_labeling(up, [S, T]). 658S = [a, b, c], T = [1, 2] ; 659S = [a, b, c], T = [1] ; 660S = [a, b], T = [1, 2] ; 661S = [a, b], T = [1] ; 662S = [a, c], T = [1, 2] ; 663S = [a, c], T = [1] ; 664S = [a], T = [1, 2] ; 665S = [a], T = [1] ; 666no 667 668?- S `:: [a] + [b, c], T `:: [1] + [2], set_labeling(down, [S, T]). 669S = [a], T = [1] ; 670S = [a], T = [1, 2] ; 671S = [a, c], T = [1] ; 672S = [a, c], T = [1, 2] ; 673S = [a, b], T = [1] ; 674S = [a, b], T = [1, 2] ; 675S = [a, b, c], T = [1] ; 676S = [a, b, c], T = [1, 2] ; 677no 678", 679 see_also:[set_labeling/1,refine/2] 680 ]). 681 682 683:-comment(set_labeling/1, [ 684 amode: set_labeling(?), 685 args: ["SetVars": "A variable or a list of set variables."], 686 summary: "Label set variable(s)", 687 desc: html("Instantiate all variables in SetVars from first to last, with 688 consecutive refinements of their domains until they are ground.<P> 689 For each set variable, for each element in its poss (lub\\glb), inclusion 690 is tried first.<P> 691 SetVars can be a set variable instead of a list. Labeling a single set 692 variable S can thus be done both with set_labeling([S]) or with 693 set_labeling(S)."), 694 resat: "Yes.", 695 fail_if: "Fails if SetVars can not be labeled (there is no solution to the CSP).", 696 eg:" 697?- S `:: [a] + [b, c], T `:: [1] + [2], set_labeling([S, T]). 698S = [a, b, c], T = [1, 2] ; 699S = [a, b, c], T = [1] ; 700S = [a, b], T = [1, 2] ; 701S = [a, b], T = [1] ; 702S = [a, c], T = [1, 2] ; 703S = [a, c], T = [1] ; 704S = [a], T = [1, 2] ; 705S = [a], T = [1] ; 706no 707 708?- S `:: [a] + [b, c], T `:: [1] + [2], set_labeling(S). 709S = [a, b, c] ; 710S = [a, b] ; 711S = [a, c] ; 712S = [a] ; 713no 714 715", 716 see_also:[set_labeling/2,refine/2] 717 ]). 718 719 720 721:-comment(card_labeling/1, [ 722 amode: card_labeling(?), 723 args: ["SetVars": "A list of set variables."], 724 summary: "Label cardinality of set variables", 725 desc: html("Instantiate all cardinalities of variables in SetVars from first to 726 last, using indomain/1 predicate of fd library.<P> 727 card_labeling/1 is defined as: 728<PRE> 729 card_labeling([]). 730 card_labeling([H|T]):- 731 cardinality(H, C), 732 indomain(C), 733 card_labeling(T). 734</PRE> 735"), 736 resat: "Yes.", 737 fail_if: "Fails if cardinalities of SetVars can not be labeled (because constraint 738 propagation leads to a failure).", 739 eg:" 740?- S `:: [a]+[b,c]:CS, T `:: [1] + [2], card_labeling([S, T]). 741CS = 1, S = [a], T = [1] ; 742CS = 1, S = [a], T = [1, 2] ; 743CS = 2, T = [1] ; 744CS = 2, T = [1, 2] ; 745CS = 3, S = [a,b,c], T = [1] ; 746CS = 3, S = [a,b,c], T = [1, 2] ; 747no 748 749?- S `:: [a] + [b,c,d,e,f]:[2,3,6,9], card_labeling([S]), cardinality(S,C). 750C = 2 ; 751C = 3 ; 752C = 6, S = [a,b,c,d,e,f] ; 753no 754 755", 756 see_also:[set_labeling/2,refine/2,cardinality/2] 757 ]). 758 759 760 761:-comment((`@)/2, [ 762% amode: `@(?,?), 763% amode: (? `@ ?), 764 template: "?Element `@ ?SetVariable", 765 args: ["SetVariable": "A set variable.", 766 "Element": "A ground term or a variable."], 767 summary: "Set membership constraint", 768 desc: html("Constrain SetVariable to include Element.<P> 769 If Element is a variable then if SetVariable is a ground singleton, 770 then Element is unified with its single element, otherwise the constraint 771 is suspended until Element or SetVariable is ground."), 772 resat: "No.", 773 fail_if: "Fails if Element can not be a member of SetVariable.", 774 eg:" 775?- S `:: []..[a,b], a `@ S, glb_poss(S,G,P). 776G = [a], P = [b] 777 778?- S `:: []+[a,b], c `@ S. 779no 780 781?- S `:: [a]+[b,c], a `@ S, glb_poss(S,G,P). 782G = [a], P = [b,c] 783 784?- S `:: []..[a,b], X `@ S, glb_poss(S,G,P). 785G = [], P = [a,b] 786 787?- S `:: []..[a,b], X `@ S, X=b, glb_poss(S,G,P). 788G = [b], P = [a] 789 790?- S `:: [a]+[b,c]:C, X `@ S, C=1. 791X = a 792", 793 see_also:[in/2,(`-@)/2,notin/2,(`::)/2] 794 ]). 795 796 797:-comment(in/2, [ 798% amode: in(?,?), 799% amode: (? in ?), 800 template: "?Element in ?SetVariable", 801 args: ["SetVariable": "A set variable.", 802 "Element": "A ground term or a variable."], 803 summary: "Set membership constraint", 804 desc: html("Constrain SetVariable to include Element.<P> 805 in/2 is available for compatibility with conjunto library syntax. 806 It is equivalent to the preferred `@/2. See its description for details."), 807 resat: "No.", 808 fail_if: "Fails if Element can not be a member of SetVariable.", 809 see_also:[(`@)/2,(`-@)/2,notin/2,(`::)/2] 810 ]). 811 812 813 814:-comment((`-@)/2, [ 815% amode: `-@(?,?), 816% amode: (? `-@ ?), 817 template: "?Element `-@ ?SetVariable", 818 args: ["SetVariable": "A set variable.", 819 "Element": "A ground term or a variable."], 820 summary: "Set non-membership constraint", 821 desc: html("Constrain SetVariable to not include Element.<P> 822 If Element is a variable then the constraint 823 is suspended until it becomes ground."), 824 resat: "No.", 825 fail_if: "Fails if Element must be a member of SetVariable.", 826 eg:" 827?- S `:: []..[a,b], a `-@ S, glb_poss(S,G,P). 828G = [], P = [b] 829 830?- S `:: [c]+[a,b], c `-@ S. 831no 832 833?- S `:: [a]+[b,c], z `-@ S, glb_poss(S,G,P). 834G = [a], P = [b,c] 835 836?- S `:: []..[a,b], X `-@ S, glb_poss(S,G,P). 837G = [], P = [a,b] 838 839?- S `:: []..[a,b], X `-@ S, X=b, glb_poss(S,G,P). 840G = [], P = [a] 841", 842 see_also:[(`@)/2,in/2,notin/2,(`::)/2] 843 ]). 844 845 846:-comment(notin/2, [ 847% amode: notin(?,?), 848% amode: (? notin ?), 849 template: "?Element notin ?SetVariable", 850 args: ["SetVariable": "A set variable.", 851 "Element": "A ground term or a variable."], 852 summary: "Set non-membership constraint", 853 desc: html("Constrain SetVariable to not include Element.<P> 854 notin/2 is available for compatibility with conjunto library syntax. 855 It is equivalent to the preferred `-@/2. See its description for details."), 856 resat: "No.", 857 fail_if: "Fails if Element must be a member of SetVariable.", 858 see_also:[(`-@)/2,(`@)/2,in/2,(`::)/2] 859 ]). 860 861 862 863 864:-comment((`$)/2, [ 865% amode: `$(?,?), 866% amode: (? `$ ?), 867 template: "?SetVar1 `$ ?SetVar2", 868 args: ["SetVar1": "A set variable.", 869 "SetVar2": "A set variable."], 870 summary: "Set disjointness constraint", 871 desc: html("Constrain sets SetVar1 and SetVar2 to be disjoint. I.e. SetVar1 and 872 SetVar2 should have no common elements (empty intersection)."), 873 resat: "No.", 874 fail_if: "Fails if SetVar1 and SetVar2 can not be disjoint.", 875 eg:" 876?- [] `$ [8], [7] `$ [8], [] `$ []. 877yes 878 879?- [7,8] `$ [8] ; [7] `$ [7,8] ; [a] `$ [a] ; [a,b] `$ [b,a]. 880no 881 882?- sets([X,Y], [],[8,9], [cardinality:1]), X `$ Y, set_labeling([X,Y]). 883X = [8], Y = [9] ; 884X = [9], Y = [8] ; 885no 886 887?- S `:: []+[a,b], X=S, X `$ S. 888S = [], X = [] 889 890?- sets([X,Y], [],[7,8,9], [cardinality:2]), X `$ Y. 891no 892 893?- sets([X,Y], [],[7,8,9], [cardinality:[1,2]]), X `$ Y, #(X,2), #(Y,C). 894C = 1 895 896?- X `:: [a]+[b,c,d], Y `:: []+[a,b,c,d,e,f], X `$ Y, c `@ Y, poss(X,PX), poss(Y,PY). 897PX = [b,d], PY = [b,d,e,f] 898", 899 see_also:[all_disjoint/1,(`<>)/2,complement/2,complement/3,(`/=)/2,(`>=)/2] 900 ]). 901 902:-comment((`<>)/2, [ 903% amode: `<>(?,?), 904% amode: (? `<> ?), 905 template: "?SetVar1 `<> ?SetVar2", 906 args: ["SetVar1": "A set variable.", 907 "SetVar2": "A set variable."], 908 summary: "Set disjointness constraint (obsolete)", 909 desc: html("Constrain sets SetVar1 and SetVar2 to be disjoint.<P> 910 Obsolete: `<>/2 is available only for compatibility with conjunto library syntax. 911 It is equivalent to the preferred `$/2. See its description for details."), 912 see_also:[(`$)/2,all_disjoint/1,complement/2,complement/3,(`/=)/2,(`>=)/2] 913 ]). 914 915 916:-comment(all_disjoint/1, [ 917 amode: all_disjoint(+), 918 args: ["SetVars": "A list of set variables."], 919 summary: "All sets disjointness global constraint", 920 desc: html("Constrain all pairs of sets in SetVars to be disjoint. I.e. No two sets 921 can have a common element (empty pairwise intersection).<P> 922 This version of all_disjoint/1 is a weak global constraint, but stronger 923 than the simple posting of all pairwise disjoint/2 constraints, since 924 it posts the additional constraint that the sum of the cardinalities of 925 SetVars must be less than or equal to the cardinality of the union of all 926 the initial LUBs."), 927 resat: "No.", 928 fail_if: "Fails if SetVars can not be all disjoint.", 929 eg:" 930?- all_disjoint([[7],[8],[i,k]]). 931yes 932 933?- all_disjoint([[7,8],[i],[8]]). 934no 935 936?- sets([X,Y,Z], [],[1,2,7,8,9], [cardinality:2]), all_disjoint([X,Y,Z]). 937no 938 939?- sets([X,Y,Z], [],[1,2,7,8,9], [cardinality:2]), all_disjoint([X,Y,Z]), 2 `@ X, lub(Y,LubY), lub(Z,LubZ) 940LubY = [1,7,8,9], LubZ = [1,7,8,9] 941", 942 see_also:[(`$)/2,(`<>)/2,complement/2,complement/3,(`/=)/2,(`>=),all_union/2] 943 ]). 944 945 946 947 948:-comment((`>=)/2, [ 949% amode: `>=(?,?), 950% amode: (? `>= ?), 951 template: "?SetVar1 `>= ?SetVar2", 952 args: ["SetVar1": "A set variable.", 953 "SetVar2": "A variable."], 954 summary: "Set inclusion constraint", 955 desc: html("Constrain sets SetVar1 and SetVar2 so that SetVar1 contains SetVar2.<P> 956 If SetVar2 is not yet a set domain variable it is declared as such, using 957 SetVar1's lub."), 958 resat: "No.", 959 fail_if: "Fails if SetVar1 can not contain SetVar2.", 960 eg:" 961?- [7,8,9] `>= [7,9], [7,8,9] `>= [7,8,9], [7,8,9] `>= [], [7,8,9] `>= [9]. 962yes 963 964?- [1,7,9] `>= [7,8]. 965no 966 967?- X `:: [a]+[b,c,d], Y `:: []+[a,b,c,d,e,f], X `>= Y, poss(Y,PY). 968PY = [a,b,c,d] 969 970?- X `:: [a]+[b,c,d], Y `:: []+[a,b,c,d,e,f], Y `>= X, glb(Y,GY). 971GY = [a] 972 973?- X `:: [a]+[b,c,d,z]:CX, Y `:: []+[a,b,c,d,e,f]:CY, X `>= Y, CX=2, fd:maxdomain(CY,MaxCY). 974MaxCY = 2 975 976?- X `:: [a]+[b,c,d,z]:CX, Y `:: []+[a,b,c,d,e,f]:CY, X `>= Y, CY=3, fd:mindomain(CX,MinCX). 977MinCX = 3. 978", 979 see_also:[(`<)/2,(`=)/2] 980 ]). 981 982:-comment((`<)/2, [ 983% amode: `<(?,?), 984% amode: (? `< ?), 985 template: "?SetVar1 `< ?SetVar2", 986 args: ["SetVar1": "A set variable.", 987 "SetVar2": "A variable."], 988 summary: "Set inclusion constraint (obsolete)", 989 desc: html("Constrain sets SetVar1 and SetVar2 so that SetVar2 contains SetVar1.<P> 990 Obsolete: (`<)/2 is available only for compatibility with conjunto library syntax. 991 It is equivalent (with swapped arguments) to the preferred `>=/2. 992 See its description for details."), 993 see_also:[(`>=)/2,(`=)/2] 994 ]). 995 996 997 998 999:-comment(all_union/2, [ 1000 amode: all_union(+,?), 1001 args: ["SetVars": "A list of variables.", 1002 "Union": "A variable or a ground set."], 1003 summary: "Union constraint of a list of sets", 1004 desc: html("Constraint: Union is the set union of SetVars.<P> 1005 Any variable in SetVars that is not yet a set domain variable, is declared 1006 as such using Union's lub."), 1007 resat: "No.", 1008 fail_if: "Fails if Union can not be the union of SetVars.", 1009 eg:" 1010?- all_union([[8,a,9],[i,8,o],[],[a,8,5]], U). 1011U = [5,8,9,a,i,o]. 1012 1013?- all_union([X,Z,S,Y,T], [8,9]), glb_poss(X,GX,PX), glb_poss(Y,GY,PY). 1014GX = [], PX = [8,9], GY = [], PY = [8,9] 1015 1016?- X `:: [a]+[b,c], all_union([X,[b,n],X], U), glb_poss(X,GX,PX), glb_poss(U,GU,PU). 1017GX = [a], PX = [b,c], GU = [a,b,n], PU = [c] 1018 1019?- sets([X,Y,Z],[a,b],[d,g,h,j],[cardinality:4]), all_union([X,Y,Z],U), #(U,C), fd:dom(C,DomC). 1020DomC = [4,5,6] 1021 1022?- sets([X,Y,Z],[a,b],[d,g,h,j],[]), all_union([X,Y,Z],U), #(U,4), #(Y,C), fd:dom(C,DomC). 1023DomC = [2,3,4] 1024", 1025 see_also:[(`=)/2,all_disjoint/1] 1026 ]). 1027 1028 1029 1030 1031:-comment((`/=)/2, [ 1032% amode: `/=(?,?), 1033% amode: (? `/= ?), 1034 template: "?SetVar1 `/= ?SetVar2", 1035 args: ["SetVar1": "A set variable.", 1036 "SetVar2": "A set variable."], 1037 summary: "Set inequality constraint", 1038 desc: html("Constrain sets SetVar1 and SetVar2 to be different.<P> 1039 This constraint is suspended until one of the two sets is bound 1040 to another set (variable or ground)."), 1041 resat: "No.", 1042 fail_if: "Fails if SetVar1 and SetVar2 must be the same set.", 1043 eg:" 1044?- [] `/= [8], [7] `/= [8], [7,8] `/= [8], [7] `/= [7,8]. 1045yes 1046 1047?- [] `/= [] ; [a] `/= [a] ; [a,b] `/= [b,a]. 1048no 1049 1050?- sets([X,Y], [],[8,9], [cardinality:1]), X `/= Y, set_labeling([X,Y]). 1051X = [8], Y = [9] ; 1052X = [9], Y = [8] ; 1053no 1054 1055?- sets([X,Y], [],[8,9], []), X `/= Y, X=Y. 1056no 1057 1058?- X `:: [8]+[8,9], [8,9] `/= X, card_labeling([X]). 1059X = [8] ; 1060no 1061", 1062 see_also:[(`$)/2,complement/2,complement/3,(`=)/2] 1063 ]). 1064 1065 1066 1067 1068:-comment(complement/3, [ 1069 amode: complement(?,++,?), 1070 args: ["SetVar": "A variable.", 1071 "Universe": "A ground set.", 1072 "Complement": "A variable"], 1073 summary: "Set complement constraint", 1074 desc: html("Constrain sets so that Complement is the complement set of SetVar, 1075 with respect to the given Universe. I.e. Complement is Universe \\ SetVar.<P> 1076 If a variable (SetVar or Complement) is not yet a set domain variable, 1077 it is declared as such, limited by the Universe.<P> 1078 This constraint is usually more efficient (stronger) than posting an 1079 equivalent set difference constraint, due to specific inferences."), 1080 resat: "No.", 1081 fail_if: "Fails if Complement can not be the set complement of SetVar in set universe Universe.", 1082 eg:" 1083?- complement([7,8], [1,7,8,9], N). 1084N = [1,9] 1085 1086?- complement(N, [1,7,8,9], [7,8]). 1087N = [1,9] 1088 1089?- X `:: [a]+[b,c,d], Y `:: []+[a,b,c,d,e,f], complement(X, [a,b,c,d,e,f,g], Y). 1090no 1091 1092?- X `:: [a]+[b,c,d], Y `:: []+[a,b,c,d,e,f], complement(X,[a,b,f],Y), domain(X,DX),domain(Y,DY). 1093DX = [[a]:1,[b]:2], DY = [[f]:1,[b]:2] 1094 1095?- X `:: [a]+[b,c,d], Y `:: []+[a,b,c,d,e,f], complement(X, [a,b,c,d,e,f], Y), domain(Y,DY). 1096DY = [[e,f]:2,[b,c,d]:5] 1097", 1098 see_also:[complement/2,(`$)/2,(`=)/2] 1099 ]). 1100 1101 1102:-comment(complement/2, [ 1103 amode: complement(?,?), 1104 args: ["SetVar": "A variable.", 1105 "Complement": "A variable"], 1106 summary: "Set complement constraint", 1107 desc: html("Constrain sets so that Complement is the complement set of SetVar. 1108 (The universe is taken as the union of their LUBs.)."), 1109 resat: "No.", 1110 fail_if: "Fails if Complement can not be the set complement of SetVar (in their universe).", 1111 eg:" 1112?- complement([8,9], []), complement([8,9], [t]). 1113yes 1114 1115?- complement([8,9], [8]). 1116no 1117 1118?- complement([8,9], N). 1119N = [] 1120 1121?- sets([X,Y], [],[7,8,9], []), complement(X,Y), 8 `@ Y, glb_poss(X,GX,PX), glb_poss(Y,GY,PY). 1122GX = [], PX = [7,9], GY = [8], PY = [7,9] 1123 1124?- sets([X,Y], [],[7,8,9], [cardinality:C]), complement(X,Y), card_labeling([X]). 1125no 1126 1127?- sets([X,Y], [],[7,8,9], []), complement(X,Y), X `>= Y, set_labeling(up,[Y]). 1128Y = [], X = [7,8,9] ; 1129no 1130 1131?- sets([X,Y], [],[7,8,9], [minimum:Min]), complement(X,Y), refine(up,X). 1132no 1133 1134?- sets([X,Y], [],[7,8,9], []), complement(X,Y), #(X,1), #(Y,CY). 1135CY = 2 1136", 1137 see_also:[complement/3,(`$)/2,(`=)/2] 1138 ]). 1139 1140 1141 1142 1143:-comment((`=)/2, [ 1144% amode: `=(?,?), 1145% amode: (? `= ?), 1146 template: "?SetExp1 `= ?SetExp2", 1147 args: ["SetExp1": "A set expression.", 1148 "SetExp2": "A set expression."], 1149 summary: "Set equality constraint", 1150 desc: html("Constrain sets in both hand sides of equation so that SetExp1 and 1151 SetExp2 represent the same set.<P> 1152 A set expression is a set (variable or ground) or a set operation between 1153 two set expressions. Possible set operations are set union, set intersection 1154 and set difference, and the respective operators are `\\/, `/\\ and `\\. 1155 These operators are defined as: 1156<PRE> 1157:- op(500, yfx, `\\/). %set union 1158:- op(400, yfx, `/\\). %set intersection 1159:- op(300, yfx, `\\ ). %set difference 1160</PRE>"), 1161 resat: "No.", 1162 fail_if: "Fails if SetExp1 can not be the same set as SetExp2.", 1163 eg:" 1164/* 1165Examples of equalities between set expressions, being S,T,U,V,W,X,Y,Z set variables: 1166 1167X `= Y 1168S `\\/ Y `\\ Z `= T `/\\ S `\\/ U `/\\ W 1169V `\\ ([a,b,d] `\\/ W) `\\/ (S `\\ W) `= ((T `/\\ [3,9]) `\\/ W) `\\ U 1170*/ 1171 1172% just union: 1173?- [8,a,9] `\\/ [i,8,o] `\\/ [] `\\/ [a,8,5] `= U. 1174U = [5,8,9,a,i,o] 1175 1176?- X `\\/ Y `= [8,9], glb_poss(X,GX,PX), glb_poss(Y,GY,PY). 1177GX = [], PX = [8,9], GY = [], PY = [8,9] 1178 1179?- X `:: [a]+[b,c], X `\\/ [b,n] `= U, glb_poss(X,GX,PX), glb_poss(U,GU,PU). 1180GX = [a], PX = [b,c], GU = [a,b,n], PU = [c] 1181 1182?- sets([A,B],[a,b],[d,g,h,j],[cardinality:4]), A`\\/B`=U, #(U,C), fd:dom(C,DomC). 1183DomC = [4,5,6] 1184 1185?- sets([X,Y],[a,b],[d,g,h,j],[]), X`\\/Y`=U, #(U,4), #(Y,C), fd:dom(C,DomC). 1186DomC = [2,3,4] 1187 1188?- sets([S,X], [],[a,b], [cardinality:[0,2]]), U `= X `\\/ S, #(U,C), fd:dom(C,DomC). 1189DomC = [0,2] 1190 1191?- S `:: [a,c]+[b,g,h,j,l]:3, X`::[a]+[b,h,t,u,y]:2, U `= X `\\/ S, #(U,C), fd:dom(C,DomC). 1192DomC = [3,4] 1193 1194?- S `:: [a,c]+[b,g,h,j,l], X`::[a]+[b,h,t,u,y], U `= X `\\/ S, #(U,C), fd:(C::0..3), #(X,CX), fd:dom(CX,DomCX). 1195DomCX = [1,2] 1196 1197 1198% just intersection: 1199?- I `= [4,6] `/\\ [3,6,8]. 1200I = [6] 1201 1202?- [a,b,c,d,e] `/\\ [a,b,c,e,f,g] `/\\ [b,d,e,f,x,y] `= I. 1203I = [b,e] 1204 1205?- X `:: [a]+[b,c], X `/\\ [b,n] `= I, glb_poss(X,GX,PX), glb_poss(I,GI,PI). 1206GX = [a], PX = [b,c], GI = [], PI = [b] 1207 1208?- S `:: [a]+[b,c], X`::[]+[7,8,9], I`::[]+[a,b,c,7,z,99], I `= X `/\\ S. 1209I = [] 1210 1211?- sets([A,B],[a,b],[d,g,h,j],[cardinality:5]), A`/\\B`=I, #(I,C), fd:dom(C,DomC). 1212DomC = [4,5] 1213 1214?- S `:: [a,c]+[g,h,j,l], X`::[a]+[b,h,t,u,y], I `= X `/\\ S, #(I,C), fd:dom(C,DomC). 1215DomC = [1,2] 1216 1217 1218% just difference: 1219?- D `= [4,6] `\\ [3,6,8]. 1220D = [4] 1221 1222?- [a,b,c,d,e] `\\ [a,e,f,g] `\\ [b,d,e,f,x,y] `= D. 1223D = [c] 1224 1225?- [a,b,c,d,e] `\\ ([a,e,f,g] `\\ [b,d,e,f,x,y]) `= D. 1226D = [b,c,d,e] 1227 1228?- X `:: [a]+[b,c], X `\\ [b,n] `= D, glb_poss(X,GX,PX), glb_poss(D,GD,PD). 1229GX = [a], PX = [b,c], GD = [a], PD = [c] 1230 1231?- S `:: [a]+[b,c], X`::[]+[7,8,9], D`::[]+[a,b,c,7,z,99], D `= X `\\ S, glb_poss(D,GD,PD). 1232GD = [], PD = [7] 1233 1234?- sets([A,B],[a,b],[d,g,h,j],[cardinality:5]), A`\\B`=D, #(D,C), fd:dom(C,DomC). 1235DomC = [0,1] 1236 1237?- sets([X,Y],[a,b],[d,g,h,j],[]), X`\\Y`=D, #(D,4). 1238X = [a,b,d,g,h,j], Y = [a,b] 1239 1240?- S `:: [a,c,z]+[g,h], X`::[a]+[b,c,h,t], D `= S `\\ X, #(D,C), fd:dom(C,DomC). 1241DomC = [1,2,3,4]. 1242 1243?- S `:: []+[a,b], X=S, #(S `\\ X, C). 1244C = 0", 1245 see_also:[(`/=)/2,set_labeling/1,set_labeling/2] 1246 ]). 1247 1248 1249 1250 1251:-comment(my_print_set_handler/2, hidden). 1252:-comment(my_unify_sets_handler/2, hidden). 1253 1254 1255:-comment(struct(cardinal), [ 1256 summary: "Cardinal attributes of a set variable", 1257 fields:[domain: "Set domain in the form [Glb:NIn,Poss:NMax], where Glb is the set's 1258 glb, NIn its cardinality, Poss is its poss (i.e. its lub\\glb), 1259 and NMax is the lub's cardinality (i.e. NIn + #(Poss)). 1260 If it is a set of sets and a union function attribute has been 1261 declared, then each element of Poss comes annotated with its 1262 respective length.", 1263 cardinality: "Cardinality function (an integer or an FD variable).", 1264 minimum: "Minimum function (an integer or an FD variable), 1265 for sets of integers. Free variable if unused.", 1266 maximum: "Maximum function (an integer or an FD variable), 1267 for sets of integers. Free variable if unused.", 1268 union: html("Union function, for sets of sets. Free variable if unused; 1269 otherwise, a list in the form 1270 [UnionVar, GlbU+PossU, Singles, Lengths], where:<PRE> 1271UnionVar: A set (variable or ground) corresponding to the union of the set's elements 1272 (sets themselves); 1273GlbU: Set union of the set's glb; 1274PossU: Set of possible union elements with counters (X:N), i.e. an ordered 1275 list of all elements in the sets in set's poss (lub\\glb) 1276 with the number of occurrences attached 1277Singles: Set of elements where N=1 in PossU</PRE>"), 1278 bounded: "Suspension list.", 1279 glb: "Suspension list.", 1280 lub: "Suspension list.", 1281 bound: "Suspension list." 1282 ] 1283 ]). 1284