kdrag.datatype.pattern_match

kdrag.datatype.pattern_match(x: DatatypeRef, pat: DatatypeRef) → tuple[list[BoolRef], dict[DatatypeRef, DatatypeRef]]

A Symbolic execution of sorts of pattern matching. Returns the constraints and substitutions for variables

>>> import kdrag.theories.nat as nat
>>> n,m = smt.Consts("n m", nat.Nat)
>>> pattern_match(n, nat.S(nat.S(m)))
([is(S, n), is(S, pred(n))], {m: pred(pred(n))})

Parameters:

• x (DatatypeRef)

• pat (DatatypeRef)

Return type:

tuple[list[BoolRef], dict[DatatypeRef, DatatypeRef]]