update b

zhezhouzz · Apr 13, 2022 · bf573ca · bf573ca
1 parent c7a14d2
commit bf573ca
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/data/client/batchedq/assertion1.ml b/data/client/batchedq/assertion1.ml
@@ -12,7 +12,7 @@ let sampling_rounds = 6
 let p_size = 4
 
 let pre (f : Batchedq.t) (r : Batchedq.t) =
-  uniq f && uniq r
+  uniq r
   && (not (empty f))
   && (not (empty r))
   && (not (size1 f))
@@ -21,7 +21,7 @@ let pre (f : Batchedq.t) (r : Batchedq.t) =
 let post (f : Batchedq.t) (r : Batchedq.t) (f' : Batchedq.t) (r' : Batchedq.t)
     (u : int) =
   iff (mem f' u || mem r' u || hd f u) (mem f u || mem r u)
-  && implies (last r u) (hd f' u)
+  (* && implies (last r u) (hd f' u) *)
   (* && implies *)
   (*      (not (hd f u)) *)
   (*      (iff *)

diff --git a/data/client/batchedq/tail.ml b/data/client/batchedq/tail.ml
@@ -5,4 +5,4 @@ let tail (f : Batchedq.t) (r : Batchedq.t) =
   | _ when (Batchedq.nil, (r0 : Batchedq.t)) -> raise Empty
   | _ when (Batchedq.cons (x : int) (f1 : Batchedq.t), (r1 : Batchedq.t)) ->
       if Batchedq.is_empty f1 then (Batchedq.rev r1, f1)
-      else (f1, Batchedq.rev r1)
+      else (Batchedq.cons x Batchedq.nil, r1)