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

More log messages

Browse source
This commit is contained in:
Guillaume Bury 2015-03-16 15:29:12 +01:00
parent a362505d86
commit f604401e47
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
solver/mcsolver.ml
View file

@ -792,6 +792,7 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
let conflictC = ref 0 in let conflictC = ref 0 in
env.starts <- env.starts + 1; env.starts <- env.starts + 1;
while (true) do while (true) do
L.debug 100 "searching %d/%d (%d)" !conflictC n_of_conflicts n_of_learnts;
match propagate () with match propagate () with
| Some confl -> (* Conflict *) | Some confl -> (* Conflict *)
incr conflictC; incr conflictC;
@ -799,13 +800,12 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
| None -> (* No Conflict *) | None -> (* No Conflict *)
if nb_assigns() = St.nb_vars () (* env.nb_init_vars *) then raise Sat; if nb_assigns() = St.nb_vars () (* env.nb_init_vars *) then raise Sat;
if n_of_conflicts >= 0 && !conflictC >= n_of_conflicts then if n_of_conflicts >= 0 && !conflictC >= n_of_conflicts then begin
begin
L.debug 1 "Restarting..."; L.debug 1 "Restarting...";
env.progress_estimate <- progress_estimate(); env.progress_estimate <- progress_estimate();
cancel_until 0; cancel_until 0;
raise Restart raise Restart
end; end;
if decision_level() = 0 then simplify (); if decision_level() = 0 then simplify ();
if n_of_learnts >= 0 && if n_of_learnts >= 0 &&