pyudbm.binding.ucdd

High-level Python API for UCDD integration.

This module layers a Python-friendly symbolic API on top of the thin native _ucdd bindings. The design mirrors the existing pyudbm.binding.udbm compatibility layer:

CDDContext provides named clock and boolean variables;
CDD is the main symbolic set object;
pure clock zones can move between Federation and CDD;
extracted DBM fragments are wrapped back into the existing DBM class rather than introducing a second DBM wrapper hierarchy.

The UCDD runtime is global, so this module keeps one process-level runtime layout. Reusing the same clock layout and boolean prefix is supported. Trying to combine incompatible runtime layouts raises a descriptive error instead of silently corrupting level mappings.

Example:

>>> from pyudbm import Context
>>> from pyudbm.binding.ucdd import CDDContext
>>> base = Context(["x", "y"], name="c")
>>> ctx = CDDContext.from_context(base, bools=["door_open"])
>>> state = ((ctx.x <= 5) & ctx.door_open) | ((ctx.y <= 2) & ~ctx.door_open)
>>> isinstance(state.reduce().bdd_traces().to_dicts(), list)
True

all

pyudbm.binding.ucdd.__all__ = ['BDDTraceSet', 'CDD', 'CDDContext', 'CDDExtraction', 'CDDBool', 'CDDClock', 'CDDLevelInfo', 'OP_AND', 'OP_XOR', 'TYPE_BDD', 'TYPE_CDD']

Built-in mutable sequence.

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

OP_AND

pyudbm.binding.ucdd.OP_AND: int = 0

Native UCDD binary-operation code for logical conjunction / symbolic intersection.

This constant is primarily used with CDD.apply() and CDD.apply_reduce() when the caller wants to select the native conjunction operator explicitly instead of using left & right.

OP_XOR

pyudbm.binding.ucdd.OP_XOR: int = 1

Native UCDD binary-operation code for logical exclusive-or.

This constant is primarily used with CDD.apply() and CDD.apply_reduce() when the caller wants to select the native XOR operator explicitly instead of using left ^ right.

TYPE_BDD

pyudbm.binding.ucdd.TYPE_BDD: int = 1

Native level-type tag identifying one boolean-decision level in the global UCDD runtime.

Values of this kind appear in CDDLevelInfo and let callers distinguish pure BDD levels from clock-difference levels.

TYPE_CDD

pyudbm.binding.ucdd.TYPE_CDD: int = 0

Native level-type tag identifying one clock-difference level in the global UCDD runtime.

Values of this kind appear in CDDLevelInfo and let callers distinguish clock-difference levels from pure boolean-decision levels.

CDDLevelInfo

class pyudbm.binding.ucdd.CDDLevelInfo(level: int, type: int, clock1: int, clock2: int, diff: int)[source]

Immutable snapshot of one UCDD level descriptor.

Parameters:

level (int) – Level index inside the global UCDD runtime.
type (int) – Native level type constant such as TYPE_CDD.
clock1 (int) – Positive clock index used by CDD levels.
clock2 (int) – Negative clock index used by CDD levels.
diff (int) – Encoded clock-difference identifier from the native runtime.

CDDClock

class pyudbm.binding.ucdd.CDDClock(context: CDDContext, base_clock: Clock)[source]

Clock variable inside a CDDContext.

The DSL mirrors Clock, but comparisons return CDD objects instead of Federation objects.

The public behavior intentionally stays close to the restored UDBM API:

clock <= n builds a pure-clock CDD constraint;
clock1 - clock2 produces a CDDVariableDifference;
non-integer comparisons are rejected instead of being silently coerced.

Parameters:

context (CDDContext) – Owning mixed symbolic context.
base_clock (Clock) – Underlying clock from the wrapped Context.

Variables:

context – Owning mixed symbolic context.
name – Declared clock name.
dbm_index – Native DBM / CDD clock index.

Example:

>>> from pyudbm import Context
>>> from pyudbm.binding.ucdd import CDDContext
>>> ctx = CDDContext.from_context(Context(["x", "y"], name="c"))
>>> str(ctx.x.get_full_name())
'c.x'
>>> (ctx.x <= 3).to_federation() == (ctx.base_context.x <= 3)
True

__eq__(other: Any) → Any[source]

Build equality to a constant, or compare identity otherwise.

Parameters:: other (Any) – Integer bound or arbitrary object.
Returns:: CDD equality constraint for integers, otherwise identity comparison result.
Return type:: Any

Example:

>>> from pyudbm import Context
>>> ctx = Context(["x"]).to_cdd_context()
>>> (ctx.x == 2).to_federation() == (ctx.base_context.x == 2)
True

__ge__(bound: Any) → Any[source]

Build the non-strict lower-bound constraint clock >= bound.

Parameters:: bound (Any) – Integer lower bound.
Returns:: Equivalent pure-clock CDD.
Return type:: Any

Example:

>>> from pyudbm import Context
>>> ctx = Context(["x"]).to_cdd_context()
>>> (ctx.x >= 2).to_federation() == (ctx.base_context.x >= 2)
True

__gt__(bound: Any) → Any[source]

Build the strict lower-bound constraint clock > bound.

Parameters:: bound (Any) – Integer lower bound.
Returns:: Equivalent pure-clock CDD.
Return type:: Any

Example:

>>> from pyudbm import Context
>>> ctx = Context(["x"]).to_cdd_context()
>>> (ctx.x > 1).to_federation() == (ctx.base_context.x > 1)
True

__hash__() → int[source]

Return a stable hash derived from context identity and clock name.

Returns:: Hash value.
Return type:: int

Example:

>>> from pyudbm import Context
>>> ctx = Context(["x"]).to_cdd_context()
>>> isinstance(hash(ctx.x), int)
True

__init__(context: CDDContext, base_clock: Clock)[source]

Initialize one mixed-context clock wrapper.

Instances are normally created by CDDContext, not directly by user code.

Parameters:

context (CDDContext) – Owning mixed symbolic context.
base_clock (Clock) – Underlying wrapped UDBM clock.

