PatternRestriction
Symbolica documentation for getting started, symbolic expressions, numerical evaluation, pattern matching, and APIs in Python and Rust.
PatternRestriction
class PatternRestrictionA restriction on wildcards.
Methods
| Name | Description |
|---|---|
__and__ |
Create a new pattern restriction that is the logical and operation between two restrictions (i.e., both should hold). |
__invert__ |
Create a new pattern restriction that takes the logical ‘not’ of the current restriction. |
__or__ |
Create a new pattern restriction that is the logical ‘or’ operation between two restrictions (i.e., one of the two should hold). |
req_matches |
Create a restriction from a callback receiving the currently matched wildcards |
__and__
PatternRestriction.__and__(other: PatternRestriction) -> PatternRestrictionCreate a new pattern restriction that is the logical and operation between two restrictions (i.e., both should hold).
Parameters
other(PatternRestriction) The other operand to combine or compare with.
__invert__
PatternRestriction.__invert__() -> PatternRestrictionCreate a new pattern restriction that takes the logical ‘not’ of the current restriction.
__or__
PatternRestriction.__or__(other: PatternRestriction) -> PatternRestrictionCreate a new pattern restriction that is the logical ‘or’ operation between two restrictions (i.e., one of the two should hold).
Parameters
other(PatternRestriction) The other operand to combine or compare with.
req_matches
PatternRestriction.req_matches(match_fn: Callable[[dict[Expression, Expression]], bool | None | Condition]) -> PatternRestrictionCreate a restriction from a callback receiving the currently matched wildcards. Return True to accept, False to reject, or None when undecidable. The dictionary may be incomplete: return None until the required wildcards are present. A completed match is accepted only when the restriction is true. A returned Condition is evaluated using the same three-valued contract.
Examples
from symbolica import *
f, x_, y_, z_ = S('f', 'x_', 'y_', 'z_')
def ordered(m: dict[Expression, Expression]) -> bool | None:
if x_ not in m or y_ not in m:
return None
if m[x_] <= m[y_] is False:
return False
if z_ not in m:
return None
return (m[x_] <= m[y_]) & (m[y_] <= m[z_])
e = f(1, 2, 3).replace(f(x_, y_, z_), 1,
PatternRestriction.req_matches(ordered))
assert e == 1