fact: Fixpoint case_split (cl: list literal) (st: state) (g : option HFormula) : result_dis := match cl with | nil => Backjump false (hconsmap st) nil LitSet.empty | f :: cl => match ProverT (insert_unit (annot_hyp f) st) g with | Success (m,prf,ann') => if lazy_and (negb (has_lit f ann')) (fun _ => annot_holds (units st) ann') then Backjump true m prf ann' else match augment_clauses prf (set_hmap m st) with | Success (m,d') => Backjump true m prf d' | Progress st' => match case_split cl st' g with | Failure f => Failure f | Backjump b m' prf' d' => Backjump b m' (prf++prf') (if b then d' else (LitSet.union d' (if (has_lit f ann') then (remove_lit f ann') else ann'))) end | Fail f => Failure f end | Fail f => Failure f | Progress st => Failure OutOfFuel end end.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause