.. DO NOT EDIT.
.. THIS FILE WAS AUTOMATICALLY GENERATED BY SPHINX-GALLERY.
.. TO MAKE CHANGES, EDIT THE SOURCE PYTHON FILE:
.. "tutorials/01_configurations.py"
.. LINE NUMBERS ARE GIVEN BELOW.

.. only:: html

    .. note::
        :class: sphx-glr-download-link-note

        :ref:`Go to the end <sphx_glr_download_tutorials_01_configurations.py>`
        to download the full example code.

.. rst-class:: sphx-glr-example-title

.. _sphx_glr_tutorials_01_configurations.py:


Configuration rules
=======================
A backup application offers local storage, remote storage, encryption, and
notifications. It needs at least one storage destination; remote backups
require encryption. The rule is

``(L ∨ R) ∧ (¬R ∨ E)``.

Notifications are optional. We will count the valid configurations, inspect
forced choices, and follow a user changing their selections.

.. GENERATED FROM PYTHON SOURCE LINES 15-29

.. code-block:: Python

    from tididi import Literal, Vtree, cube, literal

    vtree = Vtree.balanced(4)
    local_choice = Literal(1)
    remote_choice = Literal(2)
    encrypted_choice = Literal(3)
    notifications_choice = Literal(4)
    names = {1: "local backups", 2: "remote backups", 3: "encryption", 4: "notifications"}

    local = literal(vtree, local_choice)
    remote = literal(vtree, remote_choice)
    encrypted = literal(vtree, encrypted_choice)
    notifications = literal(vtree, notifications_choice)








.. GENERATED FROM PYTHON SOURCE LINES 30-34

Build and count
-------------------
``remote.copy()`` creates an operand for this operation so the original
remains available. The resulting circuit owns its storage.

.. GENERATED FROM PYTHON SOURCE LINES 34-41

.. code-block:: Python

    destination = local | remote.copy()
    encryption_rule = ~remote.copy() | encrypted.copy()
    configurations = destination & encryption_rule
    print("Valid configurations:", configurations.model_count())
    with_notifications = configurations.copy() & notifications
    print("With notifications:", with_notifications.model_count())





.. rst-class:: sphx-glr-script-out

 .. code-block:: none

    Valid configurations: 8
    With notifications: 4




.. GENERATED FROM PYTHON SOURCE LINES 42-45

Inspect a user's choices
----------------------------
Requiring remote backups leaves only configurations with encryption.

.. GENERATED FROM PYTHON SOURCE LINES 45-52

.. code-block:: Python

    with_remote = configurations.copy() & remote
    print("With remote backups:", with_remote.model_count())
    for choice in with_remote.implied_literals():
        print(f"Required choice: {names[choice.variable]} = {choice.sign}")
    remote_without_encryption = with_remote & ~encrypted
    print("Satisfiable:", remote_without_encryption.is_sat())





.. rst-class:: sphx-glr-script-out

 .. code-block:: none

    With remote backups: 4
    Required choice: remote backups = True
    Required choice: encryption = True
    Satisfiable: False




.. GENERATED FROM PYTHON SOURCE LINES 53-55

A witness chooses one value for every variable. It is a list of immutable
``Literal`` values that can be reused to construct a cube.

.. GENERATED FROM PYTHON SOURCE LINES 55-61

.. code-block:: Python

    witness = configurations.satisfying_assignment()
    for choice in witness:
        print(f"{names[choice.variable]}: {choice.sign}")
    selected = configurations.copy() & cube(vtree, witness)
    print("Selected valid configurations:", selected.model_count())





.. rst-class:: sphx-glr-script-out

 .. code-block:: none

    local backups: True
    remote backups: True
    encryption: True
    notifications: False
    Selected valid configurations: 1




.. GENERATED FROM PYTHON SOURCE LINES 62-67

Count under changing observations
-------------------------------------
A counter owns the circuit while it retains cached counts. Creating it
consumes ``configurations``. Observations use the named literal values,
which are reusable and do not own circuits.

.. GENERATED FROM PYTHON SOURCE LINES 67-77

.. code-block:: Python

    counter = configurations.counter()
    counter.observe([remote_choice])
    print("Matching configurations:", counter.model_count())
    counter.observe([~notifications_choice])
    print("Matching configurations:", counter.model_count())
    counter.observe([~remote_choice, ~encrypted_choice])
    print("Matching configurations:", counter.model_count())
    counter.clear_observations()
    print("Matching configurations:", counter.model_count())





.. rst-class:: sphx-glr-script-out

 .. code-block:: none

    Matching configurations: 4
    Matching configurations: 2
    Matching configurations: 1
    Matching configurations: 8




.. GENERATED FROM PYTHON SOURCE LINES 78-80

Finish the counter to recover its original diagram. Its observations never
changed that diagram. Minimization returns a canonical circuit for this vtree.

.. GENERATED FROM PYTHON SOURCE LINES 80-83

.. code-block:: Python

    configurations = counter.finish().minimize()
    print("Valid configurations:", configurations.model_count())
    print("Minimized pairs:", configurations.pair_count())




.. rst-class:: sphx-glr-script-out

 .. code-block:: none

    Valid configurations: 8
    Minimized pairs: 8





.. _sphx_glr_download_tutorials_01_configurations.py:

.. only:: html

  .. container:: sphx-glr-footer sphx-glr-footer-example

    .. container:: sphx-glr-download sphx-glr-download-jupyter

      :download:`Download Jupyter notebook: 01_configurations.ipynb <01_configurations.ipynb>`

    .. container:: sphx-glr-download sphx-glr-download-python

      :download:`Download Python source code: 01_configurations.py <01_configurations.py>`

    .. container:: sphx-glr-download sphx-glr-download-zip

      :download:`Download zipped: 01_configurations.zip <01_configurations.zip>`