From db30e6b17392467a576fdda5e846ac62ee702b23 Mon Sep 17 00:00:00 2001 From: Filipe Marques Date: Thu, 26 Dec 2024 22:58:27 +0000 Subject: [PATCH] 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 | 2 ++ doc/index.mld | 4 ++-- src/altergo_mappings.default.ml | 2 +- src/mappings_intf.ml | 19 +++++++------------ src/optimizer_intf.ml | 4 +--- src/solver.ml | 8 +++----- src/solver_intf.ml | 6 ++---- src/ty.ml | 1 - 8 files changed, 18 insertions(+), 28 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index ad1dac3d..5c2dfdd3 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -4,6 +4,8 @@ ### Fixed ### Changed +- Removes `satisfiability` type + ## v0.4.1 ### Added diff --git a/doc/index.mld b/doc/index.mld index efd167c3..144dac88 100644 --- a/doc/index.mld +++ b/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 diff --git a/src/altergo_mappings.default.ml b/src/altergo_mappings.default.ml index 4d5ed458..39f013b8 100644 --- a/src/altergo_mappings.default.ml +++ b/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 diff --git a/src/mappings_intf.ml b/src/mappings_intf.ml index cd599aa9..13c3daed 100644 --- a/src/mappings_intf.ml +++ b/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 diff --git a/src/optimizer_intf.ml b/src/optimizer_intf.ml index 1f883c74..0c07e3c6 100644 --- a/src/optimizer_intf.ml +++ b/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 diff --git a/src/solver.ml b/src/solver.ml index 40ebcde2..f66213c6 100644 --- a/src/solver.ml +++ b/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 diff --git a/src/solver_intf.ml b/src/solver_intf.ml index e0deaa90..652d7ce6 100644 --- a/src/solver_intf.ml +++ b/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 diff --git a/src/ty.ml b/src/ty.ml index 17ae1a81..8dc6c9f3 100644 --- a/src/ty.ml +++ b/src/ty.ml @@ -452,4 +452,3 @@ module Naryop = struct | Concat -> Fmt.string fmt "++" | Regexp_union -> Fmt.string fmt "union" end -