Returns:

None.

Return type:

None

Example:

>>> from pyudbm import Context
>>> ctx = Context(["x"]).to_cdd_context()
>>> ctx.x.name
'x'

__le__(bound: Any) → Any[source]

Build the non-strict upper-bound constraint clock <= bound.

Parameters:: bound (Any) – Integer upper bound.
Returns:: Equivalent pure-clock CDD.
Return type:: Any

Example:

>>> from pyudbm import Context
>>> ctx = Context(["x"]).to_cdd_context()
>>> (ctx.x <= 3).to_federation() == (ctx.base_context.x <= 3)
True

__lt__(bound: Any) → Any[source]

Build the strict upper-bound constraint clock < bound.

Parameters:: bound (Any) – Integer upper bound.
Returns:: Equivalent pure-clock CDD.
Return type:: Any

Example:

>>> from pyudbm import Context
>>> ctx = Context(["x"]).to_cdd_context()
>>> (ctx.x < 4).to_federation() == (ctx.base_context.x < 4)
True

__ne__(other: Any) → Any[source]

Build disequality to a constant, or compare identity otherwise.

Parameters:: other (Any) – Integer bound or arbitrary object.
Returns:: CDD disequality constraint for integers, otherwise identity comparison result.
Return type:: Any

Example:

>>> from pyudbm import Context
>>> ctx = Context(["x"]).to_cdd_context()
>>> (ctx.x != 2).to_federation() == (ctx.base_context.x != 2)
True

__repr__() → str[source]

Return a debugging representation of the clock.

Returns:: Representation containing the fully-qualified clock name.
Return type:: str

Example:

>>> from pyudbm import Context
>>> ctx = Context(["x"], name="c").to_cdd_context()
>>> repr(ctx.x)
'<CDDClock c.x>'

__sub__(other: Any) → CDDVariableDifference[source]

Build a symbolic clock difference.

Parameters:: other (Any) – Right-hand clock.
Returns:: Symbolic clock-difference helper.
Return type:: CDDVariableDifference
Raises:: ValueError – If the clocks belong to different contexts.

Example:

>>> from pyudbm import Context
>>> from pyudbm.binding.ucdd import CDDVariableDifference
>>> ctx = Context(["x", "y"]).to_cdd_context()
>>> isinstance(ctx.x - ctx.y, CDDVariableDifference)
True

get_full_name() → str[source]

Return the context-qualified clock name used in string rendering.

Returns:: Qualified or plain clock name.
Return type:: str

CDDVariableDifference

class pyudbm.binding.ucdd.CDDVariableDifference(variables: List[CDDClock])[source]

Symbolic difference between two CDDClock variables.

This helper mirrors VariableDifference, but every comparison returns a CDD.

Parameters:

variables (list[CDDClock]) – Two clocks from the same CDDContext.

Variables:

context – Shared owning context.
vars – Ordered [left, right] clock pair.

Example:

>>> from pyudbm import Context
>>> ctx = Context(["x", "y"]).to_cdd_context()
>>> ((ctx.x - ctx.y) <= 1).to_federation() == (ctx.base_context.x - ctx.base_context.y <= 1)
True

__eq__(bound: Any) → Any[source]

Build left - right == bound for integer operands.

Parameters:: bound (Any) – Integer difference value or arbitrary object.
Returns:: CDD equality constraint for integers, otherwise False.
Return type:: Any

Example:

>>> from pyudbm import Context
>>> ctx = Context(["x", "y"]).to_cdd_context()
>>> ((ctx.x - ctx.y) == 0).to_federation() == (ctx.base_context.x - ctx.base_context.y == 0)
True

__ge__(bound: Any) → Any[source]

Build left - right >= bound.

Parameters:: bound (Any) – Integer lower bound.
Returns:: Equivalent CDD constraint.
Return type:: Any

Example:

>>> from pyudbm import Context
>>> ctx = Context(["x", "y"]).to_cdd_context()
>>> ((ctx.x - ctx.y) >= 1).to_federation() == (ctx.base_context.x - ctx.base_context.y >= 1)
True

__gt__(bound: Any) → Any[source]

Build left - right > bound.

Parameters:: bound (Any) – Integer lower bound.
Returns:: Equivalent CDD constraint.
Return type:: Any

Example:

>>> from pyudbm import Context
>>> ctx = Context(["x", "y"]).to_cdd_context()
>>> ((ctx.x - ctx.y) > 1).to_federation() == (ctx.base_context.x - ctx.base_context.y > 1)
True

__init__(variables: List[CDDClock])[source]

Initialize one symbolic clock-difference helper.

Parameters:: variables (List[CDDClock]) – Exactly two clocks from the same context.
Returns:: None.
Return type:: None
Raises:: ValueError – If the input does not contain exactly two compatible clocks.

Example:

>>> from pyudbm import Context
>>> ctx = Context(["x", "y"]).to_cdd_context()
>>> diff = CDDVariableDifference([ctx.x, ctx.y])
>>> len(diff.vars)
2

__le__(bound: Any) → Any[source]

Build left - right <= bound.

Parameters:: bound (Any) – Integer upper bound.
Returns:: Equivalent CDD constraint.
Return type:: Any

Example:

>>> from pyudbm import Context
>>> ctx = Context(["x", "y"]).to_cdd_context()
>>> ((ctx.x - ctx.y) <= 1).to_federation() == (ctx.base_context.x - ctx.base_context.y <= 1)
True

__lt__(bound: Any) → Any[source]

Build left - right < bound.

Parameters:: bound (Any) – Integer upper bound.
Returns:: Equivalent CDD constraint.
Return type:: Any

Example:

>>> from pyudbm import Context
>>> ctx = Context(["x", "y"]).to_cdd_context()
>>> ((ctx.x - ctx.y) < 1).to_federation() == (ctx.base_context.x - ctx.base_context.y < 1)
True

__ne__(bound: Any) → Any[source]

Build left - right != bound for integer operands.

Parameters:: bound (Any) – Integer difference value or arbitrary object.
Returns:: CDD disequality constraint for integers, otherwise True.
Return type:: Any

Example:

>>> from pyudbm import Context
>>> ctx = Context(["x", "y"]).to_cdd_context()
>>> ((ctx.x - ctx.y) != 0).to_federation() == (ctx.base_context.x - ctx.base_context.y != 0)
True

CDDBool

class pyudbm.binding.ucdd.CDDBool(context: CDDContext, name: str, level: int)[source]

Boolean variable inside a CDDContext.

The variable object is intentionally lightweight. Using it in symbolic expressions transparently produces CDD objects.

Parameters:

context (CDDContext) – Owning mixed symbolic context.
name (str) – Declared boolean name.
level (int) – Native BDD level in the global UCDD runtime.

Variables:

context – Owning mixed symbolic context.
name – User-visible boolean name.
level – Native BDD level.

Example:

>>> from pyudbm import Context
>>> ctx = Context(["x"]).to_cdd_context(bools=["flag"])
>>> (ctx.flag & (ctx.x <= 2)).extract_bdd_and_dbm().dbm.to_cdd().to_federation() == (ctx.base_context.x <= 2)
True

__and__(other: Any) → CDD[source]

Return the conjunction with another symbolic operand.

Parameters:: other (Any) – Another symbolic operand.
Returns:: Conjoined symbolic set.
Return type:: CDD

Example:

>>> from pyudbm import Context
>>> ctx = Context(["x"]).to_cdd_context(bools=["flag"])
>>> (ctx.flag & (ctx.x <= 2)).extract_bdd_and_dbm().has_bdd_part()
True

__eq__(other: Any) → Any[source]

Compare the boolean variable with a concrete boolean.

Parameters:: other (Any) – Boolean literal or arbitrary object.
Returns:: Positive or negative literal for booleans, otherwise identity comparison result.
Return type:: Any

Example:

>>> from pyudbm import Context
>>> ctx = Context(["x"]).to_cdd_context(bools=["flag"])
>>> (ctx.flag == True).equiv(ctx.flag.as_cdd())
True

__hash__() → int[source]

Return a stable hash derived from context, name, and level.

Returns:: Hash value.
Return type:: int

Example:

>>> from pyudbm import Context
>>> ctx = Context(["x"]).to_cdd_context(bools=["flag"])
>>> isinstance(hash(ctx.flag), int)
True

__init__(context: CDDContext, name: str, level: int)[source]

Initialize one boolean variable wrapper.

Instances are normally created by CDDContext.

Parameters:

context (CDDContext) – Owning mixed symbolic context.
name (str) – Declared boolean name.
level (int) – Native BDD level.

Returns:

None.

Return type:

None

Example:

>>> from pyudbm import Context
>>> ctx = Context(["x"]).to_cdd_context(bools=["flag"])
>>> ctx.flag.name
'flag'

__invert__() → CDD[source]

Return the negated boolean literal.

Returns:: Negative boolean literal.
Return type:: CDD

Example:

>>> from pyudbm import Context
>>> ctx = Context(["x"]).to_cdd_context(bools=["flag"])
>>> (~ctx.flag).equiv(CDD.bddnvar(ctx, "flag"))
True

__ne__(other: Any) → Any[source]

Compare the boolean variable for disequality with a concrete boolean.

Parameters:: other (Any) – Boolean literal or arbitrary object.
Returns:: Negative or positive literal for booleans, otherwise identity comparison result.
Return type:: Any

Example:

>>> from pyudbm import Context
>>> ctx = Context(["x"]).to_cdd_context(bools=["flag"])
>>> (ctx.flag != True).equiv(~ctx.flag.as_cdd())
True

__or__(other: Any) → CDD[source]

Return the disjunction with another symbolic operand.

Parameters:: other (Any) – Another symbolic operand.
Returns:: Union of the two symbolic sets.
Return type:: CDD

Example:

>>> from pyudbm import Context
>>> ctx = Context(["x"]).to_cdd_context(bools=["flag"])
>>> (ctx.flag | ~ctx.flag).is_true()
True

__rand__(other: Any) → CDD[source]

Return the reflected conjunction with another symbolic operand.

Parameters:: other (Any) – Another symbolic operand.
Returns:: Conjoined symbolic set.
Return type:: CDD

Example:

>>> from pyudbm import Context
>>> ctx = Context(["x"]).to_cdd_context(bools=["flag"])
>>> ((ctx.x <= 2) & ctx.flag).equiv(ctx.flag & (ctx.x <= 2))
True

__repr__() → str[source]

Return a debugging representation of the boolean variable.

Returns:: Representation containing the fully-qualified name.
Return type:: str

Example:

>>> from pyudbm import Context
>>> ctx = Context(["x"], name="c").to_cdd_context(bools=["flag"])
>>> repr(ctx.flag)
'<CDDBool c.flag>'

__ror__(other: Any) → CDD[source]

Return the reflected disjunction with another symbolic operand.

Parameters:: other (Any) – Another symbolic operand.
Returns:: Union of the two symbolic sets.
Return type:: CDD

Example:

>>> from pyudbm import Context
>>> ctx = Context(["x"]).to_cdd_context(bools=["flag"])
>>> ((ctx.x <= 2) | ctx.flag).equiv(ctx.flag | (ctx.x <= 2))
True

__rsub__(other: Any) → CDD[source]

Return the reflected set difference with another symbolic operand.

Parameters:: other (Any) – Another symbolic operand.
Returns:: Symbolic set difference other - self.
Return type:: CDD

Example:

>>> from pyudbm import Context
>>> ctx = Context(["x"]).to_cdd_context(bools=["flag"])
>>> (((ctx.x <= 2) | ctx.flag) - ctx.flag).contains_dbm((ctx.base_context.x <= 2).to_dbm_list()[0])
True

__rxor__(other: Any) → CDD[source]

Return the reflected exclusive-or with another symbolic operand.

Parameters:: other (Any) – Another symbolic operand.
Returns:: Exclusive-or symbolic set.
Return type:: CDD

Example:

>>> from pyudbm import Context
>>> ctx = Context(["x"]).to_cdd_context(bools=["flag"])
>>> ((ctx.x <= 2) ^ ctx.flag).equiv(ctx.flag ^ (ctx.x <= 2))
True

__sub__(other: Any) → CDD[source]

Return the set difference with another symbolic operand.

Parameters:: other (Any) – Another symbolic operand.
Returns:: Symbolic set difference.
Return type:: CDD

Example:

>>> from pyudbm import Context
>>> ctx = Context(["x"]).to_cdd_context(bools=["flag"])
>>> (ctx.flag - ctx.flag).is_false()
True

__xor__(other: Any) → CDD[source]

Return the exclusive-or with another symbolic operand.

Parameters:: other (Any) – Another symbolic operand.
Returns:: Exclusive-or symbolic set.
Return type:: CDD

Example:

>>> from pyudbm import Context
>>> ctx = Context(["x"]).to_cdd_context(bools=["flag"])
>>> (ctx.flag ^ ctx.flag).is_false()
True

as_cdd() → CDD[source]

Return this boolean variable as a one-node symbolic CDD.

Returns:: Positive boolean literal.
Return type:: CDD

get_full_name() → str[source]

Return the context-qualified boolean name.

Returns:: Qualified or plain boolean name.
Return type:: str

CDDContext

class pyudbm.binding.ucdd.CDDContext(clocks: Iterable[str], bools: Iterable[str] = (), name: str | None = None)[source]

Mixed clock/boolean symbolic context for UCDD.

A CDDContext wraps one clock layout together with an ordered set of boolean variables. Clock naming reuses the existing Context semantics so that federation and CDD conversions stay dimension-stable.

Parameters:

clocks (iterable[str]) – Clock names when creating a fresh compatibility context.
bools (iterable[str]) – Boolean variable names.
name (str or None) – Optional context display name.

Variables:

base_context – Wrapped clock-only Context.
clocks – List of CDDClock objects in declaration order.
bools – List of CDDBool objects in declaration order.
dimension – DBM / CDD dimension including the reference clock.

Example:

>>> from pyudbm import Context
>>> ctx = Context(["x", "y"], name="c").to_cdd_context(bools=["door_open"])
>>> ctx["x"] is ctx.x
True
>>> ctx["door_open"] is ctx.door_open
True
>>> ctx.dimension
3

__getitem__(name: str) → CDDClock | CDDBool[source]

Return one declared clock or boolean variable by name.

Parameters:: name (str) – Clock or boolean variable name.
Returns:: Matching symbolic variable.
Return type:: CDDClock or CDDBool
Raises:: KeyError – If the name is unknown.

Example:

>>> from pyudbm import Context
>>> ctx = Context(["x"], name="c").to_cdd_context(bools=["flag"])
>>> ctx["x"] is ctx.x
True

__hash__() → int[source]

Return a stable hash derived from clock names, boolean names, and the display name.

Returns:: Hash value.
Return type:: int

Example:

>>> from pyudbm import Context
>>> ctx = Context(["x"]).to_cdd_context(bools=["flag"])
>>> isinstance(hash(ctx), int)
True

__init__(clocks: Iterable[str], bools: Iterable[str] = (), name: str | None = None)[source]

Initialize a mixed clock/boolean symbolic context.

Parameters:

clocks (Iterable[str]) – Clock names to declare.
bools (Iterable[str]) – Boolean variable names to declare.
name (str or None) – Optional display prefix used for rendering.

Returns:

None.

Return type:

None

Raises:

ValueError – If boolean names are duplicated or collide with clock names.

Example:

>>> ctx = CDDContext(["x", "y"], bools=["flag"], name="c")
>>> ctx.bool_names
('flag',)

all_level_info() → List[CDDLevelInfo][source]

Return all currently visible runtime level descriptors.

Returns:: Level descriptors in runtime order.
Return type:: List[CDDLevelInfo]

property base_context: Context

Return the underlying clock-only Context.

Returns:: Wrapped clock-only context.
Return type:: Context

bool(name: str) → CDDBool[source]

Return one boolean variable by name.

Parameters:: name (str) – Declared boolean name.
Returns:: Matching boolean variable.
Return type:: CDDBool

bool_name_for_level(level: int) → str[source]

Return the declared boolean name for one runtime level.

Parameters:: level (int) – Runtime BDD level.
Returns:: Declared boolean name.
Return type:: str

clock(name: str) → CDDClock[source]

Return one clock variable by name.

Parameters:: name (str) – Declared clock name.
Returns:: Matching clock variable.
Return type:: CDDClock

false() → CDD[source]

Return the empty CDD for this context.

Returns:: Empty symbolic set in this context.
Return type:: CDD

classmethod from_context(context: Context, bools: Iterable[str] = (), name: str | None = None) → CDDContext[source]

Build a CDDContext from an existing Context.

The resulting object preserves the existing clock order so that Federation and DBM objects from the source context can be converted without dimension remapping.

Parameters:

context (Context) – Existing clock-only context.
bools (Iterable[str]) – Boolean variable names to add.
name (str or None) – Optional display-name override.

Returns:

New mixed symbolic context.

Return type:

CDDContext

Example:

>>> from pyudbm import Context
>>> base = Context(["x"], name="c")
>>> mixed = CDDContext.from_context(base, bools=["flag"])
>>> mixed.base_context is base
True

level_info(level: int) → CDDLevelInfo[source]

Return one decoded runtime level descriptor.

Parameters:: level (int) – Runtime level index.
Returns:: Immutable level-info snapshot.
Return type:: CDDLevelInfo

true() → CDD[source]

Return the tautological CDD for this context.

Returns:: Symbolic tautology in this context.
Return type:: CDD

BDDTraceSet

class pyudbm.binding.ucdd.BDDTraceSet(context: CDDContext, native: Any)[source]

Iterable wrapper around the native bdd_arrays structure.

The underlying native object stores one collection of BDD traces extracted from a symbolic CDD. The Python wrapper turns that low-level array-shaped data into normal Python iteration helpers.

