Class Paramita::PbToCnfEncoder

An encoder from PB constraints to Satisfiability CNF.

Note:

Use PB_TO_CNF_ENCODER_C_INTERFACE to register any subclass of this interface.

• #include <PbToCnfEncoder.hpp>

Inherits the following classes: Paramita::Plugin

Classes

Type	Name
class	ContextState Opaque type for storing arbitrary context for incremental encoders.

Public Types

Type	Name
typedef std::unique_ptr< ContextState >	Context

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
	PbToCnfEncoder () = default
	PbToCnfEncoder (const PbToCnfEncoder &) = delete Deleted copy constructor (pure interface).
	PbToCnfEncoder (PbToCnfEncoder &&) = delete Deleted move constructor (pure interface).
virtual Context	encode (const PbConstraint & constraint, ClauseContainer & container, Context context) = 0 Encode the PB constraint to the specified container.
PbToCnfEncoder &	operator= (const PbToCnfEncoder & container) = delete Deleted copy assignment (pure interface).
PbToCnfEncoder &	operator= (PbToCnfEncoder &&) = delete Deleted move assignment (pure interface).
	~PbToCnfEncoder () 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 Types Documentation

typedef Context

using Paramita::PbToCnfEncoder::Context =  std::unique_ptr<ContextState>;

---

Public Static Attributes Documentation

variable m_interface_id

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

---

Public Functions Documentation

function PbToCnfEncoder [1/3]

Paramita::PbToCnfEncoder::PbToCnfEncoder () = default

---

function PbToCnfEncoder [2/3]

Deleted copy constructor (pure interface).

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

---

function PbToCnfEncoder [3/3]

Deleted move constructor (pure interface).

Paramita::PbToCnfEncoder::PbToCnfEncoder (
    PbToCnfEncoder &&
) = delete

---

function encode

Encode the PB constraint to the specified container.

virtual Context Paramita::PbToCnfEncoder::encode (
    const PbConstraint & constraint,
    ClauseContainer & container,
    Context context
) = 0

This method receives an optional Context that the encoder can use to encode constraints incrementally.

In this sense, it can also return another Context to be used by the same encoder later.

Non-incremental encoders can fully ignore the Context, both as parameter and return value.

Parameters:

• constraint The PbConstraint to be encoded to CNF.
• container A ClauseContainer where clauses will be added.
• context An (possibly empty) Context for incremental encoders.

Returns:

A (possibly empty) Context to be used by the same encoder to incrementally encode constraints in subsequent calls.

---

function operator=

Deleted copy assignment (pure interface).

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

---

function operator=

Deleted move assignment (pure interface).

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

---

function ~PbToCnfEncoder

Paramita::PbToCnfEncoder::~PbToCnfEncoder () override

---