setup dyn-trans in main solver

src/base-solver/dune

@@ -3,7 +3,7 @@
   (public_name sidekick-base.solver)
   (synopsis "Instantiation of solver and theories for Sidekick_base")
   (libraries sidekick-base sidekick.core sidekick.smt-solver
-             sidekick.th-bool-static
+             sidekick.th-bool-static sidekick.th-dyn-trans
              sidekick.mini-cc sidekick.th-data
              sidekick.arith-lra sidekick.zarith)
   (flags :standard -warn-error -a+8 -safe-string -color always -open Sidekick_util))

src/base-solver/sidekick_base_solver.ml

@@ -116,6 +116,11 @@ module Th_lra = Sidekick_arith_lra.Make(struct
   end
 end)
 
+module Th_dyn_trans = Sidekick_th_dyn_trans.Make(struct
+    module Solver = Solver
+    end)
+
 let th_bool : Solver.theory = Th_bool.theory
 let th_data : Solver.theory = Th_data.theory
 let th_lra : Solver.theory = Th_lra.theory
+let th_dyn_trans : Solver.theory = Th_dyn_trans.theory

src/main/main.ml

@@ -107,6 +107,7 @@ let main_smt () : _ result =
         Process.th_bool;
         Process.th_data;
         Process.th_lra;
+        Process.th_dyn_trans;
       ]
     in
     Process.Solver.create ~proof ~theories tst () ()

src/smtlib/Process.ml

@@ -282,7 +282,9 @@ let process_stmt
 module Th_data = SBS.Th_data
 module Th_bool = SBS.Th_bool
 module Th_lra = SBS.Th_lra
+module Th_dyn_trans = SBS.Th_dyn_trans
 
 let th_bool : Solver.theory = Th_bool.theory
 let th_data : Solver.theory = Th_data.theory
 let th_lra : Solver.theory = Th_lra.theory
+let th_dyn_trans : Solver.theory = Th_dyn_trans.theory

src/smtlib/Process.mli

@@ -12,6 +12,7 @@ module Solver
 val th_bool : Solver.theory
 val th_data : Solver.theory
 val th_lra : Solver.theory
+val th_dyn_trans : Solver.theory
 
 type 'a or_error = ('a, string) CCResult.t