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

small details

Browse source
This commit is contained in:
Simon Cruanes 2015-02-09 11:35:55 +01:00
parent c2cfa14e86
commit 425043a362
2 changed files with 14 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
Makefile
View file

@ -40,7 +40,7 @@ clean:
TO_INSTALL=META $(addprefix _build/,$(LIB) $(NAME).a $(NAME).cmi)
install: all
install: lib
ocamlfind install msat $(TO_INSTALL)
uninstall:

26
solver/solver.ml
View file

@ -359,19 +359,19 @@ module Make (L : Log_intf.S)(F : Formula_intf.S)
exception Trivial
let simplify_zero atoms init0 =
(* TODO: could be more efficient than [@] everywhere? *)
assert (decision_level () = 0);
let aux (atoms, init) a =
if a.is_true then raise Trivial;
if a.neg.is_true then
match a.var.vpremise with
| History v -> atoms, [init0]
| Lemma p -> assert false
else
a::atoms, init
in
let atoms, init = List.fold_left aux ([], []) atoms in
List.fast_sort (fun a b -> a.var.vid - b.var.vid) atoms, init
(* TODO: could be more efficient than [@] everywhere? *)
assert (decision_level () = 0);
let aux (atoms, init) a =
if a.is_true then raise Trivial;
if a.neg.is_true then
match a.var.vpremise with
| History v -> atoms, [init0]
| Lemma p -> assert false
else
a::atoms, init
in
let atoms, init = List.fold_left aux ([], []) atoms in
List.fast_sort (fun a b -> a.var.vid - b.var.vid) atoms, init
let partition atoms init0 =
let rec partition_aux trues unassigned falses init = function