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

remove dead code

Browse source
This commit is contained in:
Simon Cruanes 2021-11-14 22:53:34 -05:00
parent 5d18086e53
commit 69ee322c45
No known key found for this signature in database
GPG key ID: 4AC01D0849AA62B6
1 changed files with 0 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/sat/Solver.ml
View file

@ -1375,19 +1375,6 @@ module Make(Plugin : PLUGIN)
cr_steps;
}
(* FIXME
let prove_unsat_ (self:t) (conflict:conflict_res) : proof_step =
if Array.length conflict.atoms = 0 then (
conflict
) else (
Log.debugf 1 (fun k -> k "(@[sat.prove-unsat@ :from %a@])" Clause.debug conflict);
let l = Array.fold_left (fun acc a -> set_atom_proof a :: acc) [] conflict.atoms in
let res = Clause.make_permanent [] (History (conflict :: l)) in
Log.debugf 1 (fun k -> k "(@[sat.proof-found@ %a@])" Clause.debug res);
res
)
*)
(* Get the correct vector to insert a clause in. *)
let[@inline] add_clause_to_vec_ ~pool self c =
if Clause.removable self.store c && Clause.n_atoms self.store c > 2 then (