- | Terms.Equation (l,r,ty,_) ->
- let left_position = if jump_to_right then None else
- first_position [2]
- (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ]) l
- (demod table vl)
- in
- match left_position with
- | Some (newt, subst, varlist, id2, pos, dir) ->
- begin
- match build_clause bag (fun _ -> true) Terms.Demodulation
- newt subst varlist id id2 pos dir
- with
- | None -> assert false
- | Some x -> Some (x,false)
- end
- | None ->
- match first_position
- [3] (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ]) r
- (demod table vl)
- with
- | None -> None
- | Some (newt, subst, varlist, id2, pos, dir) ->
- match build_clause bag (fun _ -> true)
- Terms.Demodulation newt subst varlist id id2 pos dir
- with
- | None -> assert false
- | Some x -> Some (x,true)
- ;;
-
- let rec demodulate ~jump_to_right bag clause table =
- match demodulate_once ~jump_to_right bag clause table with
- | None -> bag, clause
- | Some ((bag, clause),r) -> demodulate ~jump_to_right:r
- bag clause table
- ;;
-
- let demodulate bag clause table = demodulate ~jump_to_right:false
- bag clause table
+ | Terms.Equation (l,r,ty,_) as lit ->
+ let bag,l,id1,lit = if jump_to_right then (bag,l,id,lit) else
+ parallel_positions bag [2]
+ (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ]) id lit l
+ (parallel_demod table vl clause_ctx)
+ in
+ let jump_to_right = id1 = id in
+ let bag,r,id2,lit =
+ parallel_positions bag [3]
+ (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ]) id1 lit r
+ (parallel_demod table vl clause_ctx)
+ in
+ if id = id2 then None
+ else
+ Some ((bag,id2,lit),jump_to_right)
+ ;;
+
+ let rec demodulate bag (id,nlit,plit,vl,proof) table =
+ let rec demod_lit ~jump_to_right bag id lit clause_ctx =
+ match demodulate_once ~jump_to_right bag id lit vl table clause_ctx with
+ | None -> bag, id, lit
+ | Some ((bag, id, lit),jump) ->
+ demod_lit ~jump_to_right:jump bag id lit clause_ctx
+ in
+ (*let cmp_bag,cmp_cl = match nlit,plit with
+ |[],[lit,_] ->
+ let bag, id, lit = demod_lit ~jump_to_right:false bag id lit (fun l -> nlit, [l,true])
+ in
+ let cl,_,_ = Terms.get_from_bag id bag in
+ bag,cl
+ |[lit,_],[] ->
+ let bag, id, lit = demod_lit ~jump_to_right:false bag id lit (fun l -> [l,true],[])
+ in
+ let cl,_,_ = Terms.get_from_bag id bag in
+ bag,cl
+ |_ -> assert false
+ in*)
+ let nlit,_,bag,id = if nlit = [] then nlit,[],bag,id
+ else List.fold_left
+ (fun (pre,post,bag,id) (lit,sel) ->
+ let bag, id, lit =
+ demod_lit ~jump_to_right:false bag id lit (fun l -> pre@[l,sel]@post,plit)
+ in
+ if post=[] then pre@[(lit,sel)],[],bag,id
+ else pre@[(lit,sel)],List.tl post,bag,id)
+ ([],List.tl nlit, bag, id) nlit
+ in
+ let _,_,bag,id = if plit = [] then plit,[],bag,id
+ else List.fold_left
+ (fun (pre,post,bag,id) (lit,sel) ->
+ let bag, id, lit =
+ demod_lit ~jump_to_right:false bag id lit (fun l -> nlit,pre@[l,sel]@post)
+ in
+ if post=[] then pre@[(lit,sel)],[],bag,id
+ else pre@[(lit,sel)],List.tl post,bag,id)
+ ([],List.tl plit, bag, id) plit
+ in
+ let cl,_,_ = Terms.get_from_bag id bag in
+ bag,cl
+ ;;
+
+ let prof_demodulate = HExtlib.profile ~enable "demodulate";;
+ let demodulate bag clause x =
+ prof_demodulate.HExtlib.profile (demodulate bag clause) x