Package org.tweetyproject.logics.commons.analysis

Interface ConsistencyWitnessProvider<B extends BeliefBase,S extends Formula>

Type Parameters:

B - the type of belief bases

S - The type of formulas.

All Known Implementing Classes:

CmdLineSatSolver, DimacsMaxSatSolver, DimacsSatSolver, MaxSatSolver, OpenWboSolver, Sat4jSolver, SatSolver, SimpleDpllSolver

public interface ConsistencyWitnessProvider<B extends BeliefBase,S extends Formula>

Provides methods for returning some model (if it exists) of a set of formulas.

Author:

Matthias Thimm

Method Summary

Modifier and Type	Method	Description
Interpretation<B,S>	getWitness(Collection<S> formulas)	If the collection of formulas is consistent this method returns some model of it or, if it is inconsistent, null.
Interpretation<B,S>	getWitness(BeliefSet<S,?> bs)	If the belief set is consistent this method returns some model of it or, if it is inconsistent, null.
Interpretation<B,S>	getWitness(S formula)	If the formula is consistent this method returns some model of it or, if it is inconsistent, null.

Method Details

getWitness

Interpretation<B,S> getWitness(Collection<S> formulas)

If the collection of formulas is consistent this method returns some model of it or, if it is inconsistent, null.

Parameters:

formulas - a set of formulas

Returns:

some model of the formulas or null.

getWitness

Interpretation<B,S> getWitness(S formula)

If the formula is consistent this method returns some model of it or, if it is inconsistent, null.

Parameters:

formula - a formula

Returns:

some model of the formula or null.

getWitness

Interpretation<B,S> getWitness(BeliefSet<S,?> bs)

If the belief set is consistent this method returns some model of it or, if it is inconsistent, null.

Parameters:

bs - a belief set

Returns:

some model of the belief set or null.