vacid-0 union-find in progress

parent 901928f5
......@@ -7,6 +7,13 @@
logic size(uf) : int
logic num (uf) : int
logic same(u:uf, x:int, y:int) = repr(u, x) = repr(u, y)
axiom OneClass :
forall u:uf. num(u) = 1 ->
forall x,y:int. (* 0 <= x < size(u) -> 0 <= y < size(u) -> *)
repr(u, x) = repr(u, y)
}
parameter create :
......@@ -14,7 +21,7 @@ parameter create :
{ 0 <= n }
uf ref
{ num(!result) = n and size(!result) = n and
forall x:int. 0 <= x < n -> repr(!result, x) = x }
forall x:int. (* 0 <= x < n -> *) repr(!result, x) = x }
parameter find :
u:uf ref -> x:int ->
......@@ -22,18 +29,19 @@ parameter find :
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) }
forall x:int. (* 0 <= x < size(!u) -> *) repr(!u, x) = repr(old(!u), x) }
parameter union :
u:uf ref -> x:int -> y:int ->
{ repr(!u,x) <> repr(!u,y) }
u:uf ref -> a:int -> b:int ->
{ not same(!u, a, b) }
unit writes u
{ repr(!u, x) = repr(!u, y) and
{ same(!u, a, b) and
size(!u) = size(old(!u)) and num(!u) = num(old(!u)) - 1 and
forall z:int. 0 <= z < size(!u) ->
repr(!u, z) = repr(old(!u), z) or
repr(!u, z) = repr(!u, x) and repr(old(!u), z) = repr(old(!u), x) or
repr(!u, z) = repr(!u, y) and repr(old(!u), z) = repr(old(!u), 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) }
parameter get_num_classes :
u:uf ref -> {} int reads u { result = num(!u) }
......@@ -48,38 +56,109 @@ parameter rand : s:int -> {} int { 0 <= result < s }
{
type graph
clone import graph.Path with type graph = graph, type vertex = int
(*clone import graph.Path with type graph = graph, type vertex = int*)
logic path(graph, int, int)
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)
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 ->
{ }
unit writes graph
{ forall x,y:int. edge(!graph, x, y) <->
edge(old(!graph), x, y) or x=a and y=b or y=a and x=b }
{ 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) =
{ 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
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)) }
{
(***
lemma Main_lemma :
forall u1,u2:uf [size(u1),size(u2)]. forall g1,g2:graph, a,b:int.
(* 0 <= a < size(u1) -> 0 <= b < size(u1) -> *)
(forall x,y:int.
(* 0 <= x < size(u1) -> 0 <= y < size(u1) -> *)
same(u1, x, y) <-> path(g1, x, y)) ->
((* post union *)
size(u2) = size(u1) and
forall x,y:int. (* 0 <= x < size(u2) -> 0 <= y < size(u2) -> *)
same(u2, x, y) <->
same(u1, x, y) or
same(u1, x, a) and same(u1, b, y) or
same(u1, x, b) and same(u1, a, y)) ->
((* post add_edge *)
(forall x,y:int.
path(g2, x, y) <->
path(g1, x, y) or
path(g1, x, a) and path(g1, b, y) or
path(g1, x, b) and path(g1, a, y)) ) ->
(forall x,y:int.
(* 0 <= x < size(u2) -> 0 <= y < size(u2) -> *)
same(u2, x, y) <-> path(g2, x, y))
***)
}
let build_maze (n:int) =
{ 1 <= n }
{ 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 { size(!u) = n*n }
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 = if d = 0 then x+1 else x in
let z = if d = 0 then y+1 else y in
if if w < n then z < n else False then (* TODO && *) begin
(*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
let b = w * n + z in
if find u a <> find u b then begin
add_edge a b;
union u a b
(*add_edge a b;
union u a b;
assert { (forall x,y:int.
(* 0 <= x < size(!u) -> 0 <= y < size(!u) -> *)
same(!u, x, y) <-> path(!graph, x, y)) }*)
add_edge_and_union u a b
(*assert { repr(!u, a) = repr(!u, b) };*)
(*assert { path(!graph, a, b) }*)
end
end
done
{ }
{ !num_edges = n*n-1 and
forall x,y:int. (* 0 <= x < n*n -> 0 <= y < n*n -> *)
path(!graph, x, y) }
(*
Local Variables:
......
......@@ -35,7 +35,11 @@ let rec split_pos split_neg acc f =
| Ftrue -> acc
| Ffalse -> f::acc
| Fapp _ -> f::acc
| Fbinop (Fand,f1,f2) -> split_pos (split_pos acc f2) f1
| Fbinop (Fand,f1,f2) ->
(* split_pos (split_pos acc f2) f1 *)
let l2 = split_pos [] f2 in
let acc = List.fold_left (fun acc f -> f_implies f1 f :: acc) acc l2 in
split_pos acc f1
| Fbinop (Fimplies,f1,f2) ->
list_fold_product
(fun acc f1 f2 -> (f_implies f1 f2)::acc)
......
......@@ -10,6 +10,17 @@ theory Path
logic edge(graph, vertex, vertex)
inductive path(graph, vertex, vertex) =
| Path_empty :
forall g : graph, v : vertex. path(g, v, v)
| Path_append:
forall g : graph, v1,v2,src,dst : vertex.
path(g, src, v1) -> edge(g, v1, v2) -> path(g, v2, dst) ->
path(g, src, dst)
end
(*
inductive simple_path(graph, vertex, vertex list, vertex) =
| Path_empty :
forall g:graph, v:vertex. simple_path(g, v, Nil : vertex list, v)
......@@ -21,5 +32,4 @@ theory Path
logic simple_cycle(g : graph, v : vertex) =
exists l : vertex list. l <> Nil and simple_path(g, v, l, v)
end
*)
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