- (* Simplification of new_clause with : *
- * - actives and cl if new_clause is not cl *
- * - only actives otherwise *)
- match
- simplify atable1 maxvar bag new_clause with
- | bag,None -> bag,(Some cl, None) (* new_clause has been discarded *)
- | bag,Some clause ->
- (* Simplification of each active clause with clause *
- * which is the simplified form of new_clause *)
- let ctable = IDX.index_unit_clause IDX.DT.empty clause in
- 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))
+ (* Simplification of new_clause with : *
+ * - actives and cl if new_clause is not cl *
+ * - only actives otherwise *)
+ match
+ simplify atable1 maxvar bag new_clause with
+ | bag,None -> bag,(Some cl, None) (* new_clause has been discarded *)
+ | bag,Some clause ->
+ (* Simplification of each active clause with clause *
+ * which is the simplified form of new_clause *)
+ let ctable = IDX.index_unit_clause maxvar IDX.DT.empty clause in
+ 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 maxvar 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