Interface ConsistencyWitnessProvider<B extends BeliefBase,S extends Formula>
- Type Parameters:
S
- The type of formulas.B
- the type of belief bases
- All Known Implementing Classes:
CmdLineSatSolver
,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 TypeMethodDescriptionInterpretation<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
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
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
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.
-