From b2f6a30cc837521df41d981ba7689032384398a2 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Mon, 10 Jun 2019 14:16:09 -0500
Subject: [PATCH] feat: function to add a theory and retain its state

---
 src/core/Sidekick_core.ml               | 9 +++++++++
 src/msat-solver/Sidekick_msat_solver.ml | 9 +++++++--
 2 files changed, 16 insertions(+), 2 deletions(-)

diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml
index 03867f7a..48ff8dc3 100644
--- a/src/core/Sidekick_core.ml
+++ b/src/core/Sidekick_core.ml
@@ -502,6 +502,10 @@ module type SOLVER = sig
   type theory = (module THEORY)
   (** A theory that can be used for this particular solver. *)
 
+  type 'a theory_p = (module THEORY with type t = 'a)
+  (** A theory that can be used for this particular solver, with state
+      of type ['a]. *)
+
   val mk_theory :
     name:string ->
     create_and_setup:(Solver_internal.t -> 'th) ->
@@ -584,6 +588,11 @@ module type SOLVER = sig
       any call to {!solve} or to {!add_clause} and the likes (otherwise
       the theory will have a partial view of the problem). *)
 
+  val add_theory_p : t -> 'a theory_p -> 'a
+  (** Add the given theory and obtain its state *)
+
+  val add_theory_l : t -> theory list -> unit
+
   val mk_atom_lit : t -> lit -> Atom.t
 
   val mk_atom_t : t -> ?sign:bool -> term -> Atom.t
diff --git a/src/msat-solver/Sidekick_msat_solver.ml b/src/msat-solver/Sidekick_msat_solver.ml
index 68fda661..1f2cf3a2 100644
--- a/src/msat-solver/Sidekick_msat_solver.ml
+++ b/src/msat-solver/Sidekick_msat_solver.ml
@@ -388,10 +388,11 @@ module Make(A : ARG)
   end
 
   type theory = (module THEORY)
+  type 'a theory_p = (module THEORY with type t = 'a)
 
   (** {2 Main} *)
 
-  let add_theory (self:t) (th:theory) : unit =
+  let add_theory_p (type a) (self:t) (th:a theory_p) : a =
     let (module Th) = th in
     Log.debugf 2
       (fun k-> k "(@[msat-solver.add-theory@ :name %S@])" Th.name);
@@ -406,7 +407,11 @@ module Make(A : ARG)
           next=self.si.th_states;
         };
     end;
-    ()
+    st
+
+  let add_theory (self:t) (th:theory) : unit =
+    let (module Th) = th in
+    ignore (add_theory_p self (module Th))
 
   let add_theory_l self = List.iter (add_theory self)