Index

Symbols

--allowed-host prodigy-web command line option --coefficients prodigy-analyze command line option --compute-exact prodigy-independent_vars command line option --decisions prodigy-analyze command line option --engine prodigy command line option --examples prodigy-web command line option --host prodigy-web command line option --intermediate-results prodigy command line option --invariant prodigy-evt_lower_bound command line option prodigy-invariant_synthesis command line option --json prodigy-analyze command line option prodigy-evt_sandwich command line option prodigy-loop_strategies command line option prodigy-outline command line option --loop prodigy-analyze command line option prodigy-main command line option --lower prodigy-evt_sandwich command line option --max-jobs prodigy-web command line option --memory-limit prodigy-web command line option --no-browser prodigy-web command line option --no-normalize prodigy command line option --no-per-query prodigy-evt_sandwich command line option

--no-simplification prodigy command line option --no-upper prodigy-evt_sandwich command line option --objective prodigy-evt_sandwich command line option --output prodigy-analyze command line option --per-query prodigy-evt_sandwich command line option --port prodigy-web command line option --pos-heuristic prodigy command line option --show-all-invs prodigy command line option --show-certificates prodigy-evt_sandwich command line option --show-input-program prodigy-main command line option --size prodigy-evt_sandwich command line option --solver prodigy command line option --steps prodigy-analyze command line option --stepwise prodigy command line option --strategy prodigy command line option --template-heuristic prodigy command line option --time-limit prodigy-web command line option --upper prodigy-evt_sandwich command line option --use-latex prodigy command line option

A

activate() (AnalysisSession method) add_message() (LoopRecord method) AIConfigurationError AIRequestError alias_of (ParamSpec attribute) ALL (Bound attribute) alloc() (Mut static method) AllOrPartialRational (class in prodigy.analysis.evtinvariants.heuristics.strategies) AnalysisResult (class in prodigy.analysis.result) AnalysisSession (class in prodigy.analysis.session) Analyzer (in module prodigy.analysis.evtinvariants.invariant_verification) analyzer (LoopTask attribute) AND (PositivityHeuristics attribute) AndHeuristic (class in prodigy.analysis.evtinvariants.heuristics.positivity.logical) APART_OR_TOGETHER (SynthesisStrategies attribute) apply() (in module prodigy.analysis.lowerbounds.explicit) approximate() (Distribution method) (FPS method) (GeneratingFunction method) (SymengineDist method)

approximate_unilaterally() (Distribution method) (FPS method) (GeneratingFunction method) (SymengineDist method) approximate_until_finite() (Distribution method) args (Example attribute) ask (Provider attribute) ask_param() (AnalysisSession method) (DecisionProvider method) (FixedDecisions method) (InteractiveDecisions method) assign() (GFCalculus method) AssignmentHandler (class in prodigy.analysis.instructionhandler.assignment_handler) Assoc (class in prodigy.pgcl.util.lark_expr_parser) atom() (in module prodigy.pgcl.util.lark_expr_parser) attempts (SandwichResult attribute)

B

basis_num (TemplateLP attribute) bernoulli() (CommonDistributionsFactory static method) (ProdigyPGF static method) (SymenginePGF static method) (SympyPGF static method) binomial() (CommonDistributionsFactory static method) (ProdigyPGF static method) (SymenginePGF static method) (SympyPGF static method) BLACK (Style attribute) BLUE (Style attribute)

body (LoopProblem attribute) Bound (class in prodigy.analysis.loop_strategies) bound (QueryResult attribute) bound_kind (AnalysisSession property) bounds (AnalysisResult attribute) (SandwichResult attribute) bounds_explanation() (in module prodigy.analysis.result) build_dependence_graph() (in module prodigy.analysis.independence.independence) build_expr_parser() (in module prodigy.pgcl.util.lark_expr_parser) build_result() (in module prodigy.analysis.result) BusyError

C

calc (Certificate attribute) cancel() (JobManager method) candidate_from_answer() (in module prodigy.analysis.ai_candidates) CandidateError category (Example attribute) cav_phi() (in module prodigy.pgcl.pgcl_operations) Certificate (class in prodigy.analysis.lowerbounds.synthesis) certificate (LoopOutcome attribute) certificate() (TemplateLP method) certificates (LoopRecord attribute) check() (TemplateLP method) check_equivalence() (in module prodigy.analysis.equivalence.equivalence_check) check_expectation() (in module prodigy.pgcl.check) check_expression() (in module prodigy.pgcl.check) check_function() (in module prodigy.pgcl.check) check_instr() (in module prodigy.pgcl.check) check_is_constant_constraint() (in module prodigy.pgcl.pgcl_checks) check_is_modulus_condition() (in module prodigy.pgcl.pgcl_checks) check_program() (in module prodigy.pgcl.check) check_source() (in module prodigy.web.diagnostics) CheckFail (class in prodigy.pgcl.check) choices (ParamSpec attribute) choose_candidate() (DecisionProvider method) CLEARTOEND (Style attribute) coefficient() (GFCalculus method) coefficient_sum() (GeneratingFunction method) (SymengineDist method) coeffs_along() (GFCalculus method) collect_details (AnalysisSession property) column (LoopInfo attribute) (QueryResult attribute) column_scales() (TemplateLP method) combine() (Bound static method) command (Example attribute) CommonDistributionsFactory (class in prodigy.distribution.distribution) compile_expectation() (in module prodigy.pgcl.compiler)

