package smtml

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Mappings.MakeSource

Parameters

Signature

Sourcemodule Fresh : sig ... end

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

Sourceval is_available : bool

is_available indicates whether the module is available for use.

Include the S module type.

include Mappings_intf.S
Sourcetype model

The type of SMT models.

Sourcetype solver

The type of SMT solvers.

Sourcetype optimize

The type of optimizers.

Sourcetype handle

The type of optimization handles.

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

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

Sourceval 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.

Sourceval set_debug : bool -> unit

set_debug flag enables or disables debug mode based on flag.

SMT-LIB Pretty Printing

Sourcemodule Smtlib : sig ... end

Solver Handling

Sourcemodule Solver : sig ... end

Optimizer Handling

Sourcemodule Optimizer : sig ... end
OCaml

Innovation. Community. Security.