do not check critical pairs with sequential symbols (fix #1140) (#1185)

fix #1140

src/tool/lcr.ml

@@ -47,7 +47,7 @@ let is_ho : rule -> bool = fun r ->
     | _ -> ()
   in try List.iter (contains_abs) r.lhs; false with Exit -> true
 
-(** [is_definable s] says if [s] is definable and non opaque but not AC. *)
+(** [is_definable s] says if [s] is definable and non opaque. *)
 let is_definable : sym -> bool = fun s ->
   (match s.sym_prop with Defin | Injec -> true | _ -> false)
   && not !(s.sym_opaq)
@@ -297,8 +297,9 @@ let _ =
   assert (unif a b = None);
   assert (unif v0 (s v0) = None)
 
-(** [can_handle r] says if the sym_rule [r] can be handled. *)
-let can_handle : sym_rule -> bool = fun (s,r) -> not (is_modulo s || is_ho r)
+(** [can_handle sr] says if the sym_rule [sr] can be handled. *)
+let can_handle : sym_rule -> bool = fun (s,r) ->
+  not (s.sym_mstrat = Sequen || is_modulo s || is_ho r)
 
 (** [iter_rules h rs] iterates function [f] on every rule of [rs]. *)
 let iter_rules : (rule -> unit) -> sym -> rule list -> unit = fun h ->
@@ -584,8 +585,8 @@ let check_cps_subterms_eq : Pos.popt -> sym_rule -> unit =
   in
   iter_subterms_eq pos f l
 
-(** [check_cps_sign_with pos rs'] checks all the critical pairs between all
-   the rules of the signature and [rs']. *)
+(** [check_cps_sign_with pos sign sym_map] checks all the critical pairs
+    between all the rules of the signature and [sym_map]. *)
 let check_cps_sign_with : Pos.popt -> Sign.t -> rule list SymMap.t -> unit =
   fun pos sign sym_map ->
   let f s' rs' =
@@ -603,7 +604,8 @@ let check_cps_sign_with : Pos.popt -> Sign.t -> rule list SymMap.t -> unit =
   in
   SymMap.iter f sym_map
 
-(** [check_cps rs] checks all the critical pairs generated by adding [rs]. *)
+(** [check_cps pos sign srs sym_map] checks all the critical pairs generated
+    by adding [srs]. *)
 let check_cps :
   Pos.popt -> Sign.t -> sym_rule list -> rule list SymMap.t -> unit =
   fun pos sign srs sym_map ->