Class PBConfig
==============

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

.. _pbconfig:

PBConfig()

  An instance of a PBConfig class contains the configuration for all options in PBLib.
  The following is its default setting:

  >>> from pypblib import pblib
  >>> c = pblib.PBConfig()
  >>> c
  PBConfig:
  ========
  PB_Encoder = BEST
  AMK_Encoder = BEST
  AMO_Encoder = BEST
  BIMANDER_M_IS = N_HALF
  bimander = 3
  k product min lit cnt for splitting = 10
  K product k = 2
  Commander encoding k = 3
  Max clause per constraint = 1000000
  Use formula cache = FALSE
  Print used encoding = FALSE
  Check for duplicate literals = FALSE
  Use gac Binary Merge = FALSE
  Binary merge no support for single bits = TRUE
  Use recursive BDD test = FALSE
  Use real robdds = TRUE
  Use watch dog encoding in Binary Merger = FALSE


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

+---------------------------------------------------+------------------------------------------------------------------------------------+
|   Return_Type                                     |                        Method                                                      |
+===================================================+====================================================================================+
|   void                                            | :ref:`set_PB_Encoder <set-PB-Encoder>` (:ref:`PB_Encoder <pb-encoder-const>`)      |
+---------------------------------------------------+------------------------------------------------------------------------------------+
|   void                                            | :ref:`set_AMK_Encoder <set-AMK-Encoder>` (:ref:`AMK_Encoder <amk-encoder-const>`)  |
+---------------------------------------------------+------------------------------------------------------------------------------------+
|   void                                            | :ref:`set_AMO_Encoder <set-AMO-Encoder>` (:ref:`AMO_Encoder <amo-encoder-const>`)  |
+---------------------------------------------------+------------------------------------------------------------------------------------+
|   void                                            | :ref:`set_Bimander <set-bimander>` (:ref:`Bimander_M_IS <bimander-m-is-const>`)    |
+---------------------------------------------------+------------------------------------------------------------------------------------+
|   void                                            | :ref:`set_Bimander_m <set-bimander-m>` (int: m)                                    |
+---------------------------------------------------+------------------------------------------------------------------------------------+
|   void                                            | :ref:`set_k_product_minimum_lit_count_for_splitting(min_lits:int) <set-k-min-lit>` |
+---------------------------------------------------+------------------------------------------------------------------------------------+
|   void                                            | :ref:`set_k_product_k(k: int) <set-kproduct-k>`                                    |
+---------------------------------------------------+------------------------------------------------------------------------------------+
|   void                                            | :ref:`set_commander_encoding_k(k: int) <set-commander-encoding-k>`                 |
+---------------------------------------------------+------------------------------------------------------------------------------------+
|   void                                            | :ref:`set_max_clause_per_constraint(max: int) <set-max-clause>`                    |
+---------------------------------------------------+------------------------------------------------------------------------------------+
|   void                                            | :ref:`set_use_formula_cache(use: bool) <set-use-formula-cache>`                    |
+---------------------------------------------------+------------------------------------------------------------------------------------+
|   void                                            | :ref:`check_for_dup_literals(check: bool) <check-for-dup-lit>`                     |
+---------------------------------------------------+------------------------------------------------------------------------------------+
|   void                                            | :ref:`use_gac_binary_merge(use: bool) <use-gac-bin-merge>`                         |
+---------------------------------------------------+------------------------------------------------------------------------------------+
|   void                                            | :ref:`binary_merge_no_support_for_single_bits(support: bool) <bin-merge-no-suport>`|
+---------------------------------------------------+------------------------------------------------------------------------------------+
|   void                                            | :ref:`use_recursive_BDD_test(use: bool) <use-recursive-BDD-test>`                  |
+---------------------------------------------------+------------------------------------------------------------------------------------+
|   void                                            | :ref:`use_real_robdds(use: bool) <use-real-robdds>`                                |
+---------------------------------------------------+------------------------------------------------------------------------------------+
|   void                                            | :ref:`use_watch_dog_encoding_in_binary_merger(use: bool) <use-watch-dog-bin-mer>`  |
+---------------------------------------------------+------------------------------------------------------------------------------------+



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

.. _set-PB-Encoder:

  .. method:: set_PB_Encoder(pb_encoder)

  Sets the :ref:`PB_Encoder <pb-encoder-const>` configuration.
  By default: pypblib.pblib.PB_BEST

    >>> from pypblib import pblib
    >>> config = pblib.PBConfig()
    >>> config.set_PB_Encoder(pblib.PB_BDD)

.. _set-AMK-Encoder:

  .. method:: set_AMK_Encoder(amk_encoder)

  Sets the :ref:`AMK_Encoder <amk-encoder-const>` configuration.
  By default: pypblib.pblib.AMK_BEST

    >>> from pypblib import pblib
    >>> config = pblib.PBConfig()
    >>> config.set_AMK_Encoder(pblib.AMK_CARD)

.. _set-AMO-Encoder:

  .. method:: set_AMO_Encoder(amo_encoder)

  Sets the :ref:`AMO_Encoder <amo-encoder-const>` configuration.
  By default: pypblib.pblib.AMO_BEST

    >>> from pypblib import pblib
    >>> config = pblib.PBConfig()
    >>> config.set_AMO_Encoder(pblib.AMO_NESTED)

.. _set-bimander:

  .. method:: set_Bimander(bimander_encode)

  Sets the :ref:`BIMANDER_M_IS <bimander-M-IS-const>` configuration.
  By default: pypblib.pblib.N_HALF

    >>> from pypblib import pblib
    >>> config = pblib.PBConfig()
    >>> config.set_Bimander(pblib.FIXED)

.. _set-bimander-m:

  .. method:: set_bimander_m(m: int)

  Sets bimander m. Defalut value is 3.

   >>> from pypblib import pblib
   >>> config = pblib.PBConfig()
   >>> config.set_bimander_m(5)

.. _set-k-min-lit:

  .. method:: set_k_product_minimum_lit_count_for_splitting(nim_lits: int)

  Sets k-product minimum literals for splitting. Default value is 10.

  >>> from pypblib import pblib
  >>> config = pblib.PBConfig()
  >>> config.set_k_product_minimum_lit_count_for_splitting(12)


.. _set-kproduct-k:

  .. method:: set_k_product_k(k: int)

  Sets the k value for k-product. Default value is 2.

  >>> from pypblib import pblib
  >>> config = pblib.PBConfig()
  >>> config.set_kproduct_k(4)

.. _set-commander-encoding-k:

  .. method:: set_commander_encoding_k(k: int)

  Sets the k value of commander encoding. Default value is 3.

  >>> from pypblib import pblib
  >>> config = pblib.PBConfig()
  >>> config.set_commander_encoding_k(5)

.. _set-max-clause:

  .. method:: set_max_clause_per_constraint(max: int)

  Sets the maximum number of clauses per constraint. Default value is 1000000.

  >>> from pypblib import pblib
  >>> config = pblib.PBConfig()
  >>> config.set_max_clause_per_constraint(2000000)


.. _set-use-formula-cache:

  .. method:: set_use_formula_cache(use: bool)

  Sets the use of formula cache. False by default.

  >>> from pypblib import pblib
  >>> config = pblib.PBConfig()
  >>> config.set_use_formula_cache(True)


.. _check-for-dup-lit:

  .. method:: check_for_dup_literals(check: bool)

  Sets the check for duplicated literals. False by default.

  >>> from pypblib import pblib
  >>> config = pblib.PBConfig()
  >>> config.check_for_dup_literals(True)


.. _use-gac-bin-merge:

  .. method:: use_gac_binary_merge(use: bool)

  Sets the use of GAC (generalized arc-consistent). False by default.

  >>> from pypblib import pblib
  >>> config = pblib.PBConfig()
  >>> config.use_gac_binary_merge(True)


.. _bin-merge-no-suport:

  .. method:: binary_merge_no_support_for_single_bits(support: bool)

  True by default.

  >>> from pypblib import pblib
  >>> config = pblib.PBConfig()
  >>> config.binary_merge_no_support_for_single_bits(False)

.. _use-recursive-BDD-test:

  .. method:: use_recursive_BDD_test(use: bool)

  False by default.

  >>> from pypblib import pblib
  >>> config = pblib.PBConfig()
  >>> config.use_recursive_BDD_test(True)

.. _use-real-robdds:

  .. method:: use_real_robdds(use: bool)

  True by default.

  >>> from pypblib import pblib
  >>> config = pblib.PBConfig()
  >>> config.use_real_robdds(False)

.. _use-watch-dog-bin-mer:

  .. method:: use_watch_dog_encoding_in_binary_merger(use: bool)

  False by default.

  >>> from pypblib import pblib
  >>> config = pblib.PBConfig()
  >>> config.use_watch_dog_encoding_in_binary_merger(True)