Add get_sat_model and improve model documentation

CHANGES.md

@@ -1,16 +1,20 @@
 ## Unreleased
 
 ### Added
+### Changed
+### Fixed
 
-- Add Bitvector library
+## v0.6.0
+
+### Added
+
+- Add `get_sat_model` function to fetch models from path conditions
 - Add `cache_hits` and `cache_misses` functions to cached solver
 - Add `Expr.Set.hash` as an alias to `Expr.Set.to_int`
 - optimize Expr.equal, cache Expr.simplify (@zapashcanon)
 - Add floating-point operator `Copysign` (Closes #185)
 - Add sign extension to operators with unsigned counter parts (Closes #207)
 
-### Changed
-
 ### Fixed
 
 - Bring back forall and exists quantifiers (Closes #200)

README.md

@@ -119,6 +119,9 @@ module Z3 :
     val check_set : t -> Expr.Set.t -> [ `Sat | `Unknown | `Unsat ]
     val get_value : t -> Expr.t -> Expr.t
     val model : ?symbols:Symbol.t list -> t -> Model.t option
+    val get_sat_model :
+      ?symbols:Symbol.t list ->
+      t -> Expr.Set.t -> [ `Model of Model.t | `Unknown | `Unsat ]
   end
 # let solver = Z3.create ();;
 val solver : Z3.t = <abstr>

doc/index.mld

@@ -48,6 +48,10 @@ module Z3 :
     val check_set : t -> Smtml.Expr.Set.t -> [ `Sat | `Unknown | `Unsat ]
     val get_value : t -> Smtml.Expr.t -> Smtml.Expr.t
     val model : ?symbols:Smtml.Symbol.t list -> t -> Smtml.Model.t option
+    val get_sat_model :
+      ?symbols:Smtml.Symbol.t list ->
+      t ->
+      Smtml.Expr.Set.t -> [ `Model of Smtml.Model.t | `Unknown | `Unsat ]
   end
 # let solver = Z3.create ();;
 val solver : Z3.t = <abstr>

src/smtml/solver.ml

@@ -55,6 +55,16 @@ module Base (M : Mappings_intf.S) = struct
   let model ?(symbols : Symbol.t list option) (s : M.solver) : Model.t option =
     let+ model = M.Solver.model s in
     M.values_of_model ?symbols model
+
+  let get_sat_model ?symbols s set =
+    match check_set s set with
+    | `Sat -> (
+      match model ?symbols s with
+      | Some model -> `Model model
+      | None ->
+        (* Should never happen *)
+        assert false )
+    | (`Unsat | `Unknown) as no_model -> no_model
 end
 
 module Incremental (M : Mappings_intf.S) : Solver_intf.S =
@@ -108,6 +118,10 @@ module Batch (Mappings : Mappings.S) = struct
 
   let get_statistics (s : t) : Statistics.t = get_statistics s.solver
 
+  let get_sat_model ?symbols s set =
+    let assert_ = Expr.Set.union set (Expr.Set.of_list s.top) in
+    get_sat_model ?symbols s.solver assert_
+
   let check (s : t) (es : Expr.t list) = check s.solver (es @ s.top)
 
   let check_set s es = check s @@ Expr.Set.to_list es
@@ -130,6 +144,7 @@ module Cached (Mappings_ : Mappings.S) = struct
       { solver : solver
       ; mutable top : Expr.Set.t
       ; stack : Expr.Set.t Stack.t
+      ; mutable last_check : Expr.Set.t option
       }
 
     module Cache = Cache.Strong
@@ -146,12 +161,13 @@ module Cached (Mappings_ : Mappings.S) = struct
       { solver = create ?params ?logic ()
       ; top = Expr.Set.empty
       ; stack = Stack.create ()
+      ; last_check = None
       }
 
-    let clone ({ solver; top; stack } : t) : t =
-      { solver = clone solver; top; stack = Stack.copy stack }
+    let clone ({ solver; top; stack; last_check } : t) : t =
+      { solver = clone solver; top; stack = Stack.copy stack; last_check }
 
-    let push ({ top; stack; solver } : t) : unit =
+    let push ({ top; stack; solver; _ } : t) : unit =
       Mappings.Solver.push solver;
       Stack.push top stack
 
@@ -181,8 +197,21 @@ module Cached (Mappings_ : Mappings.S) = struct
 
     let get_statistics (s : t) : Statistics.t = get_statistics s.solver
 
+    let get_sat_model ?symbols s set =
+      let assert_ = Expr.Set.union set s.top in
+      get_sat_model ?symbols s.solver assert_
+
+    let model ?(symbols : Symbol.t list option) (s : t) : Model.t option =
+      let open Option in
+      let* last_check = s.last_check in
+      (* We need to explicitly check_set because we don't want a cached reseponse *)
+      match check_set s.solver last_check with
+      | `Sat -> model ?symbols s.solver
+      | `Unsat | `Unknown -> None
+
     let check_set s es =
       let assert_ = Expr.Set.union es s.top in
+      s.last_check <- Some assert_;
       match Cache.find_opt cache assert_ with
       | Some res -> res
       | None ->
@@ -194,9 +223,6 @@ module Cached (Mappings_ : Mappings.S) = struct
 
     let get_value (solver : t) (e : Expr.t) : Expr.t = get_value solver.solver e
 
-    let model ?(symbols : Symbol.t list option) (s : t) : Model.t option =
-      model ?symbols s.solver
-
     let interrupt { solver; _ } = interrupt solver
   end
 

src/smtml/solver_intf.ml

@@ -89,8 +89,28 @@ module type S = sig
   (** [model ?symbols solver] retrieves the model of the last [check] query. If
       [?symbols] is provided, only the values of the specified symbols are
       included. Returns [None] if [check] was not invoked before or its result
-      was not [`Sat]. *)
+      was not [`Sat].
+
+      @warning Not compatible with cached solver mode - use {!get_sat_model} instead
+      @see 'get_sat_model' For cached solver-compatible alternative *)
   val model : ?symbols:Symbol.t list -> t -> Model.t option
+
+  (** Compute and retrieve a model for specific constraints.
+
+      [get_sat_model ?symbols solver exprs] performs:
+        1. [check_set] with [exprs] constraints
+        2. Returns model if result is [`Sat]
+
+      Filters output using [?symbols] when provided. Designed for cached
+      solvers.
+
+      @see {!model} For non-cached solvers when you have already performed
+      your own [check]/[check_set] and want to retrieve the results *)
+  val get_sat_model :
+       ?symbols:Symbol.t list
+    -> t
+    -> Expr.Set.t
+    -> [ `Model of Model.t | `Unsat | `Unknown ]
 end
 
 (** The [Intf] module type defines the interface for creating and working with

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

test/solver/test_solver_altergo.expected

@@ -1,3 +1,5 @@
+(model
+  (x int 0))
 (model
   (w i32 4)
   (x i32 1)

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 ()

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 ();

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 ()

test/solver/test_solver_z3.expected

@@ -1,3 +1,5 @@
+(model
+  (x int 0))
 (model
   (w i32 4)
   (x i32 1)

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 ();