clp2zinc is a front-end to compile CLP specifications of search strategies into Zinc models. Zinc is a well-established language to describe CSP: MiniZinc should be installed to run the generated models. Moreover, dynamic search strategies (with indexicals) should be run with a patched solver.

`clp2zinc`

command-line usage
`clp2zinc`

is a command-line tool. The basic usage is

, which compiles the ClpZinc model `clp2zinc `

*file*`.plz`

*file*`.plz`

and generates the MiniZinc model *file*`.mzn`

. `clp2zinc`

recognizes a few options:

`-g`

: this option traces the execution of the main goal on standard error. That is useful for debugging and seeing what happens. This option does not affect the output file, which will still be generated identically.*E.g.*,

.`clp2zinc -g`

*file*`.plz`

`-t`

: this option asks`clp2zinc`

to produce an and-or tree instead of a MiniZinc model. By default, the tree will be written in*file*`.inc`

in the tikz-qtree format. To include it in a TeX document:\documentclass{article} \usepackage{tikz,tikz-qtree} \begin{document} \begin{tikzpicture} \input{file.inc} \end{tikzpicture} \end{document}

`-o`

*output file name*: this option specifies the name for the generated file.*E.g.*,

or`clp2zinc -o output.mzn`

*file*`.plz`

.`clp2zinc -o tree.inc -t`

*file*`.plz`

`-I`

*path*: this option adds a search path for`include`

items, see the

section for more informations.`include`

Items`-O`

*prefix*: this option adds a prefix to the search paths for`include`

items, see the

section for more informations.`include`

Items

Several files can be compiled together: *e.g.*

, the result is identical as if the files were concatenated in a single file in the same order.
If the output file name is not specified with the `clp2zinc `

*file _{1}*

`.plz `

`.plz`

...`-o`

option, then the base name

`.mzn`

or `.inc`

suffix.Either use our build: choco-3.1.1-clpzinc.jar, or recompile it yourself:

- Download Choco 3.1.1,
- Download choco-3.1.1-clpzinc.patch,
- In the parent directory of
`choco3-choco-3.1.1/`

, run the following command:`patch -s -p0 < choco-3.1.1-clpzinc.patch`

, - In the directory
`choco3-choco-3.1.1/`

, run the following command:`mvn package -DskipTests`

, - The
`.jar`

file is in`choco3-choco-3.1.1/choco-parser/target/choco-parser-3.1.1-jar-with-dependencies.jar`

.

To solve a `.mzn`

model:

`mzn2fzn -I choco3-choco-3.1.1/choco-parser/src/chocofzn/globals/`

*file*`.mzn`

,`java -jar choco-3.1.1-clpzinc.jar`

*file*`.fzn | solns2out`

*file*`.ozn`

.

Either use our build: jacop-4.0.0-clpzinc.jar, or recompile it yourself:

`git clone https://github.com/radsz/jacop.git`

,- Download jacop-4.0.0-clpzinc.patch,
- In the parent directory of
`jacop/`

, run the following command:`patch -s -p0 < jacop-4.0.0-clpzinc.patch`

, - In the directory
`jacop/`

, run the following command:`mvn install -DskipTests`

, - The
`.jar`

file is in`jacop/target/jacop-4.0.0.jar`

.

To solve a `.mzn`

model:

`mzn2fzn -I jacop/src/main/minizinc/org/jacop/minizinc/mznlib/`

*file*`.mzn`

,`java -cp jacop-4.0.0.jar org.jacop.fz.Fz2jacop`

*file*`.fzn | solns2out`

*file*`.ozn`

.

Recompile it yourself:

`svn checkout https://svn.gecode.org/svn/gecode/tags/release-4.2.1`

,- Download gecode-4.2.1-clpzinc.patch,
- In the parent directory of
`release-4.2.1/`

, run the following command:`patch -s -p0 < gecode-4.2.1-clpzinc.patch`

, - In the directory
`gecode-4.2.1/`

, run the following command:`./configure && make`

, - The executable file is in
`release-4.2.1/tools/flatzinc/fzn-gecode`

.

To solve a `.mzn`

model:

`mzn2fzn -I release-4.2.1/gecode/flatzinc/mznlib/`

*file*`.mzn`

,`release-4.2.1/tools/flatzinc/fzn-gecode`

*file*`.fzn | solns2out`

*file*`.ozn`

.

Install it with the patch:

- Download SICStus 4.2.3 with a licence and install it,
- Download sicstus-4.2.3-clpzinc.patch,
- In the parent directory of
`sicstus4.2.3/`

(typically in`/usr/local/`

), run the following command:`patch -s -p0 < sicstus-4.2.3-clpzinc.patch`

,

To solve a `.mzn`

model:

- Run
`sicstus`

, - Execute
`use_module(library(zinc)).`

- Execute
`mzn_run_file('`

*file*`.plz').`

Recompile it yourself:

`svn checkout http://or-tools.googlecode.com/svn/trunk/ or-tools`

,- Download or-tools-clpzinc.patch,
- In the parent directory of
`or-tools/`

