Fixedpoint (Datalog) solver backed by Lean's ``grind`` tactic. Encodes facts as hypotheses and rules as universally-quantified implications, then proves the query via the kernel's tactic engine.
| 863 | |
| 864 | |
| 865 | class Fixedpoint: |
| 866 | """Fixedpoint (Datalog) solver backed by Lean's ``grind`` tactic. |
| 867 | |
| 868 | Encodes facts as hypotheses and rules as universally-quantified |
| 869 | implications, then proves the query via the kernel's tactic engine. |
| 870 | """ |
| 871 | |
| 872 | def __init__(self, ctx: Any = None) -> None: |
| 873 | self._decls: list[FuncDeclRef] = [] |
| 874 | self._declared_vars: list[ExprRef] = [] |
| 875 | self._premises: list[BoolRef] = [] |
| 876 | self._rules: list[BoolRef] = [] |
| 877 | self._last_result: CheckSatResult = unknown |
| 878 | |
| 879 | # -- declarations -------------------------------------------------------- |
| 880 | |
| 881 | def register_relation(self, *decls: Any) -> None: |
| 882 | for d in decls: |
| 883 | if isinstance(d, FuncDeclRef): |
| 884 | self._decls.append(d) |
| 885 | |
| 886 | def declare_var(self, *args: Any) -> None: |
| 887 | for v in args: |
| 888 | if isinstance(v, ExprRef): |
| 889 | self._declared_vars.append(v) |
| 890 | |
| 891 | def set(self, *args: Any, **kws: Any) -> None: |
| 892 | pass |
| 893 | |
| 894 | # -- helpers ------------------------------------------------------------- |
| 895 | |
| 896 | def _abstract(self, expr: BoolRef) -> BoolRef: |
| 897 | """Wrap *expr* in ForAll over declared vars that appear in it.""" |
| 898 | var_names = {name for name, _ in expr._vars} |
| 899 | used = [ |
| 900 | v for v in self._declared_vars if isinstance(v._ast, Var) and v._ast.name in var_names |
| 901 | ] |
| 902 | if used: |
| 903 | return ForAll(used, expr) |
| 904 | return expr |
| 905 | |
| 906 | # -- add_rule / fact / rule ---------------------------------------------- |
| 907 | |
| 908 | def add_rule(self, head: Any, body: Any = None, name: str | None = None) -> None: |
| 909 | if body is not None and not isinstance(body, str): |
| 910 | # Explicit head/body split: head :- body |
| 911 | if not isinstance(body, (list, tuple)): |
| 912 | body = [body] |
| 913 | if len(body) == 1: |
| 914 | rule: BoolRef = Implies(body[0], head) |
| 915 | else: |
| 916 | rule = Implies(And(*body), head) |
| 917 | rule = self._abstract(rule) |
| 918 | self._premises.append(rule) |
| 919 | self._rules.append(rule) |
| 920 | return |
| 921 | |
| 922 | # body is None (or a name string) -- head is the full formula |
no outgoing calls