Universe::UniverseJavaPseudoBooleanSolver class
#include <UniverseJavaPseudoBooleanSolver.hpp>

Contents

The UniverseJavaPseudoBooleanSolver class defines an adapter for an IUniversePseudoBooleanSolver written in Java (and implementing the JUniverse interface). The solver is run through the Java Native Interface (JNI).

Base classes

class UniverseJavaSatSolver virtual
class IUniversePseudoBooleanSolver virtual

Derived classes

class UniverseJavaCspSolver

Constructors, destructors, conversion operators

UniverseJavaPseudoBooleanSolver(easyjni::JavaClass* interface, easyjni::JavaObject object)
~UniverseJavaPseudoBooleanSolver() defaulted override

Public functions

void addPseudoBoolean(const std::vector<int>& literals, const std::vector<Universe::BigInteger>& coefficients, bool moreThan, const BigInteger& degree) override
void addAtMost(const std::vector<int>& literals, int degree) override
void addAtMost(const std::vector<int>& literals, const std::vector<int>& coefficients, int degree) override
void addAtMost(const std::vector<int>& literals, const std::vector<Universe::BigInteger>& coefficients, const Universe::BigInteger& degree) override
void addAtLeast(const std::vector<int>& literals, int degree) override
void addAtLeast(const std::vector<int>& literals, const std::vector<int>& coefficients, int degree) override
void addAtLeast(const std::vector<int>& literals, const std::vector<Universe::BigInteger>& coefficients, const Universe::BigInteger& degree) override
void addExactly(const std::vector<int>& literals, int degree) override
void addExactly(const std::vector<int>& literals, const std::vector<int>& coefficients, int degree) override
void addExactly(const std::vector<int>& literals, const std::vector<Universe::BigInteger>& coefficients, const Universe::BigInteger& degree) override
auto solveDimacs(const std::vector<int>& assumptions) -> UniverseSolverResult override
auto solveBoolean(const std::vector<UniverseAssumption<bool>>& assumptions) -> UniverseSolverResult override
auto solve(const std::vector<UniverseAssumption<BigInteger>>& assumptions) -> UniverseSolverResult override

Protected static functions

static auto asList(const std::vector<Universe::BigInteger>& integers, bool hasStar = false) -> Universe::JavaList

Function documentation

Universe::UniverseJavaPseudoBooleanSolver::UniverseJavaPseudoBooleanSolver(easyjni::JavaClass* interface, easyjni::JavaObject object)

Parameters
interface The Java interface corresponding to IUniversePseudoBooleanSolver.
object The Java object to adapt.

Creates a UniverseJavaPseudoBooleanSolver.

Universe::UniverseJavaPseudoBooleanSolver::~UniverseJavaPseudoBooleanSolver() override defaulted

Destroys this UniverseJavaPseudoBooleanSolver.

void Universe::UniverseJavaPseudoBooleanSolver::addPseudoBoolean(const std::vector<int>& literals, const std::vector<Universe::BigInteger>& coefficients, bool moreThan, const BigInteger& degree) override

Parameters
literals The literals of the constraint to add.
coefficients The coefficients of the literals.
moreThan Whether the constraint is an at-least constraint, or an at-most constraint.
degree The degree of the constraint.
Exceptions
UniverseContradictionException If the constraint to add is inconsistent.

Creates a pseudo-Boolean constraint of type at-least or at-most.

void Universe::UniverseJavaPseudoBooleanSolver::addAtMost(const std::vector<int>& literals, int degree) override

Parameters
literals The literals of the constraint to add.
degree The degree of the constraint.
Exceptions
UniverseContradictionException If the constraint to add is inconsistent.

Creates an at-most cardinality constraint.

void Universe::UniverseJavaPseudoBooleanSolver::addAtMost(const std::vector<int>& literals, const std::vector<int>& coefficients, int degree) override

Parameters
literals The literals of the constraint to add.
coefficients The coefficients of the literals.
degree The degree of the constraint.
Exceptions
UniverseContradictionException If the constraint to add is inconsistent.

Creates an at-most pseudo-Boolean constraint.

void Universe::UniverseJavaPseudoBooleanSolver::addAtMost(const std::vector<int>& literals, const std::vector<Universe::BigInteger>& coefficients, const Universe::BigInteger& degree) override

Parameters
literals The literals of the constraint to add.
coefficients The coefficients of the literals.
degree The degree of the constraint.
Exceptions
UniverseContradictionException If the constraint to add is inconsistent.

Creates an at-most pseudo-Boolean constraint.

void Universe::UniverseJavaPseudoBooleanSolver::addAtLeast(const std::vector<int>& literals, int degree) override

Parameters
literals The literals of the constraint to add.
degree The degree of the constraint.
Exceptions
UniverseContradictionException If the constraint to add is inconsistent.

Creates an at-least cardinality constraint.

void Universe::UniverseJavaPseudoBooleanSolver::addAtLeast(const std::vector<int>& literals, const std::vector<int>& coefficients, int degree) override

Parameters
literals The literals of the constraint to add.
coefficients The coefficients of the literals.
degree The degree of the constraint.
Exceptions
UniverseContradictionException If the constraint to add is inconsistent.

Creates an at-least pseudo-Boolean constraint.

void Universe::UniverseJavaPseudoBooleanSolver::addAtLeast(const std::vector<int>& literals, const std::vector<Universe::BigInteger>& coefficients, const Universe::BigInteger& degree) override

Parameters
literals The literals of the constraint to add.
coefficients The coefficients of the literals.
degree The degree of the constraint.
Exceptions
UniverseContradictionException If the constraint to add is inconsistent.

Creates an at-least pseudo-Boolean constraint.

void Universe::UniverseJavaPseudoBooleanSolver::addExactly(const std::vector<int>& literals, int degree) override

Parameters
literals The literals of the constraint to add.
degree The degree of the constraint.
Exceptions
UniverseContradictionException If the constraint to add is inconsistent.

Creates an exactly cardinality constraint.

void Universe::UniverseJavaPseudoBooleanSolver::addExactly(const std::vector<int>& literals, const std::vector<int>& coefficients, int degree) override

Parameters
literals The literals of the constraint to add.
coefficients The coefficients of the literals.
degree The degree of the constraint.
Exceptions
UniverseContradictionException If the constraint to add is inconsistent.

Creates an exactly pseudo-Boolean constraint.

void Universe::UniverseJavaPseudoBooleanSolver::addExactly(const std::vector<int>& literals, const std::vector<Universe::BigInteger>& coefficients, const Universe::BigInteger& degree) override

Parameters
literals The literals of the constraint to add.
coefficients The coefficients of the literals.
degree The degree of the constraint.
Exceptions
UniverseContradictionException If the constraint to add is inconsistent.

Creates an exactly pseudo-Boolean constraint.

UniverseSolverResult Universe::UniverseJavaPseudoBooleanSolver::solveDimacs(const std::vector<int>& assumptions) override

Parameters
assumptions The assumptions to consider when solving (as a set of literals).
Returns The outcome of the search conducted by the solver.

Solves the problem associated to this solver.

UniverseSolverResult Universe::UniverseJavaPseudoBooleanSolver::solveBoolean(const std::vector<UniverseAssumption<bool>>& assumptions) override

Parameters
assumptions The assumptions to consider when solving.
Returns The outcome of the search conducted by the solver.

Solves the problem associated to this solver.

UniverseSolverResult Universe::UniverseJavaPseudoBooleanSolver::solve(const std::vector<UniverseAssumption<BigInteger>>& assumptions) override

Parameters
assumptions The assumptions to consider when solving.
Returns The outcome of the search conducted by the solver.

Solves the problem associated to this solver.

static Universe::JavaList Universe::UniverseJavaPseudoBooleanSolver::asList(const std::vector<Universe::BigInteger>& integers, bool hasStar = false) protected

Parameters
integers The vector of BigIntegers to transform into a list.
hasStar
Returns The created list.

Creates a JavaList corresponding to the given vector of BigIntegers.