, run the following command:`patch -s -p0 < or-tools-clpzinc.patch`

, - In the directory
`or-tools/`

, run the following command:`make third_party bin/fz`

, - The executable file is in
`or-tools/bin/fz`

.

To solve a `.mzn`

model:

`mzn2fzn -I or-tools/src/flatzinc/mznlib/`

*file*`.mzn`

,`or-tools/bin/fz`

*file*`.fzn | solns2out`

*file*`.ozn`

.

ClpZinc extends the Zinc programming language by allowing the

item to be replaced by a CLP goal `solve`

.
There can be at most one goal item in a ClpZinc model, as there can be only one
`:- `

*goal*`.`

`solve`

item in a Zinc model.

A *ClpZinc goal* is either:

- a constraint,
- a MiniZinc search annotation,
- a call to a user-defined predicate,
- the conjunction of two goals (
`A,B`

) or the disjunction of two goals (`A;B`

).

Terms are either:

- logical variables (
`X`

,`Y`

,`Max`

, ...), - atomic constants (integers, floats, strings),
- compound terms of the form
`p(`

*t*_{1}`,`

...`,`

*t*_{n}`)`

, - records of the form
`(`

*f*_{1}`:`

*t*_{1}`,`

...`,`

*f*_{n}`:`

*t*_{n}`)`

(or, alternatively,`{`

*f*_{1}`:`

*t*_{1}`,`

...`,`

*f*_{n}`:`

*t*_{n}`}`

) - record projection of the form
*record*`.`

*field*(or, alternatively,*record*`:`

*field*) - quantified constraints of the form
`forall (`

*scope*) (*constraint*) and`exists (`

*scope*) (*constraint*)

where
*f _{1}*, ..., and

`a`

, `b`

, ...)
or array accessors (`x[I,J]`

).
Lists are denoted `[`

*X _{1}*

`,`

...`,`

`]`

(`[]`

for the empty list)
and partial lists are denoted `[`

`,`

...`,`

` | `

`]`

.
Zinc arrays have been unified with Prolog-like lists to ease their
enumeration in search strategies.
CLP lists are mapped to Zinc arrays in code generation.
Zinc two-dimensional arrays have been unified with lists of lists.
Basic constraints are:

`true`

: always true.`false`

: always false (Prolog`fail`

goal is therefore denoted`false`

in ClpZinc).*X*`=`

*Y*: states that*X*equals*Y*.*X*and*Y*can be terms, numbers or model variables, and they can be mixed:`(`

*A*`,`

*B*`) = (`

*C*`,`

*D*`)`

is equivalent to*A*`=`

*C*`,`

*B*`=`

*D*.

The following constraints are only defined when *X* and *Y* are numbers
(or arithmetic expressions, or model variables, but not terms).

*X*`!=`

*Y*: states that*X*and*Y*are different.*X*`<=`

*Y*: states that*X*is less than or equal to*Y*.*X*`>`

*Y*: states that*X*is strictly greater than*Y*.*X*`>=`

*Y*: states that*X*is greater than or equal to*Y*.*X*`<`

*Y*: states that*X*is strictly less than*Y*.

The following pseudo-constraints are only tests, they do not change the current store.

*X*`==`

*Y*: tests whether*X*and*Y*are identical (if they contain model variables, they should refer to the same variable).*X*`\=`

*Y*: equivalent to`\+`

*X*`==`

*Y*,*i.e.*, the negation of the previous test.

Goals without pending constraints can be negated with the
negation-by-failure `\+`

.
Note that MiniZinc pending constraints never fail at compile time when
they are not fully instantiated, therefore their negation will never succeed.

A comprehensive list of constraints is given in the MiniZinc specification. Every unknown predicate is assumed to be a constraint and is passed to MiniZinc, therefore all the constraints can be accessed, even solver-specific constraints.

CLP predicates can be defined with clauses:
a *ClpZinc clause* is an item of the form

where `p(`

*t _{1}*

`,`

...`,`

`) :- `

`.`

is a shorthand for`p(`

t_{1}`,`

...`,`

t_{n}`).`

.`p(`

t_{1}`,`

...`,`

t_{n}`) :- true.`

`include`

Items
Every

item is evaluated by ClpZinc by expanding it with the contents of the file `include "`

*file*`.plz";`

.
*file*`.plz`

`include`

items that include files with any other suffix than

(typically, `.plz`

`.mzn`

) are left to MiniZinc.

Files are searched in the current directory and in the list of include directories,
in their order of appearance.
This list contains all the directories listed in the `CLP2ZINCPATH`

environment variable if it exists (separated by

),
and ends with the `:`

`lib/`

sub-directory in the directory where
the `clp2zinc`

executable is located.
Search paths can be added on the top of this list with the

option.
`-I `

*path*

Moreover, for every directory in this list, prefixes can be added with the

. By default, only the `-O `

*prefix*

prefix is tried (the directory itself), but sub-directories can be added as prefix, for example to look in a sub-directory specific to a particular solver.
`.`

