Class CadetSolver
java.lang.Object
org.tweetyproject.logics.qbf.reasoner.QbfSolver
org.tweetyproject.logics.qbf.reasoner.CadetSolver
- All Implemented Interfaces:
BeliefSetConsistencyTester<PlFormula>
,ConsistencyTester<BeliefSet<PlFormula,
?>>
A wrapper for the Cadet (https://markusrabe.github.io/cadet/) solver.
Tested with version 2.5.
- Author:
- Anna Gessler
-
Constructor Summary
ConstructorDescriptionCadetSolver
(String binaryLocation) Constructs a new instance pointing to a specific CadetSolverCadetSolver
(String binaryLocation, Shell bash) Constructs a new instance pointing to a specific CadetSolver. -
Method Summary
Modifier and TypeMethodDescriptionboolean
boolean
Checks whether the given set of formulas is satisfiable.Methods inherited from class org.tweetyproject.logics.qbf.reasoner.QbfSolver
isConsistent, isConsistent, isConsistent
-
Constructor Details
-
CadetSolver
Constructs a new instance pointing to a specific CadetSolver.- Parameters:
binaryLocation
- of the GhostQ executable on the hard drivebash
- shell to run commands
-
CadetSolver
Constructs a new instance pointing to a specific CadetSolver- Parameters:
binaryLocation
- of the CadetSolver executable on the hard drive
-
-
Method Details
-
isSatisfiable
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.
-
isInstalled
public boolean isInstalled()- Specified by:
isInstalled
in classQbfSolver
-