.. include:: ../shared/references.rst
.. include:: ../shared/formulas-substitutions.rst

.. _VarManager:

.. py:module:: optilog.formulas
    :noindex:

.. autoclass:: VarManager


Methods sumary
---------------

.. list-table::
    :widths: 60 300
    :header-rows: 1

    * - Return type
      - Methods
    * - int
      - :py:meth:`VarManager.new_var`
    * - int
      - :py:meth:`VarManager.add_var`
    * - int
      - :py:meth:`VarManager.get_lit`
    * - int
      - :py:meth:`VarManager.max_var`
    * - None
      - :py:meth:`VarManager.extend_vars`
    * - None
      - :py:meth:`VarManager.set_minimum_vars`


Example on how to use a VarManager:

.. code:: python
  :number-lines:

  >>> from optilog.formulas import VarManager, CNF
  >>> v = VarManager()
  >>> c1 = CNF(var_manager=v)
  >>> c2 = CNF(var_manager=v)
  >>> c1.new_var()
  1
  >>> c2.new_var()
  2
  >>> c1.new_var()
  3
  >>> v.new_var()
  4
  >>> from optilog.modelling import Bool, Not
  >>> b1 = Bool('b1')
  >>> v.add_var(b1)
  5
  >>> v.new_var()
  6
  >>> v.get_lit(b1)
  5
  >>> v.get_lit(Not(b1))
  -5
  >>> b2 = Bool('b2')
  >>> v.get_lit(b2)
  7
  >>> v.decode_dimacs([-5,7])
  [~b1, b2]

You may also assume implicit initialization of the VarManager
and reuse it across objects:

>>> c1 = CNF()
>>> c1.new_var()
1
>>> c2 = CNF(var_manager=c1.var_manager)
>>> c1.new_var()
2
>>> c2.new_var()
3


All of these examples would be exactly equivalent with CNF/WCNF/QCNF.