Home

JSetL User's Manual

1. gt true x equals y gt false x equals v gt true e Output bound unbound logical variables x output gt unknown y output gt y unknown z output gt z 2 e Convert to string x toString gt _ y toString gt _y z toString gt 2 2 3 Constraint methods Constraints see Sect 7 can be posted over logical variables In particular the class LVar provides methods for generating equality inequality membership and not membership con straints Constraint eq Object o Returns the atomic constraint this o that unifies this logical variable with the object o In particular if o is an object other than a logical variable and this variable is unbound this variable becomes bound to o after the constraint has been solved Constraint neq Object o Returns the atomic constraint this o that requires this logical variable to be different from the object o Constraint in LSet 1s Constraint in Set lt gt s Return the atomic constraint this 1s resp this s that requires this logical variable to be a member of the logical set 1s resp of the Java generic set s see Sect 4 for the notion of logical set When solved this constraint will nondeterministically unify this logical variable with each value in 1s resp in s The constraint will succeed if at least one unification succeeds Note that if this logical variable is unbound
2. 1 50 100 1000 and D 0 40 respectively Let us see how the variable choice heuristics work e LEFT_MOST selects the variable x e MID_MOST selects the variable y e RIGHT_MOST selects the variable z e MIN selects the variable z e MAX selects the variable y e FIRST_FAIL selects the variable x e RANDOM selects a variable v x y z such that P v q Plv y Pv 2 3 The enumeration ValHeuristic ValHeuristic is a Java enumeration that implements the possible value choice heuristics for a selected IntLVar x with domain the multi interval Dx I U U Ip Such enum consists of the following fields GLB Selects the GLB of Dz LUB Selects the LUB of Dy MID_MOST 3 ES Ig it 9 n Selects the middle point o of the central interval Ig where k z MEDIAN Selects the median value of D note that if D is even the minimum between the two median values of D will be selected EQUI_RANDOM Selects a pseudorandom equidistributed value in D The notation P E indicates the probability that a given event E occurs 45 RANGE_RANDOM Selects a pseudorandom equidistributed value in I where k is a pseudorandom equidistributed value in 1 n MID_RANDOM Selects the midpoint of an interval I where k is a pseudorandom equidistributed value in 1 n Note that unlike EQUI_RANDOM RANGE_RANDOM does not select an equidistributed value in D the probability that a
3. Constraint eq IntLVar vars Constraint eq Collection lt IntLVar gt vars Returns the constraint Xy X1 Xn A Co where Xo is this logical variable Co is its associated constraint and X1 Xn is the collection of integer logical variables belonging to vars 26 Constraint eq IntLVar vars SetLVar r Constraint eq Collection lt IntLVar gt vars SetLVar r Returns the constraint Xy X1 Xn r A Co where Xo is this logical vari able Co is its associated constraint and X X is the collection of integer logical variables belonging to vars Note that in the current implementation constraints of the form S X Xn R are simply unfolded in n union constraints S S8 U U SUR where S X for each i 1 n Moreover in order to represent each singleton S X the following constraints are added to the constraint store for i 1 n Xi Si A Si 7 Constraints the class Constraint Constraints represent operations that can be applied to logical variables and logical collec tions as well as to objects created by their derived sub classes These operations can be performed even if the involved logical objects have no precise value associated with them A constraint in JSetL is an expression that can take one of the forms e atomic constraints the empty constraint denoted e9 0p 1 n or opl eo e1 n with n 0 3 where op is the name of the co
4. Example 14 New constraint absTest public class MathOps extends NewConstraintsClass public MathOps SolverClass s super s public Constraint absTest IntLVar x IntLVar y return new Constraint absTest x y protected void user_code Constraint c throws Failure NotDefConstraintException if c getName absTest absTest c else if other constraints implemented by MarhOps else throw new NotDefConstraintException private void absTest Constraint c throws Failure IntLVar x IntLVar c getArg 1 IntLVar y IntLVar c getArg 2 if x isBound irreducible case c notSolved return F if x getValue gt 0 Solver add x eq y x else Solver add x eq new IntLVar 0 sub y x return Il lt Il o l lt A possible use of the new constraint absTest is 34 MathOps mathOps new MathOps solver IntLVar x new IntLVar x 3 IntLVar y new IntLVar y solver check mathOps absTest x y y output whose execution generates the output s Note that by default a user defined constraint is always set to solved whenever it is processed by the solver If this is not the case e g the constraint is simply left unchanged in the constraint store then the user should explicitly state that the constraint is still unsolved This is obtained by using the following method of the class Constraint void notSolved Sets the solved
5. where elems is a set 9 n n gt 0 of objects of arbitrary types the set value and rest is either an empty or an unbound l set representing the remainder of s When rest is an unbound l set r we say that s represents an open set and we use the abstract notation eo n r to denote it conversely when rest is the empty l set we say that s represents a closed set and we use the abstract notation eo en When elems is the empty set and rest is null s is the empty l set and we use to denote it Logical sets are similar to logic lists in many aspects In particular like l lists l sets can represent partially specified collections The main difference with lists is that the order of elements and repetitions in a l set do not matter while they are important in lists Note that differently from lists the cardinality of a partially specified set is not de termined uniquely even if the set is closed For example the cardinality of the set 1 x where x is an unbound variable can be 1 or 2 depending on whether x will be subsequently bound to a value equal to 1 or different from 1 respectively 10 In JSetL a logical set is defined as an instance of the class LSet which extends the class LCollection In particular set values i e the elems part of the l set are instances of the class HashSet which implements the java util Set interface Methods provided by the class LSet are basically the same as those of
6. Create a logical variable with no external name resp with external name extName equivalent to the logical variable 1v Same as to create an unbound logical variable x and to post and solve the constraint x eq 1v We say that two logical variables x and y are equivalent if they have been successfully unified e g by x eq y Equivalent variables are dealt with as they were the same variable If a and y are unbound and z is unified to y both x and y remain unbound if later on x is bound to some value o then y becomes bound to the same value o Example 1 e Create an unbound logical variable x without any external name LVar x new LVar e Create an unbound logical variable y with external name y LVar y new LVar y e Create a logical variable z with external name z bound to the integer value 2 LVar z new LVar z 2 e Create a logical variable v equivalent to the logical variable x LVar v new LVar x Note that in the last definition the logical variable v is unified with the logical variable x Both variables are unbound If either x or v is subsequently bound to some value both x and v become bound to this value 2 2 General utility methods The class LVar provides a number of utility methods that allow to inspect the logical variable e g to test if it is bound to get and set its external name to print its value and so on LVar clone Creates and returns a copy of this logical
7. Sa Y A B A B C Zp The class SetInterval allows to represent and manipulate the set intervals A B Sg First of all it is worth noting that the integer sets belonging to set intervals are modelled by the class MultiInterval This is not surprising as seen in the previous section multi intervals and sets of integers belonging to a fixed universe are in bijective correspondence Moreover as for integer intervals observe that set intervals are e finite even if they contain an exponential number of elements A B 218171 Thus a normalization operator g P Z P Zg such that def DI DONP Zg is needed e convex a convex closure operator CHg P Z Sg such that CHAD Y minc S Sg DIl3 S is needed Since for each set interval A B Sg we have that Y C A and B C Zg 68 6 SetInterval class will have two static fields e public static final MultiInterval INF new MultiInterval e public static final MultiInterval SUP new MultiInterval Interval SUP 2 Interval SUP 2 which represent respectively the minimum and the maximum value according to the partial order C that a set interval element can take Obviously INF is the empty set Instead SUP corresponds to Zg it means that the fixed value of 68 is Interval SUP 2 Moreover SetInterval provides the static method universe which returns the universe 9 Zg Constructors SetInterval Creates the
8. provided 1v resp o belongs to 1s resp to s Constraint size IntLVar lv Constraint size Integer i Return the atomic constraint this 1v resp this i that requires the logical variable 1v resp the integer variable i to be equal to the cardinality of this l set Constraint subset LSet ls Constraint subset Set lt gt s Return the atomic constraint this C 1s resp this C s Constraint union LSet 1s1 LSet 1s2 Constraint union LSet 1s Set lt gt s Constraint union Set lt gt s LSet 1s Constraint union Set lt gt si Set lt gt s2 Return the atomic constraint this 1s1 U 1s2 resp this 1s Us this s U ls this s1 U s2 14 Global constraints Constraint allDiff Same as allDiff of class LList Constraint forallElems LVar y Constraint c Same as forallElems of class LList 5 Integer logical variables the class IntLVar Integer logical variables are a special case of the logical variables described in Section 2 in which values are restricted to be integer numbers Moreover an integer logical variable has a finite domain and a possibly empty integer arithmetic constraint associated with it The domain is represented as a multi interval that is the union of n n gt 0 disjoint intervals see Sections A 1 and A 2 for a precise description of intervals and multi intervals in JSetL A domain for an integer logical variable v can be specified when the variable v is cre
9. see Sect 3 4 e constraints over LSet objects see Sect 4 4 e constraints over IntLvar objects see Sect 5 4 e constraints over SetLVar objects see Sect 6 4 8 Constraint solving the class SolverClass Constraints are solved using a constraint solver In JSetl a constraint solver can be created as an instance of the class SolverClass Basically this class provides methods for post ing constraints i e adding constraints to the current collection of constraints constraint store as well as inspecting checking satisfiability and finding all solutions of the posted constraints The class SolverClass and its methods are described in detail in this section 29 8 1 Posting and inspecting constraints Constraints can be posted to a specific constraint solver by adding them to its constraint store The collection of constraints in the constraint store is logically interpreted as a conjunction of constraints Each addition to the constraint store adds a conjunct to the constraint conjunction represented by the store void add Constraint c Adds a constraint c either atomic or compound to the constraint store of this solver No processing of the added constraint is performed at this stage void addChoicePoint Constraint c See Sect 9 3 void clearStore Removes all constraints from the constraint store of this solver It also removes all choice points possibly associated with the current collection of constraints Cons
10. String getName Set lt gt get Value boolean isBound void output LSet setName String extName String toString Remarks of Section 3 3 apply to l sets as well 4 3 2 Logical collection methods The class LSet provides all the collection methods of class LList see Section 3 3 2 Note that like in the case of l lists most of the collection methods take into account only the elems part i e the set value of the invocation l set while the rest part is simply ignored Object get int i LSet getRest int getSize boolean isClosed boolean isEmpty O 12 boolean isGround O Iterator iterator void printElems char sep boolean testContains Object o Vector toVector Remarks e LSet objects may contain multiple occurrences of the same value For example if s is the set x 2 where x is a logical variable and x is bound to 2 then s contains two occurrences of the same value 2 However all methods dealing with l sets but method toVector ignore repetitions i e they consider multiple occurrences of the same value as a single set element For example calling getSize on the set s considered above will get 1 as its result Conversely s toVector will get the vector 2 2 e Since the order of elements in a l set does not matter s get i where s is a l set can return any element of s The implementation only guarantees that different values of i correspond to diff
11. are VarHeuristic var The variable choice heuristic ValHeuristic val The value choice heuristic SetHeuristic set For labeling on SetLVar s see Section B 2 This class provides only one constructor LabelingOptions that initializes such fields to their default values which are e var LEFT_MOST e val GLB e set FIRST_NIN Example 22 The statements 47 LabelingOptions lop new LabelingOptions lop var VarHeuristic FIRST_FAIL lop val ValHeuristic MEDIAN set the variable choice heuristic to FIRST_FAIL and the value choice heuristic to MEDIAN Note that since the field set is not modified lop set will retain the default value SetHeuristic FIRST_NIN Objects of type LabelingOptions are used as parameters for labeling constraint methods see Sections 5 4 and 6 4 B 2 Labeling on integer set logical variables In addition to the data structures presented in the previous section JSetL provides the enumeration SetHeuristic Before introducing such enumeration it is important to note that labeling on set variables is quite different from labeling on integer variables Indeed while for integer logical variables each labeled variable x is directly instantiated with a value k belonging to its domain for set variables the same approach turns out to be impracticable This is because each set variable X with domain A B could be instantiated by an exponential number of elements precisely 211 141 belonging to it
12. by the character sep without the surrounding square brackets If this l list is unbound prints _extName where extName is the external name of this list Vector toVector If this Hist is bound returns a vector containing all of the elements of its list value Ortherwise raises an exception NotInitVarException The following methods are also provided by the interface List of java util and are intended to work on the list value possibly associated with a LList object They could always be replaced by an invocation to the equivalent method of List applied to the list value that is returned by calling getValue on the llist However they are provided by LList for the user convenience int getSize If this Llist is bound returns the number of elements in its list value Otherwise i e if this Hist is unbound it raises an exception NotInitVarException When the l list v is bound v getSize is equivalent to v getValue O size Iterator iterator If this l list is bound returns an Iterator over the elements of its list value Other wise it raises an exception NotInitVarException When the Llist vis bound v iterator is equivalent to v getValue iterator boolean testContains Object o If this hlist is bound returns true if its list value contains o Note that o can be a logical object i e either a logical variable or a logical collection in this case the value possibly associated with o is considered for the member
13. computed if possible Computing the solution may involve nondeterminism The resulting constraint store will contain a possibly simplified form of the constraint C A c Conversely if C A c is unsatisfiable all unbound variables in C A c and the constraint store remain unchanged boolean check Same as check c in which c is the empty constraint void failure Raises a failure exception void solve Constraint c void solve Same as check c resp check but if the constraint C A c resp C is found to be unsatisfiable a failure exception is raised Remark The JSetL constraint solving procedure is guaranteed to be complete for con straints involving only equality inequality and l set constraints Conversely if also con straints over IntLVar and SetLVar are considered completeness is guaranteed only if solu tions are forced to be computed through labeling Sections 5 4 and 6 4 8 3 Getting solutions boolean nextSolution If issued after a check or a solve or another nextSolution it tries to compute the next solution for the constraint in the constraint store of this solver If a solution exists it returns true otherwise it returns false In the last case the content of the resulting constraint store is undefined LSet setof LVar x Constraint c If C is the constraint currently in the constraint store of this solver returns the logical set obtained by adding to it all assignments for x that makes the constrai
14. empty set interval 42 SetInterval Multilnterval A Creates the set interval A SetInterval Multilnterval A Multilnterval B Creates the interval A B g SetInterval Collection lt MultiInterval gt D Creates the interval CHg D Example 19 Set interval constructors e Create an empty set interval since 2 8 1 g 2 8 1 NP Za MultiInterval m new Multilnterval 2 SetInterval SUP getLubQ 1 SetInterval s new SetInterval m e Create the set interval CHg 0 1 2 0 1 minc S e Sa 0 1 CS 5 0 1 Multilnterval m new Multilnterval 2 SetInterval SUP getLub 1 Multilnterval m0 new MultilInterval 0 Multilnterval mi new Multilnterval 1 Vector lt MultiInterval gt v new Vector lt MultiInterval gt v add m v add m0 v add mi SetInterval s new SetInterval v Other utility methods boolean contains MultiInterval M Returns true iff M this boolean isEmpty O Returns true iff this 9 boolean isSingleton O Returns true iff this 1 boolean isUniverse Returns true iff this 9 Z g double size Let A and B be the GLB and LUB of this respectively This method returns this 214 121 iff B A lt Double MAX_EXPONENT 1023 otherwise it returns Double POSITIVE_INFINITY MultiInterval getGlb Returns the GLB of this if this null otherwise MultiInterval getLub Returns the LUB of this if thi
15. etc as well as equality inequality and comparison operations over integers Constraint solving over integers uses the well known finite domain FD constraint solving techniques Constraint solving over sets uses both the efficient finite set FS constraint solving tech niques of 5 for completely specified sets of integers and the less efficient but more general and complete constraint solving procedure of CLP SET 1 for general possibly partially specified and nested sets of elements of any type Nondeterminism using choice points and backtracking is exploited both by specific methods for solution search namely the labeling methods as well as by constraints over general sets e g set unification set union etc JSetL provides also a simple way the method setof to collect into a set all the computed solutions of a given constraint for a specified logical variable Finally JSetL allows the user to define new constraints and to deal with them as the built in ones How to get JSetL JSetL has been developed at the Department of Mathematics of the University of Parma Italy It is completely written in Java The full Java code of the JSetL library along with sample programs and related documents is available at http cmt math unipr it jsetl html The library is free software one can redistribute it and or modify it under the terms of the GNU General Public License How to use JSetL The library is carried out as a
16. fields Remind that the default value for the set field in class LabelingOptions is SetHeuristic FIRST_NIN 48 Example 23 The statements LabelingOptions lop new LabelingOptions lop var VarHeuristic RANDOM lop val ValHeuristic LUB lop set SetHeuristic FIRST_IN set the variable choice heuristic to RANDOM the value choice heuristic to LUB and the set choice heuristic to FIRST_IN 49 Stampato in proprio a cura degli autori presso il Dipartimento di Matematica dell Universita degli Studi di Parma Parco Area delle Scienze 53 A 43124 Parma adempiuti gli obblighi ai sensi della Legge n 160 del 15 04 2004 Norme relative al deposito legale dei documenti di interesse culturale destinate all uso pubblico G U n 98 del 27 aprile 2004 e del Re golamento di attuazione emanato con D P R n 252 del 3 maggio 2006 G U n 191 del 18 agosto 2006 entrato in vigore il 2 settembre 2006 precedente normativa abrogata Legge n 374 del 2 2 1939 modificata in D L n 660 del 31 agosto 1945 Esemplare fuori commercio per il deposito legale agli effetti della legge 15 aprile 2004 n 160 50
17. flag of this constraint to false i e this constraint is unsolved 9 3 Exploiting nondeterminism Implementation of user defined constraints can exploit the nondeterministic facilities of JSetL In particular the following two methods are provided to support nondeterminism handling int getAlternative in class Constraint Returns an integer associated with the invocation constraint c that can be used to count nondeterministic alternatives within this constraint Its initial value is 0 Each time the constraint c is re considered due to backtracking the value returned by getAlternative is automatically incremented by 1 void fail in class Constraint Causes the invocation constraint to fail This in turn causes the solver to backtrack to the nearest open choice point If no open choice point exists a failure exception is raised void addChoicePoint Constraint c in class solverClass Adds a choice point to the alternative stack of the invocation solver This allows the solver to backtrack and re consider the constraint c if a failure occurs subsequently Upon backtracking the original constraint state is restored as before except for the alternative counter that is incremented by 1 The following is a nondeterministic version of the new constraint absTest x y shown in Example 14 In this case if x is unbound the constraint solving procedure opens two nondeterministic alternatives one in which x is assumed to be non n
18. is unsatisfiable for each integer value that z could take Example 7 e Create an integer logical variable with an associated integer arithmetic constraint IntLVar x new IntLVar x IntLVar y new IntLVar y IntLVar z x sum y sub 1 setName z z output Output z unknown Constraint _z x _ _ _y 1 where _ represents the internal name of the IntLVar object created in correspondence with the subexpression y sub 1 Note that the precedence order of operators is implicitly defined by invoking the corre sponding methods For example the expression x sum y mul 2 allows us to represent the arithmetic expression x y 2 If instead we wanted to build the term x y 2 we should write something like x sum y mul 2 5 4 Constraint methods The class IntLVar provides methods for generating the usual arithmetic comparison con straints Moreover it provides some methods for generating other kinds of constraints such as domain membership all different and labeling constraints Integer comparison constraints Constraint eq Integer k Returns the constraint Xy k A Co where Xo is this logical variable and Co is its associated constraint Constraint eq IntLVar v Returns the constraint Xy v A Co A Cy where Xy is this logical variable Co is its associated constraint and C is the constraint associated with the logical variable v Constraint neq Integer k Constraint neq IntLVar v Sam
19. methods are invoked on IntLVar objects and returns IntLVar objects hence they can be concatenated to form compound arithmetic expressions IntLVar sum Integer k Returns an integer logical variable X with an associated constraint Xy X9 k A Co where Xo is this logical variable and Co is the associated constraint IntLVar sum IntLVar v Returns an integer logical variable X with an associated constraint X Xo v A Cy A Co where Xo is this logical variable Co is its associated constraint and C is the constraint associated with the logical variable v IntLVar sub Integer k IntLVar sub IntLVar v Same as above but with replaced by in the associated constraint IntLVar mul Integer k IntLVar mul IntLVar v Same as above but with replaced by x in the associated constraint IntLVar div Integer k Same as above but with an associated constraint X Xo k A Co A k 0 where Xo is this logical variable and Co is the associated constraint 17 IntLVar div IntLVar v Same as above but with an associated constraint Xy Xo v A Cy A CoA v 40 where Xo is this logical variable Co is the associated constraint and C is the constraint associated with the logical variable v Note that div operator refers to the exact integer division a constraint of the form z x y is satisfiable iff the constraint x z xy y 0 is satisfiable For example z x y with x 7 and y 2 is not satisfiable because the constraint 7 z 2
20. reasonable computational complexity For this reason labeling is improved by special heuristics which allow to reduce the search space Specifically e Variable Choice Heuristics determine the order in which variables are selected for assignment e Value Choice Heuristics determine the order in which domain values are assigned to a selected variable The next subsections will describe techniques and data structures for dealing with labeling on IntLVar and SetLVar objects in JSetL B 1 Labeling on integer logical variables JSetL provides three data structures for modeling choice heuristics the enumerations VarHeuristic and ValHeuristic and the class LabelingOptions The enumeration VarHeuristic VarHeuristic is a Java enumeration that implements the possible variable choice heuristics for a given collection 71 2 of IntLVar s Such enum consists of the following fields LEFT_MOST Selects the leftmost variable x1 RIGHT_MOST Selects the rightmost variable xp 44 MID_MOST i Selects the midmost variable xx where k 5 MIN Selects the leftmost variable with the smallest GLB MAX Selects the leftmost variable with the greatest LUB FIRST_FAIL Selects the leftmost variable with the smallest domain RANDOM Selects a variable xx where k is a pseudorandom equidistributed value in 1 n Example 20 Let us consider three integer logical variables x y and z with associated do mains D 1 10 28 30 Dy
21. solving the constraint will nondeterministically bind this variable to each value in 1s s Constraint nin LSet 1s Constraint nin Set lt gt s Return the atomic constraint this 1s resp this s that requires this logical variable to be not a member of the logical set 1s resp of of the Java generic set s 3 Logical lists the class LList A logical list l or simply a l list 1 is a special kind of logical variable whose value is a pair elems rest where elems the list value is a list eo en n gt 0 of objects of arbitrary types and rest is either an empty or an unbound l list representing the remainder of l When rest is an unbound l list r we say that l represents an open list and we use the abstract notation ep en r to denote it conversely when rest is the empty Hist we say that l represents a closed list and we use the abstract notation eo en When elems is the empty list and rest is null lis the empty l list and we use to denote it A Hist that contains unbound logical objects i e either variables or lists or sets see Sect 4 represents a partially specified list Intuitively some of the list elements are unknown Also an open l list has an unknown part and hence it also represents a partially specified list regardless of whether its elements are bound or not In JSetL a logical list is defined as an instance of the class LList which extends the class LCollection In parti
22. value d D will be chosen is inversely proportional to the size of the interval I to which d belongs However if Dy is an interval then EQUI_RANDOM and RANGE_RANDOM are in fact the same heuristic MID_RANDOM is an hybrid solution first a random interval J is chosen and then the midpoint of I is selected Thus each midpoint has a probability 1 n to be selected Note that if D is an interval then MID_RANDOM MID_MOST and MEDIAN are in fact the same heuristic Example 21 Let us consider again the integer logical variables x y and z with associated domains Dz 1 10 28 30 Dy 1 50 100 1000 and D 0 40 of Example 20 Let us see now how the value choice heuristics work on them indicating with A v the selected value for each variable v x y z GLB A x 1 Ay 1 A z 0 LUB A x 30 A y 100 Az 40 MID MOST A x 5 A y 100 A z 20 MEDIAN A x 7 A y 26 A z 20 Moreover for each a Dz b E Dy ec D we have that EQUI_ RANDOM P A x a 5 PIA y b 5 46 1 1 1 59 86 1 10 RANGE RANDOM P A x a 1 g a 28 30 1 be fl En se b 1 50 1 3 se b 100 se b 1000 if a 5 29 MID_RANDOM P A x a otherwise if b 25 100 1000 Wir O 0 otherwise The class LabelingOptions The class LabelingOptions allows the user to set up the labeling heuristics by properly setting its public fields which
23. 2 Logical variables the class LVar Logical variables represent unknowns As such they have no modifiable value stored in them as ordinary programming languages variables have Conversely one can associate values to logical variables through relations or constraints involving logical variables and values from some specific domains When the domain of a variable is restricted to a single value we say that the variable is bound to or instantiated with this value Otherwise the variable is unbound With a little abuse of terminology we say that the value associated with a bound variable x is the value of x The equality relation in particular allows a precise value to be associated to a logical variable For example if x is a logical variable ranging over the domain of integers the equality x 3 forces x to be bound to the value 3 However the same result can be obtained through other relations e g 1 lt 4Azx gt 2 The value of a logical variable is immutable That is it can not be changed e g by an assignment statement A logical variable may have also an external name associated with The external name is a string value which can be useful when printing the variable and the possible constraints involving it In JSetL a logical variable is an instance of the class LVar This class provides con structors for creating logical variables and a number of simple methods for testing and manipulating logical variables as well as basi
24. Create a constraint with name extName and from 1 to 4 arguments 01 04 7 2 General utility methods boolean equals Constraint c boolean equals Object o Return true if the argument is a constraint and all the atomic constraints occurring in this constraint and in the argument constraint are ordinately equals Atomic con straints are considered equals if all their non null arguments are equal int get Alternative See Sect 9 3 Object getArg int i Returns the i th argument of this constraint if 1 lt i lt k where k is the number of arguments of this constraint null otherwise Note that if applied to a constraint conjunction getArg 1 returns the first conjunct whereas getArg 2 returns the rest of the conjunction void fail See Sect 9 3 String getName Returns the external name associated with this constraint Note that if applied to a constraint conjunction getName returns and boolean isGround Returns true if this constraint does not contain any unbound logical variable or logical collection String toStringO Returns the string corresponding to the external view of this constraint e g using standard infix arithmetic operators String toStringInternals Returns the string corresponding to the internal view of this constraint i e constraint extName arg arg2 arg3 arg4 where arg is either the i th argument of this constraint if 1 lt i lt k or null for i gt k wh
25. Cy where Xo is this logical variable Co is its associated constraint and C is the constraint associated with the logical variable v Constraint subset MultiInterval m Returns the constraint Xy Cm A Co where Xo is this logical variable and Co is its associated constraint Constraint subset SetLVar v Returns the constraint Xy Cv A Xo lt lv A Co A Cy where Xo is this logical variable Co is its associated constraint and C is the constraint associated with the logical variable v Example 11 e Generate the constraint X CY UZ X subset Y union Z e Generate the constraint X NY Y X X intersect Y eq Y diff X e Generate the constraint X 2 7 X neq new MultiInterval 2 union new MultiInterval 7 25 Domain handling constraints Constraint dom Multilnterval a Multilnterval b Returns the constraint Xo a b A Co where Xo is this logical variable and Co is its associated constraint The domain constraint Xo a b constrains Xo to belong to the domain a b If such domain is empty the exception NotValidDomainException is raised Constraint dom SetInterval s Same as above but with domain constraint Xo s Labeling constraints Given n gt 0 integer set logical variables v1 Un labeling them means try to assign to each variable an integer set value belonging to its domain For a more formal and comprehensive explanation of labeling and its heuristics see Append
26. JSetL User s Manual Version 2 3 GIANFRANCO ROSSI AND ROBERTO AMADINI Dipartimento di Matematica Universit di Parma Parma Italy Abstract This manual describes JSetL 2 3 a Java library that offers a number of facilities to support declarative programming like those usually found in constraint logic pro gramming languages logical variables list and set data structures possibly partially specified unification constraint solving over integers and sets nondeterminism JSetL is intended to be used as a general purpose tool not devoted to any specific application The manual describes all the features of JSetL and it shows through simple examples how to use them JSetL has been developed at the Department of Mathematics of the University of Parma Italy It is completely written in Java The full Java code of the JSetL library along with sample programs and related material is available at the JSetL WEB page http cmt math unipr it jsetl html Correspondence to Gianfranco Rossi Dipartimento di Matematica Universit degli Studi di Parma Parco Area delle Scienze 53 A 1 43124 Parma Italy E mail address gianfranco rossi unipr it Contents 1 Introduction 1 2 Logical variables the class LVar 2 2el Constructorso s a ete ee a bbe ha E eee degree Ae eee Pee 2 2 2 General utility methods o ee eee 3 2 9 Cotistraint methods toma aug eee a a eS ae Eee ern 4 3 Logical lists the cla
27. Java package and as such it is subject to the common rules of use defined by the language The classes of the library must be saved into a folder named JSetL To use JSetL in a program it is necessary to import the library by inserting the statement import JSetL at the beginning of the source file JSetL must be a sub folder of the folder in which the classes that import JSetL are saved Otherwise the path from root to the library folder must be added to the variable CLASSPATH Credits The first implementation of JSetL was carried out by Elisabetta Poleo during her Laurea Thesis in 2002 under the supervision of Gianfranco Rossi The library code was subsequently fixed by Elio Panegai and Gianfranco Rossi From that moment on several students un der the supervision of Gianfranco Rossi have helped to improve the library adding new functionalities and enhancing the existing ones in chronological order Nadia Toledi Delia Di Giorgio Roberto Amadini Daniele Pandini Michele Giacomo Filippi Luca Pedrelli Al berto Dalla Valle Lucia Guglielmetti More recently Federico Bergenti and Luca Chiarabini joined the JSetL Team at the Department of Mathematics In the last year Roberto Ama dini was deeply involved in the design and implementation of part of the JSetL constraint solver Currently the students Andrea Longo and Fabio Biselli are still working on JSetL as part of their Laurea Thesis We thank very much all of them
28. P with Sets In PPDP 03 Proc of the Fifth ACM SIGPLAN Conference on 4 A Dovier E Pontelli and G Rossi Set unification Theory and Practice of Logic 5 C Gervet Interval Propagation to Reason about Sets Definition and Implementation 6 J Jaffar and M J Maher Constraint Logic Programming A Survey Journal of Logic The following classes represent three different finite domains intervals multi intervals and set intervals Their primary purpose is to model the domain of integer and integer set logical variables see Sections 5 and 6 36 A 1 The class Interval Given two integers a b Z the integer interval bounded by a and b is the set of integers lab Y re Zia lt a lt b a is the GLB Greatest Lower Bound while b is the LUB Least Upper Bound of the interval Fixed an integer constant a gt 0 we first define an universe Zo a a and then the set I of all the intervals contained in Za that is Ia Y a b a b e Za The class Interval allows to represent and manipulate the intervals a b Ia First of all note that Za is defined by e a Interval sup Y Integer MAX_VALUE 2 1073741823 e a Interval INF ees Interval SUP 1073741823 In addition to static fields INF and SUP this class also provides the static method universe which returns an Interval corresponding to the universe Za Constructors Before introducing class constructors it is worth noting that in
29. aint methods in other classes o a 29 8 Constraint solving the class SolverClass 29 8 1 Posting and inspecting constraints o e 30 8 2 Checking constraint satisfiability o 31 8 3 Getting solutions A fee ae a a a anda li ia 31 9 User defined constraints 9 1 The class NewConstraintsClass 0 0000 2c eee 9 2 Implementing new constraints 2 0 0 e 002000004 9 3 Exploiting nondeterminism 00 00 0000 0000 4 References A Data structures for finite domain modeling Al The class Interval a a c paso ae annie db amin e A A a a od i A 2 The class MultiInterval 1 0 a A 3 The class SetInterval 2 2 ee B Data structures for dealing with labeling B 1 Labeling on integer logical variables o o B 2 Labeling on integer set logical variables 0 0008 iii 32 32 33 35 36 1 Introduction JSetL is a Java library that combines the object oriented programming paradigm of Java with valuable concepts of CLP languages 6 such as logical variables lists possibly partially specified unification constraint solving nondeterminism The library provides also sets and set constraints like those found in CLP SET 1 Unification may involve logical variables as well as list and set objects set unification Constraints concern basic set theoretical operations e g membership union intersection
30. al INF 2 0 a 2 0 NZa a 0 IntLVar v new IntLVar Multilnterval INF 2 0 Note that when the multi interval is actually an interval we use the more standard notation with the square brackets to represent it Interval SUP respectively then the latter can either be used in place of the former 16 e Raise NotValidDomainException since MultiInterval SUP 1 a 1 N Za D IntLVar v new IntLVar MultiInterval SUP 1 5 2 General utility methods The class IntLVar provides all utility methods of the class LVar see Section 2 2 suitably adapted to IntLVar and Integer objects along with a few other methods that take into account the presence of domains and arithmetic constraints boolean equals LVar lv Returns true iff this and 1v are equal logical variables and they have equal domain and associated integer arithmetic constraint Constraint getConstraint Returns the conjunction of constraints associated with this integer logical variable MultiInterval getDomain Returns the multi interval representing the domain associated with this integer logical variable void output Like output of LVar but if the variable is unbound also information about the domain and the arithmetic constraint associated with this variable are printed 5 3 Integer logical expressions IntLVar objects can be created also by using the integer arithmetic operation methods sum sub mul and div These
31. and its heuristics see Appendix B In this section we will only list the methods that the class IntLVar provides to support labeling Constraint label Constraint label ValHeuristic val Label this variable using the default value choice heuristic GLB resp using the value choice heuristic val static Constraint label AbstractList lt IntLVar gt vars static Constraint label IntLVar vars Label the variables in vars using the default value and variable choice heuristics GLB and LEFTMOST respectively static Constraint label AbstractList lt IntLVar gt vars LabelingOptions lop static Constraint label IntLVar vars LabelingOptions lop Label the variables in vars using the heuristics specified in lop Note that all these methods return an object of class Constraint since the labeling requests on one or more variables are treated as particular kinds of constraints over them 6 Integer set logical variables the class SetLVar Integer set logical variables or more briefly set variables are a special case of the logical variables described in Section 2 in which values are restricted to be set of integers Like integer logical variables a set variable has a finite domain and a possibly empty constraint associated with it Moreover each set variable has an associated integer logical variable which represents its cardinality The domain is represented as a set interval that is a lattice of integer sets see Section A 3 f
32. ated and it is automatically updated when the constraints possibly posted on v are solved in order to maintain constraint consistency For example if x and y are integer logical variables both with domain 1 10 and we add the constraint x gt y then the domain of x is updated to 2 10 and the domain of y to 1 9 When the domain of a variable is restricted to a single value k i e it is a singleton k the variable becomes bound to this value Conversely if the domain is reduced to the empty set it means that the constraints involving that variable are not satisfiable The arithmetic constraints associated with integer logical variables are generated by eval uating integer logical expressions i e expressions built using the usual arithmetic operators sum sub mul and div applied to integer logical variables and integer constants Evaluating an integer logical expression e yields a new integer logical variable X with an associated constraint X1 A Xo 92 Asa Xn tn where ej en are the subexpressions occurring in e and Xj Xn are internal integer logical variables that represents a flattened form of the expression e For example if e is the integer logical expression x sum y sub 1 where x and y are integer logical variables the evaluation of e returns the integer logical variable X with the associated constraint X x X2 A X2 y 1l In JSetL an integer logical variable is an instance of the clas
33. c constraints over logical variables namely equality and inequality membership and not membership The class LVar has a number of subclasses that deal with specific values of specific types A primary distinction is between atomic and structured values The variables which can assume atomic values are the integer logical variables class IntLVar see Section 5 and the integer set logical variables class SetLVar see Section 6 whose values are integer numbers and set of integers respectively Conversely the variables which can assume structured values are the set logical variables and list logical variables classes LSet and LList see Sections 4 and 3 whose values are respectively possibly partially specified sets and lists of elements of any type 2 1 Constructors LVar LVar String extName Create an unbound logical variable with no external name resp with external name extName If extName is omitted a default external name is assigned to the variable automatically LVar Object 0 LVar String extName Object o Create a bound logical variable with no external name resp with external name extName with value o o can be of any type but a String in the case of the one parameter constructor in fact in a such case the LVar String extName constructor would be called Same as to create an unbound logical variable x and to post and solve the constraint x eq o LVar LVar lv LVar String extName LVar lv
34. c2 c else throw new NotDefConstraintException private void c1 Constraint c t1 x t1 c getArg 1 t2 y t2 c getArg 2 implementation of constraint c1 over objects x and y return private void c2 Constraint c t3 x t3 c getArg 1 implementation of constraint c2 over object x return J The one argument constructor of the class ListOps initializes the field Solver in the super class NewConstraintsClass with a reference to the solver currently in use by the user program 33 The other public methods simply construct and return new objects of class Constraint Each different constraint is identified by a string name which is specified as a parameter of the constraint constructor The method user_code which is defined as abstract in NewConstraintsClass imple ments a router that associates each constraint name with the corresponding user defined constraint method It will be called by the solver during constraint solving Finally the private methods provide the implementation of the new constraints These methods must first of all retrieve the constraint arguments whose number and type depend on the constraint itself The following is an example of the definition of a class derived from NewConstraintsClass that implements among others a new constraint absTest absTest x y where x and y are IntLVar is true if x is bound and y x if x is unbound the constraint is simply left unchanged
35. cular list values i e the elems part of the l list are instances of the class ArrayList which implements the java util List interface The class LList provides methods to create new l lists possibly starting from existing ones to deal with 1 lists as logical variables and to deal with values possibly bound to lists Moreover like logical variables Lists can be used to post constraints that implement basic list operations 3 1 Constructors LList LList String extName Create an unbound Llist with no external name resp with external name extName LList List lt gt 1 LList String extName List lt gt 1 Create a bound 1 list with no external name resp with external name extName with value 1 Same as to create an unbound l list x and to post and solve the constraint x eq 1 LList LList 11 LList String extName LList 11 Create a Llist with no external name resp with external name extName equivalent to the l list 11 Same as to create an unbound l list x and to post and solve the constraint x eq 11 Example 3 e Create an unbound l list a LList a new LList e Create a l list b with external name b bound to the list value 1 2 3 List 1 new ArrayList l add 1 l add 2 l add 3 LList b new LList b 1 e Create a l list c equivalent to the l list a LList c new LList a 3 2 Creating new bound 1 lists static LList empty Returns the empty Llist LList i
36. domain constraint Xo s Constraint ndom Integer a Integer b Constraint ndom MultiInterval m Same as the dom methods except that these methods constrain this logical variable to not belong to the domain a b resp to the multi interval m Membership constraints Membership constraints involve integer logical variables and integer set logical variables see Section 6 Constraint in SetLVar X Constraint in Multilnterval A Return the constraint this X resp the constraint this A Constraint nin SetLVar X Constraint nin Multilnterval A Return the constraint this X resp the constraint this A 19 All different constraints Given n gt 0 integer logical variables v1 U the constraint allDifferent v1 Un is logically equivalent to the constraint c A vi A vj 1 lt i lt j lt mn The class IntLVar has two static methods called allDifferent which take as input a collection of integer logical variables and return such a constraint static Constraint allDifferent AbstractList lt IntLVar gt vars static Constraint allDifferent IntLVar vars Return the constraint A lt vi vj if vars is an AbstractList resp a Java array of IntLVar v1 al Labeling constraints Given n gt 0 integer logical variables v1 0n labeling them means try to assign to each variable an integer value belonging to its domain For a more formal and comprehensive explanation of labeling
37. e extName and value k The domain of this variable is k and the associated constraint is the empty conjunction IntLVar IntLVar v IntLVar String extName IntLVar v Create an integer logical variable with no external name resp with external name extName equivalent to the logical variable v The domain and the constraint of this variable are the domain and the constraint of the variable v IntLVar Integer a Integer b IntLVar String extName Integer a Integer b Create an unbound integer logical variable with no external name resp with ex ternal name extName and with domain the multi interval a b The associated constraint is the empty conjunction llo IntLVar Multilnterval m IntLVar String extName Multilnterval m Create an integer logical variable with no external name resp with external name extName and with domain the multi interval m The associated constraint is the empty conjunction All such constructors may raise the exception NotValidDomainException if the do main of the logical variable is empty In this way we anticipate a certain failure when trying to solve a constraint involving that variable Example 6 e Create an integer logical variable v with domain 1 1 3 MultiInterval m new MultiInterval m add 1 m add 1 m add 2 m add 3 IntLVar v new IntLVar m e Create an integer logical variable v with domain MultiInterval INF 0 since MultiInterv
38. e as above but with replaced by in the generated constraint Constraint le Integer k Constraint le IntLVar v Same as above but with replaced by lt in the generated constraint 18 Constraint lt Integer k Constraint lt IntLVar v Same as above but with replaced by lt in the generated constraint Constraint ge Integer k Constraint ge IntLVar v Same as above but with replaced by gt in the generated constraint Constraint gt Integer k Constraint gt IntLVar v Same as above but with replaced by gt in the generated constraint Example 8 e The method invocation x sub 1 1t y sum 3 where x and y are unbound logical variables with external names x and y respec tively returns the constraint lt _ _x 1 _ _y 3 where the two in the lt constraint represent the internal names of the IntLVar objects created in correspondence with the subexpressions x sub 1 and y sum 3 respectively Domain handling constraints Constraint dom Integer a Integer b Returns the constraint Xo a b A Co where Xo is this logical variable and Co is its associated constraint The domain constraint Xo a b constrains Xo to belong to the domain a b If such domain is empty the exception NotValidDomainException is raised lle Constraint dom MultiInterval m Same as above but with domain constraint Xo m Constraint dom Set lt Integer gt s Same as above but with
39. egative and another one in which x is assumed to be negative the new version of the absolute value constraint is simply called abs Example 15 New constraint abs private void abs Constraint c throws Failure IntLVar x IntLVar c getArg 1 IntLVar y IntLVar c getArg 2 35 switch c getAlternative case 0 x gt 0 andx y Solver addChoicePoint c Solver add x ge 0 and x eq y break case 1 x lt 0andx 0 y Solver add x lt 0 and x eq new IntLVar 0 sub y return J A sample usage of the new constraint abs is IntLVar x new IntLVar x IntLVar y new IntLVar y 3 solver check mathOps abs x y x output solver nextSolution x output whose execution generates the output x 3 x 3 References 1 A Dovier C Piazza E Pontelli and G Rossi Sets and constraint logic programming ACM TOPLAS 22 5 861 931 2000 2 A Dovier C Piazza and G Rossi A uniform approach to constraint solving for lists multisets compact lists and sets ACM Transactions on Computational Logic 9 3 1 30 2008 Principles and Practice of Declarative Programming ACM Press 219 229 2003 Programming 6 645 701 2006 of a Practical Language Constraints 1 3 191 244 1997 Programming 19 20 503 581 1994 A Data structures for finite domain modeling 3 A Dal Pal A Dovier E Pontelli and G Rossi Integrating Finite Domain Constraints and CL
40. erations which do not over approximate the result have a public interface boolean subset Interval I Returns true iff this C I Interval intersect Interval I Returns the interval corresponding to this MI Interval sum Interval I Returns the interval corresponding to this I where in general a b c d f Ila b dilla Interval sub Interval I Returns the interval corresponding to this I where in general a b e d E la d b dll Interval opposite O Returns the interval corresponding to Othis def 0 this Other utility methods boolean contains Integer k Returns true iff k this boolean isEmpty Returns true iff this 9 boolean isSingleton Returns true iff this 1 38 boolean isUniverse Returns true iff this Za int size Returns this Integer getGlb Returns the GLB of this if this null otherwise Integer getLub Returns the LUB of this if this null otherwise TreeSet lt Integer gt toSet Returns a java util TreeSet containing all the elements of this Iterator lt Integer gt iterator Returns an iterator over the elements of this in ascending order Interval clone Returns a copy of this Interval equals Object obj Returns true iff this is equals to obj String toString Returns a string representation of this A 2 The class MultiInterval A multi interval of integers is a set of integers M C Z def
41. ere k is the number of arguments of this constraint 28 7 3 Meta constraints Constraint and Constraint c Returns the constraint this A c Constraint impliesTest Constraint c Returns the constraint this c where is the logical implication Constraint notTest Returns the constraint this where is the logical negation Constraint or Constraint c Constraint orTest Constraint c Return the constraint this V c The difference between or and orTest is that the latter is just a test over two ground i e completely specified constraints and it is simply left unchanged by the solver if either c or this are not ground conversely the former is always evaluated even if c or this are not ground using backtracking to try the second constraint if the first fails As an example the constraint x eq 1 orTest x eq 2 and x neq 1 and x neq 2 where x is an unbound logical variable is simply left unchanged when the solver tries to solve it whereas the logically equivalent constraint x eq 1 or x eq 2 and x neq 1 and x neq 2 is found to be unsatisfiable by the solver Similar considerations apply to constraints notTest and impliesTest 7 4 Constraint methods in other classes Constraints are generated also by a number of methods provided by classes implementing logical variables and logical collections Specifically e constraints over LVar objects see Sect 2 3 e constraints over LList objects
42. erent elements of s 4 4 Constraint methods The class LSet provides methods for generating constraints over sets i e l set constraints that implement most of the usual set theoretical operations Comparison constraints Constraint eq LSet 1s Returns the atomic constraint this 1s that unifies this l set with the lset 1s If this l set is unbound and 1s is bound to a set s this l set becomes bound to s after the constraint has been solved conversely if 1s is unbound this l set remains unbound Note that solving this constraint causes the unbound variables possibly occurring in 1s to be bound to the proper values as required by set unification see e g 4 Constraint eq Set lt gt s Returns the atomic constraint this s that unifies this l set with the set s If this l set is unbound it becomes bound to s after the constraint has been solved Constraint neq LSet 1s Constraint neq Set lt gt s Return the atomic constraint this s that requires this l set to be different from the l set 1s resp from the set s Membership constraints Constraint contains LVar lv Constraint contains Object o Return the atomic constraint 1v this resp o this that requires this l set to contain the logical variable 1v resp the object o Same as 1v in this resp new LVar o in this see Sect 2 3 13 Constraint ncontains LVar lv Constraint ncontains Object o Return the atomic constraint 1v thi
43. he logical variable v The constraint v X corresponds to the set disjointness between v and X thus their intersection must be empty SetLVar intersect MultiInterval m Returns this intersect new SetLVar m SetLVar intersect SetLVar v Returns an integer set logical variable Xi with an associated constraint X Xo NVA Xi CXo A X1 Cv A Co A Cy where Xo is this logical variable Co is its associated constraint and C is the constraint associated with the logical variable v static SetLVar singleton IntLVar v Returns an integer set logical variable X such that X v SetLVar union MultiInterval m Returns this union new SetLVar m SetLVar union SetLVar v Returns an integer set logical variable Xi with an associated constraint X Xo Uva Xo C Xi A ve Xi N X lt Xo lv A Co A Co where Xo is this logical variable Co its associated constraint and C is the constraint associated with the logical variable v Example 10 e Create an integer set logical variable with an associated set complement constraint SetLVar x new SetLVar x SetLVar y x compl setName y y output Output y _ Domain 536870911 536870911 Size 0 1073741823 Constraint _ compl _x where _ represents the internal name of the SetLVar object created in correspondence with the subexpression x compl O 6 4 Constraint methods The class SetLVar provides methods for generating the usual set theoretic co
44. his integer set logical variable void output Like output of LVar but if the variable is unbound also information about the domain the cardinality and the arithmetic constraint associated with this variable are printed Moreover SetLVar provides a method to compute the cardinality of the set possibly bound to a set variable Since this method returns an integer logical variable it can be used within integer logical expressions and to post IntLVar constraints IntLVar card Returns an integer logical variable which represents the cardinality of this 6 3 Integer set expressions SetLVar objects can be created also by using the integer set operation methods compl intersect union diff and singleton These methods are invoked on SetLVar objects and returns SetLVar objects hence they can be concatenated to form compound set expres sions SetLVar compl Returns an integer set logical variable Xy with an associated constraint Xi Xo A Xo X1 Zg A Co where Xo is this logical variable is the set complementation with respect to the universe Zg and Co is the constraint associated 23 SetLVar diff MultiInterval m Returns this diff new SetLVar m SetLVar diff SetLVar v Returns an integer set logical variable Xy with an associated constraint X Xo v A X C Xo A v X A X gt Xo lv A Co A Cy where Xo is this logical variable Co its associated constraint and C is the constraint associated with t
45. implementing user defined operations Once objects of the new class have been created one can use the user defined constraints contained in it as the built in ones user defined constraints can be added to the constraint store using the method add and solved using the SolverClass methods for constraint solv ing For example the statements 32 MyOps myOps new MyOps solver solver solve my0ps c1 01 02 create an object of type MyOps called myOps and use it to invoke and solve the constraint c1 over two objects 01 and 02 using the constraint solver solver provided c1 is one of ther constraint defined in MyOps 9 2 Implementing new constraints The actual implementation of the class that extends the JSetL abstract class NewConstraintsClass requires some programming conventions to be respected The following example shows the implementation of the class MyOps which offers two new constraints c1 01 02 and c2 03 where 01 02 03 are objects of type t1 t2 and t3 respectively Example 13 Implementing new constraints public class MyOps extends NewConstraintsClass public MyOps SolverClass currentSolver super currentSolver public Constraint ci t1 o1 t2 02 return new Constraint c1 o1 02 public Constraint c2 t3 03 return new Constraint c2 03 protected void user_code Constraint c throws Failure NotDefConstraintException if c getName c1 ci c else if c getName c2
46. ined by n gt 0 intervals I Ig In Ia such that i M LULRU UL ii E X Ig lt In where a b lt c d EE hice The set of all the multi intervals M C Za will be named Ma Example 17 Examples of multi intervals are eM 9 e M 1 10 e M 3 0 U 5 5 U 15 30 For multi intervals defined by n gt 1 intervals we will use a simpler notation where intervals are simply listed in curly brackets and singleton intervals of the form k k are replaced by k For example the last multi interval of the above example can be written as 3 0 5 15 30 It is important to observe that Ma P Za in other terms every subset of Za is uniquely identified by a multi interval in Ma and viceversa 39 The class MultiInterval allows to represent and manipulate all the multi intervals M Ma Note that although an interval is a particular case of multi interval is trivial to prove that I C Ma MultiInterval is not a super class of Interval Moreover this class implements the Java interface Set lt Integer gt for this reason all the methods of Set and its super interfaces Collection and Iterable must be implemented for more details see Java APIs specification Finally like class Interval MultiInterval has static fields INF and SUP which repre sent a and a respectively and a static method universe which returns the universe Lo Constructors MultiInterval Creates the empty m
47. ist of three new unbound logical variables X_1 X_2 X_3 LList i LList mkList 3 3 3 General utility methods The class LList provides the utility methods of the class LVar see Section 2 2 along with a few other methods that take into account the fact that values possibly bound to LList objects are collections namely lists possibly containing other logical variables and collections 3 3 1 Basic methods The following methods are the same as LVar s methods but adapted to l list objects LList clone boolean equals LList 1 boolean equals Object o String getName List lt gt getValue boolean isBound O void output LList setName String extName String toString Remarks e equals and getValue consider only the list value of the given list i e they ignore its rest part In particular getValue returns the elems list of the given Mist In order to obtain also its rest part one must use the getRest method see 3 3 2 e Ifthe l list denotes an open list the string returned by toString is e_1 en _r where e_1 e_n are the strings obtained from the list elements and _r is the external name of the unbound list denoting the rest part of the list Similarly the output produced by the method output is 1 e1 en r where 1 is the external name of the list 3 3 2 Logical collection methods The following methods take into account the fact that the value of a b
48. ix B In this section we will only list the methods that the class SetLVar provides to support labeling Constraint label Constraint label ValHeuristic val Label this variable using the default value choice heuristic GLB resp using the value choice heuristic val and the default set heuristic FIRST_NIN static Constraint label AbstractList lt SetLVar gt vars static Constraint label SetLVar vars Label the variables in vars using the default heuristics GLB LEFT_MOST and FIRST_NIN static Constraint label AbstractList lt SetLVar gt vars LabelingOptions lop static Constraint label SetLVar vars LabelingOptions lop Label the variables in vars using the heuristics specified in lop Note that as for class IntLVar all these methods return an object of class Constraint since the labeling requests on one or more variables are treated as particular kinds of con straints over them Partially specified integer sets The class SetLVar allows to define partially specified integer sets according to the CLP SET approach Specifically if X1 Xn are integer logical variables n gt 0 and S and R are integer set logical variables then we can define and solve constraints of the form S X Xn R Xi U U X PUR The following methods allow the user to define this kind of constraints Constraint eq IntLVar x Returns the constraint Xo x A Co where Xo is this logical variable and C is its associated constraint
49. main the set interval a b The associated constraint is the empty conjunction SetLVar Set lt Integer gt s Set lt Integer gt t SetLVar String extName Set lt Integer gt s Set lt Integer gt t Create an unbound integer set logical variable with no external name resp with external name extName and with domain the set interval s t The associated constraint is the empty conjunction SetLVar SetInterval s SetLVar String extName SetInterval s Create an integer set logical variable with no external name resp with external name extName and with domain the set interval s The associated constraint is the empty conjunction SetLVar SetInterval s Integer k SetLVar String extName SetInterval s Integer k Create an integer set logical variable with no external name resp with external name extName with domain the set interval s and cardinality k The associated constraint is the empty conjunction SetLVar SetInterval s MultiInterval m SetLVar String extName SetInterval s MultiInterval m Create an integer set logical variable with no external name resp with external name extName with domain the set interval s and cardinality variable domain m The associated constraint is the empty conjunction Note that like integer logical variables such constructors may raise the exception NotValidDomainException if the domain of the set variable is empty Moreover observe that some constructors all
50. ns Object 0 If this l list is bound returns the new 1 list whose value is obtained by adding o as the first element of the list bound to this variable Otherwise i e this l list is unbound it returns the new 1 list whose value is the list containing o as its first element and this Llist as the rest part i e o 1 where 1 is this Mist LList insn Object o Like ins but o is added as the last element of the list bound to this variable LList insAll Object c LList insAll Collection c If this 1 list is bound return the new 1 list whose value is obtained by adding all elements of c as the head elements of the list bound to this l list respecting the order they have in c Otherwise returns the new l list whose value is the list containing all elements in c and this 1 list as its rest part i e a1 an 1 where a an are the elements of c and 1 is this Mist static LList mkList int n static LList mkList String extName int n Returns a l list with no external name resp with external name extName whose value is a list of n unbound logical variables Remarks e The ins insn and insAll methods do not modify the object on which they are invoked rather they build and return a new l list obtained by adding the elements to the given list Hence list insertion methods can be concatenated left associative e Elements to be added to the list value through the ins insn and insA11 methods can be of any
51. nstraint and e 0 lt i lt 3 are expressions whose type depends on op In particular op can be one of a collection of predefined meth ods that implement operations such as equality inequality integer comparison as well as basic set theoretic operations e g membership union intersection etc e compound constraints c and c2 conjunction c or c2 disjunction cy orTest c2 disjunction c impliesTest c2 implication where c and cz are JSetL constraints and and or orTest impliesTest represent the logical conjunction c1 A c2 disjunction ci V c2 and implication c c2 between c and c2 respectively e negation constraint c notTest negation where c is a JSetL constraint and notTest represents the negation of ci 21 Constraints in JSetL are defined as instances of the class Constraint Constraint objects are created by using constructors and other methods of the class Constraint e g and or as well as the result of calling a number of constraint methods supplied by the classes implementing logical objects presented in the previous sections 27 7 1 Constructors Constraint Creates the empty constraint default name no name Constraint String extName Object o1 Constraint String extName Object oi Object 02 Constraint String extName Object oi Object 02 Object 03 Constraint String extName Object 01 Object 02 Object 03 Object 04
52. nstraints More over it allows to deal with set domains labeling and partially specified sets Integer set constraints Constraint disj MultiInterval m Returns the constraint Xo m A Co where Xo is this logical variable Co is its associated constraint and is the set disjointness 24 Constraint disj SetLVar v Returns the constraint Xo v A Xo v lt Zg A Co A Cu where Xo is this logical variable Co is its associated constraint and C is the constraint associated with the logical variable v Constraint eq Multilnterval m Returns the constraint Xy m A Co where Xo is this logical variable and Co is its associated constraint Constraint eq SetLVar v Returns the constraint Xy v A Xo v A Co A Cy where Xo is this logical variable Co is its associated constraint and C is the constraint associated with the logical variable v Constraint neq Multilnterval m Returns the constraint Xo 4m A Co where Xy is this logical variable and Cp is its associated constraint Constraint neq SetLVar v Returns the constraint Xy 4v A Co A Cy where Xo is this logical variable Co is its associated constraint and C is the constraint associated with the logical variable v Constraint strictSubset Multilnterval m Returns the constraint Xy Cm A Xo lt m A Co where Xo is this logical variable and Co is its associated constraint Constraint strictSubset SetLVar v Returns the constraint Xy C v A Xo lt lv A Co A
53. nt C A c satisfiable If C A c is unsatisfiable it returns the empty LSet In all cases all unbound variables in C A c remain unchanged boolean setof LVar x Same as setof x c in which c is the empty constraint Example 12 e Print all solutions LVar x new LVar x LSet s LSet empty ins 3 ins 2 ins 1 setName s solver solve x in s do x output 31 while solver nextSolution System out println No more solutions Executing this code will output x 1 x 2 x 3 No more solutions e Collect all solutions LVar x new LVar x LSet s LSet empty ins 3 ins 2 ins 1 setName s LSet r solver setof x x in s r output Executing this code will output r 1 2 3 e No solutions LVar x new LVar x LSet s LSet empty ins 2 ins 1 setName s solver add x neq 1 and x neq 2 LSet r solver setof x x in s r output Executing this code will output r 9 User defined constraints JSetL allows the user to define new possibly nondeterministic constraints and to deal with them as the built in constraints 9 1 The class NewConstraintsClass User defined constraints are defined as part of a user class that extends the JSetL abstract class NewConstraintsClass For example public class MyOps extends NewConstraintsClass public and private methods implementing new constraints is intended to define a collection of new constraints
54. onstructors SettLVar SetLVar String extName Create an unbound integer set logical variable with no external name resp with external name extName The domain of this variable is the universe set interval SetInterval INF SetInterval SUP which corresponds to the maximum repre sentable set interval The constraint associated with this variable is the empty con junction SetLVar MultiInterval m SetLVar String extName Multilnterval m Create an integer set logical variable with no external name resp with external name extName and value m The domain of this variable is m and the associated constraint is the empty conjunction 21 SetLVar Set lt Integer gt s SetLVar String extName Set lt Integer gt s Create an integer set logical variable with no external name resp with external name extName and value s The domain of this variable is s and the associated constraint is the empty conjunction SetLVar SetLVar 1 SetLVar String extName SetLVar 1 Create an integer set logical variable with no external name resp with external name extName equivalent to the set variable 1 The domain and the constraint of this variable are the domain and the constraint of the variable 1 SetLVar MultiInterval a MultiInterval b SetLVar String extName MultiInterval a MultiInterval b Create an unbound integer set logical variable with no external name resp with external name extName and with do
55. or a precise description of set intervals in JSetL A domain for a set variable s can be specified when the variable s is created and it is automatically updated when the constraints possibly posted on s are solved in order to 20 maintain constraint consistency For example if X is a set variable with domain 1 2 3 and we add the cardinality constraint X 3 then the domain of X will be restricted to the singleton 1 2 3 because the only set belonging to the domain of X which has cardinality 3 is precisely 1 2 3 Note that when the domain of a variable is restricted to a singleton A the variable becomes bound to this value Conversely if the domain is reduced to the empty set it means that the constraints involving that variable are not satisfiable Moreover when the domain of a set variable is specified or updated the domain of its cardinality variable is updated accordingly if the domain of a set variable is the set interval A B then the domain of its cardinality will be 4 B The constraints associated with set variables are generated by evaluating integer set expressions i e expressions built using the usual set operations union intersection differ ence complementation cardinality applied to set variables and integer set constants Moreover when a set constraint is posted it is possible that other constraints inferable from it are added to the store For example when the constraint X C Y is pos
56. ound logical list is a collection possibly partially specified i e containing unknown elements and that a logical list may have a rest part The first group of methods are specific of the class LList while the second group is common to all collections in particular to List objects Object get int i If this Llist is bound returns the i th element of its list value Otherwise it raises an exception NotInitVarException LList getRest If this Llist is bound to a not empty list returns its rest part that is either an unbound Llist if this 1 list is open or the empty list if this l list is closed Returns null if this Hist is the empty Mist the variable itself if this 1 list is unbound boolean isClosed If this list is bound returns true if it has an empty rest part false otherwise i e if it denotes an open list Raises an exception NotInitVarException if this l list is unbound boolean isEmpty If this l list is bound returns true if it is the empty llist Raises an exception NotInitVarException if this list is unbound 1All exceptions defined in JSETL are extensions of the class java lang Exception boolean isGround If this l list is bound returns true if its value is ground that is it does not contain any unbound logical variable or collection Raises an exception NotInitVarException if this 1 list is unbound void printElems char sep If this l list is bound prints all elements of its list value separated
57. ow set variables domain to be defined by using generic implemen tation of Set lt Integer gt interface which can be different from the class MultiInterval Example 9 e Create a SetLVar with domain 2 1 3 Multilnterval a new Multilnterval Multilnterval b new Multilnterval 1 3 SetLVar x new SetLVar a b 22 e Create a SetLVar with domain 0 1 and cardinality 1 in fact CHa O 1 2 8 1 minc S Sg 0 1 E S 0 1 MultiInterval m new MultiInterval 2 SetInterval SUP getLub 1 MultiInterval m0 new MultiInterval 0 MultiInterval mi new MultiInterval 1 Vector lt MultiInterval gt v new Vector lt MultiInterval gt v add m v add m0 v add m1 SetInterval s new SetInterval v SetLVar x new SetLVar s 1 e Raise NotValidDomainException since 2 8 1 g 2 8 1 NP Zs MultiInterval m new MultiInterval 2 SetInterval SUP getLub 1 SetLVar x new SetLVar m 6 2 General utility methods The class SetLVar provides all utility methods of the class LVar see Section 2 2 suitably adapted to SetLVar and MultiInterval objects along with a few other methods that take into account the presence of domains and set constraints Constraint getConstraint Returns the conjunction of constraints associated with this integer set logical variable SetInterval getDomain Returns the set interval representing the domain associated with t
58. quired by the unification of the two lists Constraint eq List lt gt 1 Returns the atomic constraint this 1 that unifies this l list with the generic Java list 1 If this Llist is unbound it becomes bound to 1 after the constraint has been solved Constraint neq LList 11 Constraint neq List lt gt 1 Return the atomic constraint this 11 that requires this l list to be different from the List 11 resp from the generic Java list 1 Constraint allDiff If this l list is bound returns a conjunction of atomic constraints e 4 e for all elements e e i different from j of the list bound to this 1 list Raises an exception NotInitVarException if this 1 list is unbound The class LList provides also a method for generating a specified constraint for all elements of a list Constraint forallElems LVar y Constraint c If this ist is bound returns a conjunction of atomic constraints cy A C2 A A Cn for all elements e en of the list bound to this Llist Each c is obtained from c by replacing all occurrences of y in it with e For example if 1 is the list 1 2 z where z is an unbound logical variable 1 forallElems y y neq 0 generates a conjunction of constraints logically equivalent to 1 0A2 0Az 0 Raises an exception NotInitVarException if this list is unbound 4 Logical sets the class LSet A logical set s or simply a l set s is a special kind of logical variable whose value is a pair elems rest
59. riable Otherwise i e this l set is unbound it returns the new l set whose value is the set containing o as its element and this l set as the rest part i e o 1s where 1s is this l set 11 LSet insAll Object c LSet insAll Collection c If this l set is bound return the new l set whose value is obtained by adding all elements of c as elements of the set bound to this l set Otherwise return the new l set whose value is the set containing all elements in c and this l set as its rest part Le a1 an s where aj a are the elements of c and s is this l set static LSet mkSet int n static LSet mkSet String extName int n Returns a l set with no external name resp with external name extName whose value is a set of n unbound logical variables Note that since the order of elements in a set is not important it is not necessary to supply distinct methods for head and tail insertion because they would produce the same set All remarks and examples shown for 1 lists in Section 3 are still valid in the case of l sets provided LList is replaced by LSet and insn is replaced by ins 4 3 General utility methods The class LSet provides all the utility methods of classes LVar see Section 2 2 and LList see Section 3 3 4 3 1 Basic methods The following methods are the same as LVar s methods but adapted to l set objects LSet clone boolean equals LSet 1s boolean equals Object o
60. s null otherwise SetInterval intersect SetInterval S Returns the set interval this N S 43 SetInterval clone Returns a copy of this SetInterval equals Object obj Returns true iff this is equals to obj String toString Returns a string representation of this Particular attention should be paid to method size Indeed since a set interval may contain an exponential number of elements the Java scalar type double is used to represent its size However note that if a set interval is too big e g the universe Z the constant value Double POSITIVE_INFINITY is returned B Data structures for dealing with labeling As is usually the case with finite domain constraint solvers the JSetL constraint solver is not complete Specifically if the constraint store contains constraints over IntLVar and SetLVar objects the solver does not ensure that all the constraints belonging to it are satisfiable In order to check satisfiability and find one or all possible solution s suitable research strategies are therefore needed labeling is one of these Given n gt 0 logical variables v v labeling them means trying to assign to each variable a value belonging to its domain Obviously considering every possible labeling of all the variables of the constraint store we obtain completeness i e every possible value assignment to the variables is computed However the excessive simplicity of this method implies a not
61. s resp o this that requires this l set to not contain the logical variable 1v resp the object o Same as 1v nin this resp new LVar o nin this see Sect 2 3 Set theoretical constraints Constraint diff LSet 1s1 LSet 1s2 Constraint diff LSet 1s Set lt gt s Constraint diff Set lt gt s LSet 1s Constraint diff Set lt gt si Set lt gt s2 Return the atomic constraint this 1s1 182 resp this 1s s this s 1s this s1 s2 that requires this l set to be the difference of the other two l set resp set objects Constraint disj LSet 1s Constraint disj Set lt gt s Return the atomic constraint this 1s resp this s that requires this l set to be disjoint from the l set 1s resp from the set s i e this N 1s 0 this N o 9 Constraint inters LSet 1s1 LSet 1s2 Constraint inters LSet ls Set lt gt s Constraint inters Set lt gt s LSet ls Constraint inters Set lt gt s1 Set lt gt s2 Return the atomic constraint this 1s1 N 1s2 resp this 1s N s this s N 1s this s1 N s2 Constraint less LSet 1s LVar lv Constraint less LSet 1s Object o Constraint less Set lt gt s LVar lv Constraint less Set lt gt s Object 0 Return the atomic constraint this less 1s 1v resp this less 1s 0 this less s lv this less s o that requires this l set to be equal to the l set 1s resp to the set s without the object 1v resp o
62. s IntLVar which extends the class LVar Values of integer logical variables are integer numbers Unions of intervals used to represent variable domains are instances of the class MultiInterval see Section A 2 Constraints possibly associated with integer logical variables are instances of the class Constraint see Section 7 The class MultiInterval provides the static fields INF and SUP to represent respectively the minimum and maximum representable values for a multi interval As a notational con vention see Sections A 1 and A 2 we will denote these values a and a respectively and we will use Za ef a a to denote the universe multi interval which corresponds to the maximum representable multi interval Moreover if M is a multi interval the nota tion M will be used to indicate the normalization operation over M which is defined as M N Za 3Note that MultiInterval INF and MultiInterval SUP have the same value as Interval INF and 15 5 1 Constructors IntLVar IntLVar String extName Create an unbound integer logical variable with no external name resp with exter nal name extName The domain of this variable is the universe multi interval Za i e MultiInterval INF MultiInterval SUP The constraint associated with this variable is the empty conjunction IntLVar Integer k IntLVar String extName Integer k Create an integer logical variable with no external name resp with external nam
63. s domain Thus given n set variables X1 Xn to be labeled the following approach is used e a variable X X1 Xn is selected according to a certain variable choice heuristic e an integer value k B A where A B is the domain of X is selected according to a certain value choice heuristic Note that the integer set B A corresponds to all the integer values that could belong to X but they do not necessarily belong to it e the meta constraint k X Vk X is added to the store and solved Note that such logic disjunction is nondeterministic thus a choice must be made about which constraint will be solved first depending on the value of a certain set choice heuristic In this way the domain of a set variable is refined by adding values to its GLB or removing values from its LUB until the variable results possibly bound The enumeration SetHeuristic Variable and value choice heuristics are modelled by using the enumerations VarHeuristic and ValHeuristic respectively see Section B 1 To decide which non membership con straint will be solved first instead the enumeration SetHeuristic is used Such enum consists of the following fields FIRST_IN The membership constraint k X is solved first FIRST_NIN The non membership constraint k X is solved fist As for the integer logical variables the class LabelingOptions allows the labeling heuris tics to be setted up by properly setting its public
64. ship test Similarly elements of the list value associated with this I list can be logical objects and their values are taken into account if any An exception NotInitVarException is raised if this 1 list is unbound When the 1 list v is bound v testContains o is equivalent to either v getValue contains o getValue or v getValue contains o depending on whether o is a bound logical object e g a logical variable or not Observe that all these methods as well as most of the methods above take into account only the elems part i e the list value of the invocation 1 list while the rest part is simply ignored 3 4 Constraint methods The class LList provides methods for generating equality and inequality constraints over lists 2The current version of the JSetL library does not support constraints over lists other than list equal ity and inequality This limitation will be possibly removed in future releases by integrating other basic constraints over lists with set constraints as proposed for instance in 2 Constraint eq LList 11 Returns the atomic constraint this 11 that unifies this 1 list with the l list 11 If this 1 list is unbound and 11 is bound to a list 1 this list becomes bound to 1 after the constraint has been solved conversely if 11 is unbound this l list remains unbound Note that solving this constraint causes the unbound variables possibly occurring in 11 to be bound to the proper values as re
65. ss LList 5 3 1 Constructors Wa rt eae Mae eee el dele a 5 3 2 Creating new bound Lists o o e e ee 6 3 3 General utility methods o e e 7 dol Basic Methods Cartas ad ai a oa 8 3 3 2 Logical collection methods o o 8 did Constraint methods p iu i eee e a de da ve ee ew Ad 9 4 Logical sets the class LSet 10 Ault Onstructors y ori A A ae eee be 11 4 2 Creating new bound sets 2 2 2 0 0 2 00002000 11 4 3 General utility methods 0 00 0 0 0 0 0000008 12 43 1 Basic methods esoo pane S HAA e EE hee ES OS 12 4 3 2 Logical collection methods o e 12 4 4 Constraint methods 13 5 Integer logical variables the class IntLVar 15 Dil Constructors sa e me A E e eee ea eae Baek SG 16 5 2 General utility methods o ee eee 17 5 3 Integer logical expressions LL 17 bid Constraint methods ana a direi te LE a A 18 6 Integer set logical variables the class SetLVar 20 Gl CONstructofs n e p Gui n a Gee ra A tan 21 6 2 General utility methods o 23 6 3 Integer set expressions a 23 6 4 Constraint methods 24 7 Constraints the class Constraint 27 Wolk C ONStructors e fit A i Soro Net tes Sas ae at ae eh 28 7 2 General utility methods o 2 ee 28 iS Meta CONStralMts lt a rete dine le le a a AS 29 7 4 Constr
66. ted also the constraint X lt Y is added to the store since X C Y implies that the cardinality of X is less than or equal to the cardinality of Y In JSetL an integer set logical variable is an instance of the class SetLVar which extends the class LVar Values of such variables are set of integers modeled by objects of class MultiInterval see Section A 2 Set intervals used to represent set variable domains are instances of the class SetInterval see Section A 3 The cardinality variable associated to a set variable is an instance of the class IntLVar see Section 5 Constraints possibly associated with integer set logical variables are instances of the class Constraint see Section 7 The class SetInterval provides two static fields INF and SUP to represent respec tively the minimum and maximum representable values for set intervals In practice INF is the empty multi interval while SUP is fixed to be the multi interval Interval SUP 2 Interval SUP 2 As a notational convention see Section A 3 we will use 8 to denote the value of the bounds of the maximum multi interval currently fixed to be Interval SUP 2 and we will use Zg ai 6 8 to represent such multi interval More over if D is a set interval D 3 will be used to indicate the normalization operation over D which is defined as D N P Zg while CHg is used to denote the convex closure operation which is defined as minc S Sg D g Sy 6 1 C
67. tervals defined in this way have two main restrictions Indeed they are e finite VIel VWxel a lt x lt a e conver VI Ia Y x y I x y CI Therefore to overcome these limitations two special operations are needed in order to represent generic integer sets as intervals belonging to Ia e normalization is an operation P Z P Za such that for each A C Z d All E A A Zo e convex closure is an operation CH P Z Ia such that for each A C Z CHA mince I Ia All CI Hence the class constructors are defined as follows Interval Creates the empty interval Interval Integer a Creates the interval a Interval Integer a Integer b Creates the interval a b Interval Set lt Integer gt s Creates the interval CH s 37 Example 16 Interval constructors e Create an empty interval since Interval SUP 1 a 1 N Za Interval i new Interval Interval SUP 1 e Create the interval Interval INF 2 0 2 0 A Za a 0 Interval i new Interval Interval INF 2 0 e Create the interval CH 3 1 0 5 3 5 HashSet lt Integer gt set new HashSet lt Integer gt set add 3 set add 1 set add 0 set add 5 Interval i new Interval set Set Operations Since intervals are sets of integers it is possible to define set operations on them However note that only those op
68. the class LList but applied to LSet objects In particular it provides methods to create new l sets possibly starting from existing ones to deal with l sets as logical variables and to deal with values possibly bound to l sets Moreover l sets can be used to post constraints that implement most of the usual set operations 4 1 Constructors LSet LSet String extName Create an unbound l set with no external name resp with external name extName LSet Set lt gt s LSet String extName Set lt gt s Create a bound l set with no external name resp with external name extName with value s Same as to create an unbound l set x and to post and solve the constraint x eq s LSet LSet 1s LSet String extName LSet 1s Create a l set with no external name resp with external name extName equivalent to the l set 1s Same as to create an unbound l set x and to post and solve the constraint x eq 1s Example 5 e Create an unbound l set a LSet a new LSet e Create a l set b with external name b bound to the set value 1 2 3 Set s new HashSet s add 1 s add 2 s add 3 LSet b new LSet b s e Create a l set c equivalent to the l set a LSet c new LSet a 4 2 Creating new bound l sets static LSet empty O Returns the empty l set LSet ins Object o If this l set is bound returns the new l set whose value is obtained by adding o as an element of the set bound to this va
69. to the universe U MultiInterval union MultiInterval M Returns this UM Multilnterval intersect MultiInterval M Returns this NM MultiInterval diff MultiInterval M Returns this M MultiInterval sum MultiInterval M Returns this HM where in general ABB ce Z Fa e A Abe B c a byla MultiInterval sub MultiInterval M Returns this M where in general ABBY ce Z Fa e A Abe B c a bl MultiInterval opposite Returns Bthis 0 BM Other utility methods In addition to the utility methods seen for the class Interval and the methods inherited from java util Set MultiInterval offers the following methods Interval convexClosure Returns the convex closure CHa this int getOrder Returns the order of this i e the number of disjoint intervals which define it 41 A 3 The class SetInterval Given two sets of integers A B C Z the integer set interval bounded by A and B is the set of integer sets more precisely the lattice of integer sets A B x CZ ACXC B A is the GLB Greatest Lower Bound while B is the LUB Least Upper Bound of the set interval Similarly to what done for integer intervals we fix an integer constant 8 gt 0 and define an universe Zg ef 8 B The set Sg of all the set intervals whose bounds are subsets of Ze is def
70. traint getConstraint Returns the conjunction of non solved constraints stored in the constraint store of this solver void showStore Prints the conjunction of non solved constraints stored in the constraint store of this solver Same as printing the result of this getConstraint void showStoreAll Prints the conjunction of all the constraints stored in the constraint store of this solver including solved constraints which have been possibly left in the constraint store Basically used for debugging purposes void showStoreInternals Like showStoreA11 but it prints constraints in their internal format see Sect 7 method toStringInternals Basically used for debugging purposes int size Returns the number of non solved constraints stored in the constraint store of this solver Remark The statement solver add c and c2 and c is equivalent to the se quence of statements solver add c solver add c2 solver add c The order in which atomic constraints are added to the constraint store is completely immaterial 30 8 2 Checking constraint satisfiability boolean check Constraint c If C is the constraint currently in the constraint store of this solver checks whether the constraint C A c is satisfiable or not and returns true or false respectively If CAc is satisfiable a viable constraint solution i e a set of substitutions for the unbound logical variables occurring in the constraint is also
71. type including bound or unbound logical variables lists or sets e The l list on which ins insn and insA11 methods are invoked can be either bound or unbound In particular invoking the ins insn and insA11 methods on an unbound l list allows an open list to be built e In a list the order of elements and the repetitions do matter whereas they do not matter in a set Thus for instance the list 1 2 is different from the list 2 1 or from the list 1 2 2 Example 4 e Create a l list d bound to the empty list LList d LList emptyO e Create a l list e bound to the list value c b a LList e LList emptyO ins a ins b ins c or char elems a b c LList e LList empty insAll elems e Create a l list f bound to the partially specified list value 1 x where x is an unbound logical variable LVar x new LVar LList f LList empty insn 1 insn x e Create a l list g representing the open list 1 2 r where r is an unbound I list LVar z new LVar 2 LList r new LList LList g r insn 1 insn z Note that the list value bound to g is the list 1 2 since z is replaced by its value 2 e Create a l list h bound to the list value 1 c b a 1 x te a list of nested lists LList e LList empty ins f ins e ins d where d e and are the l lists defined above e Create a l list i bound to the l
72. ulti interval 2 MultiInterval Integer a Creates the multi interval a MultiInterval Integer a Integer b Creates the multi interval a b MultiInterval Set lt Integer gt s Creates the multi interval corresponding to s MultiInterval Collection lt Interval gt I Creates the multi interval corresponding to I U U In if I is an interval collection of the form In Example 18 Multi interval constructors e Create the multi interval 10 5 8 0 1 1 9 0 1 0 5 8 10 TreeSet lt Integer gt set new TreeSet lt Integer gt set add 10 set add 5 set add 8 set add Multilnterval SUP 1 set add 1 set add 9 set add 0 MultiInterval m new MultiInterval set e Create the multi interval 2 4 U 3 5 U U 10 20 2 5 10 20 Vector lt Interval gt v new Vector lt Interval gt v add new Interval 2 4 v add new Interval 3 5 v add new Interval v add new Interval 10 20 MultiInterval m new MultiInterval v 40 Set Operations Since multi intervals are all and only the subsets of Za it is possible to define on them the same set operations applicable to Za boolean subset Multilnterval M Returns true iff this CM Multilnterval complement Returns the set complement of this with respect to the universe Za Multilnterval complement MultiInterval U Returns the set complement of this with respect
73. variable boolean equals LVar lv Returns true if this logical variable is equal to the logical variable 1v Two logical variables are equal if they are the same object either bound or unbound or they are equivalent logical variables either bound or unbound or they are distinct logical variables but bound to equal values boolean equals Object o Returns true if this logical variable is equal to the object o A logical variable x is equal to an object o other than a logical variable if x is bound to a value equal to o String getName Returns the external name associated with this logical variable Object get Value Returns the value of this logical variable if it is bound null otherwise boolean isBound Returns true if this logical variable is bound void output Prints the external name of this logical variable followed by followed by the value of this logical variable if it is bound or by unknown if it is unbound e g x 3 or y unknown LVar setName String extName Sets the external name of this logical variable to extName and returns this logical variable for reasons of convenience String toString Returns the string corresponding to the value of this logical variable if it is bound otherwise returns the string _extName where extName is the external name of this logical variable Example 2 refer to declarations of Example 1 e Test equals x equals x gt true z equals 2

JSetL User's Manual

Contents

Download Pdf Manuals

Related Search

Related Contents