Module Z3.Simplifier

module Simplifier: sig .. end

type simplifier

val get_help : simplifier -> string

A string containing a description of parameters accepted by the simplifier.

val get_param_descrs : simplifier -> Params.ParamDescrs.param_descrs

Retrieves parameter descriptions for Simplifiers.

val get_num_simplifiers : context -> int

The number of supported simplifiers.

val get_simplifier_names : context -> string list

The names of all supported simplifiers.

val get_simplifier_description : context -> string -> string

Returns a string containing a description of the simplifier with the given name.

val mk_simplifier : context -> string -> simplifier

Creates a new Simplifier.

val and_then : context ->
       simplifier ->
       simplifier ->
       simplifier list -> simplifier

Create a simplifier that applies one simplifier to a Goal and then another one to every subgoal produced by the first one.

val using_params : context ->
       simplifier -> Params.params -> simplifier

Create a simplifier that applies a simplifier using the given set of parameters.

val with_ : context ->
       simplifier -> Params.params -> simplifier