Module Smtml.Smtzilla

module Fresh : sig ... end

Fresh.Make () creates a new instance of the S module type.

val is_available : bool

is_available indicates whether the module is available for use.

Include the S module type.

include Mappings_intf.S
type model

The type of SMT models.

type solver

The type of SMT solvers.

type optimize

The type of optimizers.

type handle

The type of optimization handles.

val value : model -> Expr.t -> Value.t

value model expr evaluates the expression expr in the given model.

val values_of_model : ?symbols:Symbol.t list -> model -> Model.t

values_of_model ?symbols model retrieves the values of the given symbols (or all symbols if not provided) from the model.

val set_debug : bool -> unit

set_debug flag enables or disables debug mode based on flag.

SMT-LIB Pretty Printing

module Smtlib : sig ... end

Solver Handling

module Solver : sig ... end

Optimizer Handling

module Optimizer : sig ... end