Class IncPBConstraint
=====================

.. _i-pbconstr:

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

IncPBConstraint(weightedlits: [:ref:`WeightedLits <weighted-lit>`], :ref:`comparator <pb-comparator>`, bound: int)

  Creates an object to represents a Pseudo-Boolean incremental costraint.

  >>> from pypblib import pblib
  >>> wl1 = pblib.WeightedLit(1, 2)
  >>> wl2 = pblib.WeightedLit(2,-1)
  >>> wl3 = pblib.WeightedLit(3, 3)
  >>> i_constr = pblib.IncPBConstraint([wl1, wl2, wl3],
                                        pblib.LEQ, 3)
  >>> i_constr
  +2x1-1x2+3x3<=3


IncPBConstraint(weightedlits: [:ref:`WeightedLits <weighted-lit>`], :ref:`comparator <pb-comparator>`, bound_geq: int, bound_leq: int)

  Creates an object to represents a Pseudo-Boolean incremental costraint, in case :ref:`pblib.BOTH <pb-comparator>` comparator and bound less-equals and greater-equal are different.

  >>> from pypblib import pblib
  >>> wl1 = pblib.WeightedLit(1, 2)
  >>> wl2 = pblib.WeightedLit(2,-1)
  >>> wl3 = pblib.WeightedLit(3, 3)
  >>> i_constr = pblib.IncPBConstraint([wl1, wl2, wl3],
                                        pblib.BOTH, 3, -1)
  >>> i_constr
  -1<=+2x1-1x2+3x3<=3


Methods summary
---------------

+----------------------------------+-----------------------------------------------------------------------------------------------------+
|    Return Type                   |                            Method                                                                   |
+==================================+=====================================================================================================+
|   void                           | :ref:`add_conditional(cond: int) <i-add-conditional>`                                               |
+----------------------------------+-----------------------------------------------------------------------------------------------------+
|   void                           | :ref:`add_conditionals(conds: [int]) <i-add-conditionals>`                                          |
+----------------------------------+-----------------------------------------------------------------------------------------------------+
|   [int]                          | :ref:`get_conditionals() <i-get-conditionals>`                                                      |
+----------------------------------+-----------------------------------------------------------------------------------------------------+
|   void                           | :ref:`clear_conditionals() <i-clear-conditionals>`                                                  |
+----------------------------------+-----------------------------------------------------------------------------------------------------+
|:ref:`comparator<pb-comparator>`  | :ref:`get_comparator() <get-comparator>`                                                            |
+----------------------------------+-----------------------------------------------------------------------------------------------------+
|   long                           | :ref:`get_leq() <get-leq>`                                                                          |
+----------------------------------+-----------------------------------------------------------------------------------------------------+
|   long                           | :ref:`get_geq() <get-geq>`                                                                          |
+----------------------------------+-----------------------------------------------------------------------------------------------------+
|   void                           | :ref:`set_comparator <set-comparator>` (:ref:`comparator <pb-comparator>`)                          |
+----------------------------------+-----------------------------------------------------------------------------------------------------+
|   void                           | :ref:`encode_new_geq(geq: long, VectorClauseDatabase: formula, AuxVarManager: aux) <encode-new-geq>`|
+----------------------------------+-----------------------------------------------------------------------------------------------------+
|   void                           | :ref:`encode_new_leq(leq: long, VectorClauseDatabase: formula, AuxVarManager: aux) <encode-new-leq>`|
+----------------------------------+-----------------------------------------------------------------------------------------------------+
|:ref:`PBConstraint<pb-constraint>`| :ref:`get_non_inc_constraint() <get-non-inc-constraint>`                                            |
+----------------------------------+-----------------------------------------------------------------------------------------------------+
|:ref:`IncPBConstraint<i-pbconstr>`| :ref:`get_geq_inc_constraint() <get-geq-iconstraint>`                                               |
+----------------------------------+-----------------------------------------------------------------------------------------------------+
|:ref:`IncPBConstraint<i-pbconstr>`| :ref:`get_leq_inc_constraint() <get-leq-iconstraint>`                                               |
+----------------------------------+-----------------------------------------------------------------------------------------------------+
|   int                            | :ref:`get_n() <i-get-n>`                                                                            |
+----------------------------------+-----------------------------------------------------------------------------------------------------+


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

.. _i-add-conditional:

 .. method:: add_conditional(cond: int)

  Adds a conditional to the incremental constraint.

  >>> from pypblib import pblib
  >>> wl1 = pblib.WeightedLit(1,-3)
  >>> wl2 = pblib.WeightedLit(2, 1)
  >>> wl3 = pblib.WeightedLit(3, 2)
  >>> i_constr = pblib.IncPBConstraint([wl1, wl2, wl3],
                                        pblib.LEQ, 1)
  >>> i_constr
  -3x1+x2+2x3<=1
  >>> i_constr.add_conditional(3)

