- if is_subsumed ~unify:false clause table then None
- else Some (bag, clause)
+ match is_subsumed ~unify:false bag maxvar clause table with
+ | None -> Some (bag, clause)
+ | Some _ -> None
+ ;;
+
+ let one_pass_simplification new_clause (alist,atable) bag maxvar =
+ match simplify atable maxvar bag new_clause with
+ | None -> None (* new_clause has been discarded *)
+ | Some (bag, clause) ->
+ let ctable = IDX.index_unit_clause IDX.DT.empty clause in
+ let bag, alist, atable =
+ List.fold_left
+ (fun (bag, alist, atable as acc) c ->
+ match simplify ctable maxvar bag c with
+ |None -> acc (* an active clause as been discarded *)
+ |Some (bag, c1) ->
+ bag, c :: alist, IDX.index_unit_clause atable c)
+ (bag,[],IDX.DT.empty) alist
+ in
+ Some (clause, bag, (alist,atable))