Class Pb2cnf
============

The class Pb2cnf is the main interface to encode a PB constraint.


Constructor
-----------

.. _pb2cnf:

Pb2cnf(config: :ref:`PBConfig <pbconfig>`, stat: Statistics)

  Creates a Pb2cnf with the specified configuration & statistics.

  >>> from pypblib import pblib
  >>> conf = pblib.PBConfig()
  >>> stat = pblib.Statistics()
  >>> pb2 = pblib.Pb2cnf(conf, stat)

|

Pb2cnf(config: :ref:`PBConfig <pbconfig>`)

  Creates a Pb2cnf with the specified configuration.

  >>> from pypblib import pblib
  >>> c = pblib.PBConfig()
  >>> c
  >>> pb2 = pblib.Pb2cnf(c)

|

Pb2cnf()

  If the constructor does not receive any parameters, it will be created with default configuration.

  >>> from pypblib import pblib
  >>> pb2 = pblib.Pb2cnf()

|

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

+-------------------+----------------------------------------------------------------------------------------------------------------------+
|   Return Type     |                           Method                                                                                     |
+===================+======================================================================================================================+
|       int         | :ref:`encode_at_most_k <encode-at-most-k>` (literals: [int], k: long, formula: [], first_free_var: int)              |
+-------------------+----------------------------------------------------------------------------------------------------------------------+
|       int         | :ref:`encode_at_least_k <encode-at-least-k>` (literals: [int], k: long, formula: [], first_free_var: int)            |
+-------------------+----------------------------------------------------------------------------------------------------------------------+
|       int         | :ref:`encode_leq <encode-leq>` (weights: [long], literals: [int], k: long, formula: [], first_free_var: int)         |
+-------------------+----------------------------------------------------------------------------------------------------------------------+
|       int         | :ref:`encode_geq <encode-geq>` (weights: [long], literals: [int], k: long, formula: [], first_free_var: int)         |
+-------------------+----------------------------------------------------------------------------------------------------------------------+
|       int         | :ref:`encode_both<encode-both>` (weights: [long], literals [int], leq: long, geq:                                    |
|                   | long, formula: [], first_free_var: int)                                                                              |
+-------------------+----------------------------------------------------------------------------------------------------------------------+
|       void        | :ref:`encode <encode-std>` (constr_list: [:ref:`PBConstraint <pb-constraint>`], formula:                             |
|                   |  :ref:`VectorClauseDatabase <vect-cdb>`, aux_var_manager :ref:`AuxVarManager <aux-var-manager>`)                     |
+-------------------+----------------------------------------------------------------------------------------------------------------------+
|       void        | :ref:`encode_inc_initial <encode-inc>` (i_const_list: [:ref:`IncPBConstraint <i-pbconstr>`], form:                   |
|                   |  :ref:`VectorClauseDatabase <vect-cdb>`, aux_var_man :ref:`AuxVarManager <aux-var-manager>`)                         |
+-------------------+----------------------------------------------------------------------------------------------------------------------+



Methods details
---------------


.. _encode-at-most-k:

    .. method:: encode_at_most_k(literals: [int], k: long, formula: [], first_free_variable: int) -> int

    For a simple interface 'at most k'. The return value is the last used variable. Hence the next integer is the first free variable. At the end, the formula will contains the codification.

   >>> from pypblib import pblib
    >>> literals = [1, 2, 3]
    >>> k = 1
    >>> first_free_var = 4
    >>> formula = []
    >>> config = pblib.PBConfig()
    >>> max_var = pb2.encode_at_most_k(literals, k, formula,
                                       first_free_var)
    >>> print(max_var)
    3
    >>> print(formula)
    [[-3, -2], [-3, -1], [-2, -1]]


.. _encode-at-least-k:

    .. method:: encode_at_least_k(literals: [int], k: long, formula: [], first_free_variable: int) -> int

    For a simple interface 'at least k'. The return value is the last used variable. Hence the next integer is the first free variable. At the end, the formula will contains the codification.

    >>> from pypblib.pblib import PBConfig, Pb2cnf
    >>> formula = []
    >>> pb2 = Pb2cnf(PBConfig())
    >>> max_var = pb2.encode_at_least_k([1, 2, 3, 4], 2,
                                        formula, 5)
    >>>print(max_var)
    10
    >>> for clause in formula:
    ... 	for var in clause:
    ... 		print(var, end=" ")
    ... 	print("0")
    ...
    5 0
    1 -6 0
    2 -6 0
    1 2 -7 0
    7 -8 0
    6 3 -8 0
    7 3 -9 0
    9 -10 0
    8 4 -10 0
    10 0


.. _encode-leq:

    .. method:: encode_leq(weights: [long], literals: [int], k: long, formula: [], first_free_variable: int) -> int

    For a simple interface and :ref:`LEQ <pb-comparator>` (less-equals) comparator. The return value is the last used variable. Hence the next integer is the first free variable. At the end, the formula will contains the codification.

    >>> from pypblib.pblib import Pb2cnf, PBConfig
    >>> pb2 = Pb2cnf(PBConfig())
    >>> formula = []
    >>> weights = [2, 3, 1, 2]
    >>> literals = [1, 2, 3, 4]
    >>> first_free_var = 5
    >>> leq = 3
    >>> max_var = pb2.encode_leq(weights, literals, leq,
                                 formula, first_free_var)
    >>> print(max_var)
    9
    >>> print(formula)
    [[5], [-3, -6], [-1, -6], [6, -7], [-4, -7], [-1, -4, -8],
     [8, -9], [7, -2, -9], [9]]


.. _encode-geq:

    .. method:: encode_geq(weights: [long], literals: [int], k: long, formula: [], first_free_variable: int) -> int

    For a simple interface and :ref:`GEQ <pb-comparator>` (greater-equals) comparator. The return value is the last used variable. Hence the next integer is the first free variable. At the end, the formula will contains the codification.

    >>> from pypblib.pblib import Pb2cnf, PBConfig
    >>> pb2 = Pb2cnf(PBConfig())
    >>> formula = []
    >>> max_var = pb2.encode_geq([2, 1, 2, 4], [1, 2, 3, 4],
                                 3, formula, 5)
    >>> print(max_var)
    9
    >>> print(formula)
    [[5], [2, -6], [1, -6], [2, 1, -7], [7, -8], [6, 3, -8],
     [8, 4, -9], [9]]


.. _encode-both:

    .. method:: encode_both(weights: [long], literals [int], leq: long, geq: long, formula: [], first_free_variable: int) -> int

    For a simple interface, :ref:`LEQ <pb-comparator>` (less-equals) and :ref:`GEQ <pb-comparator>` (greater-equals) comparators. The return value is the last used variable. Hence the next integer is the first free variable. At the end, the formula will contains the codification.

    >>> from pypblib import pblib
    >>> config = pblib.PBConfig()
    >>> pb2 = pblib.Pb2cnf(config)
    >>> formula = []
    >>> leq = 3
    >>> geq = 1
    >>> weights = [2, 3, 1, 1]
    >>> literals = [1, 2, 3, 4]
    >>> first_free_var = 5
    >>> max_var = pb2.encode_both(weights, literals, leq, geq,
                                  formula, first_free_var)
    >>> print(max_var)
    10
    >>> for clause in formula:
    ... 	for var in clause:
    ... 		print(var, end=" ")
    ... 	print("0")
    ...
    4 3 2 1 0
    5 0
    -3 -6 0
    -4 -6 0
    6 -7 0
    -1 -7 0
    -3 -4 -8 0
    8 -1 -9 0
    9 -10 0
    7 -2 -10 0
    10 0


.. _encode-std:

    .. method:: encode(constr: PBConstraint, formula: VectorClauseDatabase, aux_var_manager: AuxVarManager)

    For this sophisticated interface you should use, besides the :ref:`PBConstraint <pb-constraint>`, a :ref:`VectorClauseDatabase <vect-cdb>` and a :ref:`AuxVarManager <aux-var-manager>` to encode a pseudo boolean constriant. At the end, the formula will contains the codification.

  >>> from pypblib import pblib
  >>> wl_List = [pblib.WeightedLit(1,3),
                 pblib.WeightedLit(2,1),
                 pblib.WeightedLit(3,5)]
  >>> comparator = pblib.GEQ
  >>> bound = 1
  >>> aux_var = pblib.AuxVarManager(4)
  >>> constr = pblib.PBConstraint(wl_List, comparator, bound)
  >>> config = pblib.PBConfig()
  >>> formula = pblib.VectorClauseDatabase(config)
  >>> pb2cnf = pblib.Pb2cnf(config)
  >>> pb2cnf.encode(constr, formula, aux_var)
  >>> print(formula)
  4 0
  2 1 -5 0
  5 3 -6 0
  6 0
  >>> formula.print_formula("encode_test.cnf",
                            aux_var.get_biggest_returned_auxvar())


.. _encode-inc:

  .. method:: encode_inc_initial(inc_constr: IncPBConstraint, formula: VectorClauseDatabase, aux_var_manager: AuxVarManager)

  For incremental pseudo boolean constraint. You should use, besides the :ref:`IncPBConstraint <i-pbconstr>`, a :ref:`VectorClauseDatabase <vect-cdb>` and a :ref:`AuxVarManager <aux-var-manager>` to encode. At the end, the formula will contains the codification.

  >>> from pypblib import pblib
  >>> wl1 = pblib.WeightedLit(1, 2)
  >>> wl2 = pblib.WeightedLit(2, 2)
  >>> wl3 = pblib.WeightedLit(3, -1)
  >>> i_contr = pblib.IncPBConstraint([wl1, wl2, wl3], pblib.LEQ, 3)
  >>> aux_var = pblib.AuxVarManager(4)
  >>> config = pblib.PBConfig()
  >>> formula = pblib.VectorClauseDatabase(config)
  >>> pb2 = pblib.Pb2cnf()
  >>> pb2.encode_inc_initial(i_contr, formula, aux_var)