.. _i-add-conditionals:

 .. method:: add_conditionals(conds: [int])

  Adds a list of conditionals to the incremental constraint.

  >>> from pypblib import pblib
  >>> wl1 = pblib.WeightedLit(1,-3)
  >>> wl2 = pblib.WeightedLit(2, 1)
  >>> wl3 = pblib.WeightedLit(2, 2)
  >>> i_constr = pblib.IncPBConstraint([wl1, wl2, wl3],
                                        pblib.LEQ, 1)
  >>> i_constr.add_conditionals([2, 3])


.. _i-get-conditionals:

 .. method:: get_conditionals() -> [int]

  Returns a list of incremental conditionals.

  >>> from pypblib import pblib
  >>> wl1 = pblib.WeightedLit(1, 2)
  >>> wl2 = pblib.WeightedLit(2, 3)
  >>> wl3 = pblib.WeightedLit(3, -1)
  >>> i_constr = pblib.IncPBConstraint([wl1, wl2, wl3],
                                        pblib.LEQ, 2)
  >>> i_constr.add_conditionals([1, 3])
  >>> i_constr.get_conditionals()
  [1, 3]

.. _i-clear-conditionals:

 .. method:: clear_conditionals()

  Removes all conditionals in a incremental constraint.

  >>> from pypblib import pblib
  >>> wl1 = pblib.WeightedLit(1, 2)
  >>> wl2 = pblib.WeightedLit(2, 3)
  >>> wl3 = pblib.WeightedLit(3, -1)
  >>> i_constr = pblib.IncPBConstraint([wl1, wl2, wl3],
                                        pblib.LEQ, 2)
  >>> i_constr.add_conditionals([1, 3])
  >>> i_constr.get_conditionals()
  [1, 3]
  >>> i_constr.clear_conditionals()
  >>> cond = i_constr.get_conditionals()
  []

.. _i-get-comparator:

  .. method:: get_comparator() -> comparator

  Returns an int to represents the :ref:`comparator <pb-comparator>` (GEQ = 0, LEQ = 1 and BOTH = 2).

  >>> from pypblib import pblib
  >>> wl1 = pblib.WeightedLit(1, 1)
  >>> wl2 = pblib.WeightedLit(2, 1)
  >>> i_constr = pblib.IncPBConstraint([wl1, wl2],
                                    pblib.GEQ, 1)
  >>> comp = i_constr.get_comparator()
  >>> print(comp)
  0

.. _i-get-leq:

  .. method:: get_leq() -> long

  Returns the less-equal value bound of the incremental constraint.


  >>> from pypblib import pblib
  >>> wl1 = pblib.WeightedLit(1, 1)
  >>> wl2 = pblib.WeightedLit(2, 1)
  >>> i_constr = pblib.PBConstraint([wl1, wl2],
                                pblib.LEQ, 1)
  >>> n = i_constr.get_leq()
  >>> print(n)
  1

.. _i-get-geq:

  .. method:: get_geq() -> long

  Returns the greater-equal value bound of the incremental constraint.

  >>> from pypblib import pblib
  >>> wl1 = pblib.WeightedLit(1, 1)
  >>> wl2 = pblib.WeightedLit(2, 1)
  >>> i_constr = pblib.PBConstraint([wl1, wl2],
                                pblib.GEQ, 0)
  >>> n = i_constr.get_geq()
  >>> print(n)
  0

.. _i-set-comparator:

  .. method:: set_comparator(comparator)

  Sets the incremental constraint's :ref:`comparator <pb-comparator>` to specified value.

  >>> from pypblib import pblib
  >>> wl1 = pblib.WeightedLit(1, 1)
  >>> wl2 = pblib.WeightedLit(2, 1)
  >>> wl3 = pblib.WeightedLit(3, -1)
  >>> wls = [wl1, wl2, wl3]
  >>> i_constr = pblib.IncPBConstraint(wls,
                                pblib.LEQ, 4)
  >>> print(i_constr.get_comparator())
  1
  >>> i_constr.set_comparator(pblib.GEQ)
  >>> print(i_constr.get_comparator())
  0

.. _encode-new-geq:

  .. method:: encode_new_geq(geq_bound: long, VectorClauseDatabase: formula, AuxVarManager: aux_var)

  After the initial encoding of an incremental pseudo-boolean constraint, it is possible to encode a new (tighter) bounds with this method.
  Encodes an incremental constraint with a new greater-equal bound.

Example::

    #!/usr/bin/env python3
    # -*- coding: utf-8 -*-

    from pypblib import pblib

    #
    ###############################################################################

    def test_formula():
        wl1 = pblib.WeightedLit(1, 1)
        wl2 = pblib.WeightedLit(2, 1)
        wl3 = pblib.WeightedLit(3, 1)
        wl4 = pblib.WeightedLit(4, -1)
        wl5 = pblib.WeightedLit(5, -1)
        wls = [wl1, wl2, wl3, wl4, wl5]
        config = pblib.PBConfig()
        aux_var = pblib.AuxVarManager(6)
        formula = pblib.VectorClauseDatabase(config)
        geq = 1
        config.set_PB_Encoder(pblib.PB_SORTINGNETWORKS)

        i_const = pblib.IncPBConstraint(wls, pblib.GEQ, 0)
        pb2 = pblib.Pb2cnf(config)

        pb2.encode_inc_initial(i_const, formula, aux_var)
        formula.print_formula("test1.cnf", aux_var.get_biggest_returned_auxvar())

        i_const.encode_new_geq(geq, formula, aux_var)
        formula.print_formula("test2.cnf", aux_var.get_biggest_returned_auxvar())


    #
    ###############################################################################

    test_formula()


.. _encode-new-leq:

  .. method:: encode_new_leq(leq_bound: long, VectorClauseDatabase: formula, AuxVarManager: aux_var)

  After the initial encoding of an incremental pseudo-boolean constraint, it is possible to encode a new (tighter) bounds with this method.
  Encodes an incremental constraint with a new leq bound.

Example::

    #!/usr/bin/env python3
    # -*- coding: utf-8 -*-

    from pypblib import pblib

    #
    ###############################################################################

    def test_formula():
        wl1 = pblib.WeightedLit(1, 1)
        wl2 = pblib.WeightedLit(2, 1)
        wl3 = pblib.WeightedLit(3, 1)
        wl4 = pblib.WeightedLit(4, 1)
        wl5 = pblib.WeightedLit(5, 1)
        wls = [wl1, wl2, wl3, wl4, wl5]
        config = pblib.PBConfig()
        aux_var = pblib.AuxVarManager(6)
        formula = pblib.VectorClauseDatabase(config)
        leq = 3
        config.set_PB_Encoder(pblib.PB_SORTINGNETWORKS)

        i_const = pblib.IncPBConstraint(wls, pblib.LEQ, 4)
        pb2 = pblib.Pb2cnf(config)

        pb2.encode_inc_initial(i_const, formula, aux_var)
        formula.print_formula("test1.cnf", aux_var.get_biggest_returned_auxvar())

        i_const.encode_new_leq(leq, formula, aux_var)
        formula.print_formula("test2.cnf", aux_var.get_biggest_returned_auxvar())


        #
        ###############################################################################

    test_formula()


.. _get-non-inc-constraint:

  .. method:: get_non_inc_constraint -> PBConstraint

  Returns a new PBConstraint with the same atributes (weighted literals, comparator and bounds) of the IncPBConstraint which takes as a parameter.

  >>> from pypblib import pblib
  >>> wl1 = pblib.WeightedLit(1, 2)
  >>> wl2 = pblib.WeightedLit(2, 2)
  >>> wl3 = pblib.WeightedLit(3, 2)
  >>> i_constr = pblib.IncPBConstraint([wl1, wl2, wl3], pblib.LEQ, 2)
  >>> i_constr
  +2x1+2x2+2x3<=2
  >>> type(i_constr)
  <class 'pypblib.pblib.IncPBConstraint'>
  >>> constr = i_constr.get_non_inc_constraint()
  >>> constr
  +2x1+2x2+2x3<=2
  >>> type(constr)
  <class 'pypblib.pblib.PBConstraint'>


.. _get-geq-iconstraint:

  .. method:: get_geq_inc_constraint() -> IncPBConstraint

  Takes an incremental pseudo boolean constraint and returns a new IncPBConstraint changing the comparator to a greater-equal.
  However, the bound does not change. If the greater-equal bound is equal to zero (because the previous incremental restriction had not been assigned any value), the bound will remain zero.

  >>> from pypblib import pblib
  >>> wl1 = pblib.WeightedLit(1, 2)
  >>> wl2 = pblib.WeightedLit(2, 2)
  >>> wl3 = pblib.WeightedLit(3, 2)
  >>> i_constr = pblib.IncPBConstraint([wl1, wl2, wl3], pblib.LEQ, 2)
  >>> i_constr
  +2x1+2x2+2x3<=2
  >>> i_constr2 = i_constr.get_geq_inc_constraint()
  >>> i_constr2
  +2x1+2x2+2x3>=0


.. _get-leq-iconstraint:

  .. method:: get_leq_inc_constraint() -> IncPBConstraint

  Takes an incremental pseudo boolean constraint and returns a new IncPBConstraint changing the comparator to a less-equal.
  However, the bound does not change. If the less-equal bound is equal to zero (because the previous incremental restriction had not been assigned any value), the bound will remain zero.

  >>> from pypblib import pblib
  >>> wl1 = pblib.WeightedLit(1, 2)
  >>> wl2 = pblib.WeightedLit(2, 2)
  >>> wl3 = pblib.WeightedLit(3, 2)
  >>> i_constr = pblib.IncPBConstraint([wl1, wl2, wl3], pblib.GEQ, 4)
  >>> i_constr
  +2x1+2x2+2x3>=4
  >>> i_constr2 = i_constr.get_leq_inc_constraint()
  >>> i_constr2
  +2x1+2x2+2x3<=0


.. _i-get-n:

 .. method:: get_n() -> int

  Returns the number of weigted literals in the incremental constraint.

  >>> from pypblib import pblib
  >>> wl1 = pblib.WeightedLit(1, 2)
  >>> wl2 = pblib.WeightedLit(2, 3)
  >>> wl3 = pblib.WeightedLit(3, -1)
  >>> i_constr = pblib.IncPBConstraint([wl1, wl2, wl3],
                                        pblib.LEQ, 2)
  >>> i_constr.get_n()
  3