prodigy.pgcl.pgcl_operations

make_else_if(instructions)

Creates an else-if chain from a list of conditions and bodies for if-instructions

Parameters:

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

Return type:

IfInstr

state_to_equality_expression(state)

Parameters:

state (Dict[str, int])

Return type:

BinopExpr

cav_phi(program, invariant)

The characteristic loop functional. It unrolls a loop exactly once.

The result is if (G) { B; I } else { skip } for a program while (G) { B } and an invariant program I. Declarations, constants, parameters and functions are taken from the invariant. The instructions are copied, so the result shares no nodes with its inputs.

Parameters:

• program (Program)

• invariant (Program)

Return type:

Program