Iteration yields sparse dictionaries mapping boolean names to truth values. This is useful when a CDD is logically a pure BDD, or when only the boolean portion of a mixed symbolic state is relevant.

Parameters:

context (CDDContext) – Owning symbolic context whose boolean names label the extracted traces.
native (Any) – Native bdd_arrays wrapper returned by the thin UCDD binding.

Variables:

context – Owning symbolic context.

Example:

>>> from pyudbm import Context
>>> ctx = Context(["x"]).to_cdd_context(bools=["door_open", "alarm"])
>>> traces = (ctx.door_open | ctx.alarm).bdd_traces()
>>> isinstance(traces.to_dicts(), list)
True

__init__(context: CDDContext, native: Any)[source]

Initialize one boolean-trace wrapper.

Instances are usually created by CDD.bdd_traces().

Parameters:

context (CDDContext) – Owning symbolic context.
native (Any) – Native bdd_arrays object.

Returns:

None.

Return type:

None

Example:

>>> from pyudbm import Context
>>> ctx = Context(["x"]).to_cdd_context(bools=["flag"])
>>> traces = ctx.flag.bdd_traces()
>>> isinstance(traces, BDDTraceSet)
True

__iter__() → Iterator[Dict[str, bool]][source]

Iterate over sparse boolean assignments.

Each yielded mapping contains only the boolean variables that were explicitly present on the corresponding BDD path.

Returns:: Iterator over sparse boolean assignments.
Return type:: Iterator[Dict[str, bool]]

Example:

>>> from pyudbm import Context
>>> ctx = Context(["x"]).to_cdd_context(bools=["flag"])
>>> next(iter(ctx.flag.bdd_traces()))["flag"]
True

__len__() → int[source]

Return the number of extracted boolean traces.

Returns:: Trace count.
Return type:: int

Example:

>>> from pyudbm import Context
>>> ctx = Context(["x"]).to_cdd_context(bools=["flag"])
>>> len(ctx.flag.bdd_traces()) >= 1
True

to_dicts(sparse: bool = True) → List[Dict[str, bool | None]][source]

Return traces as dictionaries keyed by boolean name.

Parameters:: sparse (bool) – When True, omit unspecified booleans. When False, include every boolean name and use None for unspecified values.
Returns:: Boolean assignments keyed by variable name.
Return type:: List[Dict[str, Optional[bool]]]

Example:

>>> from pyudbm import Context
>>> ctx = Context(["x"]).to_cdd_context(bools=["flag"])
>>> rows = ctx.flag.bdd_traces().to_dicts(sparse=False)
>>> rows[0]["flag"]
True

to_rows() → List[Tuple[Tuple[str, bool], ...]][source]

Return each trace as an ordered tuple of (bool_name, value) pairs.

This preserves the native row order and is useful when a deterministic positional representation is more convenient than dictionaries.

Returns:: Ordered boolean assignments.
Return type:: List[Tuple[Tuple[str, bool], …]]

CDDExtraction

class pyudbm.binding.ucdd.CDDExtraction(context: CDDContext, native: Any)[source]

High-level wrapper for one extract_bdd_and_dbm result.

A mixed CDD path can be seen as a boolean guard together with one extracted DBM zone. This wrapper keeps those parts in public high-level objects so callers can continue working with familiar CDD and DBM values.

Parameters:

context (CDDContext) – Owning symbolic context.
native (Any) – Native extraction result object returned by the thin UCDD binding.

Variables:

remainder – Remaining symbolic graph after one DBM extraction.
bdd_part – Boolean guard associated with the extracted DBM.
dbm – Extracted DBM wrapped through the existing DBM class.

Example:

>>> from pyudbm import Context
>>> ctx = Context(["x"]).to_cdd_context(bools=["flag"])
>>> extraction = (ctx.flag & (ctx.x <= 3)).extract_bdd_and_dbm()
>>> extraction.has_bdd_part()
True

__init__(context: CDDContext, native: Any)[source]

Initialize one extracted mixed symbolic fragment.

Parameters:

context (CDDContext) – Owning symbolic context.
native (Any) – Native extraction result.

Returns:

None.

Return type:

None

Example:

>>> from pyudbm import Context
>>> ctx = Context(["x"]).to_cdd_context(bools=["flag"])
>>> extraction = (ctx.flag & (ctx.x <= 2)).extract_bdd_and_dbm()
>>> isinstance(extraction, CDDExtraction)
True

has_bdd_part() → bool[source]

Return whether the extraction carried a non-trivial boolean guard.

Returns:: True if bdd_part is not the tautology.
Return type:: bool

to_federation(require_pure: bool = True) → Federation[source]

Convert the extracted DBM to a one-zone federation when its boolean guard is trivial.

Parameters:

require_pure (bool) – Whether to reject non-trivial boolean guards with ValueError. When False, mixed guarded conversion still raises NotImplementedError because this wrapper does not yet materialize guarded federation fragments.

Returns:

One-zone federation equivalent to dbm.

Return type:

Federation

Raises:

ValueError – If the extraction still carries a boolean guard and require_pure is True.
NotImplementedError – If guarded federation conversion is requested with require_pure=False.

CDD

class pyudbm.binding.ucdd.CDD(context: CDDContext, native: _NativeCDD)[source]

High-level symbolic Clock Difference Diagram wrapper.

Instances behave like symbolic sets. Boolean variables and clock constraints can be combined through the normal Python operators &, |, ^, -, and ~.

Conceptually this class is the mixed-symbolic counterpart to Federation:

pure clock states can move between Federation and CDD;
boolean literals can be combined with clock constraints in one symbolic graph;
extraction helpers expose individual DBM fragments and their associated boolean guards.

Unless stated otherwise, operations return new symbolic objects and do not mutate the original CDD.

Parameters:

context (CDDContext) – Owning mixed symbolic context.
native (_NativeCDD) – Native UCDD handle.

Variables:

context – Owning mixed symbolic context.

Example:

