SugarTrace version 1.0.1 Core API Specification

sugartracer
Class Tracer

java.lang.Object
  extended by sugartracer.Tracer
Direct Known Subclasses:
ServerTracer, TextTracer

public abstract class Tracer
extends Object

This is a class for tracer.


Field Summary
 boolean debug
           
 Decoder decoder
           
 boolean done
           
 List<Integer> propagations
           
 boolean quick
           
 boolean showAuxVars
           
 SatSolver solver
           
 List<Integer> undos
           
 
Constructor Summary
Tracer(SatSolver solver, Decoder decoder)
          Creates the tracer.
 
Method Summary
 void backjump(int backjumpLevel)
          Called when backjump is done by SAT solver.
 void conflict(int[] clause)
          Called when conflict happened at the clause by SAT solver.
 void decide(int lit)
          Called when decision is done for the literal by SAT solver.
 void end(boolean result)
          Called when the result was returned from SAT solver.
 void found()
          Called when the solution was found by SAT solver.
 void learnt(int[] clause)
          Called when learnt clause is added by SAT solver.
 void propagate(int lit)
          Called when propagation is done for the literal by SAT solver.
 void restart()
          Called when restart happened by SAT solver.
abstract  void show(String[] strs)
          Shows the strings
 void showAssignment()
          Shows the current assignment.
 void showAssignment(Variable v)
          Shows the current assignment of the variable.
 void showCommand(String command, String[] args)
          Shows the command.
 void startTracer()
          Starts the tracer.
 void stopTracer()
          Stops the tracer.
 void undo(int lit)
          Called when undo is done for the literal by SAT solver.
 
Methods inherited from class java.lang.Object
equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Field Detail

solver

public SatSolver solver

decoder

public Decoder decoder

propagations

public List<Integer> propagations

undos

public List<Integer> undos

done

public boolean done

showAuxVars

public boolean showAuxVars

quick

public boolean quick

debug

public boolean debug
Constructor Detail

Tracer

public Tracer(SatSolver solver,
              Decoder decoder)
Creates the tracer.

Parameters:
decoder -
Method Detail

show

public abstract void show(String[] strs)
Shows the strings

Parameters:
strs -

showCommand

public void showCommand(String command,
                        String[] args)
Shows the command.

Parameters:
command -

showAssignment

public void showAssignment(Variable v)
Shows the current assignment of the variable.

Parameters:
v -

showAssignment

public void showAssignment()
Shows the current assignment.


startTracer

public void startTracer()
                 throws TracerException
Starts the tracer.

Throws:
TracerException
See Also:
SatSolver.startSolver()

stopTracer

public void stopTracer()
                throws TracerException
Stops the tracer.

Throws:
TracerException
See Also:
SatSolver.stopSolver()

decide

public void decide(int lit)
Called when decision is done for the literal by SAT solver.

Parameters:
lit - the literal

propagate

public void propagate(int lit)
Called when propagation is done for the literal by SAT solver.

Parameters:
lit - the literal

undo

public void undo(int lit)
Called when undo is done for the literal by SAT solver.

Parameters:
lit - the literal

backjump

public void backjump(int backjumpLevel)
Called when backjump is done by SAT solver.

Parameters:
backjumpLevel -

learnt

public void learnt(int[] clause)
Called when learnt clause is added by SAT solver. The clauses is added to the learnt clauses.

Parameters:
clause - the learnt clause

conflict

public void conflict(int[] clause)
Called when conflict happened at the clause by SAT solver.

Parameters:
clause - the clause

restart

public void restart()
Called when restart happened by SAT solver.


found

public void found()
Called when the solution was found by SAT solver.


end

public void end(boolean result)
Called when the result was returned from SAT solver.

Parameters:
result - the result of SAT (true) or UNSAT (false)

SugarTrace version 1.0.1 Core API Specification

SugarTracer: Tracer of Sugar