Previous: Node record, Up: Solver
In this section, we explain how you can write new principles. Principles must be written in Mozart/Oz. In order to write an principle, you need to provide two things:
You write the principle definition in the IL, and embed it into a
functor. The functor has to export the principle definition as
Principle, and has to reside in Solver/Principles.
We display an example principle definition functor of the graph
principle (Solver/Principles/Graph.oz) below:
%% Copyright 2001-2008
%% by Ralph Debusmann <rade@ps.uni-sb.de> (Saarland University) and
%% Denys Duchier <duchier@ps.uni-sb.de> (LIFO, Orleans) and
%% Jorge Marques Pelizzoni <jpeliz@icmc.usp.br> (ICMC, Sao Paulo) and
%% Jochen Setz <info@jochensetz.de> (Saarland University)
%%
functor
export
Principle
define
Principle =
elem(tag: principledef
id: elem(tag: constant
data: 'principle.graph')
dimensions: [elem(tag: variable
data: 'D')]
model:
elem(tag: 'type.record'
args:
[elem(tag: constant
data: 'mothers')#
elem(tag: 'type.ints')
%%
elem(tag: constant
data: 'daughters')#
elem(tag: 'type.ints')
%%
elem(tag: constant
data: 'up')#
elem(tag: 'type.ints')
%%
elem(tag: constant
data: 'down')#
elem(tag: 'type.ints')
%%
elem(tag: constant
data: 'eq')#
elem(tag: 'type.ints')
%%
elem(tag: constant
data: 'equp')#
elem(tag: 'type.ints')
%%
elem(tag: constant
data: 'eqdown')#
elem(tag: 'type.ints')
%%
elem(tag: constant
data: 'labels')#
elem(tag: 'type.set'
arg: elem(tag: 'type.labelref'
arg: elem(tag: variable
data: 'D')))
%%
elem(tag: constant
data: 'mothersL')#
elem(tag: 'type.vec'
arg1: elem(tag: 'type.labelref'
arg: elem(tag: variable
data: 'D'))
arg2: elem(tag: 'type.ints'))
%%
elem(tag: constant
data: 'daughtersL')#
elem(tag: 'type.vec'
arg1: elem(tag: 'type.labelref'
arg: elem(tag: variable
data: 'D'))
arg2: elem(tag: 'type.ints'))
%%
elem(tag: constant
data: 'upL')#
elem(tag: 'type.vec'
arg1: elem(tag: 'type.labelref'
arg: elem(tag: variable
data: 'D'))
arg2: elem(tag: 'type.ints'))
%%
elem(tag: constant
data: 'downL')#
elem(tag: 'type.vec'
arg1: elem(tag: 'type.labelref'
arg: elem(tag: variable
data: 'D'))
arg2: elem(tag: 'type.ints'))
])
constraints: [elem(tag: constant
data: 'GraphMakeNodes')#
elem(tag: integer
data: 130)
%%
elem(tag: constant
data: 'GraphConditions')#
elem(tag: integer
data: 120)
%%
elem(tag: constant
data: 'GraphMakeEdges')#
elem(tag: integer
data: 100)
%%
elem(tag: constant
data: 'GraphDist')#
elem(tag: integer
data: 90)
]
)
end
The value of the id feature is an IL constant representing the
unique principle identifier (here: 'principle.graph').
The value of the dimensions feature is a list of IL variables
representing the dimension variables introduced by the principle (here:
'D').
The value of the model feature is a list of IL pairs
representing the type of the model record introduced by the principle.
Here, the graph principle introduces the following features:
mothers (a set of integers)
daughters (a set of integers)
up (a set of integers)
down (a set of integers)
eq (a set of integers)
equp (a set of integers)
eqdown (a set of integers)
labels (a set of edge labels on dimension D)
mothersL (a mapping from edge labels on dimension D
to sets of integers)
daughtersL (a mapping from edge labels on dimension D
to sets of integers)
upL (a mapping from edge labels on dimension D
to sets of integers)
downL (a mapping from edge labels on dimension D
to sets of integers)
The value of the constraints feature is a list of pairs of an
IL constant and an IL integer, representing a mapping from constraint
functor file names (modulo the suffix .ozf) to their
priorities. Here, the constraint functor GraphMakeNodes has
priority 130, GraphConditions 120, GraphMakeEdges 100,
and GraphDist 90. The XDK solver invokes constraint functors
with higher priority first. Changing the priority of the constraint
functors can lead to less/more efficient solving.
The graph principle does not have any arguments. Therefore, we display
another example principle definition functor of the out principle
(Solver/Principles/Out.oz), since it does have an argument:
%% Copyright 2001-2008
%% by Ralph Debusmann <rade@ps.uni-sb.de> (Saarland University) and
%% Denys Duchier <duchier@ps.uni-sb.de> (LIFO, Orleans) and
%% Jorge Marques Pelizzoni <jpeliz@icmc.usp.br> (ICMC, Sao Paulo) and
%% Jochen Setz <info@jochensetz.de> (Saarland University)
%%
functor
export
Principle
define
Principle =
elem(tag: principledef
id: elem(tag: constant
data: 'principle.out')
dimensions: [elem(tag: variable
data: 'D')]
args: [elem(tag: variable
data: 'Out')#
elem(tag: 'type.valency'
arg: elem(tag: 'type.labelref'
arg: elem(tag: variable
data: 'D')))]
defaults: [elem(tag: variable
data: 'Out')#
elem(tag: featurepath
root: '_'
dimension: elem(tag: variable
data: 'D')
aspect: 'entry'
fields: [elem(tag: constant
data: 'out')])]
constraints: [elem(tag: constant
data: 'Out')#
elem(tag: integer
data: 130)])
end
Here, the principle identifier is 'principle.out', the dimension
variable is D, and the principle makes use of the constraint
functor Out with priority 130.
The value of the args feature is a list of IL pairs representing
the argument variables introduced by the principle and their types.
Here, the out principle introduces the argument Out (a valency of
edge labels on dimension D).
The value of the default feature is a list of IL pairs
representing the default values of a subset of the argument variables
introduced by the principle. Here, the default value of the Out
argument is a feature path.
To integrate the principle definition into the XDK, you can either
trust the perl-script scripts/addprinciple, or, by hand do the
following:
ozmake makefileSolver/Principles/makefile.oz
Solver/Principles/Principles.oz, and also to the list
Principles on top ofSolver/Principles/Principles.oz.
Solver/Principles/principles.xml. Here, for each new principle,
you add a line like the following for the graph principle:
<principleDef id="principle.graph"/>
This step is necessary because XML language grammar files contain only principle uses, but not principle definitions. Therefore, the principle identifiers of the used principles are only referred to but not defined in XML language grammar files, which leads to errors running an XML validator on them.
solver-principles_overview.texi and
solver-principles_list.texi
You write a constraint functor as an Oz functor exporting the
procedure Constraint: Nodes G Principle FD FS Select -> U.
Constraint has six arguments:
Nodes is a list of node records representing the solution
G is the current grammar
Principle is the current principle instantiation
FD is the FD functor (finite domain constraints)
FS is the FS functor (finite set constraints)
Select is the Select functor (selection constraints)
Principle is a record of the following type:
principle(pIDA: PIDA
modelLat: ModelLat
dVA2DIDA: DVA2DIDA
dIDAs: DIDAs
argRecProc: ArgRecProc
argsLat: ArgsLat
dIDA: DIDA
...)
where we omit the features modelTn, constraints,
edgeconstraints, dVA2DIDARec, argRec and
argsTn, which are irrelevant for writing constraint functors.
where the value of pIDA is the principle identifier (e.g.
principle.valency.
The value of modelLat is the lattice for the model record.
The value of dVA2DIDA is a function mapping dimension variables
to dimension identifiers.
The value of argRecProc is a function of type ArgRecProc:
A AXRec -> SL from a principle argument variable (A) and a
record (AXRec) to the argument value bound to the argument
variable.
The value of argsLat is the lattice for the argument record of
the principle.
The value of DIDA is the dimension identifier of the dimension
on which the principle is instantiated.
By convention, you should only access the argument values of a
principle use through the ArgRecProc function. The record
AXRec is a mapping from either Oz atom '_', '^', or 'ql' to
either a node record ('_' and '^') or an Oz atom representing an edge
label ('ql'). I.e., the record AXRec includes two mappings in
one record:
In a constraint functor, you usually posit constraints over all nodes.
In order to get a principle argument, you usually call
ArgRecProc providing only the mapping of root variable
'_' to the current node.
Here is an example of using ArgRecProc to get the value of the
Out argument of the out principle, taken from the constraint
functor implementing the out principle
(Solver/Principles/Lib/Out.oz):
for Node in Nodes do
LAOutMRec = {ArgRecProc 'Out' o('_': Node)}
in
...
end
Here, in a for loop, the constraint functor posits a constraint
over each node Node (in Nodes). The root variable '_' is
bound to Node in the call of the ArgRecProc function to
get the value of the argument variable Out for node
Node.
The functor Solver/Principles/Lib/Helpers.oz exports the
procedure CheckModel: V Nodes DIDAATups -> B. By convention,
CheckModel should be used to check whether all model record
features accessed in the constraint functor are actually present (in
order to prevent crashes of the XDK solver).
The CheckModel procedure has three arguments:
V: an Oz virtual string representing the file name of the
constraint functor invoking the CheckModel procedure. This way
the procedure knows in which constraint functor an error has occurred if
there is one.
Nodes: a list of node records representing the solution.
DIDAATups: a list of pairs DIDA#A of a dimension
identifier (DIDA) and an Oz atom (A).
The procedure returns true if for a node Node (in
Nodes), it is the case that for all pairs DIDA#A in
DIDAATups, the model record of the node (Node.DIDA.model)
has field A. If the model record lacks a
feature, it returns false and the procedure prints out a warning
to stderr.
By convention, you should call CheckModel before the constraint
functor actually posits constraints, and the constraint functor should
not posit any constraints if CheckModel returns false.
Here is an example of a use of the CheckModel procedure in the
constraint functor implementing the barriers principle
(Solver/Principles/Lib/Barriers.oz):
proc {Constraint Nodes G Principle}
DVA2DIDA = Principle.dVA2DIDA
ArgRecProc = Principle.argRecProc
%%
D1DIDA = {DVA2DIDA 'D1'}
D2DIDA = {DVA2DIDA 'D2'}
in
%% check features
if {Helpers.checkModel 'Barriers.oz' Nodes
[D2DIDA#down
D1DIDA#mothers
D2DIDA#up
D2DIDA#labels]} then
D2DownMs = {Map Nodes
fun {$ Node} Node.D2DIDA.model.down end}
%%
BlocksMs = {Map Nodes
fun {$ Node}
BlocksM = {ArgRecProc 'Blocks' o('_':Node)}
in
BlocksM
end}
in
for Node in Nodes do
%% get all nodes below my D1 mother on D2
%% down_D2_mothers_D1(v) =
%% union { down_D2(v') | v' in mothers_D1(v) }
D2DownD1MothersM =
{Select.union D2DownMs Node.D1DIDA.model.mothers}
%% from this set, keep only those nodes which are above me
%% these are then between my D1 mother and myself on D2
%% between(v) = down_D2_mothers_D1(v) intersect up_D2(v)
BetweenM =
{FS.intersect D2DownD1MothersM Node.D2DIDA.model.up}
%% get all edge labels which are blocked by the nodes in
%% between(v)
%% blocked(v) = union { blocks(v') | v' in between(v) }
BlockedLM = {Select.union BlocksMs BetweenM}
in
%% my incoming edge labels set must be disjoint from the
%% set of blocked labels.
%% labels_D2(v) disjoint blocked(v)
{FS.disjoint Node.D2DIDA.model.labels BlockedLM}
end
end
end
This constraint functor accesses the model record fields
mothers on dimension D1, and down, up and
labels on dimension D2. It makes use of the
CheckModel procedure to check this.
To integrate the constraint functor into the XDK, you can again either
trust the perl-script scripts/addprinciple, or by hand do the
following:
ozmake makefileSolver/Principles/Lib/makefile.oz
ozmake makefile makefile.oz in
order to include it in the ozmake package created for the XDK.