From 5b87ff3e465653a9b16ae26f3c74ee416c0ff665 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Tue, 16 Aug 2022 21:29:58 -0400 Subject: [PATCH] feat(theory): add name accessor --- src/smt/theory.ml | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/smt/theory.ml b/src/smt/theory.ml index 7039ecb6..72410afe 100644 --- a/src/smt/theory.ml +++ b/src/smt/theory.ml @@ -31,6 +31,11 @@ type 'a p = (module S with type t = 'a) (** A theory that can be used for this particular solver, with state of type ['a]. *) +(** Name of the theory *) +let name (th : t) = + let (module T) = th in + T.name + let make (type st) ~name ~create_and_setup ?(push_level = fun _ -> ()) ?(pop_levels = fun _ _ -> ()) () : t = let module Th = struct