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

Simplified proof generation

Browse source
This commit is contained in:
Guillaume Bury 2015-02-09 16:07:28 +01:00
parent 74238bbed8
commit 5f155f6bde
2 changed files with 4 additions and 37 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

35
solver/res.ml
View file

@ -39,7 +39,6 @@ module Make(St : Solver_types.S) = struct
let equal = equal_cl let equal = equal_cl
end) end)
let proof : node H.t = H.create 1007;; let proof : node H.t = H.create 1007;;
let unit_hyp : (clause * St.atom list) H.t = H.create 37;;
(* Misc functions *) (* Misc functions *)
let equal_atoms a b = St.(a.aid) = St.(b.aid) let equal_atoms a b = St.(a.aid) = St.(b.aid)
@ -84,33 +83,10 @@ module Make(St : Solver_types.S) = struct
res res
(* Adding hyptoheses *) (* Adding hyptoheses *)
let is_unit_hyp = function
| [a] -> St.(a.var.level = 0 && a.var.reason = None && a.var.vpremise <> History [])
| _ -> false
let make_unit_hyp a =
let aux a = St.(make_clause (fresh_name ()) [a] 1 false (History [])) in
if St.(a.is_true) then
aux a
else if St.(a.neg.is_true) then
aux St.(a.neg)
else
assert false
let unit_hyp a =
let a = St.(a.var.pa) in
try
H.find unit_hyp [a]
with Not_found ->
let c = make_unit_hyp a in
let cl = to_list c in
H.add unit_hyp [a] (c, cl);
(c, cl)
let is_proved (c, cl) = let is_proved (c, cl) =
if H.mem proof cl then if H.mem proof cl then
true true
else if is_unit_hyp cl || not St.(c.learnt) then begin else if not St.(c.learnt) then begin
H.add proof cl Assumption; H.add proof cl Assumption;
true true
end else match St.(c.cpremise) with end else match St.(c.cpremise) with
@ -148,12 +124,6 @@ module Make(St : Solver_types.S) = struct
let clause_unit a = match St.(a.var.level, a.var.reason) with let clause_unit a = match St.(a.var.level, a.var.reason) with
| 0, Some c -> c, to_list c | 0, Some c -> c, to_list c
| 0, None ->
let c, cl = unit_hyp a in
if is_proved (c, cl) then
c, cl
else
assert false
| _ -> | _ ->
raise (Resolution_error "Could not find a reason needed to resolve") raise (Resolution_error "Could not find a reason needed to resolve")
@ -209,9 +179,6 @@ module Make(St : Solver_types.S) = struct
Log.debug 2 "Eliminating %a in %a" St.pp_atom a St.pp_clause c; Log.debug 2 "Eliminating %a in %a" St.pp_atom a St.pp_clause c;
let d = match St.(a.var.level, a.var.reason) with let d = match St.(a.var.level, a.var.reason) with
| 0, Some d -> d | 0, Some d -> d
| 0, None ->
let d, cl_d = unit_hyp a in
if is_proved (d, cl_d) then d else raise Exit
| _ -> raise Exit | _ -> raise Exit
in in
prove d; prove d;

6
solver/solver.ml
View file

@ -365,8 +365,8 @@ module Make (L : Log_intf.S)(F : Formula_intf.S)
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, false | History _ -> atoms, false
| Lemma p -> assert false | Lemma _ -> assert false
else else
a::atoms, init a::atoms, init
in in
@ -426,7 +426,7 @@ module Make (L : Log_intf.S)(F : Formula_intf.S)
| [a] -> | [a] ->
cancel_until 0; cancel_until 0;
a.var.vpremise <- History [init0]; a.var.vpremise <- History [init0];
enqueue a 0 (if init then None else Some init0) enqueue a 0 (Some init0)
with Trivial -> () with Trivial -> ()