In CLP(*X* + *H*), arithmetic differs from Prolog.
Indeed, in accordance with the theory of CLP
and unlike most Prolog systems,
arithmetic is supposed to be contained in *X* and is distinguished from *H* terms,
*e.g.*,

is undistinguishable from `1 + 1`

and is not a `2`

*H* term.
In ClpZinc,
the different forms of unification, equality, and evaluation predicates
that are encountered in Prolog systems (`=`

, `#=`

, `is`

, ...)
are thus all unified in a unique notion of equality, which is accessible either
explicitly with the predicate `=`

, or implicitly when predicate arguments in either *X* of *H* are unified.

*I*`+`

*J*: addition.*I*`-`

*J*: subtraction.`-`

*I*: opposite.*I*`*`

*J*: multiplication.*I*`div`

*J*: division (either integer division if*I*and*J*are integers, floating-point division otherwise).*I*`rem`

*J*: modulo.*X*`/`

*Y*: floating-point division.`log(`

*B*`,`

*X*`)`

: logarithm of*X*in base*B*.`ceil(`

: smallest integer greater than*X*)*X*.`floor(`

: largest integer smaller than*X*)*X*.`min(`

*A*`,`

*B*`)`

: minimum between two values.`max(`

*A*`,`

*B*`)`

: maximum between two values.`min([`

*X*_{1}`,`

...`,`

*X*_{n}`])`

: minimum of a list (distinguished from the indexical of the same name, if`min`

is applied to a model integer variable rather than a list).`max([`

*X*_{1}`,`

...`,`

*X*_{n}`])`

: maximum of a list (distinguished from the indexical of the same name, if`max`

is applied to a model integer variable rather than a list).

A comprehensive list of arithmetic operators is given in the MiniZinc specification. Every unknown term is treated as an Herbrand term and is printed as is in the MiniZinc generated model, therefore every MiniZinc function symbol can be used.

Arithmetic expressions are also extended for accessing
the indexicals of the model variables. For instance,
the goal `M = min(X)`

assumes that `X`

is a model variable and unifies `M`

with the
currently known lower-bound of `X`

.
The available indexicals are:

`min(`

*X*`)`

: returns the current lower-bound in the domain of*X*.`max(`

*X*`)`

: returns the current upper-bound in the domain of*X*.`card(`

*X*`)`

: returns the number of elements in the domain of*X*.`dom_nth(`

*X*`,`

*N*`)`

: returns the*N*th element in the domain of*X*.

Some search strategies require to iterate a search tree several times with some kind of memory passed from one branch to another.
That is typically the case for optimization methods like branch-and-bound where the best score reached up to now is remembered
from one iteration to another of the underlying search strategy,
or for shaving, where one step of propagation is performed and undone in
order to select the best one.
In languages like Prolog, such methods are implemented with the help of some kind of global state, most commonly
stored within the fact database (with `assert`

and `retract`

).
The two additional annotations can be used in ClpZinc to handle global state.

`store("`

*global*`", [`

*X*_{1}`,`

...`,`

*X*_{n}`])`

: stores the current values of the sequence of variables`[`

*X*_{1}`,`

...`,`

*X*_{n}`]`

into the global state identified as*global*.`retrieve("`

*global*`", [`

*X*_{1}`,`

...`,`

*X*_{n}`])`

: assigns the values previously remembered into the global state identified as*global*into the sequence of variables`[`

*X*_{1}`,`

...`,`

*X*_{n}`]`

.

The search annotations of MiniZinc are accessible in goals in order to allow the composition of user-defined strategies with built-in ones. MiniZinc search annotations (except indexicals and accesses to global states) cannot appear under an unsolved choice-point.

`int_search([`

*X*_{1}`,`

...`,`

*X*_{n}`],`

*variable selector*`,`

*value selector*`,`

*search method*`)`

: defines a search step choosing between the variables*X*_{1}`,`

...`,`

*X*according to the_{n}*variable selector*(either`input_order`

,`first_fail`

,`most_constrained`

, etc.) using the*value selector*(either`indomain_min`

,`indomain_max`

,`indomain_split`

, etc.). Search method can be either`complete`

or`lds(`

*N*`)`

when solvers support this annotation.

The three following pseudo-search annotations can appear at most once in the goal.

`satisfy`

(default): tells the solver to look for any solution.`minimize(`

*N*`)`

: tells the solver to find a solution that minimizes the value of the objective*N*.`maximize(`

*N*`)`

: tells the solver to find a solution that maximizes the value of the objective*N*.

The standard library is in the lib/ directory. It contains the following ClpZinc files:

- prolog.plz: definition of some usual Prolog predicates.
- dichotomy.plz: definition of the
dichotomic search

search strategy, bissecting over the domain of a variable. - interval_splitting.plz: definition of the
interval splitting

partial search strategy. - lds.plz: definition of the
limited discrepancy search

search strategy transformer, by meta-interpretation. - branch_and_bound.plz: definition of the
branch & bound

optimization procedure, for minimization or maximization.