Class Paramita::CnfToPbDecoder

A decoder from CNF to Pseudo-Boolean (PB) constraints.

A decoder analyzes a CNF formula and reconstructs one or more PB constraints that are semantically equivalent to a subset of the clauses.

The decoder operates on a ClauseContainer and uses a set of target literals from where constraints will be detected.

Note:

Use CNF_TO_PB_DECODER_C_INTERFACE to register any subclass of this interface.

• #include <CnfToPbDecoder.hpp>

Inherits the following classes: Paramita::Plugin

Public Static Attributes

Type	Name
constexpr const char *const	m_interface_id = /* multi line expression */

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
	CnfToPbDecoder () = default
	CnfToPbDecoder (const CnfToPbDecoder &) = delete Deleted copy constructor (pure interface).
	CnfToPbDecoder (CnfToPbDecoder &&) = delete Deleted move constructor (pure interface).
virtual std::vector< PbConstraint >	decode (ClauseContainer & container, std::vector< Literal > target_lits) = 0 Decode PB constraints from a CNF formula.
CnfToPbDecoder &	operator= (const CnfToPbDecoder & container) = delete Deleted copy assignment (pure interface).
CnfToPbDecoder &	operator= (CnfToPbDecoder &&) = delete Deleted move assignment (pure interface).
	~CnfToPbDecoder () 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::CnfToPbDecoder::m_interface_id;

---

Public Functions Documentation

function CnfToPbDecoder [1/3]

Paramita::CnfToPbDecoder::CnfToPbDecoder () = default

---

function CnfToPbDecoder [2/3]

Deleted copy constructor (pure interface).

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

---

function CnfToPbDecoder [3/3]

Deleted move constructor (pure interface).

Paramita::CnfToPbDecoder::CnfToPbDecoder (
    CnfToPbDecoder &&
) = delete

---

function decode

Decode PB constraints from a CNF formula.

virtual std::vector< PbConstraint > Paramita::CnfToPbDecoder::decode (
    ClauseContainer & container,
    std::vector< Literal > target_lits
) = 0

An implementation analyzes the clauses stored in the given ClauseContainer and reconstructs any PB constraints it recognizes. The target_lits parameter is used to restrict the search to constraints involving specific literals.

Parameters:

• container The ClauseContainer containing the CNF formula to analyze.
• target_lits The literals of interest for the decoding process.

Returns:

A vector containing the decoded PB constraints.

---

function operator=

Deleted copy assignment (pure interface).

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

---

function operator=

Deleted move assignment (pure interface).

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

---

function ~CnfToPbDecoder

Paramita::CnfToPbDecoder::~CnfToPbDecoder () override

---