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

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

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

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