The predicates described here operate on a data structure FznState representing a FlatZinc program and consisting of the following members:
var_is_introduced
annotation.
This data structure can be constructed from a FlatZinc program by the
predicates fzn_load_stream/2
and fzn_load_file/2
described
next, or directly from a MiniZinc program (see MiniZinc).
fzn_load_stream(
+FznStream,
-FznState)
Exceptions: Exceptions regarding errors in FznStream
(see Zinc Errors).
fzn_load_file(
+FznFile,
-FznState)
fzn_load_stream/2
handling stream opening and closing.
Exceptions:
Consider the following FlatZinc program for solving the 4 Queens problem
located in library('zinc/examples/queen4.fzn')
. (Note that
FlatZinc programs are not intended to be written (or read) by humans,
but rather to be automatically generated. One method to generate
FlatZinc programs is described in MiniZinc.)
% queen4.fznint: n = 4; array[1 .. 4] of var 1 .. 4: q::output_array([ 1 .. 4 ]); constraint int_lin_ne([ 1, -1 ], [ q[1], q[2] ], 1); constraint int_ne(q[1], q[2]); constraint int_lin_ne([ 1, -1 ], [ q[1], q[2] ], -1); constraint int_lin_ne([ 1, -1 ], [ q[1], q[3] ], 2); constraint int_ne(q[1], q[3]); constraint int_lin_ne([ 1, -1 ], [ q[1], q[3] ], -2); constraint int_lin_ne([ 1, -1 ], [ q[1], q[4] ], 3); constraint int_ne(q[1], q[4]); constraint int_lin_ne([ 1, -1 ], [ q[1], q[4] ], -3); constraint int_lin_ne([ 1, -1 ], [ q[2], q[3] ], 1); constraint int_ne(q[2], q[3]); constraint int_lin_ne([ 1, -1 ], [ q[2], q[3] ], -1); constraint int_lin_ne([ 1, -1 ], [ q[2], q[4] ], 2); constraint int_ne(q[2], q[4]); constraint int_lin_ne([ 1, -1 ], [ q[2], q[4] ], -2); constraint int_lin_ne([ 1, -1 ], [ q[3], q[4] ], 1); constraint int_ne(q[3], q[4]); constraint int_lin_ne([ 1, -1 ], [ q[3], q[4] ], -1); solve satisfy;
A FlatZinc state Queen4State
representing the program above can be
constructed by typing:
| ?- fzn_load_file(library('zinc/examples/queen4'), Queen4State).
The predicates presented next are used to query an already initialized FlatZinc state.
fzn_post(
+FznState)
fzn_solve(
+FznState)
fzn_output(
+FznState)
output_var/0
or output_array/1
.
Exceptions: An instatiation error if the output variables are not instantiated.
Consider again the FlatZinc program queen4.fzn
described above
and the following goal at the Prolog top level:
| ?- fzn_load_file(library('zinc/examples/queen4'), Queen4State), fzn_post(Queen4State), fzn_solve(Queen4State), fzn_output(Queen4State).
The first line initializes Queen4State
with respect to
queen4.fzn
. The second and third line posts the constraints of
queen4.fzn
and runs the solve part of queen4.fzn
,
respectively. Finally, the fourth line runs the output part of
queen4.fzn
which means that the following is written on the
current output stream:
q = array1d(1..4, [2, 4, 1, 3]); ----------
Upon backtracking the solve and output parts of Queen4State
are
rerun, which means that the following is written on the current output
stream:
q = array1d(1..4, [3, 1, 4, 2]); ----------
fzn_identifier(
+FznState,
+Id,
-Value)
bool
is translated into a Prolog integer:
false
is translated into 0
and true
is translated
into 1
.
int
is translated into a Prolog integer.
float
is translated into a Prolog float.
library(clpfd)
FD set term (see FD Set Operations).
var int
is translated into a library(clpfd)
domain
variable (see CLPFD Interface).
var bool
is translated into a library(clpfd)
domain
variable with the domain 0..1
(see CLPFD Interface).
Exceptions: An existence error if Id is not an
identifier of FznState.
fzn_objective(
+FznState,
-Objective)
Exceptions: An existence error if there is no objective in FznState.
A possible use of fzn_identifier/3
is to post additional
library(clpfd)
constraints or to apply a Prolog labeling
predicate on the FlatZinc variables. For example, given the 4 Queens
problem in queen4.fzn
described above, the following goal labels
the variables to find all solutions:
| ?- fzn_load_file(library('zinc/examples/queen4'), Queen4State), fzn_post(Queen4State), fzn_identifier(Queen4State, q, Q), findall(_, (labeling([], Q), fzn_output(Queen4State)), _).
Given this goal, the following is written on the current output stream:
q = array1d(1..4, [2, 4, 1, 3]); ---------- q = array1d(1..4, [3, 1, 4, 2]); ----------
To avoid symmetric solutions where the chess board is rotated 180 degrees, the following goal posts an additional symmetry breaking constraint on the first two queens:
| ?- fzn_load_file(library('zinc/examples/queen4'), Queen4State), fzn_post(Queen4State), fzn_identifier(Queen4State, q, Q), Q = [Q1, Q2|_], Q1 #< Q2, findall(_, (labeling([], Q), fzn_output(Queen4State)), _).
Given this goal, the following is written on the current output stream:
q = array1d(1..4, [2, 4, 1, 3]); ----------
Note that, now, only the first one of the previous two solutions is displayed.
The following two predicates can be used to run a FlatZinc program in one go. They both take as optional argument a list Options which can be used to change the default behavior of the execution. This list may contain zero or more of the following:
search(
Method)
since release 4.3bab
and
restart
. Tells the solver which optimization algorithm to use:
branch-and-bound (the default), or to restart the search each time a new
solution is found. The corresponding spfz option is
-search Method.
solutions(
NumberOfSolutions)
all
. Describes the number of solutions to search
for; the default is 1. The corresponding spfz options are
-n N and -a.
output(
File)
ozn_file(
File)
since release 4.2.3statistics(
Boolean)
true
or false
(default).
The corresponding spfz option is -s.
If true
, the following statistics are written on the current output
stream (see the built-in statistics/[0,2]
and
fd_statistics/[0,2]
of library(clpfd)
for more detailed
information on their meaning):
runtime
solvetime
solutions
constraints
backtracks
prunings
timeout(
Time)
fzn_run_stream(
+FznStream)
fzn_run_stream(
+FznStream,
+Options)
fzn_load_stream/2
), initializing a
FlatZinc state.
fzn_post/1
).
fzn_solve/1
).
output_var/0
or output_array/1
.
The two final steps are repeated until the number of solutions as specified in Options have been found or until no more solutions can be found. At this point, if the whole search space have been explored ten consecutive equal signs are output on a separate line.
Exceptions:
all
.
fzn_run_file(
+FznFile)
fzn_run_file(
+FznFile,
+Options)
fzn_run_stream/[1,2]
handling
stream opening and closing.
Exceptions:
all
.
The next predicate can be used to write the constraints of a FlatZinc
program to a file, in the format of library(clpfd)
.
fzn_dump(
+FznState,
+File)
fzn_dump(
+FznState,
+Options,
+File)
library(clpfd)
.
Options is a list containing zero or more of the following (currently, this is the only available option):
variables(
ListOfVarDef)
query/1
that is written to File. Default is
ListOfVarDef=[vars=Vars]
, with the meaning that Vars
is a list containing all variables of the FlatZinc state, in the order
they were introduced.
Exceptions: Exceptions related to the opening of File for writing.
Consider again the FlatZinc program queen4.fzn
described above
and the following goal at the Prolog top level:
| ?- fzn_load_file(library('zinc/examples/queen4'), Queen4State), fzn_dump(Queen4State, [variables([q=Q])], queen4).
The file queen4.pl
then contains the following:
queen4.pl:- use_module(library(clpfd)). query([q=[A,B,C,D]]) :- true, domain([A,B,C,D], 1, 4), scalar_product([1,-1], [A,B], #\=, -1), scalar_product([1,-1], [A,B], #\=, 1), scalar_product([1,-1], [A,C], #\=, -2), scalar_product([1,-1], [A,C], #\=, 2), scalar_product([1,-1], [A,D], #\=, -3), scalar_product([1,-1], [A,D], #\=, 3), scalar_product([1,-1], [B,C], #\=, -1), scalar_product([1,-1], [B,C], #\=, 1), scalar_product([1,-1], [B,D], #\=, -2), scalar_product([1,-1], [B,D], #\=, 2), scalar_product([1,-1], [C,D], #\=, -1), scalar_product([1,-1], [C,D], #\=, 1), A#\=B, A#\=C, A#\=D, B#\=C, B#\=D, C#\=D.