Class QuteSolver
- java.lang.Object
-
- net.sf.tweety.logics.qbf.reasoner.QbfSolver
-
- net.sf.tweety.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
-
-
Field Summary
Fields Modifier and Type Field Description private java.lang.String
binaryLocation
String representation of the Qute binary path.
-
Constructor Summary
Constructors Constructor Description QuteSolver(java.lang.String binaryLocation)
Constructs a new instance pointing to a specific QuteSolverQuteSolver(java.lang.String binaryLocation, Shell bash)
Constructs a new instance pointing to a specific QuteSolver.
-
Method Summary
Modifier and Type Method Description private boolean
evaluate(java.io.File file)
Invokes Qute with the given input file.boolean
isSatisfiable(java.util.Collection<PlFormula> kb)
Checks whether the given set of formulas is satisfiable.-
Methods inherited from class net.sf.tweety.logics.qbf.reasoner.QbfSolver
isConsistent, isConsistent, isConsistent
-
-
-
-
Constructor Detail
-
QuteSolver
public QuteSolver(java.lang.String binaryLocation, Shell bash)
Constructs a new instance pointing to a specific QuteSolver.- Parameters:
binaryLocation
- of the Qute executable on the hard drivebash
- shell to run commands
-
QuteSolver
public QuteSolver(java.lang.String binaryLocation)
Constructs a new instance pointing to a specific QuteSolver- Parameters:
binaryLocation
- of the Qute executable on the hard drive
-
-
Method Detail
-
evaluate
private boolean evaluate(java.io.File file) throws java.lang.Exception
Invokes Qute with the given input file.- Parameters:
file
- input file for Qute- Returns:
- true if the result is SAT, false if the result is UNSAT
- Throws:
java.lang.Exception
- if the bash command fails or if Qute produces no interpretable output
-
isSatisfiable
public boolean isSatisfiable(java.util.Collection<PlFormula> kb)
Description copied from class:QbfSolver
Checks whether the given set of formulas is satisfiable.- Specified by:
isSatisfiable
in classQbfSolver
- Parameters:
kb
- a set of formulas.- Returns:
- "true" if the set is consistent.
-
-