package mc2

  1. Overview
  2. Docs

Plugins

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

type _ 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

type _ 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

module type S = sig ... end

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

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

Factory

module Factory : sig ... end