.. only:: html

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

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

    .. _sphx_glr_Examples_4_DncExample.py:


DNC Example
====================

Top contributors (to current version):
  - Andrew Wu
  - Kyle Julian
  
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

    # Append to path if needed
    #sys.path.append(</Path/To/Marabou/>)

    from maraboupy import Marabou


Load an example network and place an output constraint


.. code-block:: default

    nnet_file_name = "../../src/input_parsers/acas_example/ACASXU_run2a_1_1_tiny_2.nnet"
    net = Marabou.read_nnet(nnet_file_name)
    net.setLowerBound(net.outputVars[0][0], .5)


Solve the query with DNC mode turned on, which should return satisfying variable values


.. code-block:: default

    options = Marabou.createOptions(snc=True, verbosity=0, initialDivides=2);
    vals, stats = net.solve(options=options)
    assert len(vals) > 0


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

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


.. _sphx_glr_download_Examples_4_DncExample.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: 4_DncExample.py <4_DncExample.py>`



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

     :download:`Download Jupyter notebook: 4_DncExample.ipynb <4_DncExample.ipynb>`


.. only:: html

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

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