org.sat4j.tools
Class TextOutputTracing<T>

java.lang.Object
  org.sat4j.tools.TextOutputTracing<T>

All Implemented Interfaces:

Serializable, SearchListener

public class TextOutputTracing<T>
extends Object
implements SearchListener

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

Since:

2.2

Author:

daniel

See Also:

Serialized Form

Constructor Summary

TextOutputTracing(Map<Integer,T> mapping)

Method Summary

void	adding(int p) adding forced variable (conflict driven assignment)
void	assuming(int p) decision variable
void	backjump(int backjumpLevel) The solver is asked to backjump to a given decision level.
void	backtracking(int p) backtrack on a decision variable
void	beginLoop() starts a propagation
void	cleaning() The solver is going to delete some learned clauses.
void	conflictFound(IConstr confl, int dlevel, int trailLevel) 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	init(ISolverService solverService) Provide access to the solver's controllable interface.
void	learn(IConstr clause) learning a new clause
void	propagating(int p, IConstr reason) Unit propagation
void	restarting() The solver restarts the search.
void	solutionFound(int[] model) 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

TextOutputTracing

public TextOutputTracing(Map<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,
                          int dlevel,
                          int trailLevel)

Description copied from interface: SearchListener

a conflict has been found.

Specified by:

conflictFound in interface SearchListener

Parameters:

confl - TODO

dlevel - TODO

trailLevel - 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(int[] model)

Description copied from interface: SearchListener

a solution is found.

Specified by:

solutionFound in interface SearchListener

Parameters:

model - the model found

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

restarting

public void restarting()

Description copied from interface: SearchListener

The solver restarts the search.

Specified by:

restarting in interface SearchListener

Since:

2.2

backjump

public void backjump(int backjumpLevel)

Description copied from interface: SearchListener

The solver is asked to backjump to a given decision level.

Specified by:

backjump in interface SearchListener

init

public void init(ISolverService solverService)

Description copied from interface: SearchListener

Provide access to the solver's controllable interface.

Specified by:

init in interface SearchListener

Parameters:

solverService - a way to safely control the solver.

Since:

2.3.2

cleaning

public void cleaning()

Description copied from interface: SearchListener

The solver is going to delete some learned clauses.

Specified by:

cleaning in interface SearchListener

Since:

2.3.2