Module Smtml.ParamsSource

Parameter Management Module. This module defines a type-safe interface for handling solver parameters, allowing configuration of options such as timeouts, model production, and parallel execution.

Parameter Types

Sourcetype t

The type t represents a set of solver parameters.

Sourcetype _ param =
  1. | Timeout : int param
    (*

    Specifies a timeout in milliseconds for each check call.

    *)
  2. | Model : bool param
    (*

    Enable or disable model production.

    *)
  3. | Unsat_core : bool param
    (*

    Enable or disable unsatisfiable core computation.

    *)
  4. | Ematching : bool param
    (*

    Enable or disable ematching.

    *)
  5. | Parallel : bool param
    (*

    Enable or disable parallel execution.

    *)
  6. | Num_threads : int param
    (*

    Specifies the maximum number of threads to use in parallel mode.

    *)
  7. | Debug : bool param
    (*

    Enable or disable solver debugging messages.

    *)

The type _ param represents a type-safe parameter, where the type parameter indicates the type of the parameter's value.

Sourcetype param' =
  1. | P : 'a param * 'a -> param'

The type param' is a wrapper for storing parameter-value pairs.

Default Values

Sourceval default_value : 'a param -> 'a

default_value param returns the default value associated with the given parameter.

Sourceval default : unit -> t

default () returns a parameter set with default values for all parameters.

Parameter Manipulation

Sourceval ($) : t -> ('a param * 'a) -> t

Infix operator for setting a parameter.

params $ (param, value) updates the parameter set params by setting param to value.

Sourceval set : t -> 'a param -> 'a -> t

set params param value updates the parameter set params by setting param to value.

Sourceval opt : t -> 'a param -> 'a option -> t

opt params param opt_value conditionally updates the parameter set params. If opt_value is Some v, it sets param to v. Otherwise, params remains unchanged.

Sourceval get : t -> 'a param -> 'a

get params param retrieves the current value of param from the parameter set params.

Conversion

Sourceval to_list : t -> param' list

to_list params converts the parameter set params into a list of parameter-value pairs.