term: new function f_close_forall_merge

src/core/term.ml

@@ -1757,6 +1757,13 @@ let f_neq_simp t1 t2 = if t_equal t1 t2 then f_false else f_neq t1 t2
 let is_true_false f = match f.f_node with
   | Ftrue | Ffalse -> true | _  -> false
 
+let f_forall_close_merge vs f =
+  match f.f_node with
+  | Fquant (Fforall, fq) ->
+      let vs', trs, f = f_open_quant fq in
+      f_forall_close (vs@vs') trs f
+  | _ -> f_forall_close vs [] f
+
 (* Could we add an optional argument which toggle
    the simplification to the other map? *)
 

src/core/term.mli

@@ -308,6 +308,13 @@ val f_quant_close_simp : quant -> vsymbol list -> trigger list -> fmla -> fmla
 val f_forall_close_simp : vsymbol list -> trigger list -> fmla -> fmla
 val f_exists_close_simp : vsymbol list -> trigger list -> fmla -> fmla
 
+
+val f_forall_close_merge : vsymbol list -> fmla -> fmla
+(** [forall_close_merge vs f] - put a universal quantifier on top of [f]; merge
+  variable lists if [f] is already a universally quantified formula; reuse
+  triggers of [f], if any, otherwise the quantifier has no triggers. *)
+
+
 (** Expr and trigger traversal *)
 
 val e_map : (term -> term) -> (fmla -> fmla) -> expr -> expr