From 9a8550de4ef268c50e8ef6eebc9b5e9ca062ced1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Sat, 25 Jan 2025 16:50:50 +0100 Subject: [PATCH] do not check critical pairs with sequential symbols (fix #1140) (#1185) fix #1140 --- src/tool/lcr.ml | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/src/tool/lcr.ml b/src/tool/lcr.ml index cb08a7abe..05ad4beac 100644 --- a/src/tool/lcr.ml +++ b/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 ->