PatternRestriction

Symbolica documentation for getting started, symbolic expressions, numerical evaluation, pattern matching, and APIs in Python and Rust.

PatternRestriction

class PatternRestriction

A 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) -> PatternRestriction

Create 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__() -> PatternRestriction

Create a new pattern restriction that takes the logical ‘not’ of the current restriction.

__or__

PatternRestriction.__or__(other: PatternRestriction) -> PatternRestriction

Create 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]) -> PatternRestriction

Create 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