pyfcstm.bmc.ast

Typed expression data model for FCSTM BMC queries.

This module defines the parser-independent expression objects used by *.fbmcq queries. The core expression nodes intentionally mirror the current FCSTM numeric and condition expression split, while BMC-only nodes add frame, cycle, active-state, event, case, and abstract-call atoms. The objects are frozen dataclasses and expose BmcExpr.to_canonical() so later parser parity tests can compare FCSTM and FBMCQ expressions through a stable, language-neutral shape.

Design contracts:

Expression nodes are data-only; they do not bind names, inspect models, or lower anything to Z3.
str() on every concrete expression returns canonical .fbmcq DSL text. This is the object-to-text half of the query round-trip contract.
repr() stays the dataclass-generated debugging representation and must not be rewritten into DSL text.
Numeric and condition expression categories stay separate at construction time, matching FCSTM num_expression and cond_expression.
FCSTM-compatible expression checks intentionally use normal Python ValueError / TypeError failures for malformed literals, operators, and operand categories. Query-facing BMC atom fields such as quoted paths, frames, selectors, and atom spellings raise pyfcstm.bmc.errors.InvalidBmcQuery, matching the top-level query wrappers in pyfcstm.bmc.query. Parser and binder code should not assume one exception family covers both layers.
Literal canonical values are kept JSON-portable. Float literals that would overflow Python’s finite float range are rejected at construction time. Finite Python floats, including subnormal values and underflow-to-zero raw spellings, are accepted because they match the current FCSTM literal conversion boundary; raw text still preserves exact spelling for parity checks and later encoding layers may impose stricter numeric policies.
Identifier and path shape validation is shallow here: quoted query atoms only require non-empty strings, and later binder layers resolve model paths and reject impossible state, event, variable, case, or call names.
The event atom always prints its cycle selector explicitly, including current. This keeps event queries visually distinct from frame-based atoms such as active("Root.A") whose default frame may be omitted.

The module contains:

BmcNumExpr and BmcCondExpr - Typed numeric and condition expression bases.
FCSTM-compatible nodes such as IntLiteral, NameRef, NumBinaryOp, NumericComparison, and CondBinaryOp.
BMC-only extension nodes such as FrameVar, Cycle, Active, Event, Case, CallCount, and Called.

Example:

>>> from pyfcstm.bmc.ast import Active, IntLiteral, NameRef, NumericComparison
>>> expr = NumericComparison(NameRef("x"), "<=", IntLiteral("3"))
>>> expr.to_canonical()["op"]
'<='
>>> isinstance(Active("Root.Idle"), BmcCondExpr)
True

all

pyfcstm.bmc.ast.__all__ = ['BmcExpr', 'BmcNumExpr', 'BmcCondExpr', 'IntLiteral', 'FloatLiteral', 'BoolLiteral', 'NameRef', 'MathConst', 'NumUnaryOp', 'NumBinaryOp', 'NumConditionalOp', 'UFuncCall', 'CondUnaryOp', 'NumericComparison', 'CondBinaryOp', 'CondConditionalOp', 'FrameVar', 'Cycle', 'CallStepPoint', 'CallStepSelector', 'CallFilter', 'CallCount', 'Active', 'Terminated', 'Event', 'Case', 'Called']

Built-in mutable sequence.

If no argument is given, the constructor creates a new empty list. The argument must be an iterable if specified.

BmcExpr

class pyfcstm.bmc.ast.BmcExpr[source]

Base class for every BMC query expression node.

Concrete subclasses provide a stable canonical form for tests, parser handoff, and later binder diagnostics. The canonical form contains only plain dictionaries, lists, strings, booleans, integers, floats, and None so it can be serialized or compared without importing grammar classes.

Variables:: _node_name – Canonical node tag emitted by BmcExpr.to_canonical().

Example:

>>> from pyfcstm.bmc.ast import IntLiteral
>>> IntLiteral("7").to_canonical()["node"]
'int_literal'

__str__() → str[source]

Return the canonical .fbmcq DSL spelling for this expression.

Returns:: Query DSL text that can be parsed back into the same canonical semantic expression shape. Operator aliases and literal spelling such as boolean casing may be normalized by this canonical text.
Return type:: str

Example:

>>> from pyfcstm.bmc.ast import IntLiteral
>>> str(IntLiteral("7"))
'7'

to_canonical() → Dict[str, Any][source]

Return a language-neutral canonical expression shape.

Returns:: Canonical dictionary for this node.
Return type:: Dict[str, object]

