;;
(* move away *)
- let is_identity_clause = function
+ let is_identity_clause ~unify = function
| _, Terms.Equation (_,_,_,Terms.Eq), _, _ -> true
- | _, Terms.Equation (l,r,_,_), vl, proof ->
+ | _, Terms.Equation (l,r,_,_), vl, proof when unify ->
(try ignore(Unif.unification vl [] l r); true
with FoUnif.UnificationFailure _ -> false)
| _, Terms.Predicate _, _, _ -> assert false
+ | _ -> false
;;
let build_new_clause bag maxvar filter rule t subst vl id id2 pos dir =
(* demodulate and check for subsumption *)
let simplify table maxvar bag clause =
let bag, clause = demodulate bag clause table in
- if is_identity_clause clause then None
+ if is_identity_clause ~unify:false clause then None
else
match is_subsumed ~unify:false bag maxvar clause table with
| None -> Some (bag, clause)
(* this is like simplify but raises Success *)
let simplify_goal maxvar table bag g_actives clause =
let bag, clause = demodulate bag clause table in
- if (is_identity_clause clause)
+ if (is_identity_clause ~unify:true clause)
then raise (Success (bag, maxvar, clause))
else match is_subsumed ~unify:true bag maxvar clause table with
| None ->