[Tagset] Don't require a maximal size, add remove

examples/stdlib/tagset/why3session.xml

@@ -4,7 +4,6 @@
 <why3session shape_version="5">
 <prover id="0" name="Alt-Ergo" version="2.2.0" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="1" name="CVC4" version="1.6" timelimit="1" steplimit="0" memlimit="1000"/>
-<prover id="2" name="Z3" version="4.4.1" timelimit="1" steplimit="0" memlimit="1000"/>
 <file proved="true">
 <path name=".."/>
 <path name=".."/>
@@ -13,13 +12,8 @@
 <path name="mach"/>
 <path name="tagset.mlw"/>
 <theory name="TagSetIntf" proved="true">
- <goal name="VC t" expl="VC for t" proved="true">
- <proof prover="1"><result status="valid" time="0.08"/></proof>
- </goal>
  <goal name="VC iterator" expl="VC for iterator" proved="true">
- <proof prover="0" obsolete="true"><result status="unknown" time="0.01"/></proof>
  <proof prover="1"><result status="valid" time="0.05"/></proof>
- <proof prover="2" obsolete="true"><result status="timeout" time="1.00"/></proof>
  </goal>
 </theory>
 <theory name="TagSet" proved="true">
@@ -38,9 +32,15 @@
  <goal name="VC max_tags" expl="VC for max_tags" proved="true">
  <proof prover="1"><result status="valid" time="0.06"/></proof>
  </goal>
+ <goal name="VC resize" expl="VC for resize" proved="true">
+ <proof prover="1"><result status="valid" time="0.54"/></proof>
+ </goal>
  <goal name="VC add" expl="VC for add" proved="true">
  <proof prover="1"><result status="valid" time="0.28"/></proof>
  </goal>
+ <goal name="VC remove" expl="VC for remove" proved="true">
+ <proof prover="1"><result status="valid" time="0.92"/></proof>
+ </goal>
  <goal name="VC iterator" expl="VC for iterator" proved="true">
  <proof prover="1"><result status="valid" time="0.10"/></proof>
  </goal>
@@ -53,7 +53,7 @@
  <goal name="Iterator.VC next" expl="VC for next" proved="true">
  <transf name="split_vc" proved="true" >
   <goal name="VC next.0" expl="assertion" proved="true">
-  <proof prover="0"><result status="valid" time="0.02" steps="122"/></proof>
+  <proof prover="0"><result status="valid" time="0.02" steps="107"/></proof>
   </goal>
   <goal name="VC next.1" expl="index in array bounds" proved="true">
   <proof prover="1"><result status="valid" time="0.06"/></proof>

stdlib/mach/tagset.mlw

@@ -6,7 +6,7 @@ module S
   type key
 
   val function tag (k:key): Int63.int63
-      ensures { 0 <= result }
+      ensures { 0 <= result < Int63.max_int63 }
 
   axiom tag_correct: forall x y. tag x = tag y -> x = y
 
@@ -34,32 +34,30 @@ module TagSetIntf
 
   type t = abstract {
          mutable elts: S.set key;
-         max_tags_: int;
          mutable iterated: iteration_state;
        }
-   invariant { forall v. S.mem v elts -> tag v <= max_tags_ }
    by {
       elts = S.empty;
-      max_tags_ = 0;
       iterated = any iteration_state;
     }
 
-  val create (s:Int63.int63) (def:key) : t
-   requires { -1 <= s < Int63.max_int63 }
+  val create (default:key) : t
    ensures { result.elts = S.empty }
-   ensures { result.max_tags_ = s }
 
   val function mem (k: key) (h: t) : bool
    ensures { result = S.mem k h.elts }
 
   val function max_tags (h: t) : Int63.int63
-    ensures { result = h.max_tags_ }
+    ensures { forall v. S.mem v h.elts -> tag v <= result }
 
   val add (h: t) (k: key): unit
-    requires { tag k <= h.max_tags }
     ensures { h.elts = S.add k (old h.elts) }
     writes { h.elts, h.iterated }
 
