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

refactor: small cleanup

Browse source
This commit is contained in:
Simon Cruanes 2019-01-22 20:26:55 -06:00 • committed by Guillaume Bury
parent ca62db00e1
commit 8f29aa8005
1 changed files with 3 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/core/Internal.ml
View file

@ -1380,11 +1380,6 @@ module Make(Plugin : PLUGIN)
let[@inline] analyze st c_clause : conflict_res = let[@inline] analyze st c_clause : conflict_res =
analyze_sat st c_clause analyze_sat st c_clause
(*
if mcsat
then analyze_mcsat c_clause
else analyze_sat c_clause
*)
(* add the learnt clause to the clause database, propagate, etc. *) (* add the learnt clause to the clause database, propagate, etc. *)
let record_learnt_clause st (confl:clause) (cr:conflict_res): unit = let record_learnt_clause st (confl:clause) (cr:conflict_res): unit =
@ -1524,7 +1519,9 @@ module Make(Plugin : PLUGIN)
(* false lit must be at index 1 *) (* false lit must be at index 1 *)
atoms.(0) <- atoms.(1); atoms.(0) <- atoms.(1);
atoms.(1) <- first atoms.(1) <- first
) else assert (a.neg == atoms.(1)); ) else (
assert (a.neg == atoms.(1))
);
let first = atoms.(0) in let first = atoms.(0) in
if first.is_true if first.is_true
then Watch_kept (* true clause, keep it in watched *) then Watch_kept (* true clause, keep it in watched *)