From 85c00ecfa26ddcbe298e0bb262fac36d3b574e1b Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Wed, 1 Sep 2021 09:00:39 -0400 Subject: [PATCH] cleanup --- src/sat/Solver.ml | 21 --------------------- 1 file changed, 21 deletions(-) diff --git a/src/sat/Solver.ml b/src/sat/Solver.ml index 37b2b3d7..e5efa960 100644 --- a/src/sat/Solver.ml +++ b/src/sat/Solver.ml @@ -1658,25 +1658,6 @@ module Make(Plugin : PLUGIN) (Format.pp_print_list (Atom.debug store)) !core); !core - (* - module Clause_gc = struct - type state = { - solver: solver; - dirty_atoms: Atom.V - - } - - end - *) - - (* FIXME: also handle clause pools. - - - pools should probably have a "needs_gc" flag instead of doing GC - themselves - - each pool GC's itself by moving clauses into self.clauses_dead - - then all dead clauses are detached (+ dirty atoms marked), - we clean dirty atoms' watchlists, and finally remove clause. - *) (* GC: remove some learnt clauses. This works even during the proof with a non empty trail. *) let reduce_clause_db (self:t) : unit = @@ -1871,8 +1852,6 @@ module Make(Plugin : PLUGIN) reduce_clause_db st; ); - (* TODO: do a GC for all clause pools that need it *) - pick_branch_lit st done