Module Smtml.Solver_mode

Solver Mode Type. This module defines different solver modes and provides utilities for conversion, pretty-printing, and command-line argument handling.

Solver Modes

type t =
  1. | Batch
    (*

    Represents batch mode, where all queries are solved at once.

    *)
  2. | Cached
    (*

    Represents cached mode, where previous results may be reused.

    *)
  3. | Incremental
    (*

    Represents incremental mode, where constraints are solved step by step.

    *)

The type t represents different solver modes.

Pretty Printing

val pp : t Fmt.t

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

Parsing

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

of_string str parses a string into a solver mode.

str is the input string. Returns `Ok mode if parsing is successful, or `Error `Msg if the string does not match a known solver mode.

Command-Line Argument Handling

val conv : t Cmdliner.Arg.conv

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