Example:

>>> from pyfcstm.bmc.ast import BoolLiteral
>>> BoolLiteral("true").to_canonical()["value"]
True

BmcNumExpr

class pyfcstm.bmc.ast.BmcNumExpr[source]

Base class for numeric BMC expressions.

Numeric expressions follow FCSTM num_expression shape and represent integer, float, variable, frame-variable, cycle, and arithmetic operator values.

Example:

>>> from pyfcstm.bmc.ast import BmcNumExpr, Cycle
>>> isinstance(Cycle(), BmcNumExpr)
True

BmcCondExpr

class pyfcstm.bmc.ast.BmcCondExpr[source]

Base class for condition BMC expressions.

Condition expressions follow FCSTM cond_expression shape and represent boolean literals, comparisons, logical operators, active-state atoms, event atoms, selected-case atoms, and abstract-call atoms.

Example:

>>> from pyfcstm.bmc.ast import Active, BmcCondExpr
>>> isinstance(Active("Root.A"), BmcCondExpr)
True

IntLiteral

class pyfcstm.bmc.ast.IntLiteral(raw: str, kind: str | None = None)[source]

Integer literal preserving raw token, numeric value, and literal kind.

Parameters:

raw (str) – Raw integer token text such as "42" or "0x2A".
kind (str, optional) – Literal kind, either "decimal" or "hex". When omitted, the kind is inferred from raw. Explicit kind values must match the raw spelling.

Example:

>>> IntLiteral("0x2A").to_canonical()["kind"]
'hex'

property value: int

Return the integer value represented by raw.

Returns:: Parsed integer value.
Return type:: int

Example:

>>> IntLiteral("0x10").value
16

CallStepPoint

class pyfcstm.bmc.ast.CallStepPoint(kind: Literal['absolute', 'relative'], value: int)[source]

Point used by called and call_count step selectors.

A point is either absolute, such as 3, or relative to the predicate anchor, such as +2 or -1. Relative zero canonicalizes to +0 so +0 and -0 compare equal after parsing.

Parameters:

kind (str) – "absolute" or "relative".
value (int) – Non-negative absolute index or signed relative offset.

Example:

>>> str(CallStepPoint.relative(0))
'+0'
>>> CallStepPoint.absolute(3).to_canonical()["value"]
3

__str__() → str[source]

Return canonical .fbmcq text for this point.

Returns:: Point DSL text.
Return type:: str

Example:

>>> str(CallStepPoint.relative(0))
'+0'

classmethod absolute(value: int) → CallStepPoint[source]

Return an absolute step point.

Parameters:: value (int) – Non-negative step index.
Returns:: Absolute step point.
Return type:: CallStepPoint

Example:

>>> str(CallStepPoint.absolute(2))
'2'

classmethod relative(value: int) → CallStepPoint[source]

Return a relative step point.

Parameters:: value (int) – Signed offset from the predicate anchor.
Returns:: Relative step point.
Return type:: CallStepPoint

Example:

>>> str(CallStepPoint.relative(-3))
'-3'

to_canonical() → Dict[str, Any][source]

Return a JSON-stable point summary.

Returns:: Canonical call step point.
Return type:: Dict[str, object]

Example:

>>> CallStepPoint.relative(1).to_canonical()["kind"]
'relative'

CallStepSelector

class pyfcstm.bmc.ast.CallStepSelector(kind: Literal['omitted', 'all', 'point', 'range'] = 'omitted', start: CallStepPoint | None = None, end: CallStepPoint | None = None)[source]

Step set selector used by abstract-call query predicates.

Parameters:

kind (str) – "omitted", "all", "point", or "range".
start (CallStepPoint, optional) – Point or None for omitted/current range starts.
end (CallStepPoint, optional) – Point or None for omitted/current range ends.

Example:

>>> str(CallStepSelector.all())
'*'
>>> str(CallStepSelector.range(CallStepPoint.relative(-2), CallStepPoint.relative(0)))
'-2..+0'

__str__() → str[source]

Return canonical selector DSL text.

Returns:: Selector text.
Return type:: str

Example:

>>> str(CallStepSelector.range(CallStepPoint.relative(-1), None))
'-1..'

classmethod all() → CallStepSelector[source]

Return the all-steps selector.

Returns:: All-steps selector.
Return type:: CallStepSelector

Example:

>>> str(CallStepSelector.all())
'*'

classmethod omitted() → CallStepSelector[source]

Return the implicit current-step selector.

Returns:: Omitted selector.
Return type:: CallStepSelector

