Index

_

__str__() (probably.pgcl.ast.DeclClass method) (probably.pgcl.ast.ExprClass method) (probably.pgcl.ast.InstrClass method) (probably.pgcl.ast.Program method) _bind_substs() (in module probably.pgcl.substitute)

_Binder (class in probably.pgcl.substitute) _doc_parser_grammar() (in module probably.pgcl.parser) _expand_region() (in module probably.pgcl.cfg) _join_regions() (in module probably.pgcl.cfg) _Region (class in probably.pgcl.cfg) _Subst (class in probably.pgcl.substitute)

A

add_block() (probably.pgcl.cfg._Region method) add_bound() (probably.pgcl.substitute._Subst method) add_variable() (probably.pgcl.ast.Program method) alloc() (probably.util.ref.Mut static method) AND (probably.pgcl.ast.Binop attribute)

apply() (probably.pgcl.substitute._Subst method) (probably.pgcl.wp.ExpectationTransformer method) AsgnInstr (class in probably.pgcl.ast) assignments (probably.pgcl.cfg.BasicBlock attribute) Assoc (class in probably.util.lark_expr_parser) atom() (in module probably.util.lark_expr_parser)

B

BasicBlock (class in probably.pgcl.cfg) BernoulliExpr (class in probably.pgcl.ast) bind() (probably.pgcl.substitute._Binder method) BinomialExpr (class in probably.pgcl.ast) Binop (class in probably.pgcl.ast) BinopExpr (class in probably.pgcl.ast) BlockType (class in probably.pgcl.cfg) body (probably.pgcl.ast.LoopInstr attribute) (probably.pgcl.ast.WhileInstr attribute) (probably.pgcl.wp.LoopExpectationTransformer attribute)

BOOLEAN (probably.pgcl.cfg.TerminatorKind attribute) BoolLitExpr (class in probably.pgcl.ast) BoolType (class in probably.pgcl.ast) Bounds (class in probably.pgcl.ast) bounds (probably.pgcl.ast.NatType attribute) branch() (probably.pgcl.cfg.Terminator static method) build_expr_parser() (in module probably.util.lark_expr_parser)

C

cast() (probably.pgcl.ast.ExprClass method) (probably.pgcl.ast.InstrClass method) CategoricalExpr (class in probably.pgcl.ast) check_expectation() (in module probably.pgcl.check) check_expression() (in module probably.pgcl.check) check_instr() (in module probably.pgcl.check) check_is_linear_expr() (in module probably.pgcl.syntax) check_is_linear_program() (in module probably.pgcl.syntax) check_is_one_big_loop() (in module probably.pgcl.syntax) check_program() (in module probably.pgcl.check) CheckFail (class in probably.pgcl.check) child() (probably.pgcl.cfg._Region static method) choice() (probably.pgcl.cfg.Terminator static method)

ChoiceInstr (class in probably.pgcl.ast) compile_expectation() (in module probably.pgcl.compiler) compile_expr() (in module probably.pgcl.compiler) compile_pgcl() (in module probably.pgcl.compiler) cond (probably.pgcl.ast.IfInstr attribute) (probably.pgcl.ast.ObserveInstr attribute) (probably.pgcl.ast.WhileInstr attribute) condition (probably.pgcl.cfg.Terminator attribute) constants (probably.pgcl.ast.Program attribute) ConstDecl (class in probably.pgcl.ast) ControlFlowGraph (class in probably.pgcl.cfg) copy() (probably.pgcl.substitute._Subst method) CUniformExpr (class in probably.pgcl.ast)

D

Decl (in module probably.pgcl.ast) declarations (probably.pgcl.ast.Program attribute) DeclClass (class in probably.pgcl.ast) dedup_list() (in module probably.util) dict_items() (probably.util.ref.Mut static method) dict_values() (probably.util.ref.Mut static method) DistrExpr (in module probably.pgcl.ast)

distribution() (probably.pgcl.ast.CategoricalExpr method) (probably.pgcl.ast.DUniformExpr method) DIVIDE (probably.pgcl.ast.Binop attribute) dominates_successor() (probably.pgcl.cfg._Region method) dominator_id (probably.pgcl.cfg._Region attribute) done (probably.pgcl.wp.LoopExpectationTransformer attribute) DUniformExpr (class in probably.pgcl.ast)

E

end (probably.pgcl.ast.CUniformExpr attribute) (probably.pgcl.ast.DUniformExpr attribute) entry_id (probably.pgcl.cfg.ControlFlowGraph attribute) (probably.pgcl.cfg.JumpTable attribute) EQ (probably.pgcl.ast.Binop attribute) error_id (probably.pgcl.cfg.JumpTable attribute) expectation (probably.pgcl.wp.ExpectationTransformer attribute) ExpectationInstr (class in probably.pgcl.ast) ExpectationTransformer (class in probably.pgcl.wp) expected_numeric_got() (probably.pgcl.check.CheckFail static method) expected_type_got() (probably.pgcl.check.CheckFail static method)

Expr (in module probably.pgcl.ast) expr (probably.pgcl.ast.ExpectationInstr attribute) (probably.pgcl.ast.OptimizationQuery attribute) (probably.pgcl.ast.ProbabilityQueryInstr attribute) (probably.pgcl.ast.SubstExpr attribute) (probably.pgcl.ast.TickExpr attribute) (probably.pgcl.ast.TickInstr attribute) (probably.pgcl.ast.UnopExpr attribute) expr_to_pysmt() (in module probably.pysmt.expr) ExprClass (class in probably.pgcl.ast) exprs (probably.pgcl.ast.CategoricalExpr attribute)

F

false (probably.pgcl.ast.IfInstr attribute) finalize() (probably.pgcl.cfg.JumpTable method) flatten() (probably.pgcl.ast.BinopExpr method) flip() (probably.pgcl.cfg.Terminator method) fmap() (probably.pgcl.check.CheckFail static method) FORWARD (probably.pgcl.cfg.BlockType attribute) fresh_block() (probably.pgcl.cfg.ControlFlowGraph method) from_instructions() (probably.pgcl.cfg.ControlFlowGraph static method) from_iverson() (probably.pgcl.simplify.SnfExpectationTransformer static method) (probably.pgcl.simplify.SnfExpectationTransformerProduct static method)

from_parse() (probably.pgcl.ast.Program static method) from_prob() (probably.pgcl.simplify.SnfExpectationTransformer static method) (probably.pgcl.simplify.SnfExpectationTransformerProduct static method) from_program() (probably.pysmt.context.TranslationContext static method) from_subst() (probably.pgcl.simplify.SnfExpectationTransformer static method) (probably.pgcl.simplify.SnfExpectationTransformerProduct static method) from_ticks() (probably.pgcl.simplify.SnfExpectationTransformer static method) (probably.pgcl.simplify.SnfExpectationTransformerProduct static method)

G

general_wp_transformer() (in module probably.pgcl.wp) GeometricExpr (class in probably.pgcl.ast) GEQ (probably.pgcl.ast.Binop attribute)

get_type() (in module probably.pgcl.check) goto() (probably.pgcl.cfg.Terminator static method) GT (probably.pgcl.ast.Binop attribute) guard (probably.pgcl.simplify.SnfExpectationTransformerProduct attribute)

I

id_subst (probably.pysmt.context.TranslationContext attribute) ident (probably.pgcl.cfg.BasicBlock attribute) if_false (probably.pgcl.cfg.Terminator attribute) if_true (probably.pgcl.cfg.Terminator attribute) IfInstr (class in probably.pgcl.ast) IidSampleExpr (class in probably.pgcl.ast) infinity (probably.pysmt.context.TranslationContext attribute) infinity() (probably.pgcl.ast.RealLitExpr static method) infixl() (in module probably.util.lark_expr_parser) infixr() (in module probably.util.lark_expr_parser) init (probably.pgcl.wp.LoopExpectationTransformer attribute) initial() (probably.pgcl.cfg._Region static method) INPUT probably command line option

Instr (in module probably.pgcl.ast) InstrClass (class in probably.pgcl.ast) instrs (probably.pgcl.cfg._Region attribute) instructions (probably.pgcl.ast.Program attribute) is_associative() (probably.pgcl.ast.Binop method) is_compatible() (in module probably.pgcl.check) is_goto() (probably.pgcl.cfg.Terminator method) is_infinite() (probably.pgcl.ast.RealLitExpr method) is_trap() (probably.pgcl.cfg.BasicBlock method) is_zero() (probably.pgcl.ast.TickExpr method) iterate() (probably.util.ref.Mut static method) iterations (probably.pgcl.ast.LoopInstr attribute) IVERSON (probably.pgcl.ast.Unop attribute)

J

JumpTable (class in probably.pgcl.cfg)

K

kind (probably.pgcl.cfg.Terminator attribute)

L

LEAF (probably.pgcl.cfg.Terminator attribute) LEFT (probably.util.lark_expr_parser.Assoc attribute) LEQ (probably.pgcl.ast.Binop attribute) lhs (probably.pgcl.ast.AsgnInstr attribute) (probably.pgcl.ast.BinopExpr attribute) (probably.pgcl.ast.ChoiceInstr attribute) list() (probably.util.ref.Mut static method) location (probably.pgcl.check.CheckFail attribute)

LogDistExpr (class in probably.pgcl.ast) lookup() (probably.pgcl.substitute._Binder method) LOOP_HEAD (probably.pgcl.cfg.BlockType attribute) LoopExpectationTransformer (class in probably.pgcl.wp) loopfree_wp() (in module probably.pgcl.wp) loopfree_wp_transformer() (in module probably.pgcl.wp) LoopInstr (class in probably.pgcl.ast) lower (probably.pgcl.ast.Bounds attribute) LT (probably.pgcl.ast.Binop attribute)

M

MAXIMIZE (probably.pgcl.ast.OptimizationType attribute) message (probably.pgcl.check.CheckFail attribute) MINIMIZE (probably.pgcl.ast.OptimizationType attribute) MINUS (probably.pgcl.ast.Binop attribute) module probably.cmd probably.pgcl probably.pgcl.ast probably.pgcl.cfg probably.pgcl.check probably.pgcl.compiler probably.pgcl.parser probably.pgcl.simplify probably.pgcl.substitute probably.pgcl.syntax probably.pgcl.walk probably.pgcl.wp probably.pysmt probably.pysmt.context probably.pysmt.expr probably.util probably.util.lark_expr_parser probably.util.ref

MODULO (probably.pgcl.ast.Binop attribute) Mut (class in probably.util.ref)

N

n (probably.pgcl.ast.BinomialExpr attribute) NatLitExpr (class in probably.pgcl.ast) NatType (class in probably.pgcl.ast)

NEG (probably.pgcl.ast.Unop attribute) Node (class in probably.pgcl.ast) normalize_expectation() (in module probably.pgcl.simplify) normalize_expectation_transformer() (in module probably.pgcl.simplify)

O

ObserveInstr (class in probably.pgcl.ast) one_big_loop() (in module probably.pgcl.cfg) one_loop_wp_transformer() (in module probably.pgcl.wp) operator (probably.pgcl.ast.BinopExpr attribute) (probably.pgcl.ast.UnopExpr attribute)

OperatorTable (in module probably.util.lark_expr_parser) OptimizationQuery (class in probably.pgcl.ast) OptimizationType (class in probably.pgcl.ast) OR (probably.pgcl.ast.Binop attribute)

P

p (probably.pgcl.ast.BinomialExpr attribute) param (probably.pgcl.ast.BernoulliExpr attribute) (probably.pgcl.ast.GeometricExpr attribute) (probably.pgcl.ast.LogDistExpr attribute) (probably.pgcl.ast.PoissonExpr attribute) parameter (probably.pgcl.ast.OptimizationQuery attribute) ParameterDecl (class in probably.pgcl.ast) parameters (probably.pgcl.ast.Program attribute) parse_expectation() (in module probably.pgcl.parser) parse_expr() (in module probably.pgcl.parser) parse_pgcl() (in module probably.pgcl.parser) PlotInstr (class in probably.pgcl.ast) PLUS (probably.pgcl.ast.Binop attribute) PoissonExpr (class in probably.pgcl.ast) postfix() (in module probably.util.lark_expr_parser) POWER (probably.pgcl.ast.Binop attribute) prefix() (in module probably.util.lark_expr_parser) PrintInstr (class in probably.pgcl.ast) prob (probably.pgcl.ast.ChoiceInstr attribute) (probably.pgcl.ast.PlotInstr attribute) (probably.pgcl.simplify.SnfExpectationTransformerProduct attribute) PROBABILISTIC (probably.pgcl.cfg.TerminatorKind attribute) ProbabilityQueryInstr (class in probably.pgcl.ast) probably command line option INPUT probably.cmd module probably.pgcl module probably.pgcl.ast module

probably.pgcl.cfg module probably.pgcl.check module probably.pgcl.compiler module probably.pgcl.parser module probably.pgcl.simplify module probably.pgcl.substitute module probably.pgcl.syntax module probably.pgcl.walk module probably.pgcl.wp module probably.pysmt module probably.pysmt.context module probably.pysmt.expr module probably.util module probably.util.lark_expr_parser module probably.util.ref module Program (class in probably.pgcl.ast) program_one_big_loop() (in module probably.pgcl.cfg)

Q

Query (in module probably.pgcl.ast)

R

read (probably.util.ref.Mut attribute) RealLitExpr (class in probably.pgcl.ast) RealType (class in probably.pgcl.ast) reduce() (probably.pgcl.ast.BinopExpr static method) reduce_cfg_to_instrs() (in module probably.pgcl.cfg) Ref (in module probably.util.ref)

render_dot() (probably.pgcl.cfg.ControlFlowGraph method) resolve() (probably.pgcl.substitute._Binder method) rhs (probably.pgcl.ast.AsgnInstr attribute) (probably.pgcl.ast.BinopExpr attribute) (probably.pgcl.ast.ChoiceInstr attribute) RIGHT (probably.util.lark_expr_parser.Assoc attribute)

S

sampling_dist (probably.pgcl.ast.IidSampleExpr attribute) simplifying_and() (in module probably.pgcl.simplify) simplifying_neg() (in module probably.pgcl.simplify) simplifying_plus() (in module probably.pgcl.simplify) simplifying_subst() (in module probably.pgcl.simplify) simplifying_times() (in module probably.pgcl.simplify) SkipInstr (class in probably.pgcl.ast) SnfExpectationTransformer (class in probably.pgcl.simplify) SnfExpectationTransformerProduct (class in probably.pgcl.simplify) start (probably.pgcl.ast.CUniformExpr attribute) (probably.pgcl.ast.DUniformExpr attribute) subst (probably.pgcl.ast.SubstExpr attribute) (probably.pgcl.simplify.SnfExpectationTransformerProduct attribute)

SubstExpr (class in probably.pgcl.ast) substitute() (probably.pgcl.cfg.ControlFlowGraph method) (probably.pgcl.cfg.Terminator method) (probably.pgcl.simplify.SnfExpectationTransformer method) (probably.pgcl.simplify.SnfExpectationTransformerProduct method) (probably.pgcl.wp.ExpectationTransformer method) substitute_constants() (in module probably.pgcl.substitute) substitute_constants_expr() (in module probably.pgcl.substitute) substitute_expr() (in module probably.pgcl.substitute) successor_id (probably.pgcl.cfg._Region attribute) successors (probably.pgcl.cfg.Terminator property)

T

term_count (probably.pgcl.ast.PlotInstr attribute) Terminator (class in probably.pgcl.cfg) terminator (probably.pgcl.cfg.BasicBlock attribute) TerminatorKind (class in probably.pgcl.cfg) TickExpr (class in probably.pgcl.ast) TickInstr (class in probably.pgcl.ast) ticks (probably.pgcl.simplify.SnfExpectationTransformerProduct attribute) TIMES (probably.pgcl.ast.Binop attribute) to_fraction() (probably.pgcl.ast.RealLitExpr method) to_networkx() (probably.pgcl.cfg.ControlFlowGraph method)

to_skeleton() (probably.pgcl.ast.Program method) TRAMPOLINE (probably.pgcl.cfg.BlockType attribute) trampoline() (probably.pgcl.cfg.JumpTable method) TranslationContext (class in probably.pysmt.context) true (probably.pgcl.ast.IfInstr attribute) typ (probably.pgcl.ast.ParameterDecl attribute) (probably.pgcl.ast.VarDecl attribute) (probably.pgcl.cfg.BasicBlock attribute) Type (in module probably.pgcl.ast) type (probably.pgcl.ast.OptimizationQuery attribute) TypeClass (class in probably.pgcl.ast)

U

Unop (class in probably.pgcl.ast)

UnopExpr (class in probably.pgcl.ast) upper (probably.pgcl.ast.Bounds attribute)

V

val (probably.util.ref.Mut property) value (probably.pgcl.ast.BoolLitExpr attribute) (probably.pgcl.ast.ConstDecl attribute) (probably.pgcl.ast.NatLitExpr attribute) (probably.pgcl.ast.RealLitExpr attribute) var (probably.pgcl.ast.ConstDecl attribute) (probably.pgcl.ast.ParameterDecl attribute) (probably.pgcl.ast.VarDecl attribute) (probably.pgcl.ast.VarExpr attribute)

var_1 (probably.pgcl.ast.PlotInstr attribute) var_2 (probably.pgcl.ast.PlotInstr attribute) VarDecl (class in probably.pgcl.ast) VarExpr (class in probably.pgcl.ast) variable (probably.pgcl.ast.IidSampleExpr attribute) (probably.pgcl.wp.ExpectationTransformer attribute) variables (probably.pgcl.ast.Program attribute) (probably.pysmt.context.TranslationContext attribute)

W

WhileInstr (class in probably.pgcl.ast)

wrap() (probably.util.ref.Mut static method) write (probably.util.ref.Mut attribute)