timers

This module provides the interface to talk about timers. The Implicit Ranking Timers library supports two modes of timers:

Uninterpreted (unint, u): Time is an uninterpreted sort with axioms that make it behave as expected.
Interpreted (int, i): Time is expressed with interpreted integers, with infinity represented as -1.

Time expressions (of sort Time) are never created directly, but through temporal formulas (see proofs.Proof.t).

When running an example the mode can be configured by setting the environment variable TIMERS:

make examples/ticket.py TIMERS=<mode>

where <mode> is either unint or int. The default mode is int (interpreted integers).

class Time(typed_z3.Expr):

Time sort. Should not be instantiated directly.

class TimeFun(typing.Protocol):

Variadic callable returning a Time expression. A function with signature:

def time_fun(*args: z3.ExprRef) -> Time: ...

The usual way of producing a TimeFun is by calling proofs.Proof.t.

def timer_zero(timer_expr: Time) -> z3.z3.BoolRef:

Return a formula expressing that the timer expression is zero.

Formula expressing that the timer is zero.

def timer_finite(timer_expr: Time) -> z3.z3.BoolRef:

Return a formula expressing that the timer expression is finite.

Formula expressing that the timer is finite.

def timer_infinite(timer_expr: Time) -> z3.z3.BoolRef:

Return a formula expressing that the timer expression is infinite.

Formula expressing that the timer is infinite.

def timer_nonzero(timer_expr: Time) -> z3.z3.BoolRef:

Return a formula expressing that the timer expression is non-zero.

Formula expressing that the timer is non-zero.

def timer_decreasable(timer_expr: Time) -> z3.z3.BoolRef:

Return a formula expressing that the timer expression is decreasable (finite and non-zero).

Formula expressing that the timer is decreasable.