From 5bfd975ed3ada41f19b3e6cbcc259e149352b0d7 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Thu, 21 Feb 2019 17:50:35 -0600 Subject: [PATCH] refactor: move constant parameters outside of the solver --- src/core/Internal.ml | 22 +++++++++------------- 1 file changed, 9 insertions(+), 13 deletions(-) diff --git a/src/core/Internal.ml b/src/core/Internal.ml index 12259a04..bb517489 100644 --- a/src/core/Internal.ml +++ b/src/core/Internal.ml @@ -822,16 +822,16 @@ module Make(Plugin : PLUGIN) mutable clause_incr : float; (* increment for clauses' activity *) - - mutable restart_first : int; - (* intial restart limit, default 100 *) - - mutable learntsize_factor : float; - (* initial limit for the number of learnt clauses, 1/3 of initial - number of clauses by default *) } type solver = t + (* intial restart limit *) + let restart_first = 100 + + (* initial limit for the number of learnt clauses, 1/3 of initial + number of clauses by default *) + let learntsize_factor = 1. /. 3. + (* Starting environment. *) let create_ ~st ~store_proof (th:theory) : t = { st; th; @@ -856,10 +856,6 @@ module Make(Plugin : PLUGIN) var_incr = 1.; clause_incr = 1.; store_proof; - - restart_first = 100; - - learntsize_factor = 1. /. 3. ; } let create ?(store_proof=true) ?(size=`Big) (th:theory) : t = @@ -2004,8 +2000,8 @@ module Make(Plugin : PLUGIN) check_unsat_ st; try flush_clauses st; (* add initial clauses *) - let n_of_conflicts = ref (float_of_int st.restart_first) in - let n_of_learnts = ref ((float_of_int (nb_clauses st)) *. st.learntsize_factor) in + let n_of_conflicts = ref (float_of_int restart_first) in + let n_of_learnts = ref ((float_of_int (nb_clauses st)) *. learntsize_factor) in while true do begin try search st (int_of_float !n_of_conflicts) (int_of_float !n_of_learnts)