prodigy.analysis.lowerbounds.ir

Translation of pGCL programs (the AST of prodigy.pgcl) into the small intermediate representation used by the exact generating-function calculus of prodigy.analysis.lowerbounds.egcalc.

Statements:

("seq", [stmt, ...]) | ("skip",) | ("abort",) | ("observe", cond)
("choice", prob, stmt, stmt) | ("if", cond, stmt, stmt) | ("assign", var, expr)

Expressions:

("num", Fraction) | ("var", name) | ("add"|"sub"|"mul"|"div"|"mod", e, e)
("call", name, [e, ...]) | ("cmp", op, e, e) | ("and"|"or", e, e) | ("not", e)
("true",) | ("false",)

abort is interpreted as divergence, i.e. its forward semantics maps every measure to the zero measure (the run never terminates), which is the semantics of diverge in the paper.

exception UnsupportedProgram[source]

Bases: Exception

The program (or loop) is outside the fragment supported by the exact template calculus.

expr_to_ir(expr)[source]

Translate a pGCL expression.

Return type:

tuple

instr_to_ir(instr)[source]

Translate a pGCL instruction or a list of instructions.

Parameters:

instr (SkipInstr | AbortInstr | WhileInstr | IfInstr | AsgnInstr | ChoiceInstr | LoopInstr | TickInstr | ObserveInstr | QueryInstr | ProbabilityQueryInstr | ExpectationInstr | PlotInstr | PrintInstr | OptimizationQuery | Sequence[SkipInstr | AbortInstr | WhileInstr | IfInstr | AsgnInstr | ChoiceInstr | LoopInstr | TickInstr | ObserveInstr | QueryInstr | ProbabilityQueryInstr | ExpectationInstr | PlotInstr | PrintInstr | OptimizationQuery])

Return type:

tuple

eval_number(e)[source]

Evaluate a closed arithmetic expression (e.g. a probability such as 1/3) to a fraction.

Parameters:

e (tuple)

Return type:

Fraction

split_program(program)[source]

Split a program into the loop-free prefix, the (single, top-level) loop, and the instructions after it.

Parameters:

program (Program)

Return type:

Tuple[List[SkipInstr | AbortInstr | WhileInstr | IfInstr | AsgnInstr | ChoiceInstr | LoopInstr | TickInstr | ObserveInstr | QueryInstr | ProbabilityQueryInstr | ExpectationInstr | PlotInstr | PrintInstr | OptimizationQuery], WhileInstr, List[SkipInstr | AbortInstr | WhileInstr | IfInstr | AsgnInstr | ChoiceInstr | LoopInstr | TickInstr | ObserveInstr | QueryInstr | ProbabilityQueryInstr | ExpectationInstr | PlotInstr | PrintInstr | OptimizationQuery]]

queries_of(instructions)[source]

The ?Pr[...] and ?Ex[...] queries among the given instructions as (kind, expression, text).

Parameters:

instructions (Sequence[SkipInstr | AbortInstr | WhileInstr | IfInstr | AsgnInstr | ChoiceInstr | LoopInstr | TickInstr | ObserveInstr | QueryInstr | ProbabilityQueryInstr | ExpectationInstr | PlotInstr | PrintInstr | OptimizationQuery])

Return type:

List[Tuple[str, tuple, str]]

eval_expr(e, state)[source]

Evaluate an IR expression in a concrete state (used by the explicit-state reference semantics).

Parameters: