.. only:: html

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

        Click :ref:`here <sphx_glr_download_Examples_5_DisjunctionConstraintExample.py>`     to download the full example code
    .. rst-class:: sphx-glr-example-title

    .. _sphx_glr_Examples_5_DisjunctionConstraintExample.py:


Disjunction Constraint Example
====================

Top contributors (to current version):
  - Haoze Andrew Wu

This file is part of the Marabou project.
Copyright (c) 2017-2019 by the authors listed in the file AUTHORS
in the top-level source directory) and their institutional affiliations.
All rights reserved. See the file COPYING in the top-level source
directory for licensing information.


.. code-block:: default


    import sys
    import numpy as np

    ## %
    # Path to Marabou folder if you did not export it

    # sys.path.append('/home/USER/git/Marabou')
    from maraboupy import Marabou
    from maraboupy import MarabouCore



Path to NNet file


.. code-block:: default

    nnetFile = "./resources/nnet/mnist/mnist10x10.nnet"


Load the network from NNet file, and set a lower bound on first output variable


.. code-block:: default

    net1 = Marabou.read_nnet(nnetFile)


Require that a input variable is either 0 or 1


.. code-block:: default

    for var in net1.inputVars[0]:
        # eq1: 1 * var = 0
        eq1 = MarabouCore.Equation(MarabouCore.Equation.EQ);
        eq1.addAddend(1, var);
        eq1.setScalar(0);

        # eq2: 1 * var = 1
        eq2 = MarabouCore.Equation(MarabouCore.Equation.EQ);
        eq2.addAddend(1, var);
        eq2.setScalar(1);

        # ( var = 0) \/ (var = 1)
        disjunction = [[eq1], [eq2]]
        net1.addDisjunctionConstraint(disjunction)

        # add additional bounds for the variable
        net1.setLowerBound(var, 0)
        net1.setUpperBound(var, 1)


Solve Marabou query


.. code-block:: default

    vals1, stats1 = net1.solve()



Example statistics


.. code-block:: default

    stats1.getNumSplits()
    stats1.getTotalTime()



Eval example

Test that the satisfying assignment found is a real one.


.. code-block:: default

    for i in range(784):
        assert(abs(vals1[i] - 1) < 0.0000001 or abs(vals1[i]) < 0.0000001)


.. rst-class:: sphx-glr-timing

   **Total running time of the script:** ( 0 minutes  0.000 seconds)


.. _sphx_glr_download_Examples_5_DisjunctionConstraintExample.py:


.. only :: html

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



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

     :download:`Download Python source code: 5_DisjunctionConstraintExample.py <5_DisjunctionConstraintExample.py>`



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

     :download:`Download Jupyter notebook: 5_DisjunctionConstraintExample.ipynb <5_DisjunctionConstraintExample.ipynb>`


.. only:: html

 .. rst-class:: sphx-glr-signature

    `Gallery generated by Sphinx-Gallery <https://sphinx-gallery.github.io>`_