Example:

>>> CallStepSelector.omitted().to_canonical()["kind"]
'omitted'

classmethod point(point: CallStepPoint) → CallStepSelector[source]

Return a point selector.

Parameters:: point (CallStepPoint) – Selected step point.
Returns:: Point selector.
Return type:: CallStepSelector

Example:

>>> str(CallStepSelector.point(CallStepPoint.absolute(3)))
'3'

classmethod range(start: CallStepPoint | None, end: CallStepPoint | None) → CallStepSelector[source]

Return an inclusive range or relative window selector.

Parameters:

start (CallStepPoint, optional) – Start point, or None for the current anchor.
end (CallStepPoint, optional) – End point, or None for the current anchor.

Returns:

Range selector.

Return type:

CallStepSelector

Example:

>>> str(CallStepSelector.range(None, CallStepPoint.relative(2)))
'..+2'

to_canonical() → Dict[str, Any][source]

Return a JSON-stable selector summary.

Returns:: Canonical call step selector.
Return type:: Dict[str, object]

Example:

>>> CallStepSelector.all().to_canonical()["kind"]
'all'

CallFilter

Shared argument model for called and call_count predicates.

Omitted filter fields mean true for that dimension. where is a filter over the matched call-time snapshot, not a global assertion over all calls. str() returns the canonical argument fragment without the surrounding called or call_count function name.

Parameters:

action (str, optional) – Resolved abstract action path filter, defaults to None.
step (CallStepSelector, optional) – Step selector, defaults to omitted/current.
stage (str, optional) – Lifecycle stage filter such as "during".
role (str, optional) – Runtime role filter such as "aspect_during_before".
state (str, optional) – Runtime public state path filter.
active_leaf (str, optional) – Runtime active leaf path filter.
named_ref (str, optional) – Named-ref callsite path filter, defaults to None.
named_ref_is_null (bool, optional) – Whether named_ref=null was requested.
where (BmcCondExpr, optional) – Snapshot predicate filter, defaults to None.

Example:

>>> str(CallFilter(action="Root.Hook"))
'"Root.Hook"'

__str__() → str[source]

Return the comma-separated canonical argument list.

Returns:: Argument DSL text without surrounding function name.
Return type:: str

Example:

>>> str(CallFilter(action="A", step=CallStepSelector.all()))
'"A", *'

property effective_step: CallStepSelector

Return explicit or omitted step selector.

Returns:: Step selector.
Return type:: CallStepSelector

Example:

>>> CallFilter().effective_step.kind
'omitted'

to_canonical() → Dict[str, Any][source]

Return a JSON-stable call-filter shape.

Returns:: Canonical call filter.
Return type:: Dict[str, object]

Example:

>>> CallFilter(action="A").to_canonical()["action"]
'A'

FloatLiteral

class pyfcstm.bmc.ast.FloatLiteral(raw: str)[source]

Floating-point literal preserving the raw token text.

Parameters:: raw (str) – Raw floating-point token text.

Example:

>>> FloatLiteral("1e2").to_canonical()["value"]
100.0

property value: float

Return the floating-point value represented by raw.

Returns:: Parsed float value.
Return type:: float

Example:

>>> FloatLiteral("3.5").value
3.5

BoolLiteral

class pyfcstm.bmc.ast.BoolLiteral(raw: str)[source]

Boolean literal preserving raw spelling and normalized value.

Canonical DSL output uses lowercase true / false even when raw records title-case or uppercase parser input. The exact input spelling remains available through to_canonical().

Parameters:: raw (str) – Raw boolean token text such as "true" or "FALSE".

Example:

>>> BoolLiteral("FALSE").to_canonical()["value"]
False

property value: bool

Return the boolean value represented by raw.

Returns:: Parsed boolean value.
Return type:: bool

Example:

>>> BoolLiteral("True").value
True

NameRef

class pyfcstm.bmc.ast.NameRef(name: str)[source]

Bare FCSTM variable reference used as a numeric expression.

Names that are reserved by FCSTM or FBMCQ syntax are rejected in bare form. A model variable whose name collides with a FBMCQ query atom, such as "cycle" or "event", should be represented through FrameVar and rendered as var("...") instead.

Parameters:: name (str) – Variable name from the query expression.

Example:

>>> NameRef("counter").to_canonical()
{'node': 'name', 'name': 'counter'}

MathConst

class pyfcstm.bmc.ast.MathConst(name: str)[source]

FCSTM mathematical constant expression.

Parameters:: name (str) – Constant name, one of "pi", "E", or "tau".

