Removes satisfiability type

Because we're using a polymorphic variant for the satisfiability result
it's nicer to have the explicit sum of polymorphic variants in the type
signature of functions.

CHANGES.md

@@ -4,6 +4,8 @@
 ### Fixed
 ### Changed
 
+- Removes `satisfiability` type
+
 ## v0.4.1
 
 ### Added

doc/index.mld

@@ -37,8 +37,8 @@ module Z3 :
     val add_set : t -> Smtml.Expr.Set.t -> unit
     val get_assertions : t -> Smtml.Expr.t list
     val get_statistics : t -> Smtml.Statistics.t
-    val check : t -> Smtml.Expr.t list -> Smtml.Solver_intf.satisfiability
-    val check_set : t -> Smtml.Expr.Set.t -> Smtml.Solver_intf.satisfiability
+    val check : t -> Smtml.Expr.t list -> [ `Sat | `Unknown | `Unsat ]
+    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
   end

src/altergo_mappings.default.ml

@@ -126,7 +126,7 @@ module Fresh = struct
       let add_decls sym_decls cmds =
         ConstMap.fold (fun _ d acc -> d :: acc) sym_decls cmds
 
-      let check s ~assumptions : Mappings_intf.satisfiability =
+      let check s ~assumptions =
         let syms, cmds = mk_cmds s.syms s.cmds assumptions in
         let cmds = add_decls syms (List.rev cmds) in
         let ftdn_env = FE.init_env s.used_context in

src/mappings_intf.ml

@@ -2,12 +2,6 @@
 (* Copyright (C) 2023-2024 formalsec *)
 (* Written by the Smtml programmers *)
 
-type satisfiability =
-  [ `Sat
-  | `Unsat
-  | `Unknown
-  ]
-
 module type M = sig
   type ty
 
@@ -356,7 +350,7 @@ module type M = sig
 
     val add : solver -> term list -> unit
 
-    val check : solver -> assumptions:term list -> satisfiability
+    val check : solver -> assumptions:term list -> [ `Sat | `Unsat | `Unknown ]
 
     val model : solver -> model option
 
@@ -378,7 +372,7 @@ module type M = sig
 
     val add : optimizer -> term list -> unit
 
-    val check : optimizer -> satisfiability
+    val check : optimizer -> [ `Sat | `Unsat | `Unknown ]
 
     val model : optimizer -> model option
 
@@ -397,7 +391,7 @@ module type M = sig
     val pp :
          ?name:string
       -> ?logic:Logic.t
-      -> ?status:satisfiability
+      -> ?status:[ `Sat | `Unsat | `Unknown ]
       -> term list Fmt.t
   end
 end
@@ -429,7 +423,7 @@ module type S = sig
     val pp :
          ?name:string
       -> ?logic:Logic.t
-      -> ?status:satisfiability
+      -> ?status:[ `Sat | `Unsat | `Unknown ]
       -> Expr.t list Fmt.t
   end
 
@@ -448,7 +442,8 @@ module type S = sig
 
     val add : solver -> Expr.t list -> unit
 
-    val check : solver -> assumptions:Expr.t list -> satisfiability
+    val check :
+      solver -> assumptions:Expr.t list -> [ `Sat | `Unsat | `Unknown ]
 
     val model : solver -> model option
 
@@ -466,7 +461,7 @@ module type S = sig
 
     val add : optimize -> Expr.t list -> unit
 
-    val check : optimize -> satisfiability
+    val check : optimize -> [ `Sat | `Unsat | `Unknown ]
 
     val model : optimize -> model option
 

src/optimizer_intf.ml

@@ -17,7 +17,7 @@ module type S = sig
 
   val protect : t -> (unit -> 'a) -> 'a
 
-  val check : t -> Mappings_intf.satisfiability
+  val check : t -> [ `Sat | `Unsat | `Unknown ]
 
   val model : t -> Model.t option
 
@@ -29,8 +29,6 @@ module type S = sig
 end
 
 module type Intf = sig
-  type nonrec satisfiability = satisfiability
-
   module type S = S
 
   module Make (_ : Mappings_intf.S) : S

src/solver.ml

@@ -38,7 +38,7 @@ module Base (M : Mappings_intf.S) = struct
   let get_statistics (solver : t) : Statistics.t =
     M.Solver.get_statistics solver
 
-  let check (solver : M.solver) (es : Expr.t list) : satisfiability =
+  let check (solver : M.solver) (es : Expr.t list) =
     incr solver_count;
     Utils.run_and_time_call
       ~use:(fun time -> solver_time := !solver_time +. time)
@@ -105,8 +105,7 @@ module Batch (Mappings : Mappings.S) = struct
 
   let get_statistics (s : t) : Statistics.t = get_statistics s.solver
 
-  let check (s : t) (es : Expr.t list) : satisfiability =
-    check s.solver (es @ s.top)
+  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
 
@@ -179,8 +178,7 @@ module Cached (Mappings : Mappings.S) = struct
       Cache.add cache es result;
       result
 
-  let check (s : t) (es : Expr.t list) : satisfiability =
-    check_set s (Expr.Set.of_list es)
+  let check (s : t) (es : Expr.t list) = check_set s (Expr.Set.of_list es)
 
   let get_value (solver : t) (e : Expr.t) : Expr.t = get_value solver.solver e
 

src/solver_intf.ml

@@ -58,10 +58,10 @@ module type S = sig
 
   (** [check solver es] checks the satisfiability of the assertions in the
       solver using the assumptions in [es]. *)
-  val check : t -> Expr.t list -> satisfiability
+  val check : t -> Expr.t list -> [ `Sat | `Unsat | `Unknown ]
 
   (** Same as [check] but receives an Expr.Set.t *)
-  val check_set : t -> Expr.Set.t -> satisfiability
+  val check_set : t -> Expr.Set.t -> [ `Sat | `Unsat | `Unknown ]
 
   (** [get_value solver e] get an expression denoting the model value of a given
       expression.
@@ -77,8 +77,6 @@ module type S = sig
 end
 
 module type Intf = sig
-  type nonrec satisfiability = satisfiability
-
   module type S = S
 
   (** The Encoding module defines two types of solvers: {!module:Batch} and

src/ty.ml

@@ -452,4 +452,3 @@ module Naryop = struct
     | Concat -> Fmt.string fmt "++"
     | Regexp_union -> Fmt.string fmt "union"
 end
-