.. include:: /rst/exports/roles.include

.. _demos_consistency_checker:

Check consistency
#################

The AML Consistency Checker shows:

* a summary of duples grouped by region,
* the result of the consistency analysis,
* if the embedding is inconsistent, it displays the potential source.

Here we use the embedding described in :ref:`demos_queens_embedding` as an example.

Consistent embedding
********************

An embedding is consistent if no rules enter in contradiction.
This contradiction can be difficult to spot when it happens with implicit rules.
For instance, :math:`A < B` and :math:`A \nless B`, produce an explicit contradiction.
However, :math:`A < B`, :math:`B < C`, (implicitly produce :math:`A < C`, which is not one of the original rules).
In this case, a sentence such as :math:`A \nless C` would give raise to a contradiction.

If we run the analysis on the N-Queens embedding we obtain that the result is consistent.


.. code-block:: bash

    python AMLConsistencyChecker.py queens_embedding.py

It also displays a summary of the number of duples generated by the embedding in each region.

Positive duples::

   + region  1 > 64
   + region  5 > 128
   + region  6 > 128
   + region  7 > 124
   + region  9 > 1
   + region  12 > 2

Negative duples::

   - region  1 > 8
   - region  2 > 8
   - region  11 > 64


Inconsistent embedding
**********************

The embedding can be turned inconsistent by adding the following duple

.. code-block:: python

    theEmbedding.REGION = 14
    ADD(INC(F("Q", 4), F("E", 4)))

If we run the analysis on this modified embedding we obtain that the result is inconsistent this time.

.. code-block:: bash

    python AMLConsistencyChecker.py queens_embedding.py

First it displays a summary of the duples in the embedding.
Notice that there is an additional region with a positive duple::

    + region  14 > 1

This follows with information about the inconsistency.
Which negative duple is producing the problem::

  Failure in region 1 at:

  R[4] !< Q[0]...Q[3] * Q[5]...Q[11] * Q[13]...Q[19] *
          Q[21]...Q[27] * Q[29]...Q[35] * Q[37]...Q[43] *
          Q[45]...Q[51] * Q[53]...Q[59] * Q[61]...Q[63] *
          E[0]...E[63]

This rule indicates that anything besides the Queens at the forth row (:math:`Q[4]`, :math:`Q[12]`, ...) produce the property :math:`R[4]`.
That constant indicates *having a Queen on the forth row*.

This output is followed by the positive duples that might be causing the inconsistency::

  Potential conflict with:
    in region 1 at:
      R[0]*C[0] < Q[0]
      R[0]*C[1] < Q[8]
      R[0]*C[2] < Q[16]
      R[0]*C[3] < Q[24]
      R[0]*C[4] < Q[32]
      R[0]*C[5] < Q[40]
      R[0]*C[6] < Q[48]
      R[0]*C[7] < Q[56]
      R[1]*C[0] < Q[1]
      R[2]*C[0] < Q[2]
      R[3]*C[0] < Q[3]
      R[5]*C[0] < Q[5]
      R[6]*C[0] < Q[6]
      R[7]*C[0] < Q[7]
      R[4]*C[0] < Q[4]
    in region 14 at:
      Q[4] < E[4]

The inconsistency comes from :math:`Q[4] < E[4]` that together with :math:`{R[4],C[0]} < Q[4]` produces :math:`R[4] < E[4]`.
This duple is inconsistent with the negative duple in region 1, :math:`R[4] \nless E[4]`.