Add get_sat_model unit test

formalsec · Mar 5, 2025 · cea1d6f · cea1d6f
1 parent 627717d
commit cea1d6f
Show file tree

Hide file tree

Showing 7 changed files with 22 additions and 5 deletions.
diff --git a/test/solver/test_solver.ml b/test/solver/test_solver.ml
@@ -25,7 +25,7 @@ module Make (M : Mappings_intf.S) = struct
     test_default_params ();
     test_solver_params ()
 
-  let test_cached_solver () =
+  let test_cache_hits () =
     let solver = Cached.create ~logic:LIA () in
     let x = Infix.symbol "x" Ty_int in
     let c = Infix.(Int.(x >= int 0)) in
@@ -36,6 +36,19 @@ module Make (M : Mappings_intf.S) = struct
     assert (Cached.cache_misses () = 1);
     assert (Cached.cache_hits () = 2)
 
+  let test_cache_get_model () =
+    let open Infix in
+    let solver = Cached.create ~logic:LIA () in
+    let x = symbol "x" Ty_int in
+    let set = Expr.Set.of_list Int.[ x >= int 0; x < int 10 ] in
+    match Cached.get_sat_model solver set with
+    | `Model m -> Fmt.pr "%a@." (Model.pp ~no_values:false) m
+    | `Unsat | `Unknown -> assert false
+
+  let test_cached () =
+    test_cache_hits ();
+    test_cache_get_model ()
+
   let test () =
     let open Infix in
     let solver = Solver.create ~logic:LIA () in

diff --git a/test/solver/test_solver_altergo.expected b/test/solver/test_solver_altergo.expected
@@ -1,3 +1,5 @@
+(model
+  (x int 0))
 (model
   (w i32 4)
   (x i32 1)

diff --git a/test/solver/test_solver_altergo.ml b/test/solver/test_solver_altergo.ml
@@ -6,7 +6,7 @@ let () =
   assert Altergo_mappings.is_available;
   let module Alt_ergo = Test_solver.Make (Altergo_mappings.Fresh.Make ()) in
   Alt_ergo.test_params ();
-  Alt_ergo.test_cached_solver ();
+  Alt_ergo.test_cached ();
   Alt_ergo.test ();
   Alt_ergo.test_bv ();
   Alt_ergo.test_lia ()
diff --git a/test/solver/test_solver_colibri2.ml b/test/solver/test_solver_colibri2.ml
@@ -5,7 +5,7 @@ let () =
   assert Colibri2_mappings.is_available;
   let module C2 = Test_solver.Make (Colibri2_mappings) in
   C2.test_params ();
-  C2.test_cached_solver ();
+  C2.test_cached ();
   C2.test ();
   C2.test_bv ();
   C2.test_fp ();

diff --git a/test/solver/test_solver_cvc5.ml b/test/solver/test_solver_cvc5.ml
@@ -5,6 +5,6 @@ let () =
   assert Cvc5_mappings.is_available;
   let module Cvc5 = Test_solver.Make (Cvc5_mappings.Fresh.Make ()) in
   Cvc5.test_params ();
-  Cvc5.test_cached_solver ();
+  Cvc5.test_cached ();
   Cvc5.test ();
   Cvc5.test_bv ()
diff --git a/test/solver/test_solver_z3.expected b/test/solver/test_solver_z3.expected
@@ -1,3 +1,5 @@
+(model
+  (x int 0))
 (model
   (w i32 4)
   (x i32 1)

diff --git a/test/solver/test_solver_z3.ml b/test/solver/test_solver_z3.ml
@@ -8,7 +8,7 @@ let () =
   Z3_opt.test ();
   let module Z3 = Test_solver.Make (Z3_mappings) in
   Z3.test_params ();
-  Z3.test_cached_solver ();
+  Z3.test_cached ();
   Z3.test ();
   Z3.test_lia ();
   Z3.test_lra ();