kdrag.rewrite.esimp

kdrag.rewrite.esimp(vs: list[ExprRef], goal: BoolRef, max_iters=7, timeout=50)

Simplify and unfold goal while seeking a ground model for vs that is provably a solution. This can be used in a minikanren-lite way or to produce counterexamples. Does not produce generalized solutions like a prolog would.

>>> n,x,y = smt.Ints("n x y")
>>> fact = smt.Function("fact", smt.IntSort(), smt.IntSort())
>>> fact = kd.define("fact", [n], smt.If(n <= 0, 1, n * fact(n - 1)))
>>> esimp([x], fact(x) == 6)
{x: 3}

Parameters:

vs (list[ExprRef])
goal (BoolRef)