Next: Graph1Constraints, Previous: GraphDist, Up: Principles list
principle.graph1
D
{ mothers: ints
daughters: ints
up: ints
down: ints
index: int
eq: ints
equp: ints
eqdown: ints
labels: set(label(D))
daughtersL: vec(label(D) ints)}
GraphMakeNodes1 (priority 130),
GraphConditions1 (120), GraphMakeEdges1 (100) and
GraphDist (90)
The Graph1 principle introduces a model record with the following features for each node v:
mothers: set of mothers of v
daughters: set of daughters of v
up: set of nodes above v
down: set of nodes below v
index: index of v
eq: singleton set containing the index of v
equp: set of nodes equal or above v
eqdown: set of nodes equal or below v
labels: set of incoming edge labels of v
daughtersL: set of daughters of v over an edge
labeled l
The integers and sets of integers contain node indices.
The Graph1 principle states that D is a graph.
The only difference of the Graph1 principle and the Graph principle
(Graph) is that the Graph1 principle omits the model record
features mothersL, upL and downL, and thereby
improves solving efficiency. Most principles work in conjunction with
both principles, but some (e.g. the Valency principle
(Valency1)) do require the additional model record features of
the Graph principle (Graph). Each such principle clearly states
this particularity in its description in this document.
Here is the definition of the GraphMakeNodes1 constraint
functor:
%% 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
import
% System(show)
Helpers(checkModel) at 'Helpers.ozf'
export
Constraint
prepare
RecordForAll = Record.forAll
define
proc {Constraint Nodes G Principle FD FS Select}
DVA2DIDA = Principle.dVA2DIDA
in
if {Helpers.checkModel 'GraphMakeNodes.oz' Nodes nil} then
DIDA = {DVA2DIDA 'D'}
%%
NodeSetM = Nodes.1.nodeSet
in
for Node in Nodes do
IndexI = Node.index
Model = Node.DIDA.model
in
{FS.subset Model.mothers NodeSetM}
{FS.subset Model.daughters NodeSetM}
{FS.equal Model.eq {FS.value.singl IndexI}}
{FS.subset Model.up NodeSetM}
{FS.subset Model.equp NodeSetM}
{FS.subset Model.down NodeSetM}
{FS.subset Model.eqdown NodeSetM}
{RecordForAll Model.daughtersL proc {$ M} {FS.subset M NodeSetM} end}
%% daughters(v) = union{ daughters_l(v) | l in labels }
Model.daughters = {FS.unionN Model.daughtersL}
%% equp(v) = eq(v) union up(v)
Model.equp = {FS.union Model.eq Model.up}
%% eqdown(v) = eq(v) union down(v)
Model.eqdown = {FS.union Model.eq Model.down}
%% eq(v) = equp(v) intersect eqdown(v)
Model.eq = {FS.intersect Model.equp Model.eqdown}
end
end
end
end
Here is the definition of the GraphConditions1 constraint
functor:
%% 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
import
% System(show)
export
Constraint
prepare
ListToRecord = List.toRecord
define
proc {Constraint Nodes G Principle FD FS Select}
DVA2DIDA = Principle.dVA2DIDA
%%
DIDA = {DVA2DIDA 'D'}
%% get label lattice LabelLat
DIDA2LabelLat = G.dIDA2LabelLat
LabelLat = {DIDA2LabelLat DIDA}
LAs = LabelLat.constants
%%
Models = {Map Nodes fun {$ Node} Node.DIDA.model end}
%%
LADaughtersLMTups =
{Map LAs
fun {$ LA}
DaughtersLMs = {Map Models
fun {$ Model} Model.daughtersL.LA end}
DaughtersLM = {FS.unionN DaughtersLMs}
in
LA#DaughtersLM
end}
LADaughtersLMRec = {ListToRecord o LADaughtersLMTups}
%% get all eqdowns EqdownMs
EqdownMs = {Map Models fun {$ Model} Model.eqdown end}
%% get all equps EqupMs
EqupMs = {Map Models fun {$ Model} Model.equp end}
in
for Model in Models I in 1..{Length Models} do
%% down(v) = union{ eqdown(v') | v' in daughters(v) }
Model.down = {Select.union EqdownMs Model.daughters}
%% up(v) = union{ equp(v') | v' in mothers(v) }
Model.up = {Select.union EqupMs Model.mothers}
%% daughters(v)={v} => down(v)={v}
{FD.impl
{FS.reified.equal Model.daughters Model.eq}
{FS.reified.equal Model.down Model.eq} 1}
in
%% l in labels(v) iff v in { daughters_l(v') | v' in nodes }
for LA in LAs do
{FD.equi
{FS.reified.include {LabelLat.aI2I LA} Model.labels}
{FS.reified.include I LADaughtersLMRec.LA} 1}
end
end
end
end
Here is the definition of the GraphMakeEdges1 constraint
functor:
%% 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
import
% System(show)
Helpers(checkModel) at 'Helpers.ozf'
export
Constraint
define
proc {Constraint Nodes G Principle FD FS Select}
DVA2DIDA = Principle.dVA2DIDA
DIDA = {DVA2DIDA 'D'}
in
if {Helpers.checkModel 'GraphMakeEdges1.oz' Nodes
[DIDA#down
DIDA#up
DIDA#daughters
DIDA#mothers]} then
for Node1 in Nodes do
Model1 = Node1.DIDA.model
in
for Node2 in Nodes do
Model2 = Node2.DIDA.model
in
%% v2 in down(v1) iff v1 in up(v2)
{FD.equi
{FS.reified.include Node2.index Model1.down}
{FS.reified.include Node1.index Model2.up} 1}
%% v2 in daughters(v1) iff v1 in mothers(v2)
{FD.equi
{FS.reified.include Node2.index Model1.daughters}
{FS.reified.include Node1.index Model2.mothers} 1}
end
end
end
end
end