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

fix(proof): unsat conflicts now call Proof.prove_unsat

Browse source 
this does the last bit of proof recording when a conflict is reached
during propagation
This commit is contained in:
Simon Cruanes 2019-02-16 12:16:41 -06:00 • committed by Guillaume Bury
parent 2e2bbfd4d0
commit cdb52ee757
1 changed files with 9 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
src/core/Internal.ml
View file

@ -521,12 +521,11 @@ module Make(Plugin : PLUGIN)
) )
let prove_atom a = let prove_atom a =
if (a.is_true && a.var.v_level = 0) then if a.is_true && a.var.v_level = 0 then
Some (set_atom_proof a) Some (set_atom_proof a)
else else
None None
(* Interface exposed *)
type t = clause type t = clause
and proof_node = { and proof_node = {
conclusion : clause; conclusion : clause;
@ -652,9 +651,7 @@ module Make(Plugin : PLUGIN)
| Duplicate _ -> "duplicate" | Duplicate _ -> "duplicate"
| Hyper_res _ -> "hyper-resolution" | Hyper_res _ -> "hyper-resolution"
(* Compute unsat-core (* Compute unsat-core by accumulating the leaves *)
TODO: replace visited bool by a int unique to each call
of unsat_core, so that the cleanup can be removed ? *)
let unsat_core proof = let unsat_core proof =
let rec aux res acc = function let rec aux res acc = function
| [] -> res, acc | [] -> res, acc
@ -1187,10 +1184,13 @@ module Make(Plugin : PLUGIN)
in multiple places (adding new clauses, or solving for instance). *) in multiple places (adding new clauses, or solving for instance). *)
let report_unsat st (us:unsat_cause) : _ = let report_unsat st (us:unsat_cause) : _ =
Log.debugf info (fun k -> k "(@[sat.unsat-conflict@ %a@])" pp_unsat_cause us); Log.debugf info (fun k -> k "(@[sat.unsat-conflict@ %a@])" pp_unsat_cause us);
begin match us with let us = match us with
| US_false c -> st.unsat_at_0 <- Some c; | US_false c ->
| _ -> () let c = if st.store_proof then Proof.prove_unsat c else c in
end; st.unsat_at_0 <- Some c;
US_false c
| _ -> us
in
raise (E_unsat us) raise (E_unsat us)
(* Simplification of boolean propagation reasons. (* Simplification of boolean propagation reasons.