stormvogel.teaching.lp
======================

.. py:module:: stormvogel.teaching.lp


Classes
-------

.. autoapisummary::

   stormvogel.teaching.lp.LP
   stormvogel.teaching.lp.LPSolution


Functions
---------

.. autoapisummary::

   stormvogel.teaching.lp._expr_to_z3
   stormvogel.teaching.lp._constraint_to_z3
   stormvogel.teaching.lp.solve_lp
   stormvogel.teaching.lp.lp_prob
   stormvogel.teaching.lp.lp_dual_prob
   stormvogel.teaching.lp.lp_dual_maxreachprob
   stormvogel.teaching.lp.lp_maxreachprob
   stormvogel.teaching.lp.lp_minreachprob
   stormvogel.teaching.lp.extract_policy_from_dual_lp


Module Contents
---------------

.. py:class:: LP

   LP formulation for MDP reachability, as sympy expressions.

   Renders as a formatted LP in Jupyter via _repr_latex_.


   .. py:attribute:: sense
      :type:  str


   .. py:attribute:: objective
      :type:  sympy.Expr


   .. py:attribute:: constraints
      :type:  list[sympy.Basic]
      :value: []



   .. py:method:: _repr_latex_() -> str


.. py:class:: LPSolution

   Exact rational solution to an LP returned by :func:`solve_lp`.

   :param objective: Optimal objective value.
   :param values: Variable assignments, keyed by the sympy Symbol used in the LP.


   .. py:attribute:: objective
      :type:  fractions.Fraction


   .. py:attribute:: values
      :type:  dict[sympy.Symbol, fractions.Fraction]


.. py:function:: _expr_to_z3(expr: sympy.Expr, var_map: dict[sympy.Symbol, Any]) -> Any

.. py:function:: _constraint_to_z3(c: sympy.Basic, var_map: dict[sympy.Symbol, Any]) -> Any

.. py:function:: solve_lp(lp: LP) -> LPSolution | None

   Solve an LP using z3 (exact rational arithmetic).

   :param lp: The LP to solve.
   :returns: Exact rational solution, or ``None`` if infeasible or unbounded.
   :raises ImportError: If z3-solver is not installed.


.. py:function:: lp_prob(mdp: stormvogel.model.Model[float], min: bool, zero_states: Iterable[stormvogel.model.State], one_states: Iterable[stormvogel.model.State]) -> LP

   Build the LP formulation for MDP reachability as sympy expressions.

   :param mdp: The stormvogel MDP.
   :param min: True for min-reachability (maximize), False for max-reachability (minimize).
   :param zero_states: States fixed at value 0.
   :param one_states: States fixed at value 1 (target states).
   :returns: LP with objective and constraints as sympy expressions.


.. py:function:: lp_dual_prob(mdp: stormvogel.model.Model[float], zero_states: Iterable[stormvogel.model.State], one_states: Iterable[stormvogel.model.State]) -> LP

   Occupancy-measure (dual) LP for single-objective reachability.


.. py:function:: lp_dual_maxreachprob(mdp: stormvogel.model.Model[float], target_label: str) -> LP

   Dual LP for maximum reachability probability to states labelled target_label.


.. py:function:: lp_maxreachprob(mdp: stormvogel.model.Model[float], target_label: str) -> LP

   LP for maximum reachability probability to states labelled target_label.


.. py:function:: lp_minreachprob(mdp: stormvogel.model.Model[float], target_label: str) -> LP

   LP for minimum reachability probability to states labelled target_label.


.. py:function:: extract_policy_from_dual_lp(mdp: stormvogel.model.Model[float], sol: LPSolution) -> dict

   Extract a deterministic policy from an occupancy-measure (dual) LP solution.

   The dual LP variables ``y_{s,a}`` represent expected visit counts for each
   state-action pair under the optimal policy. For each state the action with
   the largest ``y`` value is chosen. States that are unreachable under the
   optimal policy (all ``y`` values zero or absent in *sol*) receive the first
   available non-empty action as a default; the choice does not affect the
   objective value.

   :param mdp: The MDP for which the dual LP was built.
   :param sol: Solution returned by :func:`solve_lp`.
   :returns: Dict mapping each state with at least one non-empty action to its
       chosen :class:`~stormvogel.model.Action`.