fix(FPA): Separate semantic triggers upon trigger construction

Currently, the theories are responsible for populating the `semantic`
field of triggers when a lemma with semantic triggers is added to the
theory (call to `assume_th_elt`).

This means that such a lemma lives for some time *without* semantic
triggers: in particular, it is initially created using `mk_forall`
without semantic triggers. During that call, the guard in
`find_particular_subst` preventing the "particular substitution"
optimization from triggering for lemmas with semantic trigger is
ignored; which means that the "particular substitution" optimization is
actually applied to lemmas with semantic triggers.

In particular, this optimization makes the lemma
`float_of_pos_pow_of_two` in the FPA theory unsound, because it removes
the check that `x` is actually a power of two, and causes OCamlPro#1111.

This patch makes the `Expr` module responsible for separating syntaxic
and semantic triggers, rather than the theory. This ensures that a lemma
with semantic triggers never appears as having no semantic triggers. In
order to make sure this invariant is properly maintained, the `trigger`
type is again made private to the `Expr` module. This required moving
from sorting code from the `Matching` module to the `Expr` module, also
ensuring that triggers are properly sorted for matching purposes at all
times.

Fixes OCamlPro#1111

Author: bclement-ocp

src/lib/frontend/cnf.ml

@@ -177,15 +177,9 @@ let rec make_term quant_basename t =
 
 and make_trigger ~in_theory name quant_basename hyp (e, from_user) =
   let content = List.map (make_term quant_basename) e in
-  let t_depth =
-    List.fold_left (fun z t -> max z (E.depth t)) 0 content in
   (* clean trigger:
      remove useless terms in multi-triggers after inlining of lets*)
-  let trigger =
-    { E.content ; t_depth; semantic = []; (* will be set by theories *)
-      hyp; from_user;
-    }
-  in
+  let trigger = E.mk_trigger ~user:from_user ~hyp content in
   E.clean_trigger ~in_theory name trigger
 
 and make_form name_base ~toplevel f loc ~decl_kind : E.t =

src/lib/frontend/d_cnf.ml

@@ -1655,14 +1655,11 @@ and make_trigger ?(loc = Loc.dummy) ~name_base ~decl_kind
     mk_expr ~loc ~name_base ~decl_kind
   in
   let content = List.map mk_expr e in
-  let t_depth =
-    List.fold_left (fun z t -> max z (E.depth t)) 0 content in
   (* clean trigger:
      remove useless terms in multi-triggers after inlining of lets*)
