Module Mc2_core.PluginSource

Plugins

The operations for a solver plugin. A plugin can contribute types, terms, or other ways of implementing a theory.

Sourcetype _ service_list =
  1. | S_nil : unit service_list
  2. | S_cons : 'a Service.Key.t * 'a * 'b service_list -> ('a * 'b) service_list

Heterogeneous tuple of services

Sourcetype _ service_key_list =
  1. | K_nil : unit service_key_list
  2. | K_cons : 'a Service.Key.t * 'b service_key_list -> ('a * 'b) service_key_list

Heterogeneous tuple of keys

Sourcemodule type S = sig ... end

Main interface for plugins. Each plugin must abide by this interface.

Sourcetype t = (module S)
Sourceval owns_term : t -> Mc2_core__.Solver_types.term -> bool
Sourceval name : t -> string

Factory

Sourcemodule Factory : sig ... end