public static interface ISatLibrary.ISATLIB
extends com.sun.jna.Library
修飾子とタイプ | フィールドと説明 |
---|---|
static ISatLibrary.ISATLIB |
INSTANCE |
修飾子とタイプ | メソッドと説明 |
---|---|
void |
isat_add_blocking_clause(com.sun.jna.Pointer solver,
int[] literals,
int length)
Adds blocking clause to restrict a certain solution.
|
void |
isat_add_clauses(com.sun.jna.Pointer solver,
int[] clauses,
int length)
Adds clause(s) to SAT solver.
|
void |
isat_clean(com.sun.jna.Pointer solver,
com.sun.jna.Pointer p)
Releases a pointer allocated native code.
|
double |
isat_get_time(com.sun.jna.Pointer solver)
Gets time of solving.
|
double |
isat_get_total_time(com.sun.jna.Pointer solver)
Gets elapsed time from invocation of SAT solver.
|
boolean |
isat_is_eliminated(com.sun.jna.Pointer solver,
int literal)
Checks if literal is frozen.
|
com.sun.jna.ptr.IntByReference |
isat_model(com.sun.jna.Pointer solver)
Gets assignments of all variables.
|
void |
isat_set_freeze(com.sun.jna.Pointer solver,
int literal)
Freezes a literal.
|
void |
isat_set_verbosity(com.sun.jna.Pointer solver,
int v)
Sets the verbosity of SAT solver's output.
|
int |
isat_vars(com.sun.jna.Pointer solver)
Gets the number of variables of SAT solver.
|
static final ISatLibrary.ISATLIB INSTANCE
void isat_set_verbosity(com.sun.jna.Pointer solver, int v)
solver
- the pointer to SAT solverv
- verbosityint isat_vars(com.sun.jna.Pointer solver)
solver
- the pointer to SAT solvervoid isat_add_clauses(com.sun.jna.Pointer solver, int[] clauses, int length)
solver
- the pointer to SAT solverclauses
- the array of clauseslength
- the length of clauses arraycom.sun.jna.ptr.IntByReference isat_model(com.sun.jna.Pointer solver)
solver
- the pointer to SAT solvervoid isat_clean(com.sun.jna.Pointer solver, com.sun.jna.Pointer p)
solver
- the pointer to SAT solverp
- the pointer required to releasedouble isat_get_time(com.sun.jna.Pointer solver)
solver
- the pointer to SAT solverdouble isat_get_total_time(com.sun.jna.Pointer solver)
solver
- the pointer to SAT solvervoid isat_add_blocking_clause(com.sun.jna.Pointer solver, int[] literals, int length)
solver
- the pointer to SAT solverliterals
- literalslength
- the length of literals arrayvoid isat_set_freeze(com.sun.jna.Pointer solver, int literal)
solver
- the pointer to SAT solverliteral
- the literal required to freezeboolean isat_is_eliminated(com.sun.jna.Pointer solver, int literal)
solver
- the pointer to SAT solverliteral
- the literal required to check if frozen