>>> from pyudbm import Context
>>> ctx = Context(["x", "y"], name="c").to_cdd_context(bools=["door_open"])
>>> state = ((ctx.x <= 5) & ctx.door_open) | ((ctx.y <= 2) & ~ctx.door_open)
>>> isinstance(state.reduce(), CDD)
True

__and__(other: Any) → CDD[source]

Return the conjunction / symbolic intersection with another operand.

Parameters:: other (Any) – Another CDD, CDDBool, Federation, or DBM from the same clock layout.
Returns:: Conjoined symbolic set.
Return type:: CDD

Example:

>>> from pyudbm import Context
>>> ctx = Context(["x"]).to_cdd_context(bools=["flag"])
>>> ((ctx.x <= 3) & ctx.flag).extract_bdd_and_dbm().has_bdd_part()
True

__eq__(other: Any) → bool[source]

Compare two CDDs by symbolic equivalence.

Unlike plain handle identity, this checks semantic equivalence inside the same CDDContext.

Parameters:: other (Any) – Object to compare with.
Returns:: Whether both CDDs denote the same symbolic set.
Return type:: bool

Example:

>>> from pyudbm import Context
>>> ctx = Context(["x"]).to_cdd_context()
>>> (ctx.x <= 3) == CDD.from_federation(ctx.base_context.x <= 3, cdd_context=ctx)
True

__init__(context: CDDContext, native: _NativeCDD)[source]

Initialize one high-level symbolic CDD wrapper.

Instances are normally created through the class constructors such as true(), from_federation(), or boolean / clock DSL expressions.

Parameters:

context (CDDContext) – Owning mixed symbolic context.
native (_NativeCDD) – Native UCDD handle.

Returns:

None.

Return type:

None

Example:

>>> from pyudbm import Context
>>> ctx = Context(["x"]).to_cdd_context()
>>> state = CDD.true(ctx)
>>> isinstance(state, CDD)
True

__invert__() → CDD[source]

Return the symbolic complement.

Returns:: Complement of this symbolic set.
Return type:: CDD

Example:

>>> from pyudbm import Context
>>> ctx = Context(["x"]).to_cdd_context()
>>> ((~(ctx.x <= 2)) | (ctx.x <= 2)).is_true()
True

__ne__(other: Any) → bool[source]

Return whether another object is not semantically equivalent.

Parameters:: other (Any) – Object to compare with.
Returns:: Negation of __eq__().
Return type:: bool

Example:

>>> from pyudbm import Context
>>> ctx = Context(["x"]).to_cdd_context()
>>> (ctx.x <= 3) != (ctx.x <= 2)
True

__or__(other: Any) → CDD[source]

Return the symbolic union with another operand.

Parameters:: other (Any) – Another symbolic operand.
Returns:: Union of the two symbolic sets.
Return type:: CDD

Example:

>>> from pyudbm import Context
>>> ctx = Context(["x"]).to_cdd_context()
>>> ((ctx.x <= 2) | (ctx.x >= 5)).to_federation() == ((ctx.base_context.x <= 2) | (ctx.base_context.x >= 5))
True

__rand__(other: Any) → CDD[source]

Return the reflected conjunction with another symbolic operand.

Parameters:: other (Any) – Another symbolic operand.
Returns:: Conjoined symbolic set.
Return type:: CDD

Example:

>>> from pyudbm import Context
>>> ctx = Context(["x"]).to_cdd_context(bools=["flag"])
>>> ((ctx.x <= 3) & ctx.flag).equiv(ctx.flag & (ctx.x <= 3))
True

__repr__() → str[source]

Return a compact debugging representation.

Returns:: Representation containing node count and context name.
Return type:: str

Example:

>>> from pyudbm import Context
>>> state = (Context(["x"], name="c").to_cdd_context().x <= 3)
>>> repr(state).startswith("<CDD nodes=")
True

__ror__(other: Any) → CDD[source]

Return the reflected union with another symbolic operand.

Parameters:: other (Any) – Another symbolic operand.
Returns:: Union of the two symbolic sets.
Return type:: CDD

Example:

>>> from pyudbm import Context
>>> ctx = Context(["x"]).to_cdd_context(bools=["flag"])
>>> ((ctx.x <= 2) | ctx.flag).equiv(ctx.flag | (ctx.x <= 2))
True

__rsub__(other: Any) → CDD[source]

Return the reflected symbolic set difference other - self.

Parameters:: other (Any) – Another symbolic operand.
Returns:: Symbolic set difference other - self.
Return type:: CDD

Example:

>>> from pyudbm import Context
>>> ctx = Context(["x"]).to_cdd_context(bools=["flag"])
>>> (((ctx.x <= 3) | ctx.flag) - ctx.flag).contains_dbm((ctx.base_context.x <= 3).to_dbm_list()[0])
True

__rxor__(other: Any) → CDD[source]

Return the reflected exclusive-or with another symbolic operand.

Parameters:: other (Any) – Another symbolic operand.
Returns:: Exclusive-or symbolic set.
Return type:: CDD

Example:

>>> from pyudbm import Context
>>> ctx = Context(["x"]).to_cdd_context(bools=["flag"])
>>> ((ctx.x <= 2) ^ ctx.flag).equiv(ctx.flag ^ (ctx.x <= 2))
True

__sub__(other: Any) → CDD[source]

Return the symbolic set difference self - other.

Parameters:: other (Any) – Another symbolic operand.
Returns:: Symbolic set difference.
Return type:: CDD

Example:

>>> from pyudbm import Context
>>> ctx = Context(["x"]).to_cdd_context()
>>> (((ctx.x <= 5) - (ctx.x <= 2)).to_federation() == ((ctx.base_context.x <= 5) - (ctx.base_context.x <= 2)))
True

__xor__(other: Any) → CDD[source]

Return the symbolic exclusive-or with another operand.

Parameters:: other (Any) – Another symbolic operand.
Returns:: Exclusive-or symbolic set.
Return type:: CDD

Example:

