From 51c6209ad027d30673b133f836ba3487247863cc Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Tue, 30 Apr 2024 03:28:09 +0200 Subject: [PATCH] Documentation of quantified type in `Expr` While fixing the issue #1099, I wrote a bit of documentation for `Expr`. --- src/lib/structures/expr.ml | 40 ++++++++++++++++++---- src/lib/structures/expr.mli | 68 ++++++++++++++++++++++++++++++++++--- 2 files changed, 96 insertions(+), 12 deletions(-) diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml index ca04c910b8..d6e7ac700e 100644 --- a/src/lib/structures/expr.ml +++ b/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 *) + loc : Loc.t; kind : decl_kind; } @@ -1438,10 +1436,27 @@ and mk_forall_bis (q : quantified) = let q = {q with binders; user_trs = trs; sko_v; main = f } in mk_forall_bis q +(* Look for a substitution [sbt] of term variables such that: + - the domain of [sbt] is a subset of [binders]; + - the application of [sbt] on the formula [f] produces a formula [g] + such that: + -- the set of free term variables of [g] in [binders] is strictly smaller; + -- the universal closures of [f] and [g] are equivalent. + + For instance, let's [f] be the formula: + x <> 1 or f(y) = x + 1 + and the set of binders is `{ x, y }`. This function will produce the + substitution `{ x |-> 1 }`. Indeed, the ground formulas + forall x, y : int. x <> 1 or f(y) < x + 1 + and + forall y : int. 1 <> 1 or f(y) < 1 + 1 + are equivalent. + + *Note*: this heuristic is disabled if the user has defined filters. + + @return [None] if the heuristic failed to produce such a substitution. *) 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 _ -> () @@ -1464,6 +1479,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 @@ -2000,6 +2016,7 @@ 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 -> @@ -2007,12 +2024,19 @@ module Triggers = struct ) 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 @@ -2360,7 +2384,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]; _ } -> @@ -2584,7 +2610,7 @@ module Purification = struct mk_term (Sy.Var fresh_var) [] t.ty , add_let fresh_var t lets | _ -> (* detect ITEs *) - match t.xs with + match tm.xs with | [_;_;_] when is_ite t.f -> let fresh_var = Sy.fresh_skolem_var "Pur-Ite" in mk_term (Sy.Var fresh_var) [] t.ty , add_let fresh_var t lets diff --git a/src/lib/structures/expr.mli b/src/lib/structures/expr.mli index 5a7526ca17..ec5924494b 100644 --- a/src/lib/structures/expr.mli +++ b/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 its type and + number of occurences. *) + 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 free term variables of [main]. + + This field 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 { @@ -268,10 +306,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