kdrag.kernel.define_simple

kdrag.kernel.define_simple(name: str, args: list[ExprRef], body: ExprRef) → FuncDeclRef

A simple non recursive definition is a conservative extension https://en.wikipedia.org/wiki/Conservative_extension

>>> x = smt.Int("x")
>>> define_simple("mysucc9034", [x], x + 1)
mysucc9034
>>> f = smt.Function("f102", smt.IntSort(), smt.IntSort())
>>> define_simple("f102", [x], f(x))
Traceback (most recent call last):
    ...
ValueError: ('Symbol appears in it's own definition. This is not a simple definition and requires further checks for consistency', f102, f102(x))

Parameters:

• name (str)

• args (list[ExprRef])

• body (ExprRef)

Return type:

FuncDeclRef