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/src/mc2.core/Plugin.ml.html
Source file Plugin.ml
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69
(** {1 Plugins} *) (** The operations for a solver plugin. A plugin can contribute types, terms, or other ways of implementing a theory. *) open Solver_types (** Heterogeneous tuple of services *) 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 keys *) 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 (** Main interface for plugins. Each plugin must abide by this interface. *) module type S = sig val id : plugin_id val name : string (** Descriptive name *) val provided_services : Service.any list (** List of provided services, to be registered for other plugins to use *) val check_if_sat : actions -> check_res (** Last call before answering "sat". If the current trail is not theory-satisfiable, the plugin {b MUST} give a conflict here. *) val iter_terms : term Iter.t (** Iterate on all terms known to the plugin. Used for checking all variables to assign, and for garbage collection. *) val gc_all : unit -> int (** Garbage collect all unmarked terms @returns the number of collected (deleted) terms *) end type t = (module S) let[@inline] owns_term (module P : S) (t:term) : bool = Term.plugin_id t = P.id let[@inline] name (module P : S) = P.name (** {2 Factory} *) module Factory = struct type plugin = t type t = Factory : { name: string; priority: int; requires: 'a service_key_list; build: plugin_id -> 'a service_list -> plugin } -> t let compare (a:t)(b:t) = let Factory {priority=p_a; _} = a in let Factory {priority=p_b; _} = b in CCInt.compare p_a p_b let make ?(priority=50) ~name ~requires ~build () = Factory { priority; name; requires; build; } end
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>