public abstract class PlMusEnumerator extends AbstractMusEnumerator<PropositionalFormula>
Modifier and Type | Field and Description |
---|---|
private static AbstractMusEnumerator<PropositionalFormula> |
defaultEnumerator
The default MUS enumerator.
|
Constructor and Description |
---|
PlMusEnumerator() |
Modifier and Type | Method and Description |
---|---|
static AbstractMusEnumerator<PropositionalFormula> |
getDefaultEnumerator()
Returns the default MUS enumerator.
If a default MUS enumerator has been configured this enumerator
is returned by this method.
|
static boolean |
hasDefaultEnumerator()
Returns "true" if a default MUS enumerator is configured.
|
abstract java.util.Collection<java.util.Collection<PropositionalFormula>> |
minimalInconsistentSubsets(java.util.Collection<PropositionalFormula> formulas)
This method returns the minimal inconsistent subsets of the given
set of formulas.
|
static void |
setDefaultEnumerator(AbstractMusEnumerator<PropositionalFormula> enumerator)
Sets the default MUS enumerator.
|
getMiComponents, isConsistent, isConsistent, isConsistent, maximalConsistentSubsets, minimalCorrectionSubsets
private static AbstractMusEnumerator<PropositionalFormula> defaultEnumerator
public static void setDefaultEnumerator(AbstractMusEnumerator<PropositionalFormula> enumerator)
solver
- some MUS enumeratorpublic static boolean hasDefaultEnumerator()
public static AbstractMusEnumerator<PropositionalFormula> getDefaultEnumerator()
public abstract java.util.Collection<java.util.Collection<PropositionalFormula>> minimalInconsistentSubsets(java.util.Collection<PropositionalFormula> formulas)
MusEnumerator
minimalInconsistentSubsets
in interface MusEnumerator<PropositionalFormula>
minimalInconsistentSubsets
in class AbstractMusEnumerator<PropositionalFormula>
formulas
- a set of formulas.