simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-08 04:05:43 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

refactor: move constant parameters outside of the solver

Browse source
This commit is contained in:
Simon Cruanes 2019-02-21 17:50:35 -06:00 • committed by Guillaume Bury
parent efe93c3647
commit 5bfd975ed3
1 changed files with 9 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

22
src/core/Internal.ml
View file

@ -822,16 +822,16 @@ module Make(Plugin : PLUGIN)
mutable clause_incr : float; mutable clause_incr : float;
(* increment for clauses' activity *) (* 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 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. *) (* Starting environment. *)
let create_ ~st ~store_proof (th:theory) : t = { let create_ ~st ~store_proof (th:theory) : t = {
st; th; st; th;
@ -856,10 +856,6 @@ module Make(Plugin : PLUGIN)
var_incr = 1.; var_incr = 1.;
clause_incr = 1.; clause_incr = 1.;
store_proof; store_proof;
restart_first = 100;
learntsize_factor = 1. /. 3. ;
} }
let create ?(store_proof=true) ?(size=`Big) (th:theory) : t = let create ?(store_proof=true) ?(size=`Big) (th:theory) : t =
@ -2004,8 +2000,8 @@ module Make(Plugin : PLUGIN)
check_unsat_ st; check_unsat_ st;
try try
flush_clauses st; (* add initial clauses *) flush_clauses st; (* add initial clauses *)
let n_of_conflicts = ref (float_of_int st.restart_first) in let n_of_conflicts = ref (float_of_int restart_first) in
let n_of_learnts = ref ((float_of_int (nb_clauses st)) *. st.learntsize_factor) in let n_of_learnts = ref ((float_of_int (nb_clauses st)) *. learntsize_factor) in
while true do while true do
begin try begin try
search st (int_of_float !n_of_conflicts) (int_of_float !n_of_learnts) search st (int_of_float !n_of_conflicts) (int_of_float !n_of_learnts)