Package net.sf.tweety.arg.adf.reasoner.sat.verifier

Class GrounderStableVerifier

java.lang.Object

net.sf.tweety.arg.adf.reasoner.sat.verifier.GrounderStableVerifier

All Implemented Interfaces:

Verifier

public final class GrounderStableVerifier
extends java.lang.Object
implements Verifier

Verifies if a given interpretation is stable by comparing it with the ground interpretation of its omega reduct.

Author:

Mathias Hofer

Constructor Summary

Constructors

Constructor	Description
GrounderStableVerifier(CandidateGenerator groundGenerator, LinkStrategy linkStrategy)

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 encodingContext, Interpretation candidate, AbstractDialecticalFramework adf)	Gets called by the Pipeline to verify if the computed candidate Interpretation asserts a certain property.

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

GrounderStableVerifier

public GrounderStableVerifier(CandidateGenerator groundGenerator,
                              LinkStrategy linkStrategy)

Parameters:

groundGenerator - the generator which is used to compute the ground interpretation

linkStrategy - the strategy which is used to compute the links of the reduct

Method Detail

prepareState

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

Description copied from interface: Verifier

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

Specified by:

prepareState in interface Verifier

Parameters:

state - the state on which we perform initializations

mapping - the propositional mapping of the ADF

adf - the ADF

verify

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

Description copied from interface: Verifier

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

Specified by:

verify in interface Verifier

Parameters:

state - the initialized and perhaps shared state

encodingContext - 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

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

Description copied from interface: Verifier

Gets called after every verify call.

Specified by:

postVerification in interface Verifier

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