public static interface ISatLibrary.ISATLIB
extends com.sun.jna.Library
修飾子とタイプ | メソッドと説明 |
---|---|
void |
isat_add_assumptions(com.sun.jna.Pointer solver,
int[] literals,
int length)
Adds assumption literals to SAT Solver at once.
|
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.
|
int |
isat_add_PB_with_assumption(com.sun.jna.Pointer solver,
int[] weights,
int[] literals,
int length,
int k,
boolean isgeq,
int assumption)
Adds PB constraint to the solver with assumption.
|
int |
isat_add_PB(com.sun.jna.Pointer solver,
int[] weights,
int[] literals,
int length,
int k,
boolean isgeq)
Adds PB constraint to the solver.
|
int |
isat_clauses(com.sun.jna.Pointer solver)
Gets the number of clauses of SAT solver.
|
void |
isat_clean(com.sun.jna.Pointer solver,
com.sun.jna.Pointer p)
Releases a pointer allocated native code.
|
com.sun.jna.ptr.IntByReference |
isat_failed(com.sun.jna.Pointer solver,
int[] literals,
int length)
Get result of assumption literals if each of them used proving unsatisfiability.
|
void |
isat_freeze(com.sun.jna.Pointer solver,
int literal)
Freezes a literal.
|
double |
isat_get_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_new_var(com.sun.jna.Pointer solver,
int howmany)
Sets SAT variables to SAT solver newly.
|
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.
|
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 solverint isat_clauses(com.sun.jna.Pointer solver)
solver
- the pointer to SAT solvervoid isat_new_var(com.sun.jna.Pointer solver, int howmany)
solver
- the pointer to SAT solverhowmany
- the number of SAT variables to add newlyvoid 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 arrayvoid isat_add_assumptions(com.sun.jna.Pointer solver, int[] literals, int length)
solver
- the pointer to SAT solverliterals
- the assumption literalslength
- the length of clauses arraycom.sun.jna.ptr.IntByReference isat_model(com.sun.jna.Pointer solver)
solver
- the pointer to SAT solvercom.sun.jna.ptr.IntByReference isat_failed(com.sun.jna.Pointer solver, int[] literals, int length)
solver
- the pointer to SAT solverliterals
- the literals of assumptionlength
- the length of literalsvoid 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 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 arrayint isat_add_PB(com.sun.jna.Pointer solver, int[] weights, int[] literals, int length, int k, boolean isgeq)
solver
- the pointer to SAT solverweights
- the weights of literalsliterals
- the literalslength
- the length of literalsk
- the rightside integerisgeq
- true (if constraint is greater or equal), false (otherwise)int isat_add_PB_with_assumption(com.sun.jna.Pointer solver, int[] weights, int[] literals, int length, int k, boolean isgeq, int assumption)
solver
- the pointer to SAT solverweights
- the weights of literalsliterals
- the literalslength
- the length of literalsk
- the rightside integerisgeq
- true (if constraint is greater or equal), false (otherwise)assumption
- the assumption literalvoid isat_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