kdrag.solvers.synth.cegis_simple

kdrag.solvers.synth.cegis_simple(spec: ExprRef) → list[ExprRef] | None

Given formula of the form exists ys, forall xs, P(xs,ys), attempt to find witness for ys.

>>> x = smt.Const("x", smt.IntSort())
>>> y = smt.Const("y", smt.IntSort())
>>> assert cegis_simple(smt.Exists([y], smt.ForAll([x], x + y > x)))[0].as_long() > 0
>>> z = smt.Const("z", smt.IntSort())
>>> assert cegis_simple(smt.Exists([y], smt.ForAll([x], smt.And(y <= 0, x + y > x)))) is None

Parameters:

spec (ExprRef)

Return type:

list[ExprRef] | None