Documentation of quantified type in Expr (OCamlPro#1106)

* Documentation of quantified type in `Expr`

While fixing the issue OCamlPro#1099, I wrote a bit of documentation for `Expr`.

* Review changes

* Clarify CNF form of implications

src/lib/structures/expr.ml

@@ -70,11 +70,9 @@ and quantified = {
   toplevel : bool;
   user_trs : trigger list;
   binders : binders;
-  (* These fields should be (ordered) lists ! important for skolemization *)
-  sko_v : t list;
-  sko_vty : Ty.t list;
-  loc : Loc.t; (* location of the "GLOBAL" axiom containing this quantified
-                  formula. It forms with name a unique id *)
+  sko_v : t list; (* This list has to be ordered for the skolemization. *)
+  sko_vty : Ty.t list; (* This list has to be ordered for the skolemization. *)
+  loc : Loc.t;
   kind : decl_kind;
 }
 
@@ -1471,6 +1469,11 @@ and mk_forall_bis (q : quantified) =
   if Var.Map.is_empty binders && Ty.Svty.is_empty q.main.vty then q.main
   else
     let q = {q with binders} in
+    (* Attempt to reduce the number of quantifiers. We try to find a
+       particular substitution [sbs] such that the application of [sbs]
+       on [q.main] produces a formula [g] such that
+       - [g] has less free term variables than [q.main] in [binders];
+       - the universal closures of [f] and [g] are equivalent. *)
     match find_particular_subst binders q.user_trs q.main with
     | None -> mk_forall_ter q
 
@@ -1487,10 +1490,17 @@ and mk_forall_bis (q : quantified) =
         let q = {q with binders; user_trs = trs; sko_v; main = f } in
         mk_forall_bis q
 
+(* If [f] is a formula of the form [x = a -> P(x)] where [a] doesn't content
+   [x], this function produces the substitution { x |-> a }.
+
+   Notice that formulas [x = a -> P(x)] are represented by
+   [Clause (x <> a, P(x), _)] or [Clause (P(x), x <> a, _)].
+
+   {b Note}: this heuristic isn't used if the user has defined filters.
+
+   @return [None] if the formula hasn't the right form. *)
 and find_particular_subst =
   let exception Found of Var.t * t in
-  (* ex: in "forall x, y : int. x <> 1 or f(y) = x+1 or P(x,y)",
-     x can be replaced with 1 *)
   let rec find_subst v tv f =
     match form_view f with
     | Unit _ | Lemma _ | Skolem _ | Let _ | Iff _ | Xor _ -> ()
@@ -1513,6 +1523,7 @@ and find_particular_subst =
       | _ -> ()
   in
   fun binders trs f ->
+    (* TODO: move the test for `trs` outside. *)
     if not (Ty.Svty.is_empty f.vty) || has_hypotheses trs ||
        has_semantic_triggers trs
     then
@@ -2039,19 +2050,27 @@ module Triggers = struct
 
   let not_pure t = not t.pure
 
+  (* Collect all the term variables in [t] that are in the set [bv]. *)
   let vars_of_term bv acc t =
     Var.Map.fold
       (fun v _ acc ->
          if Var.Set.mem v bv then Var.Set.add v acc else acc
       )
       t.vars acc
 
+  (* TODO: we should define here a predicate `good_triggers`
+     and call it with List.filter in the appropriate locations. *)
   let filter_good_triggers (bv, vty) trs =
     List.filter
       (fun { content = l; _ } ->
+         (* Check if the multi-trigger covers all the type and term
+            variables. *)
          not (List.exists not_pure l) &&
          let s1 = List.fold_left (vars_of_term bv) Var.Set.empty l in
          let s2 = List.fold_left vty_of_term Svty.empty l in
+         (* TODO: we can replace `Var.Set.subset bv s1`
+            by `Var.Seq.equal bv s1`. By construction `s1` is
+            a subset of `bv`. *)
          Var.Set.subset bv s1 && Svty.subset vty s2 )
       trs
 
@@ -2392,7 +2411,9 @@ module Triggers = struct
         Var.Map.fold (fun v _ s -> Var.Set.add v s) binders Var.Set.empty
       in
       match decl_kind, f with
-      | Dtheory, _ -> assert false
+      | Dtheory, _ ->
+        (* TODO: Add Dobjective here. We never generate triggers for them. *)
+        assert false
       | (Dpredicate e | Dfunction e), _ ->
         let defn = match f with
           | { f = (Sy.Form Sy.F_Iff | Sy.Lit Sy.L_eq) ; xs = [e1; e2]; _ } ->

src/lib/structures/expr.mli

@@ -48,8 +48,13 @@ type term_view = private {
   ty: Ty.t;
   bind : bind_kind;
   tag: int;
-  vars : (Ty.t * int) Var.Map.t; (* vars to types and nb of occurences *)
+  vars : (Ty.t * int) Var.Map.t;
+  (** Map of free term variables in the term to their type and
+      number of occurrences. *)
+
   vty : Ty.Svty.t;
+  (** Map of free type variables in the term. *)
+
   depth: int;
   nb_nodes : int;
   pure : bool;
@@ -64,16 +69,49 @@ and bind_kind =
 
 and quantified = private {
   name : string;
+  (** Name of the lemma. This field is used by printers. *)
+
   main : t;
+  (** The underlying formula. *)
+
   toplevel : bool;
+  (** Determine if the quantified formula is at the top level.
+      This flag is important for the prenex polymorphism.
+      - If this flag is [true], all the free type variables of [main]
+        are implicitely considered as quantified.
+      - Otherwise, the free type variables of the lemma are the
+        same as the underlying formula [main] and are stored in the field
+        [sko_vty]. *)
+
   user_trs : trigger list;
+  (** List of the triggers defined by the user.
+
+      The solver doesn't generate multi-triggers if the user has defined
+      some multi-triggers. *)
+
   binders : binders;
-  (* These fields should be (ordered) lists ! important for skolemization *)
+  (** The ordered list of quantified term variables of [main].
+
+      This list has to be ordered for the skolemization. *)
+
   sko_v : t list;
+  (** Set of all the free variables of the quantified formula. In other words,
+      this set is always the complementary of [binders] in the set of
+      free variables of [main].
+
+      The purpose of this field is to retrieve these variables quickly while
+      performing the lazy skolemization in the SAT solver (see [skolemize]). *)
+
   sko_vty : Ty.t list;
-  loc : Loc.t; (* location of the "GLOBAL" axiom containing this quantified
-                  formula. It forms with name a unique id *)
+  (** The set of free type variables. In particular this set is always
+      empty if we are the top level. *)
+
+  loc : Loc.t;
+  (** Location of the "GLOBAL" axiom containing this quantified formula. It
+      forms with name a unique identifier. *)
+
   kind : decl_kind;
+  (** Kind of declaration. *)
 }
 
 and letin = private {
@@ -271,10 +309,30 @@ val max_ground_terms_rec_of_form : t -> Set.t
 
 val make_triggers:
   t -> binders -> decl_kind -> Util.matching_env -> trigger list
+(** [make_triggers f binders decl menv] generate multi-triggers for the
+    formula [f] and binders [binders].
+
+    For axioms, we try to produce multi-triggers in the following order
+    (if we succeed to produce at least one multi-trigger, we don't try other
+    strategies):
+    1. In greedy mode:
+    - Mono-triggers without variables;
+    - Mono-triggers with variables;
+    - Multi-triggers without variables;
+    - Multi-triggers with variables.
+      2. Otherwise:
+    - Mono and multi-triggers without variables;
+    - Mono and multi-triggers with variables.
+
+    Mono-trigger with `Sy.Plus` or `Sy.Minus` top symbols are ignored
+    if other mono-triggers have been generated.
+
+    The matching environment [env] is used to limit the number of
+    multi-triggers generated per axiom. *)
 
+val clean_trigger: in_theory:bool -> string -> trigger -> trigger
 (** clean trigger:
     remove useless terms in multi-triggers after inlining of lets*)
-val clean_trigger: in_theory:bool -> string -> trigger -> trigger
 
 val resolution_triggers: is_back:bool -> quantified -> trigger list