union-find in progress

parent faf830a5
......@@ -131,6 +131,6 @@ let build_maze (n:int) =
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/vacid_0_union_find"
compile-command: "unset LANG; make -C ../.. examples/programs/vacid_0_build_maze"
End:
*)
{
type uf
use array.ArrayLength as A
logic repr(uf, int) : int
logic size(uf) : int
logic num (uf) : int
type 'a array = 'a A.t
logic same(u:uf, x:int, y:int) = repr(u, x) = repr(u, y)
logic (#)(a : 'a array, i : int) : 'a = A.select(a, i)
axiom OneClass :
forall u:uf. num(u) = 1 ->
forall x,y:int. 0 <= x < size(u) -> 0 <= y < size(u) -> same(u, x, y)
type uf = (* link: *) int array *
(* dist: *) int array * (* distance to representative *)
(* size: *) int *
(* num : *) int
}
logic link(u : uf) : int array = let (l, _, _, _) = u in l
logic dist(u : uf) : int array = let (_, d, _, _) = u in d
logic size(u : uf) : int = let (_, _, s, _) = u in s
logic num (u : uf) : int = let (_, _, _, n) = u in n
parameter create :
n:int ->
{ 0 <= n }
uf ref
{ num(!result) = n and size(!result) = n and
forall x:int. 0 <= x < n -> repr(!result, x) = x }
parameter find :
u:uf ref -> x:int ->
{ 0 <= x < size(!u) }
int writes u
{ result = repr(!u, x) and
size(!u) = size(old(!u)) and num(!u) = num(old(!u)) and
forall x:int. 0 <= x < size(!u) -> repr(!u, x) = repr(old(!u), x) }
parameter union :
u:uf ref -> a:int -> b:int ->
{ 0 <= a < size(!u) and 0 <= b < size(!u) and not same(!u, a, b) }
unit writes u
{ same(!u, a, b) and
size(!u) = size(old(!u)) and num(!u) = num(old(!u)) - 1 and
forall x,y:int. 0 <= x < size(!u) -> 0 <= y < size(!u) ->
same(!u, x, y) <->
same(old(!u), x, y) or
same(old(!u), x, a) and same(old(!u), b, y) or
same(old(!u), x, b) and same(old(!u), a, y) }
parameter get_num_classes :
u:uf ref -> {} int reads u { result = num(!u) }
parameter rand : s:int -> {} int { 0 <= result < s }
logic inv(u : uf) =
let (l, d, s, n) = u in
(forall i:int. 0 <= i < s -> 0 <= l#i < s) and
(forall i:int. 0 <= i < s ->
(d#i = 0 and l#i = i or d#i > 0 and d#(l#i) = d#i - 1))
{
axiom Ineq1 :
forall n,x,y:int. 0 <= n -> 0 <= x < n -> 0 <= y < n -> 0 <= x*n+y < n*n
}
logic repr(u:uf, x:int) : int =
let l = link(u) in
let y = l#x in
if y = x then y else repr(u, y)
{
type graph
(*clone import graph.Path with type graph = graph, type vertex = int*)
logic path(graph, int, int)
logic same(u:uf, x:int, y:int) = repr(u, x) = repr(u, y)
axiom Path_refl : forall g:graph, x:int. path(g, x, x)
axiom Path_sym : forall g:graph, x,y:int. path(g, x, y) -> path(g, y, x)
axiom Path_trans:
forall g:graph, x,y,z:int. path(g, x, y) -> path(g, y, z) -> path(g, x, z)
axiom OneClass :
forall u:uf. num(u) = 1 ->
forall x,y:int. 0 <= x < size(u) -> 0 <= y < size(u) -> same(u, x, y)
logic select(d:int, x:'a, y:'a) : 'a = if d = 0 then x else y
}
parameter graph : graph ref
parameter num_edges : int ref
parameter add_edge :
a:int -> b:int ->
{ not path(!graph, a, b) }
unit writes num_edges, graph
{ !num_edges = old(!num_edges) + 1 and
(forall x,y:int.
path(!graph, x, y) <->
path(old(!graph), x, y) or
path(old(!graph), x, a) and path(old(!graph), b, y) or
path(old(!graph), x, b) and path(old(!graph), a, y))
}
let add_edge_and_union (u:uf ref) (a:int) (b:int) =
{ 0 <= a < size(!u) and 0 <= b < size(!u) and
not same(!u, a,b) and not path(!graph, a, b) and
forall x,y:int.
0 <= x < size(!u) -> 0 <= y < size(!u) ->
same(!u, x, y) <-> path(!graph, x, y)
}
add_edge a b;
union u a b
{ !num_edges = old(!num_edges) + 1 and
let get_num_classes (u:uf ref) =
{} num !u { result = num(!u) }
let create (n:int) =
{ 0 <= n }
let l = ref (A.const_length 0 n) in
let i = ref 0 in
while !i < n do
invariant { 0 <= !i <= n and
forall j:int. 0 <= j < !i -> !l#j = j }
variant { n - !i }
l := A.store !l !i !i;
i := !i + 1
done;
ref ((!l, A.const_length 0 n, n, n))
{ inv(!result) and
num(!result) = n and size(!result) = n and
forall x:int. 0 <= x < n -> repr(!result, x) = x }
let find (u:uf ref) (x:int) =
{ inv(!u) and 0 <= x < size(!u) }
let l = link !u in
let y = ref x in
while A.select l !y <> !y do
invariant { 0 <= !y < size(!u) and same(!u, x, !y) }
variant { dist(!u) # !y }
y := A.select l !y
done;
!y
{ inv(!u) and
result = repr(!u, x) and
size(!u) = size(old(!u)) and num(!u) = num(old(!u)) and
forall x:int. 0 <= x < size(!u) -> repr(!u, x) = repr(old(!u), x) }
parameter ghost_find : u:uf ref -> x:int ->
{ inv(!u) and 0 <= x < size(!u) }
int reads u
{ result = repr(!u, x) }
let increment (u : uf ref) (r : int) =
{ inv(!u) and 0 <= r < size(!u) }
let i = ref 0 in
let d = ref (dist !u) in
while !i < size !u do
invariant { 0 <= !i <= size(!u) and
forall j:int. 0 <= j < size(!u) ->
!d#j = dist(!u)#j +
if repr(!u, j) = r and j < !i then 1 else 0 }
variant { size(!u) - !i }
if ghost_find u !i = r then
d := A.store !d !i (A.select !d !i + 1)
done;
!d
{ forall i:int. 0 <= i < size(!u) ->
result#i = dist(!u)#i + if repr(!u, i) = r then 1 else 0 }
let union (u:uf ref) (a:int) (b:int) =
{ inv(!u) and
0 <= a < size(!u) and 0 <= b < size(!u) and not same(!u, a, b) }
let ra = find u a in
let rb = find u b in
let l = link !u in
let d = increment u ra in
u := (A.store l ra rb, d, size !u, num !u - 1)
{ inv(!u) and
same(!u, a, b) and
size(!u) = size(old(!u)) and num(!u) = num(old(!u)) - 1 and
(forall x,y:int.
0 <= x < size(!u) -> 0 <= y < size(!u) ->
same(!u, x, y) <-> path(!graph, x, y))
}
let build_maze (n:int) =
{ 1 <= n and
!num_edges = 0 and
forall x,y:int. x<>y -> not path(!graph, x, y)
}
let u = create (n*n) in
while get_num_classes u > 1 do
invariant
{ 1 <= num(!u) and num(!u) + !num_edges = size(!u) = n*n and
forall x,y:int. 0 <= x < n*n -> 0 <= y < n*n ->
same(!u, x, y) <-> path(!graph, x, y)
}
let x = rand n in
let y = rand n in
(*let d = rand 2 in*)
let w = x+1 (* select d (x+1) x *) (*if d = 0 then x+1 else x *) in
let z = y (* select d y (y+1) *) (*if d = 0 then y else y+1*) in
if andb (w < n) (z < n) then (* TODO && *) begin
let a = y * n + x in
assert { 0 <= a < n*n };
let b = w * n + z in
assert { 0 <= b < n*n };
if find u a <> find u b then
add_edge_and_union u a b
end
done
{ !num_edges = n*n-1 and
forall x,y:int. 0 <= x < n*n -> 0 <= y < n*n ->
path(!graph, x, y) }
forall x,y:int. 0 <= x < size(!u) -> 0 <= y < size(!u) ->
same(!u, x, y) <->
same(old(!u), x, y) or
same(old(!u), x, a) and same(old(!u), b, y) or
same(old(!u), x, b) and same(old(!u), a, y) }
(*
Local Variables:
......
......@@ -55,6 +55,9 @@ theory ArrayLength
logic const_length('a, int) : 'a t
axiom Const_contents :
forall b:'a. forall n,i:int. select(const_length(b, n), i) = b
axiom Length_const :
forall a : 'a. forall n : int. length(const_length(a, n)) = n
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment