Class Paramita::ClauseContainer¶

A container of clauses.

The variables used in this container are represented as an integer larger than 0 (its identifier), as in the DIMACS CNF format.

A clause is composed by literals, which are a variable or its negation. A negated variable is represented by negating its identifier.

This interface acts as a clause container, in the sense that we can add new clauses and (optionally) keep track on how many clauses we added. No additional assumptions are made on how the container stores them (or even if they are stored at all). Specializations of this interface might provide additional methods to retrieve clauses, but this is not part of the interface.

#include <ClauseContainer.hpp>

Inherits the following classes: Paramita::Plugin

Public Static Attributes¶

Type	Name
constexpr const char *const	m_interface_id = `"Paramita::ClauseContainer"`

Public Static Attributes inherited from Paramita::Plugin¶

See Paramita::Plugin

Type	Name
constexpr const char *const	m_interface_id = `"Paramita::Plugin"`

Public Functions¶

Type	Name
	ClauseContainer () = default Constructor that initializes an empty container.
	ClauseContainer (const ClauseContainer &) = delete Deleted copy constructor (pure interface).
	ClauseContainer (ClauseContainer &&) = delete Deleted move constructor (pure interface).
virtual	add_clause (const Clause & clause) = 0 Add a single clause.
virtual	add_clauses (const std::vector< Clause > & clauses) Add multiple clauses to the container.
virtual	add_lit (Literal lit) Add a clause literal by literal.
virtual ClauseContainer *	clone () Clones the current CNF Container.
virtual std::uint64_t	max_var () const = 0 Get the largest variable used by the container.
virtual int	num_clauses () const Get the number of clauses hold currently by the container.
ClauseContainer &	operator= (const ClauseContainer & container) = delete Deleted copy assignment (pure interface).
ClauseContainer &	operator= (ClauseContainer &&) = delete Deleted move assignment (pure interface).
virtual	set_minimum_var (std::uint64_t var) = 0 Sets the maximum variable known to the container to at least this one.
	~ClauseContainer () override Virtual destructor for the container.

Public Functions inherited from Paramita::Plugin¶

See Paramita::Plugin

Type	Name
	Plugin () = default
	Plugin (const Plugin &) = delete Deleted constructor (pure interface).
	Plugin (Plugin &&) = delete Deleted constructor (pure interface).
virtual ParameterType	get (const std::string & name) Get the parameter's value.
virtual ParameterSpace	get_parameter_space () Get the parameter space for this class.
Plugin &	operator= (const Plugin & container) = delete Deleted constructor (pure interface).
Plugin &	operator= (Plugin &&) = delete Deleted constructor (pure interface).
virtual	set (const std::string & name, const ParameterType & value) Set a parameter.
virtual	~Plugin () = default

Public Static Attributes Documentation¶

variable m_interface_id¶

constexpr const char* const Paramita::ClauseContainer::m_interface_id;

Public Functions Documentation¶

function ClauseContainer [1/3]¶

Constructor that initializes an empty container.

Paramita::ClauseContainer::ClauseContainer () = default

function ClauseContainer [2/3]¶

Deleted copy constructor (pure interface).

Paramita::ClauseContainer::ClauseContainer (
    const ClauseContainer &
) = delete

function ClauseContainer [3/3]¶

Deleted move constructor (pure interface).

Paramita::ClauseContainer::ClauseContainer (
    ClauseContainer &&
) = delete

function add_clause¶

Add a single clause.

virtual Paramita::ClauseContainer::add_clause (
    const Clause & clause
) = 0

The clause is represented as a sequence of literals. Each literal is represented as an integer, where its absolut value is the identifier of a variable. A positive integer represents the variable and a negative integer its negation.

Parameters:

clause The clause to be added to the container.

function add_clauses¶

Add multiple clauses to the container.

virtual Paramita::ClauseContainer::add_clauses (
    const std::vector< Clause > & clauses
)

The default implementation will call add_clause once per element in the vector.

See also: add_clause

Parameters:

clauses The clauses to be added to the container.

function add_lit¶

Add a clause literal by literal.

virtual Paramita::ClauseContainer::add_lit (
    Literal lit
)

This method is intended to be used to add clauses literal by literal. To insert a clause, call add_lit with each literal for the clause, and then commit the clause to the container by using add_lit(0).

See BALYO201645 for more details.

Parameters:

lit The next literal for the current clause being added, or 0 to indicate the end of the clause.

Exception:

UnsupportedMethodException This method is optional.

function clone¶

Clones the current CNF Container.

virtual ClauseContainer * Paramita::ClauseContainer::clone ()

Returns:

The cloned CNF Container.

Exception:

UnsupportedMethodException This method is optional.

function max_var¶

Get the largest variable used by the container.

virtual std::uint64_t Paramita::ClauseContainer::max_var () const = 0

The largest variable is determined by its identifier.

Note:

Note that this does not mean that the container has clauses containing literals for all the variables between 1 and CnfContainerinterface::max_var, there may be gaps.

Warning:

If the container creates variables internally, this method MUST also consider those variables, even if the user did not add them directly. This ensures that the user cannot generate variable clashes when adding new clauses to the container.

Postcondition:

The return value is equal or larger to the absolute value for any literal passed to add_clause, add_clauses, or add_lit.

Returns:

The (positive) integer representing the largest variable.

function num_clauses¶

Get the number of clauses hold currently by the container.

virtual int Paramita::ClauseContainer::num_clauses () const

This method returns the number of clauses that the container currently holds. It is implementation defined, meaning that it does not need to match the number of times that add_clause was called. For example, a simplification could be performed on the clauses, eliminating some of them.

Returns:

The number of clauses held by the container.

Exception:

UnsupportedMethodException This method is optional.

function operator=¶

Deleted copy assignment (pure interface).

ClauseContainer & Paramita::ClauseContainer::operator= (
    const ClauseContainer & container
) = delete

function operator=¶

Deleted move assignment (pure interface).

ClauseContainer & Paramita::ClauseContainer::operator= (
    ClauseContainer &&
) = delete

function set_minimum_var¶

Sets the maximum variable known to the container to at least this one.

virtual Paramita::ClauseContainer::set_minimum_var (
    std::uint64_t var
) = 0

This method can be used to ensure that the container knows a certain variable. If the container internally generates new variables, or if someone relies on the ClauseContainer::max_var method to determine the next free variable, this method ensures that existing variables cannot be reused.

Postcondition:

The value returned by max_var must be larger or equal than the one provided.

Postcondition:

The value returned by max_var cannot be reduced by this call.

Parameters:

var The variable to be registered to the container.

function ~ClauseContainer¶

Virtual destructor for the container.

Paramita::ClauseContainer::~ClauseContainer () override