Module Swal.Solver

SMT solver selector: dispatches --smt z3|cvc5|bitwuzla to the appropriate Smtml.Solver.Incremental backend.

type t =
  1. | Z3
  2. | CVC5
  3. | BITWUZLA
val pp : Ppx_deriving_runtime.Format.formatter -> t -> Ppx_deriving_runtime.unit
val show : t -> Ppx_deriving_runtime.string
val yojson_of_t : t -> Ppx_yojson_conv_lib.Yojson.Safe.t
type stats = Smtml.Statistics.t
val show_stats : Smtml.Statistics.t -> string
val pp_stats : Smtml.Statistics.t Fmt.t
val yojson_of_stats : Smtml.Statistics.t -> [> `Assoc of (string * [> `Float of float | `Int of int ]) Base.List.t ]
val get : t -> (module Smtml.Solver.S)