kdrag.smt.register_well_formed

kdrag.smt.register_well_formed(sort: SortRef, predicate: Callable[[ExprRef], BoolRef])

Register a well-formedness predicate for a sort.

>>> register_well_formed(IntSort(), lambda x: x >= 0)
>>> Const("x", IntSort()).assumes
x >= 0
>>> del well_formed[IntSort()]

Parameters: