|
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.decoder.Decoder
public class Decoder
The class for decoding SAT solver information to CSP information.
Constructor Summary | |
---|---|
Decoder(EncodingMap encodingMap)
Constructs the decoder using given encoding map |
|
Decoder(String mapFileName)
Constructs the decoder using given map file |
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. |
String |
decode(int lit)
Returns the string representation of the literal. |
String[] |
decode(int[] lits)
Returns the array of string representations of literals |
List<String> |
decode(List<Integer> lits)
Returns the list of string representations of literals |
List<String[]> |
decodeClauses(List<int[]> clauses)
Returns the list of string representations of clauses |
void |
end(boolean result)
Called when the search was done by SAT solver. |
Assignment |
getAssignment()
Returns the current assignment |
List<String[]> |
getAssignmentDecoded(boolean includeAux)
Returns the string representation of the assignment. |
Stack<Integer> |
getDecisions()
Returns the current decision stack |
List<String> |
getDecisionsDecoded()
Returns the string representation of decision stack. |
EncodingMap |
getEncodingMap()
Returns the encoding map |
List<int[]> |
getLearnts()
Returns the current learnt clauses |
List<String[]> |
getLearntsDecoded()
Returns the string representation of learnt clauses. |
Boolean |
getResult()
Returns the result of SAT solving. |
Stack<Integer> |
getTrail()
Returns the current trail stack |
List<String> |
getTrailDecoded()
Returns the string representation of trail stack. |
List<Variable> |
getVariables()
Returns the list of SAT variables |
void |
learnt(int[] clause)
Called when learnt clause is added by SAT solver. |
Variable |
propagate(int lit)
Called when propagation is done for the literal by SAT solver. |
void |
reset()
Resets the decoder to initial state |
void |
restart()
Called when restart happened by SAT solver. |
void |
saveState()
Saves the current assignment. |
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 |
Constructor Detail |
---|
public Decoder(EncodingMap encodingMap)
encodingMap
- the encoding mappublic Decoder(String mapFileName) throws TracerException
mapFileName
- map file name
TracerException
Method Detail |
---|
public void reset()
public EncodingMap getEncodingMap()
public List<Variable> getVariables()
public Assignment getAssignment()
public Stack<Integer> getDecisions()
public Stack<Integer> getTrail()
public List<int[]> getLearnts()
public Boolean getResult()
public String decode(int lit) throws TracerException
lit
- the literal
TracerException
public List<String> decode(List<Integer> lits) throws TracerException
lits
- literals
TracerException
public String[] decode(int[] lits) throws TracerException
lits
- literals
TracerException
public List<String[]> decodeClauses(List<int[]> clauses) throws TracerException
clauses
- clauses
TracerException
public List<String[]> getAssignmentDecoded(boolean includeAux)
includeAux
- true to include aux variables
public List<String> getDecisionsDecoded() throws TracerException
TracerException
public List<String> getTrailDecoded() throws TracerException
TracerException
public List<String[]> getLearntsDecoded() throws TracerException
TracerException
public void saveState() throws TracerException
TracerException
public void decide(int lit)
lit
- the literalpublic Variable propagate(int lit)
lit
- the literal
public 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 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 |