org.sat4j.minisat.core
Class TextOutputListener<T>

java.lang.Object
  org.sat4j.minisat.core.TextOutputListener<T>

All Implemented Interfaces:

java.io.Serializable, SearchListener

public class TextOutputListener<T>
extends java.lang.Object
implements SearchListener

Debugging Search Listener allowing to follow the search in a textual way.

Author:

daniel

See Also:

Serialized Form

Constructor Summary

TextOutputListener(java.util.Map<java.lang.Integer,T> mapping)

Method Summary

void	adding(int p) adding forced variable (conflict driven assignment)
void	assuming(int p) decision variable
void	backtracking(int p) backtrack on a decision variable
void	beginLoop() starts a propagation
void	conflictFound(IConstr confl) a conflict has been found.
void	conflictFound(int p) a conflict has been found while propagating values.
void	delete(int[] clause) delete a clause
void	end(Lbool result) End the search.
void	learn(IConstr clause) learning a new clause
void	propagating(int p, IConstr reason) Unit propagation
void	solutionFound() a solution is found.
void	start() Start the search.

Methods inherited from class java.lang.Object

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

Constructor Detail

TextOutputListener

public TextOutputListener(java.util.Map<java.lang.Integer,T> mapping)

Since:

2.1

Method Detail

assuming

public void assuming(int p)

Description copied from interface: SearchListener

decision variable

Specified by:

assuming in interface SearchListener

propagating

public void propagating(int p,
                        IConstr reason)

Description copied from interface: SearchListener

Unit propagation

Specified by:

propagating in interface SearchListener

reason - TODO

Since:

2.1

backtracking

public void backtracking(int p)

Description copied from interface: SearchListener

backtrack on a decision variable

Specified by:

backtracking in interface SearchListener

adding

public void adding(int p)

Description copied from interface: SearchListener

adding forced variable (conflict driven assignment)

Specified by:

adding in interface SearchListener

learn

public void learn(IConstr clause)

Description copied from interface: SearchListener

learning a new clause

Specified by:

learn in interface SearchListener

Since:

2.1

delete

public void delete(int[] clause)

Description copied from interface: SearchListener

delete a clause

Specified by:

delete in interface SearchListener

conflictFound

public void conflictFound(IConstr confl)

Description copied from interface: SearchListener

a conflict has been found.

Specified by:

conflictFound in interface SearchListener

Parameters:

confl - TODO

Since:

2.1

conflictFound

public void conflictFound(int p)

Description copied from interface: SearchListener

a conflict has been found while propagating values.

Specified by:

conflictFound in interface SearchListener

Parameters:

p - the conflicting value.

Since:

2.1

solutionFound

public void solutionFound()

Description copied from interface: SearchListener

a solution is found.

Specified by:

solutionFound in interface SearchListener

beginLoop

public void beginLoop()

Description copied from interface: SearchListener

starts a propagation

Specified by:

beginLoop in interface SearchListener

start

public void start()

Description copied from interface: SearchListener

Start the search.

Specified by:

start in interface SearchListener

end

public void end(Lbool result)

Description copied from interface: SearchListener

End the search.

Specified by:

end in interface SearchListener

Parameters:

result - the result of the search.

Since:

2.1