Extended Indexicals: User Manual
Contents
1. Defines a propagator The body is a list of instructions Note prop can be used as a shortcut for propagator Table 2 1 Continued Construction Example s Type Semantics propagator lt NAME gt lt INSTRS Same as above but with a name by which the propagator can be referred to propagator lt ANNOTS gt lt INSTR Same as above but with annotations attached to the propagator The used annotations for propagators are BR DR VR Default They are used in the Gecode code generation We refer to Section 3 3 2 for their meaning propagator lt NAME gt lt ANNOTS lt INSTRS Same as above with both name and annotation checker lt BOOL gt Defines a checker The body is a Boolean formula checker lt NAME gt lt BOOL gt Checker Same as above with a name names are not yet used checker lt ANNOT gt lt BOOL gt Same as above with an annotation checker lt NAME gt lt ANNOT gt BOOL gt Instructions VOID Same as above with both name and annotation lt VAR gt in lt SET gt X in dom Y VOID Updates the domain of lt VAR gt to be the intersection of its current domain and the set lt SET gt post lt CINVOKE gt lt PNAME gt post PLUS X Y 10 FC VOID Calls a propagator of the constraint given in first argument In the current compiler the effect is to expand the c2. min N 1 gt sum j in j in rng X i j b2i max X j lt v 1 and sum j in j in rng X i j b2i min X j lt v 1 gt max N 1 gt X i in v sup min N gt sum j in j in rng X i j b2i max X j lt v 1 and sum j in j in rng X i j b2i min X j lt v 1 gt max N gt X i in inf v 1 Feeding it to the compiler again results in a bit pipler code which we save again in cstr idx def Exactly_geq vint X vint N int v checker val N sum i in rng X b2i v lt val X i propagator genbnd N in sum i in rng X b2i v lt min X i sup N in inf sum i in rng X b2i v lt max X i forall i in rng X sum j in j in rng X i j b2i v lt max X j lt min N 1 and max N 1 lt sum j in j in rng X i j b2i v lt min X j gt X i in v sup 10 sum j in j in rng X i j b2iW lt max X j lt min N and max N lt sum j in j in rng X i j b 2i v lt min X j gt X i in inf v 1 CONDTEWNH 11 12 13 Now we will make use of our human knowledge to remove some parts of the conditions in the forall Indeed some parts are always true thanks to the indexicals that restrict N Further we know that the remaining of the condition can only be true when N is fixed so we will replace the min N and max N by val N This
3. naryvar9 v lt X j min naryvar9 for int i 0 i lt localvar41 i int localvar34 N val if X i max lt v 1 naryvar8 lt localvar34 1 GECODE_ME_CHECK_ MODIFIED nafp X i gq home v if localvar34 lt X i min lt v 1 naryvar9 GECODE_ME_CHECK MODIFIED nafp X i lq home v 1 11 if boolvar12 int localvar38 N val if naryvar7 lt localvar38 if localvar38 lt naryvar6 return home ESSUBSUMED this if X assigned amp amp N assigned amp amp true return home ESSUBSUMED this return ES_FIX This code can be further simplified as the variables naryvar8 and naryvar7 compute the same value and the same thing happens with naryvar9 and naryvar6 In addition the while loop and the last if statement can be removed as they are not necessary here Indeed one can show that this propagator is idempotent without the need to repeat it Finally variables can also be renamed to more meaningful names ExecStatus propagate Space amp home const Gecode ModEventDelta amp med int size X size int lbound 0 for int i 0 i lt size i lbound v lt X i min lbound GECODE_ME_CHECK N gq home lbound int ubound 0 for int i 0 i lt size i ubound v lt X i max ubound GECODE_ME _CHECK N 1q home ubound if N assigned int valN N val
4. applied pointwise U U SET The universe set emptyset emptyset SET The empty set lt ID gt S SET The set represent by this identifier lt INT gt lt INT gt 1 10 SET The range of integer between the two given integers included rng lt ID gt rng X SET The range of values on which the array is defined ID must be the identifier of some array lt NarySetOp gt lt ID gt in lt SET gt lt SET gt inter i in rng X dom X i SET The result of applying the operator inter union or sum on the all the sets constructed from all the values in the range set lt SET gt dom X SET The set where all values have been replaced by their opposite lt INT gt 1 3 5 SET A set given in extension lt ID gt in lt SET gt lt BOOL gt i in dom X i gt min x SET The subset of SET retaining only the values that satisfy the BOOL predicate lt ID gt lt INT gt Integers s i SET INT Accesses an element of an array of sets min lt VAR gt min X INT The minimum of the domain of variable lt VAR gt in the current store max lt VAR gt max X INT The maximum of the domain of variable lt VAR gt in the current store Table 2 1 Continued Constr
5. for int i 0 i lt size i if X i max lt v ubound lt valN GECODE_ME_CHECK X i gq home v if valN lt X i min lt v 1 lbound GECODE ME CHECK X i 1q home v 1 if ubound lt valN amp amp valN lt lbound return home ESSUBSUMED this return ES_FIX Notice that this last step at the C level is not strictly necessary and even so would only take a few minutes to perform The resulting propagator has a linear temporal complexity in the number of variables while the indexical formulation might seem quadratic because of the n ary operators in the loop Notice that this optimisation is not always possible 12 Bibliography 1 Gecode Team Gecode A generic constraint development environment 2006 Available from http www gecode org Jean No l Monette Pierre Flener and Justin Pearson Towards solver independent propagators In Michela Milano editor CP 2012 volume 7514 of LNCS pages 544 560 Springer 2012 3 Nicholas Nethercote Peter J Stuckey Ralph Becket Sebastian Brand Gregory J Duck and Guido Tack MiniZinc Towards a standard CP modelling language In Proceedings of CP 07 volume 4741 of LNCS pages 529 543 2007 4 Pascal Van Hentenryck and Laurent Michel Control abstractions for local search In Francesca Rossi editor CP 2003 volume 2833 of LNCS pages 65 80 Springer 2003 5 Pascal Van Hentenryck Vijay Saraswat and Yves Devill
6. on the right hand side The types of both sides must coincide Such variables are immutable and cannot be redefined The type can be int set and bool lt TYPE gt lt ID gt all lt ID gt in lt SET gt lt gt booll b all i in rng X true VOID Same as above for arrays cstr lt CNAME gt lt args gt Sarre cstr EQO vint X EQ X 0 VOID Defines a new constraint template i e a constraint that can take some argument The right hand side is some constraint invocation that can use the formal parameters of the template cstr lt CNAME gt lt gt cstr OK PLUS X i Y Z VOID Defines a new constraint instance vint lt VAR gt Sh 25 2 vint ZO Z 0 VOID Defines an alias for a variable vint lt VAR gt freshvint vint W freshvint VOID Defines a fresh local decision variable Table 2 1 Continued Construction Example s Type Semantics Various Expressions ANY lt VAR gt X XLi VAR Represents a variable Variable and variables arrays names must start with an uppercase letter They can contain letters numbers and underscores lt ID gt ANY Represents a value integer set Boolean or array thereof Their names start with a lowercase letter They can contain letters numbers and underscores lt NAME gt This is the name of a propagator o
7. possible to change the type of the output to compile toward some solver The option t target changes the target of the compiler The following values of target are allowed e idxs Prints indexical code This is the same as not specifying a target e gecode Compiles to Gecode propagators Two files are written the header and source files by appending respec tively hh and cpp to the given output file name e comet Compiles to Comet propagators e oscar Compiles to OscaR propagators The given output file name is interpreted as the directory where the Java files are to be written e gecode fzn Creates the Gecode FlatZinc interpreter binding for the Gecode propagator created with gecode e list Prints the list of constraints and for each the list of propagators and checkers e none Does not print anything Useful if one wants to output only some stats option s The input file can contain several constraints It is possible to specify to use only one of them by giving its name to the option c constraintname Before outputting the code several transformations can be applied They are activated with the following flags e genReif suffix Generates a reified version of the constraints by adding the suffix to the constraint name and adding an indicator variable as last parameter The constraints whose name already end with the suffix or for which there exists already another constraint with the same name and
8. results in 1 def Exactly_geq vint X vint N int v 2 checker 3 val N sum i in rng X b2i v lt val X i 4 5 propagator genbnd 6 N in sum i in rng X b2i v lt min X i sup 7 N in inf sum i in rng X b2i v lt max X i 8 forall i in rng X 9 sum j in j in rng X i j b2i v lt max X j lt val N 1 gt X i in v sup 10 val N lt sum j in j in rng X i j b2iW lt min X j gt X i in inf v 1 11 12 13 Now that we are satisfied with our propagator we will generate Gecode code from it using the options o exactly geq t gecode to create the files exactly geq hh and exactly geq cpp We report here only the code of the propagator ExecStatus propagate Space amp home const Gecode ModEventDelta amp med bool nafp true while nafp nafp false int naryvar6 0 int localvar4l X size 1 for int i 0 i lt localvar41 i naryvar6 v lt X i min naryvar6 GECODE_ME_CHECK MODIFIED nafp N gq home naryvar6 int naryvar7 0 for int i 0 i lt localvar41 i naryvar7 v lt X i max naryvar7 GECODE_ME_CHECK MODIFIED nafp N lq home naryvar7 bool boolvarl2 N assigned if boolvar12 int naryvar8 0 for int j 0 j lt localvar41 j 4 naryvar8 v lt X j max naryvar8 int naryvar9 0 for int j 0 j lt localvar4l j
9. 1 10 cp var lt CP gt int y cp 10 1 solve lt cp gt cp post ACSTR x y eel 3 3 2 Gecode A propagator generated for Gecode is defined as a class extending Propagator In addition two functions are defined to post the constraint Their name is exactly the name defined in the indexical file The first function follows the Gecode convention that is the first argument is the Home in which to post the constraint the next arguments are the actual arguments of the constraint and the optional last argument is the consistency level IntConLevel Note that this last argument makes sense only if you defined several propagators and annotate them The correspondence is as follows 2 8 a 0 Annotation Meaning IntConLevel DR Domain Reasoning ICL_DOM BR Bounds Reasoning ICL_BND VR Value Reasoning ICL_VAL Default Default Propagator ICL DEF If more than one propagator has the same annotation one is chosen arbitrarily A propagator is also chosen arbitrarily as the default if no default is given The arguments of the posting functions are in the order specified in the source The types are translated as follows Indexicals Gecode vint Int Var vint Int VarArgs vint Bool BoolVar vint Bool BoolVarArgs int int int IntArgs bool bool bool IntArgs set IntSet set IntSetArgs Notice that the Bool annotation put after a vint argument e g vint X Bool makes it compiled
10. E 6 available from The main features of our compiler in its current state are Compilation of stateless non incremental propagators to Gecode 1 Comet Syntactic verification of monotonicity and correctness of propagators Simple transformations of propagators Deductive synthesis of propagators from checkers not yet documented Generation of an extended Gecode FlatZinc interpreter not yet documented The remainder of this document is structured as follows Chapter 2 describes in details the indexical language Chapter 3 shows how to use the compiler and the generated code 4 and OscaR Chapter 4 gives a complete example of the use of the compiler in an interactive fashion 1 1 Getting Started 1 1 1 Installation You can download it from http user it uu se jeamo371 http www oracle com technetwork java javase downloads index html versions 5 and 7 should work as well but have not been tested and a copy of Antlr 3 4 available at indexicals jar http www antlr org download antlr 3 4 complete jar to be put in the same folder as 1 1 2 Executing the compiler The compiler is run at the command line and accepts a set of options detailed in Section 3 1 To execute the compiler type java jar indexicals jar options As an example java jar indexicals jar f examples mzn flatzinc idx genProp c FZN_int_eq t gecode o int
11. Extended Indexicals User Manual Jean No l Monette Version 1 4th October 2012 Chapter 1 Introduction This document describes how to use the compiler for extended indexicals Indexicals have been introduced in 5 to de scribe constraint propagators Extended indexicals aim at representing propagation of global constraints in a high level and solver independent way yet being compilable into real and efficient propagators This extension has been published first in 2 If you want to refer to the compiler please refer to that article 2 in priority over the present document The language and the compiler are research tools and are currently subject to potential major modifications Any way we think it is important to make it available to get feedback from potential users So if you try to use the indexical compiler we would be grateful to hear your feedback be it positive this is encouraging or negative this is useful for future improvements We try to keep the documentation up to date with the program If this is not the case please inform us as well Some functionality may even not be documented at all You can contact the main author at jean noel monette it uu se The program is distributed under a BSD style license see the file LICENSE in the jar The compiler is mainly written in Java and uses Antlr and StringTemplate The compiler is distributed as a Java jar file indexicals You need a Java Runtime Environment JRE S
12. R WN FR CONDOR WNH 10 def Exactly_geq vint X vint N int v checker val N sum i in rng X b2i v lt val X i Then we ask the compiler to generate a corresponding propagator adding the genProp option The result is def Exactly_geq vint X vint N int v checker val N sum i in rng X b2i v lt val X i propagator genbnd N in sum i in rng X b2i v lt min X i sup N in inf sum i in rng X b2i v lt max X i forall i in rng X 1 lt min N sum iiO in ii0 in rng X i ii10 b2i max X ii0 lt v 1 and max N sum iiO in ii0 in rng X i i10 b2i min X ii0 lt v 1 lt 1 gt Xfi in v sup 0 lt min N sum iiO in ii0 in rng X i i1i10 b2i max X ii0 lt v 1 and max N sum iiO in i110 in rng X i i110 b2iGmin X ii0 lt v 1 lt 0 gt X i in inf v 1 This seems a bit heavy so we decide to save this code in the file cstr idx overwriting the previous content to manually modify it We replace all the loop indices ii0 by j and we rewrite slightly the inequations CONOTKBRWNEH 10 def Exactly_geq vint X vint N int v checker val N sum i in rng X b2i v lt val X i propagator genbnd N in sum i in rng X b2i v lt min X i sup N in inf sum i in rng X b2i v lt max X i forall i in rng X
13. Semantics The following table gives the semantics of each construct of the language lt CSTRorINC gt lt CSTR gt lt INCLUDE gt include lt FILENAME gt def lt CNAME gt lt args gt lt PROPAG gt lt CHECKER gt propagator lt NAME gt lt INSTRS gt checker lt NAME gt lt BOOL gt lt INSTR gt lt VAR gt in lt SET gt post lt CINVOKE gt PNAME fail lt BOOL gt gt lt INSTR gt once lt BOOL gt lt INSTR gt forall lt ID gt in lt SET gt lt INSTR gt lt INSTRS gt lt DEF gt U emptyset lt ID gt lt INT gt lt INT gt rng lt ID gt dom lt VAR gt lt NarySetOp gt lt ID gt in lt SET gt lt SET gt lt SET gt lt SET gt lt BinSetOp gt lt SET gt lt INT gt lt ID gt in lt SET gt lt BOOL gt inf sup lt NUM gt lt ID gt card lt SET gt min lt SET gt max lt SET gt min lt VAR gt max lt VAR gt val lt VAR gt b2i lt BOOL gt lt INT gt lt INT gt lt BinIntOp gt lt INT gt lt NaryIntOp gt lt ID gt in lt SET gt lt INT gt true false lt ID gt lt INT gt lt BoolIntOp gt lt INT gt lt INT gt memberof lt SET gt lt SET gt lt BoolSetOp gt lt SET gt not lt BOOL gt lt BOOL gt lt BinBoolOp gt lt BOOL gt lt NaryBool0p gt lt ID gt in lt SET gt lt BOOL gt entailed lt CINVOKE gt satisfiable lt CINVOKE g
14. _eq will read the content of one of the files provided with the distribution and look for the constraint named FZN_int_eq The compiler will then generate the propagator from the checker and compile it to Gecode in the files named int_eq hh and int_eq cpp 1 1 3 Examples The compiler comes with various examples of constraint descriptions They can be found in the example directory of the jar file The subdirectory mzn contains examples of checkers related to FlatZinc and MiniZinc 3 the subdirectory CP2012 contains the code that has been use to produce the figures in 2 Acknowledgements This work is supported by grant 2011 6133 of the Swedish Research Council VR I thank the anonymous reviewers and Christian Schulte for their useful comments for the original paper as well as Mats Carlsson for encouraging us to write it Many thanks to Hakan Kjellerstrand for the early and valuable feedback on the compiler Finally I would like to thank my colleagues Pierre Flener and Justin Pearson for the good collaboration and their many advices lhttps bitbucket org oscarlib oscar Chapter 2 The Language This chapter presents the language used to describe the indexicals It first describes the syntax of the language and then gives the semantics of the various constructs Parts of this chapter are taken from 2 2 1 Syntax Comments Comments can appear in the source file at any place They are C Java style i e they are enclosed
15. all replacing it by the actual propagator where the formal arguments have substituted for the actual ones If PNAME is present then calls the propagator with that name if any fail fail VOID Fails the current store once lt BOOL gt lt INSTR gt once 1 lt 2 fail VOID Executes the instruction INSTR once the Boolean condition is verified The condition should be monotonic i e if it is true in some store it should be true in any stronger store The compiler may use this fact when transforming the code to some targets lt BOOL gt gt lt INSTR gt true gt fail VOID Syntactic sugar for the above forall lt ID gt in lt SET gt lt INSTR gt forall i in rng X xli in 0 1 VOID Executes the instruction for all values in the set ID takes the value of the current el ement and can be used in the instruction forall lt ID gt in lt SET gt lt BOOL gt lt INSTR gt forall i in rng X i 0 x i in 0 1 VOID Same as above but the instruction is executed only for the elements that satisfy the Boolean condition INSTRS X in dom Y Y in dom X VOID Used to group several instructions in one to define the body of the once and forall instructions lt TYPE gt lt ID gt lt gt int a 1 VOID Defines a new program variable In the current compiler the left hand side is really a shortcut for the expression
16. by and or are started by and end at the end of the current line Currently comments are simply discarded by the compiler and are not transferred to the compiled file Types The language is strongly typed and has six basic types integers int Booleans boo1 sets of integers set integer decision variables vint and constraints cstr and cstr The two types for constraints are discussed later The compiler supports arrays of any basic type but currently not arrays of arrays Identifiers of arrays of decision variables and constraints start with an uppercase letter Identifiers of constants denoting integers Booleans sets and arrays thereof start with a lowercase letter Grammar Figure 2 1 presents the slightly simplified grammar of our language The main rule CSTR defines a constraint A constraint is defined by its name and list of arguments Constraint name overloading is allowed as long as the concerned constraints have different arguments in type or in number A constraint definition contains the description of zero one or more propagators and zero one or more checkers A propagator is a procedure that reduces the domains of the variable in order to remove values that cannot participate in a solution of the constraint given the current domains A checker is a logical formula that decides whether an assignment satisfies the constraint There are four accessors to the domain of a decision variable d
17. e Design implementation and evaluation of the constraint language cc FD Technical Report CS 93 02 Brown University Providence USA January 1993 Revised version in Journal of Logic Programming 37 1 3 293 316 1998 Based on the unpublished manuscript Constraint Processing in cc FD 1991 13
18. e a decision variable as an integer Even in a checker if you want to access the value of a variable you must use the val accessor or one of the other accessors e Calling a constraint without enclosing it in a function Even in a checker you must enclose a call to another constraint in one of the following functions post to post a propagator of the constraint Used n another constraint s propagator as an instruction check to test if the constraint is satisfied on a ground instance Typically used in a checker entailed to test if the constraint is entailed Typically used in a propagator in a Boolean context satisfiable to test if the constraint is satisfiable Typically used in a propagator in a Boolean context Understanding the error outputs e mismatched input C expecting ID means that you probably used an upper case letter C in this case for an identifier of something that is not a variable or a constraint e Exception in thread main java lang IllegalArgumentException Can t find template ite st group hierarchy is ToGecode is a problem inside the compiler please report it so that we can fix it e line 34 13 no viable alternative at input Alldiff means that you probably used a constraint without enclosing it into a post or check function 3 3 Using the produced code This section describes the structure of the produced code for the different targets and how to interface with it 3 3 1 Co
19. esented by this identifier lt ID gt lt INT gt bli BOOL Accesses an element of an array of Booleans lt INT gt lt BoolIntOp gt lt INT gt 3 lt 8 BOOL The result of testing the predicate on the two integers The operator can be lt gt lt gt l lt INT gt memberof lt SET gt 3 memberof dom X BOOL true if the integer is a member of the set false otherwise lt SET gt lt BoolSetOp gt lt SET gt dom X subseteq dom Y BOOL The result of testing the predicate on the two sets The operator can be seteq or subseteq not lt BOOL gt not true BOOL The negation of the Boolean lt BOOL gt lt BinBool0p gt bi and b2 BOOL The result of applying the binary operator lt BOOL gt and or lt gt andThen orElse on the two operands The two last operators andThen orElse are lazy in that they should never consult the second operand if the result can be determined from the first operand alone lt NaryBool0p gt lt ID gt in or i in BOOL The result of applying the operator and lt SET gt lt BOOL gt rng X check C X i and or on all the Booleans constructed from all the values in the set entailed lt CINVOKE gt entailed SUM X Z BOOL Tests if the constraint is entailed in the current store satisfiable lt CINVOKE gt satisfiable C BOOL Tests if the constraint is satisfiable in the current store check lt CINVOKE gt check REIFY SUM X Z B BOOL Tests if the co
20. into a Gecode Boolean variable The second defined function replaces the IntConLevel by an enumeration letting one choose among all the defined propagators of the constraint The enumeration is defined in the header file just before the function prototypes As an example if you defined a constraint by indexicals as def ACSTR vint X vint Z an example program that uses it could be include lt gecode driver hh gt include lt gecode int hh gt include generated_file hh using namespace Gecode class TestCSTR public Script private IntVarArray X IntVar Z public TestCSTR X this 10 2 8 Z this 10 10 ACSTR this X Z 3 3 3 Oscar TOCOME 3 3 4 Gecode FlatZinc TOCOME Chapter 4 Example This section presents an example use of the compiler in an interactive fashion For the details of the syntax see Chapter 2 Our case is the development of a propagator in Gecode that constraints the number of variables that are larger than some given value We call this constraint exactly_geq We start by writing the signature of this constraint and a checker for it in a text file called here cstr idx oR WN RE def Exactly_geq vint X vint N int v checker val N sum i in rng X b2i v lt val X i Calling the compiler as java jar indexicals jar f cstr idx prints the very same code to the standard output this assures us that we have not made any syntax error o
21. met A propagator generated for Comet is defined in a class that extends MyUserConstraint lt CP gt This last class is defined in the file propsupport co that you can find in the jar file in the runtime comet directory You need to extract this file and place it along the generated files or in any place that the Comet compiler knows In addition to the classes for the propagators two functions are defined for each constraint These functions are used to post the constraint and their name is exactly the one defined in the indexical file The first function takes as argument the set of arguments of the constraint in the order defined in the indexical The types are translated as would be expected In particular a vint becomes a var lt CP gt int The second function adds an argument to choose which propagator to use The type of this last argument is an enumeration corresponding to the propagators If using the first function the first propagator of the constraint is ar bitrarily chosen These functions return an object of type UserConstraint lt CP gt To use the newly defined constraints in your constraint program it suffices to include the generated file and call the corresponding function as argument of a post method As an example if you defined a constraint by indexicals as def ACSTR vint X vint Z an example Comet program that uses it could be include generated_file co Solver lt CP gt cp var lt CP gt int x
22. nstraint is verified in the cur rent store where the variables appearing in the constraint are ground Chapter 3 Using the Compiler 3 1 From the command line The compiler is run at the command line and accepts a set of options detailed hereafter To execute the compiler you type java jar indexicals jar options The first option is to set the input file using f filename The file name can be given relative to the working directory or with an absolute path The file name must end with idx If the file name does not end with the right extension idx is appended to the file name If the file is not found in the file system it is also searched for in the jar file which contains some predefined constraints in the examples subdirectory For instance java jar indexicals jar f examples mzn flatzinc idx reads the file that contains the definition of all the FlatZinc built in constraints supported by our compiler i e without set or float variables If no more option is given the compiler just parses the file performs a normalisation of the code prints some statis tics and outputs the resulting code to standard output The normalisations that are performed are straightforward simplifications of formulas expansion of calls to other constraints and removal of local program variables It is possible to change the output file with the o filename option The file name can be relative or absolute It is also
23. om x min x max x and val x denote respec tively the domain of decision variable x its minimum value its maximum value and its unique value As val is only determined when the decision variable x is ground the compiler adds guards to ensure a correct treatment when x is not ground The instruction post invokes the propagator of another constraint The functions entailed satisfiable and check query the status of another constraint Let S be the current store entailed c and satisfiable c decide whether the constraint c is entailed respectively satisfiable in S if S is an assignment then the function check c can be called and decides whether S satisfies the constraint c A new feature of our language is what we call a meta constraint which is a constraint that takes other constraint s as argument s We distinguish between constraints on actual arguments cstr and constraints on formal arguments cstr Meta constraints allow one to write more concise propagators by encapsulating common functionalities See the file examples meta idx for some examples lt FILE gt lt CSTRorINC gt lt INCLUDE gt lt CSTR gt lt PROPAG gt lt CHECKER gt lt INSTRS gt lt INSTR gt lt SET gt lt INT gt lt BOOL gt lt DEF gt lt BinIntOp gt lt NaryIntOp gt lt BinSetOp gt lt NarySetOp gt lt BoolIntOp gt lt BoolSetOp gt lt BinBool0p gt lt NaryBool0p gt lt NUM gt lt CINVOKE gt 2 2
24. r checker It can be any name composed of letters numbers and underscores which is not a reserved keyword It can also be a number lt CNAME gt SUM Sum The name of a constraint It must start with an uppercase letter It can contain letters numbers and underscore lt args gt int x vint X Arguments are comma separated Each formal argument is composed of a type and a name The name must follow the capitalisation rules defined above The name may be followed by some annota tions In particular Bool tells that the integer variable represents a 0 1 variable lt CINVOKE gt PLUS X Y 10 The invocation of a constraint which is used in post check entailed satisfiable and local cstr definitions The name of the constraint is followed by the actual arguments in parenthesis and comma separated It can also be a local constraint instance lt ANNOTS gt Sets BR SET Defines annotations Several annotations can be attached to the same element by separating them by dom lt VAR gt dom X SET The domain of variable lt VAR gt in the current store lt SET gt lt BinSetOp gt lt SET gt dom X inter dom Y SET The result of the binary set operator union inter minus lt SET gt lt BinIntOp gt lt SET gt dom X dom Y SET The result of the binary operator mod on the two operands Those integer operators are
25. t check lt CINVOKE gt lt type gt lt ID gt lt gt lt type gt lt ID gt all lt ID gt in lt SET gt lt gt cstr lt CNAME gt args lt gt x mod sum min max union inter minus lt BinIntOp gt union inter sum fiat lt a ef SS seteq subseteq lt NaryBool0p gt lt gt andThen orElse and or 1 2 12 lt CNAME gt lt CNAME gt lt args gt Figure 2 1 BNF like notation for a simplified definition of the language Table 2 1 Semantics of the language Construction Example s Type Semantics Structures include lt FILENAME gt include basis Includes the content of the given file into the current file The file name is appended idx if necessary and the file is looked for both in the directory of the including file and the calling directory of the application def lt CNAME gt lt args gt def INC vint x Creates a constraint with the given name and parameters It is possible to overload constraints with different arguments The body of the definition is made of zero one or more propagators and checkers A constraint name must start with a upper case letter def def INC FZN vint x lt CNAME gt lt args gt lt ANNOTS gt Same as above but with annotations attached to the constraint propagator lt INSTRS gt
26. the suffix are not treated Currently only the checkers of the reified constraints are generated as we don t have a general way to transform the propagator e genProp Generates a propagator for each checker of the constraints Constraints that already have a propagator are not concerned e genPropForce Generates a propagator for each checker of the constraints This is done even if the constraint already has some propagator e dom2bnd Replaces all appearances of the dom X accessor by the range min X max X for any variable X The transformations are applied in the order given above The order in which options are given at the command line does not matter Two more options exist e h prints a short help message summarising the available options and quit e s prints some statistics on the constraints to the standard output 3 2 Debugging The purpose of this section is to help debug code in case the compiler complains Indeed in the current version the error messages can be very unhelpful We are working on improving this Notice that some errors might be due to errors in the compiler Do not hesitate to report problems you have You might save time as well as the one of other users Usual sources of errors e Confusion in identifier syntax Decision variable names vint and constraint identifiers start with an upper case letter Integer set and Boolean identifiers start with with a lower case letter e Trying to us
27. uction Example s Type Semantics val lt VAR gt val X INT The unique value in the domain of variable lt VAR gt Is not evaluated until lt VAR gt is indeed bound to a single value lt INT gt lt BinIntOp gt lt INT gt i 3 INT The result of the binary operator on the two operands The operators are mod with their usual meaning inf inf INT The negative infinity infimum sup sup INT The positive infinity supremum lt NUM gt 0 1 13 999 INT A natural number Negative integers are obtained by applying the unary minus operator below lt ID gt x INT The integer represented by this identifier card lt SET gt card rng X INT The cardinality size of the given set min lt SET gt min 1 2 INT The smallest value in the given set max lt SET gt max dom X INT The largest value in the given set b2i lt BOOL gt b2i true INT The reified value of the given Boolean 1 stands for true and 0 for false lt INT gt 5 INT The opposite of the given integer lt NaryIntOp gt lt ID gt in min i in INT The result of applying the operator sum lt SET gt lt INT gt rng X min X i min or max on all the integers constructed from all the values in the set lt ID gt lt INT gt ali INT Accesses an element of an array of integers Booleans BOOL true true BOOL The true Boolean literal false false BOOL The false Boolean literal lt ID gt b BOOL The Boolean repr
Download Pdf Manuals
Related Search