6. Class VectorClauseDatabase

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

6.1. Constructor

VectorClauseDatabase(config: PBConfig)

Constructs a vector clause database with the specified configuration. Takes one parameters: a PBConfig.

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

VectorClauseDatabase(config: PBConfig, clauses: [[int]])

Constructs a vector clause database with the specified configuration and save the recieved clauses. Takes two parameters: a 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
==============================

6.2. Methods summary

Return Type	Method
int	get_num_clauses()
void	print_formula()
void	print_formula(fname: string, nclauses: int)
[[int]]	get_clauses()
void	clear_database()
void	reset_internal_unsat_state()

6.3. Methods details

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() → [[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()

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(fname: string, nclauses: int)

Prints the codification into a file with specified name.

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()

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()