let proof = Terms.Step(rule,id,id2,dir,pos,subst) in
let t = Subst.apply_subst subst t in
if filter subst then
- let literal =
+ let tooflex,literal =
match t with
| Terms.Node [ Terms.Leaf eq ; ty; l; r ] when B.eq (B.eqP()) eq ->
- let o = Order.compare_terms l r in
- (* CSC: to avoid equations of the form ? -> T that
- can always be applied and that lead to type-checking errors *)
- (match l,r,o with
- Terms.Var _,_,Terms.Gt
- | _,Terms.Var _,Terms.Lt -> assert false
- | Terms.Var _,_,(Terms.Incomparable | Terms.Invertible) ->
- Terms.Equation (l, r, ty, Terms.Lt)
- | _, Terms.Var _,(Terms.Incomparable | Terms.Invertible) ->
- Terms.Equation (l, r, ty, Terms.Gt)
- | _ -> Terms.Equation (l, r, ty, o))
- | t -> Terms.Predicate t
+ let o = Order.compare_terms l r in
+ (match l,r,o with
+ Terms.Var _,_,Terms.Gt
+ | _,Terms.Var _,Terms.Lt -> assert false
+ | Terms.Var _,_,(Terms.Incomparable | Terms.Invertible) ->
+ true, Terms.Equation (l, r, ty, o)
+ | _, Terms.Var _,(Terms.Incomparable | Terms.Invertible) ->
+ true, Terms.Equation (l, r, ty, o)
+ | _ -> false, Terms.Equation (l, r, ty, o))
+ | t -> false,Terms.Predicate t
in
let bag, uc =
Terms.add_to_bag (0, literal, Terms.vars_of_term t, proof) bag
in
- Some (bag, uc)
+ if tooflex then None else Some (bag, uc)
else
((*prerr_endline ("Filtering: " ^ Pp.pp_foterm t);*)None)
;;
match build_clause bag (fun _ -> true)
Terms.Demodulation (ctx inewside) subst id id2 pos dir
with
- | None -> assert false
+ | None -> (bag,[],t,id) (* see tooflex; was assert false *)
| Some (bag,(id,_,_,_)) ->
(bag,subst,newside,id)
;;