Module Smtml.Solver_type

Solver Type Module. This module defines types and utilities for working with different SMT solvers, including parsing, pretty-printing, availability checks, and mapping retrieval.

Solver Types

type t =
  1. | Z3_solver
    (*

    Represents the Z3 solver.

    *)
  2. | Bitwuzla_solver
    (*

    Represents the Bitwuzla solver.

    *)
  3. | Colibri2_solver
    (*

    Represents the Colibri2 solver.

    *)
  4. | Cvc5_solver
    (*

    Represents the CVC5 solver.

    *)
  5. | Altergo_solver
    (*

    Represents the Alt-Ergo solver.

    *)
  6. | Smtzilla_solver
    (*

    Represents the SMTZilla solver.

    *)

The type t represents different SMT solvers.

val supported_solvers : t list

supported_solvers returns a list of all supported solvers.

Parsing

val of_string : string -> (t, [> `Msg of string ]) Smtml_prelude.result

of_string s attempts to convert the string s into a solver type. Returns Ok solver if successful, or an error message otherwise.

Pretty Printing

val pp : t Fmt.t

pp fmt solver pretty-prints the solver type solver using the formatter fmt.

Command-Line Argument Handling

val conv : t Cmdliner.Arg.conv

conv provides a command-line argument converter for solver types.

Solver Availability

val is_available : t -> bool

is_available solver checks whether the given solver is available in the current environment.

Solver Mappings

val to_mappings : t -> (module Mappings.S_with_fresh)

to_mappings solver retrieves the corresponding solver mappings module for the given solver type.