functor
import FD FS
export SolutionPredicate
define
fun {SolutionPredicate Desc}
proc {$ Info}
{New Solver init(Desc Info) _}
end
end
fun {MakeNode I Vars}
[Eq Down Up Side] = {FS.var.list.decl 4}
EqDown = {FS.union Eq Down}
EqUp = {FS.union Eq Up}
in
{FS.partition [Eq Down Up Side] Vars}
{FS.include I Eq}
node(
eq : Eq
down : Down
up : Up
side : Side
eqdown : EqDown
equp : EqUp
daughters : _)
end
proc {Equal N1 N2} N1=N2 end
proc {NotEqual N1 N2}
{FS.disjoint N1.eq N2.eq}
end
proc {Above N1 N2}
{FS.subset N2.eqdown N1.down}
{FS.subset N1.equp N2.up}
{FS.subset N1.side N2.side}
end
proc {NotAbove N1 N2}
{FS.disjoint N1.eq N2.up}
{FS.disjoint N2.eq N1.down}
end
proc {Disjoint N1 N2}
{FS.subset N1.eqdown N2.side}
{FS.subset N2.eqdown N1.side}
end
proc {NotDisjoint N1 N2}
{FS.disjoint N1.eq N2.side}
{FS.disjoint N2.eq N1.side}
end
proc {Clauses N1 N2 C}
thread or {Equal N1 N2} C=1 [] C\=:1 {NotEqual N1 N2} end end
thread or {Above N1 N2} C=2 [] C\=:2 {NotAbove N1 N2} end end
thread or {Above N2 N1} C=3 [] C\=:3 {NotAbove N2 N1} end end
thread or {Disjoint N1 N2} C=4 [] C\=:4 {NotDisjoint N1 N2} end end
end
class Solver
attr counter:0 var2int int2node vars labs choices
meth init(Desc Info)
var2int <- {NewDictionary}
int2node <- {NewDictionary}
vars <- {FS.var.decl}
labs <- {FS.var.decl}
choices <- {NewDictionary}
for D in Desc do {self D} end
{CloseSet @vars}
{CloseSet @labs}
{self info(Info)}
for I in 1..@counter do
for J in 1..(I-1) do
{Clauses @int2node.I @int2node.J @choices.(I*1000+J)}
end
end
{FD.distribute ff {Dictionary.items @choices}}
end
meth var2node(X Node)
I = {Dictionary.condGet @var2int X unit}
in
if I==unit then
I=(counter<-I)+1
in
{FS.include I @vars}
Node={MakeNode I @vars}
@var2int.X := I
@int2node.I := Node
for J in 1..(I-1) do
@choices.(I*1000+J) := {FD.int 1#4}
end
else Node=@int2node.I end
end
meth lab(X R)
N = {self var2node(X $)}
in
N.daughters =
{Record.map R fun {$ Xi} {self var2node(Xi $)} end}
{FS.partition
{Record.map N.daughters
fun {$ Ni}
Ni.up = N.equp
Ni.eqdown
end}
N.down}
{FS.include @var2int.X @labs}
end
meth dom(X R Y)
{self var2node(X _)}
{self var2node(Y _)}
I = @var2int.X
J = @var2int.Y
in
if I==J then 1::{Encode R}
elseif I>J then
@choices.(I*1000+J)::{Encode R}
else
@choices.(J*1000+I)::{Encode {Inverse R}}
end
end
meth labeled(X)
N = {self var2node(X $)}
I = {FD.decl}
in
{FS.include I @labs}
{FS.include I N.eq}
end
meth info($)
Int2var = {NewDictionary}
in
{ForAll {Dictionary.entries @var2int}
proc {$ V#I} Int2var.I := V end}
{Record.mapInd {Dictionary.toRecord o @int2node}
fun {$ I N}
{AdjoinAt N var Int2var.I}
end}
end
end
proc {CloseSet S}
{FS.var.upperBound {FS.reflect.lowerBound S} S}
end
fun {Encode R}
case R
of eq then 1
[] above then 2
[] below then 3
[] side then 4
[] _|_ then {Map R Encode}
end
end
fun {Inverse R}
case R
of eq then eq
[] above then below
[] below then above
[] side then side
[] _|_ then {Map R Inverse}
end
end
end