public class LingelingSolver extends SatSolver
Modifier and Type | Field and Description |
---|---|
private java.lang.String |
binaryLocation
The binary location of Lingeling.
|
Constructor and Description |
---|
LingelingSolver(java.lang.String binaryLocation)
Creates a new solver based on the Lingeling
executable given as a parameter.
|
Modifier and Type | Method and Description |
---|---|
Interpretation |
getWitness(java.util.Collection<PropositionalFormula> formulas)
If the collection of formulas is consistent this method
returns some model of it or, if it is inconsistent, null.
|
boolean |
isSatisfiable(java.util.Collection<PropositionalFormula> formulas)
Checks whether the given set of formulas is satisfiable.
|
convertToDimacs, convertToDimacs, createTmpDimacsFile, createTmpDimacsFile, getDefaultSolver, getWitness, getWitness, hasDefaultSolver, isConsistent, isConsistent, isConsistent, setDefaultSolver, setTempFolder
private java.lang.String binaryLocation
public LingelingSolver(java.lang.String binaryLocation)
binaryLocation
- the path to the executable.public Interpretation getWitness(java.util.Collection<PropositionalFormula> formulas)
SatSolver
getWitness
in interface ConsistencyWitnessProvider<PropositionalFormula>
getWitness
in class SatSolver
public boolean isSatisfiable(java.util.Collection<PropositionalFormula> formulas)
SatSolver
isSatisfiable
in class SatSolver
formulas
- a set of formulas.