ConsistencyWitnessProvider

Type Parameters:

S - The type of formulas.

B - the type of belief bases

All Known Implementing Classes:

IncrementalSatSolver, LingelingSolver, MaxSatSolver, NativeLingelingSolver, NativeMinisatSolver, NativePicosatSolver, OpenWboSolver, Sat4jSolver, SatSolver, SimpleDpllSolver, SimpleIncrementalSatSolver
```
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(java.util.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 Detail
  - getWitness
```
Interpretation<B,S> getWitness(java.util.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.