kdrag.utils.pmatch_fo

kdrag.utils.pmatch_fo(vs: list[ExprRef], pat: ExprRef, t: ExprRef, subst=None) → dict[ExprRef, ExprRef] | None

First order pattern matching. Faster and simpler. Pattern match t against pat considering vs as variables. Returns substitution dictionary if succeeds

>>> x, y = smt.Ints("x y")
>>> pmatch_fo([x], x + x, y + y)
{x: y}

Parameters:

• vs (list[ExprRef])

• pat (ExprRef)

• t (ExprRef)

Return type:

dict[ExprRef, ExprRef] | None