fact: Definition insert_literal (l:Annot.t literal) (st: state) : state := {| fresh_clause_id := fresh_clause_id st; hconsmap := hconsmap st; defs := defs st; wneg := remove_wneg (Annot.elt l) (wneg st); arrows := if is_neg_arrow (Annot.elt l) then (Annot.elt l::arrows st) else arrows st; units := add_literal l (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