>>> from pyudbm import Context
>>> ctx = Context(["x"]).to_cdd_context(bools=["flag"])
>>> (ctx.flag ^ ctx.flag).is_false()
True

apply(op: int, other: Any) → CDD[source]

Apply one native binary operator code to another symbolic operand.

The public constants OP_AND and OP_XOR expose the currently supported operator codes at the Python layer.

Parameters:

op (int) – Native operation code.
other (Any) – Another symbolic operand.

Returns:

Result of the native binary operation.

Return type:

CDD

apply_reduce(op: int, other: Any) → CDD[source]

Apply one native binary operator code and reduce the result.

Parameters:

op (int) – Native operation code.
other (Any) – Another symbolic operand.

Returns:

Reduced result of the native binary operation.

Return type:

CDD

Apply Python-friendly clock and boolean reset mappings.

Clock resets use integer assignments, while boolean resets use Python bool values. Keys may be variable names or the corresponding public clock / boolean objects.

Parameters:

clock_resets (mapping or iterable or None) – Mapping or iterable of (clock, value) pairs.
bool_resets (mapping or iterable or None) – Mapping or iterable of (bool_var, value) pairs.

Returns:

Reset symbolic set.

Return type:

CDD

Example:

>>> from pyudbm import Context
>>> ctx = Context(["x"]).to_cdd_context(bools=["flag"])
>>> state = (ctx.x <= 3) & ctx.flag
>>> isinstance(state.apply_reset({"x": 0}, {"flag": False}), CDD)
True

bdd_traces() → BDDTraceSet[source]

Return the boolean traces of this CDD interpreted as a BDD.

The result is most meaningful for pure-boolean or BDD-shaped CDDs, but the native helper is exposed as-is.

Returns:: Iterable boolean-trace wrapper.
Return type:: BDDTraceSet

classmethod bddnvar(context: CDDContext | Context, level_or_name: int | str) → CDD[source]

Build the negative literal of one boolean variable.

Parameters:

context (CDDContext or Context) – Target mixed context, or a plain clock context that has already been promoted to a compatible boolean layout.
level_or_name (int or str) – Boolean runtime level or declared variable name.

Returns:

Negative boolean literal.

Return type:

CDD

classmethod bddvar(context: CDDContext | Context, level_or_name: int | str) → CDD[source]

Build the positive literal of one boolean variable.

Parameters:

context (CDDContext or Context) – Target mixed context, or a plain clock context that has already been promoted to a compatible boolean layout.
level_or_name (int or str) – Boolean runtime level or declared variable name.

Returns:

Positive boolean literal.

Return type:

CDD

contains_dbm(dbm: DBM) → bool[source]

Return whether one DBM zone is contained in this CDD.

Parameters:

dbm (DBM) – Candidate DBM zone.

Returns:

Whether the DBM is contained.

Return type:

bool

Raises:

TypeError – If dbm is not a DBM.
ValueError – If the DBM context has an incompatible clock layout.

copy() → CDD[source]

Return a copied symbolic handle for the same symbolic set.

Returns:: Semantically equivalent copied CDD.
Return type:: CDD

delay() → CDD[source]

Apply forward time elapse to the symbolic state.

This is the mixed-symbolic counterpart to federation up-style behavior.

Returns:: Time-successor symbolic set.
Return type:: CDD

delay_invariant(invariant: Any) → CDD[source]

Apply forward time elapse constrained by an invariant.

Parameters:: invariant (Any) – Invariant symbolic set that must remain satisfied during time passage.
Returns:: Time-successor symbolic set respecting the invariant.
Return type:: CDD

edgecount() → int[source]

Return the native edge count reported for this symbolic graph.

Returns:: Native edge count.
Return type:: int

equiv(other: Any) → bool[source]

Return whether another symbolic operand is semantically equivalent.

Parameters:: other (Any) – Another symbolic operand.
Returns:: Whether both denote the same symbolic set.
Return type:: bool

extract_bdd() → CDD[source]

Extract the bottom BDD of the first reduced DBM path.

Returns:: Extracted boolean guard as a CDD.
Return type:: CDD

extract_bdd_and_dbm() → CDDExtraction[source]

Extract one DBM together with its boolean guard.

The native operation expects a reduced CDD. The Python wrapper performs that reduction automatically so callers do not have to remember the precondition.

Returns:: High-level extraction bundle containing remainder, BDD guard, and DBM fragment.
Return type:: CDDExtraction

extract_dbm() → Tuple[CDD, DBM][source]

Extract one DBM from the reduced CDD and return (remainder, dbm).

This helper is convenient for pure-clock iteration where the boolean guard is known to be trivial and only the next DBM fragment matters.

Returns:: (remainder, dbm) pair.
Return type:: tuple[CDD, DBM]

classmethod false(context: CDDContext | Context) → CDD[source]

Return the empty symbolic set for one context.

Parameters:: context (CDDContext or Context) – Target mixed context, or a plain clock Context that will be promoted automatically.
Returns:: Empty symbolic set.
Return type:: CDD

classmethod from_dbm(dbm: DBM, cdd_context: CDDContext | None = None) → CDD[source]

Build a pure clock CDD from one DBM snapshot.

Parameters:

dbm (DBM) – Source DBM snapshot.
cdd_context (CDDContext or None) – Optional target mixed context. When omitted, a compatible clock-only CDDContext is built automatically from dbm.context.

Returns:

Equivalent pure-clock symbolic set.

Return type:

CDD

Raises:

TypeError – If dbm is not a DBM.
ValueError – If the target context has an incompatible clock layout.

Example:

>>> from pyudbm import Context
>>> base = Context(["x"], name="c")
>>> dbm = (base.x <= 3).to_dbm_list()[0]
>>> CDD.from_dbm(dbm).to_federation() == (base.x <= 3)
True

classmethod from_federation(federation: Federation, cdd_context: CDDContext | None = None) → CDD[source]

Build a pure clock CDD from a Federation.

Parameters:

federation (Federation) – Source federation.
cdd_context (CDDContext or None) – Optional target mixed context. When omitted, a compatible clock-only CDDContext is built automatically from federation.context.

