From 56f98d9a82aee183619a7a7978f3e3c19f5d2190 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Wed, 17 Aug 2016 19:20:05 +0200 Subject: [PATCH] Explicit status for local assumption clauses Proofs require local assumptions to be recognisable. Keeping the reason of local assumptions as Bcp simplfies the code, since a proof is a clause, and allows to not have to recreate the local unit clause that effectively propagates the local assumptions. With this fix, simplification of clauses is not required aymore for levels between 0 (excluded) and base_level, so the partition function can be simplified accordingly. --- src/core/internal.ml | 56 ++++++++++++------------ src/core/res.ml | 80 +++++++++++++++++++++++------------ src/core/res_intf.ml | 1 + src/core/solver_types.ml | 2 + src/core/solver_types_intf.ml | 1 + 5 files changed, 83 insertions(+), 57 deletions(-) diff --git a/src/core/internal.ml b/src/core/internal.ml index db29c488..f13a3a63 100644 --- a/src/core/internal.ml +++ b/src/core/internal.ml @@ -292,8 +292,8 @@ module Make Clauses that propagated false lits are remembered to reconstruct resolution proofs. *) - let partition root atoms : atom list * clause list = - let rec partition_aux root trues unassigned falses history i = + let partition atoms : atom list * clause list = + let rec partition_aux trues unassigned falses history i = if i >= Array.length atoms then trues @ unassigned @ falses, history else begin @@ -307,30 +307,28 @@ module Make (arr_to_list atoms (i + 1)), history else if a.neg.is_true then let l = a.var.v_level in - if 0 <= l && l <= root then begin + if l = 0 then begin match a.var.reason with - | None | Some Decision -> assert false - (* The var must have a reason, and it cannot be a decision/assumption, - its level is below root level. *) | Some (Bcp cl) -> - partition_aux root trues unassigned falses (cl :: history) (i + 1) + partition_aux trues unassigned falses (cl :: history) (i + 1) (* A var false at level 0 can be eliminated from the clause, but we need to kepp in mind that we used another clause to simplify it. *) - | Some (Semantic n) when 0 <= n && n <= root -> - partition_aux root trues unassigned falses history (i + 1) + | Some (Semantic 0) -> + partition_aux trues unassigned falses history (i + 1) (* Semantic propagations at level 0 are, well not easy to deal with, this shouldn't really happen actually (because semantic propagations at level 0 should come with a proof). *) (* TODO: get a proof of the propagation. *) - | _ -> assert false + | None | Some (Decision | Semantic _ ) -> assert false + (* The var must have a reason, and it cannot be a decision/assumption, + since its level is 0. *) end else - partition_aux root trues unassigned (a::falses) history (i + 1) + partition_aux trues unassigned (a::falses) history (i + 1) else - partition_aux root trues (a::unassigned) falses history (i + 1) + partition_aux trues (a::unassigned) falses history (i + 1) end in - assert (0 <= root); - partition_aux root [] [] [] [] 0 + partition_aux [] [] [] [] 0 (* Making a decision. @@ -445,7 +443,7 @@ module Make be able to build a correct proof at the end of proof search. *) let simpl_reason : reason -> reason = function | (Bcp cl) as r -> - let l, history = partition env.base_level cl.atoms in + let l, history = partition cl.atoms in begin match l with | [ a ] -> if history = [] then r @@ -471,7 +469,7 @@ module Make if not a.is_true then begin assert (a.var.v_level < 0 && a.var.reason = None && lvl >= 0); let reason = - if lvl > env.base_level then reason + if lvl > 0 then reason else simpl_reason reason in a.is_true <- true; @@ -596,7 +594,7 @@ module Make c := res | _ -> assert false end - | None | Some Decision | Some Semantic _ -> () + | None | Some (Decision | Semantic _ ) -> () end done; assert false with Exit -> @@ -636,7 +634,7 @@ module Make while !cond do begin match !c.cpremise with | History _ -> clause_bump_activity !c - | Hyp | Lemma _ -> () + | Hyp | Local | Lemma _ -> () end; history := !c :: !history; (* visit the current predecessors *) @@ -751,10 +749,10 @@ module Make let vec = match init.cpremise with | Hyp -> env.clauses_hyps | Lemma _ -> env.clauses_learnt - | History _ -> assert false + | Local | History _ -> assert false in try - let atoms, history = partition 0 init.atoms in + let atoms, history = partition init.atoms in let clause = if history = [] then init else make_clause ?tag:init.tag (fresh_name ()) atoms (History (init :: history)) @@ -1147,15 +1145,15 @@ module Make Log.debugf 10 "local assumption: @[%a@]" (fun k->k pp_atom a); assert (decision_level () = env.base_level); if a.is_true then () - else if a.neg.is_true then begin - (* conflict between assumptions: UNSAT *) - let c = make_clause (fresh_hname ()) [a] Hyp in - report_unsat c; - end else begin - (* make a decision, propagate *) - let level = decision_level() in - let c = make_clause (fresh_hname ()) [a] Hyp in - enqueue_bool a ~level (Bcp c); + else + let c = make_clause (fresh_hname ()) [a] Local in + if a.neg.is_true then begin + (* conflict between assumptions: UNSAT *) + report_unsat c; + end else begin + (* make a decision, propagate *) + let level = decision_level() in + enqueue_bool a ~level (Bcp c); end in assert (env.base_level > 0); diff --git a/src/core/res.ml b/src/core/res.ml index daaf2bdb..c98d213d 100644 --- a/src/core/res.ml +++ b/src/core/res.ml @@ -83,23 +83,44 @@ module Make(St : Solver_types.S) = struct assert St.(conclusion.cpremise <> History []); conclusion - let prove_unsat c = - let l = Array.to_list c.St.atoms in - let l = List.map (fun a -> - match St.(a.var.reason) with - | Some St.Bcp d -> d - | _ -> assert false) l + let rec set_atom_proof a = + let aux acc b = + if equal_atoms a.St.neg b then acc + else set_atom_proof b :: acc in - St.make_clause (fresh_pcl_name ()) [] (St.History (c :: l)) + assert St.(a.var.v_level >= 0); + match St.(a.var.reason) with + | Some St.Bcp c -> + Log.debugf 50 "Analysing: @[%a@ %a@]" + (fun k -> k St.pp_atom a St.pp_clause c); + if Array.length c.St.atoms = 1 then begin + Log.debugf 30 "Old reason: @[%a@]" (fun k -> k St.pp_atom a); + c + end else begin + assert (a.St.neg.St.is_true); + let r = St.History (c :: (Array.fold_left aux [] c.St.atoms)) in + let c' = St.make_clause (fresh_pcl_name ()) [a.St.neg] r in + a.St.var.St.reason <- Some St.(Bcp c'); + Log.debugf 30 "New reason: @[%a@ %a@]" + (fun k -> k St.pp_atom a St.pp_clause c'); + c' + end + | _ -> assert false + + let prove_unsat conflict = + if Array.length conflict.St.atoms = 0 then conflict + else begin + Log.debugf 3 "Proving unsat from: @[%a@]" (fun k -> k St.pp_clause conflict); + let l = Array.fold_left (fun acc a -> set_atom_proof a :: acc) [] conflict.St.atoms in + let res = St.make_clause (fresh_pcl_name ()) [] (St.History (conflict :: l)) in + Log.debugf 5 "Proof found: @[%a@]" (fun k -> k St.pp_clause res); + res + end let prove_atom a = - if St.(a.is_true && a.var.v_level = 0) then begin - match St.(a.var.reason) with - | Some St.Bcp c -> - assert (Array.length St.(c.atoms) = 1 && equal_atoms a St.(c.atoms).(0)); - Some c - | _ -> assert false - end else + if St.(a.is_true && a.var.v_level = 0) then + Some (set_atom_proof a) + else None (* Interface exposed *) @@ -110,6 +131,7 @@ module Make(St : Solver_types.S) = struct } and step = | Hypothesis + | Assumption | Lemma of lemma | Resolution of proof * proof * atom @@ -119,15 +141,15 @@ module Make(St : Solver_types.S) = struct (fun k -> k St.pp_clause c St.pp_clause d); let dl = to_list d in begin match resolve (merge cl dl) with - | [ a ], l -> - begin match r with - | [] -> (l, c, d, a) - | _ -> - let new_clause = St.make_clause (fresh_pcl_name ()) - l (St.History [c; d]) in - chain_res (new_clause, l) r - end - | _ -> assert false + | [ a ], l -> + begin match r with + | [] -> (l, c, d, a) + | _ -> + let new_clause = St.make_clause (fresh_pcl_name ()) + l (St.History [c; d]) in + chain_res (new_clause, l) r + end + | _ -> assert false end | _ -> assert false @@ -138,6 +160,8 @@ module Make(St : Solver_types.S) = struct {conclusion; step = Lemma l; } | St.Hyp -> { conclusion; step = Hypothesis; } + | St.Local -> + { conclusion; step = Assumption; } | St.History [] -> assert false | St.History [ c ] -> @@ -163,11 +187,11 @@ module Make(St : Solver_types.S) = struct if not c.St.visited then begin c.St.visited <- true; match c.St.cpremise with - | St.Hyp | St.Lemma _ -> aux (c :: res) acc r - | St.History h -> - let l = List.fold_left (fun acc c -> - if not c.St.visited then c :: acc else acc) r h in - aux res (c :: acc) l + | St.Hyp | St.Local | St.Lemma _ -> aux (c :: res) acc r + | St.History h -> + let l = List.fold_left (fun acc c -> + if not c.St.visited then c :: acc else acc) r h in + aux res (c :: acc) l end else aux res acc r in diff --git a/src/core/res_intf.ml b/src/core/res_intf.ml index fd224762..dd600568 100644 --- a/src/core/res_intf.ml +++ b/src/core/res_intf.ml @@ -27,6 +27,7 @@ module type S = sig } and step = | Hypothesis + | Assumption | Lemma of lemma | Resolution of proof * proof * atom (** Lazy type for proof trees. Proofs are persistent objects, and can be diff --git a/src/core/solver_types.ml b/src/core/solver_types.ml index 8a1dc92c..d67aca27 100644 --- a/src/core/solver_types.ml +++ b/src/core/solver_types.ml @@ -72,6 +72,7 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct and premise = | Hyp + | Local | Lemma of proof | History of clause list @@ -277,6 +278,7 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct let pp_premise out = function | Hyp -> Format.fprintf out "hyp" + | Local -> Format.fprintf out "local" | Lemma _ -> Format.fprintf out "th_lemma" | History v -> List.iter (fun {name=name} -> Format.fprintf out "%s,@ " name) v diff --git a/src/core/solver_types_intf.ml b/src/core/solver_types_intf.ml index 955f60dd..1d3e0dc4 100644 --- a/src/core/solver_types_intf.ml +++ b/src/core/solver_types_intf.ml @@ -67,6 +67,7 @@ module type S = sig and premise = | Hyp + | Local | Lemma of proof | History of clause list