Package org.tweetyproject.logics.qbf.reasoner

Class QuteSolver

java.lang.Object

org.tweetyproject.logics.qbf.reasoner.QbfSolver

org.tweetyproject.logics.qbf.reasoner.QuteSolver

All Implemented Interfaces:

BeliefSetConsistencyTester<PlFormula>, ConsistencyTester<BeliefSet<PlFormula,?>>

public class QuteSolver
extends QbfSolver

A wrapper for the Qute (https://www.ac.tuwien.ac.at/research/qute/) solver.
Tested with the 2019 version: https://github.com/perebor/qute

Author:

Anna Gessler

Constructor Summary

Constructors

Constructor	Description
QuteSolver(String binaryLocation)	Constructs a new instance pointing to a specific QuteSolver
QuteSolver(String binaryLocation, Shell bash)	Constructs a new instance pointing to a specific QuteSolver.

Method Summary

Modifier and Type	Method	Description
boolean	isInstalled()
boolean	isSatisfiable(Collection<PlFormula> kb)	Checks whether the given set of formulas is satisfiable.

Methods inherited from class org.tweetyproject.logics.qbf.reasoner.QbfSolver

isConsistent, isConsistent, isConsistent

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Details

QuteSolver

public QuteSolver(String binaryLocation,
 Shell bash)

Constructs a new instance pointing to a specific QuteSolver.

Parameters:

binaryLocation - of the Qute executable on the hard drive

bash - shell to run commands

QuteSolver

public QuteSolver(String binaryLocation)

Constructs a new instance pointing to a specific QuteSolver

Parameters:

binaryLocation - of the Qute executable on the hard drive

Method Details

isSatisfiable

public boolean isSatisfiable(Collection<PlFormula> kb)

Description copied from class: QbfSolver

Checks whether the given set of formulas is satisfiable.

Specified by:

isSatisfiable in class QbfSolver

Parameters:

kb - a set of formulas.

Returns:

"true" if the set is consistent.

isInstalled

public boolean isInstalled()

Specified by:

isInstalled in class QbfSolver