fact: Fixpoint cnf_list (pol:bool) (is_classic: bool) (cp cm: IntMap.ptrie unit) (ar: list literal) (acc: list watched_clause) (l: list HFormula) := match l with | nil => (cp,cm,ar,acc) | f :: l => let '(cp,cm,ar,acc) := cnf pol is_classic cp cm ar acc f.(elt) f in cnf_list pol is_classic cp cm ar acc l end.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause