Index of values

Division and modulo on expressions.

Exponentiation of an expression to an integer value.

Addition, substraction, multiplication on expressions.

Strictly less, less or equal, equal, greater or equal, strictly greater and different constraints on expressions.

Reified strictly less, less or equal, equal, greater or equal, strictly greater and different.

e1 op~~ e2 is equivalent to fd2e (Reify.boolean (e1 op~ e2)).

Conjunction and disjunction over goals.

Absolute value on expressions.

active_store () returns the list of all active constraints, i.e.

add n d returns d {n}.

all_disjoint vars ensures that all the set variables of array vars are pairwise disjoint.

argmin a c returns the BIR index of the minimum BIR value of a for criterion c.

array n inf sup returns an array of n new variables with domain [inf..sup].

atomic ~name:"atomic" f returns a goal calling function f.

binary ~name:"Invariant.binary" f wraps the binary function f into an operator on BIRs.

boolean ~delay_on_negation:true c returns a boolean (0..1) variable associated to the constraint c.

The domain containing 0 and 1.

cardinal v returns the cardinal (an integer variable) of the set v.

choose ord d returns the mininum value of d for order ord.

choose_index order fds returns the index of the best (minimun) free (not instantiated) variable in the array fds for the criterion order.

Compares two variables.

compare d1 d2 is a comparison function working first on the cardinal, then (if d1 and d2 have the same size) on the lexicographic order of the domains (expressed in extension).

compare_elt e1 e2 is a comparison function on elements of domains.

constant ~name:"" cst returns an unsetable BIR with initial content cst.

constraints_number a returns the number of different constraints attached to a.

create ~name:"create" f a returns a goal calling f a.

create ~name:"" v returns a setable BIR with initial content v.

create ?name d returns a new variable with domain d.

create ?name ?nb_wakings ?fprint ?priority ?init ?check ?not update delay builds a new constraint: name is a describing string for the constraint. Default value is "anonymous"., nb_wakings is the number of calls to Var.delay with distinct "waking_id" arguments within the constraint own delay function (see below). Default value is 1. Beware that if nb_wakings is greater than 1 and the optional init argument is not provided, init default behaviour is to do nothing (i.e. the update function will not be called)., fprint should print the constraint on an output channel taken as its only argument. Default value is to print the name string., priority is either immediate, normal or later. Time costly constraints should be waken after quick ones. Default value is normal., init is useful to perform initialization of auxiliary data structures needed and maintained by the update function. init () is called as soon as the constraint is posted. Default value is to call (update 0) if nb_wakings is equal to 1 to perform an initial propagation; if nb_wakings is greater than 1, default value is fun () -> (), i.e. it does nothing. Hence, an init argument must be provided if this is not the desired behaviour., check must be specified if the constraint is to be reifiable (as well as the not function). When the constraint is reified, check () is called to verify whether the constraint is satisfied or violated, i.e. the constraint itself or its negation is entailed by the constraint store. It should return true if the constraint is satisfied, false if it is violated and raise DontKnow when it is not known. check must not change the domains of the variables involved in the constraint. Default: Failure exception is raised., not must be specified if the constraint is reifiable (as well as check). not () should return a constraint which is the negation of the constraint being defined. When the constraint is reified, it is called to post the negation of the constraint whenever check () return false, i.e. the negation is entailed by the constraint store. Default: Failure exception is raised., update is a mandatory argument which propagates the constraint, i.e. filters domains and checks consistency. This function takes an integer as its unique parameter, according to the optional waking_id argument given to the Var.delay calls featured in the constraint own delay function (see below). When a waking event occurs, this function is called with the corresponding integer "waking_id", and must return true when the constraint is (partially) satisfied for this event, false if further propagations have to be performed, and raise Stak.Fail whenever an inconsistency is detected. The whole constraint is solved when update 0, ..., update (nb_wakings-1) have all returned true. E.g. a global constraint on an array of variables can be aware of which variable has triggered the awakening by providing the integer index of the variable as its "waking_id" to the Var.delay function. update is called with 0 by default when the nb_wakings argument has been omitted; in this case, the constraint is solved as soon as update returns true., delay schedules the awakening of the constraint ct (which is taken as its unique argument), i.e. the execution of its update function. If update id should be called (because it may propagates) when one of the events contained in the events list es occurred on variable v, then Var.delay es v ~waking_id:id ct should be called within the body of the delay function. Beware that all the "waking_ids" must be contiguous integers ranging from 0 to nb_wakings-1, otherwise the behaviour is unspecified. delay is a mandatory argument.

create l builds a new domain containing the values of l.

create_rec ~name:"create_rec" f returns a goal calling f.

cstr v inf sup b returns a constraint ensuring that the boolean variable b is instantiated to 1 if v is in inf..sup and to 0 otherwise.

cstr a (?perm:None) sorted returns the constraint ensuring that sorted is the result of sorting array a according to the permutation perm.

alldiff (?algo:Lazy) vars States that the variables of vars are different from each other.

cstr (?level:High) vars distribution returns a constraint ensuring that for each pair (c,v) of cardinal variable c and integer value v in the list distribution, c variables in the array vars will be instantiated to v, i.e.

cstr ~delay_on_negation:true c b is equivalent to the constraint boolean ?delay_on_negation c =~ b.

cut l cuts the choice points left on the stack until level l.

delay event_list v ~waking_id:id c suspends constraint c on all the events in event_list occurring on v.

Depth of the stack, i.e.

Non-deterministic instantiation of a variable, by dichotomic recursive exploration of its domain.

diff d1 d2 returns d1 d2, i.e.

difference big small returns big small.

disjoint v1 v2 defined by all_disjoint [|v1; v2|].

disjoint d1 d2 tests whether d1 and d2 are disjoint.

dom a returns the integer domain of an attribute.

e2fd e creates and returns a new variable v and posts the constraint fd2e v =~ e.

int n returns a new variable instantiated to integer value n.

Creates a set from a list of integers.

int_value v returns the value of v if it is instantiated and raises a Failure exception otherwise.

The empty domain.

Tests if two variables are equal with respect to compare.

eval e returns the integer numerical value of a fully instantiated expression e.

exists ?select g [x1;x2;...;xn] is g x1 ||~ g x2 ||~ ... ||~ g xn, i.e.

exists ?select g a defined by existsi ?select (fun _i x -> g x) a, i.e.

existsi ?select g a returns the disjunctive iteration of the application of goal g on the elements of array a and on their indices.

fail x equivalent to raise (Fail x).

fd2e v returns an expression which evaluates to n if the variable v is instantiated to n.

forall ?select g [x1;x2;...;xn] is g x1 &&~ g x2 &&~ ... &&~ g xn, i.e.

forall ?select g a defined by foralli ?select (fun _i x -> g x) a, i.e.

foralli ?select g a returns the conjunctive iteration of the application of goal g on the elements of array a and on their indices.

