Class CadetSolver
- java.lang.Object
-
- net.sf.tweety.logics.qbf.reasoner.QbfSolver
-
- net.sf.tweety.logics.qbf.reasoner.CadetSolver
-
- All Implemented Interfaces:
BeliefSetConsistencyTester<PlFormula>,ConsistencyTester<BeliefSet<PlFormula,?>>
public class CadetSolver extends QbfSolver
A wrapper for the Cadet (https://markusrabe.github.io/cadet/) solver. Tested with version 2.5.- Author:
- Anna Gessler
-
-
Constructor Summary
Constructors Constructor Description CadetSolver(java.lang.String binaryLocation)Constructs a new instance pointing to a specific CadetSolverCadetSolver(java.lang.String binaryLocation, Shell bash)Constructs a new instance pointing to a specific CadetSolver.
-
Method Summary
Modifier and Type Method Description booleanisSatisfiable(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
-
CadetSolver
public CadetSolver(java.lang.String binaryLocation, Shell bash)Constructs a new instance pointing to a specific CadetSolver.- Parameters:
binaryLocation- of the GhostQ executable on the hard drivebash- shell to run commands
-
CadetSolver
public CadetSolver(java.lang.String binaryLocation)
Constructs a new instance pointing to a specific CadetSolver- Parameters:
binaryLocation- of the CadetSolver executable on the hard drive
-
-
Method Detail
-
isSatisfiable
public boolean isSatisfiable(java.util.Collection<PlFormula> kb)
Description copied from class:QbfSolverChecks whether the given set of formulas is satisfiable.- Specified by:
isSatisfiablein classQbfSolver- Parameters:
kb- a set of formulas.- Returns:
- "true" if the set is consistent.
-
-