From b540e9d2bf201a2c1d6cef93ea41368e36153b6e Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Wed, 10 Jun 2026 11:59:42 +0200 Subject: [PATCH] =?UTF-8?q?smt:=20add=20`[smt=5Finline]`=20operator=20tag?= =?UTF-8?q?=20to=20=CE=B4/=CE=B2-reduce=20at=20use=20sites?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Higher-order combinators whose body builds a lambda from their own parameters (e.g. `right_loop inv o = forall y, cancel (fun x => o x y) ...`) are translated once, polymorphically, into a why3 predicate. The inner lambdas become polymorphic `unamed_lambda` symbols, forcing why3's polymorphism encoding (the `uni`/`sort`/`t2tb` bridges). Discharging a fully-ground goal like `right_loop idfun (^)` then requires the prover to chain several trigger-less higher-order `@`-apply axioms across that encoding before it can even case-split — which older SMT solvers fail to do within the time limit, even though the goal is trivial. Add a per-operator `[smt_inline]` tag (mirroring `[smt_opaque]`): a fully-applied tagged operator/predicate is δ/β-reduced into the goal before translation, so its lambdas are created at the call's concrete instantiation and stay monomorphic — no `uni`/`t2tb` detour. Unmarked definitions are translated exactly as before. The tag is threaded through the parser, parsetree (`pp_tags`), scope, and `op_opaque.inline`, and consulted by `EcSmt.try_inline`. Tag the eight `*_loop*` combinators in Logic.ec. --- src/ecDecl.ml | 4 ++-- src/ecDecl.mli | 2 +- src/ecHiPredicates.ml | 9 ++++++++- src/ecParser.mly | 10 +++++++--- src/ecParsetree.ml | 1 + src/ecScope.ml | 5 +++-- src/ecSmt.ml | 27 +++++++++++++++++++++++++++ theories/prelude/Logic.ec | 16 ++++++++-------- 8 files changed, 57 insertions(+), 17 deletions(-) diff --git a/src/ecDecl.ml b/src/ecDecl.ml index 70f3ec7e0b..3eb798d0d7 100644 --- a/src/ecDecl.ml +++ b/src/ecDecl.ml @@ -144,7 +144,7 @@ type operator = { op_unfold : int option; } -and opopaque = { smt: bool; reduction: bool; } +and opopaque = { smt: bool; reduction: bool; inline: bool; } (* -------------------------------------------------------------------- *) type axiom_kind = [`Axiom of (Ssym.t * bool) | `Lemma] @@ -229,7 +229,7 @@ let mk_pred ?clinline ?unfold ~opaque tparams dom body lc = gen_op ?clinline ?unfold ~opaque tparams ty kind lc let optransparent : opopaque = - { smt = false; reduction = false; } + { smt = false; reduction = false; inline = false; } let mk_op ?clinline ?unfold ~opaque tparams ty body lc = let kind = OB_oper body in diff --git a/src/ecDecl.mli b/src/ecDecl.mli index f67d497e7d..c523f1c2f5 100644 --- a/src/ecDecl.mli +++ b/src/ecDecl.mli @@ -128,7 +128,7 @@ type operator = { op_unfold : int option; } -and opopaque = { smt: bool; reduction: bool; } +and opopaque = { smt: bool; reduction: bool; inline: bool; } val op_ty : operator -> ty val is_pred : operator -> bool diff --git a/src/ecHiPredicates.ml b/src/ecHiPredicates.ml index 49e725ad58..dcf3440a89 100644 --- a/src/ecHiPredicates.ml +++ b/src/ecHiPredicates.ml @@ -83,7 +83,14 @@ let trans_preddecl_r (env : EcEnv.env) (pr : ppredicate located) = let dom = Tuni.subst_dom uidmap dom in - EcDecl.mk_pred ~opaque:optransparent tparams dom body pr.pp_locality + let tags = Ssym.of_list (List.map unloc pr.pp_tags) in + let opaque = { + EcDecl.smt = Ssym.mem "smt_opaque" tags; + EcDecl.reduction = Ssym.mem "opaque" tags; + EcDecl.inline = Ssym.mem "smt_inline" tags; + } in + + EcDecl.mk_pred ~opaque tparams dom body pr.pp_locality (* -------------------------------------------------------------------- *) let trans_preddecl (env : EcEnv.env) (pr : ppredicate located) = diff --git a/src/ecParser.mly b/src/ecParser.mly index 95d9999e64..d5c5201bd6 100644 --- a/src/ecParser.mly +++ b/src/ecParser.mly @@ -1867,22 +1867,25 @@ exception_: (* -------------------------------------------------------------------- *) (* Predicate definitions *) predicate: -| locality=locality PRED x=oident +| locality=locality PRED tags=bracket(ident*)? x=oident { { pp_name = x; pp_tyvars = None; pp_def = PPabstr []; + pp_tags = odfl [] tags; pp_locality = locality; } } -| locality=locality PRED x=oident tyvars=tyvars_decl? COLON sty=pred_tydom +| locality=locality PRED tags=bracket(ident*)? x=oident tyvars=tyvars_decl? COLON sty=pred_tydom { { pp_name = x; pp_tyvars = tyvars; pp_def = PPabstr sty; + pp_tags = odfl [] tags; pp_locality = locality; } } -| locality=locality PRED x=oident tyvars=tyvars_decl? p=ptybindings? EQ f=form +| locality=locality PRED tags=bracket(ident*)? x=oident tyvars=tyvars_decl? p=ptybindings? EQ f=form { { pp_name = x; pp_tyvars = tyvars; pp_def = PPconcr (odfl [] p, f); + pp_tags = odfl [] tags; pp_locality = locality; } } | locality=locality INDUCTIVE x=oident tyvars=tyvars_decl? p=ptybindings? @@ -1891,6 +1894,7 @@ predicate: { { pp_name = x; pp_tyvars = tyvars; pp_def = PPind (odfl [] p, b); + pp_tags = []; pp_locality = locality; } } indpred_def: diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml index e9deac3f92..5b74c02c60 100644 --- a/src/ecParsetree.ml +++ b/src/ecParsetree.ml @@ -508,6 +508,7 @@ type ppredicate = { pp_name : psymbol; pp_tyvars : psymbol list option; pp_def : ppred_def; + pp_tags : psymbol list; pp_locality : locality; } diff --git a/src/ecScope.ml b/src/ecScope.ml index c6f1ff7fdb..63b1b16eec 100644 --- a/src/ecScope.ml +++ b/src/ecScope.ml @@ -1349,7 +1349,8 @@ module Op = struct let tags = Sstr.of_list (List.map unloc op.po_tags) in let opaque = { smt = Sstr.mem "smt_opaque" tags; - reduction = Sstr.mem "opaque" tags + reduction = Sstr.mem "opaque" tags; + inline = Sstr.mem "smt_inline" tags; } in let unfold = match op.po_args with @@ -1383,7 +1384,7 @@ module Op = struct let axop = let nargs = List.sum (List.map (List.length -| fst) args) in EcDecl.axiomatized_op ~nargs path (tyop.op_tparams, bd) lc in - let tyop = { tyop with op_opaque = { reduction = true; smt = false; }} in + let tyop = { tyop with op_opaque = { reduction = true; smt = false; inline = false; }} in let scope = bind scope (unloc op.po_name, tyop) in Ax.bind scope (unloc ax, axop) diff --git a/src/ecSmt.ml b/src/ecSmt.ml index 2e523e770c..f4a167b172 100644 --- a/src/ecSmt.ml +++ b/src/ecSmt.ml @@ -654,9 +654,36 @@ and trans_kpatterns env (ks : (kpattern * w3_known_op) list) (f : form) = ks) (* -------------------------------------------------------------------- *) +(* Operators tagged `[smt_inline]` are δ/β-reduced at their use sites instead + of being emitted as a symbol plus a defining axiom. This keeps lambdas + occurring in their bodies monomorphic at the call's instantiation, which + avoids the polymorphic higher-order encoding (uni/t2tb bridges) that + weaker SMT solvers fail to navigate. *) +and try_inline ((genv, _) : tenv * lenv) (fp : form) = + let hd, args = + match fp.f_node with + | Fapp (hd, args) -> (hd, args) + | _ -> (fp, []) in + match hd.f_node with + | Fop (p, tys) -> begin + match Op.by_path_opt p genv.te_env with + | Some op when op.op_opaque.inline -> begin + match op.op_kind with + | OB_oper (Some (OP_Plain _)) | OB_pred (Some (PR_Plain _)) -> + Some (f_app_simpl (Op.reduce ~mode:`Force genv.te_env p tys) args fp.f_ty) + | _ -> None + end + | _ -> None + end + | _ -> None + and trans_form ((genv, lenv) as env : tenv * lenv) (fp : form) = try trans_kpatterns env genv.tk_known_w3 fp with CanNotTranslate -> + match try_inline env fp with + | Some fp -> trans_form env fp + | None -> + match fp.f_node with | Fquant (qt, bds, body) -> begin diff --git a/theories/prelude/Logic.ec b/theories/prelude/Logic.ec index c4b133b7ff..2187bc3915 100644 --- a/theories/prelude/Logic.ec +++ b/theories/prelude/Logic.ec @@ -181,28 +181,28 @@ pred right_commutative (o:'a -> 'b -> 'a) = pred left_distributive (o1:'a -> 'b -> 'a) (o2:'a -> 'a -> 'a) = forall x y z, o1 (o2 x y) z = o2 (o1 x z) (o1 y z). -pred right_loop (inv : 'b -> 'b) (o:'a -> 'b -> 'a) = +pred [smt_inline] right_loop (inv : 'b -> 'b) (o:'a -> 'b -> 'a) = forall y, cancel (fun x, o x y) (fun x, o x (inv y)). -pred rev_right_loop inv (o:'a -> 'b -> 'a) = +pred [smt_inline] rev_right_loop inv (o:'a -> 'b -> 'a) = forall y, cancel (fun x, o x (inv y)) (fun x, o x y). -pred left_loop inv (o:'a -> 'b -> 'b) = +pred [smt_inline] left_loop inv (o:'a -> 'b -> 'b) = forall x, cancel (o x) (o (inv x)). -pred rev_left_loop inv (o:'a -> 'b -> 'b) = +pred [smt_inline] rev_left_loop inv (o:'a -> 'b -> 'b) = forall x, cancel (o (inv x)) (o x). -pred right_loop_in p (inv : 'b -> 'b) (o:'a -> 'b -> 'a) = +pred [smt_inline] right_loop_in p (inv : 'b -> 'b) (o:'a -> 'b -> 'a) = forall y, p y => cancel (fun x, o x y) (fun x, o x (inv y)). -pred rev_right_loop_in p inv (o:'a -> 'b -> 'a) = +pred [smt_inline] rev_right_loop_in p inv (o:'a -> 'b -> 'a) = forall y, p y => cancel (fun x, o x (inv y)) (fun x, o x y). -pred left_loop_in p inv (o:'a -> 'b -> 'b) = +pred [smt_inline] left_loop_in p inv (o:'a -> 'b -> 'b) = forall x, p x => cancel (o x) (o (inv x)). -pred rev_left_loop_in p inv (o:'a -> 'b -> 'b) = +pred [smt_inline] rev_left_loop_in p inv (o:'a -> 'b -> 'b) = forall x, p x => cancel (o (inv x)) (o x). pred left_id e (o:'a -> 'b -> 'b) =