kdrag.utils.search_expr
- kdrag.utils.search_expr(e: ExprRef, pfs: dict[object, Proof]) dict[tuple[str, Proof], Any]
Search for expressions in the proof database that match e using pattern matching.
>>> x,z = smt.Ints("x z") >>> search_expr(z + 0, { "thm1": kd.prove(smt.ForAll([x], x + 0 == x)), "thm2" : kd.prove(z + 0 == z), "thm3" : kd.prove(smt.ForAll([x], x + 1 == 1 + x)), "thm4" : kd.prove(smt.BoolVal(True))}) {('thm1', |- ForAll(x, x + 0 == x)): [z], ('thm2', |- z + 0 == z): []}