fact: Definition insert_defs (m : IntMap.ptrie unit * IntMap.ptrie unit) (ar : list literal) (st : state ) := {| fresh_clause_id := fresh_clause_id st; hconsmap := hconsmap st; wneg := wneg st; defs := m; arrows := ar; units := units st; unit_stack := unit_stack st; clauses := clauses st |}.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause