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

Contents

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

Base classes

class UniverseJavaSolver virtual
class IUniverseSatSolver virtual

Derived classes

class UniverseJavaPseudoBooleanSolver virtual

Constructors, destructors, conversion operators

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

Public functions

void addClause(const std::vector<int>& literals) override
auto solveDimacs(const std::vector<int>& assumptions) -> UniverseSolverResult override
auto solveBoolean(const std::vector<UniverseAssumption<bool>>& assumptions) -> Universe::UniverseSolverResult override
auto solve(const std::vector<UniverseAssumption<BigInteger>>& assumptions) -> Universe::UniverseSolverResult override

Protected static functions

static auto asList(const std::vector<int>& integers) -> Universe::JavaList

Function documentation

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

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

Creates a UniverseJavaSatSolver.

Universe::UniverseJavaSatSolver::~UniverseJavaSatSolver() override defaulted

Destroys this UniverseJavaSatSolver.

void Universe::UniverseJavaSatSolver::addClause(const std::vector<int>& literals) override

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

Adds to this solver a clause from a set of literals. The literals are represented by non-zero integers such that opposite literals are represented by opposite values (following the classical DIMACS way of representing literals).

UniverseSolverResult Universe::UniverseJavaSatSolver::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.

Universe::UniverseSolverResult Universe::UniverseJavaSatSolver::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.

Universe::UniverseSolverResult Universe::UniverseJavaSatSolver::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::UniverseJavaSatSolver::asList(const std::vector<int>& integers) protected

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

Creates a JavaList corresponding to the given vector of integers.