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

chore: remove dead code in sat

Browse source
This commit is contained in:
Simon Cruanes 2018-08-18 17:47:20 -05:00
parent 72750b9e1a
commit e6a96df0d9
1 changed files with 0 additions and 27 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

27
src/sat/Internal.ml
View file

@ -842,33 +842,6 @@ module Make (Th : Theory_intf.S) = struct
Clause.make_l !res (Simplified clause)
)
(* Sort literals for new clause, into:
- true literals (maybe makes the clause trivial if the lit is proved true at level 0)
- unassigned literals, yet to be decided
- false literals (not suitable to watch)
*)
let sort_lits_by_level atoms : atom list =
let rec aux trues unassigned falses i =
if i >= Array.length atoms then (
trues @ unassigned @ falses
) else (
let a = atoms.(i) in
if a.is_true then (
let l = a.var.v_level in
if l = 0 then
raise Trivial (* A var true at level 0 gives a trivially true clause *)
else
(a :: trues) @ unassigned @ falses @ (array_slice_to_list atoms (i + 1))
) else if a.neg.is_true then (
aux trues unassigned (a::falses) (i + 1)
) else (
aux trues (a::unassigned) falses (i + 1)
)
)
in
try aux [] [] [] 0
with Trivial -> Array.to_list atoms
(* Making a decision.
Before actually creatig a new decision level, we check that
all propagations have been done and propagated to the theory,