kdrag.utils.antipattern

kdrag.utils.antipattern(xs: list[ExprRef]) → tuple[list[ExprRef], ExprRef]

Anti pattern matching. Given a list of concrete examples, return the most specific pattern that matches them all. Returns tuple of list of pattern variables and pattern expression.

https://arxiv.org/pdf/2302.00277 Anti-unification and Generalization: A Survey https://arxiv.org/abs/2212.04596 babble: Learning Better Abstractions with E-Graphs and Anti-Unification https://ericlippert.com/2018/10/29/anti-unification-part-1/

>>> a,b,c,d = smt.Ints("a b c d")
>>> f = smt.Function("f", smt.IntSort(), smt.IntSort(), smt.IntSort())
>>> g = smt.Function("g", smt.IntSort(), smt.IntSort(), smt.IntSort())
>>> t1 = f(a,g(a,b))
>>> t2 = f(c,g(c,d))
>>> t3 = f(a,g(d,b))
>>> antipattern([t1,t2])
([a!..., b!...], f(a!..., g(a!..., b!...)))
>>> antipattern([t1,t2,t3])
([a!..., a!..., b!...], f(a!..., g(a!..., b!...)))

Parameters:

xs (list[ExprRef])

Return type:

tuple[list[ExprRef], ExprRef]