.. _Cadical 1.0.3: http://fmv.jku.at/cadical/

.. _how-add-a-new-solver:

How to add a new solver to OptiLog
==================================

This framework provides a quick and easy way to make a wrapper for a new solver
that allows its use from a Python environment.

To do it, three steps must be followed:

    1. Implement the iSAT interface.
    2. Provide the linking functions
    3. Compile the solver as a library (a Linux shared object)

.. _implementing-interface:

Implementing the iSAT interface
--------------------------------

Please, checkout the `OptiLogFrameworkInterface <https://github.com/optilog/OptiLogFrameworkInterface>`_ repository to download the interface.

The interface source code can be found in the ``FrameworkInterface`` directory.
The most important files are ``isat.hpp``, ``parameter.hpp`` and ``pyexceptions.hpp``.

First of all, you have to implement the :ref:`iSAT <isat-interface>` interface.
You do not need to implement the whole interface; only the methods you need.
A method not implemented will throw a ``NotImplementedException``.

Let see an example of an implementation:

In this example we will see how to make a basic implementation of the  the `Cadical 1.0.3`_ solver.

The first thing we will do is declare a C++ class that will act as a wrapper of the Cadical
SAT solver.

    **solver.hpp**

    .. literalinclude:: examples/solver.hpp


    We will also provide an implementation for all the defined methods:

    **solver.cpp**

    .. literalinclude:: examples/solver.cpp


.. _provide_linking:

The Linking Functions
---------------------

The ``optilogcinterface.hpp`` defines two macros that automatically define the linking functions for OptiLog.
First, we will tell OptiLog how to instantiate and destruct our newly created SAT solver.
We will do this by adding the following code at the end of the **solver.cpp** file:

    .. literalinclude:: examples/linking1.cpp

The first parameter to the OPTILOG_C_INTERFACE macro is the name of the class that implements the iSAT interface.
The second parameter is the name of the SAT solver that is going to be exported to Python.

Optionally, you can provide a vector that specifies the configurable options of the SAT solver on the ``set`` and ``get`` method calls.
See:

    .. literalinclude:: examples/linking2.cpp

The ``OptilogConfigParameter`` objects expose a ``name``, ``lower_bound``, ``upper_bound`` and ``default`` parameters.
You can find the corresponding source code on ``configparameter.hpp``.

Compiling as a library
----------------------

We will compile the Cadical solver with ``gcc``. The only requirements for this step are:

    * The solver *must* be compiled with position independent code (-fPIC flag)
    * The solver *must* be compiled as a shared library (-shared flag)
    * No symbols related to the iSAT interface must be undefined. *Recommended*: Compile with ``-Wl,--no-undefined`` to make sure that the solver includes the source files for for ``*.cpp`` files of the FrameworkInterface.
    * Include ``-lm``, ``-lstdc++`` and other libraries as necessary.

Here is a compilation example command:

    .. literalinclude:: examples/compile.sh

.. note::

    You can copy the files in the FrameworkInterface into your working environment.
    However, these files should *not be edited*

Loading the solver
------------------

When imported, OptiLog will check for solver libraries in the following locations:

    * The solvers already distributed with OptiLog (``<optilog-installation/sat/solvers>``)
    * The solvers on ``~/.optilog_solvers``
    * Each location on the environment variable OPTILOG_SOLVERS. The paths are separated like PATH environment variable (with ':').

If you are developing a new SAT solver, simply copying the library to ``~/.optilog_solvers`` will work!

The solvers are imported when the ``optilog.solvers.sat`` module is loaded. If you want to modify the environment variables with python code, make sure to do it before
actually importing your solvers.

.. code:: python
    :number-lines:

    import os
    os.environ['OPTILOG_SOLVERS'] = '/path/to/new/sat/solver/'
    from optilog.solvers.sat import NewSatSolver