-  let trigger =
-    { E.content; t_depth; semantic = []; (* will be set by theories *)
-      hyp; from_user; }
-  in
+  let trigger = E.mk_trigger ~user:from_user ~hyp content in
+  if not in_theory && not (Lists.is_empty trigger.semantic) then
+    Errors.typing_error ThSemTriggerError loc;
   E.clean_trigger ~in_theory name trigger
 
 (** Preprocesses the body of a goal by:

src/lib/reasoners/intervalCalculus.ml

@@ -2481,64 +2481,20 @@ let instantiate ~do_syntactic_matching match_terms env uf selector =
   env, insts
 
 
-let separate_semantic_triggers =
-  fun th_form ->
-  let { E.user_trs; _ } as q =
-    match E.form_view th_form with
-    | E.Lemma q -> q
-    | E.Unit _ | E.Clause _ | E.Literal _ | E.Skolem _
-    | E.Let _ | E.Iff _ | E.Xor _ -> assert false
-  in
-  let r_triggers =
-    List.rev_map
-      (fun tr ->
-         (* because sem-triggers will be set by theories *)
-         assert (tr.E.semantic == []);
-         let syn, sem =
-           List.fold_left
-             (fun (syn, sem) t ->
-                match E.term_view t with
-                | { E.f = Symbols.In (lb, ub); xs = [x]; _ } ->
-                  syn, (E.Interval (x, lb, ub)) :: sem
-
-                | { E.f = Symbols.MapsTo x; xs = [t]; _ } ->
-                  syn, (E.MapsTo (x, t)) :: sem
-
-                | { E.f = Sy.Op Not_theory_constant; xs = [x]; _ } ->
-                  syn, (E.NotTheoryConst x) :: sem
-
-                | { E.f = Sy.Op Is_theory_constant; xs = [x]; _ } ->
-                  syn, (E.IsTheoryConst x) :: sem
-
-                | { E.f = Sy.Op Linear_dependency; xs = [x;y]; _ } ->
-                  syn, (E.LinearDependency(x,y)) :: sem
-
-                | _ -> t::syn, sem
-             )([], []) (List.rev tr.E.content)
-         in
-         {tr with E.content = syn; semantic = sem}
-      )user_trs
-  in
-  E.mk_forall
-    q.E.name q.E.loc q.E.binders (List.rev r_triggers) q.E.main
-    ~toplevel:true ~decl_kind:E.Dtheory
-
 let assume_th_elt t th_elt dep =
   let { Expr.axiom_kind; ax_form; th_name; extends; _ } = th_elt in
   let kd_str =
     if axiom_kind == Util.Propagator then "Th propagator" else "Th CS"
   in
   match extends with
   | Util.NIA | Util.NRA | Util.FPA | Util.RIA ->
-    let th_form = separate_semantic_triggers ax_form in
-    let th_elt = {th_elt with Expr.ax_form} in
     if get_debug_fpa () >= 2 then
       Printer.print_dbg
         ~module_name:"IntervalCalculus" ~function_name:"assume_th_elt"
         "[Theory %s][%s] %a"
-        th_name kd_str E.print th_form;
-    assert (not (ME.mem th_form t.th_axioms));
-    {t with th_axioms = ME.add th_form (th_elt, dep) t.th_axioms}
+        th_name kd_str E.print ax_form;
+    assert (not (ME.mem ax_form t.th_axioms));
+    {t with th_axioms = ME.add ax_form (th_elt, dep) t.th_axioms}
 
   | _ -> t
 

src/lib/reasoners/matching.ml

@@ -482,19 +482,10 @@ module Make (X : Arg) : S with type theory = X.t = struct
     Debug.match_pats_modulo pat lsubsts;
     List.fold_left (match_one_pat mconf env tbox pat) [] lsubsts
 
-  let pat_weight s t =
-    let sf = (Expr.term_view s).f in
-    let tf = (Expr.term_view t).f in
-    match sf, tf with
-    | Symbols.Name _, Symbols.Op _ -> -1
-    | Symbols.Op _, Symbols.Name _ -> 1
-    | _ -> Expr.(depth t - depth s)
-
   let matching mconf env tbox pat_info =
     let open Matching_types in
     let pats = pat_info.trigger in
     let pats_list = pats.E.content in
-    Options.heavy_assert (fun () -> Lists.is_sorted pat_weight pats_list);
     Debug.matching pats;
     if List.length pats_list > Options.get_max_multi_triggers_size () then
       pat_info, []
@@ -610,21 +601,16 @@ module Make (X : Arg) : S with type theory = X.t = struct
 
   module HE = Hashtbl.Make (E)
 
-  let sort_pats tr =
-    let content = List.stable_sort pat_weight tr.E.content in
-    { tr with content }
-
   let triggers_of, clear_triggers_of_trs_tbl =
     let trs_tbl = HEI.create 101 in
     let triggers_of q mconf =
       match q.E.user_trs with
-      | _::_ as l -> List.map sort_pats l
+      | _::_ as l -> l
       | [] ->
         try HEI.find trs_tbl (q.E.main, mconf)
         with Not_found ->
           let trs =
             E.make_triggers q.E.main q.E.binders q.E.kind mconf
-            |> List.map sort_pats
           in
           HEI.add trs_tbl (q.E.main, mconf) trs;
           trs
@@ -641,7 +627,6 @@ module Make (X : Arg) : S with type theory = X.t = struct
       with Not_found ->
         let trs =
           E.resolution_triggers ~is_back:true q
-          |> List.map sort_pats
         in
         HE.add trs_tbl q.E.main trs;
         trs
@@ -658,7 +643,6 @@ module Make (X : Arg) : S with type theory = X.t = struct
       with Not_found ->
         let trs =
           E.resolution_triggers ~is_back:false q
-          |> List.map sort_pats
         in
         HE.add trs_tbl q.E.main trs;
         trs

src/lib/structures/expr.ml

@@ -95,8 +95,6 @@ and semantic_trigger =
 
 and trigger = {
   content : t list;
-  (* this field is filled (with a part of 'content' field) by theories
-     when assume_th_elt is called *)
   semantic : semantic_trigger list;
   hyp : t list;
   t_depth : int;
@@ -843,6 +841,50 @@ let is_ite s = match s with
   | Sy.Op Sy.Tite -> true
   | _ -> false
 
+let pat_weight s t =
+  let sf = (term_view s).f in
+  let tf = (term_view t).f in
+  match sf, tf with
+  | Symbols.Name _, Symbols.Op _ -> -1
+  | Symbols.Op _, Symbols.Name _ -> 1
+  | _ -> depth t - depth s
+
+let separate_semantic_triggers content =
+  let syn, sem =
+    List.fold_left
+      (fun (syn, sem) t ->
+         match term_view t with
+         | { f = Symbols.In (lb, ub); xs = [x]; _ } ->
+           syn, (Interval (x, lb, ub)) :: sem
+
+         | { f = Symbols.MapsTo x; xs = [t]; _ } ->
+           syn, (MapsTo (x, t)) :: sem
+
+         | { f = Sy.Op Not_theory_constant; xs = [x]; _ } ->
+           syn, (NotTheoryConst x) :: sem
+
+         | { f = Sy.Op Is_theory_constant; xs = [x]; _ } ->
+           syn, (IsTheoryConst x) :: sem
+
+         | { f = Sy.Op Linear_dependency; xs = [x;y]; _ } ->
+           syn, (LinearDependency(x,y)) :: sem
+
+         | _ -> t::syn, sem
+      )([], []) (List.rev content)
+  in
+  syn, sem
+
+let mk_trigger ?user:(from_user = false) ?depth ?(hyp = []) content =
+  let t_depth =
+    match depth with
+    | Some t_depth -> t_depth
+    | None ->
+      List.fold_left (fun z t -> max z t.depth) 0 content
+  in
+  let content = List.stable_sort pat_weight content in
+  let content, semantic = separate_semantic_triggers content in
+  { content ; semantic ; hyp ; t_depth ; from_user }
+
 let mk_term s l ty =
   assert (match s with Sy.Lit _ | Sy.Form _ -> false | _ -> true);
   let d = match l with
@@ -1375,9 +1417,11 @@ let rec apply_subst_aux (s_t, s_ty) t =
 
 and apply_subst_trigger subst ({ content; _ } as tr) =
   {tr with
-   content = List.map (apply_subst_aux subst) content;
-   (* semantic_trigger = done on theory side *)
-   (* hyp = done on theory side *)
+   content =
+     List.rev_map (apply_subst_aux subst) content |>
+     List.stable_sort pat_weight
+     (* semantic_trigger = done on theory side *)
+     (* hyp = done on theory side *)
   }
 
 (* *1* We should never subst formulas inside termes. We could allow to
@@ -1643,12 +1687,7 @@ let resolution_triggers ~is_back { kind; main = f; binders; _ } =
     | Dpredicate t | Dfunction t ->
       if type_info t != Ty.Tbool then []
       else
-        [ { content = [t];
-            hyp = [];
-            semantic = [];
-            t_depth = t.depth;
-            from_user = false;
-          } ]
+        [ mk_trigger ~depth:t.depth [t] ]
     | Dtheory | Dobjective -> []
     | Daxiom
     | Dgoal ->
@@ -1664,12 +1703,7 @@ let resolution_triggers ~is_back { kind; main = f; binders; _ } =
               TSet.exists (cand_is_more_general t) others then
              acc
            else
-             { content = [t];
-               hyp = [];
-               semantic = [];
-               t_depth = t.depth;
-               from_user = false;
-             } :: acc
+             mk_trigger ~depth:t.depth [t] ::acc
         )cand []
 
 let free_type_vars_as_types e =
@@ -2212,6 +2246,7 @@ module Triggers = struct
         if sz_l = sz_s then trig
         else
           let content = TMap.fold (fun t _ acc -> t :: acc) res [] in
+          let content = List.stable_sort pat_weight content in
           if Options.get_verbose () then
             Printer.print_dbg ~module_name:"Cnf"
               ~function_name:"clean_trigger"
@@ -2258,15 +2293,7 @@ module Triggers = struct
       aux vars (STRS.empty, Var.Map.empty) e
 
   let triggers_of_list l =
-    List.map
-      (fun content ->
-         { content;
-           semantic = [];
-           hyp = [];
-           from_user = false;
-           t_depth = List.fold_left (fun z t -> max z (depth t)) 0 content
-         }
-      ) l
+    List.map mk_trigger l
 
   (* Should return false iff lit_view fails with Failure _, but this version
      does not build the literal view. *)

src/lib/structures/expr.mli

@@ -91,10 +91,8 @@ and semantic_trigger =
   | IsTheoryConst of t
   | LinearDependency of t * t
 
-and trigger = (*private*) {
+and trigger = private {
   content : t list;
-  (* this field is filled (with a part of 'content' field) by theories
-     when assume_th_elt is called *)
   semantic : semantic_trigger list;
   hyp : t list;
   t_depth : int;
@@ -192,6 +190,7 @@ val print_tagged_classes : Format.formatter -> Set.t list -> unit
 
 (** smart constructors for terms *)
 
+val mk_trigger : ?user:bool -> ?depth:int -> ?hyp:t list -> t list -> trigger
 val mk_term : Symbols.t -> t list -> Ty.t -> t
 val vrai : t
 val faux : t