More parametric tests and only run tests when z3 available

.github/workflows/build.yml

@@ -41,3 +41,6 @@ jobs:
 
       - name: Build
         run: opam exec -- dune build @install
+
+      - name: Test
+        run: opam exec -- dune runtest

example/dune

@@ -3,6 +3,7 @@
  (libraries smtml))
 
 (cram
+ (enabled_if %{lib-available:z3})
  (deps
   ./product_mix.exe
   (source_tree test)))

lib/optimizer.mli

@@ -16,4 +16,5 @@
 (* along with this program.  If not, see <https://www.gnu.org/licenses/>.  *)
 (***************************************************************************)
 
-include Optimizer_intf.Intf (** @inline *)
+(** @inline *)
+include Optimizer_intf.Intf

test/dune

@@ -6,13 +6,16 @@
   test_harness
   test_solver_params
   test_solver
-  test_lia)
+  test_lia
+  test_lra
+  test_optimizer)
  (libraries smtml))
 
 (test
  (name test_z3)
  (modules test_z3)
- (libraries smtml smtml_tests))
+ (libraries smtml smtml_tests)
+ (build_if %{lib-available:z3}))
 
 (test
  (name test_colibri2)

test/parser/dune

@@ -1,4 +1,5 @@
 (cram
+ (enabled_if %{lib-available:z3})
  (deps
   %{bin:smtml}
   test_core.smtml

test/regression/dune

@@ -1,4 +1,5 @@
 (cram
+ (enabled_if %{lib-available:z3})
  (deps %{bin:smtml} test_pr_71.smtml))
 
 (tests

test/test_lra.ml

@@ -0,0 +1,18 @@
+open Smtml
+
+module Make (M : Mappings_intf.S) = struct
+  module Solver = Solver.Batch (M)
+
+  let () =
+    let solver = Solver.create () in
+    assert (
+      let x = Expr.mk_symbol Symbol.("x" @: Ty_real) in
+      let y = Expr.mk_symbol Symbol.("y" @: Ty_real) in
+      let c0 = Expr.relop Ty_bool Eq x y in
+      let c1 =
+        Expr.relop Ty_bool Eq
+          (Expr.cvtop Ty_real ToString x)
+          (Expr.cvtop Ty_real ToString y)
+      in
+      `Sat = Solver.check solver [ c0; c1 ] )
+end

test/test_optimizer.ml

@@ -0,0 +1,15 @@
+open Smtml
+
+module Make (M : Mappings_intf.S) = struct
+  open Test_harness
+  module Optimizer = Optimizer.Make (M)
+
+  let () =
+    let open Infix in
+    let opt = Optimizer.create () in
+    let x = symbol "x" Ty_int in
+    Optimizer.add opt Int.[ x >= int 0; x < int 5 ];
+    Optimizer.protect opt (fun () ->
+        assert (Stdlib.(Some (Value.Int 0) = Optimizer.minimize opt x)) );
+    assert (Stdlib.(Some (Value.Int 4) = Optimizer.maximize opt x))
+end

test/test_z3.ml

@@ -5,6 +5,8 @@ let () = assert Z3_mappings.is_available
 
 module Test_solver_params = Test_solver_params.Make (Z3_mappings.Fresh.Make ())
 module Test_solver = Test_solver.Make (Z3_mappings.Fresh.Make ())
+module Test_optimizer = Test_optimizer.Make (Z3_mappings.Fresh.Make ())
 module Test_bv = Test_bv.Make (Z3_mappings.Fresh.Make ())
 module Test_fp = Test_fp.Make (Z3_mappings.Fresh.Make ())
 module Test_lia = Test_lia.Make (Z3_mappings.Fresh.Make ())
+module Test_lra = Test_lra.Make (Z3_mappings.Fresh.Make ())

test/unit/dune

@@ -1,8 +1,6 @@
 (tests
  (names
   test_expr_hc
-  test_optimizer
-  test_real
   test_simplify
   test_unop
   test_binop