kdrag.kernel.declare

kdrag.kernel.declare(name: str, *sorts: SortRef) → FuncDeclRef

Reserve a name. This helps avoid accidental clashing of axioms over the same symbol. It also make serialization possible and easier.

>>> declare("reserved_example", smt.IntSort())
reserved_example
>>> declare("reserved_example", smt.IntSort())
Traceback (most recent call last):
    ...
ValueError: ('Declaration name already reserved: reserved_example', 'with sorts', [], Int)

Parameters:

name (str)
sorts (SortRef)

Return type:

FuncDeclRef