compile_expr() (in module prodigy.pgcl.compiler) compile_pgcl() (in module prodigy.pgcl.compiler) compute() (AssignmentHandler static method) (FunctionHandler static method) (InstructionHandler static method) (ITEHandler static method) (LoopHandler static method) (ObserveHandler static method) (PChoiceHandler static method) (QueryBlockHandler static method) (QueryHandler static method) (SampleHandler static method) (WhileHandler static method) compute_discrete_distribution() (in module prodigy.analysis.analyzer) compute_hadamard_product() (in module prodigy.util) compute_semantics() (in module prodigy.analysis.analyzer) cond (LoopInfo attribute) (LoopRecord attribute) condition_distribution() (in module prodigy.analysis.analyzer) config (LoopTask attribute) ConfigurationError conn (Job attribute) constant_value() (in module prodigy.distribution.distribution) continue_plot() (DecisionProvider method) (InteractiveDecisions method) copy() (Distribution method) (FPS method) (GeneratingFunction method) (State method) (SymengineDist method) create() (PositivityHeuristics static method) (TemplateHeuristics static method) create_app() (in module prodigy.web.app) created (Job attribute) current_session() (in module prodigy.analysis.session) CYAN (Style attribute)

D

d (LoopProblem property) data (QueryResult attribute) decay_rate() (in module prodigy.analysis.lowerbounds.parameters) decide_loop() (AnalysisSession method) decide_nonneg() (in module prodigy.analysis.lowerbounds.subinvariant) decision (LoopTask attribute) DecisionProvider (class in prodigy.analysis.session) DecisionRequired decisions (DecisionProvider attribute) decrement() (GFCalculus method) dedup_list() (in module prodigy.pgcl.util) (in module prodigy.util) default (ParamSpec attribute) DEFAULT (PositivityHeuristics attribute) (SynthesisStrategies attribute) (TemplateHeuristics attribute) default_examples_dir() (in module prodigy.web.examples) DEFAULT_KEY (in module prodigy.analysis.session) default_monomial_iterator() (in module prodigy.util.order) DefaultStrategy (class in prodigy.analysis.evtinvariants.heuristics.strategies) defect_mass() (GFCalculus method) degrees() (in module prodigy.analysis.lowerbounds.egcalc) den (Certificate property)

Denominator (class in prodigy.analysis.lowerbounds.egcalc) depth (LoopInfo attribute) describe() (LoopInfo method) (LoopProblem method) (TemplateShape method) describe_distribution() (in module prodigy.analysis.result) description (LoopStrategy attribute) detached() (AnalysisSession class method) diagnostics (Provider attribute) dict_items() (Mut static method) dict_values() (Mut static method) directed_decimal() (in module prodigy.analysis.lowerbounds.egcalc) dist_factory (AllOrPartialRational attribute) (DefaultStrategy attribute) (FinitePolynomial attribute) (InfinitePolynomial attribute) (PartialRational attribute) distribution (AnalysisResult attribute) Distribution (class in prodigy.distribution.distribution) distribution (LoopOutcome attribute) (LoopTask attribute) DistributionParameterError divide_exponents() (in module prodigy.distribution.exact_division) DominantRootHeuristic (class in prodigy.analysis.evtinvariants.heuristics.positivity.dominat_root_rejection)

E

elapsed (Job property) eliminate() (GFCalculus method) engine (ForwardAnalysisConfig attribute) epilogue (LoopProblem attribute) error (AnalysisResult attribute) error_prob (LoopOutcome attribute) (LoopTask attribute) error_probability (AnalysisResult attribute) error_probability_float (AnalysisResult attribute) eval_expr() (in module prodigy.analysis.lowerbounds.ir) eval_number() (in module prodigy.analysis.lowerbounds.ir) evaluate() (Distribution static method) (FPS static method) (GeneratingFunction static method) (SymengineDist static method) evaluate_condition() (Distribution class method) (GeneratingFunction class method) evaluate_expression() (Distribution method) evt_invariant_check() (in module prodigy.analysis.evtinvariants.invariant_verification) evt_invariant_synthesis() (in module prodigy.analysis.evtinvariants.invariant_synthesis) evt_invariant_verification() (in module prodigy.analysis.evtinvariants.invariant_verification) evt_sandwich() (in module prodigy.analysis.lowerbounds.sandwich) evt_subinvariant_verification() (in module prodigy.analysis.lowerbounds.subinvariant)

EXACT (Bound attribute) exact_and_float() (in module prodigy.analysis.result) exact_mass() (in module prodigy.analysis.lowerbounds.subinvariant) Example (class in prodigy.web.examples) ExampleLibrary (class in prodigy.web.examples) examples (ExampleLibrary property) EXCLUDE (MarginalType attribute) exit_box_functional() (TemplateLP method) exit_functional() (TemplateLP method) exit_mass (Certificate attribute) exit_numerator (Certificate attribute) exit_unbounded (VariableProfile attribute) expand() (GFCalculus method) expected_numeric_got() (CheckFail static method) expected_type_got() (CheckFail static method) Exploration (class in prodigy.analysis.lowerbounds.explicit) exploration (ParameterPlan attribute) expr (Query attribute) (QueryResult attribute) expr_to_ir() (in module prodigy.analysis.lowerbounds.ir) expr_to_pysmt() (in module prodigy.pgcl.pysmt.expr) extend() (State method) extra (Certificate attribute)

F

factor() (Denominator method) factory (ForwardAnalysisConfig property) factory() (Distribution static method) (FPS static method) (GeneratingFunction static method) (SymengineDist static method) failed (LoopRecord attribute) FALSE (SolverType attribute) filter() (Distribution method) (GeneratingFunction method) (SymengineDist method) filter_state() (Distribution method) FIN_POLY (SynthesisStrategies attribute) find_nested_inference() (in module prodigy.pgcl.pgcl_checks) finish_query() (in module prodigy.analysis.result) finished (Job attribute) finite_mass() (in module prodigy.analysis.instructionhandler.while_handler) FinitePolynomial (class in prodigy.analysis.evtinvariants.heuristics.strategies)

