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

remove debug msgs

Browse source
This commit is contained in:
Simon Cruanes 2021-08-31 23:19:06 -04:00
parent debd8bcaf8
commit a22bfe06c1
No known key found for this signature in database
GPG key ID: 4AC01D0849AA62B6
1 changed files with 1 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/sat/Solver.ml
View file

@ -1125,9 +1125,7 @@ module Make(Plugin : PLUGIN)
(* save current state of [to_unmark] *) (* save current state of [to_unmark] *)
let top = Vec.size to_unmark in let top = Vec.size to_unmark in
Log.debugf 1 (fun k->k"lit.redundant v%d abstract_levels 0x%xd" (v:var:>int) abstract_levels);
let rec aux v = let rec aux v =
Log.debugf 1 (fun k->k"lit.redundant.aux v%d" (v:var:>int));
match Var.reason store v with match Var.reason store v with
| None -> assert false | None -> assert false
| Some Decision -> raise_notrace Non_redundant | Some Decision -> raise_notrace Non_redundant
@ -1151,10 +1149,9 @@ module Make(Plugin : PLUGIN)
) )
done done
in in
try aux v; Log.debug 1 "redundant"; true try aux v; true
with Non_redundant -> with Non_redundant ->
(* clear new marks, they are not actually redundant *) (* clear new marks, they are not actually redundant *)
Log.debug 1 "non redundant";
for i = top to Vec.size to_unmark-1 do for i = top to Vec.size to_unmark-1 do
Var.unmark store (Vec.get to_unmark i) Var.unmark store (Vec.get to_unmark i)
done; done;