kdrag.theories.set.Closed

kdrag.theories.set.Closed(S: ArrayRef, f: FuncDeclRef) → BoolRef

A set S is closed under function f if for all x1,…,xn in S, f(x1,…,xn) is also in S. >>> x = smt.Int(“x”) >>> kd.prove(Closed(smt.Lambda([x], x >= 0), (x + x).decl())) |= ForAll([x0!…, x1!…],

Implies(And(x0!… >= 0, x1!… >= 0), x0!… + x1!… >= 0))

Parameters:

• S (ArrayRef)

• f (FuncDeclRef)

Return type:

BoolRef