From c9e257d40b6060534591f3b1421c62f469f397f3 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 5989ad6c..91399678 100644 --- a/src/sat/Solver.ml +++ b/src/sat/Solver.ml @@ -1745,25 +1745,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 = @@ -1958,8 +1939,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