From 8661027426bedf1698c72a5c83f2923f3e75d323 Mon Sep 17 00:00:00 2001 From: Pierrot Date: Fri, 10 May 2024 19:13:44 +0200 Subject: [PATCH] Documentation of quantified type in `Expr` (#1106) * Documentation of quantified type in `Expr` While fixing the issue #1099, I wrote a bit of documentation for `Expr`. * Review changes * Clarify CNF form of implications --- src/lib/structures/expr.ml | 37 +++++++++++++++----- src/lib/structures/expr.mli | 68 ++++++++++++++++++++++++++++++++++--- 2 files changed, 92 insertions(+), 13 deletions(-) diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml index 463ffa74e..0516955b4 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 *) + 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,6 +2050,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 -> @@ -2046,12 +2058,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 @@ -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]; _ } -> diff --git a/src/lib/structures/expr.mli b/src/lib/structures/expr.mli index 3a9c6681a..b3a112797 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 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