orders

This module provides constructors to build verifiably well-founded orders, used in ranks.DomainLexRank.

class Order(abc.ABC):

Abstract base class for order constructors.

Orders are used in ranks.DomainLexRank to define lexicographic orderings over domains.

type OrderLike = Order | FormulaLike

Any value that can be converted to Order: an already constructed Order or a formula-like that would be converted to a FormulaOrder.

@dataclass(frozen=True)

class RelOrder(Order, typing.Generic[T]):

Order constructed from a binary relation. Considered well-founded when it is declared so (see typed_z3.WFRel) or when its input sort is declared finite (see typed_z3.Finite).

Constructed by giving a binary relation and a parameter name:

class Thread(Expr): ...
lt: WFRel[Thread]

rel_order = RelOrder(lt, "a")

rel: BiRel[T]

The binary relation.

param: str

Name of parameter.

Inherited Members

Order: check_well_founded

@dataclass(frozen=True)

class FormulaOrder(Order):

Order constructed from a ts.TSFormula. Considered well-founded when all its input sorts are declared finite (see typed_z3.Finite).

Constructed from any formula-like value:

class Thread(Finite): ...
class System(TransitionSystem):
    gt: BiRel[Thread]

def lt_formula(ts: System, a1: Thread, a2: Thread, b1: Thread, b2: Thread) -> BoolRef:
    return Or(ts.gt(a2, a1), And(a1 == a2, ts.gt(b2, b1))

formula_order = FormulaOrder(lt_formula)

Note that the parameter names for the formula must be of the form <name>1 <name>2 <other_name>1 <other_name>2. Order does not matter, but every parameter must end in 1 or 2, and must have a matching parameter ending in 2 or 1 (respectively).

formula: ts.FormulaLike

Source formula that can be converted to a ts.TSFormula.

def check_well_founded(self) -> bool:

Check whether the order is well-founded.

Returns

True if all input sorts are finite.

@dataclass(frozen=True)

class LexOrder(Order):

Order constructed from a lexicographic order over multiple binary relations. Considered well-founded when all of its underlying orders are well-founded.

Constructed by mapping parameters to binary relations:

class Thread(Finite): ...
class Ticket(Expr): ...

thread_order: BiRel[Thread]
ticket_order: WFRel[Ticket]
lex_order = LexOrder(a=thread_order, b=ticket_order)

def check_well_founded(self) -> bool:

Check whether the order is well-founded.

Returns

True if all underlying orders are well-founded.

@dataclass(frozen=True)

class PointwiseOrder(Order):

Order constructed from a pointwise order over multiple binary relations. Considered well-founded when all of its underlying orders are well-founded.

Constructed by mapping parameters to binary relations:

class Thread(Finite): ...
class Ticket(Expr): ...

thread_order: BiRel[Thread]
ticket_order: WFRel[Ticket]
pw_order = PointwiseOrder(a=thread_order, b=ticket_order)

def check_well_founded(self) -> bool:

Check whether the order is well-founded.

Returns

True if all underlying orders are well-founded.