+  val remove (h: t) (k: key): unit
+    ensures { h.elts = S.remove k (old h.elts) }
+    writes { h.elts, h.iterated }
+
   type iterator = abstract {
        iterating: iteration_state;
        mutable seen: S.set key;
@@ -101,6 +99,7 @@ end
 module TagSet
 
   use int.Int
+  use mach.int.MinMax63
   use import mach.int.Int63 as Int63
   use set.Fset as S
   use import mach.array.Array63 as Array
@@ -113,19 +112,16 @@ module TagSet
   clone import S as S with axiom tag_correct
 
   type iteration_state = mutable {
-       ghost max_tags_': int;
        ghost mutable elts': S.set key;
-       present: array bool;
-       value: array key;
+       mutable present: array bool;
+       mutable value: array key;
   }
-  invariant { forall v. S.mem v elts' -> tag v <= max_tags_'  }
+  invariant { forall v. S.mem v elts' -> tag v < present.length  }
   invariant { forall v. S.mem v elts' -> present[tag v] }
-  invariant { forall i. 0 <= i <= max_tags_' -> present[i] -> tag (value[i]) = i }
-  invariant { forall i. 0 <= i <= max_tags_' -> present[i] -> forall v. tag v = i -> S.mem v elts' }
-  invariant { present.length = max_tags_' + 1 }
-  invariant { value.length = max_tags_' + 1 }
+  invariant { forall i. 0 <= i < present.length -> present[i] -> tag (value[i]) = i }
+  invariant { forall i. 0 <= i < present.length -> present[i] -> forall v. tag v = i -> S.mem v elts' }
+  invariant { value.length = present.length }
   by {
-     max_tags_' = -1;
      elts' = S.empty;
      present = Array.make 0 false;
      value = Array.make 0 (any key);
@@ -133,26 +129,21 @@ module TagSet
 
   type t = {
          ghost mutable elts: S.set key;
-         ghost max_tags_: int;
          mutable iterated: iteration_state;
        }
-   invariant { max_tags_ = iterated.max_tags_' }
    invariant { elts = iterated.elts' }
 
-  let create (s:Int63.int63) (def:key) : t
-   requires { -1 <= s < Int63.max_int63 }
+  let create (def:key) : t
    ensures { result.elts = S.empty }
-   ensures { result.max_tags_ = s } =
+   =
    let iterated =  {
          elts' = S.empty;
-         max_tags_' = Int63.to_int s;
-         present = Array.make (s+1) false;
-         value = Array.make (s+1) def;
+         present = Array.make 8 false;
+         value = Array.make 8 def;
       }
    in
    {
       elts = S.empty;
-      max_tags_ = Int63.to_int s;
       iterated = iterated;
    }
 
@@ -161,25 +152,55 @@ module TagSet
      tag k < Array.length h.iterated.present && Array.(h.iterated.present[tag k])
 
   let function max_tags (h: t) : Int63.int63
-    ensures { result = h.max_tags_ } =
+    ensures { forall v. S.mem v h.elts -> tag v <= result } =
     Array.(length h.iterated.present) - 1
 
+  let resize (h:t) (k:key) : unit
+     ensures { tag k < Array.(length h.iterated.present) }
+    =
+    let len = tag k + 1 in
+    let n = Array.length h.iterated.value in
+    if len > n then begin
+    let nlen = (max len (2 * (min n (Int63.max_int / 2)))) in
+      let a = Array.(make nlen k) in
+      Array.blit h.iterated.value 0 a 0 n;
+      h.iterated.value <- a;
+      let b = Array.make nlen false in
+      Array.blit h.iterated.present 0 b 0 n;
+      h.iterated.present <- b
+    end
+
+
   let add (h: t) (k: key): unit
-    requires { tag k <= h.max_tags }
     ensures { h.elts = S.add k (old h.elts) }
-    writes { h.elts , h.iterated, h.iterated.present, h.iterated.value(*, h.iterated.elts'*) } =
+    writes { h.elts , h.iterated } =
+    resize h k;
     h.elts <- S.add k h.elts;
     h.iterated.elts' <- S.add k h.iterated.elts';
     h.iterated.present[tag k] <- true;
     h.iterated.value[tag k] <- k ;
     if false then
        h.iterated <- {
-           max_tags_' = h.iterated.max_tags_';
            elts' = h.iterated.elts';
            present = h.iterated.present;
            value = h.iterated.value;
          }
 
+  let remove (k: key) (h: t) : unit
+   ensures { h.elts = S.remove k h.elts } =
+    if tag k < Array.length h.iterated.present then begin
+        h.elts <- S.remove k h.elts;
+        h.iterated.elts' <- S.remove k h.iterated.elts';
+        Array.(h.iterated.present[tag k] <- false);
+    end;
+    if false then
+       h.iterated <- {
+           elts' = h.iterated.elts';
+           present = h.iterated.present;
+           value = h.iterated.value;
+         }
+
+
   type iterator = {
        iterating: iteration_state;
        ghost mutable seen: S.set key;
@@ -199,7 +220,6 @@ module TagSet
     all = S.empty;
     offset = 0;
     iterating =  {
-     max_tags_' = -1;
      elts' = S.empty;
      present = Array.make 0 false;
      value = Array.make 0 (any key);