Proper handling of in_interval and bounds in triggers

src/interface/tag.ml

@@ -34,8 +34,9 @@ module type Ae_Base = sig
   val named : string t
   (** A tag used to name formulas in alt-ergo. *)
 
-  val triggers : term list list t
-  (** Multi-triggers that can be added to quantified formulas *)
+  val triggers : term list t
+  (** Multi-triggers that can be added to quantified formulas.
+      Each term is a multi-trigger represented as a conjunction of triggers. *)
 
   val filters : term list t
   (** Filters that can be added to quantified formulas *)
@@ -55,9 +56,11 @@ module type Smtlib_Base = sig
     (** A tag used to named formulas in smtlib.
         Should correspond to the `:named` attribute. *)
 
-    val triggers : term list list t
+    val triggers : term list t
     (** Multi-triggers (typically annotated on the body of
-        a quantified formula and not the quantified formula itself). *)
+        a quantified formula and not the quantified formula itself).
+        Each term is a multi-trigger represented as a
+        conjunction of triggers. *)
 
     val rwrt : unit t
     (** A flag (i.e. unit tag), indicating that the tagged term/formula

src/interface/term.ml

@@ -573,10 +573,12 @@ module type Tff = sig
   (** Given a constructor [c] and a term [t], returns a terms that evaluates
       to [true] iff [t] has [c] as head constructor. *)
 
+  val _true : t
+  (** The `true` literal. *)
+
   val _and : t list -> t
   (** Conjunction of formulas *)
 
-
   val lam : ty_var list * Var.t list -> t -> t
   (** Create a local function. *)
 
@@ -681,8 +683,11 @@ module type Ae_Base = sig
   val distinct : t list -> t
   (** Distinct constraints on terms. *)
 
-  val in_interval : t -> bool * bool -> t -> t -> t
-  (** Semantic trigger: "in interval" check. *)
+  val multi_trigger : t list -> t
+  (** Create a multi trigger from a list of arbtirary terms. *)
+
+  val semantic_trigger : t -> t
+  (** Semantic triggers for alt-ergo. *)
 
   val maps_to : term_var -> t -> t
   (** Semantic trigger: maps to. *)
@@ -741,8 +746,8 @@ module type Ae_Arith = sig
   val real : string -> t
   (** Real literals *)
 
-  val _and : t list -> t
-  (** Conjunction of formulas *)
+  val semantic_trigger : t -> t
+  (** Semantic triggers for alt-ergo. *)
 
   module Int : sig
     include Ae_Arith_Common with type t := t
@@ -1220,6 +1225,9 @@ module type Smtlib_Base = sig
   val distinct : t list -> t
   (** Distinct constraints on terms. *)
 
+  val multi_trigger : t list -> t
+  (** Create a multi trigger from a list of arbtirary terms. *)
+
 end
 
 (** Common signature for first-order arithmetic *)

src/interface/ty.ml

@@ -175,6 +175,12 @@ module type Ae_Base = sig
   val unit : t
   (** Unit type *)
 
+  val int : t
+  (** The type of integers *)
+
+  val real : t
+  (** The type of reals *)
+
 end
 
 (** Signature required by types for typing ae's arithmetic *)

src/standard/builtin.ml

@@ -24,8 +24,9 @@ type _ t += | Unit | Univ
 type _ t += Coercion
 
 type _ t +=
-  | In_interval of bool * bool
   | Maps_to
+  | Multi_trigger
+  | Semantic_trigger
 
 (* Boolean builtins *)
 (* ************************************************************************* *)

src/standard/builtin.mli

@@ -94,23 +94,24 @@ type _ t +=
       guarded by a clause verifying the rational is an integer). *)
 
 type _ t +=
-  | In_interval of bool * bool
-  (** [In_interval (b1, b2): Int -> Int -> Int -> Prop]:
-      Tests whether or not an interger is in an interval, [b1] (resp. [b2])
-      determines if the interval is open on the lower bound
-      (resp. upper bound).
-
-      [warning:] It is an Alt-Ergo semantic trigger that should only be
-      allowed inside theories. *)
+  | Multi_trigger
+  (** [Multi_trigger: 'a1 ... 'an. 'a1 -> ... -> 'an -> Prop]:
+      Create a multi trigger: it takes an arbitrarily long list
+      of terms of arbitrary types. *)
 
   | Maps_to
