Namespace Paramita

Namespaces

Type	Name
namespace	OutData
namespace	Testing

Classes

Type	Name
class	BooleanParameter Represents a boolean-valued parameter.
class	CategoricalParameter Represents a categorical parameter with discrete choices.
class	ClauseContainer A container of clauses.
class	CnfToPbDecoder A decoder from CNF to Pseudo-Boolean (PB) constraints.
class	IntegerParameter Represents an integer-valued parameter with a range of valid values.
struct	InterfaceInfo
class	InterfaceParameter <typename T>
class	Learner Interface for components that consume learnt clauses.
class	MaxSatSolver An incremental MaxSAT solver.
class	NonIncrMaxSatSolver A MaxSAT solver.
class	NonIncrSatSolver A SAT solver.
class	NotSolvedException
class	Parameter Base class for all parameter types.
class	ParameterSpace Manages a collection of parameters, each identified by a unique name.
struct	PbConstraint A Pseudo-Boolean (PB) constraint.
class	PbToCnfEncoder An encoder from PB constraints to Satisfiability CNF.
class	Plugin Provides capabilities to tweak parameters from the inheriting class.
class	Propagator Interface for implementing external propagation.
class	Range <typename T> Represents a range of values (inclusive).
class	RealParameter Represents a floating-point parameter with range constraints.
class	SatSolver An incremental SAT Solver.
struct	SolvingBudget A budget for the underlying solver.
class	UnsatisfiableException
class	UnsupportedMethodException The method is not implemented for this extension.
class	WClauseContainer A container of weighted clauses. A clause is a multiset of literals.

Public Types

Type	Name
typedef std::vector< Literal >	Clause
typedef InterfaceParameter< ClauseContainer >	ClauseContainerParameter Represents a ClauseContainer .
typedef std::int64_t	Literal
enum	MAXSAT_ANSWER Represents the answer for a MaxSAT solve call.
typedef InterfaceParameter< NonIncrMaxSatSolver >	NonIncrMaxSatSolverParameter Represents a NonIncrMaxSatSolver .
typedef InterfaceParameter< NonIncrSatSolver >	NonIncrSatSolverParameter Represents a NonIncrSatSolver .
typedef std::variant< std::string, int, float, bool, std::shared_ptr< SatSolver >, std::shared_ptr< NonIncrSatSolver >, std::shared_ptr< ClauseContainer >, std::shared_ptr< NonIncrMaxSatSolver >, std::shared_ptr< WClauseContainer >, std::shared_ptr< PbToCnfEncoder >, std::shared_ptr< Plugin > >	ParameterType Type definition for handling parameters of various types.
typedef InterfaceParameter< PbToCnfEncoder >	PbToCnfEncoderParameter Represents a PbToCnfEncoder .
typedef InterfaceParameter< Plugin >	PluginParameter Represents a Plugin .
enum std::uint8_t	SPECIAL_WEIGHTS
typedef InterfaceParameter< SatSolver >	SatSolverParameter Represents a SatSolver .
typedef InterfaceParameter< WClauseContainer >	WClauseContainerParameter Represents a WClauseContainer .
typedef std::variant< std::uint64_t, SPECIAL_WEIGHTS >	Weight

Public Attributes

Type	Name
constexpr int	paramita_interfaces_version = 1

Public Functions

Type	Name
auto	visit_parameter (const std::shared_ptr< Parameter > & ptr, Visitor && visitor)
auto	visit_parameter (const Parameter & param, Visitor && visitor)

Public Types Documentation

typedef Clause

using Paramita::Clause = typedef std::vector<Literal>;

---

typedef ClauseContainerParameter

Represents a ClauseContainer .

using Paramita::ClauseContainerParameter = typedef InterfaceParameter<ClauseContainer>;

---

typedef Literal

using Paramita::Literal = typedef std::int64_t;

---

enum MAXSAT_ANSWER

Represents the answer for a MaxSAT solve call.

enum Paramita::MAXSAT_ANSWER {
    UNKNOWN,
    SATISFIABLE,
    UNSATISFIABLE,
    OPTIMAL
};

See also: NonIncrMaxSatSolver::solve for more details on each value.

---

typedef NonIncrMaxSatSolverParameter

Represents a NonIncrMaxSatSolver .

using Paramita::NonIncrMaxSatSolverParameter = typedef InterfaceParameter<NonIncrMaxSatSolver>;

---

typedef NonIncrSatSolverParameter

Represents a NonIncrSatSolver .

using Paramita::NonIncrSatSolverParameter = typedef InterfaceParameter<NonIncrSatSolver>;

---

typedef ParameterType

Type definition for handling parameters of various types.

using Paramita::ParameterType = typedef std::variant< std::string, int, float, bool, std::shared_ptr<SatSolver>, std::shared_ptr<NonIncrSatSolver>, std::shared_ptr<ClauseContainer>, std::shared_ptr<NonIncrMaxSatSolver>, std::shared_ptr<WClauseContainer>, std::shared_ptr<PbToCnfEncoder>, std::shared_ptr<Plugin> >;

---

typedef PbToCnfEncoderParameter

Represents a PbToCnfEncoder .

using Paramita::PbToCnfEncoderParameter = typedef InterfaceParameter<PbToCnfEncoder>;

---

typedef PluginParameter

Represents a Plugin .

using Paramita::PluginParameter = typedef InterfaceParameter<Plugin>;

---

enum SPECIAL_WEIGHTS

enum Paramita::SPECIAL_WEIGHTS {
    TOP_WEIGHT
};

---

typedef SatSolverParameter

Represents a SatSolver .

using Paramita::SatSolverParameter = typedef InterfaceParameter<SatSolver>;

---

typedef WClauseContainerParameter

Represents a WClauseContainer .

using Paramita::WClauseContainerParameter = typedef InterfaceParameter<WClauseContainer>;

---

typedef Weight

using Paramita::Weight = typedef std::variant<std::uint64_t, SPECIAL_WEIGHTS>;

---

Public Attributes Documentation

variable paramita_interfaces_version

constexpr int Paramita::paramita_interfaces_version;

---

Public Functions Documentation

function visit_parameter

template<typename Visitor>
auto Paramita::visit_parameter (
    const std::shared_ptr< Parameter > & ptr,
    Visitor && visitor
) 

---

function visit_parameter

template<typename Visitor>
auto Paramita::visit_parameter (
    const Parameter & param,
    Visitor && visitor
) 

---