feat(util): a Bitvec module, refactor testing

sidekick.opam

@@ -15,6 +15,7 @@ depends: [
   "containers" { >= "3.0" & < "4.0" }
   "iter" { >= "1.0" & < "2.0" }
   "ocaml" { >= "4.04" }
+  "zarith" { with-test }
   "alcotest" {with-test}
   "odoc" {with-doc}
 ]

src/lra/tests/dune

@@ -1,25 +1,15 @@
-(executable
- (name run_tests)
- (modules run_tests test_simplex2)
- (libraries containers sidekick.arith-lra
-            sidekick.zarith zarith iter alcotest qcheck)
- (flags :standard -warn-error -a+8 -color always))
 
-(alias
+(library
- (name runtest)
+  (name sidekick_test_simplex2)
- (locks /test)
+  (libraries zarith sidekick.arith-lra sidekick.util sidekick.zarith
- (package sidekick)
+             qcheck alcotest))
- (action
-   (progn
-     (run ./run_tests.exe alcotest) ; run regressions first
-     (run ./run_tests.exe qcheck --verbose))))
 
 (rule
-  (targets test_simplex2.ml)
+  (targets sidekick_test_simplex2.ml)
   (enabled_if (>= %{ocaml_version} 4.08.0))
   (action (copy test_simplex2.real.ml %{targets})))
 
 (rule
-  (targets test_simplex2.ml)
+  (targets sidekick_test_simplex2.ml)
   (enabled_if (< %{ocaml_version} 4.08.0))
   (action (with-stdout-to %{targets} (echo "let props=[];; let tests=\"simplex2\",[]"))))

src/mini-cc/tests/dune

@@ -1,7 +1,4 @@
-(tests
+(library
- (names tests)
+  (name sidekick_test_minicc)
- (libraries sidekick.mini-cc sidekick-base alcotest)
+  (libraries sidekick.mini-cc sidekick-base alcotest)
- (package sidekick-base)
+  (flags :standard -warn-error -a+8))
- (flags :standard -warn-error -a+8 -safe-string -color always)
- (locks /test)
- (modes native))

src/mini-cc/tests/sidekick_test_minicc.ml

@@ -40,7 +40,7 @@ module Setup() = struct
   let p t1 = app_l fun_p [t1]
 end
 
