prodigy.analysis.lowerbounds.explicit

Explicit-state semantics of loop-free statements of the intermediate representation, on measures given as dicts state tuple -> weight (exact fractions.Fraction or float), and a sparse Kleene iteration for loops. Used to validate the generating-function calculus, to choose template parameters, and as the unrolling baseline.

run_state(stmt, state, w, out, variables, geo_cut=400)[source]

Execute stmt from a single state with weight w and add the output sub-measure to out.

Parameters:
apply(stmt, measure, variables, geo_cut=400)[source]

Forward semantics of a loop-free statement on an explicit measure.

Parameters:
Return type:

Dict[Tuple[int, ...], Any]

class Kernel(guard, body, variables, exact=False)[source]

Bases: object

The transition kernel of a loop ("loop", guard, body): step(s) is None if the guard is false in s and the list of successor states with probabilities otherwise (cached).

Parameters:
step(s)[source]
Parameters:

s (Tuple[int, ...])

class Exploration(init, guard, body, variables, box=None, max_states=2000000)[source]

Bases: object

Sparse floating-point Kleene iteration of the occupation measure of a loop, restricted to a box.

After run(n): occupation approximates the occupation measure on the box (sum of the first n iterates), exit the output measure of the runs that terminated within n iterations, remaining the mass still inside the loop, and leaked the mass that left the box (it is dropped).

Parameters:
property remaining: float
run(n, tol=0.0, max_work=None, time_limit=None)[source]

Perform up to n iterations; stop early when the mass inside the loop drops to tol, after max_work state expansions, or after time_limit seconds.

Parameters:
reachable(init_states, guard, body, variables, box, limit=1000000)[source]

States reachable from init_states without leaving box (support only, no weights).

Parameters:
Return type:

set