- let bag, newa, alist, atable =
- List.fold_left
- (fun (bag, newa, alist, atable) c ->
- match simplify ctable maxvar bag c with
- |bag,None -> (bag, newa, alist, atable)
- (* an active clause as been discarded *)
- |bag,Some c1 ->
- if (c1 == c) then
- bag, newa, c :: alist,
- IDX.index_unit_clause atable c
- else
- bag, c1 :: newa, alist, atable)
- (bag,[],[],IDX.DT.empty) alist
- in
- if new_cl then
- bag, (Some cl, Some (clause, (alist,atable), newa))
- else
- (* if new_clause is not cl, we simplify cl with clause *)
- match simplify ctable maxvar bag cl with
- | bag,None ->
- (* cl has been discarded *)
- bag,(None, Some (clause, (alist,atable), newa))
- | bag,Some cl1 ->
- bag,(Some cl1, Some (clause, (alist,atable), newa))
+ let bag, newa, alist, atable =
+ List.fold_left
+ (fun (bag, newa, alist, atable) c ->
+ match simplify ctable maxvar bag c with
+ |bag,None -> (bag, newa, alist, atable)
+ (* an active clause as been discarded *)
+ |bag,Some c1 ->
+ if (c1 == c) then
+ bag, newa, c :: alist,
+ IDX.index_unit_clause atable c
+ else
+ bag, c1 :: newa, alist, atable)
+ (bag,[],[],IDX.DT.empty) alist
+ in
+ if new_cl then
+ bag, (Some cl, Some (clause, (alist,atable), newa))
+ else
+ (* if new_clause is not cl, we simplify cl with clause *)
+ match simplify ctable maxvar bag cl with
+ | bag,None ->
+ (* cl has been discarded *)
+ bag,(None, Some (clause, (alist,atable), newa))
+ | bag,Some cl1 ->
+ bag,(Some cl1, Some (clause, (alist,atable), newa))
+ ;;
+ let prof_simplification_step = HExtlib.profile ~enable "simplification_step";;
+ let simplification_step ~new_cl cl (alist,atable) bag maxvar x =
+ prof_simplification_step.HExtlib.profile (simplification_step ~new_cl cl (alist,atable) bag maxvar) x