Returns:

Equivalent pure-clock symbolic set.

Return type:

CDD

Raises:

TypeError – If federation is not a Federation.
ValueError – If the target context has an incompatible clock layout.

classmethod interval(context: CDDContext | Context, i: int, j: int, low: int, up: int) → CDD[source]

Build the raw interval constraint low <= x_i - x_j <= up.

Parameters:

context (CDDContext or Context) – Target mixed context, or a plain clock context.
i (int) – Left DBM clock index.
j (int) – Right DBM clock index.
low (int) – Inclusive lower bound.
up (int) – Inclusive upper bound.

Returns:

Equivalent pure-clock CDD.

Return type:

CDD

is_bdd() → bool[source]

Return whether this symbolic graph is purely boolean.

Returns:: True if the graph contains only BDD structure.
Return type:: bool

is_false() → bool[source]

Return whether this symbolic set is empty.

Returns:: True if the symbolic set is empty.
Return type:: bool

is_true() → bool[source]

Return whether this symbolic set is the tautology.

Returns:: True if the symbolic set is universally true.
Return type:: bool

ite(then_branch: Any, else_branch: Any) → CDD[source]

Build the symbolic if-then-else self ? then_branch : else_branch.

Parameters:

then_branch (Any) – Symbolic branch chosen where self holds.
else_branch (Any) – Symbolic branch chosen where self does not hold.

Returns:

Resulting symbolic combination.

Return type:

CDD

classmethod lower(context: CDDContext | Context, i: int, j: int, bound: int) → CDD[source]

Build the raw clock-difference constraint x_i - x_j >= bound.

Parameters:

context (CDDContext or Context) – Target mixed context, or a plain clock context.
i (int) – Left DBM clock index.
j (int) – Right DBM clock index.
bound (int) – Lower bound.

Returns:

Equivalent pure-clock CDD.

Return type:

CDD

nodecount() → int[source]

Return the native node count reported for this symbolic graph.

Returns:: Native node count.
Return type:: int

past() → CDD[source]

Apply inverse time elapse to the symbolic state.

Returns:: Past-closed symbolic set.
Return type:: CDD

predt(safe: Any) → CDD[source]

Compute the time predecessor relative to a safe region.

Parameters:: safe (Any) – Symbolic set that must remain satisfied during backward time propagation.
Returns:: Symbolic predecessor set.
Return type:: CDD

reduce() → CDD[source]

Return a reduced symbolic graph.

Reduction is a common prerequisite for extraction-oriented native UCDD operations. High-level helpers such as extract_bdd_and_dbm() already call it automatically.

Returns:: Reduced symbolic graph.
Return type:: CDD

reduce2() → CDD[source]

Return the alternative reduced form provided by native UCDD.

Returns:: Reduced symbolic graph.
Return type:: CDD

remove_negative() → CDD[source]

Remove negative constraints through the native UCDD helper.

Returns:: Transformed symbolic set.
Return type:: CDD

to_federation(require_pure: bool = True) → Federation[source]

Convert a pure clock CDD back into a Federation.

A non-trivial boolean guard cannot be represented as a plain federation, so mixed CDDs raise by default.

Parameters:

require_pure (bool) – Whether to reject mixed CDDs with ValueError. When False, mixed conversion still raises NotImplementedError because guarded federation output is not materialized by this wrapper.

Returns:

Equivalent pure-clock federation.

Return type:

Federation

Raises:

ValueError – If this CDD contains non-trivial boolean guards and require_pure is True.
NotImplementedError – If guarded federation conversion is requested with require_pure=False.

Example:

>>> from pyudbm import Context
>>> base = Context(["x"])
>>> pure = (base.x <= 3).to_cdd()
>>> pure.to_federation() == (base.x <= 3)
True

Apply a guard and then perform clock/boolean resets.

This corresponds to the common forward symbolic transition pattern: intersect with the transition guard, then apply discrete updates.

Parameters:

guard (Any) – Transition guard.
clock_resets (mapping or iterable or None) – Clock reset assignments.
bool_resets (mapping or iterable or None) – Boolean reset assignments.

Returns:

Forward transition successor.

Return type:

CDD

Compute the symbolic backward transition predecessor.

guard is the transition guard and update is the updated post- transition symbolic relation used by the native backward operator.

Parameters:

guard (Any) – Transition guard.
update (Any) – Updated symbolic target.
clock_resets (iterable or None) – Clocks reset by the transition.
bool_resets (iterable or None) – Boolean variables reset by the transition.

Returns:

Backward predecessor.

Return type:

CDD

Compute the backward predecessor and include inverse time elapse.

Parameters:

guard (Any) – Transition guard.
update (Any) – Updated symbolic target.
clock_resets (iterable or None) – Clocks reset by the transition.
bool_resets (iterable or None) – Boolean variables reset by the transition.

Returns:

Backward predecessor closed under inverse time elapse.

Return type:

CDD

classmethod true(context: CDDContext | Context) → CDD[source]

Return the tautological symbolic set for one context.

Parameters:: context (CDDContext or Context) – Target mixed context, or a plain clock Context that will be promoted automatically.
Returns:: Tautological symbolic set.
Return type:: CDD

classmethod upper(context: CDDContext | Context, i: int, j: int, bound: int) → CDD[source]

Build the raw clock-difference constraint x_i - x_j <= bound.

This is the low-level indexed constructor mirroring the native UCDD API. Most user code should prefer the clock DSL such as ctx.x - ctx.y <= 3.

Parameters:

context (CDDContext or Context) – Target mixed context, or a plain clock context.
i (int) – Left DBM clock index.
j (int) – Right DBM clock index.
bound (int) – Upper bound.

Returns:

Equivalent pure-clock CDD.

Return type:

CDD

pyudbm.binding.ucdd

__all__

OP_AND

OP_XOR

TYPE_BDD

TYPE_CDD

CDDLevelInfo

CDDClock

CDDVariableDifference

CDDBool

CDDContext

BDDTraceSet

CDDExtraction

CDD

all