net.sf.tweety.logics.pl.sat

Class PlMusEnumerator

java.lang.Object

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

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

All Implemented Interfaces:

BeliefSetConsistencyTester<PropositionalFormula>, ConsistencyTester<BeliefSet<PropositionalFormula>>, MusEnumerator<PropositionalFormula>

Direct Known Subclasses:

MarcoMusEnumerator, MimusMusEnumerator

public abstract class PlMusEnumerator
extends AbstractMusEnumerator<PropositionalFormula>

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 and Description
private static AbstractMusEnumerator<PropositionalFormula>	defaultEnumerator The default MUS enumerator.

Constructor Summary

Constructors

Constructor and Description
PlMusEnumerator()

Method Summary

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.

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<PropositionalFormula> defaultEnumerator

The default MUS enumerator.

Constructor Detail

PlMusEnumerator

public PlMusEnumerator()

Method Detail

setDefaultEnumerator

public static void setDefaultEnumerator(AbstractMusEnumerator<PropositionalFormula> enumerator)

Sets the default MUS enumerator.

Parameters:

solver - 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<PropositionalFormula> 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<PropositionalFormula>> minimalInconsistentSubsets(java.util.Collection<PropositionalFormula> 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<PropositionalFormula>

Specified by:

minimalInconsistentSubsets in class AbstractMusEnumerator<PropositionalFormula>

Parameters:

formulas - a set of formulas.

Returns:

the minimal inconsistent subsets of the given set of formulas