simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-10 05:03:59 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

details

Browse source
This commit is contained in:
Simon Cruanes 2021-02-15 13:54:35 -05:00
parent aea634ca8b
commit f0dd1b08e8
2 changed files with 4 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/arith/lra/simplex2.ml
View file

@ -404,10 +404,10 @@ module Make(Var: VAR)
assert Erat.(sum = zero); assert Erat.(sum = zero);
done; done;
() (* TODO: more *) ()
(* for internal checking *) (* for internal checking *)
let _check_invariants_internal self = let[@inline] _check_invariants_internal self =
if false (* FUDGE *) then _check_invariants self if false (* FUDGE *) then _check_invariants self
let[@inline] has_var_ (self:t) x : bool = V_map.mem x self.var_tbl let[@inline] has_var_ (self:t) x : bool = V_map.mem x self.var_tbl

3
src/arith/tests/test_simplex2.ml
View file

@ -277,7 +277,7 @@ let check_sound =
let ar = let ar =
Step.(rand_for 0 300) Step.(rand_for 0 300)
|> QC.set_collect (fun pb -> if check_steps pb then "sat" else "unsat") |> QC.set_collect (fun pb -> if check_steps pb then "sat" else "unsat")
|> QC.set_stats steps_stats (* |> QC.set_stats steps_stats *)
in in
QC.Test.make ~long_factor:10 ~count:500 ~name:"simplex2_sound" ar prop_sound QC.Test.make ~long_factor:10 ~count:500 ~name:"simplex2_sound" ar prop_sound
@ -287,6 +287,7 @@ let prop_invariants pb =
add_steps simplex pb ~f:(fun () -> Spl._check_invariants simplex); add_steps simplex pb ~f:(fun () -> Spl._check_invariants simplex);
Spl.check_exn simplex Spl.check_exn simplex
with Spl.E_unsat _ -> ()); with Spl.E_unsat _ -> ());
Spl._check_invariants simplex;
true true
let check_invariants = let check_invariants =