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

Class CompleteVerifier

java.lang.Object

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

All Implemented Interfaces:

AutoCloseable, Verifier

public final class CompleteVerifier
extends Object
implements Verifier

The CompleteVerifier is a verifier class that checks whether a given interpretation is a complete interpretation within an abstract dialectical framework (ADF). It ensures that the interpretation is conflict-free and adheres to acceptance conditions for all undecided arguments.

Author:

Mathias Hofer

Constructor Summary

Constructors

Constructor	Description
CompleteVerifier(Supplier<SatSolverState> stateSupplier, AbstractDialecticalFramework adf, PropositionalMapping mapping)	Constructs a CompleteVerifier with the given SAT solver state supplier, abstract dialectical framework, and propositional mapping.

Method Summary

Modifier and Type	Method	Description
void	close()	Closes the SAT solver state and releases any resources associated with it.
void	prepare()	Prepares the SAT solver state for verification.
boolean	verify(Interpretation candidate)	Verifies whether the given interpretation is a complete interpretation.

Methods inherited from class java.lang.Object

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

Constructor Details

CompleteVerifier

public CompleteVerifier(Supplier<SatSolverState> stateSupplier,
 AbstractDialecticalFramework adf,
 PropositionalMapping mapping)

Constructs a CompleteVerifier with the given SAT solver state supplier, abstract dialectical framework, and propositional mapping. Initializes the SAT encodings for conflict-free and partial interpretation fixing.

Parameters:

stateSupplier - a supplier that provides new instances of SatSolverState, must not be null

adf - the abstract dialectical framework to be processed, must not be null

mapping - the propositional mapping used for SAT encoding, must not be null

Throws:

NullPointerException - if any of the parameters are null

Method Details

prepare

public void prepare()

Prepares the SAT solver state for verification. This implementation does not perform any preparation. This method is provided to comply with the Verifier interface.

Specified by:

prepare in interface Verifier

verify

public boolean verify(Interpretation candidate)

Verifies whether the given interpretation is a complete interpretation. It checks if the interpretation is conflict-free and verifies the acceptance conditions for all undecided arguments.

For each undecided argument, the method encodes the acceptance condition and verifies that it is neither tautologically satisfied nor unsatisfied in the given interpretation.

Specified by:

verify in interface Verifier

Parameters:

candidate - the interpretation to be verified

Returns:

true if the interpretation is complete, false otherwise

close

public void close()

Closes the SAT solver state and releases any resources associated with it. This method should be called when the verifier is no longer needed to ensure proper resource management.

Specified by:

close in interface AutoCloseable

Specified by:

close in interface Verifier