Function varisat::load::load_clause

pub fn load_clause<'a>(
    ctx: Mut<WatchlistsP, Mut<VsidsP, Mut<VariablesP, Mut<TrailP, Mut<TmpFlagsP, Mut<TmpDataP, Mut<SolverStateP, Mut<ProofP<'a>, Mut<ImplGraphP, Mut<ClauseDbP, Mut<ClauseAllocP, Mut<BinaryClausesP, Mut<AssumptionsP, Mut<AssignmentP, Mut<AnalyzeConflictP, Ref<Context<'a>>>>>>>>>>>>>>>>>, 
    user_lits: &[Lit]
)

Adds a clause to the current formula.

The input uses user variable names.

Removes duplicated literals, ignores tautological clauses (eg. x v -x v y), handles empty clauses and dispatches among unit, binary and long clauses.