Example:

>>> MathConst("pi").to_canonical()["name"]
'pi'

NumUnaryOp

class pyfcstm.bmc.ast.NumUnaryOp(op: str, operand: BmcNumExpr)[source]

Numeric unary operator expression.

Parameters:

op (str) – Unary operator, either "+" or "-".
operand (BmcNumExpr) – Numeric operand.

Example:

>>> NumUnaryOp("-", NameRef("x")).to_canonical()["op"]
'-'

NumBinaryOp

class pyfcstm.bmc.ast.NumBinaryOp(left: BmcNumExpr, op: str, right: BmcNumExpr)[source]

Numeric binary operator expression.

Parameters:

left (BmcNumExpr) – Left numeric operand.
op (str) – Numeric operator following FCSTM grammar spelling.
right (BmcNumExpr) – Right numeric operand.

Example:

>>> NumBinaryOp(NameRef("x"), "+", IntLiteral("1")).to_canonical()["op"]
'+'

NumConditionalOp

class pyfcstm.bmc.ast.NumConditionalOp(condition: BmcCondExpr, if_true: BmcNumExpr, if_false: BmcNumExpr)[source]

Numeric conditional expression with a condition selector.

Parameters:

condition (BmcCondExpr) – Condition deciding which branch is selected.
if_true (BmcNumExpr) – Numeric expression used when condition is true.
if_false (BmcNumExpr) – Numeric expression used when condition is false.

Example:

>>> NumConditionalOp(BoolLiteral("true"), IntLiteral("1"), IntLiteral("0")).to_canonical()["node"]
'num_conditional'

UFuncCall

class pyfcstm.bmc.ast.UFuncCall(func: str, operand: BmcNumExpr)[source]

FCSTM unary math function call.

Parameters:

func (str) – Function name from FCSTM UFUNC_NAME.
operand (BmcNumExpr) – Numeric function argument.

Example:

>>> UFuncCall("sqrt", NameRef("x")).to_canonical()["func"]
'sqrt'

CondUnaryOp

class pyfcstm.bmc.ast.CondUnaryOp(op: str, operand: BmcCondExpr)[source]

Condition unary operator expression.

Parameters:

op (str) – Unary condition operator, "!" or alias "not".
operand (BmcCondExpr) – Condition operand.

Example:

>>> CondUnaryOp("not", BoolLiteral("true")).to_canonical()["op"]
'!'

NumericComparison

class pyfcstm.bmc.ast.NumericComparison(left: BmcNumExpr, op: str, right: BmcNumExpr)[source]

Comparison between two numeric expressions.

Parameters:

left (BmcNumExpr) – Left numeric operand.
op (str) – Comparison operator.
right (BmcNumExpr) – Right numeric operand.

Example:

>>> NumericComparison(NameRef("x"), "<", IntLiteral("2")).to_canonical()["op"]
'<'

CondBinaryOp

class pyfcstm.bmc.ast.CondBinaryOp(left: BmcCondExpr, op: str, right: BmcCondExpr)[source]

Condition binary operator expression.

Parameters:

left (BmcCondExpr) – Left condition operand.
op (str) – Condition operator or FCSTM alias.
right (BmcCondExpr) – Right condition operand.

Example:

>>> CondBinaryOp(BoolLiteral("true"), "and", BoolLiteral("false")).to_canonical()["op"]
'&&'

CondConditionalOp

class pyfcstm.bmc.ast.CondConditionalOp(condition: BmcCondExpr, if_true: BmcCondExpr, if_false: BmcCondExpr)[source]

Condition conditional expression.

Parameters:

condition (BmcCondExpr) – Condition deciding which branch is selected.
if_true (BmcCondExpr) – Condition expression used when condition is true.
if_false (BmcCondExpr) – Condition expression used when condition is false.

Example:

>>> CondConditionalOp(BoolLiteral("true"), BoolLiteral("true"), BoolLiteral("false")).to_canonical()["node"]
'cond_conditional'

FrameVar

class pyfcstm.bmc.ast.FrameVar(name: str, spelling: str = 'var_call')[source]

Numeric reference produced by the query-level var("...") atom.

The query AST is frame-relative rather than solver-frame-indexed. Later binder and lowering phases decide which concrete frame a var("x") expression reads from. The spelling field distinguishes this explicit query atom from a bare NameRef that still follows FCSTM ID lexical rules. The current data model accepts only the explicit var("...") spelling family; the field is preserved in the canonical form so parser tests can assert that bare names and frame-variable calls do not collapse together.

