add optional size argument to create functions

src/core/Internal.ml

@@ -134,7 +134,7 @@ module Make
   }
 
   (* Starting environment. *)
-  let create ?(st=St.create()) () : t = {
+  let create_ ~st ~size_trail ~size_lvl () : t = {
     st;
     unsat_conflict = None;
     next_decision = None;
@@ -149,10 +149,10 @@ module Make
     th_head = 0;
     elt_head = 0;
 
-    trail = Vec.make 601 (Trail_elt.of_atom Atom.dummy);
+    trail = Vec.make size_trail (Trail_elt.of_atom Atom.dummy);
-    elt_levels = Vec.make 601 (-1);
+    elt_levels = Vec.make size_lvl (-1);
-    th_levels = Vec.make 100 Plugin.dummy;
+    th_levels = Vec.make size_lvl Plugin.dummy;
-    user_levels = Vec.make 10 (-1);
+    user_levels = Vec.make 0 (-1);
 
     order = H.create();
 
@@ -181,6 +181,14 @@ module Make
     nb_init_clauses = 0;
   }
 
+  let create ?(size=`Big) ?st () : t =
+    let st = match st with Some s -> s | None -> St.create ~size () in
+    let size_trail, size_lvl = match size with
+      | `Tiny -> 0, 0
+      | `Small -> 32, 16
+      | `Big -> 600, 50
+    in create_ ~st ~size_trail ~size_lvl ()
+
   (* Misc functions *)
   let to_float = float_of_int
   let to_int = int_of_float

src/core/Internal.mli

@@ -27,7 +27,7 @@ module Make
   type t
   (** Solver *)
 
-  val create : ?st:St.t -> unit -> t
+  val create : ?size:[`Tiny|`Small|`Big] -> ?st:St.t -> unit -> t
 
   val st : t -> St.t
   (** Underlying state *)

src/core/Solver_intf.ml

@@ -64,7 +64,7 @@ module type S = sig
   type t
   (** Main solver type, containing all state *)
 
-  val create : ?st:St.t -> unit -> t
+  val create : ?size:[`Tiny|`Small|`Big] -> ?st:St.t -> unit -> t
   (** Create new solver *)
   (* TODO: add size hint, callbacks, etc. *)
 

src/core/Solver_types.ml

@@ -148,15 +148,21 @@ module McMake (E : Expr_intf.S) = struct
 
   type state = t
 
-  let create() : t = {
+  let create_ size_map size_vars () : t = {
-    f_map = MF.create 4096;
+    f_map = MF.create size_map;
-    t_map = MT.create 4096;
+    t_map = MT.create size_map;
-    vars = Vec.make 107 (E_var dummy_var);
+    vars = Vec.make size_vars (E_var dummy_var);
     cpt_mk_var = 0;
     cpt_mk_clause = 0;
   }
 
-  (* TODO: embed a state `t` with these inside *)
+  let create ?(size=`Big) () : t =
+    let size_map, size_vars = match size with
+      | `Tiny -> 8, 0
+      | `Small -> 16, 10
+      | `Big -> 4096, 128
+    in
+    create_ size_map size_vars ()
 
   let nb_elt st = Vec.size st.vars
   let get_elt st i = Vec.get st.vars i

src/core/Solver_types_intf.ml

@@ -35,8 +35,7 @@ module type S = sig
   type t
   (** State for creating new terms, literals, clauses *)
 
-  (* TODO: add size hint *)
+  val create: ?size:[`Tiny|`Small|`Big] -> unit -> t
-  val create: unit -> t
 
   (** {2 Type definitions} *)
 

src/main/main.ml

@@ -37,7 +37,7 @@ module Make
 
   let hyps = ref []
 
-  let st = S.create()
+  let st = S.create ~size:`Big ()
 
   let check_model sat =
     let check_clause c =