-let l = ref []
+let l : unit Alcotest.test_case list ref = ref []
 let mk_test name f =
   l := (name, `Quick, f) :: !l
 
@@ -165,5 +165,4 @@ let () = mk_test "test_reg_1" @@ fun () ->
   A.(check bool) "is-unsat" (CC.check_sat cc) false;
   ()
 
-(* run alcotest *)
+let tests = "mini-cc", List.rev !l
-let () = Alcotest.run "mini-cc-tests" ["mini-cc", List.rev !l]

src/tests/dune

@@ -0,0 +1,16 @@
+
+(executable
+ (name run_tests)
+ (modules run_tests)
+ (libraries containers alcotest qcheck sidekick.util
+            sidekick_test_simplex2 sidekick_test_util sidekick_test_minicc)
+ (flags :standard -warn-error -a+8 -color always))
+
+(alias
+ (name runtest)
+ (locks /test)
+ (package sidekick)
+ (action
+   (progn
+     (run ./run_tests.exe alcotest) ; run regressions first
+     (run ./run_tests.exe qcheck --verbose))))

src/tests/run_tests.ml

@@ -1,11 +1,15 @@
 
-let tests : unit Alcotest.test list = [
+let tests : unit Alcotest.test list =
-  Test_simplex2.tests;
+  List.flatten @@ [
-]
+    [Sidekick_test_simplex2.tests];
+    [Sidekick_test_minicc.tests];
+    Sidekick_test_util.tests;
+  ]
 
 let props =
   List.flatten
-    [ Test_simplex2.props;
+    [ Sidekick_test_simplex2.props;
+      Sidekick_test_util.props;
     ]
 
 let () =

src/util/Bitvec.ml

@@ -0,0 +1,59 @@
+
+module I32Vec = Vec
+type i32vec = int Vec.t
+
+type t = {
+  mutable chunks: bytes; (* TODO: use a in32vec with bigarray *)
+}
+
+let create () : t = {
+  chunks = Bytes.make 32 '\x00';
+}
+
+let n_bits_ = 8
+let i2c = Char.chr
+let c2i = Char.code
+
+(* from index to offset in bytes *)
+let[@inline] idx_bytes_ (i:int) : int = i lsr 3
+
+(* from index to offset in a single char *)
+let mask_ = 0b111
+
+(* number of bytes *)
+let[@inline] len_ (self:t) : int = Bytes.length self.chunks
+
+let[@inline never] resize_ self idx : unit =
+  let new_size =
+    min Sys.max_string_length
+      (max (idx+2) (let l = len_ self in l + 10 + l / 2))
+  in
+  let new_chunks = Bytes.make new_size (i2c 0) in
+  Bytes.blit self.chunks 0 new_chunks 0 (len_ self);
+  self.chunks <- new_chunks;
+  assert (len_ self > idx)
+
+let[@inline] ensure_size self i =
+  let idx = idx_bytes_ i in
+  if idx >= len_ self then (
+    resize_ self idx
+  )
+
+let[@inline] get self i : bool =
+  let idx = idx_bytes_ i in
+  let c = c2i (Bytes.get self.chunks idx) in
+  (c land (1 lsl (i land mask_))) <> 0
+
+let set self i b : unit =
+  let idx = idx_bytes_ i in
+  let c = c2i (Bytes.get self.chunks idx) in
+  let c =
+    if b
+    then c lor (1 lsl (i land mask_))
+    else c land (lnot (1 lsl (i land mask_)))
+  in
+  Bytes.set self.chunks idx (i2c c)
+
+let clear_all self =
+  Bytes.fill self.chunks 0 (len_ self) '\x00'
+

src/util/Bitvec.mli

@@ -0,0 +1,15 @@
+
+(** Bitvector *)
+
+type t
+
+val create : unit -> t
+
+val ensure_size : t -> int -> unit
+(** [ensure_size bv i] ensures that [i] is a valid index in [bv] *)
+
+val get : t -> int -> bool
+
+val set : t -> int -> bool -> unit
+
+val clear_all : t -> unit

src/util/Sidekick_util.ml

@@ -4,6 +4,7 @@ module Fmt = CCFormat
 
 module Util = Util
 module Vec = Vec
+module Bitvec = Bitvec
 module Log = Log
 module Backtrack_stack = Backtrack_stack
 module Backtrackable_tbl = Backtrackable_tbl

src/util/tests/dune

@@ -0,0 +1,5 @@
+
+(library
+  (name sidekick_test_util)
+  (flags :standard -warn-error -a+8 -open Sidekick_util)
+  (libraries qcheck alcotest sidekick.util))

src/util/tests/sidekick_test_util.ml

@@ -0,0 +1,5 @@
+
+let tests = [Test_bitvec.tests]
+
+let props = [
+]

src/util/tests/test_bitvec.ml

@@ -0,0 +1,30 @@
+
+module A = Alcotest
+
+let spf = Printf.sprintf
+let msgline line = spf "test at line %d" line
+let alco_mk name f = name, `Quick, f
+
+module BV = Bitvec
+
+let t1 = alco_mk "mkgetset" @@ fun () ->
+  let bv = BV.create() in
+  BV.ensure_size bv 200;
+  A.(check bool) (msgline __LINE__) false (BV.get bv 0);
+  A.(check bool) (msgline __LINE__) false (BV.get bv 1);
+  for i=30 to 150 do
+    A.(check bool) (msgline __LINE__) false (BV.get bv i);
+  done;
+
+  BV.set bv 25 true;
+  BV.set bv 1 true;
+  BV.set bv 127 true;
+  BV.set bv 126 true;
+  BV.set bv 126 false;
+
+  for i=0 to 150 do
+    A.(check bool) (msgline __LINE__) (i=1||i=25||i=127) (BV.get bv i);
+  done;
+  ()
+
+let tests = "bitvec", [t1]