kdrag.utils.pmatch_rec_ctx

kdrag.utils.pmatch_rec_ctx(vs: list[ExprRef], pat: ExprRef, t: ExprRef) → tuple[ExprCtx, ExprRef, dict[ExprRef, ExprRef]] | None

Pattern match pat against subterms of t, returning the context, matched term, and substitution if successful. >>> x,y,z,a,b = smt.Ints(“x y z a b”) >>> kd.utils.pmatch_rec_ctx([a,b], a*b, smt.Lambda([x], x * y)) ([LambdaHole(vs=[X!…], orig_vs=[x])], X!…*y, {b: y, a: X!…})

Parameters: