SugarTrace version 1.0.1 Core API Specification

sugartracer.decoder
Class Decoder

java.lang.Object
  extended by sugartracer.decoder.Decoder

public class Decoder
extends Object

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

Decoder

public Decoder(EncodingMap encodingMap)
Constructs the decoder using given encoding map

Parameters:
encodingMap - the encoding map

Decoder

public Decoder(String mapFileName)
        throws TracerException
Constructs the decoder using given map file

Parameters:
mapFileName - map file name
Throws:
TracerException
Method Detail

reset

public void reset()
Resets the decoder to initial state


getEncodingMap

public EncodingMap getEncodingMap()
Returns the encoding map

Returns:
the encoding map

getVariables

public List<Variable> getVariables()
Returns the list of SAT variables

Returns:
the list of SAT variables

getAssignment

public Assignment getAssignment()
Returns the current assignment

Returns:
the assignment

getDecisions

public Stack<Integer> getDecisions()
Returns the current decision stack

Returns:
the decision stack

getTrail

public Stack<Integer> getTrail()
Returns the current trail stack

Returns:
the trail stack

getLearnts

public List<int[]> getLearnts()
Returns the current learnt clauses

Returns:
the learnt clauses

getResult

public Boolean getResult()
Returns the result of SAT solving.

Returns:
the result

decode

public String decode(int lit)
              throws TracerException
Returns the string representation of the literal.

Parameters:
lit - the literal
Returns:
the string representation of the literal
Throws:
TracerException

decode

public List<String> decode(List<Integer> lits)
                    throws TracerException
Returns the list of string representations of literals

Parameters:
lits - literals
Returns:
the list of string representations
Throws:
TracerException

decode

public String[] decode(int[] lits)
                throws TracerException
Returns the array of string representations of literals

Parameters:
lits - literals
Returns:
the array of string representations
Throws:
TracerException

decodeClauses

public List<String[]> decodeClauses(List<int[]> clauses)
                             throws TracerException
Returns the list of string representations of clauses

Parameters:
clauses - clauses
Returns:
the list of string representations
Throws:
TracerException

getAssignmentDecoded

public List<String[]> getAssignmentDecoded(boolean includeAux)
Returns the string representation of the assignment.

Parameters:
includeAux - true to include aux variables
Returns:
the string representation of the assignment.

getDecisionsDecoded

public List<String> getDecisionsDecoded()
                                 throws TracerException
Returns the string representation of decision stack.

Returns:
the string representation of decision stack
Throws:
TracerException

getTrailDecoded

public List<String> getTrailDecoded()
                             throws TracerException
Returns the string representation of trail stack.

Returns:
the string representation of trail stack
Throws:
TracerException

getLearntsDecoded

public List<String[]> getLearntsDecoded()
                                 throws TracerException
Returns the string representation of learnt clauses.

Returns:
the string representation of learnt clauses
Throws:
TracerException

saveState

public void saveState()
               throws TracerException
Saves the current assignment.

Throws:
TracerException

decide

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

Parameters:
lit - the literal

propagate

public Variable propagate(int lit)
Called when propagation is done for the literal by SAT solver. It returns the variable when its domain is updated. The assignment is updated.

Parameters:
lit - the literal
Returns:
the variable when it is modified, otherwise null

undo

public void undo(int lit)
Called when undo is done for the literal by SAT solver. It cancels assignments not only the literal but also literals propagated after the decision on lit.

Parameters:
lit - the literal

backjump

public void backjump(int backjumpLevel)
Called when backjump is done by SAT solver. The decision stack is truncated to the backjumpLevel.

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. Currently it does nothing.

Parameters:
clause - the clause

restart

public void restart()
Called when restart happened by SAT solver. Currently it does nothing.


end

public void end(boolean result)
Called when the search was done by SAT solver.

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

SugarTrace version 1.0.1 Core API Specification

SugarTracer: Tracer of Sugar