forto min max g (resp.

fprint chan g prints the name of goal g on channel chan.

fprint chan e prints expression e on channel chan.

fprint c ~printer:(fun _ _ -> ()) r prints BIR r on channel c.

fprint chan v prints variable v on channel chan.

fprint chan a prints attribute a on channel chan.

fprint chan c prints the constraint c on channel chan.

Pretty printing of elements and domains.

Pretty printing of elements and domains.

fprint_array chan vs prints array of variables vs on channel chan.

get vars index returns a variable constrained to be equal to vars.(index).

get a i returns the BIR element number i of array a.

Access to the content of a BIR.

Dereference.

Returns the minimum size for boolean sums optimization.

get_cstr vars index v returns the constraint fd2e vars.(index) =~ fd2e v.

smallest_geq dom val (resp.

i2e n returns an expression which evaluates to n.

id r returns a unique integer associated to BIR r.

id v returns a unique integer identifying the attribute associated with v.

id a returns a unique integer identifying the attribute a.

id c returns a unique integer identifying the constraint c.

included d1 d2 tests whether the domain d1 is included in d2, i.e.

included d1 d2 tests whether domain d1 is included in domain d2.

Non-deterministic instantiation of set variables (refine of Gervet's Conjunto).

Non-deterministic instantiation of a variable, by labeling its domain (in increasing order).

inf_min v1 v2 ensures that the minimal element of v1 is less than or equal to the minimal element of v2.

instantiate choose var Non-deterministic instantiation of a variable, by labeling its domain using the value returned by the choose function.

The largest representable domain.

Operations on sets.

interval ?name inf sup returns a new variable with domain [inf..sup].

interval glb lub builds the domain of sets greater than glb and smaller than lub.

interval inf sup returns the domain of all integers in the closed interval [inf..sup].

interval_iter f d successively applies function f to the bounds of all the disjoint intervals of d in increasing order.

is_bound v returns true if v is instantiated and false otherwise.

is_empty d tests whether the domain d is empty or not.

is_member v inf sup returns a boolean variable which will be instantiated to 1 if v is in inf..sup and to 0 otherwise.

is_solved c returns true if c is satisfied and false otherwise.

BIR variants of Fd.Var access functions.

is_var v returns true if v is not instantiated and false otherwise.

iter f v iterates f on each integer in the domain of v.

Iteration on values of the domain.

iter f d successively applies function f to all element of d in increasing order.

Standard labeling, i.e.

Standard labeling, i.e.

largest_hole_around dom val returns the largest hole (interval) in dom centred around val.

Available priorities: immediate: as soon as possible, for quick updates;, normal: standard priority;, later: for time consuming constraints (e.g. Gcc.cstr, Alldiff.cstr...).

lds ~step:1 g returns a goal which will iteratively search g with increasing limited discrepancy (see ) by increment step.

Returns the current level.

Returns the current active levels.

min vars (resp.

max v returns the upper bound of v.

min a (resp.

min d (resp.

min_cstr vars mini (resp.

min_of_expr e (resp.

mem x v states that x belongs to v.

mem x d tests whether x belongs to the domain d.

member v l returns the disjunctive iteration of the instantiation of the variable v to the values in the integer list l.

member v l ensures that v will have a value in l.

member v n returns true if n belongs to the domain of v and false otherwise.

member a n tests if n belongs to dom a.

member n d tests if n belongs to d.

min a c returns the minimum BIR value of a for criterion c.

min v returns the lower bound of v.

min_max v returns both the lower and upper bounds of v.

Access to glb and lub.

min_max d returns both the lower and upper bound of d.

min_max_of_expr e is equivalent to (min_of_expr e, max_of_expr e).

minimize ~step:1 ~mode:Continue goal cost solution runs a Branch and Bound algorithm on goal for bound cost, with an improvement of at least step between each solution found.

minus d returns the domain of opposite values of d.

name g returns the name of the goal g.

name r returns the name (specified or generated) of BIR r.

name v returns the name of variable v (the empty string if it was not provided while created).

name c returns the name of the constraint c.

Access to a global counter incremented at each choice point.

Logical reification operators on constraints, namely and, or, implies, equivalent, exclusive or, not.

not c returns the negation of c.

not_instantiated_fd fds returns the index of one element in fds which is not instantiated.

older l1 l2 true if level l1 precedes l2.

Event occuring when the lower (resp.

Event occuring when the lower (resp.

Event occuring when a variable is changed, i.e.

Event occuring when a variable is changed, i.e.

Event occuring when a variable is instantiated.

Event occuring when a variable is instantiated.

once g cuts choice points left on goal g.

order v1 v2 ensures that v1 is less than or equal to v2 according to Domain.compare .

order_with_card v1 card1 v2 card2 is equivalent to order but the cardinals of the variables must be provided too.

Basic refinements for labeling.

plus d n translates a domain by n.

post c posts the constraint c to the constraint store.

priority c returns the priority of the constraint c.

sum a returns a BIR equal to the product of elements of a.

prod exps (resp.

Returns a reference whose modifications will be trailed during the solving of a goal.

refine v d reduces the domain of v with domain d.

refine_low v inf reduces the domain of v by cutting all values strictly less than inf.

refine_low_up v inf sup reduces the domain of v by cutting all values strictly less than inf and greater than sup.

refine_up v sup reduces the domain of v by cutting all values strictly greater than sup.

remove v a removes a from the domain of v.

remove n d returns d {n}.

remove_closed_inter inf sup d returns d [inf..sup], i.e.

remove_up n d (resp.

remove_low_up low up d is a shortcut for remove_up up (remove_low low d).

remove_min d (resp.

scalprod coeffs exps (resp.

Assignment of a setable BIR.

set t i x Bactrackable assignment of t.(i) with x.

Sets a backtrackable reference.

Set the minimum size for boolean sums optimization.

shift x d returns a finite domain variable constrained to be equal to x+d.

sigma ~domain:Domain.int fgoal creates the goal (fgoal v) where v is a new variable of domain domain.

size v returns the number of integer values in the domain of v (1 if v is instantiated).

size a returns the number of integer values in the domain of a.

Size of the stack, i.e.

size d returns |glb(d)|-|lub(d)|+1, i.e.

size d returns the number of integers in d.

smallest v returns the smallest element (an integer variable) of v.

solve ~control:(fun _ -> ()) g solves the goal g and returns a success (true) or a failure (false).

sort a returns an array of variables constrained to be the variables in a sorted in increasing order.

sortp a same as sort but returns a couple (sorted, perm) where sorted is the array of sorted variables and perm is an array of variables constrained to be the permutation between a and sorted, i.e.

sprint d returns a string representation of d.

subset v1 v2 ensures that v1 is a subset of v2.

Failure (resp.

sum a returns a BIR equal to the sum of elements of a.

sum exps (resp.

sum_weight v weights returns an integer variable equal to the sum of the weights associated with the value in v.

ternary ~name:"Invariant.ternary" f wraps the ternary function f into an operator on BIRs.

times d k expands a domain by factor k.

unary ~name:"Invariant.XxxFd.unary" f v Wrapper of any access function over fd type.

unary ~name:"Invariant.unary" f wraps the unary function f into an operator on BIRs.

unify var x instantiates variable var to x.

unify v n instantiates variable v with integer value n.

Intersection (resp.

unsafe_create l builds a new domain containing the values of l.

value v returns Val n if v is instantiated to n, Unk a otherwise where a is the attribute of v.

values v returns the list of all integers in the domain of v.

Returns values of a domain.

value d returns the list of values of the domain d

The constraint which succeeds (resp.