FinitePolynomialPositivity (class in prodigy.analysis.evtinvariants.heuristics.positivity.polynomial_positivity) first_negative() (GFCalculus method) FixedDecisions (class in prodigy.analysis.session) fmap() (CheckFail static method) forced_rates (LoopProblem attribute) ForwardAnalysisConfig (class in prodigy.analysis.config) ForwardAnalysisConfig.Engine (class in prodigy.analysis.config) ForwardAnalysisError FPS (class in prodigy.distribution.fast_generating_function) from_dist() (FPS class method) from_expr() (CommonDistributionsFactory static method) (ProdigyPGF static method) (SymenginePGF static method) (SympyPGF static method) FROM_HEURISTICS (SynthesisStrategies attribute) from_json() (LoopDecision static method) from_program() (TranslationContext static method) function (LoopInfo attribute) FunctionHandler (class in prodigy.analysis.instructionhandler.function_handler)

G

generate() (PolynomialEnumeration method) (RationalFunctionMaxDeg method) (TemplateHeuristic method) generate_equivalence_test_distribution() (in module prodigy.analysis.equivalence.equivalence_check) GeneratingFunction (class in prodigy.distribution.generating_function) geometric() (CommonDistributionsFactory static method) (ProdigyPGF static method) (SymenginePGF static method) (SympyPGF static method) get() (JobManager method) get_expected_value_of() (Distribution method) (FPS method) (GeneratingFunction method) (SymengineDist method) get_fresh_variable() (Distribution method) (FPS method) (GeneratingFunction method) (SymengineDist method) get_loop_strategy() (in module prodigy.analysis.loop_strategies) get_parameters() (Distribution method) (FPS method) (GeneratingFunction method) (SymengineDist method)

get_prob_by_diff() (SymengineDist method) get_prob_by_series() (SymengineDist method) get_probability_mass() (Distribution method) (FPS method) (GeneratingFunction method) (SymengineDist method) get_probability_of() (Distribution method) get_provider() (in module prodigy.analysis.ai_candidates) get_state() (Distribution method) get_symbols() (Distribution method) (FPS method) (GeneratingFunction method) get_type() (in module prodigy.pgcl.check) get_variables() (Distribution method) (FPS method) (GeneratingFunction method) (SymengineDist method) GFCalculus (class in prodigy.analysis.lowerbounds.egcalc) GFOptimizer (class in prodigy.analysis.optimization.gf_optimizer) GINAC (ForwardAnalysisConfig.Engine attribute) GREEN (Style attribute) group (TemplateShape attribute) guard (LoopProblem attribute)

H

hadamard_product() (Distribution method) (FPS method) (GeneratingFunction method) (SymengineDist method)

has_variable() (in module prodigy.pgcl.pgcl_checks) help (ParamSpec attribute) HeuristicsError

I

id (Example attribute) (Job attribute) (LoopInfo attribute) id_subst (TranslationContext attribute) INCLUDE (MarginalType attribute) independent_vars() (in module prodigy.analysis.independence.independence) independents_vars (ProgramInfo attribute) index (QueryResult attribute) INDIVIDUAL_SUM (PositivityHeuristics attribute) INF_POLY (SynthesisStrategies attribute) InfinitePolynomial (class in prodigy.analysis.evtinvariants.heuristics.strategies) infinity (TranslationContext attribute) infixl() (in module prodigy.pgcl.util.lark_expr_parser) infixr() (in module prodigy.pgcl.util.lark_expr_parser) init_form (LoopProblem attribute) initial_measure() (LoopProblem method) initial_state (LoopProblem attribute) input (AnalysisResult attribute) INPUT_DIST prodigy-analyze command line option prodigy-evt_lower_bound command line option prodigy-invariant_synthesis command line option prodigy-main command line option inside_checks (LoopRecord attribute) instr_to_ir() (in module prodigy.analysis.lowerbounds.ir) instruction (LoopTask attribute)

InstructionHandler (class in prodigy.analysis.instructionhandler.instruction_handler) interactive (DecisionProvider attribute) (FixedDecisions attribute) (InteractiveDecisions attribute) (LoopTask property) interactive() (AnalysisSession class method) InteractiveDecisions (class in prodigy.analysis.session) InvariantRefutedError invocations (LoopRecord attribute) is_compatible() (in module prodigy.pgcl.check) is_finite() (Distribution method) (FPS method) (GeneratingFunction method) (SymengineDist method) is_monotone_nonnegative() (in module prodigy.analysis.result) is_nonneg() (GFCalculus method) is_positive() (PositivityHeuristic method) is_zero_dist() (Distribution method) (FPS method) (GeneratingFunction method) (SymengineDist method) ITEHandler (class in prodigy.analysis.instructionhandler.ite_handler) items() (State method) iter_with() (SymengineDist method) iterate() (Mut static method) ITERATE_TERMS (PositivityHeuristics attribute) IterateTermsHeuristic (class in prodigy.analysis.evtinvariants.heuristics.positivity.iterate_terms)

J

Job (class in prodigy.web.jobs)

JobManager (class in prodigy.web.jobs) joint_table() (in module prodigy.analysis.result)

K

Kernel (class in prodigy.analysis.lowerbounds.explicit) kind (Certificate attribute) (LoopOutcome attribute) (LoopRecord attribute) (ParamSpec attribute) (Query attribute) (QueryResult attribute) (VariableProfile attribute)

known_issue (Example attribute)

L

label (ParamSpec attribute) LEFT (Assoc attribute) legacy_key (LoopStrategy attribute) line (LoopInfo attribute) (QueryResult attribute) LinearForm (in module prodigy.distribution.linear_guards) list() (ExampleLibrary method) (Mut static method) load() (ExampleLibrary method) load_problem() (in module prodigy.analysis.lowerbounds.problem) location (CheckFail attribute) log (AnalysisResult attribute) (Job attribute) log() (CommonDistributionsFactory static method) (ProdigyPGF static method) (SymenginePGF static method) (SympyPGF static method) log_dropped (Job attribute) log_radius() (TailKernel method) log_setup() (in module prodigy.util.logger) logger (DominantRootHeuristic attribute) (FinitePolynomialPositivity attribute) (MockFalseSolver attribute) (MockNoneSolver attribute) (MockTrueSolver attribute) (RationalFunctionDenomSign attribute) (SingleRationalFunction attribute) (SMTZ3Solver attribute) (SumPositivity attribute) (SympySolver attribute)

lookup() (LoopRegistry method) loop (LoopRecord attribute) (LoopTask attribute) loop_decision() (DecisionProvider method) (FixedDecisions method) (InteractiveDecisions method) loop_query_bounds() (AnalysisSession method) loop_records (AnalysisSession attribute) loop_strategies() (in module prodigy.analysis.loop_strategies) LoopDecision (class in prodigy.analysis.session) LoopHandler (class in prodigy.analysis.instructionhandler.loop_handler) LoopInfo (class in prodigy.analysis.session) LoopOutcome (class in prodigy.analysis.loop_strategies) LoopProblem (class in prodigy.analysis.lowerbounds.problem) LoopRecord (class in prodigy.analysis.session) LoopRegistry (class in prodigy.analysis.session) loops (AnalysisResult attribute) (LoopRegistry attribute) LoopStrategy (class in prodigy.analysis.loop_strategies) LoopTask (class in prodigy.analysis.loop_strategies) LOWER (Bound attribute) lower (ParameterPlan attribute) (QueryBound attribute) (QueryResult attribute) (SandwichResult attribute) lower_float (QueryResult attribute)

M

MAGENTA (Style attribute) make() (SolverType static method) (SynthesisStrategies class method) make_config() (in module prodigy.web.requests) make_else_if() (in module prodigy.pgcl.pgcl_operations) make_interval() (in module prodigy.analysis.result) make_poly_clause() (in module prodigy.util) margin (Certificate attribute) margin_used (TemplateLP attribute) marginal() (Distribution method) (FPS method) (GeneratingFunction method) (SymengineDist method) MarginalType (class in prodigy.distribution.distribution) mass() (GFCalculus method) mass_bounds (SandwichResult attribute) matrix() (TailKernel method) max_deg (FinitePolynomial attribute) max_degree (AllOrPartialRational attribute) (DefaultStrategy attribute) (PartialRational attribute) MAX_MESSAGES (LoopRecord attribute) max_value (VariableProfile attribute) menu_text (LoopStrategy attribute) message (CheckFail attribute) messages (LoopOutcome attribute) (LoopRecord attribute) minimum (ParamSpec attribute) MIXED_RAT_FUNC (PositivityHeuristics attribute) MockFalseSolver (class in prodigy.analysis.solver.mock_solver) MockNoneSolver (class in prodigy.analysis.solver.mock_solver) MockTrueSolver (class in prodigy.analysis.solver.mock_solver) model (Provider attribute) module prodigy prodigy.analysis prodigy.analysis.ai_candidates prodigy.analysis.analyzer prodigy.analysis.config prodigy.analysis.equivalence prodigy.analysis.equivalence.equivalence_check prodigy.analysis.evtinvariants prodigy.analysis.evtinvariants.heuristics prodigy.analysis.evtinvariants.heuristics.positivity prodigy.analysis.evtinvariants.heuristics.positivity.dominat_root_rejection prodigy.analysis.evtinvariants.heuristics.positivity.heuristics_factory prodigy.analysis.evtinvariants.heuristics.positivity.individual_sum_terms prodigy.analysis.evtinvariants.heuristics.positivity.iterate_terms prodigy.analysis.evtinvariants.heuristics.positivity.logical prodigy.analysis.evtinvariants.heuristics.positivity.polynomial_positivity prodigy.analysis.evtinvariants.heuristics.positivity.positivity prodigy.analysis.evtinvariants.heuristics.positivity.rational_function prodigy.analysis.evtinvariants.heuristics.strategies prodigy.analysis.evtinvariants.heuristics.templates prodigy.analysis.evtinvariants.heuristics.templates.polynomial_function prodigy.analysis.evtinvariants.heuristics.templates.rational_function prodigy.analysis.evtinvariants.heuristics.templates.templates prodigy.analysis.evtinvariants.heuristics.templates.templates_factory prodigy.analysis.evtinvariants.invariant_synthesis prodigy.analysis.evtinvariants.invariant_verification prodigy.analysis.exceptions prodigy.analysis.independence prodigy.analysis.independence.independence prodigy.analysis.independence.utils prodigy.analysis.instructionhandler prodigy.analysis.instructionhandler.assignment_handler prodigy.analysis.instructionhandler.function_handler prodigy.analysis.instructionhandler.instruction_handler prodigy.analysis.instructionhandler.ite_handler prodigy.analysis.instructionhandler.loop_handler prodigy.analysis.instructionhandler.observe_handler prodigy.analysis.instructionhandler.probchoice_handler prodigy.analysis.instructionhandler.program_info prodigy.analysis.instructionhandler.query_handler prodigy.analysis.instructionhandler.queryblock_handler prodigy.analysis.instructionhandler.sample_handler prodigy.analysis.instructionhandler.while_handler prodigy.analysis.loop_strategies prodigy.analysis.lowerbounds prodigy.analysis.lowerbounds.egcalc prodigy.analysis.lowerbounds.explicit prodigy.analysis.lowerbounds.ir prodigy.analysis.lowerbounds.parameters prodigy.analysis.lowerbounds.problem prodigy.analysis.lowerbounds.sandwich prodigy.analysis.lowerbounds.subinvariant prodigy.analysis.lowerbounds.synthesis prodigy.analysis.optimization prodigy.analysis.optimization.gf_optimizer prodigy.analysis.optimization.optimizer prodigy.analysis.result prodigy.analysis.session prodigy.analysis.solver prodigy.analysis.solver.mock_solver prodigy.analysis.solver.smtz3_solver prodigy.analysis.solver.solver prodigy.analysis.solver.solver_type prodigy.analysis.solver.sympy_solver prodigy.cli prodigy.distribution prodigy.distribution.distribution prodigy.distribution.exact_division prodigy.distribution.fast_generating_function prodigy.distribution.generating_function prodigy.distribution.linear_guards prodigy.distribution.symengine_distribution prodigy.pgcl prodigy.pgcl.ast prodigy.pgcl.check prodigy.pgcl.compiler prodigy.pgcl.parser prodigy.pgcl.pgcl_checks prodigy.pgcl.pgcl_operations prodigy.pgcl.pysmt prodigy.pgcl.pysmt.context prodigy.pgcl.pysmt.expr prodigy.pgcl.substitute prodigy.pgcl.util prodigy.pgcl.util.lark_expr_parser prodigy.pgcl.util.ref prodigy.util prodigy.util.color prodigy.util.logger prodigy.util.order prodigy.util.plotter prodigy.web prodigy.web.app prodigy.web.diagnostics prodigy.web.examples prodigy.web.jobs prodigy.web.requests

moment() (GFCalculus method) monomial() (in module prodigy.analysis.lowerbounds.egcalc) Mut (class in prodigy.pgcl.util.ref)

N

name (LoopStrategy attribute) (ParamSpec attribute) (Provider attribute) (VariableProfile attribute) next_query_position() (AnalysisSession method) next_step() (DecisionProvider method) (InteractiveDecisions method) nice_rate() (in module prodigy.analysis.lowerbounds.parameters) NONE (SolverType attribute) nonneg_by_construction() (in module prodigy.analysis.lowerbounds.subinvariant) normalize (ForwardAnalysisConfig attribute)

normalize() (Distribution method) (FPS method) (GeneratingFunction method) (SymengineDist method) normalize_guard() (in module prodigy.distribution.linear_guards) NOT (PositivityHeuristics attribute) note (QueryResult attribute) note() (AnalysisSession method) (LoopTask method) NotHeuristic (class in prodigy.analysis.evtinvariants.heuristics.positivity.logical) numerator (Certificate attribute) numerator() (TemplateLP method)

O

ObserveHandler (class in prodigy.analysis.instructionhandler.observe_handler) ObserveZeroEventError OKBLUE (Style attribute) OKCYAN (Style attribute) OKGREEN (Style attribute) OKMAGENTA (Style attribute) OKRED (Style attribute) OKWHITE (Style attribute) OKYELLOW (Style attribute) old_update() (FPS method) on_instruction() (AnalysisSession method) on_normalize() (AnalysisSession method) one() (CommonDistributionsFactory static method) (ProdigyPGF static method) (SymenginePGF static method) (SympyPGF static method)

OperatorTable (in module prodigy.pgcl.util.lark_expr_parser) optimize() (GFOptimizer static method) (Optimizer static method) Optimizer (class in prodigy.analysis.optimization.optimizer) optimizer (ForwardAnalysisConfig property) optional (ParamSpec attribute) OR (PositivityHeuristics attribute) OrHeuristic (class in prodigy.analysis.evtinvariants.heuristics.positivity.logical) OTHER_PROGRAM_FILE prodigy-check_equality command line option outline_program() (in module prodigy.analysis.result)

P

padd() (in module prodigy.analysis.lowerbounds.egcalc) param() (LoopStrategy method) (LoopTask method) ParameterPlan (class in prodigy.analysis.lowerbounds.parameters) params (LoopDecision attribute) (LoopRecord attribute) (LoopStrategy attribute) ParamSpec (class in prodigy.analysis.loop_strategies) parse() (ParamSpec method) parse_decisions() (in module prodigy.analysis.session) parse_expectation() (in module prodigy.pgcl.parser) parse_expr() (in module prodigy.pgcl.parser) parse_pgcl() (in module prodigy.pgcl.parser) parse_spec() (LoopDecision static method) PartialRational (class in prodigy.analysis.evtinvariants.heuristics.strategies) PChoiceHandler (class in prodigy.analysis.instructionhandler.probchoice_handler) per_query (SandwichResult attribute) period (VariableProfile attribute) periods (TemplateShape attribute) phases (TailKernel attribute) plan (SandwichResult attribute) plan_parameters() (in module prodigy.analysis.lowerbounds.parameters) plot() (Plotter static method) Plotter (class in prodigy.util.plotter) pmul() (in module prodigy.analysis.lowerbounds.egcalc) poisson() (CommonDistributionsFactory static method) (ProdigyPGF static method) (SymenginePGF static method) (SympyPGF static method) POLY (TemplateHeuristics attribute) poly() (Denominator method) POLYNOMIAL (PositivityHeuristics attribute) PolynomialEnumeration (class in prodigy.analysis.evtinvariants.heuristics.templates.polynomial_function) positivity_box() (GFCalculus method) positivity_heuristic (ForwardAnalysisConfig attribute) positivity_heuristics (SynthesisStrategy attribute) PositivityHeuristic (class in prodigy.analysis.evtinvariants.heuristics.positivity.positivity) PositivityHeuristics (class in prodigy.analysis.evtinvariants.heuristics.positivity.heuristics_factory) postfix() (in module prodigy.pgcl.util.lark_expr_parser) prefix (LoopProblem attribute) prefix() (in module prodigy.pgcl.util.lark_expr_parser) preset() (DecisionProvider method) print_progress_bar() (in module prodigy.util.logger) print_result() (in module prodigy.analysis.lowerbounds.sandwich) problem (SandwichResult attribute) problem_from_loop() (in module prodigy.analysis.lowerbounds.problem) process (Job attribute) prodigy module prodigy command line option --engine --intermediate-results --no-normalize --no-simplification --pos-heuristic --show-all-invs --solver --stepwise --strategy --template-heuristic --use-latex prodigy-analyze command line option --coefficients --decisions --json --loop --output --steps INPUT_DIST PROGRAM_FILE prodigy-check_equality command line option OTHER_PROGRAM_FILE PROGRAM_FILE prodigy-evt_lower_bound command line option --invariant INPUT_DIST PROGRAM_FILE prodigy-evt_sandwich command line option --json --lower --no-per-query --no-upper --objective --per-query --show-certificates --size --upper PROGRAM_FILE prodigy-independent_vars command line option --compute-exact PROGRAM_FILE prodigy-invariant_synthesis command line option --invariant INPUT_DIST PROGRAM_FILE prodigy-loop_strategies command line option --json prodigy-main command line option --loop --show-input-program INPUT_DIST PROGRAM_FILE prodigy-outline command line option --json PROGRAM_FILE prodigy-web command line option --allowed-host --examples --host --max-jobs --memory-limit --no-browser --port --time-limit prodigy.analysis module prodigy.analysis.ai_candidates module prodigy.analysis.analyzer module prodigy.analysis.config module prodigy.analysis.equivalence module prodigy.analysis.equivalence.equivalence_check module prodigy.analysis.evtinvariants module prodigy.analysis.evtinvariants.heuristics module prodigy.analysis.evtinvariants.heuristics.positivity module prodigy.analysis.evtinvariants.heuristics.positivity.dominat_root_rejection module prodigy.analysis.evtinvariants.heuristics.positivity.heuristics_factory module prodigy.analysis.evtinvariants.heuristics.positivity.individual_sum_terms module prodigy.analysis.evtinvariants.heuristics.positivity.iterate_terms module prodigy.analysis.evtinvariants.heuristics.positivity.logical module prodigy.analysis.evtinvariants.heuristics.positivity.polynomial_positivity module prodigy.analysis.evtinvariants.heuristics.positivity.positivity module prodigy.analysis.evtinvariants.heuristics.positivity.rational_function module prodigy.analysis.evtinvariants.heuristics.strategies module prodigy.analysis.evtinvariants.heuristics.templates module prodigy.analysis.evtinvariants.heuristics.templates.polynomial_function module prodigy.analysis.evtinvariants.heuristics.templates.rational_function module prodigy.analysis.evtinvariants.heuristics.templates.templates module prodigy.analysis.evtinvariants.heuristics.templates.templates_factory module prodigy.analysis.evtinvariants.invariant_synthesis module prodigy.analysis.evtinvariants.invariant_verification module prodigy.analysis.exceptions module

prodigy.analysis.independence module prodigy.analysis.independence.independence module prodigy.analysis.independence.utils module prodigy.analysis.instructionhandler module prodigy.analysis.instructionhandler.assignment_handler module prodigy.analysis.instructionhandler.function_handler module prodigy.analysis.instructionhandler.instruction_handler module prodigy.analysis.instructionhandler.ite_handler module prodigy.analysis.instructionhandler.loop_handler module prodigy.analysis.instructionhandler.observe_handler module prodigy.analysis.instructionhandler.probchoice_handler module prodigy.analysis.instructionhandler.program_info module prodigy.analysis.instructionhandler.query_handler module prodigy.analysis.instructionhandler.queryblock_handler module prodigy.analysis.instructionhandler.sample_handler module prodigy.analysis.instructionhandler.while_handler module prodigy.analysis.loop_strategies module prodigy.analysis.lowerbounds module prodigy.analysis.lowerbounds.egcalc module prodigy.analysis.lowerbounds.explicit module prodigy.analysis.lowerbounds.ir module prodigy.analysis.lowerbounds.parameters module prodigy.analysis.lowerbounds.problem module prodigy.analysis.lowerbounds.sandwich module prodigy.analysis.lowerbounds.subinvariant module prodigy.analysis.lowerbounds.synthesis module prodigy.analysis.optimization module prodigy.analysis.optimization.gf_optimizer module prodigy.analysis.optimization.optimizer module prodigy.analysis.result module prodigy.analysis.session module prodigy.analysis.solver module prodigy.analysis.solver.mock_solver module prodigy.analysis.solver.smtz3_solver module prodigy.analysis.solver.solver module prodigy.analysis.solver.solver_type module prodigy.analysis.solver.sympy_solver module prodigy.cli module prodigy.distribution module prodigy.distribution.distribution module prodigy.distribution.exact_division module prodigy.distribution.fast_generating_function module prodigy.distribution.generating_function module prodigy.distribution.linear_guards module prodigy.distribution.symengine_distribution module prodigy.pgcl module prodigy.pgcl.ast module prodigy.pgcl.check module prodigy.pgcl.compiler module prodigy.pgcl.parser module prodigy.pgcl.pgcl_checks module prodigy.pgcl.pgcl_operations module prodigy.pgcl.pysmt module prodigy.pgcl.pysmt.context module prodigy.pgcl.pysmt.expr module prodigy.pgcl.substitute module prodigy.pgcl.util module prodigy.pgcl.util.lark_expr_parser module prodigy.pgcl.util.ref module prodigy.util module prodigy.util.color module prodigy.util.logger module prodigy.util.order module prodigy.util.plotter module prodigy.web module prodigy.web.app module prodigy.web.diagnostics module prodigy.web.examples module prodigy.web.jobs module prodigy.web.requests module prodigy_version() (in module prodigy.analysis.result) ProdigyPGF (class in prodigy.distribution.fast_generating_function) profile_loop() (in module prodigy.analysis.lowerbounds.parameters) profiles (ParameterPlan attribute) prog_info (LoopTask attribute) program (AnalysisResult attribute) (ProgramInfo attribute) PROGRAM_FILE prodigy-analyze command line option prodigy-check_equality command line option prodigy-evt_lower_bound command line option prodigy-evt_sandwich command line option prodigy-independent_vars command line option prodigy-invariant_synthesis command line option prodigy-main command line option prodigy-outline command line option ProgramInfo (class in prodigy.analysis.instructionhandler.program_info) progress (Job attribute) (LoopRecord attribute) progress() (AnalysisSession method) (LoopTask method) prompt (ParamSpec attribute) prompt() (in module prodigy.analysis.ai_candidates) Provider (class in prodigy.analysis.ai_candidates) pscale() (in module prodigy.analysis.lowerbounds.egcalc) pshift() (in module prodigy.analysis.lowerbounds.egcalc)

Q

queries (AnalysisResult attribute) (AnalysisSession attribute) (LoopProblem attribute) queries_after() (in module prodigy.analysis.lowerbounds.problem) queries_of() (in module prodigy.analysis.lowerbounds.ir) Query (class in prodigy.analysis.lowerbounds.problem) query (QueryBound attribute)

query_bounds (LoopOutcome attribute) query_bounds() (in module prodigy.analysis.lowerbounds.sandwich) query_instructions() (in module prodigy.analysis.session) QueryBlockHandler (class in prodigy.analysis.instructionhandler.queryblock_handler) QueryBound (class in prodigy.analysis.lowerbounds.sandwich) QueryHandler (class in prodigy.analysis.instructionhandler.query_handler) QueryResult (class in prodigy.analysis.result)

R

rate (VariableProfile attribute) rates (TemplateShape attribute) rational_mass() (in module prodigy.analysis.lowerbounds.subinvariant) RationalFunctionDenomSign (class in prodigy.analysis.evtinvariants.heuristics.positivity.rational_function) RationalFunctionMaxDeg (class in prodigy.analysis.evtinvariants.heuristics.templates.rational_function) reach_box (TemplateShape attribute) reachable() (in module prodigy.analysis.lowerbounds.explicit) read (Mut attribute) record (LoopTask attribute) record_query() (AnalysisSession method) record_step() (AnalysisSession method) RED (Style attribute) Ref (in module prodigy.pgcl.util.ref) refine_upper_per_query() (in module prodigy.analysis.lowerbounds.sandwich) register_loop_strategy() (in module prodigy.analysis.loop_strategies) remaining (Exploration property) requires_unconditioned (LoopStrategy attribute)

RESET (Style attribute) residual (AnalysisSession property) (LoopOutcome attribute) (LoopRecord attribute) resolve_alias() (AnalysisSession method) restrict() (GFCalculus method) restrict_pred() (GFCalculus method) result (Job attribute) RIGHT (Assoc attribute) run (LoopStrategy attribute) run() (AnalysisSession method) (Exploration method) (GFCalculus method) run_analysis() (in module prodigy.web.requests) run_loop() (AnalysisSession method) run_state() (in module prodigy.analysis.lowerbounds.explicit) running (Job property) running_count() (JobManager method)

S

safe_subs() (SymengineDist method) SampleHandler (class in prodigy.analysis.instructionhandler.sample_handler) SandwichResult (class in prodigy.analysis.lowerbounds.sandwich) scale_bulk (VariableProfile attribute) scale_trunc (VariableProfile attribute) scaled_expansion() (in module prodigy.analysis.lowerbounds.synthesis) scope (AnalysisSession property) serve() (in module prodigy.web.app) session (LoopTask attribute) set_parameters() (Distribution method) (FPS method) (GeneratingFunction method) (SymengineDist method) set_variables() (Distribution method) (FPS method) (GeneratingFunction method) (SymengineDist method) set_variables_and_parameters() (Distribution method) (SymengineDist method) show() (in module prodigy.analysis.result) show_all_invs (ForwardAnalysisConfig attribute) show_intermediate_steps (ForwardAnalysisConfig attribute) shutdown() (JobManager method) silent (AnalysisSession property) SingleRationalFunction (class in prodigy.analysis.evtinvariants.heuristics.positivity.rational_function) size (TemplateLP property) size() (TemplateShape method) SMTZ3Solver (class in prodigy.analysis.solver.smtz3_solver) so_vars (ProgramInfo attribute) solve() (MockFalseSolver method) (MockNoneSolver method) (MockTrueSolver method) (SMTZ3Solver method) (Solver method) (SympySolver method) (TemplateLP method) SolveError Solver (class in prodigy.analysis.solver.solver)

solver_type (ForwardAnalysisConfig attribute) SolverType (class in prodigy.analysis.solver.solver_type) soundness (LoopStrategy attribute) split_program() (in module prodigy.analysis.lowerbounds.ir) started (Job attribute) State (class in prodigy.distribution.distribution) state (Job attribute) state_to_equality_expression() (in module prodigy.pgcl.pgcl_operations) status (AnalysisResult attribute) step() (Kernel method) step_wise (ForwardAnalysisConfig attribute) steps (AnalysisResult attribute) (AnalysisSession attribute) strategy (ForwardAnalysisConfig attribute) (LoopDecision attribute) (LoopRecord attribute) (LoopTask attribute) Style (class in prodigy.util.color) sub_analysis() (AnalysisSession method) submit() (JobManager method) substitute_constants() (in module prodigy.pgcl.substitute) substitute_constants_expr() (in module prodigy.pgcl.substitute) substitute_expr() (in module prodigy.pgcl.substitute) SUM_THEN_RATIONAL (SynthesisStrategies attribute) summary (Job attribute) SumPositivity (class in prodigy.analysis.evtinvariants.heuristics.positivity.individual_sum_terms) suppressed_messages (LoopRecord attribute) sym() (in module prodigy.analysis.result) SYMENGINE (ForwardAnalysisConfig.Engine attribute) SymengineDist (class in prodigy.distribution.symengine_distribution) SymenginePGF (class in prodigy.distribution.symengine_distribution) SYMPY (ForwardAnalysisConfig.Engine attribute) (SolverType attribute) SympyPGF (class in prodigy.distribution.generating_function) SympySolver (class in prodigy.analysis.solver.sympy_solver) SynthesisStrategies (class in prodigy.analysis.evtinvariants.heuristics.strategies) SynthesisStrategy (class in prodigy.analysis.evtinvariants.heuristics.strategies) synthesize_lower() (in module prodigy.analysis.lowerbounds.sandwich) synthesize_upper() (in module prodigy.analysis.lowerbounds.sandwich)

T

tail_kernel() (in module prodigy.analysis.lowerbounds.parameters) tail_start (Certificate attribute) (TemplateShape attribute) TailKernel (class in prodigy.analysis.lowerbounds.parameters) templ_heuristic (ForwardAnalysisConfig attribute) template_heuristics (SynthesisStrategy attribute) template_size (Certificate attribute) TemplateHeuristic (class in prodigy.analysis.evtinvariants.heuristics.templates.templates) TemplateHeuristics (class in prodigy.analysis.evtinvariants.heuristics.templates.templates_factory) TemplateLP (class in prodigy.analysis.lowerbounds.synthesis) TemplateShape (class in prodigy.analysis.lowerbounds.parameters) text (Query attribute) tighten_interval() (in module prodigy.analysis.result) time (LoopRecord attribute) time_build (Certificate attribute) time_limit (Job attribute) time_lp (Certificate attribute) time_total (SandwichResult attribute) timing (AnalysisResult attribute) title (Example attribute) (LoopStrategy attribute) to_expr() (GFCalculus method) to_float() (in module prodigy.analysis.result) to_json() (AnalysisResult method) (Certificate method) (DecisionRequired method) (Example method) (Job method) (LoopDecision method) (LoopInfo method) (LoopRecord method) (LoopStrategy method) (ParamSpec method) (QueryBound method) (QueryResult method) (SandwichResult method)

to_latex() (in module prodigy.analysis.result) to_monomial() (State method) to_product_form() (in module prodigy.analysis.lowerbounds.subinvariant) to_sympy() (in module prodigy.analysis.result) token_positions() (in module prodigy.analysis.session) total_mass (Certificate attribute) transitions (TailKernel attribute) TranslationContext (class in prodigy.pgcl.pysmt.context) TRUE (SolverType attribute) TRUE_RAT_FUNC (PositivityHeuristics attribute) tuple() (Mut static method) type_name() (in module prodigy.analysis.result)

U

undefined() (CommonDistributionsFactory static method) (ProdigyPGF static method) (SymenginePGF static method) (SympyPGF static method) UNDERLINE (Style attribute) uniform() (CommonDistributionsFactory static method) (ProdigyPGF static method) (SymenginePGF static method) (SympyPGF static method) univariate_table() (in module prodigy.analysis.result) UNKNOWN (Bound attribute) UnsupportedFeatureError UnsupportedLoopError UnsupportedProgram update() (Distribution method)

update_iid() (Distribution method) (FPS method) (GeneratingFunction method) (SymengineDist method) UPPER (Bound attribute) upper (ParameterPlan attribute) (QueryBound attribute) (QueryResult attribute) (SandwichResult attribute) upper_float (QueryResult attribute) upper_objective() (in module prodigy.analysis.lowerbounds.sandwich) upper_tail_rates() (in module prodigy.analysis.lowerbounds.parameters) use_latex (ForwardAnalysisConfig attribute) use_latex_output (GeneratingFunction attribute) use_simplification (ForwardAnalysisConfig attribute) (GeneratingFunction attribute)

V

val (Mut property) validate_decisions() (in module prodigy.analysis.session) validate_request() (in module prodigy.web.requests) valuations (State attribute) value (QueryResult attribute) value_at_one() (Denominator method) value_float (QueryResult attribute) VariableProfile (class in prodigy.analysis.lowerbounds.parameters)

variables (AllOrPartialRational attribute) (DefaultStrategy attribute) (FinitePolynomial attribute) (InfinitePolynomial attribute) (LoopProblem attribute) (PartialRational attribute) (TranslationContext attribute) VerificationError verify_certificate() (in module prodigy.analysis.lowerbounds.synthesis)

W

warn() (AnalysisSession method) warnings (AnalysisResult attribute) (AnalysisSession attribute) WhileHandler (class in prodigy.analysis.instructionhandler.while_handler) WHITE (Style attribute)

with_den() (GFCalculus method) without() (Denominator method) wrap() (Mut static method) write (Mut attribute) write_json() (in module prodigy.analysis.lowerbounds.sandwich)

Y

YELLOW (Style attribute)

Z

Z3 (SolverType attribute) zero() (ProdigyPGF static method) (SymenginePGF static method) (SympyPGF static method)