Class Paramita::WClauseContainer¶

A container of weighted clauses. A clause is a multiset of literals.

#include <WClauseContainer.hpp>

Inherits the following classes: Paramita::Plugin

Public Static Attributes¶

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

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
	WClauseContainer () = default
	WClauseContainer (const WClauseContainer &) = delete
	WClauseContainer (WClauseContainer &&) = delete
virtual	add_clause (const Clause & clause, Weight weight) = 0 Add a single clause with the specified weight.
virtual	add_clauses (const std::vector< Clause > & clauses, Weight weight) Add multiple clauses to the container.
virtual	add_lit (Literal lit) Add a clause literal by literal.
virtual	add_soft_lit (Literal lit, std::uint64_t weight) Declare a literal as a soft literal with a weight.
virtual	add_weight (Weight weight) Changes the weight for the next clause that is added literal by literal.
virtual WClauseContainer *	clone () Clones the current container.
virtual std::uint64_t	max_var () const = 0 Get the largest variable used in the container.
virtual std::unordered_map< Weight, int >	num_clauses () const Obtain the distribution of clauses hold by the container over weights.
WClauseContainer &	operator= (const WClauseContainer & container) = delete
WClauseContainer &	operator= (WClauseContainer &&) = delete
virtual	set_minimum_var (std::uint64_t var) = 0 Sets the maximum variable known to the container to at least this one.
	~WClauseContainer () override

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::WClauseContainer::m_interface_id;

Public Functions Documentation¶

function WClauseContainer [1/3]¶

Paramita::WClauseContainer::WClauseContainer () = default

function WClauseContainer [2/3]¶

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

function WClauseContainer [3/3]¶

Paramita::WClauseContainer::WClauseContainer (
    WClauseContainer &&
) = delete

function add_clause¶

Add a single clause with the specified weight.

virtual Paramita::WClauseContainer::add_clause (
    const Clause & clause,
    Weight weight
) = 0

Parameters:

clause The clause to be added to the container.
weight The associated weight for this clause.

function add_clauses¶

Add multiple clauses to the container.

virtual Paramita::WClauseContainer::add_clauses (
    const std::vector< Clause > & clauses,
    Weight weight
)

Parameters:

clauses The clauses to be added to the container.
weight The associated weight for the clauses.

function add_lit¶

Add a clause literal by literal.

virtual Paramita::WClauseContainer::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).

Postcondition:

After add_lit(0), the clause is added with the weight specified previously with add_weight.

See ipamir2022 and 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 add_soft_lit¶

Declare a literal as a soft literal with a weight.

virtual Paramita::WClauseContainer::add_soft_lit (
    Literal lit,
    std::uint64_t weight
)

This function declares a literal as a soft literal in the underlying MaxSAT formula. Assigning the literal to true incurs cost weight.

If the literal is already set in the formula, this overrides the previous cost the literal had.

See ipamir2022 for more details.

Parameters:

lit The soft literal.
weight The new weight for the literal.

function add_weight¶

Changes the weight for the next clause that is added literal by literal.

virtual Paramita::WClauseContainer::add_weight (
    Weight weight
)

See also: add_lit

Parameters:

weight The weight for the next clause.

Exception:

UnsupportedMethodException This method is optional.

function clone¶

Clones the current container.

virtual WClauseContainer * Paramita::WClauseContainer::clone ()

Returns:

The cloned container.

Exception:

UnsupportedMethodException This method is optional.

function max_var¶

Get the largest variable used in the container.

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

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 assigned to the largest variable.

function num_clauses¶

Obtain the distribution of clauses hold by the container over weights.

virtual std::unordered_map< Weight, int > Paramita::WClauseContainer::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 map with the distribution of clauses.

function operator=¶

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

function operator=¶

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

function set_minimum_var¶

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

virtual Paramita::WClauseContainer::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 WClauseContainer::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 ~WClauseContainer¶

Paramita::WClauseContainer::~WClauseContainer () override