org.sat4j.tools

Class CheckMUSSolutionListener

java.lang.Object

org.sat4j.tools.CheckMUSSolutionListener

All Implemented Interfaces:

SolutionFoundListener

public class CheckMUSSolutionListener
extends Object
implements SolutionFoundListener

Field Summary

Fields inherited from interface org.sat4j.tools.SolutionFoundListener

VOID

Constructor Summary

Constructors

Constructor and Description
CheckMUSSolutionListener(ASolverFactory<? extends ISolver> factory)

Method Summary

Methods

Modifier and Type	Method and Description
void	addOriginalClause(IVecInt clause)
boolean	checkThatItIsAMUS(IVecInt mus)
void	onSolutionFound(int[] solution) Callback method called when a new solution is found.
void	onSolutionFound(IVecInt solution) Callback method called when a new solution is found.
void	onUnsatTermination() Callback method called when the search is finished (either unsat problem or no more solutions found)

Methods inherited from class java.lang.Object

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

Constructor Detail

CheckMUSSolutionListener

public CheckMUSSolutionListener(ASolverFactory<? extends ISolver> factory)

Method Detail

addOriginalClause

public void addOriginalClause(IVecInt clause)

checkThatItIsAMUS

public boolean checkThatItIsAMUS(IVecInt mus)

Parameters:

mus - containing the clauses identifiers

clauses - the original set of clauses

Returns:

onSolutionFound

public void onSolutionFound(int[] solution)

Description copied from interface: SolutionFoundListener

Callback method called when a new solution is found. While a solution will often be a model, it might also be the case that the solution is something else (MUS, group MUS, etc).

Specified by:

onSolutionFound in interface SolutionFoundListener

Parameters:

solution - a set of Dimacs literals.

onSolutionFound

public void onSolutionFound(IVecInt solution)

Description copied from interface: SolutionFoundListener

Callback method called when a new solution is found. While a solution will often be a model, it might also be the case that the solution is something else (MUS, group MUS, etc).

Specified by:

onSolutionFound in interface SolutionFoundListener

Parameters:

solution - a set of Dimacs literals.

onUnsatTermination

public void onUnsatTermination()

Description copied from interface: SolutionFoundListener

Callback method called when the search is finished (either unsat problem or no more solutions found)

Specified by:

onUnsatTermination in interface SolutionFoundListener