Package org.tweetyproject.arg.adf.reasoner.sat.verifier

Interface Verifier

All Known Implementing Classes:

AdmissibleVerifier, CompleteVerifier, GrounderStableVerifier

public interface Verifier

Is used to verify a certain property of an Interpretation, e.g. admissibility.

Author:

Mathias Hofer

Method Summary

Modifier and Type	Method	Description
boolean	postVerification(SatSolverState state, PropositionalMapping mapping, Interpretation candidate, AbstractDialecticalFramework adf, boolean verificationResult)	Gets called after every verify call.
void	prepareState(SatSolverState state, PropositionalMapping mapping, AbstractDialecticalFramework adf)	Gets called exactly once for each SatSolverState before the first use in verify.
boolean	verify(SatSolverState state, PropositionalMapping mapping, Interpretation candidate, AbstractDialecticalFramework adf)	Gets called by the Pipeline to verify if the computed candidate Interpretation asserts a certain property.

Method Detail

prepareState

void prepareState(SatSolverState state,
                  PropositionalMapping mapping,
                  AbstractDialecticalFramework adf)

Gets called exactly once for each SatSolverState before the first use in verify. This method exists to perform initializations on each state.

Parameters:

state - the state on which we perform initializations

mapping - the propositional mapping of the ADF

adf - the ADF

verify

boolean verify(SatSolverState state,
               PropositionalMapping mapping,
               Interpretation candidate,
               AbstractDialecticalFramework adf)

Gets called by the Pipeline to verify if the computed candidate Interpretation asserts a certain property.

Parameters:

state - the initialized and perhaps shared state

mapping - the propositional mapping of the ADF

candidate - the candidate to verify

adf - the ADF

Returns:

true if we could verify the property for candidate, false otherwise

postVerification

boolean postVerification(SatSolverState state,
                         PropositionalMapping mapping,
                         Interpretation candidate,
                         AbstractDialecticalFramework adf,
                         boolean verificationResult)

Gets called after every verify call.

Parameters:

state - the state used by the previous verify call

mapping - the propositional mapping of the ADF

candidate - the candidate of the previous verify call

adf - the ADF

verificationResult - the return value of the previous verify call

Returns:

true if the state was consumed, hence we need a new one for the subsequent verifications, false if we can reuse the state