Refactor Inductive to use subclass instead of monkey-patching

[Copilot]

Replaces monkey-patched method reassignment in Inductive and InductiveRel with proper subclassing of z3.Datatype.

Changes

src/kdrag/kernel.py

• Add _InductiveDatatype class extending z3.Datatype
• Override create() method to handle validation and registration
• Store unique name in instance variable instead of closure

src/kdrag/datatype.py

• Add _InductiveRelDatatype class extending _InductiveDatatype
• Override declare() and create() methods
• Replace closure variables (preds, relname, params) with instance variables (_preds, _relname, _params)

Before/After

Before:

def Inductive(name: str) -> smt.Datatype:
    dt = smt.Datatype(name)
    oldcreate = dt.create
    
    def create():
        dt = oldcreate()
        # custom logic...
        return dt
    
    dt.create = create  # monkey-patch
    return dt

After:

class _InductiveDatatype(smt.Datatype):
    def create(self):
        dt = super().create()
        # custom logic...
        return dt

def Inductive(name: str) -> _InductiveDatatype:
    return _InductiveDatatype(name)

All existing code remains compatible.

Original prompt

---

This section details on the original issue you should resolve

<issue_title>Refactor inductive</issue_title>
<issue_description>Refactor inductive to instead be defined using a subclass of z3's datatype constructor class instead of goofy monkey patched lambdas</issue_description>

Comments on the Issue (you are @copilot in this section)

• Fixes Refactor inductive #16

---

💡 You can make Copilot smarter by setting up custom instructions, customizing its development environment and configuring Model Context Protocol (MCP) servers. Learn more Copilot coding agent tips in the docs.