-  (** [Maps_to: 'term_var -> 'term -> 'term]:
+  (** [Maps_to: 'term_var -> 'term -> Prop]:
       Used in semantic triggers for floating point arithmetic.
       See [alt-ergo/src/preludes/fpa-theory-2017-01-04-16h00.ae].
 
       [warning:] It is an Alt-Ergo semantic trigger that should only be
       allowed inside theories. *)
 
+  | Semantic_trigger
+  (** [Semantic_trigger: Prop -> Prop]:
+      Denote that its argument is a semantic trigger
+      (used only by Alt-ergo currently). *)
+
 (** {2 Boolean Builtins} *)
 (*  ************************************************************************* *)
 

src/standard/expr.ml

@@ -1895,9 +1895,17 @@ module Term = struct
       mk' ~builtin:Builtin.Coercion "coerce"
         [a; b] [Ty.of_var a] (Ty.of_var b)
 
-    let in_interval (b1, b2) = mk'
-        ~name:"in_interval" ~builtin:(Builtin.In_interval (b1, b2))
-        "InInterval" [] [Ty.int; Ty.int; Ty.int] Ty.prop
+    let multi_trigger =
+      with_cache ~cache:(Hashtbl.create 5) (fun n ->
+          let vars = List.init n (fun _ -> Ty.Var.mk "_") in
+          let tys = List.map Ty.of_var vars in
+          mk' ~name:"multi-trigger" ~builtin:Builtin.Multi_trigger
+            "Multi_trigger" vars tys Ty.prop
+        )
+
+    let semantic_trigger =
+      mk' ~name:"sem_trig" ~builtin:Builtin.Semantic_trigger
+        "Semantic_trigger" [] [Ty.prop] Ty.prop
 
     let maps_to =
       let a = Ty.Var.mk "alpha" in
@@ -3140,9 +3148,14 @@ module Term = struct
       in
       mk_record aux l
 
+  (* Triggers *)
+  let multi_trigger l =
+    let tys = List.map ty l in
+    apply_cst (Const.multi_trigger (List.length l)) tys l
+
   (* Alt-Ergo's semantic triggers *)
-  let in_interval t (b1, b2) t1 t2 =
-    apply_cst (Const.in_interval (b1, b2)) [] [t; t1; t2]
+  let semantic_trigger trig =
+    apply_cst Const.semantic_trigger [] [trig]
 
   let maps_to tv t =
     let ntv = of_var tv in

src/standard/expr.mli

@@ -891,8 +891,11 @@ module Term : sig
     val coerce : t
     (** Type coercion. *)
 
-    val in_interval : bool * bool -> t
-    (** Interger interval inclusion. *)
+    val multi_trigger : int -> t
+    (** Multi_triggers, indexed by the number of triggers. *)
+
+    val semantic_trigger : t
+    (** Semantic_triggers. *)
 
     val maps_to : t
     (** Mapping (used in triggers).  *)
@@ -1815,10 +1818,15 @@ module Term : sig
   val subst : ?fix:bool -> Ty.subst -> subst -> t -> t
   (** Substitution over terms. *)
 
+  (* Triggers *)
+
+  val multi_trigger : t list -> t
+  (** Create a multi trigger from a list of arbtirary terms. *)
+
   (* Alt-Ergo's semantic triggers *)
 
-  val in_interval : t -> bool * bool -> t -> t -> t
-  (** Interger interval inclusion. *)
+  val semantic_trigger : t -> t
+  (** Semantic triggers. *)
 
   val maps_to : Var.t -> t -> t
   (** Variable mapping to term. *)

src/standard/term.ml

@@ -48,6 +48,7 @@ type builtin =
   | Record_with
   | Record_access       (* record operations *)
 
+  | Multi_trigger       (* multi-triggers *)
   | Maps_to
   | In_interval of bool * bool
   | Check | Cut         (* alt-ergo builtins *)
@@ -144,6 +145,7 @@ let builtin_to_string = function
   | Record -> "record"
   | Record_with -> "record_with"
   | Record_access -> "."
+  | Multi_trigger -> "multi"
   | Maps_to -> "↦"
   | In_interval (b, b') ->
     let bracket = function true -> "]" | false -> "[" in
@@ -516,38 +518,39 @@ let arrow ?loc arg ret = fun_ty ?loc [arg] ret
 
 module S = Set.Make(Id)
 
-let rec free_vars acc t =
+let rec free_ids ~test acc t =
   match t.term with
   | Builtin _ -> acc
-  | Colon (t, t') -> free_vars (free_vars acc t) t'
-  | Symbol i -> if i.Id.ns = Namespace.Var then S.add i acc else acc
+  | Colon (t, t') -> free_ids ~test (free_ids ~test acc t) t'
+  | Symbol id -> if test id then S.add id acc else acc
   | App (t, l) ->
-    List.fold_left free_vars (free_vars acc t) l
+    List.fold_left (free_ids ~test) (free_ids ~test acc t) l
   | Binder (Arrow, l, t) ->
-    List.fold_left free_vars (free_vars acc t) l
+    List.fold_left (free_ids ~test) (free_ids ~test acc t) l
   | Binder (_, l, t) ->
-    let s = free_vars S.empty t in
+    let s = free_ids ~test S.empty t in
     let bound, free =
-      List.fold_left free_vars_bound (S.empty, S.empty) l
+      List.fold_left (free_ids_bound ~test) (S.empty, S.empty) l
     in
     let s' = S.filter (fun x -> not (S.mem x bound)) s in
     S.union acc (S.union s' free)
   | Match (t, l) ->
     let acc = List.fold_left (fun acc (pattern, branch) ->
-        let s = free_vars S.empty branch in
-        let bound = free_vars S.empty pattern in
+        let s = free_ids ~test S.empty branch in
+        let bound = free_ids ~test S.empty pattern in
         let s' = S.filter (fun x -> not (S.mem x bound)) s in
         S.union s' acc
       ) acc l in
-    free_vars acc t
+    free_ids ~test acc t
 
-and free_vars_bound (bound, free) t =
+and free_ids_bound ~test (bound, free) t =
   match t.term with
-  | Colon (v, ty) -> free_vars bound v, free_vars free ty
-  | _ -> free_vars bound t, free
+  | Colon (v, ty) -> free_ids ~test bound v, free_ids ~test free ty
+  | _ -> free_ids ~test bound t, free
 
 let fv t =
-  S.elements (free_vars S.empty t)
+  let test id = id.Id.ns = Namespace.Var in
+  S.elements (free_ids ~test S.empty t)
 
 
 (* {2 Wrappers for alt-ergo} *)
@@ -557,7 +560,8 @@ let bitv ?loc s = const ?loc Id.(mk (Value Bitvector) s)
 let cut = unary (builtin Cut)
 let check = unary (builtin Check)
 
-let trigger = and_
+let trigger ?loc l =
+  apply ?loc (builtin ?loc Multi_trigger ()) l
 
 let triggers_t = Id.(mk Attr "triggers")
 let triggers ?loc t = function
@@ -584,7 +588,6 @@ let maps_to ?loc id t =
 let in_interval ?loc t (lb, ls) (rb, rs) =
   tertiary (builtin (In_interval (ls, rs))) ?loc t lb rb
 
-
 (* {2 Wrappers for dimacs} *)
 
 let atom ?loc i =

src/standard/term.mli

@@ -123,6 +123,8 @@ type builtin =
   | Record_access
   (** Record field access *)
 
+  | Multi_trigger
+  (* Multi-triggers *)
   | Maps_to
   (** Mapping; used in Alt-ergo triggers. *)
   | In_interval of bool * bool
@@ -167,7 +169,7 @@ type binder =
   *)
   | Let_par
   (** Similar to [Let_seq]; except that the list of bindings should be considered all
-      bound at the same time/level/scope. 
+      bound at the same time/level/scope.
       More precisely, for [Let_seq], the list of bindings is to be understood
       sequentially (i.e. [Let_seq (b1 :: b2 ...)] is semantically the same as
       [Let_seq b1 (Let_seq b2 (..))]. For [Let_par], the list of bindings all
@@ -242,6 +244,15 @@ val ite_t : ?loc:location -> unit -> t
 
 (** {2 Term inspection} *)
 
+module S : Set.S with type elt = Id.t
+(** Sets of Ids *)
+
+val free_ids :
+  test:(Id.t -> bool) ->
+  S.t -> t -> S.t
+(** Returns the set of identifiers that respect the test:predicate function,
+    and occurs free in the term (i.e. not bound by a binder). *)
+
 val fv : t -> Id.t list
 (** Return the list of free variables (i.e currently, Ids that are in
     the [Var] namespace). *)