fact: Fixpoint cnf (pol:bool) (is_classic: bool) (cp cm: IntMap.ptrie unit) (ar:list literal) (acc : list watched_clause) (f: LForm) (hf: HFormula) : IntMap.ptrie unit * IntMap.ptrie unit * list literal * list watched_clause := let h := hf.(id) in if is_cons h (if pol then cp else cm) then (cp,cm,ar,acc) else match f with | LAT _ => (cp,cm,ar,acc) | LOP o l => let cp := if pol then set_cons h cp else cp in let cm := if pol then cm else set_cons h cm in let acc := (if pol then cnf_of_op_plus else cnf_of_op_minus) is_classic o l hf acc in cnf_list cnf pol is_classic cp cm ar acc l | LIMPL l r => let ar := if negb (lazy_or is_classic (fun x => List.forallb HCons.is_dec l)) && pol then POS hf::ar else ar in let acc := (if pol then cnf_plus_impl is_classic else cnf_minus_impl) l r hf acc in let '(cp,cm,ar,acc) := cnf_list cnf (negb pol) is_classic cp cm ar acc l in cnf pol is_classic cp cm ar acc r.(elt) r end.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause