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

Merge branch 'master' of github.com:Gbury/mSAT

Browse source
This commit is contained in:
Guillaume Bury 2015-02-09 14:01:59 +01:00
commit 4ff01d2a7e
3 changed files with 18 additions and 18 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) TO_INSTALL=META $(addprefix _build/,$(LIB) $(NAME).a $(NAME).cmi)
install: all install: lib
ocamlfind install msat $(TO_INSTALL) ocamlfind install msat $(TO_INSTALL)
uninstall: uninstall:

8
solver/res.ml
View file

@ -273,14 +273,14 @@ module Make(St : Solver_types.S) = struct
aux (to_list c, to_list d) aux (to_list c, to_list d)
let unsat_core proof = let unsat_core proof =
let rec aux proof = let rec aux acc proof =
let p = proof () in let p = proof () in
match p.step with match p.step with
| Hypothesis | Lemma _ -> [p.conclusion] | Hypothesis | Lemma _ -> p.conclusion :: acc
| Resolution (proof1, proof2, _) -> | Resolution (proof1, proof2, _) ->
List.rev_append (aux proof1) (aux proof2) aux (aux acc proof1) proof2
in in
List.sort_uniq compare_cl (aux proof) List.sort_uniq compare_cl (aux [] proof)
(* Print proof graph *) (* Print proof graph *)
let _i = ref 0 let _i = ref 0

26
solver/solver.ml
View file

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