package mc2
A mcsat-based SMT solver in pure OCaml
Install
Dune Dependency
Authors
Maintainers
Sources
v0.1.tar.gz
md5=92de696251ec76fbf3eba6ee917fd80f
sha512=e88ba0cfc23186570a52172a0bd7c56053273941eaf3cda0b80fb6752e05d1b75986b01a4e4d46d9711124318e57cba1cd92d302e81d34f9f1ae8b49f39114f0
doc/mc2.core/Mc2_core/Plugin/index.html
Module Mc2_core.PluginSource
Plugins
The operations for a solver plugin. A plugin can contribute types, terms, or other ways of implementing a theory.
Source
type _ service_list = | S_nil : unit service_list| S_cons : 'a Service.Key.t * 'a * 'b service_list -> ('a * 'b) service_list
Heterogeneous tuple of services
Source
type _ service_key_list = | K_nil : unit service_key_list| K_cons : 'a Service.Key.t * 'b service_key_list -> ('a * 'b) service_key_list
Heterogeneous tuple of keys
Main interface for plugins. Each plugin must abide by this interface.