prodigy.analysis.lowerbounds.problem

A single-loop program split into the parts used by the lower-bound modes: the loop-free prefix (which determines the initial measure g of the loop), the loop, and the loop-free epilogue with its queries.

class Query(kind, expr, text)[source]

Bases: object

Parameters:
kind: str
expr: tuple
text: str
class LoopProblem(variables, prefix, guard, body, epilogue, queries=list(), forced_rates=dict(), initial_state=None, init_form=None)[source]

Bases: object

Parameters:
variables: List[str]
prefix: tuple
guard: tuple
body: tuple
epilogue: tuple
queries: List[Query]
forced_rates: Dict[str, Tuple[Fraction, int]]
initial_state: Tuple[int, ...] | None = None
init_form: tuple | None = None
property d: int
initial_measure(cap=400)[source]

The initial measure g of the loop as an explicit measure (exact; infinite tails are truncated after cap values per variable).

Parameters:

cap (int)

Return type:

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

describe()[source]
Return type:

str

load_problem(program)[source]

Split a program with exactly one top-level loop (and no nested loops) into a LoopProblem.

Parameters:

program (Program)

Return type:

LoopProblem

queries_after(program, loop)[source]

The ?Pr and ?Ex queries that directly follow loop at the top level of program (!Plot and !Print are skipped; any other instruction ends the list). Marginal queries ?Pr[x] and queries outside the supported expressions are left out.

Parameters:

  • program (Program)

  • loop (WhileInstr)

Return type:

List[Query]

problem_from_loop(loop, variables, init_expr)[source]

A LoopProblem for a loop whose input distribution is given as a generating function (used by the interactive modes of the while handler).

Parameters:

  • loop (WhileInstr)

  • variables (List[str])

  • init_expr (str)

Return type:

LoopProblem