Package net.sf.tweety.logics.pl.sat

Class PlMusEnumerator

java.lang.Object

net.sf.tweety.logics.commons.analysis.AbstractMusEnumerator<PlFormula>

net.sf.tweety.logics.pl.sat.PlMusEnumerator

All Implemented Interfaces:

BeliefSetConsistencyTester<PlFormula>, ConsistencyTester<BeliefSet<PlFormula,?>>, MusEnumerator<PlFormula>

Direct Known Subclasses:

MarcoMusEnumerator, MimusMusEnumerator

public abstract class PlMusEnumerator
extends AbstractMusEnumerator<PlFormula>

This abstract class models a MUS enumerator for propositional logic, i.e. an approach that lists all minimal unsatisfiable subsets of a given set of formulas. It also provides some static methods for accessing a centrally configured default MUS enumerator.

Author:

Matthias Thimm

Field Summary

Fields

Modifier and Type	Field	Description
private static AbstractMusEnumerator<PlFormula>	defaultEnumerator	The default MUS enumerator.

Constructor Summary

Constructors

Constructor	Description
PlMusEnumerator()

Method Summary

Modifier and Type	Method	Description
static AbstractMusEnumerator<PlFormula>	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<PlFormula>>	minimalInconsistentSubsets(java.util.Collection<PlFormula> formulas)	This method returns the minimal inconsistent subsets of the given set of formulas.
static void	setDefaultEnumerator(AbstractMusEnumerator<PlFormula> enumerator)	Sets the default MUS enumerator.

Methods inherited from class net.sf.tweety.logics.commons.analysis.AbstractMusEnumerator

getMiComponents, isConsistent, isConsistent, isConsistent, maximalConsistentSubsets, minimalCorrectionSubsets

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

defaultEnumerator

private static AbstractMusEnumerator<PlFormula> defaultEnumerator

The default MUS enumerator.

Constructor Detail

PlMusEnumerator

public PlMusEnumerator()

Method Detail

setDefaultEnumerator

public static void setDefaultEnumerator(AbstractMusEnumerator<PlFormula> enumerator)

Sets the default MUS enumerator.

Parameters:

enumerator - some MUS enumerator

hasDefaultEnumerator

public static boolean hasDefaultEnumerator()

Returns "true" if a default MUS enumerator is configured.

Returns:

"true" if a default MUS enumerator is configured.

getDefaultEnumerator

public static AbstractMusEnumerator<PlFormula> getDefaultEnumerator()

Returns the default MUS enumerator.

If a default MUS enumerator has been configured this enumerator is returned by this method. If no default MUS enumerator is configured, a naive enumerator based on the default SAT solver is returned as a fallback and a message is printed to stderr pointing out that no default MUS enumerator is configured.

Returns:

the default MUS enumerator.

minimalInconsistentSubsets

public abstract java.util.Collection<java.util.Collection<PlFormula>> minimalInconsistentSubsets(java.util.Collection<PlFormula> formulas)

Description copied from interface: MusEnumerator

This method returns the minimal inconsistent subsets of the given set of formulas.

Specified by:

minimalInconsistentSubsets in interface MusEnumerator<PlFormula>

Specified by:

minimalInconsistentSubsets in class AbstractMusEnumerator<PlFormula>

Parameters:

formulas - a set of formulas.

Returns:

the minimal inconsistent subsets of the given set of formulas