fix(bstack): fix bug in n-levels

This commit is contained in:
Simon Cruanes 2019-02-01 21:25:50 -06:00
parent a2e177abe8
commit 91389d2b5e

View file

@ -8,7 +8,7 @@ type 'a t = {
let create() : _ t = {vec=Vec.create(); lvls=Vec.create()}
let[@inline] n_levels self : int = Vec.size self.vec
let[@inline] n_levels self : int = Vec.size self.lvls
let[@inline] push self x : unit =
Vec.push self.vec x
@ -21,9 +21,10 @@ let[@inline] push_if_nonzero_level self x : unit =
let[@inline] push_level (self:_ t) : unit =
Vec.push self.lvls (Vec.size self.vec)
let pop_levels (self:_ t) (n:int) ~f : unit =
if n > n_levels self then invalid_arg "Backtrack_stack.pop_levels";
if n > n_levels self then (
Error.errorf "Backtrack_stack.pop_levels %d (size: %d)" n (n_levels self);
);
if n > 0 then (
let new_lvl = n_levels self - n in
let i = Vec.get self.lvls new_lvl in