Class VectorClauseDatabase
==========================

Its a default implementation of a Clause Database, in PBLib. Every constraint is saved into a vector of clauses.

.. _vect-cdb:

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


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

  Constructs a vector clause database with the specified configuration. Takes one parameters: a :ref:`PBConfig <pbconfig>`.

  >>> from pypblib.pblib import PBConfig, VectorClauseDatabase
  >>> config = PBConfig()
  >>> formula = VectorClauseDatabase(config)
  >>> formula
  Num. Causes: 0
  ==============================
  ==============================


VectorClauseDatabase(config: :ref:`PBConfig <pbconfig>`, clauses: [[int]])

  Constructs a vector clause database with the specified configuration and save the recieved clauses. Takes two parameters: a :ref:`PBConfig <pbconfig>` and a list of integer's lists. Every list represents a clause in a previous formula.

  >>> from pypblib import pblib
  >>> formula = pblib.VectorClauseDatabase(pblib.PBConfig(),
                          [[1, 2, 3], [4, 5, 6], [7, 8, 9]])
  >>> formula
  Num. Causes: 3
  ==============================
  1 2 3 0
  4 5 6 0
  7 8 9 0
  ==============================


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

+-------------------------------+-----------------------------------------------------------------------------------+
|   Return Type                 |                   Method                                                          |
+===============================+===================================================================================+
|   int                         |   :ref:`get_num_clauses() <get-num-clauses>`                                      |
+-------------------------------+-----------------------------------------------------------------------------------+
|   void                        |   :ref:`print_formula() <print-formula-std>`                                      |
+-------------------------------+-----------------------------------------------------------------------------------+
|   void                        |   :ref:`print_formula(fname: string, nclauses: int) <print-formula-file>`         |
+-------------------------------+-----------------------------------------------------------------------------------+
|   [[int]]                     |   :ref:`get_clauses() <get-clauses>`                                              |
+-------------------------------+-----------------------------------------------------------------------------------+
|   void                        |   :ref:`clear_database() <clear-database>`                                        |
+-------------------------------+-----------------------------------------------------------------------------------+
|   void                        |   :ref:`reset_internal_unsat_state() <reset-internal-unsat-state>`                |
+-------------------------------+-----------------------------------------------------------------------------------+



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

.. _get-num-clauses:

  .. method:: get_num_clauses() -> int

  Returns the number of clauses in database.

  >>> from pypblib import pblib
  >>> config = pblib.PBConfig()
  >>> cl = [[1, -2, 3], [4, -5, 6], [2, -4,]]
  >>> formula = pblib.VectorClauseDatabase(config, cl)
  >>> formula.get_num_clauses()
  3


.. _get-clauses:

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

  Returns a list of integer's lists to represents the clauses in VectorClauseDatabase.

  >>> from pypblib import pblib
  >>> config = pblib.PBConfig()
  >>> formula = pblib.VectorClauseDatabase(config,
                [[1, -2, 3], [4, -5, 6], [7, -8, 9]])
  >>> clauses = formula.get_clauses()
  >>> print(clauses)
  [[1, -2, 3], [4, -5, 6], [7, -8, 9]]


.. _print-formula-std:

  .. method:: print_formula()

  Prints the codification into standard output.

  >>> from pypblib import pblib
  >>> config = pblib.PBConfig()
  >>> cl = [[1, -2, 3], [4, -5, 6], [2, -4,]]
  >>> formula = pblib.VectorClauseDatabase(config, cl)
  >>> formula.print_formula()
   1 -2 3 0
   4 -5 6 0
   2 -4 0


.. _print-formula-file:

  .. method:: print_formula(fname: string, nclauses: int)

  Prints the codification into a file with specified name.


.. _clear-database:

  .. method:: clear_database()

  Resets the clause database.

  >>> from pypblib import pblib
  >>> config = pblib.PBConfig()
  >>> cl = [[1, -2, 3], [4, -5, 6], [2, -4,]]
  >>> formula = pblib.VectorClauseDatabase(config, cl)
  >>> formula.print_formula()
   1 -2 3 0
   4 -5 6 0
   2 -4 0
  >>> formula.clear_database()
  >>> formula.print_formula()
  >>>


.. _reset-internal-unsat-state:

  .. method:: reset_internal_unsat_state()

  Sets the internal unsat state to false.

  >>> from pypblib import pblib
  >>> config = pblib.PBConfig()
  >>> cl = [[1, -2, 3], [4, -5, 6], [2, -4,]]
  >>> formula = pblib.VectorClauseDatabase(config, cl)
  >>> formula.reset_internal_unsat_state()