Function varisat::proof::add_clause

pub fn add_clause<'a>(
    ctx: Const<VariablesP, Mut<SolverStateP, Mut<ProofP<'a>, Ref<Context<'a>>>>>, 
    clause: &[Lit]
)

Call when adding an external clause.

This is required for on the fly checking and checking of incremental solving.

Note: this function expects the clause to use solver var names.