Parameters:

name (str) – Persistent variable name carried by var("...").
spelling (str, optional) – Query spelling family, defaults to "var_call".

Example:

>>> FrameVar("x").to_canonical()["spelling"]
'var_call'

Cycle

class pyfcstm.bmc.ast.Cycle[source]

Built-in numeric cycle expression for query predicates.

cycle is a reserved bare numeric atom, not a function call. This keeps it close to FCSTM mathematical constants such as pi while BMC predicates that require quoted model paths keep function-call spellings such as active("Root.A") and event("Root.E", current).

Example:

>>> Cycle().to_canonical()
{'node': 'cycle'}

Active

class pyfcstm.bmc.ast.Active(state_path: str, frame: int | Literal['current'] = 'current')[source]

Boolean atom stating that a state is active at a frame.

Parameters:

state_path (str) – Fully qualified or query-local state path string.
frame (int or str, optional) – Frame index or "current", defaults to "current".

Example:

>>> Active("Root.Idle").to_canonical()["frame"]
'current'

Terminated

class pyfcstm.bmc.ast.Terminated(frame: int | Literal['current'] = 'current')[source]

Boolean atom stating that execution is terminated at a frame.

Parameters:: frame (int or str, optional) – Frame index or "current", defaults to "current".

Example:

>>> Terminated().to_canonical()["node"]
'terminated'

Event

class pyfcstm.bmc.ast.Event(event_path: str, selector: int | Literal['current'] = 'current')[source]

Boolean atom stating that an event is selected for a query cycle.

Event atoms always render their selector argument explicitly, even for the default "current" selector. The explicit spelling keeps event-cycle selection separate from the optional frame shorthand used by state and case atoms.

Parameters:

event_path (str) – Fully qualified or query-local event path string.
selector (int or str, optional) – Concrete cycle index or "current", defaults to "current".

Example:

>>> str(Event("Root.Idle.Start"))
'event("Root.Idle.Start", current)'
>>> Event("Root.Idle.Start", selector=0).to_canonical()["event_path"]
'Root.Idle.Start'

Case

class pyfcstm.bmc.ast.Case(label: str, frame: int | Literal['current'] = 'current')[source]

Boolean atom stating that a macro-step case is selected at a frame.

Parameters:

label (str) – Canonical macro-step case label.
frame (int or str, optional) – Frame index or "current", defaults to "current".

Example:

>>> Case("Root.A::fallback::Root.A::0", frame=1).to_canonical()["frame"]
1

CallCount

class pyfcstm.bmc.ast.CallCount(filter: CallFilter = CallFilter(action=None, step=None, stage=None, role=None, state=None, active_leaf=None, named_ref=None, named_ref_is_null=False, where=None))[source]

Numeric expression counting matching abstract-call occurrences.

Parameters:: filter (CallFilter, optional) – Shared abstract-call filter, defaults to an empty filter.

Example:

>>> str(CallCount(CallFilter(action="Root.Hook")))
'call_count("Root.Hook")'

Called

class pyfcstm.bmc.ast.Called(name: str | None = None, frame: int | Literal['current'] = 'current', filter: CallFilter | None = None)[source]

Boolean atom testing whether a matching abstract call exists.

The legacy Called("Hook", frame=2) constructor remains accepted for compatibility with earlier query-model tests. New parser output should use CallFilter so called() and richer named arguments are available.

Parameters:

name (str, optional) – Legacy abstract action or hook name, defaults to None.
frame (int or str, optional) – Legacy frame/step selector, defaults to "current".
filter (CallFilter, optional) – Shared call filter for the new argument model, defaults to None.

Example:

>>> Called("Check", frame=2).to_canonical()["name"]
'Check'
>>> str(Called(filter=CallFilter()))
'called()'

property call_filter: CallFilter

Return the normalized call filter.

Returns:: Call filter used by semantic lowering.
Return type:: CallFilter

Example:

>>> Called("Hook", frame=1).call_filter.action
'Hook'

pyfcstm.bmc.ast

__all__

BmcExpr

BmcNumExpr

BmcCondExpr

IntLiteral

CallStepPoint

CallStepSelector

CallFilter

FloatLiteral

BoolLiteral

NameRef

MathConst

NumUnaryOp

NumBinaryOp

NumConditionalOp

UFuncCall

CondUnaryOp

NumericComparison

CondBinaryOp

CondConditionalOp

FrameVar

Cycle

Active

Terminated

Event

Case

CallCount

Called

all