Sugar version 1.13 Core API Specification

jp.ac.kobe_u.cs.sugar.encoder
Class Encoder

java.lang.Object
  extended by jp.ac.kobe_u.cs.sugar.encoder.Encoder

public class Encoder
extends Object

Encoder encodes CSP into SAT.

See Also:
CSP

Field Summary
static int FALSE_CODE
           
static long MAX_SAT_SIZE
           
static int SAT_BUFFER_SIZE
           
static String satSolverName
           
static int TRUE_CODE
           
static boolean USE_NEWIO
           
 
Constructor Summary
Encoder(CSP csp)
           
 
Method Summary
 boolean decode(String outFileName)
           
 void encode(String satFileName, boolean incremental)
           
 void flush()
           
 String getHeader(int numOfVariables, int numOfClauses)
           
 int getSatClausesCount()
           
 long getSatFileSize()
           
 void modifySat(String satFileName, int[] clause)
           
 void modifySat(String satFileName, int[][] clauses)
           
static int negateCode(int code)
           
 void outputMap(String mapFileName)
           
 String summary()
           
 void write(String s)
           
 void writeClause(int[] clause)
           
 void writeClause(List<Integer> clause0)
           
 void writeComment(String comment)
           
 
Methods inherited from class java.lang.Object
equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Field Detail

satSolverName

public static String satSolverName

FALSE_CODE

public static final int FALSE_CODE
See Also:
Constant Field Values

TRUE_CODE

public static final int TRUE_CODE
See Also:
Constant Field Values

USE_NEWIO

public static boolean USE_NEWIO

SAT_BUFFER_SIZE

public static int SAT_BUFFER_SIZE

MAX_SAT_SIZE

public static long MAX_SAT_SIZE
Constructor Detail

Encoder

public Encoder(CSP csp)
Method Detail

negateCode

public static int negateCode(int code)

getSatClausesCount

public int getSatClausesCount()

getSatFileSize

public long getSatFileSize()

flush

public void flush()
           throws IOException
Throws:
IOException

write

public void write(String s)
           throws IOException
Throws:
IOException

writeComment

public void writeComment(String comment)
                  throws IOException
Throws:
IOException

writeClause

public void writeClause(int[] clause)
                 throws IOException
Throws:
IOException

writeClause

public void writeClause(List<Integer> clause0)
                 throws IOException
Throws:
IOException

getHeader

public String getHeader(int numOfVariables,
                        int numOfClauses)
                 throws UnsupportedEncodingException
Throws:
UnsupportedEncodingException

encode

public void encode(String satFileName,
                   boolean incremental)
            throws SugarException,
                   IOException
Throws:
SugarException
IOException

modifySat

public void modifySat(String satFileName,
                      int[][] clauses)
               throws IOException
Throws:
IOException

modifySat

public void modifySat(String satFileName,
                      int[] clause)
               throws IOException
Throws:
IOException

outputMap

public void outputMap(String mapFileName)
               throws SugarException,
                      IOException
Throws:
SugarException
IOException

decode

public boolean decode(String outFileName)
               throws SugarException,
                      IOException
Throws:
SugarException
IOException

summary

public String summary()

Sugar version 1.13 Core API Specification

Sugar: A SAT-based Constraint Solver