MCPcopy Create free account
hub / github.com/BasisResearch/lean.py / add_rule

Method add_rule

lean_py/z3/solver.py:908–925  ·  view source on GitHub ↗
(self, head: Any, body: Any = None, name: str | None = None)

Source from the content-addressed store, hash-verified

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
923 if isinstance(head, BoolRef):
924 self._premises.append(self._abstract(head))
925 self._rules.append(head)
926
927 def rule(self, head: Any, body: Any = None, name: str | None = None) -> None:
928 self.add_rule(head, body, name)

Callers 3

ruleMethod · 0.95
factMethod · 0.95
test_add_ruleMethod · 0.95

Calls 3

_abstractMethod · 0.95
ImpliesFunction · 0.90
AndFunction · 0.90

Tested by 1

test_add_ruleMethod · 0.76