let assume cnf ~cnumber = let implied = ref [] in let cnf = List.map (List.map (Enumsolver_types.add_atom implied)) cnf in let blevel = min_blevel !implied in assert (blevel >= 0 && blevel <= decision_level ()); cancel_until blevel; List.iter (fun (a, c, lvl) -> if lvl = blevel && a.var.level < 0 then begin Vec.push env.learnts c; attach_clause c; clause_bump_activity c; enqueue a lvl (Some c) end) !implied; (match propagate () with | None -> () | Some confl -> if decision_level () = 0 then report_b_unsat confl else cancel_until 0); init_solver cnf ~cnumber