proposition: Lemma unit_propagation_rew : forall (n:nat) (concl: option HFormula), unit_propagation n concl = match n with | O => fun st => Fail OutOfFuel | S n => fun st => match extract_unit st with | None => Progress st | Some(l,st) => match success concl (units st) l with | Some deps => Success (hconsmap st,deps) | None => let st := insert_literal l st in let lelt := Annot.elt l in let lc := WMap.find_clauses lelt (clauses st) in match shorten_clauses l lc st with | Success d => Success d | Progress st => unit_propagation n concl st | Fail f => Fail f end end end end.
proof: Proof. destruct n ; reflexivity. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause