Reorganise some stuff

formalsec · Aug 3, 2024 · 2bcdf49 · 2bcdf49
1 parent 2b1d34d
commit 2bcdf49
Show file tree

Hide file tree

Showing 32 changed files with 48 additions and 44 deletions.
diff --git a/example/dune b/example/dune
@@ -6,4 +6,4 @@
  (enabled_if %{lib-available:z3})
  (deps
   ./product_mix.exe
-  (source_tree test)))
+  (source_tree in)))
diff --git a/example/test/teste01.in → example/in/teste01.in b/example/test/teste01.in → example/in/teste01.in
diff --git a/example/test/teste02.in → example/in/teste02.in b/example/test/teste02.in → example/in/teste02.in
diff --git a/example/test/teste03.in → example/in/teste03.in b/example/test/teste03.in → example/in/teste03.in
diff --git a/example/test/teste04.in → example/in/teste04.in b/example/test/teste04.in → example/in/teste04.in
diff --git a/example/test/teste05.in → example/in/teste05.in b/example/test/teste05.in → example/in/teste05.in
diff --git a/example/test/teste06.in → example/in/teste06.in b/example/test/teste06.in → example/in/teste06.in
diff --git a/example/test/teste07.in → example/in/teste07.in b/example/test/teste07.in → example/in/teste07.in
diff --git a/example/test/teste08.in → example/in/teste08.in b/example/test/teste08.in → example/in/teste08.in
diff --git a/example/test/teste09.in → example/in/teste09.in b/example/test/teste09.in → example/in/teste09.in
diff --git a/example/test/teste10.in → example/in/teste10.in b/example/test/teste10.in → example/in/teste10.in
diff --git a/example/test/teste11.in → example/in/teste11.in b/example/test/teste11.in → example/in/teste11.in
diff --git a/example/test/teste12.in → example/in/teste12.in b/example/test/teste12.in → example/in/teste12.in
diff --git a/example/product_mix.t b/example/product_mix.t
@@ -1,25 +1,25 @@
 Tests Product Mix:
-  $ ./product_mix.exe < test/teste01.in
+  $ ./product_mix.exe < in/teste01.in
   6440
-  $ ./product_mix.exe < test/teste02.in
+  $ ./product_mix.exe < in/teste02.in
   750
-  $ ./product_mix.exe < test/teste03.in
+  $ ./product_mix.exe < in/teste03.in
   50
-  $ ./product_mix.exe < test/teste04.in
+  $ ./product_mix.exe < in/teste04.in
   60
-  $ ./product_mix.exe < test/teste05.in
+  $ ./product_mix.exe < in/teste05.in
   56
-  $ ./product_mix.exe < test/teste06.in
+  $ ./product_mix.exe < in/teste06.in
   55
-  $ ./product_mix.exe < test/teste07.in
+  $ ./product_mix.exe < in/teste07.in
   40
-  $ ./product_mix.exe < test/teste08.in
+  $ ./product_mix.exe < in/teste08.in
   60
-  $ ./product_mix.exe < test/teste09.in
+  $ ./product_mix.exe < in/teste09.in
   95
-  $ ./product_mix.exe < test/teste10.in
+  $ ./product_mix.exe < in/teste10.in
   215
-  $ ./product_mix.exe < test/teste11.in
+  $ ./product_mix.exe < in/teste11.in
   4204
-  $ ./product_mix.exe < test/teste12.in
+  $ ./product_mix.exe < in/teste12.in
   0
diff --git a/test/dune → test/solver/dune b/test/dune → test/solver/dune
diff --git a/test/test_bitwuzla.expected → test/solver/test_bitwuzla.expected b/test/test_bitwuzla.expected → test/solver/test_bitwuzla.expected
diff --git a/test/solver/test_bitwuzla.ml b/test/solver/test_bitwuzla.ml
@@ -0,0 +1,10 @@
+open Smtml
+open Smtml_tests
+
+let () =
+  assert Bitwuzla_mappings.is_available;
+  let module Test_solver_params =
+    Test_solver_params.Make (Bitwuzla_mappings.Fresh.Make ()) in
+  let module Test_bv = Test_bv.Make (Bitwuzla_mappings) in
+  let module Test_fp = Test_fp.Make (Bitwuzla_mappings) in
+  ()
diff --git a/test/test_bv.ml → test/solver/test_bv.ml b/test/test_bv.ml → test/solver/test_bv.ml
diff --git a/test/test_colibri2.expected → test/solver/test_colibri2.expected b/test/test_colibri2.expected → test/solver/test_colibri2.expected
diff --git a/test/solver/test_colibri2.ml b/test/solver/test_colibri2.ml
@@ -0,0 +1,11 @@
+open Smtml
+open Smtml_tests
+
+let () =
+  assert Colibri2_mappings.is_available;
+  let module Test_solver_params = Test_solver_params.Make (Colibri2_mappings) in
+  let module Test_solver = Test_solver.Make (Colibri2_mappings) in
+  let module Test_bv = Test_bv.Make (Colibri2_mappings) in
+  let module Test_fp = Test_fp.Make (Colibri2_mappings) in
+  let module Test_lia = Test_lia.Make (Colibri2_mappings) in
+  ()
diff --git a/test/test_fp.ml → test/solver/test_fp.ml b/test/test_fp.ml → test/solver/test_fp.ml
diff --git a/test/test_harness.ml → test/solver/test_harness.ml b/test/test_harness.ml → test/solver/test_harness.ml
diff --git a/test/test_lia.ml → test/solver/test_lia.ml b/test/test_lia.ml → test/solver/test_lia.ml
diff --git a/test/test_lra.ml → test/solver/test_lra.ml b/test/test_lra.ml → test/solver/test_lra.ml
diff --git a/test/test_optimizer.ml → test/solver/test_optimizer.ml b/test/test_optimizer.ml → test/solver/test_optimizer.ml
diff --git a/test/test_solver.ml → test/solver/test_solver.ml b/test/test_solver.ml → test/solver/test_solver.ml
diff --git a/test/test_solver_params.ml → test/solver/test_solver_params.ml b/test/test_solver_params.ml → test/solver/test_solver_params.ml
diff --git a/test/test_z3.expected → test/solver/test_z3.expected b/test/test_z3.expected → test/solver/test_z3.expected
diff --git a/test/solver/test_z3.ml b/test/solver/test_z3.ml
@@ -0,0 +1,14 @@
+open Smtml
+open Smtml_tests
+
+let () =
+  assert Z3_mappings.is_available;
+  let module Test_solver_params =
+    Test_solver_params.Make (Z3_mappings.Fresh.Make ()) in
+  let module Test_solver = Test_solver.Make (Z3_mappings.Fresh.Make ()) in
+  let module Test_optimizer = Test_optimizer.Make (Z3_mappings.Fresh.Make ()) in
+  let module Test_bv = Test_bv.Make (Z3_mappings.Fresh.Make ()) in
+  let module Test_fp = Test_fp.Make (Z3_mappings.Fresh.Make ()) in
+  let module Test_lia = Test_lia.Make (Z3_mappings.Fresh.Make ()) in
+  let module Test_lra = Test_lra.Make (Z3_mappings.Fresh.Make ()) in
+  ()
diff --git a/test/test_bitwuzla.ml b/test/test_bitwuzla.ml
diff --git a/test/test_colibri2.ml b/test/test_colibri2.ml
diff --git a/test/test_z3.ml b/test/test_z3.ml