|
SugarTrace version 1.0.1 Core API Specification |
||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Objectsugartracer.Tracer
public abstract class Tracer
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 |
---|
public SatSolver solver
public Decoder decoder
public List<Integer> propagations
public List<Integer> undos
public boolean done
public boolean showAuxVars
public boolean quick
public boolean debug
Constructor Detail |
---|
public Tracer(SatSolver solver, Decoder decoder)
decoder
- Method Detail |
---|
public abstract void show(String[] strs)
strs
- public void showCommand(String command, String[] args)
command
- public void showAssignment(Variable v)
v
- public void showAssignment()
public void startTracer() throws TracerException
TracerException
SatSolver.startSolver()
public void stopTracer() throws TracerException
TracerException
SatSolver.stopSolver()
public void decide(int lit)
lit
- the literalpublic void propagate(int lit)
lit
- the literalpublic void undo(int lit)
lit
- the literalpublic void backjump(int backjumpLevel)
backjumpLevel
- public void learnt(int[] clause)
clause
- the learnt clausepublic void conflict(int[] clause)
clause
- the clausepublic void restart()
public void found()
public void end(boolean result)
result
- the result of SAT (true) or UNSAT (false)
|
SugarTrace version 1.0.1 Core API Specification |
||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |